src/Pure/more_unify.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 63615 d786d54efc70
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/more_unify.ML
     2     Author:     Makarius
     3 
     4 Add-ons to Higher-Order Unification, outside the inference kernel.
     5 *)
     6 
     7 signature UNIFY =
     8 sig
     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
    12 end;
    13 
    14 structure Unify: UNIFY =
    15 struct
    16 
    17 (*Pattern matching*)
    18 fun 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*)
    24 fun 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 
    78 fun matches_list context ps os =
    79   length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
    80 
    81 
    82 open Unify;
    83 
    84 end;
    85