1(*  Title:      Pure/envir.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3
4Free-form environments.  The type of a term variable / sort of a type variable is
5part of its name.  The lookup function must apply type substitutions,
6since they may change the identity of a variable.
7*)
8
9signature ENVIR =
10sig
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
52end;
53
54structure Envir: ENVIR =
55struct
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
64type tenv = (typ * term) Vartab.table;
65
66datatype 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
71fun make_env (maxidx, tenv, tyenv) =
72  Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
73
74fun maxidx_of (Envir {maxidx, ...}) = maxidx;
75fun term_env (Envir {tenv, ...}) = tenv;
76fun type_env (Envir {tyenv, ...}) = tyenv;
77
78fun is_empty env =
79  Vartab.is_empty (term_env env) andalso
80  Vartab.is_empty (type_env env);
81
82
83(* build env *)
84
85fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
86val init = empty ~1;
87
88fun 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!? *)
97val 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. *)
101fun 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.*)
111fun genvar name (env, T) : env * term =
112  let val (env', [v]) = genvars name (env, [T])
113  in (env', v) end;
114
115fun var_clash xi T T' =
116  raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]);
117
118fun 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.*)
127fun lookup1 tenv = lookup_check (op =) tenv;
128
129fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv;
130
131fun 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*)
135fun 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*)
140fun 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
158local
159
160fun 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
170fun 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
186fun 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
207in
208
209fun norm_type_same tyenv T =
210  if Vartab.is_empty tyenv then raise Same.SAME
211  else norm_type0 tyenv T;
212
213fun norm_types_same tyenv Ts =
214  if Vartab.is_empty tyenv then raise Same.SAME
215  else Same.map (norm_type0 tyenv) Ts;
216
217fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
218
219fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
220  if Vartab.is_empty tyenv then norm_term1 tenv
221  else norm_term2 envir;
222
223fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
224
225fun beta_norm t =
226  if Term.could_beta_contract t then norm_term init t else t;
227
228end;
229
230
231(* head normal form for unification *)
232
233fun 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
251fun 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
269local
270
271fun 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
275and decrh lev t = (decr lev t handle Same.SAME => t);
276
277fun 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
291in
292
293fun eta_contract t =
294  if Term.could_eta_contract t then Same.commit eta t else t;
295
296end;
297
298val beta_eta_contract = eta_contract o beta_norm;
299
300fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
301
302
303fun 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
310fun 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
317fun 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*)
321fun 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
340local
341
342fun 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
349fun 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
356fun 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
372in
373
374fun subst_type_same tyenv T =
375  if Vartab.is_empty tyenv then raise Same.SAME
376  else subst_type0 tyenv T;
377
378fun 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
382fun 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
387fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
388fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
389fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
390
391end;
392
393
394
395(** expand defined atoms -- with local beta reduction **)
396
397fun 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
401fun 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
418fun 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
424end;
425