Proofrecording/diffs/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 (* ------------------------------------------------------------------------- *)
  11 (* Create probably-fresh variable                                            *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let genvar =
  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));;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Convenient functions for manipulating types.                              *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 let dest_fun_ty ty =
  25   match ty with
  26     Tyapp("fun",[ty1;ty2]) -> (ty1,ty2)
  27   | _ -> failwith "dest_fun_ty";;
  28
  29 let rec occurs_in ty bigty =
  30   bigty = ty or
  31   is_type bigty & exists (occurs_in ty) (snd(dest_type bigty));;
  32
  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);;
  38
  39 (* ------------------------------------------------------------------------- *)
  40 (* A bit more syntax.                                                        *)
  41 (* ------------------------------------------------------------------------- *)
  42
  43 let bndvar tm =
  44   try fst(dest_abs tm)
  45   with Failure _ -> failwith "bndvar: Not an abstraction";;
  46
  47 let body tm =
  48   try snd(dest_abs tm)
  49   with Failure _ -> failwith "body: Not an abstraction";;
  50
  51 let list_mk_comb(h,t) = rev_itlist (C (curry mk_comb)) t h;;
  52
  53 let list_mk_abs(vs,bod) = itlist (curry mk_abs) vs bod;;
  54
  55 let strip_comb = rev_splitlist dest_comb;;
  56
  57 let strip_abs = splitlist dest_abs;;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* Generic syntax to deal with some binary operators.                        *)
  61 (*                                                                           *)
  62 (* Note that "mk_binary" only works for monomorphic functions.               *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let is_binary s tm =
  66   match tm with
  67     Comb(Comb(Const(s',_),_),_) -> s' = s
  68   | _ -> false;;
  69
  70 let dest_binary s tm =
  71   match tm with
  72     Comb(Comb(Const(s',_),l),r) when s' = s -> (l,r)
  73   | _ -> failwith "dest_binary";;
  74
  75 let mk_binary s =
  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";;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* Produces a sequence of variants, considering previous inventions.         *)
  82 (* ------------------------------------------------------------------------- *)
  83
  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));;
  87
  88 (* ------------------------------------------------------------------------- *)
  89 (* Gets all variables (free and/or bound) in a term.                         *)
  90 (* ------------------------------------------------------------------------- *)
  91
  92 let variables =
  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)
  99     else
 100       let l,r = dest_comb tm in
 101       vars(vars(acc,l),r) in
 102   fun tm -> vars([],tm);;
 103
 104 (* ------------------------------------------------------------------------- *)
 105 (* General substitution (for any free expression).                           *)
 106 (* ------------------------------------------------------------------------- *)
 107
 108 let subst =
 109   let rec ssubst ilist tm =
 110     if ilist = [] then tm else
 111     try fst (find ((aconv tm) o snd) ilist) with Failure _ ->
 112     match tm with
 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')
 115     | Abs(v,bod) ->
 116           let ilist' = filter (not o (vfree_in v) o snd) ilist in
 117           mk_abs(v,ssubst ilist' bod)
 118     | _ -> tm in
 119   fun ilist ->
 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
 123     fun tm ->
 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';;
 127
 128 (* ------------------------------------------------------------------------- *)
 129 (* Alpha conversion term operation.                                          *)
 130 (* ------------------------------------------------------------------------- *)
 131
 132 let alpha v tm =
 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";;
 139
 140 (* ------------------------------------------------------------------------- *)
 141 (* Type matching.                                                            *)
 142 (* ------------------------------------------------------------------------- *)
 143
 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
 148   else
 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";;
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* Conventional matching version of mk_const (but with a sanity test).       *)
 155 (* ------------------------------------------------------------------------- *)
 156
 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";;
 163
 164 (* ------------------------------------------------------------------------- *)
 165 (* Like mk_comb, but instantiates type variables in rator if necessary.      *)
 166 (* ------------------------------------------------------------------------- *)
 167
 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);;
 172
 173 (* ------------------------------------------------------------------------- *)
 174 (* Instantiates types for constant c and iteratively makes combination.      *)
 175 (* ------------------------------------------------------------------------- *)
 176
 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);;
 181
 182 (* ------------------------------------------------------------------------- *)
 183 (* Free variables in assumption list and conclusion of a theorem.            *)
 184 (* ------------------------------------------------------------------------- *)
 185
 186 let thm_frees th =
 187   let asl,c = dest_thm th in
 188   itlist (union o frees) asl (frees c);;
 189
 190 (* ------------------------------------------------------------------------- *)
 191 (* Is one term free in another?                                              *)
 192 (* ------------------------------------------------------------------------- *)
 193
 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
 201   else false;;
 202
 203 (* ------------------------------------------------------------------------- *)
 204 (* Searching for terms.                                                      *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207 let rec find_term p tm =
 208   if p tm then tm else
 209   if is_abs tm then find_term p (body tm) else
 210   if is_comb tm then
 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";;
 214
 215 let find_terms =
 216   let rec accum tl p tm =
 217     let tl' = if p tm then insert tm tl else tl in
 218     if is_abs tm then
 219        accum tl' p (body tm)
 220     else if is_comb tm then
 221        accum (accum tl' p (rator tm)) p (rand tm)
 222     else tl' in
 223   accum [];;
 224
 225 (* ------------------------------------------------------------------------- *)
 226 (* General syntax for binders.                                               *)
 227 (*                                                                           *)
 228 (* NB! The "mk_binder" function expects polytype "A", which is the domain.   *)
 229 (* ------------------------------------------------------------------------- *)
 230
 231 let is_binder s tm =
 232   match tm with
 233     Comb(Const(s',_),Abs(_,_)) -> s' = s
 234   | _ -> false;;
 235
 236 let dest_binder s tm =
 237   match tm with
 238     Comb(Const(s',_),Abs(x,t)) when s' = s -> (x,t)
 239   | _ -> failwith "dest_binder";;
 240
 241 let mk_binder op =
 242   let c = mk_const(op,[]) in
 243   fun (v,tm) -> mk_comb(inst [type_of v,aty] c,mk_abs(v,tm));;
 244
 245 (* ------------------------------------------------------------------------- *)
 246 (* Syntax for binary operators.                                              *)
 247 (* ------------------------------------------------------------------------- *)
 248
 249 let is_binop op tm =
 250   match tm with
 251     Comb(Comb(op',_),_) -> op' = op
 252   | _ -> false;;
 253
 254 let dest_binop op tm =
 255   match tm with
 256     Comb(Comb(op',l),r) when op' = op -> (l,r)
 257   | _ -> failwith "dest_binop";;
 258
 259 let mk_binop op tm1 =
 260   let f = mk_comb(op,tm1) in
 261   fun tm2 -> mk_comb(f,tm2);;
 262
 263 let list_mk_binop op = end_itlist (mk_binop op);;
 264
 265 let binops op = striplist (dest_binop op);;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Some common special cases                                                 *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let is_conj = is_binary "/\\";;
 272 let dest_conj = dest_binary "/\\";;
 273 let conjuncts = striplist dest_conj;;
 274
 275 let is_imp = is_binary "==>";;
 276 let dest_imp = dest_binary "==>";;
 277
 278 let is_forall = is_binder "!";;
 279 let dest_forall = dest_binder "!";;
 280 let strip_forall = splitlist dest_forall;;
 281
 282 let is_exists = is_binder "?";;
 283 let dest_exists = dest_binder "?";;
 284 let strip_exists = splitlist dest_exists;;
 285
 286 let is_disj = is_binary "\\/";;
 287 let dest_disj = dest_binary "\\/";;
 288 let disjuncts = striplist dest_disj;;
 289
 290 let is_neg tm =
 291   try fst(dest_const(rator tm)) = "~"
 292   with Failure _ -> false;;
 293
 294 let dest_neg tm =
 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";;
 298
 299 let is_uexists = is_binder "?!";;
 300 let dest_uexists = dest_binder "?!";;
 301
 302 let dest_cons = dest_binary "CONS";;
 303 let is_cons = is_binary "CONS";;
 304 let dest_list tm =
 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;;
 309
 310 (* ------------------------------------------------------------------------- *)
 311 (* Syntax for numerals.                                                      *)
 312 (* ------------------------------------------------------------------------- *)
 313
 314 let dest_numeral =
 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
 322     else fail() in
 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";;
 326
 327 (* ------------------------------------------------------------------------- *)
 328 (* Syntax for generalized abstractions.                                      *)
 329 (*                                                                           *)
 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 (* ------------------------------------------------------------------------- *)
 335
 336 let dest_gabs =
 337   let dest_geq = dest_binary "GEQ" in
 338   fun tm ->
 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
 343         rand ltm,rtm
 344     with Failure _ -> failwith "dest_gabs: Not a generalized abstraction";;
 345
 346 let is_gabs = can dest_gabs;;
 347
 348 let mk_gabs =
 349   let mk_forall(v,t) =
 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
 353   let mk_geq(t1,t2) =
 354     let p = mk_const("GEQ",[type_of t1,aty]) in
 355     mk_comb(mk_comb(p,t1),t2) in
 356   fun (tm1,tm2) ->
 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);;
 363
 364 let list_mk_gabs(vs,bod) = itlist (curry mk_gabs) vs bod;;
 365
 366 let strip_gabs = splitlist dest_gabs;;
 367
 368 (* ------------------------------------------------------------------------- *)
 369 (* Syntax for let terms.                                                     *)
 370 (* ------------------------------------------------------------------------- *)
 371
 372 let dest_let tm =
 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";;
 380
 381 let is_let = can dest_let;;
 382
 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);;
 390
 391 (* ------------------------------------------------------------------------- *)
 392 (* Useful function to create stylized arguments using numbers.               *)
 393 (* ------------------------------------------------------------------------- *)
 394
 395 let make_args =
 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
 400   fun s avoid tys ->
 401     if length tys = 1 then
 402       [variant avoid (mk_var(s,hd tys))]
 403     else
 404       margs 0 s avoid tys;;
 405
 406 (* ------------------------------------------------------------------------- *)
 407 (* Director strings down a term.                                             *)
 408 (* ------------------------------------------------------------------------- *)
 409
 410 let find_path =
 411   let rec find_path p tm =
 412     if p tm then [] else
 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);;
 417
 418 let follow_path =
 419   let rec follow_path s tm =
 420     match s with
 421       [] -> 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;;