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 (* ========================================================================= *)
10 (* ------------------------------------------------------------------------- *)
11 (* Create probably-fresh variable *)
12 (* ------------------------------------------------------------------------- *)
15 let gcounter = ref 0 in
16 fun ty -> let count = !gcounter in
17 (gcounter := count + 1;
18 mk_var("_"^(string_of_int count),ty));;
20 (* ------------------------------------------------------------------------- *)
21 (* Convenient functions for manipulating types. *)
22 (* ------------------------------------------------------------------------- *)
26 Tyapp("fun",[ty1;ty2]) -> (ty1,ty2)
27 | _ -> failwith "dest_fun_ty";;
29 let rec occurs_in ty bigty =
31 is_type bigty & exists (occurs_in ty) (snd(dest_type bigty));;
33 let rec tysubst alist ty =
34 try rev_assoc ty alist with Failure _ ->
35 if is_vartype ty then ty else
36 let tycon,tyvars = dest_type ty in
37 mk_type(tycon,map (tysubst alist) tyvars);;
39 (* ------------------------------------------------------------------------- *)
40 (* A bit more syntax. *)
41 (* ------------------------------------------------------------------------- *)
45 with Failure _ -> failwith "bndvar: Not an abstraction";;
49 with Failure _ -> failwith "body: Not an abstraction";;
51 let list_mk_comb(h,t) = rev_itlist (C (curry mk_comb)) t h;;
53 let list_mk_abs(vs,bod) = itlist (curry mk_abs) vs bod;;
55 let strip_comb = rev_splitlist dest_comb;;
57 let strip_abs = splitlist dest_abs;;
59 (* ------------------------------------------------------------------------- *)
60 (* Generic syntax to deal with some binary operators. *)
62 (* Note that "mk_binary" only works for monomorphic functions. *)
63 (* ------------------------------------------------------------------------- *)
67 Comb(Comb(Const(s',_),_),_) -> s' = s
70 let dest_binary s tm =
72 Comb(Comb(Const(s',_),l),r) when s' = s -> (l,r)
73 | _ -> failwith "dest_binary";;
76 let c = mk_const(s,[]) in
77 fun (l,r) -> try mk_comb(mk_comb(c,l),r)
78 with Failure _ -> failwith "mk_binary";;
80 (* ------------------------------------------------------------------------- *)
81 (* Produces a sequence of variants, considering previous inventions. *)
82 (* ------------------------------------------------------------------------- *)
84 let rec variants av vs =
85 if vs = [] then [] else
86 let vh = variant av (hd vs) in vh::(variants (vh::av) (tl vs));;
88 (* ------------------------------------------------------------------------- *)
89 (* Gets all variables (free and/or bound) in a term. *)
90 (* ------------------------------------------------------------------------- *)
93 let rec vars(acc,tm) =
94 if is_var tm then insert tm acc
95 else if is_const tm then acc
96 else if is_abs tm then
97 let v,bod = dest_abs tm in
98 vars(insert v acc,bod)
100 let l,r = dest_comb tm in
101 vars(vars(acc,l),r) in
102 fun tm -> vars([],tm);;
104 (* ------------------------------------------------------------------------- *)
105 (* General substitution (for any free expression). *)
106 (* ------------------------------------------------------------------------- *)
109 let rec ssubst ilist tm =
110 if ilist = [] then tm else
111 try fst (find ((aconv tm) o snd) ilist) with Failure _ ->
113 Comb(f,x) -> let f' = ssubst ilist f and x' = ssubst ilist x in
114 if f' == f & x' == x then tm else mk_comb(f',x')
116 let ilist' = filter (not o (vfree_in v) o snd) ilist in
117 mk_abs(v,ssubst ilist' bod)
120 let theta = filter (fun (s,t) -> Pervasives.compare s t <> 0) ilist in
121 if theta = [] then (fun tm -> tm) else
122 let ts,xs = unzip theta in
124 let gs = variants (variables tm) (map (genvar o type_of) xs) in
125 let tm' = ssubst (zip gs xs) tm in
126 if tm' == tm then tm else vsubst (zip ts gs) tm';;
128 (* ------------------------------------------------------------------------- *)
129 (* Alpha conversion term operation. *)
130 (* ------------------------------------------------------------------------- *)
133 let v0,bod = try dest_abs tm
134 with Failure _ -> failwith "alpha: Not an abstraction"in
135 if v = v0 then tm else
136 if type_of v = type_of v0 & not (vfree_in v bod) then
137 mk_abs(v,vsubst[v,v0]bod)
138 else failwith "alpha: Invalid new variable";;
140 (* ------------------------------------------------------------------------- *)
142 (* ------------------------------------------------------------------------- *)
144 let rec type_match vty cty sofar =
145 if is_vartype vty then
146 try if rev_assoc vty sofar = cty then sofar else failwith "type_match"
147 with Failure "find" -> (cty,vty)::sofar
149 let vop,vargs = dest_type vty and cop,cargs = dest_type cty in
150 if vop = cop then itlist2 type_match vargs cargs sofar
151 else failwith "type_match";;
153 (* ------------------------------------------------------------------------- *)
154 (* Conventional matching version of mk_const (but with a sanity test). *)
155 (* ------------------------------------------------------------------------- *)
157 let mk_mconst(c,ty) =
158 try let uty = get_const_type c in
159 let mat = type_match uty ty [] in
160 let con = mk_const(c,mat) in
161 if type_of con = ty then con else fail()
162 with Failure _ -> failwith "mk_const: generic type cannot be instantiated";;
164 (* ------------------------------------------------------------------------- *)
165 (* Like mk_comb, but instantiates type variables in rator if necessary. *)
166 (* ------------------------------------------------------------------------- *)
168 let mk_icomb(tm1,tm2) =
169 let "fun",[ty;_] = dest_type (type_of tm1) in
170 let tyins = type_match ty (type_of tm2) [] in
171 mk_comb(inst tyins tm1,tm2);;
173 (* ------------------------------------------------------------------------- *)
174 (* Instantiates types for constant c and iteratively makes combination. *)
175 (* ------------------------------------------------------------------------- *)
177 let list_mk_icomb cname args =
178 let atys,_ = nsplit dest_fun_ty args (get_const_type cname) in
179 let tyin = itlist2 (fun g a -> type_match g (type_of a)) atys args [] in
180 list_mk_comb(mk_const(cname,tyin),args);;
182 (* ------------------------------------------------------------------------- *)
183 (* Free variables in assumption list and conclusion of a theorem. *)
184 (* ------------------------------------------------------------------------- *)
187 let asl,c = dest_thm th in
188 itlist (union o frees) asl (frees c);;
190 (* ------------------------------------------------------------------------- *)
191 (* Is one term free in another? *)
192 (* ------------------------------------------------------------------------- *)
194 let rec free_in tm1 tm2 =
195 if aconv tm1 tm2 then true
196 else if is_comb tm2 then
197 let l,r = dest_comb tm2 in free_in tm1 l or free_in tm1 r
198 else if is_abs tm2 then
199 let bv,bod = dest_abs tm2 in
200 not (vfree_in bv tm1) & free_in tm1 bod
203 (* ------------------------------------------------------------------------- *)
204 (* Searching for terms. *)
205 (* ------------------------------------------------------------------------- *)
207 let rec find_term p tm =
209 if is_abs tm then find_term p (body tm) else
211 let l,r = dest_comb tm in
212 try find_term p l with Failure _ -> find_term p r
213 else failwith "find_term";;
216 let rec accum tl p tm =
217 let tl' = if p tm then insert tm tl else tl in
219 accum tl' p (body tm)
220 else if is_comb tm then
221 accum (accum tl' p (rator tm)) p (rand tm)
225 (* ------------------------------------------------------------------------- *)
226 (* General syntax for binders. *)
228 (* NB! The "mk_binder" function expects polytype "A", which is the domain. *)
229 (* ------------------------------------------------------------------------- *)
233 Comb(Const(s',_),Abs(_,_)) -> s' = s
236 let dest_binder s tm =
238 Comb(Const(s',_),Abs(x,t)) when s' = s -> (x,t)
239 | _ -> failwith "dest_binder";;
242 let c = mk_const(op,[]) in
243 fun (v,tm) -> mk_comb(inst [type_of v,aty] c,mk_abs(v,tm));;
245 (* ------------------------------------------------------------------------- *)
246 (* Syntax for binary operators. *)
247 (* ------------------------------------------------------------------------- *)
251 Comb(Comb(op',_),_) -> op' = op
254 let dest_binop op tm =
256 Comb(Comb(op',l),r) when op' = op -> (l,r)
257 | _ -> failwith "dest_binop";;
259 let mk_binop op tm1 =
260 let f = mk_comb(op,tm1) in
261 fun tm2 -> mk_comb(f,tm2);;
263 let list_mk_binop op = end_itlist (mk_binop op);;
265 let binops op = striplist (dest_binop op);;
267 (* ------------------------------------------------------------------------- *)
268 (* Some common special cases *)
269 (* ------------------------------------------------------------------------- *)
271 let is_conj = is_binary "/\\";;
272 let dest_conj = dest_binary "/\\";;
273 let conjuncts = striplist dest_conj;;
275 let is_imp = is_binary "==>";;
276 let dest_imp = dest_binary "==>";;
278 let is_forall = is_binder "!";;
279 let dest_forall = dest_binder "!";;
280 let strip_forall = splitlist dest_forall;;
282 let is_exists = is_binder "?";;
283 let dest_exists = dest_binder "?";;
284 let strip_exists = splitlist dest_exists;;
286 let is_disj = is_binary "\\/";;
287 let dest_disj = dest_binary "\\/";;
288 let disjuncts = striplist dest_disj;;
291 try fst(dest_const(rator tm)) = "~"
292 with Failure _ -> false;;
295 try let n,p = dest_comb tm in
296 if fst(dest_const n) = "~" then p else fail()
297 with Failure _ -> failwith "dest_neg";;
299 let is_uexists = is_binder "?!";;
300 let dest_uexists = dest_binder "?!";;
302 let dest_cons = dest_binary "CONS";;
303 let is_cons = is_binary "CONS";;
305 try let tms,nil = splitlist dest_cons tm in
306 if fst(dest_const nil) = "NIL" then tms else fail()
307 with Failure _ -> failwith "dest_list";;
308 let is_list = can dest_list;;
310 (* ------------------------------------------------------------------------- *)
311 (* Syntax for numerals. *)
312 (* ------------------------------------------------------------------------- *)
315 let rec dest_num tm =
316 if try fst(dest_const tm) = "_0" with Failure _ -> false then num_0 else
317 let l,r = dest_comb tm in
318 let n = num_2 */ dest_num r in
319 let cn = fst(dest_const l) in
320 if cn = "BIT0" then n
321 else if cn = "BIT1" then n +/ num_1
323 fun tm -> try let l,r = dest_comb tm in
324 if fst(dest_const l) = "NUMERAL" then dest_num r else fail()
325 with Failure _ -> failwith "dest_numeral";;
327 (* ------------------------------------------------------------------------- *)
328 (* Syntax for generalized abstractions. *)
330 (* These are here because they are used by the preterm->term translator; *)
331 (* preterms regard generalized abstractions as an atomic notion. This is *)
332 (* slightly unclean --- for example we need locally some operations on *)
333 (* universal quantifiers --- but probably simplest. It has to go somewhere! *)
334 (* ------------------------------------------------------------------------- *)
337 let dest_geq = dest_binary "GEQ" in
339 try if is_abs tm then dest_abs tm else
340 let l,r = dest_comb tm in
341 if not (fst(dest_const l) = "GABS") then fail() else
342 let ltm,rtm = dest_geq(snd(strip_forall(body r))) in
344 with Failure _ -> failwith "dest_gabs: Not a generalized abstraction";;
346 let is_gabs = can dest_gabs;;
350 let cop = mk_const("!",[type_of v,aty]) in
351 mk_comb(cop,mk_abs(v,t)) in
352 let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
354 let p = mk_const("GEQ",[type_of t1,aty]) in
355 mk_comb(mk_comb(p,t1),t2) in
357 if is_var tm1 then mk_abs(tm1,tm2) else
358 let fvs = frees tm1 in
359 let fty = mk_fun_ty (type_of tm1) (type_of tm2) in
360 let f = variant (frees tm1 @ frees tm2) (mk_var("f",fty)) in
361 let bod = mk_abs(f,list_mk_forall(fvs,mk_geq(mk_comb(f,tm1),tm2))) in
362 mk_comb(mk_const("GABS",[fty,aty]),bod);;
364 let list_mk_gabs(vs,bod) = itlist (curry mk_gabs) vs bod;;
366 let strip_gabs = splitlist dest_gabs;;
368 (* ------------------------------------------------------------------------- *)
369 (* Syntax for let terms. *)
370 (* ------------------------------------------------------------------------- *)
373 try let l,aargs = strip_comb tm in
374 if fst(dest_const l) <> "LET" then fail() else
375 let vars,lebod = strip_gabs (hd aargs) in
376 let eqs = zip vars (tl aargs) in
377 let le,bod = dest_comb lebod in
378 if fst(dest_const le) = "LET_END" then eqs,bod else fail()
379 with Failure _ -> failwith "dest_let: not a let-term";;
381 let is_let = can dest_let;;
383 let mk_let(assigs,bod) =
384 let lefts,rights = unzip assigs in
385 let lend = mk_comb(mk_const("LET_END",[type_of bod,aty]),bod) in
386 let lbod = list_mk_gabs(lefts,lend) in
387 let ty1,ty2 = dest_fun_ty(type_of lbod) in
388 let ltm = mk_const("LET",[ty1,aty; ty2,bty]) in
389 list_mk_comb(ltm,lbod::rights);;
391 (* ------------------------------------------------------------------------- *)
392 (* Useful function to create stylized arguments using numbers. *)
393 (* ------------------------------------------------------------------------- *)
396 let rec margs n s avoid tys =
397 if tys = [] then [] else
398 let v = variant avoid (mk_var(s^(string_of_int n),hd tys)) in
399 v::(margs (n + 1) s (v::avoid) (tl tys)) in
401 if length tys = 1 then
402 [variant avoid (mk_var(s,hd tys))]
404 margs 0 s avoid tys;;
406 (* ------------------------------------------------------------------------- *)
407 (* Director strings down a term. *)
408 (* ------------------------------------------------------------------------- *)
411 let rec find_path p tm =
413 if is_abs tm then "b"::(find_path p (body tm)) else
414 try "r"::(find_path p (rand tm))
415 with Failure _ -> "l"::(find_path p (rator tm)) in
416 fun p tm -> implode(find_path p tm);;
419 let rec follow_path s tm =
422 | "l"::t -> follow_path t (rator tm)
423 | "r"::t -> follow_path t (rand tm)
424 | _::t -> follow_path t (body tm) in
425 fun s tm -> follow_path (explode s) tm;;