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