|
1 (* Title: HOL/Tools/TFL/usyntax.ML |
|
2 ID: $Id$ |
|
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
|
5 |
|
6 Emulation of HOL's abstract syntax functions. |
|
7 *) |
|
8 |
|
9 signature USYNTAX = |
|
10 sig |
|
11 datatype lambda = VAR of {Name : string, Ty : typ} |
|
12 | CONST of {Name : string, Ty : typ} |
|
13 | COMB of {Rator: term, Rand : term} |
|
14 | LAMB of {Bvar : term, Body : term} |
|
15 |
|
16 val alpha : typ |
|
17 |
|
18 (* Types *) |
|
19 val type_vars : typ -> typ list |
|
20 val type_varsl : typ list -> typ list |
|
21 val mk_vartype : string -> typ |
|
22 val is_vartype : typ -> bool |
|
23 val strip_prod_type : typ -> typ list |
|
24 |
|
25 (* Terms *) |
|
26 val free_vars_lr : term -> term list |
|
27 val type_vars_in_term : term -> typ list |
|
28 val dest_term : term -> lambda |
|
29 |
|
30 (* Prelogic *) |
|
31 val inst : (typ*typ) list -> term -> term |
|
32 |
|
33 (* Construction routines *) |
|
34 val mk_abs :{Bvar : term, Body : term} -> term |
|
35 |
|
36 val mk_imp :{ant : term, conseq : term} -> term |
|
37 val mk_select :{Bvar : term, Body : term} -> term |
|
38 val mk_forall :{Bvar : term, Body : term} -> term |
|
39 val mk_exists :{Bvar : term, Body : term} -> term |
|
40 val mk_conj :{conj1 : term, conj2 : term} -> term |
|
41 val mk_disj :{disj1 : term, disj2 : term} -> term |
|
42 val mk_pabs :{varstruct : term, body : term} -> term |
|
43 |
|
44 (* Destruction routines *) |
|
45 val dest_const: term -> {Name : string, Ty : typ} |
|
46 val dest_comb : term -> {Rator : term, Rand : term} |
|
47 val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list |
|
48 val dest_eq : term -> {lhs : term, rhs : term} |
|
49 val dest_imp : term -> {ant : term, conseq : term} |
|
50 val dest_forall : term -> {Bvar : term, Body : term} |
|
51 val dest_exists : term -> {Bvar : term, Body : term} |
|
52 val dest_neg : term -> term |
|
53 val dest_conj : term -> {conj1 : term, conj2 : term} |
|
54 val dest_disj : term -> {disj1 : term, disj2 : term} |
|
55 val dest_pair : term -> {fst : term, snd : term} |
|
56 val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list} |
|
57 |
|
58 val lhs : term -> term |
|
59 val rhs : term -> term |
|
60 val rand : term -> term |
|
61 |
|
62 (* Query routines *) |
|
63 val is_imp : term -> bool |
|
64 val is_forall : term -> bool |
|
65 val is_exists : term -> bool |
|
66 val is_neg : term -> bool |
|
67 val is_conj : term -> bool |
|
68 val is_disj : term -> bool |
|
69 val is_pair : term -> bool |
|
70 val is_pabs : term -> bool |
|
71 |
|
72 (* Construction of a term from a list of Preterms *) |
|
73 val list_mk_abs : (term list * term) -> term |
|
74 val list_mk_imp : (term list * term) -> term |
|
75 val list_mk_forall : (term list * term) -> term |
|
76 val list_mk_conj : term list -> term |
|
77 |
|
78 (* Destructing a term to a list of Preterms *) |
|
79 val strip_comb : term -> (term * term list) |
|
80 val strip_abs : term -> (term list * term) |
|
81 val strip_imp : term -> (term list * term) |
|
82 val strip_forall : term -> (term list * term) |
|
83 val strip_exists : term -> (term list * term) |
|
84 val strip_disj : term -> term list |
|
85 |
|
86 (* Miscellaneous *) |
|
87 val mk_vstruct : typ -> term list -> term |
|
88 val gen_all : term -> term |
|
89 val find_term : (term -> bool) -> term -> term option |
|
90 val dest_relation : term -> term * term * term |
|
91 val is_WFR : term -> bool |
|
92 val ARB : typ -> term |
|
93 end; |
|
94 |
|
95 structure USyntax: USYNTAX = |
|
96 struct |
|
97 |
|
98 infix 4 ##; |
|
99 |
|
100 fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; |
|
101 |
|
102 |
|
103 (*--------------------------------------------------------------------------- |
|
104 * |
|
105 * Types |
|
106 * |
|
107 *---------------------------------------------------------------------------*) |
|
108 val mk_prim_vartype = TVar; |
|
109 fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS); |
|
110 |
|
111 (* But internally, it's useful *) |
|
112 fun dest_vtype (TVar x) = x |
|
113 | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; |
|
114 |
|
115 val is_vartype = can dest_vtype; |
|
116 |
|
117 val type_vars = map mk_prim_vartype o typ_tvars |
|
118 fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []); |
|
119 |
|
120 val alpha = mk_vartype "'a" |
|
121 val beta = mk_vartype "'b" |
|
122 |
|
123 val strip_prod_type = HOLogic.prodT_factors; |
|
124 |
|
125 |
|
126 |
|
127 (*--------------------------------------------------------------------------- |
|
128 * |
|
129 * Terms |
|
130 * |
|
131 *---------------------------------------------------------------------------*) |
|
132 |
|
133 (* Free variables, in order of occurrence, from left to right in the |
|
134 * syntax tree. *) |
|
135 fun free_vars_lr tm = |
|
136 let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end |
|
137 fun add (t, frees) = case t of |
|
138 Free _ => if (memb t frees) then frees else t::frees |
|
139 | Abs (_,_,body) => add(body,frees) |
|
140 | f$t => add(t, add(f, frees)) |
|
141 | _ => frees |
|
142 in rev(add(tm,[])) |
|
143 end; |
|
144 |
|
145 |
|
146 |
|
147 val type_vars_in_term = map mk_prim_vartype o term_tvars; |
|
148 |
|
149 |
|
150 |
|
151 (* Prelogic *) |
|
152 fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) |
|
153 fun inst theta = subst_vars (map dest_tybinding theta,[]) |
|
154 |
|
155 |
|
156 (* Construction routines *) |
|
157 |
|
158 fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
159 | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) |
|
160 | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; |
|
161 |
|
162 |
|
163 fun mk_imp{ant,conseq} = |
|
164 let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
|
165 in list_comb(c,[ant,conseq]) |
|
166 end; |
|
167 |
|
168 fun mk_select (r as {Bvar,Body}) = |
|
169 let val ty = type_of Bvar |
|
170 val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty) |
|
171 in list_comb(c,[mk_abs r]) |
|
172 end; |
|
173 |
|
174 fun mk_forall (r as {Bvar,Body}) = |
|
175 let val ty = type_of Bvar |
|
176 val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) |
|
177 in list_comb(c,[mk_abs r]) |
|
178 end; |
|
179 |
|
180 fun mk_exists (r as {Bvar,Body}) = |
|
181 let val ty = type_of Bvar |
|
182 val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) |
|
183 in list_comb(c,[mk_abs r]) |
|
184 end; |
|
185 |
|
186 |
|
187 fun mk_conj{conj1,conj2} = |
|
188 let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
|
189 in list_comb(c,[conj1,conj2]) |
|
190 end; |
|
191 |
|
192 fun mk_disj{disj1,disj2} = |
|
193 let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) |
|
194 in list_comb(c,[disj1,disj2]) |
|
195 end; |
|
196 |
|
197 fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); |
|
198 |
|
199 local |
|
200 fun mk_uncurry(xt,yt,zt) = |
|
201 Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) |
|
202 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
|
203 | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" |
|
204 fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false |
|
205 in |
|
206 fun mk_pabs{varstruct,body} = |
|
207 let fun mpa (varstruct, body) = |
|
208 if is_var varstruct |
|
209 then mk_abs {Bvar = varstruct, Body = body} |
|
210 else let val {fst, snd} = dest_pair varstruct |
|
211 in mk_uncurry (type_of fst, type_of snd, type_of body) $ |
|
212 mpa (fst, mpa (snd, body)) |
|
213 end |
|
214 in mpa (varstruct, body) end |
|
215 handle TYPE _ => raise USYN_ERR "mk_pabs" ""; |
|
216 end; |
|
217 |
|
218 (* Destruction routines *) |
|
219 |
|
220 datatype lambda = VAR of {Name : string, Ty : typ} |
|
221 | CONST of {Name : string, Ty : typ} |
|
222 | COMB of {Rator: term, Rand : term} |
|
223 | LAMB of {Bvar : term, Body : term}; |
|
224 |
|
225 |
|
226 fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} |
|
227 | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} |
|
228 | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} |
|
229 | dest_term(M$N) = COMB{Rator=M,Rand=N} |
|
230 | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) |
|
231 in LAMB{Bvar = v, Body = Term.betapply (M,v)} |
|
232 end |
|
233 | dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; |
|
234 |
|
235 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} |
|
236 | dest_const _ = raise USYN_ERR "dest_const" "not a constant"; |
|
237 |
|
238 fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} |
|
239 | dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; |
|
240 |
|
241 fun dest_abs used (a as Abs(s, ty, M)) = |
|
242 let |
|
243 val s' = Name.variant used s; |
|
244 val v = Free(s', ty); |
|
245 in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) |
|
246 end |
|
247 | dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; |
|
248 |
|
249 fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} |
|
250 | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; |
|
251 |
|
252 fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} |
|
253 | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; |
|
254 |
|
255 fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a) |
|
256 | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; |
|
257 |
|
258 fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a) |
|
259 | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; |
|
260 |
|
261 fun dest_neg(Const("not",_) $ M) = M |
|
262 | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; |
|
263 |
|
264 fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} |
|
265 | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; |
|
266 |
|
267 fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} |
|
268 | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; |
|
269 |
|
270 fun mk_pair{fst,snd} = |
|
271 let val ty1 = type_of fst |
|
272 val ty2 = type_of snd |
|
273 val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) |
|
274 in list_comb(c,[fst,snd]) |
|
275 end; |
|
276 |
|
277 fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} |
|
278 | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; |
|
279 |
|
280 |
|
281 local fun ucheck t = (if #Name(dest_const t) = "split" then t |
|
282 else raise Match) |
|
283 in |
|
284 fun dest_pabs used tm = |
|
285 let val ({Bvar,Body}, used') = dest_abs used tm |
|
286 in {varstruct = Bvar, body = Body, used = used'} |
|
287 end handle Utils.ERR _ => |
|
288 let val {Rator,Rand} = dest_comb tm |
|
289 val _ = ucheck Rator |
|
290 val {varstruct = lv, body, used = used'} = dest_pabs used Rand |
|
291 val {varstruct = rv, body, used = used''} = dest_pabs used' body |
|
292 in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} |
|
293 end |
|
294 end; |
|
295 |
|
296 |
|
297 val lhs = #lhs o dest_eq |
|
298 val rhs = #rhs o dest_eq |
|
299 val rand = #Rand o dest_comb |
|
300 |
|
301 |
|
302 (* Query routines *) |
|
303 val is_imp = can dest_imp |
|
304 val is_forall = can dest_forall |
|
305 val is_exists = can dest_exists |
|
306 val is_neg = can dest_neg |
|
307 val is_conj = can dest_conj |
|
308 val is_disj = can dest_disj |
|
309 val is_pair = can dest_pair |
|
310 val is_pabs = can (dest_pabs []) |
|
311 |
|
312 |
|
313 (* Construction of a cterm from a list of Terms *) |
|
314 |
|
315 fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; |
|
316 |
|
317 (* These others are almost never used *) |
|
318 fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; |
|
319 fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t; |
|
320 val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) |
|
321 |
|
322 |
|
323 (* Need to reverse? *) |
|
324 fun gen_all tm = list_mk_forall(term_frees tm, tm); |
|
325 |
|
326 (* Destructing a cterm to a list of Terms *) |
|
327 fun strip_comb tm = |
|
328 let fun dest(M$N, A) = dest(M, N::A) |
|
329 | dest x = x |
|
330 in dest(tm,[]) |
|
331 end; |
|
332 |
|
333 fun strip_abs(tm as Abs _) = |
|
334 let val ({Bvar,Body}, _) = dest_abs [] tm |
|
335 val (bvs, core) = strip_abs Body |
|
336 in (Bvar::bvs, core) |
|
337 end |
|
338 | strip_abs M = ([],M); |
|
339 |
|
340 |
|
341 fun strip_imp fm = |
|
342 if (is_imp fm) |
|
343 then let val {ant,conseq} = dest_imp fm |
|
344 val (was,wb) = strip_imp conseq |
|
345 in ((ant::was), wb) |
|
346 end |
|
347 else ([],fm); |
|
348 |
|
349 fun strip_forall fm = |
|
350 if (is_forall fm) |
|
351 then let val {Bvar,Body} = dest_forall fm |
|
352 val (bvs,core) = strip_forall Body |
|
353 in ((Bvar::bvs), core) |
|
354 end |
|
355 else ([],fm); |
|
356 |
|
357 |
|
358 fun strip_exists fm = |
|
359 if (is_exists fm) |
|
360 then let val {Bvar, Body} = dest_exists fm |
|
361 val (bvs,core) = strip_exists Body |
|
362 in (Bvar::bvs, core) |
|
363 end |
|
364 else ([],fm); |
|
365 |
|
366 fun strip_disj w = |
|
367 if (is_disj w) |
|
368 then let val {disj1,disj2} = dest_disj w |
|
369 in (strip_disj disj1@strip_disj disj2) |
|
370 end |
|
371 else [w]; |
|
372 |
|
373 |
|
374 (* Miscellaneous *) |
|
375 |
|
376 fun mk_vstruct ty V = |
|
377 let fun follow_prod_type (Type("*",[ty1,ty2])) vs = |
|
378 let val (ltm,vs1) = follow_prod_type ty1 vs |
|
379 val (rtm,vs2) = follow_prod_type ty2 vs1 |
|
380 in (mk_pair{fst=ltm, snd=rtm}, vs2) end |
|
381 | follow_prod_type _ (v::vs) = (v,vs) |
|
382 in #1 (follow_prod_type ty V) end; |
|
383 |
|
384 |
|
385 (* Search a term for a sub-term satisfying the predicate p. *) |
|
386 fun find_term p = |
|
387 let fun find tm = |
|
388 if (p tm) then SOME tm |
|
389 else case tm of |
|
390 Abs(_,_,body) => find body |
|
391 | (t$u) => (case find t of NONE => find u | some => some) |
|
392 | _ => NONE |
|
393 in find |
|
394 end; |
|
395 |
|
396 fun dest_relation tm = |
|
397 if (type_of tm = HOLogic.boolT) |
|
398 then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm |
|
399 in (R,y,x) |
|
400 end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" |
|
401 else raise USYN_ERR "dest_relation" "not a boolean term"; |
|
402 |
|
403 fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true |
|
404 | is_WFR _ = false; |
|
405 |
|
406 fun ARB ty = mk_select{Bvar=Free("v",ty), |
|
407 Body=Const("True",HOLogic.boolT)}; |
|
408 |
|
409 end; |