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