----------------------------------------------------------------- --- LISB is copyright 2005 by Steve Lauterburg and Andrew Lenharth ----------------------------------------------------------------- ----------------------------------------------------------------- --- LISP Syntax ------------------------------------------------- ----------------------------------------------------------------- ----------------------------------------------------------------- fmod NAME is protecting QID . sorts Name BuiltInName . subsort Qid < Name . subsort BuiltInName < Name . ops a b c d e f g h i j k l m n o p q r s u v w x y z : -> BuiltInName . --- the following represent builtin functions/macros and special symbols ops nil t : -> BuiltInName . ops append apply atom cond cons defun defvar eval expt funcall function if lambda let let* list print progn prog1 prog2 quote setf : -> BuiltInName . ops car cdr cadr first second rest : -> BuiltInName . ops endp fboundp integerp numberp zerop symbolp stringp consp listp null : -> BuiltInName . ops and not or &rest : -> BuiltInName . op Name2String : Name -> String . var Q : Qid . eq Name2String(Q) = "'" + string(Q) . --- special symbols eq Name2String(nil) = "nil" . eq Name2String(t) = "t" . --- builtin forms eq Name2String(append) = "append" . eq Name2String(apply) = "apply" . eq Name2String(atom) = "atom" . eq Name2String(cond) = "cond" . eq Name2String(cons) = "cons" . eq Name2String(defun) = "defun" . eq Name2String(defvar) = "defvar" . eq Name2String(eval) = "eval" . eq Name2String(expt) = "expt" . eq Name2String(funcall) = "funcall" . eq Name2String(function) = "function" . eq Name2String(if) = "if" . eq Name2String(lambda) = "lambda" . eq Name2String(let) = "let" . eq Name2String(let*) = "let*" . eq Name2String(list) = "list" . eq Name2String(print) = "print" . eq Name2String(progn) = "progn" . eq Name2String(prog1) = "prog1" . eq Name2String(prog2) = "prog2" . eq Name2String(quote) = "quote" . eq Name2String(setf) = "setf" . --- accessor forms eq Name2String(car) = "car" . eq Name2String(cadr) = "cadr" . eq Name2String(cdr) = "cdr" . eq Name2String(first) = "first" . eq Name2String(rest) = "rest" . eq Name2String(second) = "second" . --- predicate forms eq Name2String(endp) = "endp" . eq Name2String(fboundp) = "fboundp" . eq Name2String(integerp) = "integerp" . eq Name2String(numberp) = "numberp" . eq Name2String(zerop) = "zerop" . eq Name2String(symbolp) = "symbolp" . eq Name2String(stringp) = "stringp" . eq Name2String(consp) = "consp" . eq Name2String(listp) = "listp" . eq Name2String(null) = "null" . --- boolean expression forms eq Name2String(and) = "and" . eq Name2String(not) = "not" . eq Name2String(or) = "or" . eq Name2String(a) = "a" . eq Name2String(b) = "b" . eq Name2String(c) = "c" . eq Name2String(d) = "d" . eq Name2String(e) = "e" . eq Name2String(f) = "f" . eq Name2String(g) = "g" . eq Name2String(h) = "h" . eq Name2String(i) = "i" . eq Name2String(j) = "j" . eq Name2String(k) = "k" . eq Name2String(l) = "l" . eq Name2String(m) = "m" . eq Name2String(n) = "n" . eq Name2String(o) = "o" . eq Name2String(p) = "p" . eq Name2String(q) = "q" . eq Name2String(r) = "r" . eq Name2String(s) = "s" . eq Name2String(u) = "u" . eq Name2String(v) = "v" . eq Name2String(w) = "w" . eq Name2String(x) = "x" . eq Name2String(y) = "y" . eq Name2String(z) = "z" . endfm ----------------------------------------------------------------- fmod NAME-LIST is including NAME . protecting NAT . sort NameList . subsort Name < NameList . op `(`) : -> NameList . op _,_ : NameList NameList -> NameList [assoc id: ()] . op length : NameList -> Nat . vars X X' : Name . var XL : NameList . eq length(X,X',XL) = 1 + length(X',XL) . eq length(X) = 1 . eq length(()) = 0 . endfm ----------------------------------------------------------------- fmod WRAPPED-STRING is including STRING . sort WrappedString . op {_} : String -> WrappedString . endfm ----------------------------------------------------------------- fmod GENERIC-EXP-SYNTAX is including NAME-LIST . including INT . including WRAPPED-STRING . sort List ItemList Exp ExpList . subsorts Name Int WrappedString List < Exp < ItemList . subsorts Exp NameList < ExpList . --- constructors for ItemLists, ExpLists and Lists op __ : ItemList ItemList -> ItemList [assoc] . op _,_ : ExpList ExpList -> ExpList [ditto] . op [_] : ItemList -> List . op [] : -> List . eq [] = nil . endfm ----------------------------------------------------------------- fmod SHORTCUT-SYNTAX is including GENERIC-EXP-SYNTAX . var E : Exp . op $_ : Exp -> Exp . eq $ E = [quote E] . op #$_ : Exp -> Exp . eq #$ E = [function E] . op #'_ : Exp -> Exp . eq #' E = [function E] . endfm ----------------------------------------------------------------- fmod SEQ-COMP-SYNTAX is including GENERIC-EXP-SYNTAX . op __ : Exp Exp -> Exp [assoc] . endfm ----------------------------------------------------------------- fmod LISP-SYNTAX is including GENERIC-EXP-SYNTAX . including SHORTCUT-SYNTAX . including SEQ-COMP-SYNTAX . endfm ----------------------------------------------------------------- --- LISP Semantics ---------------------------------------------- ----------------------------------------------------------------- ----------------------------------------------------------------- fmod OUTPUT is including STRING . sorts Output . subsorts String < Output . op none : -> Output . op _:_ : Output Output -> Output [assoc id: none] . endfm ----------------------------------------------------------------- fmod LOCATION is including INT . sort Location . sort LocationList . subsort Location < LocationList . op loc : Nat -> Location . op nill : -> LocationList . op _,_ : LocationList LocationList -> LocationList [assoc id: nill] . op locs : Nat Nat -> LocationList . vars N # : Nat . eq locs(N, 0) = nill . eq locs(N, #) = loc(N), locs(N + 1, # - 1) . endfm ----------------------------------------------------------------- fmod ENVIRONMENT is including NAME-LIST . including LOCATION . sort Env . op empty : -> Env . op [_,_] : Name Location -> Env . op __ : Env Env -> Env [assoc comm id: empty] . op _[_] : Env Name -> Location . op _[_<-_] : Env Name Location -> Env . var X : Name . var Env : Env . vars L L' : Location . eq ([X,L] Env)[X] = L . eq ([X,L] Env)[X <- L'] = ([X,L'] Env) . eq Env[X <- L] = (Env [X,L]) [owise] . endfm ----------------------------------------------------------------- fmod VALUE is sort Value . op nothing : -> Value . endfm ----------------------------------------------------------------- fmod VALUE-LIST is including VALUE . protecting INT . sort ValueList . subsorts Value < ValueList . op nill : -> ValueList . op _,_ : ValueList ValueList -> ValueList [assoc id: nill] . op firstN : ValueList Nat -> ValueList . op restN : ValueList Nat -> ValueList . vars V V' : Value . var VL : ValueList . var N : NzNat . eq firstN((V,VL), N) = V,firstN(VL, (N - 1)) . eq firstN(VL, 0) = nill . eq restN((V,VL), N) = restN(VL, N - 1) . eq restN(VL, 0) = VL . endfm ------------------------------------------------------------- fmod CONS-CELL is sort ConsCell . including LOCATION . op {_._} : Location Location -> ConsCell . endfm ----------------------------------------------------------------- fmod STORE is including LOCATION . including VALUE-LIST . sort Store . op empty : -> Store . op [_,_] : Location Value -> Store . op __ : Store Store -> Store [assoc comm id: empty] . op _[_] : Store Location -> Value . op _[_<-_] : Store Location Value -> Store . var L : Location . var Mem : Store . vars Pv Pv' : Value . eq ([L,Pv] Mem)[L] = Pv . eq ([L,Pv] Mem)[L <- Pv'] = ([L,Pv'] Mem) . eq Mem[L <- Pv'] = (Mem [L,Pv']) [owise] . endfm ----------------------------------------------------------------- fmod CONTINUATION is sorts Continuation ContinuationItem . op stop : -> Continuation . op _->_ : ContinuationItem Continuation -> Continuation . endfm ----------------------------------------------------------------- fmod STATE is sorts PLStateAttribute PLState . subsort PLStateAttribute < PLState . including ENVIRONMENT . including STORE . including CONTINUATION . including OUTPUT . op empty : -> PLState . op __ : PLState PLState -> PLState [assoc comm id: empty] . op k : Continuation Store -> PLStateAttribute . op nextLoc : Nat -> PLStateAttribute . op env : Env -> PLStateAttribute . op globalenv : Env -> PLStateAttribute . op globalfenv : Env -> PLStateAttribute . op output : Output -> PLStateAttribute . op lastaloc : Location -> PLStateAttribute . endfm ------------------------------------------------------------- fmod INTTOSTRING is protecting CONVERSION . protecting INT . protecting STRING . op inttostring : Int -> String . var N : Int . var S : String . eq inttostring(N) = string(N,10) . endfm ----------------------------------------------------------------- fmod HELPING-OPERATIONS is including CONS-CELL . including NAME-LIST . including GENERIC-EXP-SYNTAX . including STATE . var X : Name . vars E E' : Exp . var El : ExpList . var K : Continuation . vars V : Value . var Vl : ValueList . var Xl : NameList . var L : Location . var Ll : LocationList . vars Env Env' : Env . var Mem : Store . var N : Nat . --- Value Types op int : Int -> Value . op string : String -> Value . op symbol : Name -> Value . op cell : ConsCell -> Value . op fbuiltin : Name -> Value . op mbuiltin : Name -> Value . op fclosure : NameList ValueList Env -> Value . op mclosure : NameList ValueList -> Value . op _->_ : Location Continuation -> Continuation . op _->_ : ExpList Continuation -> Continuation . op _->_ : ValueList Continuation -> Continuation . eq k(E,E',El -> K, Mem) = k(E -> E',El -> K, Mem) . eq k(V -> El -> K, Mem) = k(El -> V -> K, Mem) . eq k(Vl -> V -> K, Mem) = k(V,Vl -> K, Mem) . op _->_ : Env Continuation -> Continuation . eq k(Vl -> Env -> K, Mem) env(Env') = k(Vl -> K, Mem) env(Env) . op discard : -> ContinuationItem . eq k(V -> discard -> K, Mem) = k(K, Mem) . --- Regular Binds and Assignments op bindTo_ : NameList -> ContinuationItem . eq k(V,Vl -> bindTo(X,Xl) -> K, Mem) env(Env) nextLoc(N) = k(Vl -> bindTo(Xl) -> K, Mem[loc(N),V]) env(Env[X <- loc(N)]) nextLoc(N + 1) . eq k((nill).ValueList -> bindTo () -> K, Mem) = k(K, Mem) . eq k((nill).ValueList -> bindTo nil -> K, Mem) = k(K, Mem) . op assignTo_ : NameList -> ContinuationItem . eq k((V,Vl) -> assignTo(X,Xl) -> K, Mem) env([X,L] Env) = k(Vl -> assignTo(Xl) -> K, Mem[L <- V]) env([X,L] Env) . eq k((nill).ValueList -> assignTo() -> K, Mem) = k(K, Mem) . --- Global Environment Binds and Assignments op globalBindTo_ : NameList -> ContinuationItem . eq k(V,Vl -> globalBindTo(X,Xl) -> K, Mem) globalenv(Env) nextLoc(N) = k(Vl -> globalBindTo(Xl) -> K, Mem[loc(N),V]) globalenv(Env[X <- loc(N)]) nextLoc(N + 1) . eq k((nill).ValueList -> globalBindTo() -> K, Mem) = k(K, Mem) . op globalAssignTo_ : NameList -> ContinuationItem . eq k((V,Vl) -> globalAssignTo(X,Xl) -> K, Mem) globalenv([X,L] Env) = k(Vl -> globalAssignTo(Xl) -> K, Mem[L <- V]) globalenv([X,L] Env) . eq k((nill).ValueList -> globalAssignTo() -> K, Mem) = k(K, Mem) . --- Global Function Environment Binds and Assignments op globalFBindTo_ : NameList -> ContinuationItem . eq k(V,Vl -> globalFBindTo(X,Xl) -> K, Mem) globalfenv(Env) nextLoc(N) = k(Vl -> globalFBindTo(Xl) -> K, Mem[loc(N) <- V]) globalfenv(Env[X <- loc(N)]) nextLoc(N + 1) . eq k((nill).ValueList -> globalFBindTo() -> K, Mem) = k(K, Mem) . op globalFAssignTo_ : NameList -> ContinuationItem . eq k((V,Vl) -> globalFAssignTo(X,Xl) -> K, Mem) globalfenv([X,L] Env) = k(Vl -> globalFAssignTo(Xl) -> K, Mem[L <- V]) globalfenv([X,L] Env) . eq k((nill).ValueList -> globalFAssignTo() -> K, Mem) = k(K, Mem) . --- Direct Location Assignment op assignToLoc : LocationList -> ContinuationItem . eq k((V,Vl) -> assignToLoc(L,Ll) -> K, Mem) = k(Vl -> assignToLoc(Ll) -> K, Mem[L <- V]) . eq k((nill).ValueList -> assignToLoc((nill).LocationList) -> K, Mem) = k(K, Mem) . endfm ----------------------------------------------------------------- fmod CODE-UTILS is including HELPING-OPERATIONS . op _[_ <- _] : Value Name Value -> ContinuationItem . op dup : Value -> ContinuationItem . op mkpair : -> ContinuationItem . op mkpair : Value -> ContinuationItem . ops makeConsCell : -> ContinuationItem . ops makeConsCell2 : -> ContinuationItem . var I : Int . vars X X' : Name . var S : String . var K : Continuation . vars V V' V1 V2 : Value . var Mem : Store . var N : Nat . var VL : ValueList . vars L1 L2 : Location . var KI : ContinuationItem . --- Beta Substitution code eq k(symbol(X)[X <- V] -> K, Mem) = k(dup(V) -> K, Mem) . ceq k(symbol(X')[X <- V] -> K, Mem) = k(symbol(X') -> K, Mem) if X =/= X' . eq k(int(I)[X <- V] -> K, Mem) = k(int(I) -> K, Mem) . eq k(string(S)[X <- V] -> K, Mem) = k(string(S) -> K, Mem) . eq k(cell({L1 . L2})[X <- V] -> K, Mem) = k(Mem[L1][X <- V] -> Mem[L2][X <- V] -> mkpair -> K, Mem) . ---List duplication eq k(dup(symbol(X)) -> K, Mem) = k(symbol(X) -> K, Mem) . eq k(dup(int(I)) -> K, Mem) = k(int(I) -> K, Mem) . eq k(dup(string(S)) -> K, Mem) = k(string(S) -> K, Mem) . eq k(dup(cell({L1 . L2})) -> K, Mem) = k(dup(Mem[L1]) -> dup(Mem[L2]) -> mkpair -> K, Mem) . ---ConsCell Making with evaluation eq k(V1 -> KI -> mkpair -> K, Mem) = k(KI -> mkpair(V1) -> K, Mem) . eq k(V2 -> mkpair(V1) -> K, Mem) = k((V1,V2) -> makeConsCell -> K, Mem) . --- make cons cell from (head,tail) value list eq k((V,V') -> makeConsCell -> K, Mem) nextLoc(N) = k((V,V') -> assignToLoc(locs(N, 2)) -> cell({loc(N) . loc(N + 1)}) -> K, Mem) nextLoc(N + 2) . --- make cons cell from (tail,head) value list eq k((V,V') -> makeConsCell2 -> K, Mem) = k((V',V) -> makeConsCell -> K, Mem) . ---List of name pulling apart code op list2Names : Value Store -> NameList . eq list2Names(cell({L1 . L2}), (Mem [L1,symbol(X)] [L2,V2])) = if (V2 == symbol(nil)) then X else (X, list2Names(V2, (Mem [L1,symbol(X)] [L2,V2]))) fi . ---List of values pulling apart code op list2Values : Value Store -> ValueList . eq list2Values(cell({L1 . L2}), (Mem [L2,V2])) = if (V2 == symbol(nil)) then Mem[L1] else ((Mem[L1]), list2Values(V2, (Mem [L2,V2]))) fi . eq list2Values(symbol(nil), Mem) = nill . ---List restructuring code op values2List : ValueList -> ContinuationItem . eq k(values2List(V) -> K, Mem) = k(symbol(nil) -> mkpair(V) -> K, Mem) . eq k(values2List(V1,V2,VL) -> K, Mem) = k(V1 -> values2List(V2,VL) -> mkpair -> K, Mem) . eq k(values2List(nill) -> K, Mem) = k(symbol(nil) -> K, Mem) . endfm ----------------------------------------------------------------- fmod EVAL-SEMANTICS is including HELPING-OPERATIONS . including CODE-UTILS . op evalk : -> ContinuationItem . op evalf : Name -> ContinuationItem . op preapply : ValueList -> ContinuationItem . op preeval(_;_) : ValueList ValueList -> ContinuationItem . op apply : ValueList -> ContinuationItem . var C : ConsCell . vars VL VL' : ValueList . vars V V1 V2 : Value . vars L1 L2 : Location . var Env : Env . var Mem : Store . var K : Continuation . vars I1 I2 : Int . var X : Name . var Xl : NameList . var S : String . --- eval an expression eq k(apply(fbuiltin(eval), V) -> K, Mem) = k(V -> evalk -> K, Mem) . --- k-evaluate the different value types eq k(symbol(X) -> evalk -> K, Mem) = k(X -> K, Mem) . eq k(int(I1) -> evalk -> K, Mem) = k(int(I1) -> K, Mem) . eq k(string(S) -> evalk -> K, Mem) = k(string(S) -> K, Mem) . eq k(cell(C) -> evalk -> K, Mem) = k(preapply(list2Values(cell(C),Mem)) -> K, Mem) . eq k((V1, V2, VL) -> evalk -> K, Mem) = k(V1 -> evalk -> discard -> (V2, VL) -> evalk -> K, Mem) . --- preapply evaluates the car of the form --- if it is a symbol, the form is a macro form or function form eq k(preapply(symbol(X),VL) -> K, Mem) = k(evalf(X) -> preapply(VL) -> K, Mem) . eq k(evalf(X) -> K, Mem) globalfenv(Env) = k(Mem[Env[X]] -> K, Mem) globalfenv(Env) . --- if it is not a symbol, the form must be a lambda form eq k(preapply(V,VL) -> K, Mem) = k(V -> evalk -> preapply(VL) -> K, Mem) [owise] . --- if the first symbol is a builtin or user-defined macro, --- then extract but do not evaluate the remaining arguments eq k(mbuiltin(X) -> preapply(VL) -> K, Mem) = k(apply(mbuiltin(X), VL) -> K, Mem) . eq k(mclosure(Xl,VL) -> preapply(VL') -> K, Mem) = k(apply(mclosure(Xl,VL), VL') -> K, Mem) . --- if the first symbol is a builtin or user-defined function, --- then extract and evaluate the remaining arguments eq k(fbuiltin(X) -> preapply(VL) -> K, Mem) = k(preeval(fbuiltin(X); VL) -> K, Mem) . eq k(fclosure(Xl,VL,Env) -> preapply(VL') -> K, Mem) = k(preeval(fclosure(Xl,VL,Env); VL') -> K, Mem) . --- preeval extracts a list of arguments and evaluates them --- when there are no more arguments apply the function eq k(preeval(VL ; V,VL') -> K, Mem) = k(V -> evalk -> preeval(VL ; VL') -> K, Mem) . eq k(V1 -> preeval(VL ; VL') -> K, Mem) = k(preeval(VL,V1 ; VL') -> K, Mem) . eq k(preeval(VL ; nill) -> K, Mem) = k(apply(VL) -> K, Mem) . endfm ----------------------------------------------------------------- fmod GENERIC-EXP-SEMANTICS is including EVAL-SEMANTICS . including CODE-UTILS . ops makeConsList : ItemList Value -> ContinuationItem . var I : Int . var X : Name . var S : String . var L : Location . var V : Value . var K : Continuation . vars Env Genv : Env . var Mem : Store . var C : ConsCell . var Li : List . var IL : ItemList . var E : Exp . --- process an item list with multiple expressions eq k(makeConsList(IL E,V) -> K, Mem) = k(makeConsList(E,V) -> makeConsList(IL,symbol(nil)) -> K, Mem) . eq k(V -> makeConsList(IL,symbol(nil)) -> K, Mem) = k(makeConsList(IL,V) -> K, Mem) . --- process an item list with one expression eq k(makeConsList(X,V) -> K, Mem) = k((symbol(X),V) -> makeConsCell -> K, Mem) . eq k(makeConsList(I,V) -> K, Mem) = k((int(I),V) -> makeConsCell -> K, Mem) . eq k(makeConsList({S},V) -> K, Mem) = k((string(S),V) -> makeConsCell -> K, Mem) . eq k(makeConsList([IL],V) -> K, Mem) = k(makeConsList(IL,symbol(nil)) -> V -> makeConsCell2 -> K, Mem) . --- Integer evaluation eq k(I -> K, Mem) = k(int(I) -> K, Mem) . --- String evaluation eq k({S} -> K, Mem) = k(string(S) -> K, Mem) . --- Symbol evaluation: --- search for symbol in current environment --- if not found, search in global environment eq k(nil -> K, Mem) = k(symbol(nil) -> K, Mem) . eq k(t -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(X -> K, Mem) env([X,L] Env) = k(Mem[L] -> K, Mem) env([X,L] Env) . eq k(X -> K, Mem) globalenv([X,L] Genv) = k(Mem[L] -> K, Mem) globalenv([X,L] Genv) [owise] . --- Form evaluation eq k([IL] -> K, Mem) = k(makeConsList(IL,symbol(nil)) -> evalk -> K, Mem) . endfm ----------------------------------------------------------------- fmod QUOTE-SEMANTICS is including EVAL-SEMANTICS . var V : Value . var K : Continuation . var Mem : Store . eq k(apply(mbuiltin(quote), V) -> K, Mem) = k(dup(V) -> K, Mem) . endfm ----------------------------------------------------------------- fmod ARITHMETIC-EXP-SEMANTICS is including EVAL-SEMANTICS . var K : Continuation . vars I1 I2 : Int . var Mem : Store . eq k(apply(fbuiltin('+), int(I1), int(I2)) -> K, Mem) = k(int(I1 + I2) -> K, Mem) . eq k(apply(fbuiltin('-), int(I1), int(I2)) -> K, Mem) = k(int( (I1 + (- I2)) ) -> K, Mem) . eq k(apply(fbuiltin('/), int(I1), int(I2)) -> K, Mem) = k(int(I1 quo I2) -> K, Mem) . eq k(apply(fbuiltin('*), int(I1), int(I2)) -> K, Mem) = k(int(I1 * I2) -> K, Mem) . eq k(apply(fbuiltin(expt), int(I1), int(I2)) -> K, Mem) = k(int(I1 ^ I2) -> K, Mem) . endfm ----------------------------------------------------------------- fmod BOOLEAN-EXP-SEMANTICS is including EVAL-SEMANTICS . var K : Continuation . var VL : ValueList . var V V' : Value . vars I1 I2 : Int . var Mem : Store . --- not eq k(apply(fbuiltin(not), symbol(nil)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(not), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- and eq k(apply(mbuiltin(and)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(mbuiltin(and), V, VL) -> K, Mem) = k(V -> evalk -> apply(mbuiltin(and), VL) -> K, Mem) . --- if argument evaluates to nil, stop precessing and return nil eq k(symbol(nil) -> apply(mbuiltin(and), V, VL) -> K, Mem) = k(symbol(nil) -> K, Mem) . --- else keep processing eq k(V' -> apply(mbuiltin(and), V, VL) -> K, Mem) = k(apply(mbuiltin(and), V, VL) -> K, Mem) [owise] . --- if all arguments have been evaluated, return the last value eq k(V' -> apply(mbuiltin(and), nill) -> K, Mem) = k(V' -> K, Mem) . --- or eq k(apply(mbuiltin(or)) -> K, Mem) = k(symbol(nil) -> K, Mem) . eq k(apply(mbuiltin(or), V, VL) -> K, Mem) = k(V -> evalk -> apply(mbuiltin(or), VL) -> K, Mem) . --- if argument evaluates to nil, keep processing eq k(symbol(nil) -> apply(mbuiltin(or), V, VL) -> K, Mem) = k(apply(mbuiltin(or), V, VL) -> K, Mem) . --- else return the first non-nil value eq k(V' -> apply(mbuiltin(or), V, VL) -> K, Mem) = k(V' -> K, Mem) [owise] . --- if all arguments have been evaluated, return the last value eq k(V' -> apply(mbuiltin(or), nill) -> K, Mem) = k(V' -> K, Mem) . --- number comparison eq k(apply(fbuiltin('=), int(I1), int(I2)) -> K, Mem) = k(if I1 == I2 then symbol(t) else symbol(nil) fi -> K, Mem) . eq k(apply(fbuiltin('/=), int(I1), int(I2)) -> K, Mem) = k(if I1 == I2 then symbol(nil) else symbol(t) fi -> K, Mem) . eq k(apply(fbuiltin('<), int(I1), int(I2)) -> K, Mem) = k(if I1 < I2 then symbol(t) else symbol(nil) fi -> K, Mem) . eq k(apply(fbuiltin('>), int(I1), int(I2)) -> K, Mem) = k(if I1 > I2 then symbol(t) else symbol(nil) fi -> K, Mem) . eq k(apply(fbuiltin('<=), int(I1), int(I2)) -> K, Mem) = k(if I1 <= I2 then symbol(t) else symbol(nil) fi -> K, Mem) . eq k(apply(fbuiltin('>=), int(I1), int(I2)) -> K, Mem) = k(if I1 >= I2 then symbol(t) else symbol(nil) fi -> K, Mem) . endfm ----------------------------------------------------------------- fmod DEFVAR-SEMANTICS is including EVAL-SEMANTICS . var X : Name . var V : Value . var Mem : Store . var K : Continuation . vars Env GEnv : Env . var L : Location . --- if the symbol exists as a variable in the current environment, --- return the symbol without changing the value. eq k(apply(mbuiltin(defvar), symbol(X), V) -> K, Mem) env([X,L] Env) globalenv(GEnv) = k(V -> evalk -> discard -> symbol(X) -> K, Mem) env([X,L] Env) globalenv(GEnv) . --- else if the symbol exists as a variable in the global environment, --- return the symbol without changing the value. eq k(apply(mbuiltin(defvar), symbol(X), V) -> K, Mem) env(Env) globalenv([X,L] GEnv) = k(V -> evalk -> discard -> symbol(X) -> K, Mem) env(Env) globalenv([X,L] GEnv) . --- else create a new variable in the global environment with the --- value of the evaluated argument V. eq k(apply(mbuiltin(defvar), symbol(X), V) -> K, Mem) env(Env) globalenv(GEnv) = k(V -> evalk -> globalBindTo(X) -> symbol(X) -> K, Mem) env(Env) globalenv(GEnv) [owise] . endfm ----------------------------------------------------------------- fmod SETF-SEMANTICS is including EVAL-SEMANTICS . vars X X1 X2 : Name . vars V V1 V2 V3 : Value . vars C1 C2 : ConsCell . var VL : ValueList . var K : Continuation . vars Env GEnv : Env . var L L1 L2 : Location . var Mem : Store . --- setf allows multiple assignments... handle one at a time. eq k(apply(mbuiltin(setf), V1, V2, V3, VL) -> K, Mem) = k(apply(mbuiltin(setf), V1, V2) -> discard -> apply(mbuiltin(setf), V3, VL) -> K, Mem) . --- handle setf with no arguments eq k(apply(mbuiltin(setf),nill) -> K, Mem) = k(symbol(nil) -> K, Mem) . --- if the symbol exists as a variable in the current environment, --- change the value and return the value. eq k(apply(mbuiltin(setf), symbol(X), V) -> K, Mem) env([X,L] Env) globalenv(GEnv) = k(V -> evalk -> assignTo(X) -> X -> K, Mem) env([X,L] Env) globalenv(GEnv) . --- else if the symbol exists as a variable in the global environment, --- change the value and return the value. eq k(apply(mbuiltin(setf), symbol(X), V) -> K, Mem) env(Env) globalenv([X,L] GEnv) = k(V -> evalk -> globalAssignTo(X) -> X -> K, Mem) env(Env) globalenv([X,L] GEnv) . --- else create a new variable in the global environment with the --- value of the expression. eq k(apply(mbuiltin(setf), symbol(X), V) -> K, Mem) env(Env) globalenv(GEnv) = k(V -> evalk -> globalBindTo(X) -> X -> K, Mem) env(Env) globalenv(GEnv) [owise] . --- handle accessors (i.e., function forms that can be used as a place) op handacc : Value -> ContinuationItem . op setfacc : -> ContinuationItem . --- evaluate the accessor eq k(apply(mbuiltin(setf), cell({L1 . L2}), V) -> K, Mem) = k(cell({L1 . L2}) -> evalk -> handacc(V) -> K, Mem) . --- save the last accessor location and evaluate the expression eq k(V1 -> handacc(V) -> K, Mem) lastaloc(L) = k(V -> evalk -> L -> setfacc -> K, Mem) lastaloc(L) . --- update the accessor location with the expression's value eq k(V -> L -> setfacc -> K, Mem) = k(V -> assignToLoc(L) -> V -> K, Mem) . endfm ----------------------------------------------------------------- fmod ACCESSOR-SEMANTICS is including EVAL-SEMANTICS . vars V V' : Value . vars L L' L'' : Location . var K : Continuation . var Mem : Store . --- car value eq k(apply(fbuiltin(car), cell({L . L'})) -> K, Mem) lastaloc(L'') = k((Mem[L]) -> K, Mem) lastaloc(L) . eq k(apply(fbuiltin(car), symbol(nil)) -> K, Mem) = k(symbol(nil) -> K, Mem) . --- cdr value eq k(apply(fbuiltin(cdr), cell({L . L'})) -> K, Mem) lastaloc(L'') = k((Mem[L']) -> K, Mem) lastaloc(L'). eq k(apply(fbuiltin(cdr), symbol(nil)) -> K, Mem) = k(symbol(nil) -> K, Mem) . endfm ----------------------------------------------------------------- fmod PREDICATE-SEMANTICS is including EVAL-SEMANTICS . var I : Int . var X : Name . var S : String . var C : ConsCell . var V : Value . vars L L' : Location . var K : Continuation . var Mem : Store . var Env : Env . --- integerp eq k(apply(fbuiltin(integerp), int(I)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(integerp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- numberp eq k(apply(fbuiltin(numberp), int(I)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(numberp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- zerop eq k(apply(fbuiltin(zerop), int(0)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(zerop), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- symbolp eq k(apply(fbuiltin(symbolp), symbol(X)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(symbolp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- stringp eq k(apply(fbuiltin(stringp), string(S)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(stringp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- consp eq k(apply(fbuiltin(consp), cell(C)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(consp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- listp eq k(apply(fbuiltin(listp), cell(C)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(listp), symbol(nil)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(listp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- null eq k(apply(fbuiltin(null), V) -> K, Mem) = k(if V == symbol(nil) then symbol(t) else symbol(nil) fi -> K, Mem) . *** eq k(apply(fbuiltin(null), symbol(nil)) -> K, Mem) = k(symbol(t) -> K, Mem) . *** eq k(apply(fbuiltin(null), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- endp eq k(apply(fbuiltin(endp), symbol(nil)) -> K, Mem) = k(symbol(t) -> K, Mem) . eq k(apply(fbuiltin(endp), V) -> K, Mem) = k(symbol(nil) -> K, Mem) [owise] . --- fboundp eq k(apply(fbuiltin(fboundp), symbol(X)) -> K, Mem) globalfenv ([X,L] Env) = k(symbol(t) -> K, Mem) globalfenv ([X,L] Env) . eq k(apply(fbuiltin(fboundp), V) -> K, Mem) globalfenv(Env) = k(symbol(nil) -> K, Mem) globalfenv(Env) [owise] . endfm ----------------------------------------------------------------- --- this module is currently being overridden by a lisp-based --- version of the list function in the initialization module ----------------------------------------------------------------- fmod LIST-SEMANTICS is including EVAL-SEMANTICS . op listc : Value -> ContinuationItem . vars V V' : Value . var VL : ValueList . var K : Continuation . var Mem : Store . --- when there are no arguments, return nil (i.e. the empty list) eq k(apply(fbuiltin(list), nill) -> K, Mem) = k(symbol(nil) -> K, Mem) . eq k(apply(fbuiltin(list), V, VL) -> K, Mem) = k(apply(fbuiltin(list), VL) -> listc(V) -> K, Mem) . eq k(V -> listc(V') -> K, Mem) = k((V',V) -> makeConsCell -> K, Mem) . endfm ----------------------------------------------------------------- fmod CONS-SEMANTICS is including EVAL-SEMANTICS . vars V1 V2 : Value . var C : ConsCell . var K : Continuation . var Mem : Store . eq k(apply(fbuiltin(cons), V1, V2) -> K, Mem) = k((V1, V2) -> makeConsCell -> K, Mem) . endfm ----------------------------------------------------------------- fmod APPEND-SEMANTICS is including EVAL-SEMANTICS . op app : Value -> ContinuationItem . op app2 : Value ConsCell -> ContinuationItem . vars V V1 V2 : Value . var C : ConsCell . var K : Continuation . var Mem : Store . vars L1 L2 L1' L2' : Location . --- if the first list is empty, just return the second item eq k(apply(fbuiltin(append), symbol(nil), V) -> K, Mem) = k(V -> K, Mem) . --- append is non-destructive, so copy the first list eq k(apply(fbuiltin(append), cell(C), V) -> K, Mem) = k(dup(cell(C)) -> app(V) -> K, Mem) . --- traverse the first list (the copy) to the tail item. --- then replace the tail with the second item eq k(cell(C) -> app(V) -> K, Mem) = k(cell(C) -> app2(V,C) -> K, Mem) . eq k(cell({L1 . L2}) -> app2(V,C) -> K, Mem[L2,cell({L1' . L2'})]) = k(cell({L1' . L2'}) -> app2(V,C) -> K, Mem[L2,cell({L1' . L2'})]) . eq k(cell({L1 . L2}) -> app2(V,C) -> K, Mem [L2,V2]) = k(cell(C) -> K, Mem [L2,V]) [owise] . endfm ------------------------------------------------------------- fmod PRINT-SEMANTICS is including GENERIC-EXP-SEMANTICS . including EVAL-SEMANTICS . including INTTOSTRING . var X : Name . var I : Int . vars S S' : String . vars L1 L2 : Location . vars V V1 V2 : Value . var C : ConsCell . var K : Continuation . var Mem : Store . var B : Bool . var O : Output . var IL : ItemList . var XL : NameList . var VL : ValueList . var Env : Env . --- the tostring arg indicates whether to print [ and ] when a cell is seen op tostring : Bool -> ContinuationItem . op prepend : -> ContinuationItem . op prepend : String -> ContinuationItem . op append : String -> ContinuationItem . op printnext : -> ContinuationItem . eq k(apply(fbuiltin(print), V) -> K, Mem) = k(V -> tostring(true) -> printnext -> K, Mem) . eq k(fbuiltin(X) -> tostring(true) -> K, Mem) = k({ "" } -> K, Mem) . eq k(fbuiltin(X) -> tostring(false) -> K, Mem) = k({ ". " } -> K, Mem) . eq k(fclosure(XL,VL,Env) -> tostring(true) -> K, Mem) = k({ "" } -> K, Mem) . eq k(fbuiltin(X) -> tostring(false) -> K, Mem) = k({ ". " } -> K, Mem) . eq k(mclosure(XL,V) -> tostring(true) -> K, Mem) = k({ "" } -> K, Mem) . eq k(fbuiltin(X) -> tostring(false) -> K, Mem) = k({ ". " } -> K, Mem) . eq k(mbuiltin(X) -> tostring(true) -> K, Mem) = k({ "" } -> K, Mem) . eq k(mbuiltin(X) -> tostring(false) -> K, Mem) = k({ ". " } -> K, Mem) . eq k(int(I) -> tostring(true) -> K, Mem) = k({inttostring(I)} -> K, Mem) . eq k(int(I) -> tostring(false) -> K, Mem) = k(string(". " + inttostring(I)) -> K, Mem) . eq k(symbol(X) -> tostring(true) -> K, Mem) = k({ Name2String(X) } -> K, Mem) . eq k(symbol(X) -> tostring(false) -> K, Mem) = if X == nil then k(string("") -> K, Mem) else k({ ". " + Name2String(X) } -> K, Mem) fi . eq k(string(S) -> tostring(true) -> K, Mem) = k(string("{" + S + "}") -> K, Mem) . eq k(string(S) -> tostring(false) -> K, Mem) = k(string(". " + S) -> K, Mem) . eq k(cell({L1 . L2}) -> tostring(false) -> K, Mem) = k(Mem[L1] -> tostring(true) -> prepend -> Mem[L2] -> tostring(false) -> K, Mem) . eq k(cell({L1 . L2}) -> tostring(true) -> K, Mem) = k(string("[") -> prepend -> Mem[L1] -> tostring(true) -> prepend -> Mem[L2] -> tostring(false) -> append("]") -> K, Mem) . eq k(string(S) -> prepend -> V2 -> tostring(B) -> K, Mem) = k(V2 -> tostring(B) -> prepend(S) -> K, Mem) . --- include a space when appending except when starting lists eq k(string(S') -> prepend("[") -> K, Mem) = k(string("[" + S') -> K, Mem) . eq k(string("") -> prepend(S) -> K, Mem) = k(string(S) -> K, Mem) . eq k(string(S') -> prepend(S) -> K, Mem) = k(string(S + " " + S') -> K, Mem) [owise] . --- include a space when appending except when closing lists eq k(string(S') -> append("]") -> K, Mem) = k(string(S' + "]") -> K, Mem) . eq k(string(S') -> append(S) -> K, Mem) = k(string(S' + " " + S) -> K, Mem) [owise] . --- append final string to the output list eq k(string(S) -> printnext -> K, Mem) output(O) = k(symbol(nil) -> K, Mem) output(O : S ) . endfm ----------------------------------------------------------------- fmod LET-SEMANTICS is including EVAL-SEMANTICS . op extractbindings(_;_) : ValueList Value -> ContinuationItem . op processbindings(_;_;_) : NameList ValueList Value -> ContinuationItem . op evalvalues(_;_;_) : NameList ValueList ValueList -> ContinuationItem . var CA : ConsCell . var K : Continuation . var Env : Env . var Mem : Store . vars L1 L2 L1' L2' : Location . var X : Name . var XL : NameList . vars V V1 V2 V1' : Value . vars VL VL' VB : ValueList . eq k(apply(mbuiltin(let), cell(CA), VL) -> K, Mem) env(Env) = k(extractbindings(nill ; cell(CA)) -> VL -> evalk -> Env -> K, Mem) env(Env) . eq k(apply(mbuiltin(let), symbol(nil), VL) -> K, Mem) = k(VL -> evalk -> K, Mem) . --- extract each binding pair (symbol initform) from the list ***>FIXME: Mem interaction eq k(extractbindings(VB ; cell({L1 . L2})) -> K, Mem[L1,V1] [L2,V2]) = k(extractbindings(VB,V1 ; V2) -> K, Mem[L1,V1] [L2,V2]) . eq k(extractbindings(VB ; symbol(nil)) -> K, Mem) = k(processbindings(() ; nill ; VB) -> K, Mem) . --- separate the list of binding pairs into a list of names and a list of initforms eq k(processbindings(XL ; VL ; cell({L1 . L2}),VB) -> K, Mem[L1,symbol(X)] [L2,cell({L1' . L2'})] [L1',V1']) = k(processbindings(XL,X ; VL,V1' ; VB) -> K, Mem[L1,symbol(X)] [L2,cell({L1' . L2'})] [L1',V1']) . eq k(processbindings(XL ; VL ; nill) -> K, Mem) = k(evalvalues(XL ; VL ; nill) -> K, Mem) . --- evaluate the list of initforms into a list of values eq k(evalvalues(XL ; V,VL ; VL') -> K, Mem) = k(V -> evalk -> evalvalues(XL ; VL ; VL') -> K, Mem) . eq k(V -> evalvalues(XL ; VL ; VL') -> K, Mem) = k(evalvalues(XL ; VL ; VL',V) -> K, Mem) . --- bind the values to the symbols eq k(evalvalues(XL ; nill ; VL') -> K, Mem) = k(VL' -> bindTo(XL) -> K, Mem) . endfm ----------------------------------------------------------------- fmod LET*-SEMANTICS is including LET-SEMANTICS . including EVAL-SEMANTICS . var CA : ConsCell . var K : Continuation . var Env : Env . var Mem : Store . vars L1 L2 : Location . vars V1 V2 : Value . var VL : ValueList . --- let* processes the bindings sequentially. this is equivalent to --- handling each binding separately in successive nested let* forms eq k(apply(mbuiltin(let*), cell({L1 . L2}), VL) -> K, Mem) env(Env) = k(processbindings(() ; nill ; (Mem[L1])) -> apply(mbuiltin(let*), (Mem[L2]), VL) -> Env -> K, Mem) env(Env) . eq k(apply(mbuiltin(let*), symbol(nil), VL) -> K, Mem) = k(VL -> evalk -> K, Mem) . endfm ----------------------------------------------------------------- fmod FUNCTION-SEMANTICS is including EVAL-SEMANTICS . var K : Continuation . vars Env Env' : Env . var Mem : Store . vars L L1 L2 : Location . vars V V2 : Value . var VL : ValueList . var XL : NameList . vars X X' : Name . --- return the function value for the symbol --- macros are not valid, only functions eq k(apply(mbuiltin(function), symbol(X)) -> K, Mem[L,fclosure(XL,VL,Env')]) globalfenv(Env [X,L]) = k(fclosure(XL,VL,Env') -> K, Mem[L,fclosure(XL,VL,Env')]) globalfenv(Env [X,L]) . eq k(apply(mbuiltin(function), symbol(X)) -> K, Mem[L,fbuiltin(X')]) globalfenv(Env [X,L]) = k(fbuiltin(X') -> K, Mem[L,fbuiltin(X')]) globalfenv(Env [X,L]) . --- if the argument is not a symbol, then it must be a lambda expression eq k(apply(mbuiltin(function), cell({L1 . L2})) -> K, Mem[L1,symbol(lambda)]) = k(cell({L1 . L2}) -> evalk -> K, Mem[L1,symbol(lambda)]) . endfm ----------------------------------------------------------------- fmod APPLY-SEMANTICS is including EVAL-SEMANTICS . vars VFunc VLast : Value . var VMid : ValueList . var K : Continuation . var Mem : Store . --- So, the rules are funky. The last argument must be a list, and all other arguments are consed onto it --- The first arg is the function eq k(apply(fbuiltin(apply), VFunc, VMid, VLast) -> K, Mem) = k(apply(VFunc, VMid, list2Values(VLast, Mem)) -> K, Mem) . endfm ----------------------------------------------------------------- fmod FUNCALL-SEMANTICS is including EVAL-SEMANTICS . var K : Continuation . vars Env Env' : Env . var Mem : Store . vars L L1 L2 : Location . vars V V2 : Value . vars VL VL' : ValueList . var XL : NameList . vars X X' : Name . --- if the function argument is a symbol, it is coerced to a function --- by finding its functional value in the global environment eq k(apply(fbuiltin(funcall), symbol(X), VL) -> K, Mem[L,fclosure(XL,VL',Env')]) globalfenv(Env [X,L]) = k(apply(fclosure(XL,VL',Env'), VL) -> K, Mem[L,fclosure(XL,VL',Env')]) globalfenv(Env [X,L]) . eq k(apply(fbuiltin(funcall), symbol(X), VL) -> K, Mem[L,fbuiltin(X')]) globalfenv(Env [X,L]) = k(apply(fbuiltin(X'), VL) -> K, Mem[L,fbuiltin(X')]) globalfenv(Env [X,L]) . --- otherwise the function argument must be a fbuiltin or fclosure eq k(apply(fbuiltin(funcall), V, VL) -> K, Mem) globalfenv(Env) = k(apply(V, VL) -> K, Mem) globalfenv(Env) [owise] . endfm ----------------------------------------------------------------- fmod SEQ-COMP-SEMANTICS is including SEQ-COMP-SYNTAX . including GENERIC-EXP-SEMANTICS . vars E E' : Exp . var K : Continuation . var V : Value . var Mem : Store . eq k((E E') -> K, Mem) = k(E -> discard -> E' -> K, Mem) . endfm ----------------------------------------------------------------- fmod PROGN-SEMANTICS is including EVAL-SEMANTICS . op progrest : ValueList -> ContinuationItem . var K : Continuation . vars V V1 V2 : Value . var VL : ValueList . var Mem : Store . --- progn eq k(apply(mbuiltin(progn), nill) -> K, Mem) = k(symbol(nil) -> K, Mem) . eq k(apply(mbuiltin(progn), V,VL) -> K, Mem) = k(V,VL -> evalk -> K, Mem) . --- prog1 eq k(apply(mbuiltin(prog1), V1) -> K, Mem) = k(V1 -> evalk -> K, Mem) . eq k(apply(mbuiltin(prog1), V1,V2,VL) -> K, Mem) = k(V1 -> evalk -> progrest(V2,VL) -> K, Mem) . eq k(V -> progrest(VL) -> K, Mem) = k(VL -> evalk -> discard -> V -> K, Mem) . --- prog2 eq k(apply(mbuiltin(prog2), V1,V2) -> K, Mem) = k((V1,V2) -> evalk -> K, Mem) . eq k(apply(mbuiltin(prog2), V1,V2,VL) -> K, Mem) = k((V1,V2) -> evalk -> progrest(VL) -> K, Mem) . endfm ----------------------------------------------------------------- fmod DEFUN-SEMANTICS is including EVAL-SEMANTICS . var X : Name . var VL : ValueList . vars V1 V2 : Value . var K : Continuation . var Env : Env . var L : Location . var Mem : Store . --- if the symbol is already fbound in the global function environment, --- update the symbol's function value. eq k(apply(mbuiltin(defun), symbol(X), VL) -> K, Mem) globalfenv([X,L] Env) = k(apply(mbuiltin(lambda), VL) -> globalFAssignTo(X) -> symbol(X) -> K, Mem) globalfenv([X,L] Env) . --- else if the symbol is not fbound, set the symbol's function value eq k(apply(mbuiltin(defun), symbol(X), VL) -> K, Mem) globalfenv(Env) = k(apply(mbuiltin(lambda), VL) -> globalFBindTo(X) -> symbol(X) -> K, Mem) globalfenv(Env) [owise] . endfm ----------------------------------------------------------------- fmod LAMBDA-SEMANTICS is including EVAL-SEMANTICS . vars CA CB : ConsCell . var K : Continuation . vars Env Env' : Env . var Mem : Store . vars L1 L2 : Location . vars X X' : Name . vars Xl Xl' : NameList . vars V V' : Value . vars VL VL' VB : ValueList . var N : Nat . eq k(apply(mbuiltin(lambda), cell(CA), VL) -> K, Mem) env(Env) = k(fclosure(list2Names(cell(CA), Mem), VL, Env) -> K, Mem) env(Env) . eq k(apply(mbuiltin(lambda), symbol(nil), VL) -> K, Mem) env(Env) = k(fclosure(nil, VL, Env) -> K, Mem) env(Env) . eq k(apply(fclosure(Xl, &rest, X, VB, Env'), VL) -> K, Mem) env(Env) = k(values2List(restN(VL, length(Xl))) -> bindTo X -> firstN(VL, length(Xl)) -> bindTo Xl -> VB -> evalk -> Env -> K, Mem) env(Env') . eq k(apply(fclosure(Xl, VB, Env'), VL) -> K, Mem) env(Env) = k(VL -> bindTo Xl -> VB -> evalk -> Env -> K, Mem) env(Env') [owise] . endfm ----------------------------------------------------------------- fmod MACRO-SEMANTICS is including EVAL-SEMANTICS . vars CA CB : ConsCell . var K : Continuation . vars Env Env' : Env . var Mem : Store . vars L1 L2 L : Location . var X : Name . var Xl : NameList . vars V1 V2 : Value . vars VL VBody : ValueList . op macroexpand : ValueList -> ContinuationItem . op desym : Value -> [Name] . eq desym(symbol(X)) = X . eq k(apply(fbuiltin('macroexpand), cell({L1 . L2})) -> K, Mem) env(Env) = k(evalf(desym(Mem[L1])) -> macroexpand(list2Values(Mem[L2], Mem)) -> Env -> K, Mem) env(Env) . eq k(mclosure(Xl, VBody) -> macroexpand(VL) -> K, Mem) = k(VL -> bindTo Xl -> VBody -> evalk -> K, Mem) [owise] . op foo : -> ContinuationItem . eq k(mclosure(Xl, &rest, X, VBody) -> macroexpand(VL) -> K, Mem) = k(values2List(restN(VL, length(Xl))) -> bindTo X -> firstN(VL, length(Xl)) -> bindTo Xl -> VBody -> evalk -> K, Mem) . ***> FIXME: globalFBindTo should handle deciding what to do rather than having to choose here. eq k(apply(mbuiltin('defmacro), symbol(X), V1, VBody) -> K, Mem) globalfenv([X,L] Env) = k(apply(mbuiltin('macro), V1, VBody) -> globalFAssignTo(X) -> symbol(X) -> K, Mem) globalfenv([X,L] Env) . eq k(apply(mbuiltin('defmacro), symbol(X), V1, VBody) -> K, Mem) globalfenv(Env) = k(apply(mbuiltin('macro), V1, VBody) -> globalFBindTo(X) -> symbol(X) -> K, Mem) globalfenv(Env) [owise] . ---construct an mclosure from a macro eq k(apply(mbuiltin('macro), cell(CA), VBody) -> K, Mem) = k(mclosure(list2Names(cell(CA), Mem), VBody) -> K, Mem) . eq k(apply(mbuiltin('macro), symbol(nil), VBody) -> K, Mem) = k(mclosure(nil, VBody) -> K, Mem) . ---apply a macro eq k(apply(mclosure(Xl, VBody), VL) -> K, Mem) = k(mclosure(Xl, VBody) -> macroexpand(VL) -> evalk -> K, Mem) . endfm ----------------------------------------------------------------- fmod IF-SEMANTICS is including EVAL-SEMANTICS . vars VC VThen VElse : Value . var K : Continuation . var Mem : Store . var Env : Env . op ifc : Value Value -> ContinuationItem . eq k(apply(mbuiltin(if), VC, VThen, VElse) -> K, Mem) = k(VC -> evalk -> ifc(VThen, VElse) -> K, Mem) . --- the else form defaults to nil if not provided eq k(apply(mbuiltin(if), VC, VThen) -> K, Mem) = k(VC -> evalk -> ifc(VThen, symbol(nil)) -> K, Mem) . eq k(VC -> ifc(VThen, VElse) -> K, Mem) = k(if VC == symbol(nil) then VElse else VThen fi -> evalk -> K, Mem) . endfm ----------------------------------------------------------------- fmod COND-SEMANTICS is including EVAL-SEMANTICS . vars V V1 V2 : Value . var VL : ValueList . vars L1 L2 : Location . var K : Continuation . var Mem : Store . var Env : Env . op body : Value -> ContinuationItem . op clause : Value -> ContinuationItem . --- test each condition eq k(apply(mbuiltin(cond), V, VL) -> K, Mem) = k(clause(V) -> apply(mbuiltin(cond), VL) -> K, Mem) . --- if no condition matches return nil eq k(apply(mbuiltin(cond), nill) -> K, Mem) = k(symbol(nil) -> K, Mem) . --- evaluate a condition form eq k(clause(cell({L1 . L2})) -> apply(mbuiltin(cond), VL) -> K, Mem) = k(Mem[L1] -> evalk -> body(Mem[L2]) -> apply(mbuiltin(cond), VL) -> K, Mem) . --- if condition form evaluates to nil, advance to the next condition eq k(symbol(nil) -> body(V1) -> apply(mbuiltin(cond), VL) -> K, Mem) = k(apply(mbuiltin(cond), VL) -> K, Mem) . --- if condition evaluates to non-nil and there is no body, return the condition value eq k(V -> body(symbol(nil)) -> apply(mbuiltin(cond), VL) -> K, Mem) = k(V -> K, Mem) . --- otherwise the condition form evaluates to non-nil and there --- is a body so evalute the body using evalnext in GENERIC-EXP-SEMANTICS eq k(V -> body(V1) -> apply(mbuiltin(cond), VL) -> K, Mem) = k((symbol(progn),V1) -> makeConsCell -> evalk -> K, Mem) [owise] . endfm ----------------------------------------------------------------- fmod INITIALIZATION is including GENERIC-EXP-SEMANTICS . op initialize : -> ContinuationItem . var K : Continuation . var Mem : Store . eq k(initialize -> K, Mem) = k( fbuiltin('+) -> globalFBindTo('+) -> fbuiltin('-) -> globalFBindTo('-) -> fbuiltin('*) -> globalFBindTo('*) -> fbuiltin('/) -> globalFBindTo('/) -> fbuiltin(append) -> globalFBindTo(append) -> fbuiltin(car) -> globalFBindTo(car) -> fbuiltin(cdr) -> globalFBindTo(cdr) -> mbuiltin(cond) -> globalFBindTo(cond) -> fbuiltin(cons) -> globalFBindTo(cons) -> mbuiltin(defun) -> globalFBindTo(defun) -> mbuiltin(defvar) -> globalFBindTo(defvar) -> fbuiltin(eval) -> globalFBindTo(eval) -> fbuiltin(expt) -> globalFBindTo(expt) -> mbuiltin(function) -> globalFBindTo(function) -> fbuiltin(funcall) -> globalFBindTo(funcall) -> fbuiltin(apply) -> globalFBindTo(apply) -> mbuiltin(if) -> globalFBindTo(if) -> mbuiltin(lambda) -> globalFBindTo(lambda) -> mbuiltin(let) -> globalFBindTo(let) -> mbuiltin(let*) -> globalFBindTo(let*) -> fbuiltin(list) -> globalFBindTo(list) -> fbuiltin(print) -> globalFBindTo(print) -> mbuiltin(progn) -> globalFBindTo(progn) -> mbuiltin(prog1) -> globalFBindTo(prog1) -> mbuiltin(prog2) -> globalFBindTo(prog2) -> mbuiltin(quote) -> globalFBindTo(quote) -> mbuiltin(setf) -> globalFBindTo(setf) --- predicates -> fbuiltin(endp) -> globalFBindTo(endp) -> fbuiltin(fboundp) -> globalFBindTo(fboundp) -> fbuiltin(integerp) -> globalFBindTo(integerp) -> fbuiltin(numberp) -> globalFBindTo(numberp) -> fbuiltin(zerop) -> globalFBindTo(zerop) -> fbuiltin(symbolp) -> globalFBindTo(symbolp) -> fbuiltin(stringp) -> globalFBindTo(stringp) -> fbuiltin(consp) -> globalFBindTo(consp) -> fbuiltin(listp) -> globalFBindTo(listp) -> fbuiltin(null) -> globalFBindTo(null) --- boolean expressions -> mbuiltin(and) -> globalFBindTo(and) -> fbuiltin(not) -> globalFBindTo(not) -> mbuiltin(or) -> globalFBindTo(or) -> fbuiltin('=) -> globalFBindTo('=) -> fbuiltin('/=) -> globalFBindTo('/=) -> fbuiltin('<) -> globalFBindTo('<) -> fbuiltin('>) -> globalFBindTo('>) -> fbuiltin('<=) -> globalFBindTo('<=) -> fbuiltin('>=) -> globalFBindTo('>=) -> mbuiltin('defmacro) -> globalFBindTo('defmacro) -> fbuiltin('macroexpand) -> globalFBindTo('macroexpand) --- atom function -> [defun atom [x] [not [consp x]]] -> discard --- list function -> [defun list [&rest x] x] -> discard --- cadr accessor -> [defun cadr [x] [car [cdr x]]] -> discard --- first accessor -> [defun first [x] [car x]] -> discard --- second accessor -> [defun second [x] [car [cdr x]]] -> discard --- rest accessor -> [defun rest [x] [cdr x]] -> discard -> K, Mem) . endfm ----------------------------------------------------------------- fmod LISP-SEMANTICS is including LISP-SYNTAX . including GENERIC-EXP-SEMANTICS . including QUOTE-SEMANTICS . including ARITHMETIC-EXP-SEMANTICS . including BOOLEAN-EXP-SEMANTICS . including PREDICATE-SEMANTICS . including DEFVAR-SEMANTICS . including SETF-SEMANTICS . including ACCESSOR-SEMANTICS . including LIST-SEMANTICS . including CONS-SEMANTICS . including APPEND-SEMANTICS . including PRINT-SEMANTICS . including SEQ-COMP-SEMANTICS . including PROGN-SEMANTICS . including LET-SEMANTICS . including LET*-SEMANTICS . including LAMBDA-SEMANTICS . including DEFUN-SEMANTICS . including FUNCTION-SEMANTICS . including FUNCALL-SEMANTICS . including MACRO-SEMANTICS . including IF-SEMANTICS . including COND-SEMANTICS . including APPLY-SEMANTICS . including INITIALIZATION . op run_ : Exp -> [Output] . op [_] : PLState -> [Output] . var E : Exp . var V : Value . var S : PLState . var O : Output . var Mem : Store . eq run(E) = [k(initialize -> E -> stop, empty) env(empty) globalenv(empty) globalfenv(empty) nextLoc(1) output(none) lastaloc(loc(0))] . eq [k(V -> stop, Mem) output(O) S] = O . endfm ----------------------------------------------------------------- --- LISP Tests -------------------------------------------------- ----------------------------------------------------------------- ----------------------------------------------------------------- red run( [setf b $ [[a b c] 2 3 4]] [print b] [setf [cadr b] {"2nd"}] [setf [second [car b]] {"inside 2nd"}] [setf [cdr [rest [car b]]] $ [76 143]] [print b] [print [first [first b]]] ) . ***> should be Output: "[[a b c] 2 3 4]" : "[[a {inside 2nd} 76 143] {2nd} 3 4]" : "a" ----------------------------------------------------------------- red run( [setf a $ [1 2 3 4]] [print a] [setf [first a] {"1st"}] [setf [second a] {"2nd"}] [setf [rest [rest a]] $ [76 143]] [print a] [print [cadr a]] ) . ***> should be Output: "[1 2 3 4]" : "[{1st} {2nd} 76 143]" : "{2nd}" ----------------------------------------------------------------- red run( [setf a $ [1 2 3 4]] [print a] [setf [car [cdr [cdr a]]] {"3rd"}] [defun 'cadr [x] [car [cdr x]]] [setf ['cadr a] {"2nd"}] [print a] ) . ***> should be Output: "[1 2 3 4]" : "[1 {2nd} {3rd} 4]" --------------------------------------------------------------- red run( ['defmacro 'my-cadr [x] [list $ car [list $ cdr x]]] [print ['macroexpand $ ['my-cadr [a b c]]]] [print ['my-cadr $ [a b c]]] ) . ***> should be Output: "[car [cdr [a b c]]]" : "b" --------------------------------------------------------------- red run( ['defmacro 'my-cadr [x] [print x] [list $ car [list $ cdr x]]] [print ['macroexpand $ ['my-cadr [a b c]]]] [print ['my-cadr $ [a b c]]] ) . ***> should be Output: "[a b c]" : "[car [cdr [a b c]]]" : "[quote [a b c]]" : "b" --------------------------------------------------------------- *** Work our way up to mapcar and let red run ( [defun 'some-null-element-p ['lists] [cond [[null 'lists] nil] [[null [car 'lists]] t] [t ['some-null-element-p [cdr 'lists]]]]] [print ['some-null-element-p $ [[] [a] [b]]]] [print ['some-null-element-p $ [[a] [b] [c]]]] [print ['some-null-element-p $ []]] [print ['some-null-element-p $ [a b c d]]] ) . ***> should be Output: "t" : "nil" : "nil" : "nil" --------------------------------------------------------------- red run ( [defun 'single-list-mapcar ['func 'arg-list] [if [null 'arg-list] 'arg-list [cons [funcall 'func [car 'arg-list]] ['single-list-mapcar 'func [cdr 'arg-list]]]]] [defun 'plus [x] ['+ 1 x]] [print ['single-list-mapcar #$ 'plus $ [1 2 3 4 5]]] ) . ***> should be: "[2 3 4 5 6]" --------------------------------------------------------------- red run( --- [defun 'first [x] [car x]] --- [defun 'second [x] [car [cdr x]]] --- [defun 'rest [x] [cdr x]] [defun 'some-null-element-p ['lists] [cond [[null 'lists] nil] [[null [car 'lists]] t] [t ['some-null-element-p [cdr 'lists]]]]] [defun 'single-list-mapcar ['func 'arg-list] [if [null 'arg-list] 'arg-list [cons [funcall 'func [car 'arg-list]] ['single-list-mapcar 'func [cdr 'arg-list]]]]] [defun 'my-mapcar ['func &rest 'arg-lists] [if ['some-null-element-p 'arg-lists] nil [cons [apply 'func ['single-list-mapcar #$ first 'arg-lists]] [apply #$ 'my-mapcar 'func ['single-list-mapcar #$ rest 'arg-lists]]]]] [defun 'plus [x y] ['+ x y]] [print ['my-mapcar #$ 'plus $ [1 2 3 4] $[4 3 2 2]]] ) . ***> should be: String: "[5 5 5 6]" --------------------------------------------------------------- red run( [defun 'some-null-element-p ['lists] [cond [[null 'lists] nil] [[null [car 'lists]] t] [t ['some-null-element-p [cdr 'lists]]]]] [defun 'single-list-mapcar ['func 'arg-list] [if [null 'arg-list] 'arg-list [cons [funcall 'func [car 'arg-list]] ['single-list-mapcar 'func [cdr 'arg-list]]]]] [defun 'my-mapcar ['func &rest 'arg-lists] [if ['some-null-element-p 'arg-lists] nil [cons [apply 'func ['single-list-mapcar #$ first 'arg-lists]] [apply #$ 'my-mapcar 'func ['single-list-mapcar #$ rest 'arg-lists]]]]] ['defmacro 'my-let ['bindings &rest 'body] [append [list [append [list $ lambda ['my-mapcar #$ first 'bindings]] 'body]] ['my-mapcar #$ second 'bindings]]] [print ['macroexpand $ ['my-let [[a 3] [b 4]] [list a b]]]] [print ['my-let [[a 3] [b 4]] [list a b]]] ) . ***> should be Output: "[[lambda [a b] [list a b]] 3 4]" : "[3 4]"