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