lisp-runtime/extract/lisp_extractScript.sml

44   ``!x. x IN FDOM e ==> R_ev (Var x,e,fns,io,ok) (e ' x,fns,io,ok)``,
48   ``!x. T ==> R_ev (Const x,e,fns,io,ok) (x,fns,io,ok)``,
54     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
56                    R_ev (If x y z,e,fns,io,ok)
67     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
69                    R_ev (If x y z,e,fns,io,ok)
78     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
80                    R_ev (Or (x::y::xs),e,fns,io,ok)
90     (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
92                    R_ev (Or (x::y::xs),e,fns,io,ok)
99   ``T ==> R_ev (Or [],a,fns,io,ok) (Sym "NIL",fns,io,ok)``,
107   ``R_ev (t,a,fns,io,ok) res =
108     R_ev (Or [t],a,fns,io,ok) res``,
115   ``(b ==> R_ev (t,a,fns,io,ok) res) ==>
116     (b ==> R_ev (Or [t],a,fns,io,ok) res)``,
121          R_ap (PrimitiveFun fc,args,a,fns,io,ok) (FST (EVAL_DATA_OP fc) args,fns,io,ok)``,
127     R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
128     R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2)``,
134     (b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
135     (b /\ bl ==> R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))``,
141   ``R_evl ([],a,fns,io,ok) ([],fns,io,ok)``,
146     (b2 ==> R_evl (el,a,fns,io,ok) (args,fns1,io1,ok1)) ==>
147     (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res)``,
153     (b2 ==> R_evl (el,a,fns,io,ok) res1) ==>
154     (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res2)``,
163     R_ap (Define,args,a,fns,io,ok)
165           io,ok /\ ~(getSym (EL 0 args) IN FDOM fns))``,
175   ``T ==> R_ap (Error,args,a,fns,io,ok) (Sym "NIL",fns,STRCAT
181   ``R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
182     R_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (CAR s,fns1,io1,ok1)``,
194   ``R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) ==>
195     R_ev (App (PrimitiveFun opCDR) [e],a,fns,io,ok) (CDR s,fns1,io1,ok1)``,
207   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
208     (b ==> R_ev (First e,a,fns,io,ok) (FIRST s,fns1,io1,ok1))``,
214   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
215     (b ==> R_ev (Second e,a,fns,io,ok) (SECOND s,fns1,io1,ok1))``,
222   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
223     (b ==> R_ev (Third e,a,fns,io,ok) (THIRD s,fns1,io1,ok1))``,
230   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
231     (b ==> R_ev (Fourth e,a,fns,io,ok) (FOURTH s,fns1,io1,ok1))``,
238   ``(b ==> R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1)) ==>
239     (b ==> R_ev (Fifth e,a,fns,io,ok) (FIFTH s,fns1,io1,ok1))``,
246   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
247     (b ==> R_ev (First e,a,fns,io,ok) (FIRST (FST res),SND res))``,
251   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
252     (b ==> R_ev (Second e,a,fns,io,ok) (SECOND (FST res),SND res))``,
256   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
257     (b ==> R_ev (Third e,a,fns,io,ok) (THIRD (FST res),SND res))``,
261   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
262     (b ==> R_ev (Fourth e,a,fns,io,ok) (FOURTH (FST res),SND res))``,
266   ``(b ==> R_ev (e,a,fns,io,ok) res) ==>
267     (b ==> R_ev (Fifth e,a,fns,io,ok) (FIFTH (FST res),SND res))``,
271   ``R_ev (x,a,fns,io,ok) res =
272     R_ev (LetStar [] x,a,fns,io,ok) res``,
279   ``R_ev (Let [z] (LetStar zs x),a,fns,io,ok) res =
280     R_ev (LetStar (z::zs) x,a,fns,io,ok) res``,
287   ``R_ev (Const (Sym "NIL"),a,fns,io,ok) res =
288     R_ev (Cond [],a,fns,io,ok) res``,
295   ``R_ev (If x1 x2 (Cond qs),a,fns,io,ok) res =
296     R_ev (Cond ((x1,x2)::qs),a,fns,io,ok) res``,
303   ``R_ev (Const (Sym "T"),a,fns,io,ok) res =
304     R_ev (And [],a,fns,io,ok) res``,
311   ``R_ev (Const (Sym "NIL"),a,fns,io,ok) res =
312     R_ev (List [],a,fns,io,ok) res``,
319   ``R_ev (t,a,fns,io,ok) res =
320     R_ev (And [t],a,fns,io,ok) res``,
327   ``R_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) res =
328     R_ev (And (t1::t2::ts),a,fns,io,ok) res``,
335   ``R_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) res =
336     R_ev (List (t::ts),a,fns,io,ok) res``,
343   ``R_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) res =
344     R_ev (Defun fname ps body,a,fns,io,ok) res``,
357       (b1 ==> R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1)) ==>
360       R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)``,
365       (b1 ==> R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1)) ==>
368       R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) (x,fns2,io2,ok2)``,
376       (b1 ==> R_evl (ys,a,fns,io,ok) res1) ==>
379       R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) res2``,
384   ``(b1 ==> R_ev (Let xs e,a,fns,io,ok) res) ==>
385     (b1 ==> R_ev (LamApp (MAP FST xs) e (MAP SND xs),a,fns,io,ok) res)``,
392   funcall_ok args fns io ok = ?result. R_ap (Funcall,args,ARB,fns,io,ok) result`;
395   funcall args fns io ok =
396     if funcall_ok args fns io ok
397     then @result. R_ap (Funcall,args,ARB,fns,io,ok) result
398     else (Sym "NIL",fns,io,ok)`;
401   ``R_ap (Funcall,args,a,fns,io,ok) x = R_ap (Funcall,args,ARB,fns,io,ok) x``,
405   ``funcall_ok args fns io ok ==>
406     R_ap (Funcall,args,a,fns,io,ok) (funcall args fns io ok)``,
411   ``T ==> R_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns,
412           io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok)``,
423       R_ev (exp,VarBind params args,fns,io,ok) res ==>
424       R_ap (Fun fc,args,a,fns,io,ok) res``,
430       (b ==> R_ap (Fun name,args,e,k,io,ok) exp) ==>
433       ((ok ==> b) ==> R_ap (Fun name,args,e,k,io,ok) (if ok then exp else (Sym "NIL",k,io,ok)))``,
434   Cases_on `ok` \\ FULL_SIMP_TAC std_ss []
510     fns_assum (FST (SND (funcall args fns io ok))) xs``,
512   \\ Cases_on `funcall_ok args fns io ok` \\ ASM_SIMP_TAC std_ss []
550   ``R_ap (Funcall,(Sym f)::xs,ARB,k,io,ok) (x1,x2,x3,ok2) /\
551     SND (SND (SND (funcall ((Sym f)::xs) k io ok))) ==> ok2``,
553   \\ `funcall_ok (Sym f::xs) k io ok` by METIS_TAC [funcall_ok_def]
555   \\ `!res. R_ap (Funcall,Sym f::xs,ARB,k,io,ok) res =