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