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