src/Pure/envir.ML
author berghofe
Fri, 31 Aug 2001 16:08:45 +0200
changeset 11513 2f6fe5b01521
parent 10485 f1576723371f
child 12231 4a25f04bea61
permissions -rw-r--r--
- exported SAME exception - exported functions for normalizing types
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
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
     6
Environments.  They don't take account that typ is part of variable
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
     7
name.  Therefore we check elsewhere that two variables with same names
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
     8
and different types cannot occur.
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
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    13
  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    14
  exception SAME
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    15
  val genvars: string -> env * typ list -> env * term list
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    16
  val genvar: string -> env * typ -> env * term
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    17
  val lookup: env * indexname -> term option
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    18
  val update: (indexname * term) * env -> env
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    19
  val empty: int -> env
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    20
  val is_empty: env -> bool
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    21
  val above: int * env -> bool
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    22
  val vupdate: (indexname * term) * env -> env
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    23
  val alist_of: env -> (indexname * term) list
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    24
  val norm_term: env -> term -> term
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    25
  val norm_term_same: env -> term -> term
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    26
  val norm_type: env -> typ -> typ
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    27
  val norm_type_same: env -> typ -> typ
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
    28
  val norm_types_same: env -> typ list -> typ list
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
    29
  val beta_norm: term -> term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    32
structure Envir : ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(*updating can destroy environment in 2 ways!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
   (1) variables out of range   (2) circular assignments
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
datatype env = Envir of
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    39
    {maxidx: int,               (*maximum index of vars*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    40
     asol: term Vartab.table,   (*table of assignments to Vars*)
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    41
     iTs: typ Vartab.table}     (*table of assignments to TVars*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
(*Generate a list of distinct variables.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  Increments index to make them distinct from ALL present variables. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  let fun genvs (_, [] : typ list) : term list = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
        | genvs (n, T::Ts) =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    50
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    51
            :: genvs(n+1,Ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*Generate a variable.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
fun genvar name (env,T) : env * term =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    56
  let val (env',[v]) = genvars name (env,[T])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  in  (env',v)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    59
fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    62
  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
5289
41b949f3b8ac fixed comment;
wenzelm
parents: 2191
diff changeset
    64
(*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
    65
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    67
(*Test for empty environment*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    68
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
    69
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    70
(*Determine if the least index updated exceeds lim*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    71
fun above (lim, Envir {asol, iTs, ...}) =
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    72
  (case (Vartab.min_key asol, Vartab.min_key iTs) of
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    73
     (None, None) => true
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    74
   | (Some (_, i), None) => i > lim
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    75
   | (None, Some (_, i')) => i' > lim
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    76
   | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    77
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
fun vupdate((a,t), env) = case t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
      Var(name',T) =>
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    81
        if a=name' then env     (*cycle!*)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    82
        else if xless(a, name')  then
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    83
           (case lookup(env,name') of  (*if already assigned, chase*)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    84
                None => update((name', Var(a,T)), env)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    85
              | Some u => vupdate((a,u), env))
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    86
        else update((a,t), env)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
    | _ => update((a,t), env);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(*Convert environment to alist*)
8407
d522ad1809e9 Envir now uses Vartab instead of association lists.
berghofe
parents: 5289
diff changeset
    91
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    94
(*** Beta normal form for terms (not eta normal form).
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    95
     Chases variables in env;  Does not exploit sharing of variable bindings
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    96
     Does not check types, so could loop. ***)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    97
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    98
(*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
    99
exception SAME;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   101
fun norm_term1 same (asol,t) : term =
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   102
  let fun norm (Var (w,T)) =
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   103
            (case Vartab.lookup (asol, w) of
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   104
                Some u => (norm u handle SAME => u)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   105
              | None   => raise SAME)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   106
        | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   107
        | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   108
        | norm (f $ t) =
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   109
            ((case norm f of
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   110
               Abs(_,_,body) => normh(subst_bound (t, body))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   111
             | nf => nf $ (norm t handle SAME => t))
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   112
            handle SAME => f $ norm t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   113
        | norm _ =  raise SAME
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   114
      and normh t = norm t handle SAME => t
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   115
  in (if same then norm else normh) t end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   117
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   118
  | normT iTs (TFree _) = raise SAME
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   119
  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   120
          Some U => normTh iTs U
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   121
        | None => raise SAME)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   122
and normTh iTs T = ((normT iTs T) handle SAME => T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   123
and normTs iTs [] = raise SAME
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   124
  | normTs iTs (T :: Ts) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   125
      ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   126
       handle SAME => T :: normTs iTs Ts);
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   127
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   128
fun norm_term2 same (asol, iTs, t) : term =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   129
  let fun norm (Const (a, T)) = Const(a, normT iTs T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   130
        | norm (Free (a, T)) = Free(a, normT iTs T)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   131
        | norm (Var (w, T)) =
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   132
            (case Vartab.lookup (asol, w) of
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   133
                Some u => normh u
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   134
              | None   => Var(w, normT iTs T))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   135
        | norm (Abs (a, T, body)) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   136
               (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   137
        | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   138
        | norm (f $ t) =
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   139
            ((case norm f of
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   140
               Abs(_, _, body) => normh (subst_bound (t, body))
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   141
             | nf => nf $ normh t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   142
            handle SAME => f $ norm t)
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   143
        | norm _ =  raise SAME
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   144
      and normh t = (norm t) handle SAME => t
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   145
  in (if same then norm else normh) t end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   147
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   148
  if Vartab.is_empty iTs then norm_term1 same (asol, t)
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   149
  else norm_term2 same (asol, iTs, t);
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   150
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   151
val norm_term = gen_norm_term false;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   152
val norm_term_same = gen_norm_term true;
10485
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   153
f1576723371f added beta_norm;
wenzelm
parents: 8407
diff changeset
   154
val beta_norm = norm_term (empty 0);
719
e3e1d1a6d408 Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents: 247
diff changeset
   155
11513
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   156
fun norm_type (Envir {iTs, ...}) = normTh iTs;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   157
fun norm_type_same (Envir {iTs, ...}) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   158
  if Vartab.is_empty iTs then raise SAME else normT iTs;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   159
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   160
fun norm_types_same (Envir {iTs, ...}) =
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   161
  if Vartab.is_empty iTs then raise SAME else normTs iTs;
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   162
2f6fe5b01521 - exported SAME exception
berghofe
parents: 10485
diff changeset
   163
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
end;