src/Pure/envir.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 63619 9c870388e87a
permissions -rw-r--r--
more robust sorted_entries;
     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 init: env
    19   val merge: env * env -> env
    20   val insert_sorts: env -> sort list -> sort list
    21   val genvars: string -> env * typ list -> env * term list
    22   val genvar: string -> env * typ -> env * term
    23   val lookup1: tenv -> indexname * typ -> term option
    24   val lookup: env -> indexname * typ -> term option
    25   val update: (indexname * typ) * term -> env -> env
    26   val above: env -> int -> bool
    27   val vupdate: (indexname * typ) * term -> env -> env
    28   val norm_type_same: Type.tyenv -> typ Same.operation
    29   val norm_types_same: Type.tyenv -> typ list Same.operation
    30   val norm_type: Type.tyenv -> typ -> typ
    31   val norm_term_same: env -> term Same.operation
    32   val norm_term: env -> term -> term
    33   val beta_norm: term -> term
    34   val head_norm: env -> term -> term
    35   val eta_long: typ list -> term -> term
    36   val eta_contract: term -> term
    37   val beta_eta_contract: term -> term
    38   val aeconv: term * term -> bool
    39   val body_type: env -> typ -> typ
    40   val binder_types: env -> typ -> typ list
    41   val strip_type: env -> typ -> typ list * typ
    42   val fastype: env -> typ list -> term -> typ
    43   val subst_type_same: Type.tyenv -> typ Same.operation
    44   val subst_term_types_same: Type.tyenv -> term Same.operation
    45   val subst_term_same: Type.tyenv * tenv -> term Same.operation
    46   val subst_type: Type.tyenv -> typ -> typ
    47   val subst_term_types: Type.tyenv -> term -> term
    48   val subst_term: Type.tyenv * tenv -> term -> term
    49   val expand_atom: typ -> typ * term -> term
    50   val expand_term: (term -> (typ * term) option) -> term -> term
    51   val expand_term_frees: ((string * typ) * term) list -> term -> term
    52 end;
    53 
    54 structure Envir: ENVIR =
    55 struct
    56 
    57 (** datatype env **)
    58 
    59 (*Updating can destroy environment in 2 ways!
    60    (1) variables out of range
    61    (2) circular assignments
    62 *)
    63 
    64 type tenv = (typ * term) Vartab.table;
    65 
    66 datatype env = Envir of
    67  {maxidx: int,          (*upper bound of maximum index of vars*)
    68   tenv: tenv,           (*assignments to Vars*)
    69   tyenv: Type.tyenv};   (*assignments to TVars*)
    70 
    71 fun make_env (maxidx, tenv, tyenv) =
    72   Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
    73 
    74 fun maxidx_of (Envir {maxidx, ...}) = maxidx;
    75 fun term_env (Envir {tenv, ...}) = tenv;
    76 fun type_env (Envir {tyenv, ...}) = tyenv;
    77 
    78 fun is_empty env =
    79   Vartab.is_empty (term_env env) andalso
    80   Vartab.is_empty (type_env env);
    81 
    82 
    83 (* build env *)
    84 
    85 fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
    86 val init = empty ~1;
    87 
    88 fun merge
    89    (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
    90     Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
    91   make_env (Int.max (maxidx1, maxidx2),
    92     Vartab.merge (op =) (tenv1, tenv2),
    93     Vartab.merge (op =) (tyenv1, tyenv2));
    94 
    95 
    96 (*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
    97 val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
    98 
    99 (*Generate a list of distinct variables.
   100   Increments index to make them distinct from ALL present variables. *)
   101 fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list =
   102   let
   103     fun genvs (_, [] : typ list) : term list = []
   104       | genvs (_, [T]) = [Var ((name, maxidx + 1), T)]
   105       | genvs (n, T :: Ts) =
   106           Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T)
   107             :: genvs (n + 1, Ts);
   108   in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end;
   109 
   110 (*Generate a variable.*)
   111 fun genvar name (env, T) : env * term =
   112   let val (env', [v]) = genvars name (env, [T])
   113   in (env', v) end;
   114 
   115 fun var_clash xi T T' =
   116   raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
   117 
   118 fun lookup_check check tenv (xi, T) =
   119   (case Vartab.lookup tenv xi of
   120     NONE => NONE
   121   | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
   122 
   123 (*When dealing with environments produced by matching instead
   124   of unification, there is no need to chase assigned TVars.
   125   In this case, we can simply ignore the type substitution
   126   and use = instead of eq_type.*)
   127 fun lookup1 tenv = lookup_check (op =) tenv;
   128 
   129 fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified 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 ((a, U), t) env =
   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 ((a, U), u) env)
   148       else update ((a, U), t) env
   149   | _ => update ((a, U), 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 (envir as Envir {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 lookup envir (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 as Envir {tenv, tyenv, ...}) =
   220   if Vartab.is_empty tyenv then norm_term1 tenv
   221   else norm_term2 envir;
   222 
   223 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
   224 
   225 fun beta_norm t =
   226   if Term.could_beta_contract t then norm_term init t else t;
   227 
   228 end;
   229 
   230 
   231 (* head normal form for unification *)
   232 
   233 fun head_norm env =
   234   let
   235     fun norm (Var v) =
   236         (case lookup env v of
   237           SOME u => head_norm env u
   238         | NONE => raise Same.SAME)
   239       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   240       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   241       | norm (f $ t) =
   242           (case norm f of
   243             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   244           | nf => nf $ t)
   245       | norm _ = raise Same.SAME;
   246   in Same.commit norm end;
   247 
   248 
   249 (* eta-long beta-normal form *)
   250 
   251 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   252   | eta_long Ts t =
   253       (case strip_comb t of
   254         (Abs _, _) => eta_long Ts (beta_norm t)
   255       | (u, ts) =>
   256           let
   257             val Us = binder_types (fastype_of1 (Ts, t));
   258             val i = length Us;
   259             val long = eta_long (rev Us @ Ts);
   260           in
   261             fold_rev (Term.abs o pair "x") Us
   262               (list_comb (incr_boundvars i u,
   263                 map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
   264           end);
   265 
   266 
   267 (* full eta contraction *)
   268 
   269 local
   270 
   271 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
   272   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   273   | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
   274   | decr _ _ = raise Same.SAME
   275 and decrh lev t = (decr lev t handle Same.SAME => t);
   276 
   277 fun eta (Abs (a, T, body)) =
   278     ((case eta body of
   279         body' as (f $ Bound 0) =>
   280           if Term.is_dependent f then Abs (a, T, body')
   281           else decrh 0 f
   282      | body' => Abs (a, T, body')) handle Same.SAME =>
   283         (case body of
   284           f $ Bound 0 =>
   285             if Term.is_dependent f then raise Same.SAME
   286             else decrh 0 f
   287         | _ => raise Same.SAME))
   288   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
   289   | eta _ = raise Same.SAME;
   290 
   291 in
   292 
   293 fun eta_contract t =
   294   if Term.could_eta_contract t then Same.commit eta t else t;
   295 
   296 end;
   297 
   298 val beta_eta_contract = eta_contract o beta_norm;
   299 
   300 fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
   301 
   302 
   303 fun body_type env (Type ("fun", [_, T])) = body_type env T
   304   | body_type env (T as TVar v) =
   305       (case Type.lookup (type_env env) v of
   306         NONE => T
   307       | SOME T' => body_type env T')
   308   | body_type _ T = T;
   309 
   310 fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U
   311   | binder_types env (TVar v) =
   312       (case Type.lookup (type_env env) v of
   313         NONE => []
   314       | SOME T' => binder_types env T')
   315   | binder_types _ _ = [];
   316 
   317 fun strip_type env T = (binder_types env T, body_type env T);
   318 
   319 (*finds type of term without checking that combinations are consistent
   320   Ts holds types of bound variables*)
   321 fun fastype (Envir {tyenv, ...}) =
   322   let
   323     val funerr = "fastype: expected function type";
   324     fun fast Ts (f $ u) =
   325           (case Type.devar tyenv (fast Ts f) of
   326             Type ("fun", [_, T]) => T
   327           | TVar _ => raise TERM (funerr, [f $ u])
   328           | _ => raise TERM (funerr, [f $ u]))
   329       | fast _ (Const (_, T)) = T
   330       | fast _ (Free (_, T)) = T
   331       | fast Ts (Bound i) =
   332           (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
   333       | fast _ (Var (_, T)) = T
   334       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
   335   in fast end;
   336 
   337 
   338 (** plain substitution -- without variable chasing **)
   339 
   340 local
   341 
   342 fun subst_type0 tyenv = Term_Subst.map_atypsT_same
   343   (fn TVar v =>
   344         (case Type.lookup tyenv v of
   345           SOME U => U
   346         | NONE => raise Same.SAME)
   347     | _ => raise Same.SAME);
   348 
   349 fun subst_term1 tenv = Term_Subst.map_aterms_same
   350   (fn Var v =>
   351         (case lookup1 tenv v of
   352           SOME u => u
   353         | NONE => raise Same.SAME)
   354     | _ => raise Same.SAME);
   355 
   356 fun subst_term2 tenv tyenv : term Same.operation =
   357   let
   358     val substT = subst_type0 tyenv;
   359     fun subst (Const (a, T)) = Const (a, substT T)
   360       | subst (Free (a, T)) = Free (a, substT T)
   361       | subst (Var (xi, T)) =
   362           (case lookup1 tenv (xi, T) of
   363             SOME u => u
   364           | NONE => Var (xi, substT T))
   365       | subst (Bound _) = raise Same.SAME
   366       | subst (Abs (a, T, t)) =
   367           (Abs (a, substT T, Same.commit subst t)
   368             handle Same.SAME => Abs (a, T, subst t))
   369       | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   370   in subst end;
   371 
   372 in
   373 
   374 fun subst_type_same tyenv T =
   375   if Vartab.is_empty tyenv then raise Same.SAME
   376   else subst_type0 tyenv T;
   377 
   378 fun subst_term_types_same tyenv t =
   379   if Vartab.is_empty tyenv then raise Same.SAME
   380   else Term_Subst.map_types_same (subst_type0 tyenv) t;
   381 
   382 fun subst_term_same (tyenv, tenv) =
   383   if Vartab.is_empty tenv then subst_term_types_same tyenv
   384   else if Vartab.is_empty tyenv then subst_term1 tenv
   385   else subst_term2 tenv tyenv;
   386 
   387 fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   388 fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   389 fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   390 
   391 end;
   392 
   393 
   394 
   395 (** expand defined atoms -- with local beta reduction **)
   396 
   397 fun expand_atom T (U, u) =
   398   subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   399     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   400 
   401 fun expand_term get =
   402   let
   403     fun expand tm =
   404       let
   405         val (head, args) = Term.strip_comb tm;
   406         val args' = map expand args;
   407         fun comb head' = Term.list_comb (head', args');
   408       in
   409         (case head of
   410           Abs (x, T, t) => comb (Abs (x, T, expand t))
   411         | _ =>
   412           (case get head of
   413             SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   414           | NONE => comb head))
   415       end;
   416   in expand end;
   417 
   418 fun expand_term_frees defs =
   419   let
   420     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   421     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   422   in expand_term get end;
   423 
   424 end;