src/Pure/unify.ML
author wenzelm
Fri Jul 17 21:33:00 2009 +0200 (2009-07-17)
changeset 32032 a6a6e8031c14
parent 29269 5c25a2012975
child 32738 15bb09ca0378
permissions -rw-r--r--
tuned/modernized Envir operations;
berghofe@15797
     1
(*  Title:      Pure/unify.ML
wenzelm@16425
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   Cambridge University 1992
clasohm@0
     4
wenzelm@16425
     5
Higher-Order Unification.
clasohm@0
     6
wenzelm@16425
     7
Types as well as terms are unified.  The outermost functions assume
wenzelm@16425
     8
the terms to be unified already have the same type.  In resolution,
wenzelm@16425
     9
this is assured because both have type "prop".
clasohm@0
    10
*)
clasohm@0
    11
wenzelm@16425
    12
signature UNIFY =
wenzelm@16425
    13
sig
wenzelm@24178
    14
  val trace_bound_value: Config.value Config.T
wenzelm@24178
    15
  val trace_bound: int Config.T
wenzelm@24178
    16
  val search_bound_value: Config.value Config.T
wenzelm@24178
    17
  val search_bound: int Config.T
wenzelm@24178
    18
  val trace_simp_value: Config.value Config.T
wenzelm@24178
    19
  val trace_simp: bool Config.T
wenzelm@24178
    20
  val trace_types_value: Config.value Config.T
wenzelm@24178
    21
  val trace_types: bool Config.T
wenzelm@16425
    22
  val unifiers: theory * Envir.env * ((term * term) list) ->
wenzelm@16425
    23
    (Envir.env * (term * term) list) Seq.seq
wenzelm@19864
    24
  val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
wenzelm@19864
    25
  val matchers: theory -> (term * term) list -> Envir.env Seq.seq
wenzelm@19864
    26
  val matches_list: theory -> term list -> term list -> bool
wenzelm@16425
    27
end
clasohm@0
    28
wenzelm@19864
    29
structure Unify : UNIFY =
clasohm@0
    30
struct
clasohm@0
    31
clasohm@0
    32
(*Unification options*)
clasohm@0
    33
wenzelm@24178
    34
(*tracing starts above this depth, 0 for full*)
paulson@28173
    35
val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 50);
wenzelm@24178
    36
val trace_bound = Config.int trace_bound_value;
wenzelm@24178
    37
wenzelm@24178
    38
(*unification quits above this depth*)
paulson@28173
    39
val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 60);
wenzelm@24178
    40
val search_bound = Config.int search_bound_value;
wenzelm@24178
    41
wenzelm@24178
    42
(*print dpairs before calling SIMPL*)
wenzelm@24178
    43
val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
wenzelm@24178
    44
val trace_simp = Config.bool trace_simp_value;
wenzelm@24178
    45
wenzelm@24178
    46
(*announce potential incompleteness of type unification*)
wenzelm@24178
    47
val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
wenzelm@24178
    48
val trace_types = Config.bool trace_types_value;
wenzelm@24178
    49
clasohm@0
    50
clasohm@0
    51
type binderlist = (string*typ) list;
clasohm@0
    52
clasohm@0
    53
type dpair = binderlist * term * term;
clasohm@0
    54
wenzelm@32032
    55
fun body_type env =
wenzelm@32032
    56
  let
wenzelm@32032
    57
    val tyenv = Envir.type_env env;
wenzelm@32032
    58
    fun bT (Type ("fun", [_, T])) = bT T
wenzelm@32032
    59
      | bT (T as TVar v) =
wenzelm@32032
    60
          (case Type.lookup tyenv v of
wenzelm@32032
    61
            NONE => T
wenzelm@32032
    62
          | SOME T' => bT T')
wenzelm@32032
    63
      | bT T = T;
wenzelm@32032
    64
  in bT end;
clasohm@0
    65
wenzelm@32032
    66
fun binder_types env =
wenzelm@32032
    67
  let
wenzelm@32032
    68
    val tyenv = Envir.type_env env;
wenzelm@32032
    69
    fun bTs (Type ("fun", [T, U])) = T :: bTs U
wenzelm@32032
    70
      | bTs (T as TVar v) =
wenzelm@32032
    71
          (case Type.lookup tyenv v of
wenzelm@32032
    72
            NONE => []
wenzelm@32032
    73
          | SOME T' => bTs T')
wenzelm@32032
    74
      | bTs _ = [];
wenzelm@32032
    75
  in bTs end;
clasohm@0
    76
clasohm@0
    77
fun strip_type env T = (binder_types env T, body_type env T);
clasohm@0
    78
berghofe@12231
    79
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
clasohm@0
    80
clasohm@0
    81
wenzelm@32032
    82
(* eta normal form *)
wenzelm@32032
    83
wenzelm@32032
    84
fun eta_norm env =
wenzelm@32032
    85
  let
wenzelm@32032
    86
    val tyenv = Envir.type_env env;
wenzelm@32032
    87
    fun etif (Type ("fun", [T, U]), t) =
wenzelm@32032
    88
          Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
wenzelm@32032
    89
      | etif (TVar v, t) =
wenzelm@32032
    90
          (case Type.lookup tyenv v of
wenzelm@32032
    91
            NONE => t
wenzelm@32032
    92
          | SOME T => etif (T, t))
wenzelm@32032
    93
      | etif (_, t) = t;
wenzelm@32032
    94
    fun eta_nm (rbinder, Abs (a, T, body)) =
wenzelm@32032
    95
          Abs (a, T, eta_nm ((a, T) :: rbinder, body))
wenzelm@32032
    96
      | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
clasohm@0
    97
  in eta_nm end;
clasohm@0
    98
clasohm@0
    99
clasohm@0
   100
(*OCCURS CHECK
wenzelm@19864
   101
  Does the uvar occur in the term t?
clasohm@0
   102
  two forms of search, for whether there is a rigid path to the current term.
clasohm@0
   103
  "seen" is list of variables passed thru, is a memo variable for sharing.
berghofe@15797
   104
  This version searches for nonrigid occurrence, returns true if found.
berghofe@15797
   105
  Since terms may contain variables with same name and different types,
berghofe@15797
   106
  the occurs check must ignore the types of variables. This avoids
berghofe@15797
   107
  that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
berghofe@15797
   108
  substitution when ?'a is instantiated with T later. *)
clasohm@0
   109
fun occurs_terms (seen: (indexname list) ref,
wenzelm@19864
   110
      env: Envir.env, v: indexname, ts: term list): bool =
clasohm@0
   111
  let fun occurs [] = false
wenzelm@19864
   112
  | occurs (t::ts) =  occur t  orelse  occurs ts
clasohm@0
   113
      and occur (Const _)  = false
wenzelm@19864
   114
  | occur (Bound _)  = false
wenzelm@19864
   115
  | occur (Free _)  = false
wenzelm@19864
   116
  | occur (Var (w, T))  =
wenzelm@20083
   117
      if member (op =) (!seen) w then false
wenzelm@29269
   118
      else if Term.eq_ix (v, w) then true
wenzelm@19864
   119
        (*no need to lookup: v has no assignment*)
wenzelm@19864
   120
      else (seen := w:: !seen;
wenzelm@19864
   121
            case Envir.lookup (env, (w, T)) of
wenzelm@19864
   122
          NONE    => false
wenzelm@19864
   123
        | SOME t => occur t)
wenzelm@19864
   124
  | occur (Abs(_,_,body)) = occur body
wenzelm@19864
   125
  | occur (f$t) = occur t  orelse   occur f
clasohm@0
   126
  in  occurs ts  end;
clasohm@0
   127
clasohm@0
   128
clasohm@0
   129
clasohm@0
   130
(* f(a1,...,an)  ---->   (f,  [a1,...,an])  using the assignments*)
clasohm@0
   131
fun head_of_in (env,t) : term = case t of
clasohm@0
   132
    f$_ => head_of_in(env,f)
wenzelm@19864
   133
  | Var vT => (case Envir.lookup (env, vT) of
wenzelm@19864
   134
      SOME u => head_of_in(env,u)  |  NONE   => t)
clasohm@0
   135
  | _ => t;
clasohm@0
   136
clasohm@0
   137
clasohm@0
   138
datatype occ = NoOcc | Nonrigid | Rigid;
clasohm@0
   139
clasohm@0
   140
(* Rigid occur check
clasohm@0
   141
Returns Rigid    if it finds a rigid occurrence of the variable,
clasohm@0
   142
        Nonrigid if it finds a nonrigid path to the variable.
clasohm@0
   143
        NoOcc    otherwise.
clasohm@0
   144
  Continues searching for a rigid occurrence even if it finds a nonrigid one.
clasohm@0
   145
clasohm@0
   146
Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ]
clasohm@0
   147
   a rigid path to the variable, appearing with no arguments.
clasohm@0
   148
Here completeness is sacrificed in order to reduce danger of divergence:
clasohm@0
   149
   reject ALL rigid paths to the variable.
wenzelm@19864
   150
Could check for rigid paths to bound variables that are out of scope.
clasohm@0
   151
Not necessary because the assignment test looks at variable's ENTIRE rbinder.
clasohm@0
   152
clasohm@0
   153
Treatment of head(arg1,...,argn):
clasohm@0
   154
If head is a variable then no rigid path, switch to nonrigid search
wenzelm@19864
   155
for arg1,...,argn.
wenzelm@19864
   156
If head is an abstraction then possibly no rigid path (head could be a
clasohm@0
   157
   constant function) so again use nonrigid search.  Happens only if
wenzelm@19864
   158
   term is not in normal form.
clasohm@0
   159
clasohm@0
   160
Warning: finds a rigid occurrence of ?f in ?f(t).
clasohm@0
   161
  Should NOT be called in this case: there is a flex-flex unifier
clasohm@0
   162
*)
wenzelm@19864
   163
fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
wenzelm@19864
   164
  let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
wenzelm@19864
   165
           else NoOcc
clasohm@0
   166
      fun occurs [] = NoOcc
wenzelm@19864
   167
  | occurs (t::ts) =
clasohm@0
   168
            (case occur t of
clasohm@0
   169
               Rigid => Rigid
clasohm@0
   170
             | oc =>  (case occurs ts of NoOcc => oc  |  oc2 => oc2))
clasohm@0
   171
      and occomb (f$t) =
clasohm@0
   172
            (case occur t of
clasohm@0
   173
               Rigid => Rigid
clasohm@0
   174
             | oc =>  (case occomb f of NoOcc => oc  |  oc2 => oc2))
clasohm@0
   175
        | occomb t = occur t
clasohm@0
   176
      and occur (Const _)  = NoOcc
wenzelm@19864
   177
  | occur (Bound _)  = NoOcc
wenzelm@19864
   178
  | occur (Free _)  = NoOcc
wenzelm@19864
   179
  | occur (Var (w, T))  =
wenzelm@20083
   180
      if member (op =) (!seen) w then NoOcc
wenzelm@29269
   181
      else if Term.eq_ix (v, w) then Rigid
wenzelm@19864
   182
      else (seen := w:: !seen;
wenzelm@19864
   183
            case Envir.lookup (env, (w, T)) of
wenzelm@19864
   184
          NONE    => NoOcc
wenzelm@19864
   185
        | SOME t => occur t)
wenzelm@19864
   186
  | occur (Abs(_,_,body)) = occur body
wenzelm@19864
   187
  | occur (t as f$_) =  (*switch to nonrigid search?*)
wenzelm@19864
   188
     (case head_of_in (env,f) of
wenzelm@19864
   189
        Var (w,_) => (*w is not assigned*)
wenzelm@29269
   190
    if Term.eq_ix (v, w) then Rigid
wenzelm@19864
   191
    else  nonrigid t
wenzelm@19864
   192
      | Abs(_,_,body) => nonrigid t (*not in normal form*)
wenzelm@19864
   193
      | _ => occomb t)
clasohm@0
   194
  in  occur t  end;
clasohm@0
   195
clasohm@0
   196
wenzelm@19864
   197
exception CANTUNIFY;  (*Signals non-unifiability.  Does not signal errors!*)
wenzelm@19864
   198
exception ASSIGN; (*Raised if not an assignment*)
clasohm@0
   199
clasohm@0
   200
wenzelm@32032
   201
fun unify_types thy (T, U, env) =
wenzelm@32032
   202
  if T = U then env
wenzelm@32032
   203
  else
wenzelm@32032
   204
    let
wenzelm@32032
   205
      val Envir.Envir {maxidx, tenv, tyenv} = env;
wenzelm@32032
   206
      val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
wenzelm@32032
   207
    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
wenzelm@32032
   208
    handle Type.TUNIFY => raise CANTUNIFY;
clasohm@0
   209
wenzelm@16664
   210
fun test_unify_types thy (args as (T,U,_)) =
wenzelm@26939
   211
let val str_of = Syntax.string_of_typ_global thy;
wenzelm@16664
   212
    fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
wenzelm@16664
   213
    val env' = unify_types thy args
clasohm@0
   214
in if is_TVar(T) orelse is_TVar(U) then warn() else ();
clasohm@0
   215
   env'
clasohm@0
   216
end;
clasohm@0
   217
clasohm@0
   218
(*Is the term eta-convertible to a single variable with the given rbinder?
clasohm@0
   219
  Examples: ?a   ?f(B.0)   ?g(B.1,B.0)
clasohm@0
   220
  Result is var a for use in SIMPL. *)
clasohm@0
   221
fun get_eta_var ([], _, Var vT)  =  vT
clasohm@0
   222
  | get_eta_var (_::rbinder, n, f $ Bound i) =
wenzelm@19864
   223
  if  n=i  then  get_eta_var (rbinder, n+1, f)
wenzelm@19864
   224
     else  raise ASSIGN
clasohm@0
   225
  | get_eta_var _ = raise ASSIGN;
clasohm@0
   226
clasohm@0
   227
clasohm@0
   228
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
clasohm@0
   229
  If v occurs rigidly then nonunifiable.
clasohm@0
   230
  If v occurs nonrigidly then must use full algorithm. *)
wenzelm@16664
   231
fun assignment thy (env, rbinder, t, u) =
berghofe@15797
   232
    let val vT as (v,T) = get_eta_var (rbinder, 0, t)
berghofe@15797
   233
    in  case rigid_occurs_term (ref [], env, v, u) of
wenzelm@19864
   234
        NoOcc => let val env = unify_types thy (body_type env T,
wenzelm@19864
   235
             fastype env (rbinder,u),env)
wenzelm@19864
   236
    in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
wenzelm@19864
   237
      | Nonrigid =>  raise ASSIGN
wenzelm@19864
   238
      | Rigid =>  raise CANTUNIFY
clasohm@0
   239
    end;
clasohm@0
   240
clasohm@0
   241
clasohm@0
   242
(*Extends an rbinder with a new disagreement pair, if both are abstractions.
clasohm@0
   243
  Tries to unify types of the bound variables!
clasohm@0
   244
  Checks that binders have same length, since terms should be eta-normal;
clasohm@0
   245
    if not, raises TERM, probably indicating type mismatch.
wenzelm@19864
   246
  Uses variable a (unless the null string) to preserve user's naming.*)
wenzelm@16664
   247
fun new_dpair thy (rbinder, Abs(a,T,body1), Abs(b,U,body2), env) =
wenzelm@19864
   248
  let val env' = unify_types thy (T,U,env)
wenzelm@19864
   249
      val c = if a="" then b else a
wenzelm@19864
   250
  in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
wenzelm@16664
   251
    | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
wenzelm@16664
   252
    | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
wenzelm@16664
   253
    | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
clasohm@0
   254
clasohm@0
   255
wenzelm@16664
   256
fun head_norm_dpair thy (env, (rbinder,t,u)) : dpair * Envir.env =
wenzelm@16664
   257
     new_dpair thy (rbinder,
wenzelm@19864
   258
    eta_norm env (rbinder, Envir.head_norm env t),
wenzelm@19864
   259
      eta_norm env (rbinder, Envir.head_norm env u), env);
clasohm@0
   260
clasohm@0
   261
clasohm@0
   262
clasohm@0
   263
(*flexflex: the flex-flex pairs,  flexrigid: the flex-rigid pairs
clasohm@0
   264
  Does not perform assignments for flex-flex pairs:
lcp@646
   265
    may create nonrigid paths, which prevent other assignments.
lcp@646
   266
  Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to
lcp@646
   267
    do so caused numerous problems with no compensating advantage.
lcp@646
   268
*)
wenzelm@16664
   269
fun SIMPL0 thy (dp0, (env,flexflex,flexrigid))
wenzelm@19864
   270
  : Envir.env * dpair list * dpair list =
wenzelm@16664
   271
    let val (dp as (rbinder,t,u), env) = head_norm_dpair thy (env,dp0);
wenzelm@19864
   272
      fun SIMRANDS(f$t, g$u, env) =
wenzelm@19864
   273
      SIMPL0 thy ((rbinder,t,u), SIMRANDS(f,g,env))
wenzelm@19864
   274
        | SIMRANDS (t as _$_, _, _) =
wenzelm@19864
   275
    raise TERM ("SIMPL: operands mismatch", [t,u])
wenzelm@19864
   276
        | SIMRANDS (t, u as _$_, _) =
wenzelm@19864
   277
    raise TERM ("SIMPL: operands mismatch", [t,u])
wenzelm@19864
   278
        | SIMRANDS(_,_,env) = (env,flexflex,flexrigid);
clasohm@0
   279
    in case (head_of t, head_of u) of
clasohm@0
   280
       (Var(_,T), Var(_,U)) =>
wenzelm@19864
   281
      let val T' = body_type env T and U' = body_type env U;
wenzelm@19864
   282
    val env = unify_types thy (T',U',env)
wenzelm@19864
   283
      in (env, dp::flexflex, flexrigid) end
clasohm@0
   284
     | (Var _, _) =>
wenzelm@19864
   285
      ((assignment thy (env,rbinder,t,u), flexflex, flexrigid)
wenzelm@19864
   286
       handle ASSIGN => (env, flexflex, dp::flexrigid))
clasohm@0
   287
     | (_, Var _) =>
wenzelm@19864
   288
      ((assignment thy (env,rbinder,u,t), flexflex, flexrigid)
wenzelm@19864
   289
       handle ASSIGN => (env, flexflex, (rbinder,u,t)::flexrigid))
clasohm@0
   290
     | (Const(a,T), Const(b,U)) =>
wenzelm@19864
   291
      if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
wenzelm@19864
   292
      else raise CANTUNIFY
clasohm@0
   293
     | (Bound i,    Bound j)    =>
wenzelm@19864
   294
      if i=j  then SIMRANDS(t,u,env) else raise CANTUNIFY
clasohm@0
   295
     | (Free(a,T),  Free(b,U))  =>
wenzelm@19864
   296
      if a=b then SIMRANDS(t,u, unify_types thy (T,U,env))
wenzelm@19864
   297
      else raise CANTUNIFY
clasohm@0
   298
     | _ => raise CANTUNIFY
clasohm@0
   299
    end;
clasohm@0
   300
clasohm@0
   301
clasohm@0
   302
(* changed(env,t) checks whether the head of t is a variable assigned in env*)
clasohm@0
   303
fun changed (env, f$_) = changed (env,f)
berghofe@15797
   304
  | changed (env, Var v) =
skalberg@15531
   305
      (case Envir.lookup(env,v) of NONE=>false  |  _ => true)
clasohm@0
   306
  | changed _ = false;
clasohm@0
   307
clasohm@0
   308
clasohm@0
   309
(*Recursion needed if any of the 'head variables' have been updated
clasohm@0
   310
  Clever would be to re-do just the affected dpairs*)
wenzelm@16664
   311
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
clasohm@0
   312
    let val all as (env',flexflex,flexrigid) =
wenzelm@23178
   313
      List.foldr (SIMPL0 thy) (env,[],[]) dpairs;
wenzelm@19864
   314
  val dps = flexrigid@flexflex
clasohm@0
   315
    in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
wenzelm@16664
   316
       then SIMPL thy (env',dps) else all
clasohm@0
   317
    end;
clasohm@0
   318
clasohm@0
   319
wenzelm@19864
   320
(*Makes the terms E1,...,Em,    where Ts = [T...Tm].
clasohm@0
   321
  Each Ei is   ?Gi(B.(n-1),...,B.0), and has type Ti
clasohm@0
   322
  The B.j are bound vars of binder.
wenzelm@19864
   323
  The terms are not made in eta-normal-form, SIMPL does that later.
clasohm@0
   324
  If done here, eta-expansion must be recursive in the arguments! *)
clasohm@0
   325
fun make_args name (binder: typ list, env, []) = (env, [])   (*frequent case*)
clasohm@0
   326
  | make_args name (binder: typ list, env, Ts) : Envir.env * term list =
clasohm@0
   327
       let fun funtype T = binder--->T;
wenzelm@19864
   328
     val (env', vars) = Envir.genvars name (env, map funtype Ts)
wenzelm@18945
   329
       in  (env',  map (fn var=> Logic.combound(var, 0, length binder)) vars)  end;
clasohm@0
   330
clasohm@0
   331
clasohm@0
   332
(*Abstraction over a list of types, like list_abs*)
clasohm@0
   333
fun types_abs ([],u) = u
clasohm@0
   334
  | types_abs (T::Ts, u) = Abs("", T, types_abs(Ts,u));
clasohm@0
   335
clasohm@0
   336
(*Abstraction over the binder of a type*)
clasohm@0
   337
fun type_abs (env,T,t) = types_abs(binder_types env T, t);
clasohm@0
   338
clasohm@0
   339
clasohm@0
   340
(*MATCH taking "big steps".
clasohm@0
   341
  Copies u into the Var v, using projection on targs or imitation.
clasohm@0
   342
  A projection is allowed unless SIMPL raises an exception.
clasohm@0
   343
  Allocates new variables in projection on a higher-order argument,
clasohm@0
   344
    or if u is a variable (flex-flex dpair).
clasohm@0
   345
  Returns long sequence of every way of copying u, for backtracking
clasohm@0
   346
  For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a.
wenzelm@19864
   347
  The order for trying projections is crucial in ?b'(?a)
clasohm@0
   348
  NB "vname" is only used in the call to make_args!!   *)
wenzelm@19864
   349
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
wenzelm@19864
   350
  : (term * (Envir.env * dpair list))Seq.seq =
wenzelm@24178
   351
let
wenzelm@24178
   352
  val trace_tps = Config.get_thy thy trace_types;
wenzelm@24178
   353
  (*Produce copies of uarg and cons them in front of uargs*)
wenzelm@24178
   354
  fun copycons uarg (uargs, (env, dpairs)) =
wenzelm@19864
   355
  Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
wenzelm@19864
   356
      (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
wenzelm@19864
   357
     (env, dpairs)));
wenzelm@19864
   358
  (*Produce sequence of all possible ways of copying the arg list*)
wenzelm@19473
   359
    fun copyargs [] = Seq.cons ([],ed) Seq.empty
wenzelm@17344
   360
      | copyargs (uarg::uargs) = Seq.maps (copycons uarg) (copyargs uargs);
clasohm@0
   361
    val (uhead,uargs) = strip_comb u;
clasohm@0
   362
    val base = body_type env (fastype env (rbinder,uhead));
clasohm@0
   363
    fun joinargs (uargs',ed') = (list_comb(uhead,uargs'), ed');
clasohm@0
   364
    (*attempt projection on argument with given typ*)
clasohm@0
   365
    val Ts = map (curry (fastype env) rbinder) targs;
wenzelm@19864
   366
    fun projenv (head, (Us,bary), targ, tail) =
wenzelm@24178
   367
  let val env = if trace_tps then test_unify_types thy (base,bary,env)
wenzelm@19864
   368
          else unify_types thy (base,bary,env)
wenzelm@19864
   369
  in Seq.make (fn () =>
wenzelm@19864
   370
      let val (env',args) = make_args vname (Ts,env,Us);
wenzelm@19864
   371
    (*higher-order projection: plug in targs for bound vars*)
wenzelm@19864
   372
    fun plugin arg = list_comb(head_of arg, targs);
wenzelm@19864
   373
    val dp = (rbinder, list_comb(targ, map plugin args), u);
wenzelm@19864
   374
    val (env2,frigid,fflex) = SIMPL thy (env', dp::dpairs)
wenzelm@19864
   375
        (*may raise exception CANTUNIFY*)
wenzelm@19864
   376
      in  SOME ((list_comb(head,args), (env2, frigid@fflex)),
wenzelm@19864
   377
      tail)
wenzelm@19864
   378
      end  handle CANTUNIFY => Seq.pull tail)
wenzelm@19864
   379
  end handle CANTUNIFY => tail;
clasohm@0
   380
    (*make a list of projections*)
clasohm@0
   381
    fun make_projs (T::Ts, targ::targs) =
wenzelm@19864
   382
        (Bound(length Ts), T, targ) :: make_projs (Ts,targs)
clasohm@0
   383
      | make_projs ([],[]) = []
clasohm@0
   384
      | make_projs _ = raise TERM ("make_projs", u::targs);
clasohm@0
   385
    (*try projections and imitation*)
clasohm@0
   386
    fun matchfun ((bvar,T,targ)::projs) =
wenzelm@19864
   387
         (projenv(bvar, strip_type env T, targ, matchfun projs))
clasohm@0
   388
      | matchfun [] = (*imitation last of all*)
wenzelm@19864
   389
        (case uhead of
wenzelm@19864
   390
     Const _ => Seq.map joinargs (copyargs uargs)
wenzelm@19864
   391
         | Free _  => Seq.map joinargs (copyargs uargs)
wenzelm@19864
   392
         | _ => Seq.empty)  (*if Var, would be a loop!*)
clasohm@0
   393
in case uhead of
wenzelm@19864
   394
  Abs(a, T, body) =>
wenzelm@19864
   395
      Seq.map(fn (body', ed') => (Abs (a,T,body'), ed'))
wenzelm@19864
   396
    (mc ((a,T)::rbinder,
wenzelm@19864
   397
      (map (incr_boundvars 1) targs) @ [Bound 0], body, ed))
wenzelm@19864
   398
      | Var (w,uary) =>
wenzelm@19864
   399
      (*a flex-flex dpair: make variable for t*)
wenzelm@19864
   400
      let val (env', newhd) = Envir.genvar (#1 w) (env, Ts---> base)
wenzelm@19864
   401
    val tabs = Logic.combound(newhd, 0, length Ts)
wenzelm@19864
   402
    val tsub = list_comb(newhd,targs)
wenzelm@19864
   403
      in  Seq.single (tabs, (env', (rbinder,tsub,u):: dpairs))
wenzelm@19864
   404
      end
clasohm@0
   405
      | _ =>  matchfun(rev(make_projs(Ts, targs)))
clasohm@0
   406
end
clasohm@0
   407
in mc end;
clasohm@0
   408
clasohm@0
   409
clasohm@0
   410
(*Call matchcopy to produce assignments to the variable in the dpair*)
wenzelm@16664
   411
fun MATCH thy (env, (rbinder,t,u), dpairs)
wenzelm@19864
   412
  : (Envir.env * dpair list)Seq.seq =
berghofe@15797
   413
  let val (Var (vT as (v, T)), targs) = strip_comb t;
clasohm@0
   414
      val Ts = binder_types env T;
clasohm@0
   415
      fun new_dset (u', (env',dpairs')) =
wenzelm@19864
   416
    (*if v was updated to s, must unify s with u' *)
wenzelm@19864
   417
    case Envir.lookup (env', vT) of
wenzelm@19864
   418
        NONE => (Envir.update ((vT, types_abs(Ts, u')), env'),  dpairs')
wenzelm@19864
   419
      | SOME s => (env', ([], s, types_abs(Ts, u'))::dpairs')
wenzelm@4270
   420
  in Seq.map new_dset
wenzelm@16664
   421
         (matchcopy thy (#1 v) (rbinder, targs, u, (env,dpairs)))
clasohm@0
   422
  end;
clasohm@0
   423
clasohm@0
   424
clasohm@0
   425
clasohm@0
   426
(**** Flex-flex processing ****)
clasohm@0
   427
wenzelm@19864
   428
(*At end of unification, do flex-flex assignments like ?a -> ?f(?b)
clasohm@0
   429
  Attempts to update t with u, raising ASSIGN if impossible*)
wenzelm@19864
   430
fun ff_assign thy (env, rbinder, t, u) : Envir.env =
berghofe@15797
   431
let val vT as (v,T) = get_eta_var(rbinder,0,t)
berghofe@15797
   432
in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
wenzelm@16664
   433
   else let val env = unify_types thy (body_type env T,
wenzelm@19864
   434
          fastype env (rbinder,u),
wenzelm@19864
   435
          env)
wenzelm@19864
   436
  in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end
clasohm@0
   437
end;
clasohm@0
   438
clasohm@0
   439
clasohm@0
   440
(*Flex argument: a term, its type, and the index that refers to it.*)
clasohm@0
   441
type flarg = {t: term,  T: typ,  j: int};
clasohm@0
   442
clasohm@0
   443
clasohm@0
   444
(*Form the arguments into records for deletion/sorting.*)
clasohm@0
   445
fun flexargs ([],[],[]) = [] : flarg list
clasohm@0
   446
  | flexargs (j::js, t::ts, T::Ts) = {j=j, t=t, T=T} :: flexargs(js,ts,Ts)
clasohm@0
   447
  | flexargs _ = error"flexargs";
clasohm@0
   448
clasohm@0
   449
clasohm@0
   450
(*If an argument contains a banned Bound, then it should be deleted.
lcp@651
   451
  But if the only path is flexible, this is difficult; the code gives up!
lcp@651
   452
  In  %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *)
lcp@651
   453
exception CHANGE_FAIL;   (*flexible occurrence of banned variable*)
clasohm@0
   454
clasohm@0
   455
lcp@651
   456
(*Check whether the 'banned' bound var indices occur rigidly in t*)
wenzelm@19864
   457
fun rigid_bound (lev, banned) t =
wenzelm@19864
   458
  let val (head,args) = strip_comb t
wenzelm@19864
   459
  in
lcp@651
   460
      case head of
wenzelm@20664
   461
    Bound i => member (op =) banned (i-lev)  orelse
wenzelm@19864
   462
               exists (rigid_bound (lev, banned)) args
wenzelm@19864
   463
  | Var _ => false  (*no rigid occurrences here!*)
wenzelm@19864
   464
  | Abs (_,_,u) =>
wenzelm@19864
   465
         rigid_bound(lev+1, banned) u  orelse
wenzelm@19864
   466
         exists (rigid_bound (lev, banned)) args
wenzelm@19864
   467
  | _ => exists (rigid_bound (lev, banned)) args
clasohm@0
   468
  end;
clasohm@0
   469
lcp@651
   470
(*Squash down indices at level >=lev to delete the banned from a term.*)
lcp@651
   471
fun change_bnos banned =
wenzelm@19864
   472
  let fun change lev (Bound i) =
wenzelm@19864
   473
      if i<lev then Bound i
wenzelm@20664
   474
      else  if member (op =) banned (i-lev)
wenzelm@19864
   475
      then raise CHANGE_FAIL (**flexible occurrence: give up**)
wenzelm@19864
   476
      else  Bound (i - length (List.filter (fn j => j < i-lev) banned))
wenzelm@19864
   477
  | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
wenzelm@19864
   478
  | change lev (t$u) = change lev t $ change lev u
wenzelm@19864
   479
  | change lev t = t
lcp@651
   480
  in  change 0  end;
clasohm@0
   481
clasohm@0
   482
(*Change indices, delete the argument if it contains a banned Bound*)
lcp@651
   483
fun change_arg banned ({j,t,T}, args) : flarg list =
wenzelm@19864
   484
    if rigid_bound (0, banned) t  then  args  (*delete argument!*)
lcp@651
   485
    else  {j=j, t= change_bnos banned t, T=T} :: args;
clasohm@0
   486
clasohm@0
   487
clasohm@0
   488
(*Sort the arguments to create assignments if possible:
clasohm@0
   489
  create eta-terms like ?g(B.1,B.0) *)
clasohm@0
   490
fun arg_less ({t= Bound i1,...}, {t= Bound i2,...}) = (i2<i1)
clasohm@0
   491
  | arg_less (_:flarg, _:flarg) = false;
clasohm@0
   492
clasohm@0
   493
(*Test whether the new term would be eta-equivalent to a variable --
clasohm@0
   494
  if so then there is no point in creating a new variable*)
clasohm@0
   495
fun decreasing n ([]: flarg list) = (n=0)
clasohm@0
   496
  | decreasing n ({j,...}::args) = j=n-1 andalso decreasing (n-1) args;
clasohm@0
   497
clasohm@0
   498
(*Delete banned indices in the term, simplifying it.
clasohm@0
   499
  Force an assignment, if possible, by sorting the arguments.
clasohm@0
   500
  Update its head; squash indices in arguments. *)
clasohm@0
   501
fun clean_term banned (env,t) =
clasohm@0
   502
    let val (Var(v,T), ts) = strip_comb t
wenzelm@19864
   503
  val (Ts,U) = strip_type env T
wenzelm@19864
   504
  and js = length ts - 1  downto 0
wenzelm@19864
   505
  val args = sort (make_ord arg_less)
wenzelm@23178
   506
    (List.foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
wenzelm@19864
   507
  val ts' = map (#t) args
clasohm@0
   508
    in
clasohm@0
   509
    if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
clasohm@0
   510
    else let val (env',v') = Envir.genvar (#1v) (env, map (#T) args ---> U)
wenzelm@19864
   511
       val body = list_comb(v', map (Bound o #j) args)
wenzelm@19864
   512
       val env2 = Envir.vupdate ((((v, T), types_abs(Ts, body)),   env'))
wenzelm@19864
   513
       (*the vupdate affects ts' if they contain v*)
wenzelm@19864
   514
   in
wenzelm@19864
   515
       (env2, Envir.norm_term env2 (list_comb(v',ts')))
clasohm@0
   516
         end
clasohm@0
   517
    end;
clasohm@0
   518
clasohm@0
   519
clasohm@0
   520
(*Add tpair if not trivial or already there.
clasohm@0
   521
  Should check for swapped pairs??*)
clasohm@0
   522
fun add_tpair (rbinder, (t0,u0), tpairs) : (term*term) list =
wenzelm@19864
   523
  if t0 aconv u0 then tpairs
clasohm@0
   524
  else
wenzelm@18945
   525
  let val t = Logic.rlist_abs(rbinder, t0)  and  u = Logic.rlist_abs(rbinder, u0);
clasohm@0
   526
      fun same(t',u') = (t aconv t') andalso (u aconv u')
clasohm@0
   527
  in  if exists same tpairs  then tpairs  else (t,u)::tpairs  end;
clasohm@0
   528
clasohm@0
   529
clasohm@0
   530
(*Simplify both terms and check for assignments.
clasohm@0
   531
  Bound vars in the binder are "banned" unless used in both t AND u *)
wenzelm@19864
   532
fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
clasohm@0
   533
  let val loot = loose_bnos t  and  loou = loose_bnos u
wenzelm@19864
   534
      fun add_index (((a,T), j), (bnos, newbinder)) =
wenzelm@20664
   535
            if  member (op =) loot j  andalso  member (op =) loou j
wenzelm@19864
   536
            then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
wenzelm@19864
   537
            else  (j::bnos, newbinder);   (*remove*)
clasohm@0
   538
      val indices = 0 upto (length rbinder - 1);
wenzelm@23178
   539
      val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
clasohm@0
   540
      val (env', t') = clean_term banned (env, t);
clasohm@0
   541
      val (env'',u') = clean_term banned (env',u)
wenzelm@16664
   542
  in  (ff_assign thy (env'', rbin', t', u'), tpairs)
wenzelm@16664
   543
      handle ASSIGN => (ff_assign thy (env'', rbin', u', t'), tpairs)
clasohm@0
   544
      handle ASSIGN => (env'', add_tpair(rbin', (t',u'), tpairs))
clasohm@0
   545
  end
clasohm@0
   546
  handle CHANGE_FAIL => (env, add_tpair(rbinder, (t,u), tpairs));
clasohm@0
   547
clasohm@0
   548
clasohm@0
   549
(*IF the flex-flex dpair is an assignment THEN do it  ELSE  put in tpairs
clasohm@0
   550
  eliminates trivial tpairs like t=t, as well as repeated ones
wenzelm@19864
   551
  trivial tpairs can easily escape SIMPL:  ?A=t, ?A=?B, ?B=t gives t=t
clasohm@0
   552
  Resulting tpairs MAY NOT be in normal form:  assignments may occur here.*)
wenzelm@19864
   553
fun add_ffpair thy ((rbinder,t0,u0), (env,tpairs))
clasohm@0
   554
      : Envir.env * (term*term)list =
clasohm@0
   555
  let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
clasohm@0
   556
  in  case  (head_of t, head_of u) of
clasohm@0
   557
      (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
wenzelm@29269
   558
  if Term.eq_ix (v, w) then     (*...occur check would falsely return true!*)
wenzelm@19864
   559
      if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
wenzelm@19864
   560
      else raise TERM ("add_ffpair: Var name confusion", [t,u])
wenzelm@29269
   561
  else if TermOrd.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
wenzelm@19864
   562
       clean_ffpair thy ((rbinder, u, t), (env,tpairs))
wenzelm@16664
   563
        else clean_ffpair thy ((rbinder, t, u), (env,tpairs))
clasohm@0
   564
    | _ => raise TERM ("add_ffpair: Vars expected", [t,u])
clasohm@0
   565
  end;
clasohm@0
   566
clasohm@0
   567
clasohm@0
   568
(*Print a tracing message + list of dpairs.
clasohm@0
   569
  In t==u print u first because it may be rigid or flexible --
clasohm@0
   570
    t is always flexible.*)
wenzelm@16664
   571
fun print_dpairs thy msg (env,dpairs) =
clasohm@0
   572
  let fun pdp (rbinder,t,u) =
wenzelm@26939
   573
        let fun termT t = Syntax.pretty_term_global thy
wenzelm@18945
   574
                              (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
clasohm@0
   575
            val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
clasohm@0
   576
                          termT t];
wenzelm@12262
   577
        in tracing(Pretty.string_of(Pretty.blk(0,bsymbs))) end;
skalberg@15570
   578
  in  tracing msg;  List.app pdp dpairs  end;
clasohm@0
   579
clasohm@0
   580
clasohm@0
   581
(*Unify the dpairs in the environment.
wenzelm@19864
   582
  Returns flex-flex disagreement pairs NOT IN normal form.
clasohm@0
   583
  SIMPL may raise exception CANTUNIFY. *)
wenzelm@19864
   584
fun hounifiers (thy,env, tus : (term*term)list)
wenzelm@4270
   585
  : (Envir.env * (term*term)list)Seq.seq =
wenzelm@24178
   586
  let
wenzelm@24178
   587
    val trace_bnd = Config.get_thy thy trace_bound;
wenzelm@24178
   588
    val search_bnd = Config.get_thy thy search_bound;
wenzelm@24178
   589
    val trace_smp = Config.get_thy thy trace_simp;
wenzelm@24178
   590
    fun add_unify tdepth ((env,dpairs), reseq) =
wenzelm@19864
   591
    Seq.make (fn()=>
wenzelm@19864
   592
    let val (env',flexflex,flexrigid) =
wenzelm@24178
   593
         (if tdepth> trace_bnd andalso trace_smp
wenzelm@19864
   594
    then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
wenzelm@19864
   595
    SIMPL thy (env,dpairs))
wenzelm@19864
   596
    in case flexrigid of
wenzelm@23178
   597
        [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
wenzelm@19864
   598
      | dp::frigid' =>
wenzelm@24178
   599
    if tdepth > search_bnd then
wenzelm@19864
   600
        (warning "Unification bound exceeded"; Seq.pull reseq)
wenzelm@19864
   601
    else
wenzelm@24178
   602
    (if tdepth > trace_bnd then
wenzelm@19864
   603
        print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
wenzelm@19864
   604
     else ();
wenzelm@19864
   605
     Seq.pull (Seq.it_right (add_unify (tdepth+1))
wenzelm@19864
   606
         (MATCH thy (env',dp, frigid'@flexflex), reseq)))
wenzelm@19864
   607
    end
wenzelm@19864
   608
    handle CANTUNIFY =>
wenzelm@24178
   609
      (if tdepth > trace_bnd then tracing"Failure node" else ();
wenzelm@19864
   610
       Seq.pull reseq));
clasohm@0
   611
     val dps = map (fn(t,u)=> ([],t,u)) tus
wenzelm@16425
   612
  in add_unify 1 ((env, dps), Seq.empty) end;
clasohm@0
   613
wenzelm@18184
   614
fun unifiers (params as (thy, env, tus)) =
wenzelm@19473
   615
  Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty
wenzelm@16425
   616
    handle Pattern.Unif => Seq.empty
wenzelm@16425
   617
         | Pattern.Pattern => hounifiers params;
clasohm@0
   618
clasohm@0
   619
clasohm@0
   620
(*For smash_flexflex1*)
clasohm@0
   621
fun var_head_of (env,t) : indexname * typ =
clasohm@0
   622
  case head_of (strip_abs_body (Envir.norm_term env t)) of
clasohm@0
   623
      Var(v,T) => (v,T)
clasohm@0
   624
    | _ => raise CANTUNIFY;  (*not flexible, cannot use trivial substitution*)
clasohm@0
   625
clasohm@0
   626
clasohm@0
   627
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975)
clasohm@0
   628
  Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a
wenzelm@19864
   629
  Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a,
wenzelm@19864
   630
  though just ?g->?f is a more general unifier.
clasohm@0
   631
  Unlike Huet (1975), does not smash together all variables of same type --
clasohm@0
   632
    requires more work yet gives a less general unifier (fewer variables).
clasohm@0
   633
  Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *)
clasohm@0
   634
fun smash_flexflex1 ((t,u), env) : Envir.env =
berghofe@15797
   635
  let val vT as (v,T) = var_head_of (env,t)
berghofe@15797
   636
      and wU as (w,U) = var_head_of (env,u);
clasohm@0
   637
      val (env', var) = Envir.genvar (#1v) (env, body_type env T)
berghofe@15797
   638
      val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env')
berghofe@15797
   639
  in  if vT = wU then env''  (*the other update would be identical*)
berghofe@15797
   640
      else Envir.vupdate ((vT, type_abs (env', T, var)), env'')
clasohm@0
   641
  end;
clasohm@0
   642
clasohm@0
   643
clasohm@0
   644
(*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
clasohm@0
   645
fun smash_flexflex (env,tpairs) : Envir.env =
wenzelm@23178
   646
  List.foldr smash_flexflex1 env tpairs;
clasohm@0
   647
clasohm@0
   648
(*Returns unifiers with no remaining disagreement pairs*)
wenzelm@19864
   649
fun smash_unifiers thy tus env =
wenzelm@16425
   650
    Seq.map smash_flexflex (unifiers(thy,env,tus));
clasohm@0
   651
wenzelm@19864
   652
wenzelm@19864
   653
(*Pattern matching*)
wenzelm@32032
   654
fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
wenzelm@20020
   655
  let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
wenzelm@32032
   656
  in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
wenzelm@19864
   657
  handle Pattern.MATCH => Seq.empty;
wenzelm@19864
   658
wenzelm@19864
   659
(*General matching -- keeps variables disjoint*)
wenzelm@19864
   660
fun matchers _ [] = Seq.single (Envir.empty ~1)
wenzelm@19864
   661
  | matchers thy pairs =
wenzelm@19864
   662
      let
wenzelm@19864
   663
        val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
wenzelm@19864
   664
        val offset = maxidx + 1;
wenzelm@19864
   665
        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
wenzelm@19864
   666
        val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
wenzelm@19864
   667
wenzelm@19864
   668
        val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
wenzelm@19864
   669
        val pat_vars = fold (Term.add_vars o #1) pairs' [];
wenzelm@19864
   670
wenzelm@19864
   671
        val decr_indexesT =
wenzelm@19864
   672
          Term.map_atyps (fn T as TVar ((x, i), S) =>
wenzelm@19864
   673
            if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
wenzelm@19864
   674
        val decr_indexes =
wenzelm@20548
   675
          Term.map_types decr_indexesT #>
wenzelm@19864
   676
          Term.map_aterms (fn t as Var ((x, i), T) =>
wenzelm@19864
   677
            if i > maxidx then Var ((x, i - offset), T) else t | t => t);
wenzelm@19864
   678
wenzelm@32032
   679
        fun norm_tvar env ((x, i), S) =
wenzelm@32032
   680
          ((x, i - offset),
wenzelm@32032
   681
            (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
wenzelm@32032
   682
        fun norm_var env ((x, i), T) =
wenzelm@19864
   683
          let
wenzelm@32032
   684
            val tyenv = Envir.type_env env;
wenzelm@19864
   685
            val T' = Envir.norm_type tyenv T;
wenzelm@19864
   686
            val t' = Envir.norm_term env (Var ((x, i), T'));
wenzelm@19864
   687
          in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
wenzelm@19864
   688
wenzelm@19864
   689
        fun result env =
wenzelm@19876
   690
          if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
wenzelm@19864
   691
            SOME (Envir.Envir {maxidx = maxidx,
wenzelm@32032
   692
              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
wenzelm@32032
   693
              tenv = Vartab.make (map (norm_var env) pat_vars)})
wenzelm@19866
   694
          else NONE;
wenzelm@19864
   695
wenzelm@19864
   696
        val empty = Envir.empty maxidx';
wenzelm@19864
   697
      in
wenzelm@19876
   698
        Seq.append
wenzelm@19920
   699
          (Seq.map_filter result (smash_unifiers thy pairs' empty))
wenzelm@20020
   700
          (first_order_matchers thy pairs empty)
wenzelm@19864
   701
      end;
wenzelm@19864
   702
wenzelm@19864
   703
fun matches_list thy ps os =
wenzelm@19864
   704
  length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os)));
wenzelm@19864
   705
clasohm@0
   706
end;