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