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