lisp-runtime/extract/lisp_extractScript.sml

43   ``!x. x IN FDOM e ==> R_ev (Var x,e,fns,io,ok) (e ' x,fns,io,ok)``,
47   ``!x. T ==> R_ev (Const x,e,fns,io,ok) (x,fns,io,ok)``,
53     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
55                    R_ev (If x y z,e,fns,io,ok)
66     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
68                    R_ev (If x y z,e,fns,io,ok)
77     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
79                    R_ev (Or (x::y::xs),e,fns,io,ok)
89     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
91                    R_ev (Or (x::y::xs),e,fns,io,ok)
98   ``T ==> R_ev (Or [],a,fns,io,ok) (Sym "NIL",fns,io,ok)``,
106   ``R_ev (t,a,fns,io,ok) res =
107     R_ev (Or [t],a,fns,io,ok) res``,
114   ``(b ==> R_ev (t,a,fns,io,ok) res) ==>
115     (b ==> R_ev (Or [t],a,fns,io,ok) res)``,
120          R_ap (PrimitiveFun fc,args,a,fns,io,ok) (FST (EVAL_DATA_OP fc) args,fns,io,ok)``,
126     R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
127     R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2)``,
133     (b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
134     (b /\ bl ==> R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))``,
140   ``R_evl ([],a,fns,io,ok) ([],fns,io,ok)``,
145     (b2 ==> R_evl (el,a,fns,io,ok) (args,fns1,io1,ok1)) ==>
146     (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res)``,
152     (b2 ==> R_evl (el,a,fns,io,ok) res1) ==>
153     (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res2)``,
162     R_ap (Define,args,a,fns,io,ok)
164           io,ok /\ ~(getSym (EL 0 args) IN FDOM fns))``,
174   ``T ==> R_ap (Error,args,a,fns,io,ok) (Sym "NIL",fns,STRCAT
180   ``R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
181     R_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (CAR s,fns1,io1,ok1)``,
193   ``R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
194     R_ev (App (PrimitiveFun opCDR) [e],a,fns,io,ok) (CDR s,fns1,io1,ok1)``,
206   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
207     (b ==> R_ev (First e,a,fns,io,ok) (FIRST s,fns1,io1,ok1))``,
213   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
214     (b ==> R_ev (Second e,a,fns,io,ok) (SECOND s,fns1,io1,ok1))``,
221   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
222     (b ==> R_ev (Third e,a,fns,io,ok) (THIRD s,fns1,io1,ok1))``,
229   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
230     (b ==> R_ev (Fourth e,a,fns,io,ok) (FOURTH s,fns1,io1,ok1))``,
237   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
238     (b ==> R_ev (Fifth e,a,fns,io,ok) (FIFTH s,fns1,io1,ok1))``,
245   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
246     (b ==> R_ev (First e,a,fns,io,ok) (FIRST (FST res),SND res))``,
250   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
251     (b ==> R_ev (Second e,a,fns,io,ok) (SECOND (FST res),SND res))``,
255   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
256     (b ==> R_ev (Third e,a,fns,io,ok) (THIRD (FST res),SND res))``,
260   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
261     (b ==> R_ev (Fourth e,a,fns,io,ok) (FOURTH (FST res),SND res))``,
265   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
266     (b ==> R_ev (Fifth e,a,fns,io,ok) (FIFTH (FST res),SND res))``,
270   ``R_ev (x,a,fns,io,ok) res =
271     R_ev (LetStar [] x,a,fns,io,ok) res``,
278   ``R_ev (Let [z] (LetStar zs x),a,fns,io,ok) res =
279     R_ev (LetStar (z::zs) x,a,fns,io,ok) res``,
286   ``R_ev (Const (Sym "NIL"),a,fns,io,ok) res =
287     R_ev (Cond [],a,fns,io,ok) res``,
294   ``R_ev (If x1 x2 (Cond qs),a,fns,io,ok) res =
295     R_ev (Cond ((x1,x2)::qs),a,fns,io,ok) res``,
302   ``R_ev (Const (Sym "T"),a,fns,io,ok) res =
303     R_ev (And [],a,fns,io,ok) res``,
310   ``R_ev (Const (Sym "NIL"),a,fns,io,ok) res =
311     R_ev (List [],a,fns,io,ok) res``,
318   ``R_ev (t,a,fns,io,ok) res =
319     R_ev (And [t],a,fns,io,ok) res``,
326   ``R_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) res =
327     R_ev (And (t1::t2::ts),a,fns,io,ok) res``,
334   ``R_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) res =
335     R_ev (List (t::ts),a,fns,io,ok) res``,
342   ``R_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) res =
343     R_ev (Defun fname ps body,a,fns,io,ok) res``,
356       (b1 ==> R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1)) ==>
359       R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)``,
364       (b1 ==> R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1)) ==>
367       R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) (x,fns2,io2,ok2)``,
375       (b1 ==> R_evl (ys,a,fns,io,ok) res1) ==>
378       R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) res2``,
383   ``(b1 ==> R_ev (Let xs e,a,fns,io,ok) res) ==>
384     (b1 ==> R_ev (LamApp (MAP FST xs) e (MAP SND xs),a,fns,io,ok) res)``,
391   funcall_ok args fns io ok = ?result. R_ap (Funcall,args,ARB,fns,io,ok) result`;
394   funcall args fns io ok =
395     if funcall_ok args fns io ok
396     then @result. R_ap (Funcall,args,ARB,fns,io,ok) result
397     else (Sym "NIL",fns,io,ok)`;
400   ``R_ap (Funcall,args,a,fns,io,ok) x = R_ap (Funcall,args,ARB,fns,io,ok) x``,
404   ``funcall_ok args fns io ok ==>
405     R_ap (Funcall,args,a,fns,io,ok) (funcall args fns io ok)``,
410   ``T ==> R_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns,
411           io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok)``,
422       R_ev (exp,VarBind params args,fns,io,ok) res ==>
423       R_ap (Fun fc,args,a,fns,io,ok) res``,
429       (b ==> R_ap (Fun name,args,e,k,io,ok) exp) ==>
432       ((ok ==> b) ==> R_ap (Fun name,args,e,k,io,ok) (if ok then exp else (Sym "NIL",k,io,ok)))``,
433   Cases_on `ok` \\ FULL_SIMP_TAC std_ss []
509     fns_assum (FST (SND (funcall args fns io ok))) xs``,
511   \\ Cases_on `funcall_ok args fns io ok` \\ ASM_SIMP_TAC std_ss []
549   ``R_ap (Funcall,(Sym f)::xs,ARB,k,io,ok) (x1,x2,x3,ok2) /\
550     SND (SND (SND (funcall ((Sym f)::xs) k io ok))) ==> ok2``,
552   \\ `funcall_ok (Sym f::xs) k io ok` by METIS_TAC [funcall_ok_def]
554   \\ `!res. R_ap (Funcall,Sym f::xs,ARB,k,io,ok) res =