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