1 (* ========================================================================= *)
2 (* More syntax constructors, and prelogical utilities like matching. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Create probably-fresh variable *)
14 (* ------------------------------------------------------------------------- *)
17 let gcounter = ref 0 in
18 fun ty -> let count = !gcounter in
19 (gcounter := count + 1;
20 mk_var("_"^(string_of_int count),ty));;
22 (* ------------------------------------------------------------------------- *)
23 (* Convenient functions for manipulating types. *)
24 (* ------------------------------------------------------------------------- *)
28 Tyapp("fun",[ty1;ty2]) -> (ty1,ty2)
29 | _ -> failwith "dest_fun_ty";;
31 let rec occurs_in ty bigty =
33 is_type bigty & exists (occurs_in ty) (snd(dest_type bigty));;
35 let rec tysubst alist ty =
36 try rev_assoc ty alist with Failure _ ->
37 if is_vartype ty then ty else
38 let tycon,tyvars = dest_type ty in
39 mk_type(tycon,map (tysubst alist) tyvars);;
41 (* ------------------------------------------------------------------------- *)
42 (* A bit more syntax. *)
43 (* ------------------------------------------------------------------------- *)
47 with Failure _ -> failwith "bndvar: Not an abstraction";;
51 with Failure _ -> failwith "body: Not an abstraction";;
53 let list_mk_comb(h,t) = rev_itlist (C (curry mk_comb)) t h;;
55 let list_mk_abs(vs,bod) = itlist (curry mk_abs) vs bod;;
57 let strip_comb = rev_splitlist dest_comb;;
59 let strip_abs = splitlist dest_abs;;
61 (* ------------------------------------------------------------------------- *)
62 (* Generic syntax to deal with some binary operators. *)
64 (* Note that "mk_binary" only works for monomorphic functions. *)
65 (* ------------------------------------------------------------------------- *)
69 Comb(Comb(Const(s',_),_),_) -> s' = s
72 let dest_binary s tm =
74 Comb(Comb(Const(s',_),l),r) when s' = s -> (l,r)
75 | _ -> failwith "dest_binary";;
78 let c = mk_const(s,[]) in
79 fun (l,r) -> try mk_comb(mk_comb(c,l),r)
80 with Failure _ -> failwith "mk_binary";;
82 (* ------------------------------------------------------------------------- *)
83 (* Produces a sequence of variants, considering previous inventions. *)
84 (* ------------------------------------------------------------------------- *)
86 let rec variants av vs =
87 if vs = [] then [] else
88 let vh = variant av (hd vs) in vh::(variants (vh::av) (tl vs));;
90 (* ------------------------------------------------------------------------- *)
91 (* Gets all variables (free and/or bound) in a term. *)
92 (* ------------------------------------------------------------------------- *)
95 let rec vars(acc,tm) =
96 if is_var tm then insert tm acc
97 else if is_const tm then acc
98 else if is_abs tm then
99 let v,bod = dest_abs tm in
100 vars(insert v acc,bod)
102 let l,r = dest_comb tm in
103 vars(vars(acc,l),r) in
104 fun tm -> vars([],tm);;
106 (* ------------------------------------------------------------------------- *)
107 (* General substitution (for any free expression). *)
108 (* ------------------------------------------------------------------------- *)
111 let rec ssubst ilist tm =
112 if ilist = [] then tm else
113 try fst (find ((aconv tm) o snd) ilist) with Failure _ ->
115 Comb(f,x) -> let f' = ssubst ilist f and x' = ssubst ilist x in
116 if f' == f & x' == x then tm else mk_comb(f',x')
118 let ilist' = filter (not o (vfree_in v) o snd) ilist in
119 mk_abs(v,ssubst ilist' bod)
122 let theta = filter (fun (s,t) -> Pervasives.compare s t <> 0) ilist in
123 if theta = [] then (fun tm -> tm) else
124 let ts,xs = unzip theta in
126 let gs = variants (variables tm) (map (genvar o type_of) xs) in
127 let tm' = ssubst (zip gs xs) tm in
128 if tm' == tm then tm else vsubst (zip ts gs) tm';;
130 (* ------------------------------------------------------------------------- *)
131 (* Alpha conversion term operation. *)
132 (* ------------------------------------------------------------------------- *)
135 let v0,bod = try dest_abs tm
136 with Failure _ -> failwith "alpha: Not an abstraction"in
137 if v = v0 then tm else
138 if type_of v = type_of v0 & not (vfree_in v bod) then
139 mk_abs(v,vsubst[v,v0]bod)
140 else failwith "alpha: Invalid new variable";;
142 (* ------------------------------------------------------------------------- *)
144 (* ------------------------------------------------------------------------- *)
146 let rec type_match vty cty sofar =
147 if is_vartype vty then
148 try if rev_assoc vty sofar = cty then sofar else failwith "type_match"
149 with Failure "find" -> (cty,vty)::sofar
151 let vop,vargs = dest_type vty and cop,cargs = dest_type cty in
152 if vop = cop then itlist2 type_match vargs cargs sofar
153 else failwith "type_match";;
155 (* ------------------------------------------------------------------------- *)
156 (* Conventional matching version of mk_const (but with a sanity test). *)
157 (* ------------------------------------------------------------------------- *)
159 let mk_mconst(c,ty) =
160 try let uty = get_const_type c in
161 let mat = type_match uty ty [] in
162 let con = mk_const(c,mat) in
163 if type_of con = ty then con else fail()
164 with Failure _ -> failwith "mk_const: generic type cannot be instantiated";;
166 (* ------------------------------------------------------------------------- *)
167 (* Like mk_comb, but instantiates type variables in rator if necessary. *)
168 (* ------------------------------------------------------------------------- *)
170 let mk_icomb(tm1,tm2) =
171 let "fun",[ty;_] = dest_type (type_of tm1) in
172 let tyins = type_match ty (type_of tm2) [] in
173 mk_comb(inst tyins tm1,tm2);;
175 (* ------------------------------------------------------------------------- *)
176 (* Instantiates types for constant c and iteratively makes combination. *)
177 (* ------------------------------------------------------------------------- *)
179 let list_mk_icomb cname args =
180 let atys,_ = nsplit dest_fun_ty args (get_const_type cname) in
181 let tyin = itlist2 (fun g a -> type_match g (type_of a)) atys args [] in
182 list_mk_comb(mk_const(cname,tyin),args);;
184 (* ------------------------------------------------------------------------- *)
185 (* Free variables in assumption list and conclusion of a theorem. *)
186 (* ------------------------------------------------------------------------- *)
189 let asl,c = dest_thm th in
190 itlist (union o frees) asl (frees c);;
192 (* ------------------------------------------------------------------------- *)
193 (* Is one term free in another? *)
194 (* ------------------------------------------------------------------------- *)
196 let rec free_in tm1 tm2 =
197 if aconv tm1 tm2 then true
198 else if is_comb tm2 then
199 let l,r = dest_comb tm2 in free_in tm1 l or free_in tm1 r
200 else if is_abs tm2 then
201 let bv,bod = dest_abs tm2 in
202 not (vfree_in bv tm1) & free_in tm1 bod
205 (* ------------------------------------------------------------------------- *)
206 (* Searching for terms. *)
207 (* ------------------------------------------------------------------------- *)
209 let rec find_term p tm =
211 if is_abs tm then find_term p (body tm) else
213 let l,r = dest_comb tm in
214 try find_term p l with Failure _ -> find_term p r
215 else failwith "find_term";;
218 let rec accum tl p tm =
219 let tl' = if p tm then insert tm tl else tl in
221 accum tl' p (body tm)
222 else if is_comb tm then
223 accum (accum tl' p (rator tm)) p (rand tm)
227 (* ------------------------------------------------------------------------- *)
228 (* General syntax for binders. *)
230 (* NB! The "mk_binder" function expects polytype "A", which is the domain. *)
231 (* ------------------------------------------------------------------------- *)
235 Comb(Const(s',_),Abs(_,_)) -> s' = s
238 let dest_binder s tm =
240 Comb(Const(s',_),Abs(x,t)) when s' = s -> (x,t)
241 | _ -> failwith "dest_binder";;
244 let c = mk_const(op,[]) in
245 fun (v,tm) -> mk_comb(inst [type_of v,aty] c,mk_abs(v,tm));;
247 (* ------------------------------------------------------------------------- *)
248 (* Syntax for binary operators. *)
249 (* ------------------------------------------------------------------------- *)
253 Comb(Comb(op',_),_) -> op' = op
256 let dest_binop op tm =
258 Comb(Comb(op',l),r) when op' = op -> (l,r)
259 | _ -> failwith "dest_binop";;
261 let mk_binop op tm1 =
262 let f = mk_comb(op,tm1) in
263 fun tm2 -> mk_comb(f,tm2);;
265 let list_mk_binop op = end_itlist (mk_binop op);;
267 let binops op = striplist (dest_binop op);;
269 (* ------------------------------------------------------------------------- *)
270 (* Some common special cases *)
271 (* ------------------------------------------------------------------------- *)
273 let is_conj = is_binary "/\\";;
274 let dest_conj = dest_binary "/\\";;
275 let conjuncts = striplist dest_conj;;
277 let is_imp = is_binary "==>";;
278 let dest_imp = dest_binary "==>";;
280 let is_forall = is_binder "!";;
281 let dest_forall = dest_binder "!";;
282 let strip_forall = splitlist dest_forall;;
284 let is_exists = is_binder "?";;
285 let dest_exists = dest_binder "?";;
286 let strip_exists = splitlist dest_exists;;
288 let is_disj = is_binary "\\/";;
289 let dest_disj = dest_binary "\\/";;
290 let disjuncts = striplist dest_disj;;
293 try fst(dest_const(rator tm)) = "~"
294 with Failure _ -> false;;
297 try let n,p = dest_comb tm in
298 if fst(dest_const n) = "~" then p else fail()
299 with Failure _ -> failwith "dest_neg";;
301 let is_uexists = is_binder "?!";;
302 let dest_uexists = dest_binder "?!";;
304 let dest_cons = dest_binary "CONS";;
305 let is_cons = is_binary "CONS";;
307 try let tms,nil = splitlist dest_cons tm in
308 if fst(dest_const nil) = "NIL" then tms else fail()
309 with Failure _ -> failwith "dest_list";;
310 let is_list = can dest_list;;
312 (* ------------------------------------------------------------------------- *)
313 (* Syntax for numerals. *)
314 (* ------------------------------------------------------------------------- *)
317 let rec dest_num tm =
318 if try fst(dest_const tm) = "_0" with Failure _ -> false then num_0 else
319 let l,r = dest_comb tm in
320 let n = num_2 */ dest_num r in
321 let cn = fst(dest_const l) in
322 if cn = "BIT0" then n
323 else if cn = "BIT1" then n +/ num_1
325 fun tm -> try let l,r = dest_comb tm in
326 if fst(dest_const l) = "NUMERAL" then dest_num r else fail()
327 with Failure _ -> failwith "dest_numeral";;
329 (* ------------------------------------------------------------------------- *)
330 (* Syntax for generalized abstractions. *)
332 (* These are here because they are used by the preterm->term translator; *)
333 (* preterms regard generalized abstractions as an atomic notion. This is *)
334 (* slightly unclean --- for example we need locally some operations on *)
335 (* universal quantifiers --- but probably simplest. It has to go somewhere! *)
336 (* ------------------------------------------------------------------------- *)
339 let dest_geq = dest_binary "GEQ" in
341 try if is_abs tm then dest_abs tm else
342 let l,r = dest_comb tm in
343 if not (fst(dest_const l) = "GABS") then fail() else
344 let ltm,rtm = dest_geq(snd(strip_forall(body r))) in
346 with Failure _ -> failwith "dest_gabs: Not a generalized abstraction";;
348 let is_gabs = can dest_gabs;;
352 let cop = mk_const("!",[type_of v,aty]) in
353 mk_comb(cop,mk_abs(v,t)) in
354 let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
356 let p = mk_const("GEQ",[type_of t1,aty]) in
357 mk_comb(mk_comb(p,t1),t2) in
359 if is_var tm1 then mk_abs(tm1,tm2) else
360 let fvs = frees tm1 in
361 let fty = mk_fun_ty (type_of tm1) (type_of tm2) in
362 let f = variant (frees tm1 @ frees tm2) (mk_var("f",fty)) in
363 let bod = mk_abs(f,list_mk_forall(fvs,mk_geq(mk_comb(f,tm1),tm2))) in
364 mk_comb(mk_const("GABS",[fty,aty]),bod);;
366 let list_mk_gabs(vs,bod) = itlist (curry mk_gabs) vs bod;;
368 let strip_gabs = splitlist dest_gabs;;
370 (* ------------------------------------------------------------------------- *)
371 (* Syntax for let terms. *)
372 (* ------------------------------------------------------------------------- *)
375 try let l,aargs = strip_comb tm in
376 if fst(dest_const l) <> "LET" then fail() else
377 let vars,lebod = strip_gabs (hd aargs) in
378 let eqs = zip vars (tl aargs) in
379 let le,bod = dest_comb lebod in
380 if fst(dest_const le) = "LET_END" then eqs,bod else fail()
381 with Failure _ -> failwith "dest_let: not a let-term";;
383 let is_let = can dest_let;;
385 let mk_let(assigs,bod) =
386 let lefts,rights = unzip assigs in
387 let lend = mk_comb(mk_const("LET_END",[type_of bod,aty]),bod) in
388 let lbod = list_mk_gabs(lefts,lend) in
389 let ty1,ty2 = dest_fun_ty(type_of lbod) in
390 let ltm = mk_const("LET",[ty1,aty; ty2,bty]) in
391 list_mk_comb(ltm,lbod::rights);;
393 (* ------------------------------------------------------------------------- *)
394 (* Useful function to create stylized arguments using numbers. *)
395 (* ------------------------------------------------------------------------- *)
398 let rec margs n s avoid tys =
399 if tys = [] then [] else
400 let v = variant avoid (mk_var(s^(string_of_int n),hd tys)) in
401 v::(margs (n + 1) s (v::avoid) (tl tys)) in
403 if length tys = 1 then
404 [variant avoid (mk_var(s,hd tys))]
406 margs 0 s avoid tys;;
408 (* ------------------------------------------------------------------------- *)
409 (* Director strings down a term. *)
410 (* ------------------------------------------------------------------------- *)
413 let rec find_path p tm =
415 if is_abs tm then "b"::(find_path p (body tm)) else
416 try "r"::(find_path p (rand tm))
417 with Failure _ -> "l"::(find_path p (rator tm)) in
418 fun p tm -> implode(find_path p tm);;
421 let rec follow_path s tm =
424 | "l"::t -> follow_path t (rator tm)
425 | "r"::t -> follow_path t (rand tm)
426 | _::t -> follow_path t (body tm) in
427 fun s tm -> follow_path (explode s) tm;;