src/Pure/envir.ML
author berghofe
Fri Mar 10 14:58:25 2000 +0100 (2000-03-10)
changeset 8407 d522ad1809e9
parent 5289 41b949f3b8ac
child 10485 f1576723371f
permissions -rw-r--r--
Envir now uses Vartab instead of association lists.
wenzelm@247
     1
(*  Title:      Pure/envir.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@247
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1988  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
paulson@2142
     7
(*Environments.  They don't take account that typ is part of variable name.
paulson@2142
     8
                 Therefore we check elsewhere that  two variables with same
paulson@2142
     9
		 names and different types cannot occur.
clasohm@0
    10
*)
clasohm@0
    11
clasohm@0
    12
wenzelm@247
    13
signature ENVIR =
clasohm@0
    14
sig
berghofe@8407
    15
  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
clasohm@1460
    16
  val alist_of		: env -> (indexname * term) list
clasohm@1460
    17
  val empty		: int->env
clasohm@1460
    18
  val is_empty		: env -> bool
paulson@2142
    19
  val above		: int * env -> bool
clasohm@1460
    20
  val genvar		: string -> env * typ -> env * term
clasohm@1460
    21
  val genvars		: string -> env * typ list -> env * term list
clasohm@1460
    22
  val lookup		: env * indexname -> term option
clasohm@1460
    23
  val norm_term		: env -> term -> term
clasohm@1460
    24
  val update		: (indexname * term) * env -> env
clasohm@1460
    25
  val vupdate		: (indexname * term) * env -> env
clasohm@0
    26
end;
clasohm@0
    27
paulson@1500
    28
structure Envir : ENVIR =
clasohm@0
    29
struct
clasohm@0
    30
clasohm@0
    31
(*updating can destroy environment in 2 ways!!
clasohm@0
    32
   (1) variables out of range   (2) circular assignments
clasohm@0
    33
*)
clasohm@0
    34
datatype env = Envir of
wenzelm@247
    35
    {maxidx: int,               (*maximum index of vars*)
berghofe@8407
    36
     asol: term Vartab.table,   (*table of assignments to Vars*)
berghofe@8407
    37
     iTs: typ Vartab.table}     (*table of assignments to TVars*)
clasohm@0
    38
clasohm@0
    39
clasohm@0
    40
(*Generate a list of distinct variables.
clasohm@0
    41
  Increments index to make them distinct from ALL present variables. *)
clasohm@0
    42
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
clasohm@0
    43
  let fun genvs (_, [] : typ list) : term list = []
clasohm@0
    44
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
clasohm@0
    45
        | genvs (n, T::Ts) =
wenzelm@247
    46
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
wenzelm@247
    47
            :: genvs(n+1,Ts)
clasohm@0
    48
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
clasohm@0
    49
clasohm@0
    50
(*Generate a variable.*)
clasohm@0
    51
fun genvar name (env,T) : env * term =
wenzelm@247
    52
  let val (env',[v]) = genvars name (env,[T])
clasohm@0
    53
  in  (env',v)  end;
clasohm@0
    54
berghofe@8407
    55
fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
clasohm@0
    56
clasohm@0
    57
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
berghofe@8407
    58
  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
clasohm@0
    59
wenzelm@5289
    60
(*The empty environment.  New variables will start with the given index+1.*)
berghofe@8407
    61
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
clasohm@0
    62
paulson@2142
    63
(*Test for empty environment*)
berghofe@8407
    64
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
wenzelm@247
    65
paulson@2142
    66
(*Determine if the least index updated exceeds lim*)
berghofe@8407
    67
fun above (lim, Envir {asol, iTs, ...}) =
berghofe@8407
    68
  (case (Vartab.min_key asol, Vartab.min_key iTs) of
berghofe@8407
    69
     (None, None) => true
berghofe@8407
    70
   | (Some (_, i), None) => i > lim
berghofe@8407
    71
   | (None, Some (_, i')) => i' > lim
berghofe@8407
    72
   | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
wenzelm@247
    73
clasohm@0
    74
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
clasohm@0
    75
fun vupdate((a,t), env) = case t of
clasohm@0
    76
      Var(name',T) =>
wenzelm@247
    77
        if a=name' then env     (*cycle!*)
wenzelm@247
    78
        else if xless(a, name')  then
wenzelm@247
    79
           (case lookup(env,name') of  (*if already assigned, chase*)
wenzelm@247
    80
                None => update((name', Var(a,T)), env)
wenzelm@247
    81
              | Some u => vupdate((a,u), env))
wenzelm@247
    82
        else update((a,t), env)
clasohm@0
    83
    | _ => update((a,t), env);
clasohm@0
    84
clasohm@0
    85
clasohm@0
    86
(*Convert environment to alist*)
berghofe@8407
    87
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
clasohm@0
    88
clasohm@0
    89
paulson@1500
    90
(*** Beta normal form for terms (not eta normal form).
paulson@1500
    91
     Chases variables in env;  Does not exploit sharing of variable bindings
paulson@1500
    92
     Does not check types, so could loop. ***)
paulson@1500
    93
paulson@1500
    94
(*raised when norm has no effect on a term, to do sharing instead of copying*)
paulson@1500
    95
exception SAME;
clasohm@0
    96
paulson@1500
    97
fun norm_term1 (asol,t) : term =
paulson@1500
    98
  let fun norm (Var (w,T)) =
berghofe@8407
    99
	    (case Vartab.lookup (asol, w) of
paulson@2191
   100
		Some u => (norm u handle SAME => u)
paulson@1500
   101
	      | None   => raise SAME)
paulson@1500
   102
	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
paulson@2191
   103
	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
paulson@1500
   104
	| norm (f $ t) =
paulson@1500
   105
	    ((case norm f of
paulson@2191
   106
	       Abs(_,_,body) => normh(subst_bound (t, body))
paulson@2191
   107
	     | nf => nf $ (norm t handle SAME => t))
paulson@1500
   108
	    handle SAME => f $ norm t)
paulson@1500
   109
	| norm _ =  raise SAME
paulson@2191
   110
      and normh t = norm t handle SAME => t
paulson@1500
   111
  in normh t end
clasohm@0
   112
paulson@1500
   113
and norm_term2(asol,iTs,t) : term =
paulson@1500
   114
  let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
paulson@1500
   115
	| normT(TFree _) = raise SAME
berghofe@8407
   116
	| normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
paulson@1500
   117
		Some(U) => normTh U
paulson@1500
   118
	      | None => raise SAME)
paulson@1500
   119
      and normTh T = ((normT T) handle SAME => T)
paulson@1500
   120
      and normTs([]) = raise SAME
paulson@2181
   121
	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
paulson@1500
   122
			   handle SAME => T :: normTs Ts)
paulson@1500
   123
      and norm(Const(a,T)) = Const(a, normT T)
paulson@1500
   124
	| norm(Free(a,T)) = Free(a, normT T)
paulson@1500
   125
	| norm(Var (w,T)) =
berghofe@8407
   126
	    (case Vartab.lookup (asol, w) of
paulson@1500
   127
		Some u => normh u
paulson@1500
   128
	      | None   => Var(w,normT T))
paulson@1500
   129
	| norm(Abs(a,T,body)) =
paulson@1500
   130
	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
paulson@2191
   131
	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
paulson@1500
   132
	| norm(f $ t) =
paulson@1500
   133
	    ((case norm f of
paulson@2191
   134
	       Abs(_,_,body) => normh(subst_bound (t, body))
paulson@1500
   135
	     | nf => nf $ normh t)
paulson@1500
   136
	    handle SAME => f $ norm t)
paulson@1500
   137
	| norm _ =  raise SAME
paulson@1500
   138
      and normh t = (norm t) handle SAME => t
paulson@1500
   139
  in normh t end;
clasohm@0
   140
clasohm@0
   141
(*curried version might be slower in recursive calls*)
clasohm@0
   142
fun norm_term (env as Envir{asol,iTs,...}) t : term =
berghofe@8407
   143
        if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
lcp@719
   144
clasohm@0
   145
end;
clasohm@0
   146