src/Pure/envir.ML
author wenzelm
Sat, 14 Apr 2007 17:36:05 +0200
changeset 22678 23963361278c
parent 22174 f2bf6bcd4a98
child 24670 9aae962b1d56
permissions -rw-r--r--
Term.string_of_vname;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/envir.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1988  University of Cambridge
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
     5
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
     6
Environments.  The type of a term variable / sort of a type variable is
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
     7
part of its name. The lookup function must apply type substitutions,
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
     8
since they may change the identity of a variable.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    11
signature ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
sig
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    13
  type tenv
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    14
  datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    15
  val type_env: env -> Type.tyenv
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    16
  exception SAME
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    17
  val genvars: string -> env * typ list -> env * term list
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    18
  val genvar: string -> env * typ -> env * term
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    19
  val lookup: env * (indexname * typ) -> term option
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    20
  val lookup': tenv * (indexname * typ) -> term option
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    21
  val update: ((indexname * typ) * term) * env -> env
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    22
  val empty: int -> env
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    23
  val is_empty: env -> bool
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19422
diff changeset
    24
  val above: env -> int -> bool
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    25
  val vupdate: ((indexname * typ) * term) * env -> env
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    26
  val alist_of: env -> (indexname * (typ * term)) list
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    27
  val norm_term: env -> term -> term
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    28
  val norm_term_same: env -> term -> term
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    29
  val norm_type: Type.tyenv -> typ -> typ
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    30
  val norm_type_same: Type.tyenv -> typ -> typ
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    31
  val norm_types_same: Type.tyenv -> typ list -> typ list
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    32
  val beta_norm: term -> term
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
    33
  val head_norm: env -> term -> term
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
    34
  val eta_contract: term -> term
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
    35
  val beta_eta_contract: term -> term
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
    36
  val fastype: env -> typ list -> term -> typ
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    37
  val typ_subst_TVars: Type.tyenv -> typ -> typ
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    38
  val subst_TVars: Type.tyenv -> term -> term
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    39
  val subst_Vars: tenv -> term -> term
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    40
  val subst_vars: Type.tyenv * tenv -> term -> term
19422
bba26da0f227 expand_atom: Type.raw_match;
wenzelm
parents: 18937
diff changeset
    41
  val expand_atom: typ -> typ * term -> term
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
    42
  val expand_term: (term -> (typ * term) option) -> term -> term
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
    43
  val expand_term_frees: ((string * typ) * term) list -> term -> term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    46
structure Envir : ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*updating can destroy environment in 2 ways!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
   (1) variables out of range   (2) circular assignments
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
*)
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    52
type tenv = (typ * term) Vartab.table
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    53
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
datatype env = Envir of
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    55
    {maxidx: int,      (*maximum index of vars*)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    56
     asol: tenv,       (*table of assignments to Vars*)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    57
     iTs: Type.tyenv}  (*table of assignments to TVars*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
12496
0a9bd5034e05 added type_env function;
wenzelm
parents: 12231
diff changeset
    59
fun type_env (Envir {iTs, ...}) = iTs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*Generate a list of distinct variables.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  Increments index to make them distinct from ALL present variables. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  let fun genvs (_, [] : typ list) : term list = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
        | genvs (n, T::Ts) =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    67
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    68
            :: genvs(n+1,Ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
(*Generate a variable.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
fun genvar name (env,T) : env * term =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    73
  let val (env',[v]) = genvars name (env,[T])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  in  (env',v)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    76
fun var_clash ixn T T' = raise TYPE ("Variable " ^
22678
23963361278c Term.string_of_vname;
wenzelm
parents: 22174
diff changeset
    77
  quote (Term.string_of_vname ixn) ^ " has two distinct types",
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    78
  [T', T], []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    80
fun gen_lookup f asol (xname, T) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17224
diff changeset
    81
  (case Vartab.lookup asol xname of
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    82
     NONE => NONE
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    83
   | SOME (U, t) => if f (T, U) then SOME t
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    84
       else var_clash xname T U);
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    85
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    86
(* When dealing with environments produced by matching instead *)
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    87
(* of unification, there is no need to chase assigned TVars.   *)
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    88
(* In this case, we can simply ignore the type substitution    *)
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    89
(* and use = instead of eq_type.                               *)
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    90
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    91
fun lookup' (asol, p) = gen_lookup op = asol p;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    92
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    93
fun lookup2 (iTs, asol) p =
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    94
  if Vartab.is_empty iTs then lookup' (asol, p)
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
    95
  else gen_lookup (Type.eq_type iTs) asol p;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    96
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    97
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    98
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    99
fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17224
diff changeset
   100
  Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
5289
41b949f3b8ac fixed comment;
wenzelm
parents: 2191
diff changeset
   102
(*The empty environment.  New variables will start with the given index+1.*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
   103
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   105
(*Test for empty environment*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
   106
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   107
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   108
(*Determine if the least index updated exceeds lim*)
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19422
diff changeset
   109
fun above (Envir {asol, iTs, ...}) lim =
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19422
diff changeset
   110
  (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19422
diff changeset
   111
  (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   112
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   114
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   115
      Var (nT as (name', T)) =>
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   116
        if a = name' then env     (*cycle!*)
20098
19871ee094b1 removed obsolete xless;
wenzelm
parents: 19861
diff changeset
   117
        else if Term.indexname_ord (a, name') = LESS then
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   118
           (case lookup (env, nT) of  (*if already assigned, chase*)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   119
                NONE => update ((nT, Var (a, T)), env)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   120
              | SOME u => vupdate ((aU, u), env))
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   121
        else update ((aU, t), env)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   122
    | _ => update ((aU, t), env);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*Convert environment to alist*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
   126
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   129
(*** Beta normal form for terms (not eta normal form).
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   130
     Chases variables in env;  Does not exploit sharing of variable bindings
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   131
     Does not check types, so could loop. ***)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   132
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   133
(*raised when norm has no effect on a term, to do sharing instead of copying*)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   134
exception SAME;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   136
fun norm_term1 same (asol,t) : term =
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   137
  let fun norm (Var wT) =
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
   138
            (case lookup' (asol, wT) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   139
                SOME u => (norm u handle SAME => u)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   140
              | NONE   => raise SAME)
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   141
        | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   142
        | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   143
        | norm (f $ t) =
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   144
            ((case norm f of
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   145
               Abs(_,_,body) => normh(subst_bound (t, body))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   146
             | nf => nf $ (norm t handle SAME => t))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   147
            handle SAME => f $ norm t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   148
        | norm _ =  raise SAME
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   149
      and normh t = norm t handle SAME => t
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   150
  in (if same then norm else normh) t end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   152
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   153
  | normT iTs (TFree _) = raise SAME
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   154
  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   155
          SOME U => normTh iTs U
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   156
        | NONE => raise SAME)
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   157
and normTh iTs T = ((normT iTs T) handle SAME => T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   158
and normTs iTs [] = raise SAME
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   159
  | normTs iTs (T :: Ts) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   160
      ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   161
       handle SAME => T :: normTs iTs Ts);
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   162
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   163
fun norm_term2 same (asol, iTs, t) : term =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   164
  let fun norm (Const (a, T)) = Const(a, normT iTs T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   165
        | norm (Free (a, T)) = Free(a, normT iTs T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   166
        | norm (Var (w, T)) =
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   167
            (case lookup2 (iTs, asol) (w, T) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   168
                SOME u => normh u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   169
              | NONE   => Var(w, normT iTs T))
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   170
        | norm (Abs (a, T, body)) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   171
               (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   172
        | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   173
        | norm (f $ t) =
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   174
            ((case norm f of
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   175
               Abs(_, _, body) => normh (subst_bound (t, body))
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   176
             | nf => nf $ normh t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   177
            handle SAME => f $ norm t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   178
        | norm _ =  raise SAME
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   179
      and normh t = (norm t) handle SAME => t
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   180
  in (if same then norm else normh) t end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   182
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   183
  if Vartab.is_empty iTs then norm_term1 same (asol, t)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   184
  else norm_term2 same (asol, iTs, t);
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   185
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   186
val norm_term = gen_norm_term false;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   187
val norm_term_same = gen_norm_term true;
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   188
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   189
val beta_norm = norm_term (empty 0);
719
e3e1d1a6d408 Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents: 247
diff changeset
   190
12496
0a9bd5034e05 added type_env function;
wenzelm
parents: 12231
diff changeset
   191
fun norm_type iTs = normTh iTs;
0a9bd5034e05 added type_env function;
wenzelm
parents: 12231
diff changeset
   192
fun norm_type_same iTs =
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   193
  if Vartab.is_empty iTs then raise SAME else normT iTs;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   194
12496
0a9bd5034e05 added type_env function;
wenzelm
parents: 12231
diff changeset
   195
fun norm_types_same iTs =
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   196
  if Vartab.is_empty iTs then raise SAME else normTs iTs;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   197
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   198
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   199
(*Put a term into head normal form for unification.*)
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   200
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   201
fun head_norm env t =
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   202
  let
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   203
    fun hnorm (Var vT) = (case lookup (env, vT) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   204
          SOME u => head_norm env u
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   205
        | NONE => raise SAME)
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   206
      | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   207
      | hnorm (Abs (_, _, body) $ t) =
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   208
          head_norm env (subst_bound (t, body))
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   209
      | hnorm (f $ t) = (case hnorm f of
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   210
          Abs (_, _, body) => head_norm env (subst_bound (t, body))
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   211
        | nf => nf $ t)
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   212
          | hnorm _ =  raise SAME
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   213
  in hnorm t handle SAME => t end;
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   214
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   215
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   216
(*Eta-contract a term (fully)*)
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   217
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   218
local
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   219
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   220
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise SAME
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   221
  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   222
  | decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u)
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   223
  | decr _ _ = raise SAME
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   224
and decrh lev t = (decr lev t handle SAME => t);
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   225
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   226
fun eta (Abs (a, T, body)) =
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   227
    ((case eta body of
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   228
        body' as (f $ Bound 0) =>
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   229
          if loose_bvar1 (f, 0) then Abs (a, T, body')
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   230
          else decrh 0 f
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   231
     | body' => Abs (a, T, body')) handle SAME =>
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   232
        (case body of
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   233
          f $ Bound 0 =>
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   234
            if loose_bvar1 (f, 0) then raise SAME
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   235
            else decrh 0 f
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   236
        | _ => raise SAME))
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   237
  | eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u)
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   238
  | eta _ = raise SAME
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   239
and etah t = (eta t handle SAME => t);
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   240
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   241
fun has_abs (Abs _) = true
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   242
  | has_abs (t $ u) = has_abs t orelse has_abs u
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   243
  | has_abs _ = false;
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   244
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   245
in
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   246
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   247
fun eta_contract t =
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   248
  if has_abs t then etah t else t;
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   249
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   250
val beta_eta_contract = eta_contract o beta_norm;
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   251
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   252
end;
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   253
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   254
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   255
(*finds type of term without checking that combinations are consistent
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   256
  Ts holds types of bound variables*)
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   257
fun fastype (Envir {iTs, ...}) =
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   258
let val funerr = "fastype: expected function type";
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   259
    fun fast Ts (f $ u) =
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   260
        (case fast Ts f of
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   261
           Type ("fun", [_, T]) => T
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   262
         | TVar ixnS =>
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   263
                (case Type.lookup (iTs, ixnS) of
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   264
                   SOME (Type ("fun", [_, T])) => T
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   265
                 | _ => raise TERM (funerr, [f $ u]))
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   266
         | _ => raise TERM (funerr, [f $ u]))
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   267
      | fast Ts (Const (_, T)) = T
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   268
      | fast Ts (Free (_, T)) = T
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   269
      | fast Ts (Bound i) =
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   270
        (List.nth (Ts, i)
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   271
         handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   272
      | fast Ts (Var (_, T)) = T
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   273
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   274
in fast end;
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   275
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   276
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   277
(*Substitute for type Vars in a type*)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   278
fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   279
  let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   280
        | subst(T as TFree _) = T
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   281
        | subst(T as TVar ixnS) =
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   282
            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   283
  in subst T end;
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   284
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   285
(*Substitute for type Vars in a term*)
20548
8ef25fe585a8 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents: 20098
diff changeset
   286
val subst_TVars = map_types o typ_subst_TVars;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   287
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   288
(*Substitute for Vars in a term *)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   289
fun subst_Vars itms t = if Vartab.is_empty itms then t else
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   290
  let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   291
        | subst (Abs (a, T, t)) = Abs (a, T, subst t)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   292
        | subst (f $ t) = subst f $ subst t
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   293
        | subst t = t
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   294
  in subst t end;
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   295
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   296
(*Substitute for type/term Vars in a term *)
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
   297
fun subst_vars (iTs, itms) =
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   298
  if Vartab.is_empty iTs then subst_Vars itms else
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   299
  let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   300
        | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
   301
        | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   302
            NONE   => Var (ixn, typ_subst_TVars iTs T)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   303
          | SOME t => t)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   304
        | subst (b as Bound _) = b
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   305
        | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   306
        | subst (f $ t) = subst f $ subst t
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   307
  in subst end;
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   308
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   309
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   310
(* expand defined atoms -- with local beta reduction *)
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   311
19422
bba26da0f227 expand_atom: Type.raw_match;
wenzelm
parents: 18937
diff changeset
   312
fun expand_atom T (U, u) =
bba26da0f227 expand_atom: Type.raw_match;
wenzelm
parents: 18937
diff changeset
   313
  subst_TVars (Type.raw_match (U, T) Vartab.empty) u
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   314
  handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   315
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   316
fun expand_term get =
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   317
  let
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   318
    fun expand tm =
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   319
      let
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   320
        val (head, args) = Term.strip_comb tm;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   321
        val args' = map expand args;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   322
        fun comb head' = Term.list_comb (head', args');
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   323
      in
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   324
        (case head of
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   325
          Abs (x, T, t) => comb (Abs (x, T, expand t))
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   326
        | _ =>
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   327
            (case get head of
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   328
              SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   329
            | NONE => comb head)
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   330
        | _ => comb head)
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   331
      end;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   332
  in expand end;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   333
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   334
fun expand_term_frees defs =
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   335
  let
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   336
    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   337
    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   338
  in expand_term get end;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   339
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
end;