src/Pure/envir.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 5289 41b949f3b8ac
child 8407 d522ad1809e9
permissions -rw-r--r--
Object logic specific operations.
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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
     7
(*Environments.  They don't take account that typ is part of variable name.
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
     8
                 Therefore we check elsewhere that  two variables with same
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
     9
		 names and different types cannot occur.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    13
signature ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  type 'a xolist
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  exception ENVIR of string * indexname;
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    17
  datatype env = Envir of {asol: term xolist, iTs: typ xolist, maxidx: int}
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    18
  val alist_of		: env -> (indexname * term) list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    19
  val alist_of_olist	: 'a xolist -> (indexname * 'a) list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    20
  val empty		: int->env
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    21
  val is_empty		: env -> bool
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    22
  val above		: int * env -> bool
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    23
  val genvar		: string -> env * typ -> env * term
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    24
  val genvars		: string -> env * typ list -> env * term list
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    25
  val lookup		: env * indexname -> term option
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    26
  val norm_term		: env -> term -> term
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    27
  val null_olist	: 'a xolist
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    28
  val olist_of_alist	: (indexname * 'a) list -> 'a xolist
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    29
  val update		: (indexname * term) * env -> env
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    30
  val vupdate		: (indexname * term) * env -> env
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    33
structure Envir : ENVIR =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
(*association lists with keys in ascending order, no repeated keys*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    37
type 'a xolist = (indexname * 'a) list;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
exception ENVIR of string * indexname;
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    41
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    42
(*look up key in ordered list*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    43
fun xsearch ([], key) = None
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    44
  | xsearch (((keyi,xi)::pairs), key) =
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    45
      if xless(keyi,key) then xsearch (pairs, key)
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    46
      else if key=keyi then Some xi
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
      else None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*insert pair in ordered list, reject if key already present*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    50
fun xinsert_new (newpr as (key, x), al) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  let fun insert [] = [newpr]
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    52
        | insert ((pair as (keyi,xi)) :: pairs) =
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    53
            if xless(keyi,key) then pair :: insert pairs
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    54
            else if key=keyi then
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    55
                raise ENVIR("xinsert_new: already present",key)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    56
            else newpr::pair::pairs
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    57
  in  (insert al)  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(*insert pair in ordered list, overwrite if key already present*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    60
fun xinsert (newpr as (key, x), al) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  let fun insert [] = [newpr]
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    62
        | insert ((pair as (keyi,xi)) :: pairs) =
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    63
            if xless(keyi,key) then pair :: insert pairs
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    64
            else if key=keyi then newpr::pairs
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    65
            else newpr::pair::pairs
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    66
  in  (insert al)  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    68
(*apply function to the contents part of each pair*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    69
fun xmap f (pairs) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  let fun xmp [] = []
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    71
        | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    72
  in (xmp pairs)  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
(*allows redefinition of a key by "join"ing the contents parts*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    75
fun xmerge_olists join (pairsa, pairsb) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  let fun xmrg ([],pairsb) = pairsb
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    77
        | xmrg (pairsa,[]) = pairsa
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    78
        | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    79
            if xless(keya,keyb) then
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    80
                (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    81
            else if xless(keyb,keya) then
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    82
                (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    83
            else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    84
  in  (xmrg (pairsa,pairsb))  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    86
val null_olist = [];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    88
fun alist_of_olist (pairs) = pairs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
    90
fun olist_of_alist pairs = foldr xinsert (pairs, []);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
(*updating can destroy environment in 2 ways!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
   (1) variables out of range   (2) circular assignments
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
datatype env = Envir of
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    98
    {maxidx: int,               (*maximum index of vars*)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
    99
     asol: term xolist,         (*table of assignments to Vars*)
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   100
     iTs:  typ  xolist}         (*table of assignments to TVars*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
(*Generate a list of distinct variables.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
  Increments index to make them distinct from ALL present variables. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  let fun genvs (_, [] : typ list) : term list = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
        | genvs (n, T::Ts) =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   109
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   110
            :: genvs(n+1,Ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
(*Generate a variable.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
fun genvar name (env,T) : env * term =
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   115
  let val (env',[v]) = genvars name (env,[T])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  in  (env',v)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
  Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
5289
41b949f3b8ac fixed comment;
wenzelm
parents: 2191
diff changeset
   123
(*The empty environment.  New variables will start with the given index+1.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   126
(*Test for empty environment*)
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   127
fun is_empty (Envir {asol = [], iTs = [], ...}) = true
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   128
  | is_empty _ = false;
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   129
2142
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   130
(*Determine if the least index updated exceeds lim*)
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   131
fun above (lim, Envir {asol, iTs, ...}) = 
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   132
    let fun upd [] = true
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   133
	  | upd (i::is) = i>lim andalso upd is
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   134
    in  upd (map (#2 o #1) asol @ (map (#2 o #1) iTs))
20f208ff085d Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents: 1500
diff changeset
   135
    end;
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*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
fun vupdate((a,t), env) = case t of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
      Var(name',T) =>
247
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   140
        if a=name' then env     (*cycle!*)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   141
        else if xless(a, name')  then
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   142
           (case lookup(env,name') of  (*if already assigned, chase*)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   143
                None => update((name', Var(a,T)), env)
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   144
              | Some u => vupdate((a,u), env))
bc10568855ee added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents: 0
diff changeset
   145
        else update((a,t), env)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
    | _ => update((a,t), env);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*Convert environment to alist*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   153
(*** Beta normal form for terms (not eta normal form).
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   154
     Chases variables in env;  Does not exploit sharing of variable bindings
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   155
     Does not check types, so could loop. ***)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   156
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   157
(*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
   158
exception SAME;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   160
fun norm_term1 (asol,t) : term =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   161
  let fun norm (Var (w,T)) =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   162
	    (case xsearch(asol,w) of
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   163
		Some u => (norm u handle SAME => u)
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   164
	      | None   => raise SAME)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   165
	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   166
	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   167
	| norm (f $ t) =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   168
	    ((case norm f of
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   169
	       Abs(_,_,body) => normh(subst_bound (t, body))
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   170
	     | nf => nf $ (norm t handle SAME => t))
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   171
	    handle SAME => f $ norm t)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   172
	| norm _ =  raise SAME
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   173
      and normh t = norm t handle SAME => t
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   174
  in normh t end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   176
and norm_term2(asol,iTs,t) : term =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   177
  let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   178
	| normT(TFree _) = raise SAME
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   179
	| normT(TVar(v,_)) = (case assoc(iTs,v) of
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   180
		Some(U) => normTh U
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   181
	      | None => raise SAME)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   182
      and normTh T = ((normT T) handle SAME => T)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   183
      and normTs([]) = raise SAME
2181
9c2b4728641d In-lined the one function call to normTsh
paulson
parents: 2142
diff changeset
   184
	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   185
			   handle SAME => T :: normTs Ts)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   186
      and norm(Const(a,T)) = Const(a, normT T)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   187
	| norm(Free(a,T)) = Free(a, normT T)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   188
	| norm(Var (w,T)) =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   189
	    (case xsearch(asol,w) of
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   190
		Some u => normh u
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   191
	      | None   => Var(w,normT T))
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   192
	| norm(Abs(a,T,body)) =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   193
	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   194
	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   195
	| norm(f $ t) =
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   196
	    ((case norm f of
2191
58383908f177 Speedups involving norm
paulson
parents: 2181
diff changeset
   197
	       Abs(_,_,body) => normh(subst_bound (t, body))
1500
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   198
	     | nf => nf $ normh t)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   199
	    handle SAME => f $ norm t)
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   200
	| norm _ =  raise SAME
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   201
      and normh t = (norm t) handle SAME => t
b2de3b3277b8 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   202
  in normh t end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
(*curried version might be slower in recursive calls*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
fun norm_term (env as Envir{asol,iTs,...}) t : term =
719
e3e1d1a6d408 Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents: 247
diff changeset
   206
        if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
e3e1d1a6d408 Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents: 247
diff changeset
   207
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209