src/Pure/envir.ML
author wenzelm
Fri May 24 17:00:46 2013 +0200 (2013-05-24)
changeset 52131 366fa32ee2a3
parent 52128 7f3549a316f4
child 52132 fa9e563f6bcf
permissions -rw-r--r--
tuned signature;
     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 -> int -> typ -> typ
    39   val binder_types: env -> int -> typ -> typ list
    40   val strip_type: env -> int -> 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           in
   258             fold_rev (Term.abs o pair "x") Us
   259               (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
   260                 (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
   261           end);
   262 
   263 
   264 (* full eta contraction *)
   265 
   266 local
   267 
   268 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
   269   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   270   | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
   271   | decr _ _ = raise Same.SAME
   272 and decrh lev t = (decr lev t handle Same.SAME => t);
   273 
   274 fun eta (Abs (a, T, body)) =
   275     ((case eta body of
   276         body' as (f $ Bound 0) =>
   277           if Term.is_dependent f then Abs (a, T, body')
   278           else decrh 0 f
   279      | body' => Abs (a, T, body')) handle Same.SAME =>
   280         (case body of
   281           f $ Bound 0 =>
   282             if Term.is_dependent f then raise Same.SAME
   283             else decrh 0 f
   284         | _ => raise Same.SAME))
   285   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
   286   | eta _ = raise Same.SAME;
   287 
   288 in
   289 
   290 fun eta_contract t =
   291   if Term.has_abs t then Same.commit eta t else t;
   292 
   293 end;
   294 
   295 val beta_eta_contract = eta_contract o beta_norm;
   296 
   297 fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
   298 
   299 
   300 fun body_type _ 0 T = T
   301   | body_type env n (Type ("fun", [_, T])) = body_type env (n - 1) T
   302   | body_type env n (T as TVar v) =
   303       (case Type.lookup (type_env env) v of
   304         NONE => T
   305       | SOME T' => body_type env n T')
   306   | body_type _ _ T = T;
   307 
   308 fun binder_types _ 0 _ = []
   309   | binder_types env n (Type ("fun", [T, U])) = T :: binder_types env (n - 1) U
   310   | binder_types env n (TVar v) =
   311       (case Type.lookup (type_env env) v of
   312         NONE => []
   313       | SOME T' => binder_types env n T')
   314   | binder_types _ _ _ = [];
   315 
   316 fun strip_type n env T = (binder_types n env T, body_type n env T);
   317 
   318 (*finds type of term without checking that combinations are consistent
   319   Ts holds types of bound variables*)
   320 fun fastype (Envir {tyenv, ...}) =
   321   let
   322     val funerr = "fastype: expected function type";
   323     fun fast Ts (f $ u) =
   324           (case Type.devar tyenv (fast Ts f) of
   325             Type ("fun", [_, T]) => T
   326           | TVar v => raise TERM (funerr, [f $ u])
   327           | _ => raise TERM (funerr, [f $ u]))
   328       | fast Ts (Const (_, T)) = T
   329       | fast Ts (Free (_, T)) = T
   330       | fast Ts (Bound i) =
   331           (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
   332       | fast Ts (Var (_, T)) = T
   333       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
   334   in fast end;
   335 
   336 
   337 (** plain substitution -- without variable chasing **)
   338 
   339 local
   340 
   341 fun subst_type0 tyenv = Term_Subst.map_atypsT_same
   342   (fn TVar v =>
   343         (case Type.lookup tyenv v of
   344           SOME U => U
   345         | NONE => raise Same.SAME)
   346     | _ => raise Same.SAME);
   347 
   348 fun subst_term1 tenv = Term_Subst.map_aterms_same
   349   (fn Var v =>
   350         (case lookup1 tenv v of
   351           SOME u => u
   352         | NONE => raise Same.SAME)
   353     | _ => raise Same.SAME);
   354 
   355 fun subst_term2 tenv tyenv : term Same.operation =
   356   let
   357     val substT = subst_type0 tyenv;
   358     fun subst (Const (a, T)) = Const (a, substT T)
   359       | subst (Free (a, T)) = Free (a, substT T)
   360       | subst (Var (xi, T)) =
   361           (case lookup1 tenv (xi, T) of
   362             SOME u => u
   363           | NONE => Var (xi, substT T))
   364       | subst (Bound _) = raise Same.SAME
   365       | subst (Abs (a, T, t)) =
   366           (Abs (a, substT T, Same.commit subst t)
   367             handle Same.SAME => Abs (a, T, subst t))
   368       | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   369   in subst end;
   370 
   371 in
   372 
   373 fun subst_type_same tyenv T =
   374   if Vartab.is_empty tyenv then raise Same.SAME
   375   else subst_type0 tyenv T;
   376 
   377 fun subst_term_types_same tyenv t =
   378   if Vartab.is_empty tyenv then raise Same.SAME
   379   else Term_Subst.map_types_same (subst_type0 tyenv) t;
   380 
   381 fun subst_term_same (tyenv, tenv) =
   382   if Vartab.is_empty tenv then subst_term_types_same tyenv
   383   else if Vartab.is_empty tyenv then subst_term1 tenv
   384   else subst_term2 tenv tyenv;
   385 
   386 fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   387 fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   388 fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   389 
   390 end;
   391 
   392 
   393 
   394 (** expand defined atoms -- with local beta reduction **)
   395 
   396 fun expand_atom T (U, u) =
   397   subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   398     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   399 
   400 fun expand_term get =
   401   let
   402     fun expand tm =
   403       let
   404         val (head, args) = Term.strip_comb tm;
   405         val args' = map expand args;
   406         fun comb head' = Term.list_comb (head', args');
   407       in
   408         (case head of
   409           Abs (x, T, t) => comb (Abs (x, T, expand t))
   410         | _ =>
   411           (case get head of
   412             SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   413           | NONE => comb head))
   414       end;
   415   in expand end;
   416 
   417 fun expand_term_frees defs =
   418   let
   419     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   420     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   421   in expand_term get end;
   422 
   423 end;