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