src/Pure/envir.ML
author wenzelm
Sun Apr 13 16:40:04 2008 +0200 (2008-04-13)
changeset 26638 1d5d42d8fd66
parent 26328 b2d6f520172c
child 29269 5c25a2012975
permissions -rw-r--r--
added insert_sorts (from thm.ML);
     1 (*  Title:      Pure/envir.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1988  University of Cambridge
     5 
     6 Environments.  The type of a term variable / sort of a type variable is
     7 part of its name. The lookup function must apply type substitutions,
     8 since they may change the identity of a variable.
     9 *)
    10 
    11 signature ENVIR =
    12 sig
    13   type tenv
    14   datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
    15   val type_env: env -> Type.tyenv
    16   val insert_sorts: env -> sort list -> sort list
    17   exception SAME
    18   val genvars: string -> env * typ list -> env * term list
    19   val genvar: string -> env * typ -> env * term
    20   val lookup: env * (indexname * typ) -> term option
    21   val lookup': tenv * (indexname * typ) -> term option
    22   val update: ((indexname * typ) * term) * env -> env
    23   val empty: int -> env
    24   val is_empty: env -> bool
    25   val above: env -> int -> bool
    26   val vupdate: ((indexname * typ) * term) * env -> env
    27   val alist_of: env -> (indexname * (typ * term)) list
    28   val norm_term: env -> term -> term
    29   val norm_term_same: env -> term -> term
    30   val norm_type: Type.tyenv -> typ -> typ
    31   val norm_type_same: Type.tyenv -> typ -> typ
    32   val norm_types_same: Type.tyenv -> typ list -> typ list
    33   val beta_norm: term -> term
    34   val head_norm: env -> term -> term
    35   val eta_contract: term -> term
    36   val beta_eta_contract: term -> term
    37   val fastype: env -> typ list -> term -> typ
    38   val typ_subst_TVars: Type.tyenv -> typ -> typ
    39   val subst_TVars: Type.tyenv -> term -> term
    40   val subst_Vars: tenv -> term -> term
    41   val subst_vars: Type.tyenv * tenv -> term -> term
    42   val expand_atom: typ -> typ * term -> term
    43   val expand_term: (term -> (typ * term) option) -> term -> term
    44   val expand_term_frees: ((string * typ) * term) list -> term -> term
    45 end;
    46 
    47 structure Envir : ENVIR =
    48 struct
    49 
    50 (*updating can destroy environment in 2 ways!!
    51    (1) variables out of range   (2) circular assignments
    52 *)
    53 type tenv = (typ * term) Vartab.table
    54 
    55 datatype env = Envir of
    56     {maxidx: int,      (*maximum index of vars*)
    57      asol: tenv,       (*table of assignments to Vars*)
    58      iTs: Type.tyenv}  (*table of assignments to TVars*)
    59 
    60 fun type_env (Envir {iTs, ...}) = iTs;
    61 
    62 (*NB: type unification may invent new sorts*)
    63 val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
    64 
    65 (*Generate a list of distinct variables.
    66   Increments index to make them distinct from ALL present variables. *)
    67 fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
    68   let fun genvs (_, [] : typ list) : term list = []
    69         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
    70         | genvs (n, T::Ts) =
    71             Var((name ^ radixstring(26,"a",n), maxidx+1), T)
    72             :: genvs(n+1,Ts)
    73   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
    74 
    75 (*Generate a variable.*)
    76 fun genvar name (env,T) : env * term =
    77   let val (env',[v]) = genvars name (env,[T])
    78   in  (env',v)  end;
    79 
    80 fun var_clash ixn T T' = raise TYPE ("Variable " ^
    81   quote (Term.string_of_vname ixn) ^ " has two distinct types",
    82   [T', T], []);
    83 
    84 fun gen_lookup f asol (xname, T) =
    85   (case Vartab.lookup asol xname of
    86      NONE => NONE
    87    | SOME (U, t) => if f (T, U) then SOME t
    88        else var_clash xname T U);
    89 
    90 (* When dealing with environments produced by matching instead *)
    91 (* of unification, there is no need to chase assigned TVars.   *)
    92 (* In this case, we can simply ignore the type substitution    *)
    93 (* and use = instead of eq_type.                               *)
    94 
    95 fun lookup' (asol, p) = gen_lookup op = asol p;
    96 
    97 fun lookup2 (iTs, asol) p =
    98   if Vartab.is_empty iTs then lookup' (asol, p)
    99   else gen_lookup (Type.eq_type iTs) asol p;
   100 
   101 fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
   102 
   103 fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
   104   Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs};
   105 
   106 (*The empty environment.  New variables will start with the given index+1.*)
   107 fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
   108 
   109 (*Test for empty environment*)
   110 fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
   111 
   112 (*Determine if the least index updated exceeds lim*)
   113 fun above (Envir {asol, iTs, ...}) lim =
   114   (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
   115   (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
   116 
   117 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   118 fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
   119       Var (nT as (name', T)) =>
   120         if a = name' then env     (*cycle!*)
   121         else if Term.indexname_ord (a, name') = LESS then
   122            (case lookup (env, nT) of  (*if already assigned, chase*)
   123                 NONE => update ((nT, Var (a, T)), env)
   124               | SOME u => vupdate ((aU, u), env))
   125         else update ((aU, t), env)
   126     | _ => update ((aU, t), env);
   127 
   128 
   129 (*Convert environment to alist*)
   130 fun alist_of (Envir{asol,...}) = Vartab.dest asol;
   131 
   132 
   133 (*** Beta normal form for terms (not eta normal form).
   134      Chases variables in env;  Does not exploit sharing of variable bindings
   135      Does not check types, so could loop. ***)
   136 
   137 (*raised when norm has no effect on a term, to do sharing instead of copying*)
   138 exception SAME;
   139 
   140 fun norm_term1 same (asol,t) : term =
   141   let fun norm (Var wT) =
   142             (case lookup' (asol, wT) of
   143                 SOME u => (norm u handle SAME => u)
   144               | NONE   => raise SAME)
   145         | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   146         | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
   147         | norm (f $ t) =
   148             ((case norm f of
   149                Abs(_,_,body) => normh(subst_bound (t, body))
   150              | nf => nf $ (norm t handle SAME => t))
   151             handle SAME => f $ norm t)
   152         | norm _ =  raise SAME
   153       and normh t = norm t handle SAME => t
   154   in (if same then norm else normh) t end
   155 
   156 fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   157   | normT iTs (TFree _) = raise SAME
   158   | normT iTs (TVar vS) = (case Type.lookup iTs vS of
   159           SOME U => normTh iTs U
   160         | NONE => raise SAME)
   161 and normTh iTs T = ((normT iTs T) handle SAME => T)
   162 and normTs iTs [] = raise SAME
   163   | normTs iTs (T :: Ts) =
   164       ((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
   165        handle SAME => T :: normTs iTs Ts);
   166 
   167 fun norm_term2 same (asol, iTs, t) : term =
   168   let fun norm (Const (a, T)) = Const(a, normT iTs T)
   169         | norm (Free (a, T)) = Free(a, normT iTs T)
   170         | norm (Var (w, T)) =
   171             (case lookup2 (iTs, asol) (w, T) of
   172                 SOME u => normh u
   173               | NONE   => Var(w, normT iTs T))
   174         | norm (Abs (a, T, body)) =
   175                (Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
   176         | norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
   177         | norm (f $ t) =
   178             ((case norm f of
   179                Abs(_, _, body) => normh (subst_bound (t, body))
   180              | nf => nf $ normh t)
   181             handle SAME => f $ norm t)
   182         | norm _ =  raise SAME
   183       and normh t = (norm t) handle SAME => t
   184   in (if same then norm else normh) t end;
   185 
   186 fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
   187   if Vartab.is_empty iTs then norm_term1 same (asol, t)
   188   else norm_term2 same (asol, iTs, t);
   189 
   190 val norm_term = gen_norm_term false;
   191 val norm_term_same = gen_norm_term true;
   192 
   193 fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
   194 
   195 fun norm_type iTs = normTh iTs;
   196 fun norm_type_same iTs =
   197   if Vartab.is_empty iTs then raise SAME else normT iTs;
   198 
   199 fun norm_types_same iTs =
   200   if Vartab.is_empty iTs then raise SAME else normTs iTs;
   201 
   202 
   203 (*Put a term into head normal form for unification.*)
   204 
   205 fun head_norm env t =
   206   let
   207     fun hnorm (Var vT) = (case lookup (env, vT) of
   208           SOME u => head_norm env u
   209         | NONE => raise SAME)
   210       | hnorm (Abs (a, T, body)) =  Abs (a, T, hnorm body)
   211       | hnorm (Abs (_, _, body) $ t) =
   212           head_norm env (subst_bound (t, body))
   213       | hnorm (f $ t) = (case hnorm f of
   214           Abs (_, _, body) => head_norm env (subst_bound (t, body))
   215         | nf => nf $ t)
   216           | hnorm _ =  raise SAME
   217   in hnorm t handle SAME => t end;
   218 
   219 
   220 (*Eta-contract a term (fully)*)
   221 
   222 local
   223 
   224 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise SAME
   225   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   226   | decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u)
   227   | decr _ _ = raise SAME
   228 and decrh lev t = (decr lev t handle SAME => t);
   229 
   230 fun eta (Abs (a, T, body)) =
   231     ((case eta body of
   232         body' as (f $ Bound 0) =>
   233           if loose_bvar1 (f, 0) then Abs (a, T, body')
   234           else decrh 0 f
   235      | body' => Abs (a, T, body')) handle SAME =>
   236         (case body of
   237           f $ Bound 0 =>
   238             if loose_bvar1 (f, 0) then raise SAME
   239             else decrh 0 f
   240         | _ => raise SAME))
   241   | eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u)
   242   | eta _ = raise SAME
   243 and etah t = (eta t handle SAME => t);
   244 
   245 in
   246 
   247 fun eta_contract t =
   248   if Term.has_abs t then etah t else t;
   249 
   250 val beta_eta_contract = eta_contract o beta_norm;
   251 
   252 end;
   253 
   254 
   255 (*finds type of term without checking that combinations are consistent
   256   Ts holds types of bound variables*)
   257 fun fastype (Envir {iTs, ...}) =
   258 let val funerr = "fastype: expected function type";
   259     fun fast Ts (f $ u) =
   260         (case fast Ts f of
   261            Type ("fun", [_, T]) => T
   262          | TVar ixnS =>
   263                 (case Type.lookup iTs ixnS of
   264                    SOME (Type ("fun", [_, T])) => T
   265                  | _ => raise TERM (funerr, [f $ u]))
   266          | _ => raise TERM (funerr, [f $ u]))
   267       | fast Ts (Const (_, T)) = T
   268       | fast Ts (Free (_, T)) = T
   269       | fast Ts (Bound i) =
   270         (List.nth (Ts, i)
   271          handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
   272       | fast Ts (Var (_, T)) = T
   273       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
   274 in fast end;
   275 
   276 
   277 (*Substitute for type Vars in a type*)
   278 fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
   279   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
   280         | subst(T as TFree _) = T
   281         | subst(T as TVar ixnS) =
   282             (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
   283   in subst T end;
   284 
   285 (*Substitute for type Vars in a term*)
   286 val subst_TVars = map_types o typ_subst_TVars;
   287 
   288 (*Substitute for Vars in a term *)
   289 fun subst_Vars itms t = if Vartab.is_empty itms then t else
   290   let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
   291         | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   292         | subst (f $ t) = subst f $ subst t
   293         | subst t = t
   294   in subst t end;
   295 
   296 (*Substitute for type/term Vars in a term *)
   297 fun subst_vars (iTs, itms) =
   298   if Vartab.is_empty iTs then subst_Vars itms else
   299   let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
   300         | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
   301         | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
   302             NONE   => Var (ixn, typ_subst_TVars iTs T)
   303           | SOME t => t)
   304         | subst (b as Bound _) = b
   305         | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
   306         | subst (f $ t) = subst f $ subst t
   307   in subst end;
   308 
   309 
   310 (* expand defined atoms -- with local beta reduction *)
   311 
   312 fun expand_atom T (U, u) =
   313   subst_TVars (Type.raw_match (U, T) Vartab.empty) u
   314   handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   315 
   316 fun expand_term get =
   317   let
   318     fun expand tm =
   319       let
   320         val (head, args) = Term.strip_comb tm;
   321         val args' = map expand args;
   322         fun comb head' = Term.list_comb (head', args');
   323       in
   324         (case head of
   325           Abs (x, T, t) => comb (Abs (x, T, expand t))
   326         | _ =>
   327             (case get head of
   328               SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   329             | NONE => comb head)
   330         | _ => comb head)
   331       end;
   332   in expand end;
   333 
   334 fun expand_term_frees defs =
   335   let
   336     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   337     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   338   in expand_term get end;
   339 
   340 end;