basics.ml

   1 (* ========================================================================= *)
   2 (* More syntax constructors, and prelogical utilities like matching.         *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "fusion.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Create probably-fresh variable                                            *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let genvar =
  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));;
  21
  22 (* ------------------------------------------------------------------------- *)
  23 (* Convenient functions for manipulating types.                              *)
  24 (* ------------------------------------------------------------------------- *)
  25
  26 let dest_fun_ty ty =
  27   match ty with
  28     Tyapp("fun",[ty1;ty2]) -> (ty1,ty2)
  29   | _ -> failwith "dest_fun_ty";;
  30
  31 let rec occurs_in ty bigty =
  32   bigty = ty or
  33   is_type bigty & exists (occurs_in ty) (snd(dest_type bigty));;
  34
  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);;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* A bit more syntax.                                                        *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 let bndvar tm =
  46   try fst(dest_abs tm)
  47   with Failure _ -> failwith "bndvar: Not an abstraction";;
  48
  49 let body tm =
  50   try snd(dest_abs tm)
  51   with Failure _ -> failwith "body: Not an abstraction";;
  52
  53 let list_mk_comb(h,t) = rev_itlist (C (curry mk_comb)) t h;;
  54
  55 let list_mk_abs(vs,bod) = itlist (curry mk_abs) vs bod;;
  56
  57 let strip_comb = rev_splitlist dest_comb;;
  58
  59 let strip_abs = splitlist dest_abs;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Generic syntax to deal with some binary operators.                        *)
  63 (*                                                                           *)
  64 (* Note that "mk_binary" only works for monomorphic functions.               *)
  65 (* ------------------------------------------------------------------------- *)
  66
  67 let is_binary s tm =
  68   match tm with
  69     Comb(Comb(Const(s',_),_),_) -> s' = s
  70   | _ -> false;;
  71
  72 let dest_binary s tm =
  73   match tm with
  74     Comb(Comb(Const(s',_),l),r) when s' = s -> (l,r)
  75   | _ -> failwith "dest_binary";;
  76
  77 let mk_binary s =
  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";;
  81
  82 (* ------------------------------------------------------------------------- *)
  83 (* Produces a sequence of variants, considering previous inventions.         *)
  84 (* ------------------------------------------------------------------------- *)
  85
  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));;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Gets all variables (free and/or bound) in a term.                         *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let variables =
  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)
 101     else
 102       let l,r = dest_comb tm in
 103       vars(vars(acc,l),r) in
 104   fun tm -> vars([],tm);;
 105
 106 (* ------------------------------------------------------------------------- *)
 107 (* General substitution (for any free expression).                           *)
 108 (* ------------------------------------------------------------------------- *)
 109
 110 let subst =
 111   let rec ssubst ilist tm =
 112     if ilist = [] then tm else
 113     try fst (find ((aconv tm) o snd) ilist) with Failure _ ->
 114     match tm with
 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')
 117     | Abs(v,bod) ->
 118           let ilist' = filter (not o (vfree_in v) o snd) ilist in
 119           mk_abs(v,ssubst ilist' bod)
 120     | _ -> tm in
 121   fun ilist ->
 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
 125     fun tm ->
 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';;
 129
 130 (* ------------------------------------------------------------------------- *)
 131 (* Alpha conversion term operation.                                          *)
 132 (* ------------------------------------------------------------------------- *)
 133
 134 let alpha v tm =
 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";;
 141
 142 (* ------------------------------------------------------------------------- *)
 143 (* Type matching.                                                            *)
 144 (* ------------------------------------------------------------------------- *)
 145
 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
 150   else
 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";;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Conventional matching version of mk_const (but with a sanity test).       *)
 157 (* ------------------------------------------------------------------------- *)
 158
 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";;
 165
 166 (* ------------------------------------------------------------------------- *)
 167 (* Like mk_comb, but instantiates type variables in rator if necessary.      *)
 168 (* ------------------------------------------------------------------------- *)
 169
 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);;
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Instantiates types for constant c and iteratively makes combination.      *)
 177 (* ------------------------------------------------------------------------- *)
 178
 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);;
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* Free variables in assumption list and conclusion of a theorem.            *)
 186 (* ------------------------------------------------------------------------- *)
 187
 188 let thm_frees th =
 189   let asl,c = dest_thm th in
 190   itlist (union o frees) asl (frees c);;
 191
 192 (* ------------------------------------------------------------------------- *)
 193 (* Is one term free in another?                                              *)
 194 (* ------------------------------------------------------------------------- *)
 195
 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
 203   else false;;
 204
 205 (* ------------------------------------------------------------------------- *)
 206 (* Searching for terms.                                                      *)
 207 (* ------------------------------------------------------------------------- *)
 208
 209 let rec find_term p tm =
 210   if p tm then tm else
 211   if is_abs tm then find_term p (body tm) else
 212   if is_comb tm then
 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";;
 216
 217 let find_terms =
 218   let rec accum tl p tm =
 219     let tl' = if p tm then insert tm tl else tl in
 220     if is_abs tm then
 221        accum tl' p (body tm)
 222     else if is_comb tm then
 223        accum (accum tl' p (rator tm)) p (rand tm)
 224     else tl' in
 225   accum [];;
 226
 227 (* ------------------------------------------------------------------------- *)
 228 (* General syntax for binders.                                               *)
 229 (*                                                                           *)
 230 (* NB! The "mk_binder" function expects polytype "A", which is the domain.   *)
 231 (* ------------------------------------------------------------------------- *)
 232
 233 let is_binder s tm =
 234   match tm with
 235     Comb(Const(s',_),Abs(_,_)) -> s' = s
 236   | _ -> false;;
 237
 238 let dest_binder s tm =
 239   match tm with
 240     Comb(Const(s',_),Abs(x,t)) when s' = s -> (x,t)
 241   | _ -> failwith "dest_binder";;
 242
 243 let mk_binder op =
 244   let c = mk_const(op,[]) in
 245   fun (v,tm) -> mk_comb(inst [type_of v,aty] c,mk_abs(v,tm));;
 246
 247 (* ------------------------------------------------------------------------- *)
 248 (* Syntax for binary operators.                                              *)
 249 (* ------------------------------------------------------------------------- *)
 250
 251 let is_binop op tm =
 252   match tm with
 253     Comb(Comb(op',_),_) -> op' = op
 254   | _ -> false;;
 255
 256 let dest_binop op tm =
 257   match tm with
 258     Comb(Comb(op',l),r) when op' = op -> (l,r)
 259   | _ -> failwith "dest_binop";;
 260
 261 let mk_binop op tm1 =
 262   let f = mk_comb(op,tm1) in
 263   fun tm2 -> mk_comb(f,tm2);;
 264
 265 let list_mk_binop op = end_itlist (mk_binop op);;
 266
 267 let binops op = striplist (dest_binop op);;
 268
 269 (* ------------------------------------------------------------------------- *)
 270 (* Some common special cases                                                 *)
 271 (* ------------------------------------------------------------------------- *)
 272
 273 let is_conj = is_binary "/\\";;
 274 let dest_conj = dest_binary "/\\";;
 275 let conjuncts = striplist dest_conj;;
 276
 277 let is_imp = is_binary "==>";;
 278 let dest_imp = dest_binary "==>";;
 279
 280 let is_forall = is_binder "!";;
 281 let dest_forall = dest_binder "!";;
 282 let strip_forall = splitlist dest_forall;;
 283
 284 let is_exists = is_binder "?";;
 285 let dest_exists = dest_binder "?";;
 286 let strip_exists = splitlist dest_exists;;
 287
 288 let is_disj = is_binary "\\/";;
 289 let dest_disj = dest_binary "\\/";;
 290 let disjuncts = striplist dest_disj;;
 291
 292 let is_neg tm =
 293   try fst(dest_const(rator tm)) = "~"
 294   with Failure _ -> false;;
 295
 296 let dest_neg tm =
 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";;
 300
 301 let is_uexists = is_binder "?!";;
 302 let dest_uexists = dest_binder "?!";;
 303
 304 let dest_cons = dest_binary "CONS";;
 305 let is_cons = is_binary "CONS";;
 306 let dest_list tm =
 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;;
 311
 312 (* ------------------------------------------------------------------------- *)
 313 (* Syntax for numerals.                                                      *)
 314 (* ------------------------------------------------------------------------- *)
 315
 316 let dest_numeral =
 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
 324     else fail() in
 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";;
 328
 329 (* ------------------------------------------------------------------------- *)
 330 (* Syntax for generalized abstractions.                                      *)
 331 (*                                                                           *)
 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 (* ------------------------------------------------------------------------- *)
 337
 338 let dest_gabs =
 339   let dest_geq = dest_binary "GEQ" in
 340   fun tm ->
 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
 345         rand ltm,rtm
 346     with Failure _ -> failwith "dest_gabs: Not a generalized abstraction";;
 347
 348 let is_gabs = can dest_gabs;;
 349
 350 let mk_gabs =
 351   let mk_forall(v,t) =
 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
 355   let mk_geq(t1,t2) =
 356     let p = mk_const("GEQ",[type_of t1,aty]) in
 357     mk_comb(mk_comb(p,t1),t2) in
 358   fun (tm1,tm2) ->
 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);;
 365
 366 let list_mk_gabs(vs,bod) = itlist (curry mk_gabs) vs bod;;
 367
 368 let strip_gabs = splitlist dest_gabs;;
 369
 370 (* ------------------------------------------------------------------------- *)
 371 (* Syntax for let terms.                                                     *)
 372 (* ------------------------------------------------------------------------- *)
 373
 374 let dest_let tm =
 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";;
 382
 383 let is_let = can dest_let;;
 384
 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);;
 392
 393 (* ------------------------------------------------------------------------- *)
 394 (* Useful function to create stylized arguments using numbers.               *)
 395 (* ------------------------------------------------------------------------- *)
 396
 397 let make_args =
 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
 402   fun s avoid tys ->
 403     if length tys = 1 then
 404       [variant avoid (mk_var(s,hd tys))]
 405     else
 406       margs 0 s avoid tys;;
 407
 408 (* ------------------------------------------------------------------------- *)
 409 (* Director strings down a term.                                             *)
 410 (* ------------------------------------------------------------------------- *)
 411
 412 let find_path =
 413   let rec find_path p tm =
 414     if p tm then [] else
 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);;
 419
 420 let follow_path =
 421   let rec follow_path s tm =
 422     match s with
 423       [] -> 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;;