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