1(*  Title:      Pure/more_unify.ML
2    Author:     Makarius
3
4Add-ons to Higher-Order Unification, outside the inference kernel.
5*)
6
7signature UNIFY =
8sig
9  include UNIFY
10  val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
11  val matches_list: Context.generic -> term list -> term list -> bool
12end;
13
14structure Unify: UNIFY =
15struct
16
17(*Pattern matching*)
18fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
19  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
20  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
21  handle Pattern.MATCH => Seq.empty;
22
23(*General matching -- keep variables disjoint*)
24fun matchers _ [] = Seq.single Envir.init
25  | matchers context pairs =
26      let
27        val thy = Context.theory_of context;
28
29        val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
30        val offset = maxidx + 1;
31        val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs;
32        val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
33
34        val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
35        val pat_vars = fold (Term.add_vars o #1) pairs' [];
36
37        val decr_indexesT =
38          Term.map_atyps (fn T as TVar ((x, i), S) =>
39            if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
40        val decr_indexes =
41          Term.map_types decr_indexesT #>
42          Term.map_aterms (fn t as Var ((x, i), T) =>
43            if i > maxidx then Var ((x, i - offset), T) else t | t => t);
44
45        fun norm_tvar env ((x, i), S) =
46          let
47            val tyenv = Envir.type_env env;
48            val T' = Envir.norm_type tyenv (TVar ((x, i), S));
49          in
50            if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE
51            else SOME ((x, i - offset), (S, decr_indexesT T'))
52          end;
53
54        fun norm_var env ((x, i), T) =
55          let
56            val tyenv = Envir.type_env env;
57            val T' = Envir.norm_type tyenv T;
58            val t' = Envir.norm_term env (Var ((x, i), T'));
59          in
60            if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE
61            else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t'))
62          end;
63
64        fun result env =
65          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
66            SOME (Envir.Envir {maxidx = maxidx,
67              tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars),
68              tenv = Vartab.make (map_filter (norm_var env) pat_vars)})
69          else NONE;
70
71        val empty = Envir.empty maxidx';
72      in
73        Seq.append
74          (Seq.map_filter result (Unify.smash_unifiers context pairs' empty))
75          (first_order_matchers thy pairs empty)
76      end;
77
78fun matches_list context ps os =
79  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
80
81
82open Unify;
83
84end;
85
86