|
1 structure USyntax : USyntax_sig = |
|
2 struct |
|
3 |
|
4 structure Utils = Utils; |
|
5 open Utils; |
|
6 open Mask; |
|
7 |
|
8 infix 7 |->; |
|
9 infix 4 ##; |
|
10 |
|
11 fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg}; |
|
12 |
|
13 type Type = typ |
|
14 type Term = cterm |
|
15 type Preterm = term |
|
16 |
|
17 |
|
18 (*--------------------------------------------------------------------------- |
|
19 * |
|
20 * Types |
|
21 * |
|
22 *---------------------------------------------------------------------------*) |
|
23 fun mk_type{Tyop, Args} = Type(Tyop,Args); |
|
24 val mk_prim_vartype = TVar; |
|
25 fun mk_vartype s = mk_prim_vartype((s,0),["term"]); |
|
26 |
|
27 fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args} |
|
28 | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"}; |
|
29 |
|
30 |
|
31 (* But internally, it's useful *) |
|
32 fun dest_vtype (TVar x) = x |
|
33 | dest_vtype _ = raise ERR{func = "dest_vtype", |
|
34 mesg = "not a flexible type variable"}; |
|
35 |
|
36 val is_vartype = Utils.can dest_vtype; |
|
37 |
|
38 val type_vars = map mk_prim_vartype o typ_tvars |
|
39 fun type_varsl L = Utils.mk_set (Utils.curry op=) |
|
40 (Utils.rev_itlist (Utils.curry op @ o type_vars) L []); |
|
41 |
|
42 val alpha = mk_vartype "'a" |
|
43 val beta = mk_vartype "'b" |
|
44 |
|
45 val bool = Type("bool",[]); |
|
46 |
|
47 fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"}; |
|
48 |
|
49 |
|
50 (* What nonsense *) |
|
51 nonfix -->; |
|
52 val --> = -->; |
|
53 infixr 3 -->; |
|
54 |
|
55 (* hol_type -> hol_type list * hol_type *) |
|
56 fun strip_type ty = |
|
57 let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty |
|
58 val (D,r) = strip_type ty2 |
|
59 in (ty1::D, r) |
|
60 end |
|
61 handle _ => ([],ty); |
|
62 |
|
63 (* hol_type -> hol_type list *) |
|
64 fun strip_prod_type ty = |
|
65 let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty |
|
66 in strip_prod_type ty1 @ strip_prod_type ty2 |
|
67 end handle _ => [ty]; |
|
68 |
|
69 |
|
70 |
|
71 (*--------------------------------------------------------------------------- |
|
72 * |
|
73 * Terms |
|
74 * |
|
75 *---------------------------------------------------------------------------*) |
|
76 nonfix aconv; |
|
77 val aconv = Utils.curry (op aconv); |
|
78 |
|
79 fun free_vars tm = add_term_frees(tm,[]); |
|
80 |
|
81 |
|
82 (* Free variables, in order of occurrence, from left to right in the |
|
83 * syntax tree. *) |
|
84 fun free_vars_lr tm = |
|
85 let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end |
|
86 fun add (t, frees) = case t of |
|
87 Free _ => if (memb t frees) then frees else t::frees |
|
88 | Abs (_,_,body) => add(body,frees) |
|
89 | f$t => add(t, add(f, frees)) |
|
90 | _ => frees |
|
91 in rev(add(tm,[])) |
|
92 end; |
|
93 |
|
94 |
|
95 |
|
96 fun free_varsl L = Utils.mk_set aconv |
|
97 (Utils.rev_itlist (Utils.curry op @ o free_vars) L []); |
|
98 |
|
99 val type_of = type_of; |
|
100 val type_vars_in_term = map mk_prim_vartype o term_tvars; |
|
101 |
|
102 (* Can't really be very exact in Isabelle *) |
|
103 fun all_vars tm = |
|
104 let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end |
|
105 fun add (t, A) = case t of |
|
106 Free _ => if (memb t A) then A else t::A |
|
107 | Abs (s,ty,body) => add(body, add(Free(s,ty),A)) |
|
108 | f$t => add(t, add(f, A)) |
|
109 | _ => A |
|
110 in rev(add(tm,[])) |
|
111 end; |
|
112 fun all_varsl L = Utils.mk_set aconv |
|
113 (Utils.rev_itlist (Utils.curry op @ o all_vars) L []); |
|
114 |
|
115 |
|
116 (* Prelogic *) |
|
117 val subst = subst_free o map (fn (a |-> b) => (a,b)); |
|
118 |
|
119 fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty) |
|
120 fun inst theta = subst_vars (map dest_tybinding theta,[]) |
|
121 |
|
122 fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2) |
|
123 | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"}; |
|
124 |
|
125 |
|
126 (* Construction routines *) |
|
127 (* fun mk_var{Name,Ty} = Var((Name,0),Ty); *) |
|
128 fun mk_var{Name,Ty} = Free(Name,Ty); |
|
129 val mk_prim_var = Var; |
|
130 |
|
131 val string_variant = variant; |
|
132 |
|
133 local fun var_name(Var((Name,_),_)) = Name |
|
134 | var_name(Free(s,_)) = s |
|
135 | var_name _ = raise ERR{func = "variant", |
|
136 mesg = "list elem. is not a variable"} |
|
137 in |
|
138 fun variant [] v = v |
|
139 | variant vlist (Var((Name,i),ty)) = |
|
140 Var((string_variant (map var_name vlist) Name,i),ty) |
|
141 | variant vlist (Free(Name,ty)) = |
|
142 Free(string_variant (map var_name vlist) Name,ty) |
|
143 | variant _ _ = raise ERR{func = "variant", |
|
144 mesg = "2nd arg. should be a variable"} |
|
145 end; |
|
146 |
|
147 fun mk_const{Name,Ty} = Const(Name,Ty) |
|
148 fun mk_comb{Rator,Rand} = Rator $ Rand; |
|
149 |
|
150 fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
151 | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
152 | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; |
|
153 |
|
154 fun list_mk_comb (h,[]) = h |
|
155 | list_mk_comb (h,L) = |
|
156 rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h; |
|
157 |
|
158 |
|
159 fun mk_eq{lhs,rhs} = |
|
160 let val ty = type_of lhs |
|
161 val c = mk_const{Name = "op =", Ty = ty --> ty --> bool} |
|
162 in list_mk_comb(c,[lhs,rhs]) |
|
163 end |
|
164 |
|
165 fun mk_imp{ant,conseq} = |
|
166 let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool} |
|
167 in list_mk_comb(c,[ant,conseq]) |
|
168 end; |
|
169 |
|
170 fun mk_select (r as {Bvar,Body}) = |
|
171 let val ty = type_of Bvar |
|
172 val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty} |
|
173 in list_mk_comb(c,[mk_abs r]) |
|
174 end; |
|
175 |
|
176 fun mk_forall (r as {Bvar,Body}) = |
|
177 let val ty = type_of Bvar |
|
178 val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool} |
|
179 in list_mk_comb(c,[mk_abs r]) |
|
180 end; |
|
181 |
|
182 fun mk_exists (r as {Bvar,Body}) = |
|
183 let val ty = type_of Bvar |
|
184 val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool} |
|
185 in list_mk_comb(c,[mk_abs r]) |
|
186 end; |
|
187 |
|
188 |
|
189 fun mk_conj{conj1,conj2} = |
|
190 let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool} |
|
191 in list_mk_comb(c,[conj1,conj2]) |
|
192 end; |
|
193 |
|
194 fun mk_disj{disj1,disj2} = |
|
195 let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool} |
|
196 in list_mk_comb(c,[disj1,disj2]) |
|
197 end; |
|
198 |
|
199 fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]}; |
|
200 |
|
201 local |
|
202 fun mk_uncurry(xt,yt,zt) = |
|
203 mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt} |
|
204 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
|
205 | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"} |
|
206 fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false |
|
207 in |
|
208 fun mk_pabs{varstruct,body} = |
|
209 let fun mpa(varstruct,body) = |
|
210 if (is_var varstruct) |
|
211 then mk_abs{Bvar = varstruct, Body = body} |
|
212 else let val {fst,snd} = dest_pair varstruct |
|
213 in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body), |
|
214 Rand = mpa(fst,mpa(snd,body))} |
|
215 end |
|
216 in mpa(varstruct,body) |
|
217 end |
|
218 handle _ => raise ERR{func = "mk_pabs", mesg = ""}; |
|
219 end; |
|
220 |
|
221 (* Destruction routines *) |
|
222 |
|
223 datatype lambda = VAR of {Name : string, Ty : Type} |
|
224 | CONST of {Name : string, Ty : Type} |
|
225 | COMB of {Rator: Preterm, Rand : Preterm} |
|
226 | LAMB of {Bvar : Preterm, Body : Preterm}; |
|
227 |
|
228 |
|
229 fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} |
|
230 | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} |
|
231 | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} |
|
232 | dest_term(M$N) = COMB{Rator=M,Rand=N} |
|
233 | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty} |
|
234 in LAMB{Bvar = v, Body = betapply (M,v)} |
|
235 end |
|
236 | dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"}; |
|
237 |
|
238 fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty} |
|
239 | dest_var(Free(s,ty)) = {Name = s, Ty = ty} |
|
240 | dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"}; |
|
241 |
|
242 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} |
|
243 | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"}; |
|
244 |
|
245 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} |
|
246 | dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"}; |
|
247 |
|
248 fun dest_abs(a as Abs(s,ty,M)) = |
|
249 let val v = mk_var{Name = s, Ty = ty} |
|
250 in {Bvar = v, Body = betapply (a,v)} |
|
251 end |
|
252 | dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"}; |
|
253 |
|
254 fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} |
|
255 | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"}; |
|
256 |
|
257 fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} |
|
258 | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"}; |
|
259 |
|
260 fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a |
|
261 | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"}; |
|
262 |
|
263 fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a |
|
264 | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"}; |
|
265 |
|
266 fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a |
|
267 | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"}; |
|
268 |
|
269 fun dest_neg(Const("not",_) $ M) = M |
|
270 | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"}; |
|
271 |
|
272 fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} |
|
273 | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"}; |
|
274 |
|
275 fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} |
|
276 | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"}; |
|
277 |
|
278 fun mk_pair{fst,snd} = |
|
279 let val ty1 = type_of fst |
|
280 val ty2 = type_of snd |
|
281 val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2} |
|
282 in list_mk_comb(c,[fst,snd]) |
|
283 end; |
|
284 |
|
285 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
|
286 | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}; |
|
287 |
|
288 |
|
289 local val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const) |
|
290 in |
|
291 fun dest_pabs tm = |
|
292 let val {Bvar,Body} = dest_abs tm |
|
293 in {varstruct = Bvar, body = Body} |
|
294 end handle _ |
|
295 => let val {Rator,Rand} = dest_comb tm |
|
296 val _ = ucheck Rator |
|
297 val {varstruct = lv,body} = dest_pabs Rand |
|
298 val {varstruct = rv,body} = dest_pabs body |
|
299 in {varstruct = mk_pair{fst = lv, snd = rv}, body = body} |
|
300 end |
|
301 end; |
|
302 |
|
303 |
|
304 (* Garbage - ought to be dropped *) |
|
305 val lhs = #lhs o dest_eq |
|
306 val rhs = #rhs o dest_eq |
|
307 val rator = #Rator o dest_comb |
|
308 val rand = #Rand o dest_comb |
|
309 val bvar = #Bvar o dest_abs |
|
310 val body = #Body o dest_abs |
|
311 |
|
312 |
|
313 (* Query routines *) |
|
314 val is_var = can dest_var |
|
315 val is_const = can dest_const |
|
316 val is_comb = can dest_comb |
|
317 val is_abs = can dest_abs |
|
318 val is_eq = can dest_eq |
|
319 val is_imp = can dest_imp |
|
320 val is_forall = can dest_forall |
|
321 val is_exists = can dest_exists |
|
322 val is_neg = can dest_neg |
|
323 val is_conj = can dest_conj |
|
324 val is_disj = can dest_disj |
|
325 val is_pair = can dest_pair |
|
326 val is_pabs = can dest_pabs |
|
327 |
|
328 |
|
329 (* Construction of a Term from a list of Terms *) |
|
330 |
|
331 fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; |
|
332 |
|
333 (* These others are almost never used *) |
|
334 fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; |
|
335 fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t; |
|
336 fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t; |
|
337 val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) |
|
338 val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm}) |
|
339 |
|
340 |
|
341 (* Need to reverse? *) |
|
342 fun gen_all tm = list_mk_forall(free_vars tm, tm); |
|
343 |
|
344 (* Destructing a Term to a list of Terms *) |
|
345 fun strip_comb tm = |
|
346 let fun dest(M$N, A) = dest(M, N::A) |
|
347 | dest x = x |
|
348 in dest(tm,[]) |
|
349 end; |
|
350 |
|
351 fun strip_abs(tm as Abs _) = |
|
352 let val {Bvar,Body} = dest_abs tm |
|
353 val (bvs, core) = strip_abs Body |
|
354 in (Bvar::bvs, core) |
|
355 end |
|
356 | strip_abs M = ([],M); |
|
357 |
|
358 |
|
359 fun strip_imp fm = |
|
360 if (is_imp fm) |
|
361 then let val {ant,conseq} = dest_imp fm |
|
362 val (was,wb) = strip_imp conseq |
|
363 in ((ant::was), wb) |
|
364 end |
|
365 else ([],fm); |
|
366 |
|
367 fun strip_forall fm = |
|
368 if (is_forall fm) |
|
369 then let val {Bvar,Body} = dest_forall fm |
|
370 val (bvs,core) = strip_forall Body |
|
371 in ((Bvar::bvs), core) |
|
372 end |
|
373 else ([],fm); |
|
374 |
|
375 |
|
376 fun strip_exists fm = |
|
377 if (is_exists fm) |
|
378 then let val {Bvar, Body} = dest_exists fm |
|
379 val (bvs,core) = strip_exists Body |
|
380 in (Bvar::bvs, core) |
|
381 end |
|
382 else ([],fm); |
|
383 |
|
384 fun strip_conj w = |
|
385 if (is_conj w) |
|
386 then let val {conj1,conj2} = dest_conj w |
|
387 in (strip_conj conj1@strip_conj conj2) |
|
388 end |
|
389 else [w]; |
|
390 |
|
391 fun strip_disj w = |
|
392 if (is_disj w) |
|
393 then let val {disj1,disj2} = dest_disj w |
|
394 in (strip_disj disj1@strip_disj disj2) |
|
395 end |
|
396 else [w]; |
|
397 |
|
398 fun strip_pair tm = |
|
399 if (is_pair tm) |
|
400 then let val {fst,snd} = dest_pair tm |
|
401 fun dtuple t = |
|
402 if (is_pair t) |
|
403 then let val{fst,snd} = dest_pair t |
|
404 in (fst :: dtuple snd) |
|
405 end |
|
406 else [t] |
|
407 in fst::dtuple snd |
|
408 end |
|
409 else [tm]; |
|
410 |
|
411 |
|
412 fun mk_preterm tm = #t(rep_cterm tm); |
|
413 |
|
414 fun mk_prop (tm as Const("Trueprop",_) $ _) = tm |
|
415 | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop", |
|
416 Ty = bool --> mk_type{Tyop = "prop",Args=[]}}, |
|
417 Rand = tm}; |
|
418 |
|
419 fun drop_Trueprop (Const("Trueprop",_) $ X) = X |
|
420 | drop_Trueprop X = X; |
|
421 |
|
422 (* Miscellaneous *) |
|
423 |
|
424 fun mk_vstruct ty V = |
|
425 let fun follow_prod_type ty vs = |
|
426 let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty |
|
427 val (ltm,vs1) = follow_prod_type ty1 vs |
|
428 val (rtm,vs2) = follow_prod_type ty2 vs1 |
|
429 in (mk_pair{fst=ltm, snd=rtm}, vs2) |
|
430 end handle _ => (hd vs, tl vs) |
|
431 in fst(follow_prod_type ty V) |
|
432 end; |
|
433 |
|
434 |
|
435 (* Search a term for a sub-term satisfying the predicate p. *) |
|
436 fun find_term p = |
|
437 let fun find tm = |
|
438 if (p tm) |
|
439 then tm |
|
440 else if (is_abs tm) |
|
441 then find (#Body(dest_abs tm)) |
|
442 else let val {Rator,Rand} = dest_comb tm |
|
443 in find Rator handle _ => find Rand |
|
444 end handle _ => raise ERR{func = "find_term",mesg = ""} |
|
445 in find |
|
446 end; |
|
447 |
|
448 (******************************************************************* |
|
449 * find_terms: (term -> bool) -> term -> term list |
|
450 * |
|
451 * Find all subterms in a term that satisfy a given predicate p. |
|
452 * |
|
453 *******************************************************************) |
|
454 fun find_terms p = |
|
455 let fun accum tl tm = |
|
456 let val tl' = if (p tm) then (tm::tl) else tl |
|
457 in if (is_abs tm) |
|
458 then accum tl' (#Body(dest_abs tm)) |
|
459 else let val {Rator,Rand} = dest_comb tm |
|
460 in accum (accum tl' Rator) Rand |
|
461 end handle _ => tl' |
|
462 end |
|
463 in accum [] |
|
464 end; |
|
465 |
|
466 |
|
467 val Term_to_string = string_of_cterm; |
|
468 |
|
469 fun dest_relation tm = |
|
470 if (type_of tm = bool) |
|
471 then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm |
|
472 in (R,y,x) |
|
473 end handle _ => raise ERR{func="dest_relation", |
|
474 mesg="unexpected term structure"} |
|
475 else raise ERR{func="dest_relation",mesg="not a boolean term"}; |
|
476 |
|
477 fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false; |
|
478 |
|
479 fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty}, |
|
480 Body=mk_const{Name="True",Ty=bool}}; |
|
481 |
|
482 end; (* Syntax *) |