src/Pure/envir.ML
author skalberg
Sun Feb 13 17:15:14 2005 +0100 (2005-02-13)
changeset 15531 08c8dad8e399
parent 12496 0a9bd5034e05
child 15570 8d8c70b41bab
permissions -rw-r--r--
Deleted Library.option type.
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@12496
    14
  val type_env: env -> typ Vartab.table
berghofe@11513
    15
  exception SAME
wenzelm@10485
    16
  val genvars: string -> env * typ list -> env * term list
wenzelm@10485
    17
  val genvar: string -> env * typ -> env * term
wenzelm@10485
    18
  val lookup: env * indexname -> term option
wenzelm@10485
    19
  val update: (indexname * term) * env -> env
wenzelm@10485
    20
  val empty: int -> env
wenzelm@10485
    21
  val is_empty: env -> bool
wenzelm@10485
    22
  val above: int * env -> bool
wenzelm@10485
    23
  val vupdate: (indexname * term) * env -> env
wenzelm@10485
    24
  val alist_of: env -> (indexname * term) list
wenzelm@10485
    25
  val norm_term: env -> term -> term
berghofe@11513
    26
  val norm_term_same: env -> term -> term
wenzelm@12496
    27
  val norm_type: typ Vartab.table -> typ -> typ
wenzelm@12496
    28
  val norm_type_same: typ Vartab.table -> typ -> typ
wenzelm@12496
    29
  val norm_types_same: typ Vartab.table -> typ list -> typ list
wenzelm@10485
    30
  val beta_norm: term -> term
berghofe@12231
    31
  val head_norm: env -> term -> term
berghofe@12231
    32
  val fastype: env -> typ list -> term -> typ
clasohm@0
    33
end;
clasohm@0
    34
paulson@1500
    35
structure Envir : ENVIR =
clasohm@0
    36
struct
clasohm@0
    37
clasohm@0
    38
(*updating can destroy environment in 2 ways!!
clasohm@0
    39
   (1) variables out of range   (2) circular assignments
clasohm@0
    40
*)
clasohm@0
    41
datatype env = Envir of
wenzelm@247
    42
    {maxidx: int,               (*maximum index of vars*)
berghofe@8407
    43
     asol: term Vartab.table,   (*table of assignments to Vars*)
berghofe@8407
    44
     iTs: typ Vartab.table}     (*table of assignments to TVars*)
clasohm@0
    45
wenzelm@12496
    46
fun type_env (Envir {iTs, ...}) = iTs;
clasohm@0
    47
clasohm@0
    48
(*Generate a list of distinct variables.
clasohm@0
    49
  Increments index to make them distinct from ALL present variables. *)
clasohm@0
    50
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
clasohm@0
    51
  let fun genvs (_, [] : typ list) : term list = []
clasohm@0
    52
        | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
clasohm@0
    53
        | genvs (n, T::Ts) =
wenzelm@247
    54
            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
wenzelm@247
    55
            :: genvs(n+1,Ts)
clasohm@0
    56
  in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
clasohm@0
    57
clasohm@0
    58
(*Generate a variable.*)
clasohm@0
    59
fun genvar name (env,T) : env * term =
wenzelm@247
    60
  let val (env',[v]) = genvars name (env,[T])
clasohm@0
    61
  in  (env',v)  end;
clasohm@0
    62
berghofe@8407
    63
fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
clasohm@0
    64
clasohm@0
    65
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
berghofe@8407
    66
  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
clasohm@0
    67
wenzelm@5289
    68
(*The empty environment.  New variables will start with the given index+1.*)
berghofe@8407
    69
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
clasohm@0
    70
paulson@2142
    71
(*Test for empty environment*)
berghofe@8407
    72
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
wenzelm@247
    73
paulson@2142
    74
(*Determine if the least index updated exceeds lim*)
berghofe@8407
    75
fun above (lim, Envir {asol, iTs, ...}) =
berghofe@8407
    76
  (case (Vartab.min_key asol, Vartab.min_key iTs) of
skalberg@15531
    77
     (NONE, NONE) => true
skalberg@15531
    78
   | (SOME (_, i), NONE) => i > lim
skalberg@15531
    79
   | (NONE, SOME (_, i')) => i' > lim
skalberg@15531
    80
   | (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim);
wenzelm@247
    81
clasohm@0
    82
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
clasohm@0
    83
fun vupdate((a,t), env) = case t of
clasohm@0
    84
      Var(name',T) =>
wenzelm@247
    85
        if a=name' then env     (*cycle!*)
wenzelm@247
    86
        else if xless(a, name')  then
wenzelm@247
    87
           (case lookup(env,name') of  (*if already assigned, chase*)
skalberg@15531
    88
                NONE => update((name', Var(a,T)), env)
skalberg@15531
    89
              | SOME u => vupdate((a,u), env))
wenzelm@247
    90
        else update((a,t), env)
clasohm@0
    91
    | _ => update((a,t), env);
clasohm@0
    92
clasohm@0
    93
clasohm@0
    94
(*Convert environment to alist*)
berghofe@8407
    95
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
clasohm@0
    96
clasohm@0
    97
paulson@1500
    98
(*** Beta normal form for terms (not eta normal form).
paulson@1500
    99
     Chases variables in env;  Does not exploit sharing of variable bindings
paulson@1500
   100
     Does not check types, so could loop. ***)
paulson@1500
   101
paulson@1500
   102
(*raised when norm has no effect on a term, to do sharing instead of copying*)
paulson@1500
   103
exception SAME;
clasohm@0
   104
berghofe@11513
   105
fun norm_term1 same (asol,t) : term =
paulson@1500
   106
  let fun norm (Var (w,T)) =
wenzelm@10485
   107
            (case Vartab.lookup (asol, w) of
skalberg@15531
   108
                SOME u => (norm u handle SAME => u)
skalberg@15531
   109
              | NONE   => raise SAME)
wenzelm@10485
   110
        | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
wenzelm@10485
   111
        | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
wenzelm@10485
   112
        | norm (f $ t) =
wenzelm@10485
   113
            ((case norm f of
wenzelm@10485
   114
               Abs(_,_,body) => normh(subst_bound (t, body))
wenzelm@10485
   115
             | nf => nf $ (norm t handle SAME => t))
wenzelm@10485
   116
            handle SAME => f $ norm t)
wenzelm@10485
   117
        | norm _ =  raise SAME
paulson@2191
   118
      and normh t = norm t handle SAME => t
berghofe@11513
   119
  in (if same then norm else normh) t end
clasohm@0
   120
berghofe@11513
   121
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
berghofe@11513
   122
  | normT iTs (TFree _) = raise SAME
berghofe@11513
   123
  | normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
skalberg@15531
   124
          SOME U => normTh iTs U
skalberg@15531
   125
        | NONE => raise SAME)
berghofe@11513
   126
and normTh iTs T = ((normT iTs T) handle SAME => T)
berghofe@11513
   127
and normTs iTs [] = raise SAME
berghofe@11513
   128
  | normTs iTs (T :: Ts) =
berghofe@11513
   129
      ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
berghofe@11513
   130
       handle SAME => T :: normTs iTs Ts);
berghofe@11513
   131
berghofe@11513
   132
fun norm_term2 same (asol, iTs, t) : term =
berghofe@11513
   133
  let fun norm (Const (a, T)) = Const(a, normT iTs T)
berghofe@11513
   134
        | norm (Free (a, T)) = Free(a, normT iTs T)
berghofe@11513
   135
        | norm (Var (w, T)) =
wenzelm@10485
   136
            (case Vartab.lookup (asol, w) of
skalberg@15531
   137
                SOME u => normh u
skalberg@15531
   138
              | NONE   => Var(w, normT iTs T))
berghofe@11513
   139
        | norm (Abs (a, T, body)) =
berghofe@11513
   140
               (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
berghofe@11513
   141
        | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
berghofe@11513
   142
        | norm (f $ t) =
wenzelm@10485
   143
            ((case norm f of
berghofe@11513
   144
               Abs(_, _, body) => normh (subst_bound (t, body))
wenzelm@10485
   145
             | nf => nf $ normh t)
wenzelm@10485
   146
            handle SAME => f $ norm t)
wenzelm@10485
   147
        | norm _ =  raise SAME
paulson@1500
   148
      and normh t = (norm t) handle SAME => t
berghofe@11513
   149
  in (if same then norm else normh) t end;
clasohm@0
   150
berghofe@11513
   151
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
berghofe@11513
   152
  if Vartab.is_empty iTs then norm_term1 same (asol, t)
berghofe@11513
   153
  else norm_term2 same (asol, iTs, t);
berghofe@11513
   154
berghofe@11513
   155
val norm_term = gen_norm_term false;
berghofe@11513
   156
val norm_term_same = gen_norm_term true;
wenzelm@10485
   157
wenzelm@10485
   158
val beta_norm = norm_term (empty 0);
lcp@719
   159
wenzelm@12496
   160
fun norm_type iTs = normTh iTs;
wenzelm@12496
   161
fun norm_type_same iTs =
berghofe@11513
   162
  if Vartab.is_empty iTs then raise SAME else normT iTs;
berghofe@11513
   163
wenzelm@12496
   164
fun norm_types_same iTs =
berghofe@11513
   165
  if Vartab.is_empty iTs then raise SAME else normTs iTs;
berghofe@11513
   166
berghofe@11513
   167
berghofe@12231
   168
(*Put a term into head normal form for unification.*)
berghofe@12231
   169
berghofe@12231
   170
fun head_norm env t =
berghofe@12231
   171
  let
berghofe@12231
   172
    fun hnorm (Var (v, T)) = (case lookup (env, v) of
skalberg@15531
   173
          SOME u => head_norm env u
skalberg@15531
   174
        | NONE => raise SAME)
berghofe@12231
   175
      | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
berghofe@12231
   176
      | hnorm (Abs (_, _, body) $ t) =
berghofe@12231
   177
          head_norm env (subst_bound (t, body))
berghofe@12231
   178
      | hnorm (f $ t) = (case hnorm f of
berghofe@12231
   179
          Abs (_, _, body) => head_norm env (subst_bound (t, body))
berghofe@12231
   180
        | nf => nf $ t)
berghofe@12231
   181
	  | hnorm _ =  raise SAME
berghofe@12231
   182
  in hnorm t handle SAME => t end;
berghofe@12231
   183
berghofe@12231
   184
berghofe@12231
   185
(*finds type of term without checking that combinations are consistent
berghofe@12231
   186
  Ts holds types of bound variables*)
berghofe@12231
   187
fun fastype (Envir {iTs, ...}) =
berghofe@12231
   188
let val funerr = "fastype: expected function type";
berghofe@12231
   189
    fun fast Ts (f $ u) =
berghofe@12231
   190
	(case fast Ts f of
berghofe@12231
   191
	   Type ("fun", [_, T]) => T
berghofe@12231
   192
	 | TVar(ixn, _) =>
berghofe@12231
   193
		(case Vartab.lookup (iTs, ixn) of
skalberg@15531
   194
		   SOME (Type ("fun", [_, T])) => T
berghofe@12231
   195
		 | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   196
	 | _ => raise TERM (funerr, [f $ u]))
berghofe@12231
   197
      | fast Ts (Const (_, T)) = T
berghofe@12231
   198
      | fast Ts (Free (_, T)) = T
berghofe@12231
   199
      | fast Ts (Bound i) =
berghofe@12231
   200
	(nth_elem (i, Ts)
berghofe@12231
   201
  	 handle LIST _=> raise TERM ("fastype: Bound", [Bound i]))
berghofe@12231
   202
      | fast Ts (Var (_, T)) = T 
berghofe@12231
   203
      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
berghofe@12231
   204
in fast end;
berghofe@12231
   205
clasohm@0
   206
end;