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