1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_semantics";
2
3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory;
4
5(*****************************************************************************)
6(* Relational semantics for Pure LISP as formalised by Mike Gordon           *)
7(* for the 2006 ACL2 workshop.                                               *)
8(*****************************************************************************)
9
10
11(*****************************************************************************)
12(* An atom is Nil or a number or a string                                    *)
13(*****************************************************************************)
14
15val _ =
16 Hol_datatype
17  `atom = Nil | Number of num | String of string`;
18
19(*****************************************************************************)
20(* An S-expression is an atom or a dotted pair (cons-cell)                   *)
21(*****************************************************************************)
22
23val _ =
24 Hol_datatype
25  `sexpression = A of atom | Cons of sexpression => sexpression`;
26
27(*****************************************************************************)
28(* Syntax of Pure Lisp                                                       *)
29(*****************************************************************************)
30
31val _ =
32 Hol_datatype
33  `term = Con of sexpression
34        | Var of string
35        | App of func => term list
36        | Ite of (term # term)list;
37
38   func = FunCon of string
39        | FunVar of string
40        | Lambda of string list => term
41        | Label  of string => func`;
42
43(*****************************************************************************)
44(* Some utility values and functions                                         *)
45(*****************************************************************************)
46
47val False_def =
48 Define
49  `False = A Nil`;
50
51val isTrue_def =
52 Define
53  `isTrue s <=> ~(s = False) /\ ~(s = A (String "nil"))`;
54
55val True_def =
56 Define
57  `True = A(String "t")`;
58
59val Car_def =
60 Define
61  `Car(Cons s1 s2) = s1`;
62
63val Cdr_def =
64 Define
65  `Cdr(Cons s1 s2) = s2`;
66
67val delete_Nil_aux_def = Define `
68  (delete_Nil_aux Nil = String "nil") /\
69  (delete_Nil_aux (Number n) = Number n) /\
70  (delete_Nil_aux (String s) = String s)`;
71
72val delete_Nil_def = Define `
73  (delete_Nil (A a) = A (delete_Nil_aux a)) /\
74  (delete_Nil (Cons s t) = Cons (delete_Nil s) (delete_Nil t))`;
75
76val Equal_def =
77 Define
78  `Equal (x,y) = if delete_Nil x = delete_Nil y:sexpression then True else False`;
79
80val Atomp_def =
81 Define
82  `(Atomp (A a) = True)
83   /\
84   (Atomp _ = False)`;
85
86val Consp_def =
87 Define
88  `(Consp (A a) = False)
89   /\
90   (Consp _ = True)`;
91
92val Numberp_def =
93 Define
94  `(Numberp (A (Number n)) = True)
95   /\
96   (Numberp _ = False)`;
97
98val Symbolp_def =
99 Define
100  `(Symbolp (A (String s)) = True)
101   /\
102   (Symbolp (A Nil) = True)
103   /\
104   (Symbolp _ = False)`;
105
106val Add_def =
107 Define
108  `Add (A(Number m)) (A(Number n)) = A(Number(m+n))`;
109
110val Sub_def =
111 Define
112  `Sub ((A(Number m)),(A(Number n))) = A(Number(m-n))`;
113
114val Mult_def =
115 Define
116  `Mult (A(Number m)) (A(Number n)) = A(Number(m*n))`;
117
118val Div_def =
119 Define
120  `Div ((A(Number m)),(A(Number n))) = A(Number(m DIV n))`;
121
122val Mod_def =
123 Define
124  `Mod ((A(Number m)),(A(Number n))) = A(Number(m MOD n))`;
125
126val Less_def =
127 Define
128  `Less ((A(Number m)),(A(Number n))) = if m < n then True else False`;
129
130val FunConSem_def =
131 Define
132  `FunConSem s sl =
133    if s = "car"     then Car(EL 0 sl)                else
134    if s = "cdr"     then Cdr(EL 0 sl)                else
135    if s = "cons"    then Cons(EL 0 sl) (EL 1 sl)     else
136    if s = "+"       then FOLDL Add (A(Number 0)) sl  else
137    if s = "*"       then FOLDL Mult (A(Number 1)) sl else
138    if s = "-"       then Sub(EL 0 sl,EL 1 sl)        else
139    if s = "div"     then Div(EL 0 sl,EL 1 sl)        else
140    if s = "mod"     then Mod(EL 0 sl,EL 1 sl)        else
141    if s = "<"       then Less(EL 0 sl,EL 1 sl)       else
142    if s = "equal"   then Equal(EL 0 sl,EL 1 sl)      else
143    if s = "atomp"   then Atomp(EL 0 sl)              else
144    if s = "consp"   then Consp(EL 0 sl)              else
145    if s = "numberp" then Numberp(EL 0 sl)            else
146    if s = "symbolp" then Symbolp(EL 0 sl)            else
147    ARB`;
148
149val FunConSemOK_def =
150 Define
151  `FunConSemOK s sl =
152    if s = "car"     then ?u v. sl = [Cons u v]   else
153    if s = "cdr"     then ?u v. sl = [Cons u v]   else
154    if s = "cons"    then ?u v. sl = [u; v]       else
155    if s = "+"       then (!x. MEM x sl ==> ?n. x = A (Number n)) else
156    if s = "-"       then ?m n. sl = [A (Number m); A (Number n)] else
157    if s = "*"       then (!x. MEM x sl ==> ?n. x = A (Number n)) else
158    if s = "div"     then ?m n. sl = [A (Number m); A (Number n)] else
159    if s = "mod"     then ?m n. sl = [A (Number m); A (Number n)] else
160    if s = "<"       then ?m n. sl = [A (Number m); A (Number n)] else
161    if s = "equal"   then ?u v. sl = [u; v]       else
162    if s = "atomp"   then ?u.   sl = [u]          else
163    if s = "consp"   then ?u.   sl = [u]          else
164    if s = "numberp" then ?u.   sl = [u]          else
165    if s = "symbolp" then ?u.   sl = [u]          else
166    F`;
167
168(*****************************************************************************)
169(* An environment (alist) is a finite function from names (strings) to       *)
170(* values of type ``:sexpression + func`` (so variables and                  *)
171(* Label-defined functions share the same namespace).                        *)
172(*****************************************************************************)
173
174(*****************************************************************************)
175(* VarBind a xl sl extends a by binding each string in xl to the             *)
176(* S-expression at the corresponding position in sl. If xl is shorter than   *)
177(* sl, then only the first n elements of sl are used, where n is the         *)
178(* length of x. If xl is longer than sl, than sl is padded with NILs.        *)
179(*                                                                           *)
180(* Subtle point: with the semantics in which clock timeout returns NONE      *)
181(* having VarBind  only partially specified is no problem, but               *)
182(* with the semantics in which timeout returns an S-expression it is         *)
183(* tricky to distinguish the arbitrary value returned when VarBind is        *)
184(* applied to lists of different lists from a real value.                    *)
185(* We thus totalise VarBind as described above.                              *)
186(*****************************************************************************)
187
188val VarBind_def =
189 Define
190  `(VarBind a [] sl = (a : (string |-> sexpression + func)))
191   /\
192   (VarBind a (x::xl) [] = (VarBind (a |+ (x, INL(A Nil))) xl []))
193   /\
194   (VarBind a (x::xl) (s::sl) = (VarBind (a |+ (x, INL s)) xl sl))`;
195
196(*****************************************************************************)
197(* 55FunBind a f fn extends a by binding fn to f                               *)
198(*****************************************************************************)
199
200val FunBind_def =
201 Define
202  `FunBind (a:string|->sexpression+func) f fn = a |+ (f, INR fn)`;
203
204(*****************************************************************************)
205(* Operational semantics of Pure Lisp using three inductive relations:       *)
206(*                                                                           *)
207(*  R_ap (fn,args,a) s - fn applied to args evaluates to s with alist a      *)
208(*  R_ev (e,a) s        - term e evaluates to S-expression s with alist a    *)
209(*  R_evl (el,a) sl     - term list el evaluates to S-expression list sl     *)
210(*                                                                           *)
211(* The names R_evl_rules, R_evl_ind, R_evl_cases are the ones                *)
212(* automatically generated to name the theorems in the theory.               *)
213(*                                                                           *)
214(*****************************************************************************)
215
216val (R_ap_rules,R_ap_ind,R_ap_cases) =
217 Hol_reln
218 `(!s a.
219    R_ev (Con s, a) s)
220  /\
221  (!x a.
222    x IN FDOM a /\ ISL (a ' x) ==>
223    R_ev (Var x, a) (OUTL(a ' x)))
224  /\
225  (!fc args a.
226    FunConSemOK fc args ==>
227    R_ap (FunCon fc,args,a) (FunConSem fc args))
228  /\
229  (!fn el args s a.
230    R_evl (el,a) args /\ R_ap (fn,args,a) s /\ (LENGTH args = LENGTH el)
231    ==> R_ev (App fn el,a) s)
232  /\
233  (!a.
234    R_ev (Ite [], a) False)
235  /\
236  (!e1 e2 el s a.
237    R_ev (e1,a) False /\ R_ev (Ite el,a) s
238    ==> R_ev (Ite ((e1,e2)::el),a) s)
239  /\
240  (!e1 e2 el s1 s a.
241    R_ev (e1,a) s1 /\ isTrue s1 /\ R_ev (e2,a) s
242    ==>
243    R_ev (Ite ((e1,e2)::el),a) s)
244  /\
245  (!x fn args s a.
246    R_ap (fn,args,FunBind a x fn) s ==> R_ap(Label x fn,args,a) s)
247  /\
248  (!fv args s a.
249    fv NOTIN {"quote";"cond";"car";"cdr";"cons";"+";"-";"*";"div";"mod";"<";
250              "equal";"atomp";"consp";"symbolp";"numberp"} /\
251    fv IN FDOM a /\ ISR (a ' fv) /\
252    R_ap (OUTR(a ' fv),args,a) s ==> R_ap (FunVar fv,args,a) s)
253  /\
254  (!xl e args s a.
255    (LENGTH args = LENGTH xl) /\ R_ev (e,VarBind a xl args) s
256    ==> R_ap (Lambda xl e,args,a) s)
257  /\
258  (!a.
259    R_evl ([],a) [])
260  /\
261  (!e el s sl a.
262    R_ev (e,a) s /\ R_evl (el,a) sl
263    ==> R_evl (e::el,a) (s::sl))`;
264
265val _ = export_theory();
266