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