1(*------------------------------------------------------------------------ 2 * First order unification restricted to specified "scheme" variables. 3 * 4 *----------------------------------------------------------------------*) 5 6structure Unify :> Unify = struct 7 8open HolKernel Psyntax liteLib Abbrev; 9infix 5 |->; 10 11val ERR = mk_HOL_ERR "Unify"; 12 13fun lookup x [] = raise ERR "lookup" "not found" 14 | lookup x ({redex,residue}::t) = 15 if aconv redex x then residue else lookup x t; 16 17fun deref_tmenv env tm = 18 if is_var tm then lookup tm env handle HOL_ERR _ => tm 19 else tm; 20 21fun restrict_tmenv P E = 22 mapfilter (fn {redex,residue} => 23 if P redex then redex |-> deref_tmenv E redex else fail()) E; 24 25fun occ env v = 26 let fun f t = 27 exists (fn fv => aconv fv v orelse f (lookup fv env) 28 handle HOL_ERR _ => false) (free_vars t) 29 handle HOL_ERR _ => false 30 in f 31 end; 32 33fun bind env v t = if occ env v t then failwith "occurs" else 34 let 35 val new_sub = v |-> subst env t; 36 val env' = map (fn {redex,residue} => (redex |-> (subst [new_sub] residue))) env 37 in new_sub::env' end 38 39(*--------------------------------------------------------------------------- 40 The following code assumes things have been renamed. 41 ---------------------------------------------------------------------------*) 42 43fun simp_unify_terms_in_env consts tm1 tm2 env = 44 let val tm1' = deref_tmenv env tm1 45 val tm2' = deref_tmenv env tm2 46 in 47 if is_var tm1' andalso not (op_mem aconv tm1' consts) 48 then if is_var tm2' andalso not (op_mem aconv tm2' consts) 49 then if aconv tm1' tm2' then env else bind env tm1' tm2' 50 else bind env tm1' tm2' 51 else 52 if is_var tm2' andalso not (op_mem aconv tm2' consts) 53 then bind env tm2' tm1' 54 else 55 case (dest_term tm1',dest_term tm2') 56 of (VAR x, VAR y) => if aconv tm1' tm2' then env 57 else failwith "unify_terms" 58 | (COMB p1,COMB p2) => 59 simp_unify_terms_in_env consts (fst p1) (fst p2) 60 (simp_unify_terms_in_env consts (snd p1) (snd p2) env) 61 | (LAMB p1,LAMB p2) => 62 let fun filt v = not (aconv v (fst p1)) andalso not (aconv v (fst p2)) 63 in restrict_tmenv filt 64 (simp_unify_terms_in_env 65 (op_set_diff aconv consts [fst p1, fst p2]) (snd p1) (snd p2) 66 (restrict_tmenv filt env)) 67 end 68 | otherwise => if aconv tm1' tm2' then env else failwith "simp_unify_terms" 69 end; 70 71 72fun simp_unify_terms consts tm1 tm2 = 73 simp_unify_terms_in_env consts tm1 tm2 []; 74 75end (* struct *) 76 77 78(* 79simp_unify_terms [] ``2 <= x`` ``m <= m`` 80SATISFY_CONV ([], [arithmeticTheory.LESS_EQ_REFL]) ``?x. 2 <= x`` 81 82simp_unify_terms [] ``f(X) /\ g(Y+2)`` ``f(2+2) /\ g(2 + Y)`` 83 84simp_unify_terms [`b:'a`] `P (x:'a) (b:'a):bool` `P (a:'a) (b:'a):bool`;; 85, `!x y:'a. Q x y`, `!z:'a. R x z`]; 86fun S facts = satisfy1 (U (map (freesl o hyp) facts)) (map concl facts); 87S facts `?a b:'a. P a b /\ R a b`; 88 89 90occ [(--`x:num`--) |-> (--`1 + 1`--)] (--`z:num`--) (--`z + x`--); 91occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`x + x`--); 92occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`y + y`--); 93occ [(--`x:num`--) |-> (--`z + 1`--)] (--`z:num`--) (--`\z. z = 1`--); 94 95 96*) 97