src/Pure/envir.ML
author wenzelm
Fri Jul 17 21:40:47 2015 +0200 (2015-07-17)
changeset 60749 f727b99faaf7
parent 58949 e9559088ba29
child 63615 d786d54efc70
permissions -rw-r--r--
skeleton for interactive debugger;
     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 lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv;
   128 
   129 fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
   130   Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
   131 
   132 (*Determine if the least index updated exceeds lim*)
   133 fun above (Envir {tenv, tyenv, ...}) lim =
   134   (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso
   135   (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true);
   136 
   137 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   138 fun vupdate (aU as (a, U), t) (env as Envir {tyenv, ...}) =
   139   (case t of
   140     Var (nT as (name', T)) =>
   141       if a = name' then env     (*cycle!*)
   142       else if Term_Ord.indexname_ord (a, name') = LESS then
   143         (case lookup env nT of  (*if already assigned, chase*)
   144           NONE => update (nT, Var (a, T)) env
   145         | SOME u => vupdate (aU, u) env)
   146       else update (aU, t) env
   147   | _ => update (aU, t) env);
   148 
   149 
   150 
   151 (** beta normalization wrt. environment **)
   152 
   153 (*Chases variables in env.  Does not exploit sharing of variable bindings
   154   Does not check types, so could loop.*)
   155 
   156 local
   157 
   158 fun norm_type0 tyenv : typ Same.operation =
   159   let
   160     fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
   161       | norm (TFree _) = raise Same.SAME
   162       | norm (TVar v) =
   163           (case Type.lookup tyenv v of
   164             SOME U => Same.commit norm U
   165           | NONE => raise Same.SAME);
   166   in norm end;
   167 
   168 fun norm_term1 tenv : term Same.operation =
   169   let
   170     fun norm (Var v) =
   171           (case lookup1 tenv v of
   172             SOME u => Same.commit norm u
   173           | NONE => raise Same.SAME)
   174       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   175       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   176       | norm (f $ t) =
   177           ((case norm f of
   178              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   179            | nf => nf $ Same.commit norm t)
   180           handle Same.SAME => f $ norm t)
   181       | norm _ = raise Same.SAME;
   182   in norm end;
   183 
   184 fun norm_term2 (envir as Envir {tenv, tyenv, ...}) : term Same.operation =
   185   let
   186     val normT = norm_type0 tyenv;
   187     fun norm (Const (a, T)) = Const (a, normT T)
   188       | norm (Free (a, T)) = Free (a, normT T)
   189       | norm (Var (xi, T)) =
   190           (case lookup envir (xi, T) of
   191             SOME u => Same.commit norm u
   192           | NONE => Var (xi, normT T))
   193       | norm (Abs (a, T, body)) =
   194           (Abs (a, normT T, Same.commit norm body)
   195             handle Same.SAME => Abs (a, T, norm body))
   196       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   197       | norm (f $ t) =
   198           ((case norm f of
   199              Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   200            | nf => nf $ Same.commit norm t)
   201           handle Same.SAME => f $ norm t)
   202       | norm _ = raise Same.SAME;
   203   in norm end;
   204 
   205 in
   206 
   207 fun norm_type_same tyenv T =
   208   if Vartab.is_empty tyenv then raise Same.SAME
   209   else norm_type0 tyenv T;
   210 
   211 fun norm_types_same tyenv Ts =
   212   if Vartab.is_empty tyenv then raise Same.SAME
   213   else Same.map (norm_type0 tyenv) Ts;
   214 
   215 fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
   216 
   217 fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
   218   if Vartab.is_empty tyenv then norm_term1 tenv
   219   else norm_term2 envir;
   220 
   221 fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
   222 fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
   223 
   224 end;
   225 
   226 
   227 (* head normal form for unification *)
   228 
   229 fun head_norm env =
   230   let
   231     fun norm (Var v) =
   232         (case lookup env v of
   233           SOME u => head_norm env u
   234         | NONE => raise Same.SAME)
   235       | norm (Abs (a, T, body)) = Abs (a, T, norm body)
   236       | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
   237       | norm (f $ t) =
   238           (case norm f of
   239             Abs (_, _, body) => Same.commit norm (subst_bound (t, body))
   240           | nf => nf $ t)
   241       | norm _ = raise Same.SAME;
   242   in Same.commit norm end;
   243 
   244 
   245 (* eta-long beta-normal form *)
   246 
   247 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
   248   | eta_long Ts t =
   249       (case strip_comb t of
   250         (Abs _, _) => eta_long Ts (beta_norm t)
   251       | (u, ts) =>
   252           let
   253             val Us = binder_types (fastype_of1 (Ts, t));
   254             val i = length Us;
   255             val long = eta_long (rev Us @ Ts);
   256           in
   257             fold_rev (Term.abs o pair "x") Us
   258               (list_comb (incr_boundvars i u,
   259                 map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
   260           end);
   261 
   262 
   263 (* full eta contraction *)
   264 
   265 local
   266 
   267 fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
   268   | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
   269   | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
   270   | decr _ _ = raise Same.SAME
   271 and decrh lev t = (decr lev t handle Same.SAME => t);
   272 
   273 fun eta (Abs (a, T, body)) =
   274     ((case eta body of
   275         body' as (f $ Bound 0) =>
   276           if Term.is_dependent f then Abs (a, T, body')
   277           else decrh 0 f
   278      | body' => Abs (a, T, body')) handle Same.SAME =>
   279         (case body of
   280           f $ Bound 0 =>
   281             if Term.is_dependent f then raise Same.SAME
   282             else decrh 0 f
   283         | _ => raise Same.SAME))
   284   | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
   285   | eta _ = raise Same.SAME;
   286 
   287 in
   288 
   289 fun eta_contract t =
   290   if Term.has_abs t then Same.commit eta t else t;
   291 
   292 end;
   293 
   294 val beta_eta_contract = eta_contract o beta_norm;
   295 
   296 fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
   297 
   298 
   299 fun body_type env (Type ("fun", [_, T])) = body_type env T
   300   | body_type env (T as TVar v) =
   301       (case Type.lookup (type_env env) v of
   302         NONE => T
   303       | SOME T' => body_type env T')
   304   | body_type _ T = T;
   305 
   306 fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U
   307   | binder_types env (TVar v) =
   308       (case Type.lookup (type_env env) v of
   309         NONE => []
   310       | SOME T' => binder_types env T')
   311   | binder_types _ _ = [];
   312 
   313 fun strip_type env T = (binder_types env T, body_type env T);
   314 
   315 (*finds type of term without checking that combinations are consistent
   316   Ts holds types of bound variables*)
   317 fun fastype (Envir {tyenv, ...}) =
   318   let
   319     val funerr = "fastype: expected function type";
   320     fun fast Ts (f $ u) =
   321           (case Type.devar tyenv (fast Ts f) of
   322             Type ("fun", [_, T]) => T
   323           | TVar v => raise TERM (funerr, [f $ u])
   324           | _ => raise TERM (funerr, [f $ u]))
   325       | fast Ts (Const (_, T)) = T
   326       | fast Ts (Free (_, T)) = T
   327       | fast Ts (Bound i) =
   328           (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i]))
   329       | fast Ts (Var (_, T)) = T
   330       | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
   331   in fast end;
   332 
   333 
   334 (** plain substitution -- without variable chasing **)
   335 
   336 local
   337 
   338 fun subst_type0 tyenv = Term_Subst.map_atypsT_same
   339   (fn TVar v =>
   340         (case Type.lookup tyenv v of
   341           SOME U => U
   342         | NONE => raise Same.SAME)
   343     | _ => raise Same.SAME);
   344 
   345 fun subst_term1 tenv = Term_Subst.map_aterms_same
   346   (fn Var v =>
   347         (case lookup1 tenv v of
   348           SOME u => u
   349         | NONE => raise Same.SAME)
   350     | _ => raise Same.SAME);
   351 
   352 fun subst_term2 tenv tyenv : term Same.operation =
   353   let
   354     val substT = subst_type0 tyenv;
   355     fun subst (Const (a, T)) = Const (a, substT T)
   356       | subst (Free (a, T)) = Free (a, substT T)
   357       | subst (Var (xi, T)) =
   358           (case lookup1 tenv (xi, T) of
   359             SOME u => u
   360           | NONE => Var (xi, substT T))
   361       | subst (Bound _) = raise Same.SAME
   362       | subst (Abs (a, T, t)) =
   363           (Abs (a, substT T, Same.commit subst t)
   364             handle Same.SAME => Abs (a, T, subst t))
   365       | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
   366   in subst end;
   367 
   368 in
   369 
   370 fun subst_type_same tyenv T =
   371   if Vartab.is_empty tyenv then raise Same.SAME
   372   else subst_type0 tyenv T;
   373 
   374 fun subst_term_types_same tyenv t =
   375   if Vartab.is_empty tyenv then raise Same.SAME
   376   else Term_Subst.map_types_same (subst_type0 tyenv) t;
   377 
   378 fun subst_term_same (tyenv, tenv) =
   379   if Vartab.is_empty tenv then subst_term_types_same tyenv
   380   else if Vartab.is_empty tyenv then subst_term1 tenv
   381   else subst_term2 tenv tyenv;
   382 
   383 fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
   384 fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
   385 fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
   386 
   387 end;
   388 
   389 
   390 
   391 (** expand defined atoms -- with local beta reduction **)
   392 
   393 fun expand_atom T (U, u) =
   394   subst_term_types (Type.raw_match (U, T) Vartab.empty) u
   395     handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
   396 
   397 fun expand_term get =
   398   let
   399     fun expand tm =
   400       let
   401         val (head, args) = Term.strip_comb tm;
   402         val args' = map expand args;
   403         fun comb head' = Term.list_comb (head', args');
   404       in
   405         (case head of
   406           Abs (x, T, t) => comb (Abs (x, T, expand t))
   407         | _ =>
   408           (case get head of
   409             SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
   410           | NONE => comb head))
   411       end;
   412   in expand end;
   413 
   414 fun expand_term_frees defs =
   415   let
   416     val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
   417     val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   418   in expand_term get end;
   419 
   420 end;