lisp-runtime/spec/lisp_semanticsScript.sml

169  (!s a fns io ok.
170     R_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
172   (!x (a: string |-> SExp) fns io ok.
174     R_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
176   (!a fns io ok s fns1 io1 ok1.
177     R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
178     R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
180   (!a fns io s1 fns1 io1 t ts ok.
181     R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
182     R_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
184   (!a fns io s1 fns1 io1 s2 fns2 io2 t ts ok ok2.
185     R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
187     R_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2))
190     R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\
193     R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
196     R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 /\
199     R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
202     R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1) /\ (LENGTH xs = LENGTH ys) /\
205     R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2))
208     R_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\
211     R_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2))
216     R_ap (PrimitiveFun fc,args,a,fns,io,ok) (f args,fns,io,ok))
221     R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
223     R_ap (Fun fc,args,a,fns,io:string,ok) (x,fns2,io2,ok2))
226     R_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns,
227           io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok))
230     R_ap (Define,[fc; formals; body],a,fns,io,ok)
232           io,ok /\ ~(getSym fc IN FDOM fns)))
235     R_ap (Error,args,a,fns,io,ok) (anything,fns,
241     R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
243     R_ap (Funcall,Sym fname::args,a,fns,io,ok) (x,fns2,io2,ok2))
254     R_evl ([],a,fns,io,ok) ([],fns,io,ok))
257     R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) /\
260     R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))
265     R_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (s,fns1,io1,ok1) ==>
266     R_ev (First e,a,fns,io,ok) (s,fns1,io1,ok1))
269     R_ev (First (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
270     R_ev (Second e,a,fns,io,ok) (s,fns1,io1,ok1))
273     R_ev (Second (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
274     R_ev (Third e,a,fns,io,ok) (s,fns1,io1,ok1))
277     R_ev (Third (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
278     R_ev (Fourth e,a,fns,io,ok) (s,fns1,io1,ok1))
281     R_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
282     R_ev (Fifth e,a,fns,io,ok) (s,fns1,io1,ok1))
285     R_ev (LamApp (MAP FST zs) x (MAP SND zs),a,fns,io,ok) (s,fns1,io1,ok1) ==>
286     R_ev (Let zs x,a,fns,io,ok) (s,fns1,io1,ok1))
289     R_ev (x,a,fns,io,ok) (s,fns1,io1,ok1) ==>
290     R_ev (LetStar [] x,a,fns,io,ok) (s,fns1,io1,ok1))
293     R_ev (Let [z] (LetStar zs x),a,fns,io,ok) (s,fns1,io1,ok1) ==>
294     R_ev (LetStar (z::zs) x,a,fns,io,ok) (s,fns1,io1,ok1))
297     R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
298     R_ev (Cond [],a,fns,io,ok) (s,fns1,io1,ok1))
301     R_ev (If x1 x2 (Cond qs),a,fns,io,ok) (s,fns1,io1,ok1) ==>
302     R_ev (Cond ((x1,x2)::qs),a,fns,io,ok) (s,fns1,io1,ok1))
305     R_ev (Const (Sym "T"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
306     R_ev (And [],a,fns,io,ok) (s,fns1,io1,ok1))
309     R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
310     R_ev (List [],a,fns,io,ok) (s,fns1,io1,ok1))
313     R_ev (t,a,fns,io,ok) (s,fns1,io1,ok1) ==>
314     R_ev (And [t],a,fns,io,ok) (s,fns1,io1,ok1))
317     R_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) (s,fns1,io1,ok1) ==>
318     R_ev (And (t1::t2::ts),a,fns,io,ok) (s,fns1,io1,ok1))
321     R_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) (s,fns1,io1,ok1) ==>
322     R_ev (List (t::ts),a,fns,io,ok) (s,fns1,io1,ok1))
325     R_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) (s,fns1,io1,ok1) ==>
326     R_ev (Defun fname ps body,a,fns,io,ok) (s,fns1,io1,ok1))`;
389   ``(R_ev (x,env,k,io,ok) (r,k',io',T) =
390      R_ev (x,env,k,io,T) (r,k',io',T) /\ ok) /\
391     (R_evl (xs,env,k,io,ok) (rs,k',io',T) =
392      R_evl (xs,env,k,io,T) (rs,k',io',T) /\ ok) /\
393     (R_ap (f,args,env,k,io,ok) (r,k',io',T) =
394      R_ap (f,args,env,k,io,T) (r,k',io',T) /\ ok)``,