src/Pure/envir.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 52221 4ffe819a9b11
child 58945 cfb254e6c261
permissions -rw-r--r--
use E 1.8's auto scheduler option
     1 (*  Title:      Pure/envir.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Free-form environments.  The type of a term variable / sort of a type variable is
     5 part of its name.  The lookup function must apply type substitutions,
     6 since they may change the identity of a variable.
     7 *)
     8 
     9 signature ENVIR =
    10 sig
    11   type tenv = (typ * term) Vartab.table
    12   datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
    13   val maxidx_of: env -> int
    14   val term_env: env -> tenv
    15   val type_env: env -> Type.tyenv
    16   val is_empty: env -> bool
    17   val empty: int -> env
    18   val merge: env * env -> env
    19   val insert_sorts: env -> sort list -> sort list
    20   val genvars: string -> env * typ list -> env * term list
    21   val genvar: string -> env * typ -> env * term
    22   val lookup1: tenv -> indexname * typ -> term option
    23   val lookup: env -> indexname * typ -> term option
    24   val update: (indexname * typ) * term -> env -> env
    25   val above: env -> int -> bool
    26   val vupdate: (indexname * typ) * term -> env -> env
    27   val norm_type_same: Type.tyenv -> typ Same.operation
    28   val norm_types_same: Type.tyenv -> typ list Same.operation
    29   val norm_type: Type.tyenv -> typ -> typ
    30   val norm_term_same: env -> term Same.operation
    31   val norm_term: env -> term -> term
    32   val beta_norm: term -> term
    33   val head_norm: env -> term -> term
    34   val eta_long: typ list -> term -> term
    35   val eta_contract: term -> term
    36   val beta_eta_contract: term -> term
    37   val aeconv: term * term -> bool
    38   val body_type: env -> typ -> typ
    39   val binder_types: env -> typ -> typ list
    40   val strip_type: env -> typ -> typ list * typ
    41   val fastype: env -> typ list -> term -> typ
    42   val subst_type_same: Type.tyenv -> typ Same.operation
    43   val subst_term_types_same: Type.tyenv -> term Same.operation
    44   val subst_term_same: Type.tyenv * tenv -> term Same.operation
    45   val subst_type: Type.tyenv -> typ -> typ
    46   val subst_term_types: Type.tyenv -> term -> term
    47   val subst_term: Type.tyenv * tenv -> term -> term
    48   val expand_atom: typ -> typ * term -> term
    49   val expand_term: (term -> (typ * term) option) -> term -> term
    50   val expand_term_frees: ((string * typ) * term) list -> term -> term
    51 end;
    52 
    53 structure Envir: ENVIR =
    54 struct
    55 
    56 (** datatype env **)
    57 
    58 (*Updating can destroy environment in 2 ways!
    59    (1) variables out of range
    60    (2) circular assignments
    61 *)
    62 
    63 type tenv = (typ * term) Vartab.table;
    64 
    65 datatype env = Envir of
    66  {maxidx: int,          (*upper bound of maximum index of vars*)
    67   tenv: tenv,           (*assignments to Vars*)
    68   tyenv: Type.tyenv};   (*assignments to TVars*)
    69 
    70 fun make_env (maxidx, tenv, tyenv) =
    71   Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
    72 
    73 fun maxidx_of (Envir {maxidx, ...}) = maxidx;
    74 fun term_env (Envir {tenv, ...}) = tenv;
    75 fun type_env (Envir {tyenv, ...}) = tyenv;
    76 
    77 fun is_empty env =
    78   Vartab.is_empty (term_env env) andalso
    79   Vartab.is_empty (type_env env);
    80 
    81 
    82 (* build env *)
    83 
    84 fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
    85 
    86 fun merge
    87    (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
    88     Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
    89   make_env (Int.max (maxidx1, maxidx2),
    90     Vartab.merge (op =) (tenv1, tenv2),
    91     Vartab.merge (op =) (tyenv1, tyenv2));
    92 
    93 
    94 (*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
    95 val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
    96 
    97 (*Generate a list of distinct variables.
    98   Increments index to make them distinct from ALL present variables. *)
    99 fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
   100   let
   101     fun genvs (_, [] : typ list) : term list = []
   102       | genvs (n, [T]) = [Var ((name, maxidx + 1), T)]
   103       | genvs (n, T :: Ts) =
   104           Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
   105             :: genvs (n + 1, Ts);
   106   in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
   107 
   108 (*Generate a variable.*)
   109 fun genvar name (env, T) : env * term =
   110   let val (env', [v]) = genvars name (env, [T])
   111   in (env', v) end;
   112 
   113 fun var_clash xi T T' =
   114   raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
   115 
   116 fun lookup_check check tenv (xi, T) =
   117   (case Vartab.lookup tenv xi of
   118     NONE => NONE
   119   | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
   120 
   121 (*When dealing with environments produced by matching instead
   122   of unification, there is no need to chase assigned TVars.
   123   In this case, we can simply ignore the type substitution
   124   and use = instead of eq_type.*)
   125 fun lookup1 tenv = lookup_check (op =) tenv;
   126 
   127 fun lookup2 (tyenv, tenv) = lookup_check (Type.eq_type tyenv) tenv;
   128 
   129 fun lookup (Envir {tenv, tyenv, ...}) = lookup2 (tyenv, tenv);
   130 
   131 fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
   132   Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
   133 
   134 (*Determine if the least index updated exceeds lim*)
   135 fun above (Envir {tenv, tyenv, ...}) lim =
   136   (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso
   137   (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true);
   138 
   139 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   140 fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
   141   (case t of
   142     Var (nT as (name', T)) =>
   143       if a = name' then env     (*cycle!*)
   144       else if Term_Ord.indexname_ord (a, name') = LESS then
   145         (case lookup env nT of  (*if already assigned, chase*)
   146           NONE => update (nT, Var (a, T)) env
   147         | SOME u => vupdate (aU, u) env)
   148       else update (aU, t) env
   149   | _ => update (aU, t) env);
   150 
   151 
   152 
   153 (** beta normalization wrt. environment **)
   154 
   155 (*Chases variables in env.  Does not exploit sharing of variable bindings
   156   Does not check types, so could loop.*)
   157 
   158 local
   159 
   160 fun norm_type0 tyenv : typ Same.operation =
   161   let
   162     fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
   163       | norm (TFree _) = raise Same.SAME
   164       | norm (TVar v) =
   165           (case Type.lookup tyenv v of
   166             SOME U => Same.commit norm U
   167           | NONE => raise Same.SAME);
   168   in norm end;
   169 
   170 fun norm_term1 tenv : term Same.operation =
   171   let
   172     fun norm (Var v) =
   173           (case lookup1 tenv v of
   174             SOME u => Same.commit norm u
   175           | NONE => raise Same.SAME)
   176       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   177       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   178       | norm (f $ t) =
   179           ((case norm f of
   180              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   181            | nf => nf $ Same.commit norm t)
   182           handle Same.SAME => f $ norm t)
   183       | norm _ = raise Same.SAME;
   184   in norm end;
   185 
   186 fun norm_term2 tenv tyenv : term Same.operation =
   187   let
   188     val normT = norm_type0 tyenv;
   189     fun norm (Const (a, T)) = Const (a, normT T)
   190       | norm (Free (a, T)) = Free (a, normT T)
   191       | norm (Var (xi, T)) =
   192           (case lookup2 (tyenv, tenv) (xi, T) of
   193             SOME u => Same.commit norm u
   194           | NONE => Var (xi, normT T))
   195       | norm (Abs (a, T, body)) =
   196           (Abs (a, normT T, Same.commit norm body)
   197             handle Same.SAME => Abs (a, T, norm body))
   198       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   199       | norm (f $ t) =
   200           ((case norm f of
   201              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   202            | nf => nf $ Same.commit norm t)
   203           handle Same.SAME => f $ norm t)
   204       | norm _ = raise Same.SAME;
   205   in norm end;
   206 
   207 in
   208 
   209 fun norm_type_same tyenv T =
   210   if Vartab.is_empty tyenv then raise Same.SAME
   211   else norm_type0 tyenv T;
   212 
   213 fun norm_types_same tyenv Ts =
   214   if Vartab.is_empty tyenv then raise Same.SAME
   215   else Same.map (norm_type0 tyenv) Ts;
   216 
   217 fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
   218 
   219 fun norm_term_same (Envir {tenv, tyenv, ...}) =
   220   if Vartab.is_empty tyenv then norm_term1 tenv
   221   else norm_term2 tenv tyenv;
   222 
   223 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
   224 fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
   225 
   226 end;
   227 
   228 
   229 (* head normal form for unification *)
   230 
   231 fun head_norm env =
   232   let
   233     fun norm (Var v) =
   234         (case lookup env v of
   235           SOME u => head_norm env u
   236         | NONE => raise Same.SAME)
   237       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   238       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   239       | norm (f $ t) =
   240           (case norm f of
   241             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   242           | nf => nf $ t)
   243       | norm _ = raise Same.SAME;
   244   in Same.commit norm end;
   245 
   246 
   247 (* eta-long beta-normal form *)
   248 
   249 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   250   | eta_long Ts t =
   251       (case strip_comb t of
   252         (Abs _, _) => eta_long Ts (beta_norm t)
   253       | (u, ts) =>
   254           let
   255             val Us = binder_types (fastype_of1 (Ts, t));
   256             val i = length Us;
   257             val long = eta_long (rev Us @ Ts);
   258           in
   259             fold_rev (Term.abs o pair "x") Us
   260               (list_comb (incr_boundvars i u,
   261                 map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
   262           end);
   263 
   264 
   265 (* full eta contraction *)
   266 
   267 local
   268 
   269 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
   270   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   271   | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
   272   | decr _ _ = raise Same.SAME
   273 and decrh lev t = (decr lev t handle Same.SAME => t);
   274 
   275 fun eta (Abs (a, T, body)) =
   276     ((case eta body of
   277         body' as (f $ Bound 0) =>
   278           if Term.is_dependent f then Abs (a, T, body')
   279           else decrh 0 f
   280      | body' => Abs (a, T, body')) handle Same.SAME =>
   281         (case body of
   282           f $ Bound 0 =>
   283             if Term.is_dependent f then raise Same.SAME
   284             else decrh 0 f
   285         | _ => raise Same.SAME))
   286   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
   287   | eta _ = raise Same.SAME;
   288 
   289 in
   290 
   291 fun eta_contract t =
   292   if Term.has_abs t then Same.commit eta t else t;
   293 
   294 end;
   295 
   296 val beta_eta_contract = eta_contract o beta_norm;
   297 
   298 fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
   299 
   300 
   301 fun body_type env (Type ("fun", [_, T])) = body_type env T
   302   | body_type env (T as TVar v) =
   303       (case Type.lookup (type_env env) v of
   304         NONE => T
   305       | SOME T' => body_type env T')
   306   | body_type _ T = T;
   307 
   308 fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U
   309   | binder_types env (TVar v) =
   310       (case Type.lookup (type_env env) v of
   311         NONE => []
   312       | SOME T' => binder_types env T')
   313   | binder_types _ _ = [];
   314 
   315 fun strip_type env T = (binder_types env T, body_type env T);
   316 
   317 (*finds type of term without checking that combinations are consistent
   318   Ts holds types of bound variables*)
   319 fun fastype (Envir {tyenv, ...}) =
   320   let
   321     val funerr = "fastype: expected function type";
   322     fun fast Ts (f $ u) =
   323           (case Type.devar tyenv (fast Ts f) of
   324             Type ("fun", [_, T]) => T
   325           | TVar v => raise TERM (funerr, [f $ u])
   326           | _ => raise TERM (funerr, [f $ u]))
   327       | fast Ts (Const (_, T)) = T
   328       | fast Ts (Free (_, T)) = T
   329       | fast Ts (Bound i) =
   330           (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
   331       | fast Ts (Var (_, T)) = T
   332       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
   333   in fast end;
   334 
   335 
   336 (** plain substitution -- without variable chasing **)
   337 
   338 local
   339 
   340 fun subst_type0 tyenv = Term_Subst.map_atypsT_same
   341   (fn TVar v =>
   342         (case Type.lookup tyenv v of
   343           SOME U => U
   344         | NONE => raise Same.SAME)
   345     | _ => raise Same.SAME);
   346 
   347 fun subst_term1 tenv = Term_Subst.map_aterms_same
   348   (fn Var v =>
   349         (case lookup1 tenv v of
   350           SOME u => u
   351         | NONE => raise Same.SAME)
   352     | _ => raise Same.SAME);
   353 
   354 fun subst_term2 tenv tyenv : term Same.operation =
   355   let
   356     val substT = subst_type0 tyenv;
   357     fun subst (Const (a, T)) = Const (a, substT T)
   358       | subst (Free (a, T)) = Free (a, substT T)
   359       | subst (Var (xi, T)) =
   360           (case lookup1 tenv (xi, T) of
   361             SOME u => u
   362           | NONE => Var (xi, substT T))
   363       | subst (Bound _) = raise Same.SAME
   364       | subst (Abs (a, T, t)) =
   365           (Abs (a, substT T, Same.commit subst t)
   366             handle Same.SAME => Abs (a, T, subst t))
   367       | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   368   in subst end;
   369 
   370 in
   371 
   372 fun subst_type_same tyenv T =
   373   if Vartab.is_empty tyenv then raise Same.SAME
   374   else subst_type0 tyenv T;
   375 
   376 fun subst_term_types_same tyenv t =
   377   if Vartab.is_empty tyenv then raise Same.SAME
   378   else Term_Subst.map_types_same (subst_type0 tyenv) t;
   379 
   380 fun subst_term_same (tyenv, tenv) =
   381   if Vartab.is_empty tenv then subst_term_types_same tyenv
   382   else if Vartab.is_empty tyenv then subst_term1 tenv
   383   else subst_term2 tenv tyenv;
   384 
   385 fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   386 fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   387 fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   388 
   389 end;
   390 
   391 
   392 
   393 (** expand defined atoms -- with local beta reduction **)
   394 
   395 fun expand_atom T (U, u) =
   396   subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   397     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   398 
   399 fun expand_term get =
   400   let
   401     fun expand tm =
   402       let
   403         val (head, args) = Term.strip_comb tm;
   404         val args' = map expand args;
   405         fun comb head' = Term.list_comb (head', args');
   406       in
   407         (case head of
   408           Abs (x, T, t) => comb (Abs (x, T, expand t))
   409         | _ =>
   410           (case get head of
   411             SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   412           | NONE => comb head))
   413       end;
   414   in expand end;
   415 
   416 fun expand_term_frees defs =
   417   let
   418     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   419     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   420   in expand_term get end;
   421 
   422 end;