src/Pure/envir.ML
author blanchet
Wed, 03 Nov 2010 22:33:23 +0100
changeset 40342 3154f63e2bda
parent 35408 b48ab741683b
child 42083 e1209fc7ecdc
permissions -rw-r--r--
don't be overly verbose in Sledgehammer's minimizer
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
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
     3
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
     4
Free-form environments.  The type of a term variable / sort of a type variable is
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
     5
part of its name.  The lookup function must apply type substitutions,
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
     6
since they may change the identity of a variable.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
     9
signature ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
sig
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    11
  type tenv = (typ * term) Vartab.table
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    12
  datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    13
  val maxidx_of: env -> int
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    14
  val term_env: env -> tenv
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    15
  val type_env: env -> Type.tyenv
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    16
  val is_empty: env -> bool
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    17
  val empty: int -> env
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    18
  val merge: env * env -> env
26638
1d5d42d8fd66 added insert_sorts (from thm.ML);
wenzelm
parents: 26328
diff changeset
    19
  val insert_sorts: env -> sort list -> sort list
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    20
  val genvars: string -> env * typ list -> env * term list
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    21
  val genvar: string -> env * typ -> env * term
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    22
  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
    23
  val lookup': tenv * (indexname * typ) -> term option
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    24
  val update: ((indexname * typ) * term) * env -> env
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19422
diff changeset
    25
  val above: env -> int -> bool
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    26
  val vupdate: ((indexname * typ) * term) * env -> env
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    27
  val norm_type_same: Type.tyenv -> typ Same.operation
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    28
  val norm_types_same: Type.tyenv -> typ list Same.operation
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    29
  val norm_type: Type.tyenv -> typ -> typ
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    30
  val norm_term_same: env -> term Same.operation
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    31
  val norm_term: env -> term -> term
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
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    37
  val subst_type_same: Type.tyenv -> typ Same.operation
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    38
  val subst_term_types_same: Type.tyenv -> term Same.operation
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    39
  val subst_term_same: Type.tyenv * tenv -> term Same.operation
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    40
  val subst_type: Type.tyenv -> typ -> typ
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    41
  val subst_term_types: Type.tyenv -> term -> term
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
    42
  val subst_term: Type.tyenv * tenv -> term -> term
19422
bba26da0f227 expand_atom: Type.raw_match;
wenzelm
parents: 18937
diff changeset
    43
  val expand_atom: typ -> typ * term -> term
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
    44
  val expand_term: (term -> (typ * term) option) -> term -> term
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
    45
  val expand_term_frees: ((string * typ) * term) list -> term -> term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    48
structure Envir: ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    51
(** datatype env **)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    52
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    53
(*Updating can destroy environment in 2 ways!
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    54
   (1) variables out of range
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    55
   (2) circular assignments
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
*)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    57
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    58
type tenv = (typ * term) Vartab.table;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
    59
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
datatype env = Envir of
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    61
 {maxidx: int,          (*upper bound of maximum index of vars*)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    62
  tenv: tenv,           (*assignments to Vars*)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    63
  tyenv: Type.tyenv};   (*assignments to TVars*)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    64
32796
2e4485b9a39f eliminated dead code;
wenzelm
parents: 32648
diff changeset
    65
fun make_env (maxidx, tenv, tyenv) =
2e4485b9a39f eliminated dead code;
wenzelm
parents: 32648
diff changeset
    66
  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    67
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    68
fun maxidx_of (Envir {maxidx, ...}) = maxidx;
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    69
fun term_env (Envir {tenv, ...}) = tenv;
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    70
fun type_env (Envir {tyenv, ...}) = tyenv;
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    71
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    72
fun is_empty env =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    73
  Vartab.is_empty (term_env env) andalso
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    74
  Vartab.is_empty (type_env env);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    76
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    77
(* build env *)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    78
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    79
fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    81
fun merge
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    82
   (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    83
    Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    84
  make_env (Int.max (maxidx1, maxidx2),
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    85
    Vartab.merge (op =) (tenv1, tenv2),
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    86
    Vartab.merge (op =) (tyenv1, tyenv2));
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    87
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    88
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    89
(*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
26638
1d5d42d8fd66 added insert_sorts (from thm.ML);
wenzelm
parents: 26328
diff changeset
    90
val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
1d5d42d8fd66 added insert_sorts (from thm.ML);
wenzelm
parents: 26328
diff changeset
    91
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(*Generate a list of distinct variables.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
  Increments index to make them distinct from ALL present variables. *)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
    94
fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    95
  let
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    96
    fun genvs (_, [] : typ list) : term list = []
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    97
      | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    98
      | genvs (n, T :: Ts) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
    99
          Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   100
            :: genvs (n + 1, Ts);
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   101
  in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
(*Generate a variable.*)
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   104
fun genvar name (env, T) : env * term =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   105
  let val (env', [v]) = genvars name (env, [T])
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   106
  in (env', v) end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   108
fun var_clash xi T T' =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   109
  raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   110
    [T', T], []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   112
fun lookup_check check tenv (xi, T) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   113
  (case Vartab.lookup tenv xi of
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   114
    NONE => NONE
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   115
  | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   116
16652
4ecf94235ec7 Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents: 15797
diff changeset
   117
(* 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
   118
(* 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
   119
(* 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
   120
(* and use = instead of eq_type.                               *)
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   121
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   122
fun lookup' (tenv, p) = lookup_check (op =) tenv p;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   123
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   124
fun lookup2 (tyenv, tenv) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   125
  lookup_check (Type.eq_type tyenv) tenv;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   126
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   127
fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   129
fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   130
  Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   131
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   132
(*Determine if the least index updated exceeds lim*)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   133
fun above (Envir {tenv, tyenv, ...}) lim =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   134
  (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   135
  (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   136
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   138
fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   139
  (case t of
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   140
    Var (nT as (name', T)) =>
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   141
      if a = name' then env     (*cycle!*)
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 32796
diff changeset
   142
      else if Term_Ord.indexname_ord (a, name') = LESS then
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   143
        (case lookup (env, nT) of  (*if already assigned, chase*)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   144
          NONE => update ((nT, Var (a, T)), env)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   145
        | SOME u => vupdate ((aU, u), env))
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   146
      else update ((aU, t), env)
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   147
  | _ => update ((aU, t), env));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   151
(** beta normalization wrt. environment **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   153
(*Chases variables in env.  Does not exploit sharing of variable bindings
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   154
  Does not check types, so could loop.*)
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   155
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   156
local
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   157
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   158
fun norm_type0 tyenv : typ Same.operation =
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   159
  let
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   160
    fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   161
      | norm (TFree _) = raise Same.SAME
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   162
      | norm (TVar v) =
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   163
          (case Type.lookup tyenv v of
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   164
            SOME U => Same.commit norm U
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   165
          | NONE => raise Same.SAME);
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   166
  in norm end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   168
fun norm_term1 tenv : term Same.operation =
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   169
  let
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   170
    fun norm (Var v) =
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   171
          (case lookup' (tenv, v) of
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   172
            SOME u => Same.commit norm u
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   173
          | NONE => raise Same.SAME)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   174
      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   175
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   176
      | norm (f $ t) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   177
          ((case norm f of
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   178
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   179
           | nf => nf $ Same.commit norm t)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   180
          handle Same.SAME => f $ norm t)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   181
      | norm _ = raise Same.SAME;
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   182
  in norm end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   184
fun norm_term2 tenv tyenv : term Same.operation =
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   185
  let
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   186
    val normT = norm_type0 tyenv;
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   187
    fun norm (Const (a, T)) = Const (a, normT T)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   188
      | norm (Free (a, T)) = Free (a, normT T)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   189
      | norm (Var (xi, T)) =
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   190
          (case lookup2 (tyenv, tenv) (xi, T) of
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   191
            SOME u => Same.commit norm u
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   192
          | NONE => Var (xi, normT T))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   193
      | norm (Abs (a, T, body)) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   194
          (Abs (a, normT T, Same.commit norm body)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   195
            handle Same.SAME => Abs (a, T, norm body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   196
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   197
      | norm (f $ t) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   198
          ((case norm f of
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   199
             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   200
           | nf => nf $ Same.commit norm t)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   201
          handle Same.SAME => f $ norm t)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   202
      | norm _ = raise Same.SAME;
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   203
  in norm end;
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   204
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   205
in
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   206
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   207
fun norm_type_same tyenv T =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   208
  if Vartab.is_empty tyenv then raise Same.SAME
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   209
  else norm_type0 tyenv T;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   211
fun norm_types_same tyenv Ts =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   212
  if Vartab.is_empty tyenv then raise Same.SAME
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   213
  else Same.map (norm_type0 tyenv) Ts;
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   214
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   215
fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   216
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   217
fun norm_term_same (Envir {tenv, tyenv, ...}) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   218
  if Vartab.is_empty tyenv then norm_term1 tenv
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   219
  else norm_term2 tenv tyenv;
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   220
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   221
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
25471
ca009b7ce693 Optimized beta_norm: only tries to normalize term when it contains
berghofe
parents: 24670
diff changeset
   222
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
719
e3e1d1a6d408 Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents: 247
diff changeset
   223
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   224
end;
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   225
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   226
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   227
(*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
   228
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   229
fun head_norm env =
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   230
  let
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   231
    fun norm (Var v) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   232
        (case lookup (env, v) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12496
diff changeset
   233
          SOME u => head_norm env u
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   234
        | NONE => raise Same.SAME)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   235
      | norm (Abs (a, T, body)) = Abs (a, T, norm body)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   236
      | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   237
      | norm (f $ t) =
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   238
          (case norm f of
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   239
            Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   240
          | nf => nf $ t)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   241
      | norm _ = raise Same.SAME;
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   242
  in Same.commit norm end;
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   243
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   244
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   245
(*Eta-contract a term (fully)*)
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   246
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   247
local
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   248
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   249
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   250
  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   251
  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   252
  | decr _ _ = raise Same.SAME
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   253
and decrh lev t = (decr lev t handle Same.SAME => t);
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   254
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   255
fun eta (Abs (a, T, body)) =
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   256
    ((case eta body of
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   257
        body' as (f $ Bound 0) =>
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   258
          if loose_bvar1 (f, 0) then Abs (a, T, body')
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   259
          else decrh 0 f
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   260
     | body' => Abs (a, T, body')) handle Same.SAME =>
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   261
        (case body of
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   262
          f $ Bound 0 =>
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   263
            if loose_bvar1 (f, 0) then raise Same.SAME
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   264
            else decrh 0 f
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   265
        | _ => raise Same.SAME))
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   266
  | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   267
  | eta _ = raise Same.SAME;
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   268
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   269
in
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   270
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   271
fun eta_contract t =
32018
3370cea95387 use structure Same;
wenzelm
parents: 30146
diff changeset
   272
  if Term.has_abs t then Same.commit eta t else t;
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   273
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   274
val beta_eta_contract = eta_contract o beta_norm;
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   275
22174
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   276
end;
f2bf6bcd4a98 tuned eta_contract;
wenzelm
parents: 21795
diff changeset
   277
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   278
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   279
(*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
   280
  Ts holds types of bound variables*)
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   281
fun fastype (Envir {tyenv, ...}) =
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   282
  let
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   283
    val funerr = "fastype: expected function type";
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   284
    fun fast Ts (f $ u) =
32648
143e0b0a6b33 Correct chasing of type variable instantiations during type unification.
paulson
parents: 32034
diff changeset
   285
          (case Type.devar tyenv (fast Ts f) of
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   286
            Type ("fun", [_, T]) => T
32648
143e0b0a6b33 Correct chasing of type variable instantiations during type unification.
paulson
parents: 32034
diff changeset
   287
          | TVar v => raise TERM (funerr, [f $ u])
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   288
          | _ => raise TERM (funerr, [f $ u]))
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   289
      | fast Ts (Const (_, T)) = T
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   290
      | fast Ts (Free (_, T)) = T
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   291
      | fast Ts (Bound i) =
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   292
          (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
20670
115262dd18e2 tuned eta_contract;
wenzelm
parents: 20548
diff changeset
   293
      | fast Ts (Var (_, T)) = T
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   294
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   295
  in fast end;
12231
4a25f04bea61 Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents: 11513
diff changeset
   296
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   297
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   298
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   299
(** plain substitution -- without variable chasing **)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   300
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   301
local
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   302
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   303
fun subst_type0 tyenv = Term_Subst.map_atypsT_same
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   304
  (fn TVar v =>
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   305
        (case Type.lookup tyenv v of
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   306
          SOME U => U
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   307
        | NONE => raise Same.SAME)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   308
    | _ => raise Same.SAME);
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   309
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   310
fun subst_term1 tenv = Term_Subst.map_aterms_same
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   311
  (fn Var v =>
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   312
        (case lookup' (tenv, v) of
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   313
          SOME u => u
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   314
        | NONE => raise Same.SAME)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   315
    | _ => raise Same.SAME);
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   316
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   317
fun subst_term2 tenv tyenv : term Same.operation =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   318
  let
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   319
    val substT = subst_type0 tyenv;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   320
    fun subst (Const (a, T)) = Const (a, substT T)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   321
      | subst (Free (a, T)) = Free (a, substT T)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   322
      | subst (Var (xi, T)) =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   323
          (case lookup' (tenv, (xi, T)) of
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   324
            SOME u => u
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   325
          | NONE => Var (xi, substT T))
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   326
      | subst (Bound _) = raise Same.SAME
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   327
      | subst (Abs (a, T, t)) =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   328
          (Abs (a, substT T, Same.commit subst t)
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   329
            handle Same.SAME => Abs (a, T, subst t))
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   330
      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   331
  in subst end;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   332
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   333
in
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   334
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   335
fun subst_type_same tyenv T =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   336
  if Vartab.is_empty tyenv then raise Same.SAME
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   337
  else subst_type0 tyenv T;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   338
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   339
fun subst_term_types_same tyenv t =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   340
  if Vartab.is_empty tyenv then raise Same.SAME
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   341
  else Term_Subst.map_types_same (subst_type0 tyenv) t;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   342
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   343
fun subst_term_same (tyenv, tenv) =
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   344
  if Vartab.is_empty tenv then subst_term_types_same tyenv
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   345
  else if Vartab.is_empty tyenv then subst_term1 tenv
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   346
  else subst_term2 tenv tyenv;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   347
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   348
fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   349
fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   350
fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   351
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   352
end;
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15570
diff changeset
   353
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   354
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   355
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   356
(** expand defined atoms -- with local beta reduction **)
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   357
19422
bba26da0f227 expand_atom: Type.raw_match;
wenzelm
parents: 18937
diff changeset
   358
fun expand_atom T (U, u) =
32034
70c0bcd0adfb tuned/modernized subst: Same.operation;
wenzelm
parents: 32031
diff changeset
   359
  subst_term_types (Type.raw_match (U, T) Vartab.empty) u
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   360
    handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
18937
0eb35519f0f3 added (beta_)eta_contract (from pattern.ML);
wenzelm
parents: 17412
diff changeset
   361
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   362
fun expand_term get =
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   363
  let
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   364
    fun expand tm =
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   365
      let
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   366
        val (head, args) = Term.strip_comb tm;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   367
        val args' = map expand args;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   368
        fun comb head' = Term.list_comb (head', args');
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   369
      in
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   370
        (case head of
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   371
          Abs (x, T, t) => comb (Abs (x, T, expand t))
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   372
        | _ =>
32031
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   373
          (case get head of
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   374
            SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
e2e6b0691264 major cleanup, simplification, modernization;
wenzelm
parents: 32018
diff changeset
   375
          | NONE => comb head))
21695
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   376
      end;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   377
  in expand end;
6c07cc87fe2b added expand_term;
wenzelm
parents: 20670
diff changeset
   378
21795
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   379
fun expand_term_frees defs =
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   380
  let
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   381
    val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   382
    val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   383
  in expand_term get end;
d7dcc3dfa7e9 added expand_term_frees;
wenzelm
parents: 21695
diff changeset
   384
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
end;