3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright Cambridge University 1992
6 Simply typed lambda-calculus: types, terms, and basic operations.
14 signature BASIC_TERM =
20 Type of string * typ list |
21 TFree of string * sort |
22 TVar of indexname * sort
23 val --> : typ * typ -> typ
24 val ---> : typ list * typ -> typ
25 val is_TVar: typ -> bool
26 val domain_type: typ -> typ
27 val range_type: typ -> typ
28 val binder_types: typ -> typ list
29 val body_type: typ -> typ
30 val strip_type: typ -> typ list * typ
32 Const of string * typ |
33 Free of string * typ |
34 Var of indexname * typ |
36 Abs of string * typ * term |
38 structure Vartab : TABLE
39 structure Termtab : TABLE
40 exception TYPE of string * typ list * term list
41 exception TERM of string * term list
42 val is_Bound: term -> bool
43 val is_Const: term -> bool
44 val is_Free: term -> bool
45 val is_Var: term -> bool
46 val dest_Type: typ -> string * typ list
47 val dest_Const: term -> string * typ
48 val dest_Free: term -> string * typ
49 val dest_Var: term -> indexname * typ
50 val type_of: term -> typ
51 val type_of1: typ list * term -> typ
52 val fastype_of: term -> typ
53 val fastype_of1: typ list * term -> typ
54 val list_abs: (string * typ) list * term -> term
55 val strip_abs_body: term -> term
56 val strip_abs_vars: term -> (string * typ) list
57 val strip_qnt_body: string -> term -> term
58 val strip_qnt_vars: string -> term -> (string * typ) list
59 val list_comb: term * term list -> term
60 val strip_comb: term -> term * term list
61 val head_of: term -> term
62 val size_of_term: term -> int
63 val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
64 val map_type_tfree: (string * sort -> typ) -> typ -> typ
65 val map_term_types: (typ -> typ) -> term -> term
66 val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
67 val map_typ: (class -> class) -> (string -> string) -> typ -> typ
70 (string -> string) -> (string -> string) -> term -> term
71 val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
72 val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
73 val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
74 val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
75 val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
79 val itselfT: typ -> typ
84 val equals: typ -> term
85 val flexpair: typ -> term
86 val strip_all_body: term -> term
87 val strip_all_vars: term -> (string * typ) list
88 val incr_bv: int * int * term -> term
89 val incr_boundvars: int -> term -> term
90 val add_loose_bnos: term * int * int list -> int list
91 val loose_bnos: term -> int list
92 val loose_bvar: term * int -> bool
93 val loose_bvar1: term * int -> bool
94 val subst_bounds: term list * term -> term
95 val subst_bound: term * term -> term
96 val subst_TVars: (indexname * typ) list -> term -> term
97 val subst_TVars_Vartab: typ Vartab.table -> term -> term
98 val betapply: term * term -> term
99 val eq_ix: indexname * indexname -> bool
100 val ins_ix: indexname * indexname list -> indexname list
101 val mem_ix: indexname * indexname list -> bool
102 val eq_sort: sort * class list -> bool
103 val mem_sort: sort * class list list -> bool
104 val subset_sort: sort list * class list list -> bool
105 val eq_set_sort: sort list * sort list -> bool
106 val ins_sort: sort * class list list -> class list list
107 val union_sort: sort list * sort list -> sort list
108 val rems_sort: sort list * sort list -> sort list
109 val aconv: term * term -> bool
110 val aconvs: term list * term list -> bool
111 val mem_term: term * term list -> bool
112 val subset_term: term list * term list -> bool
113 val eq_set_term: term list * term list -> bool
114 val ins_term: term * term list -> term list
115 val union_term: term list * term list -> term list
116 val inter_term: term list * term list -> term list
117 val could_unify: term * term -> bool
118 val subst_free: (term * term) list -> term -> term
119 val subst_atomic: (term * term) list -> term -> term
120 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
121 val typ_subst_TVars: (indexname * typ) list -> typ -> typ
122 val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
123 val subst_Vars: (indexname * term) list -> term -> term
124 val incr_tvar: int -> typ -> typ
125 val xless: (string * int) * indexname -> bool
126 val atless: term * term -> bool
127 val insert_aterm: term * term list -> term list
128 val abstract_over: term * term -> term
129 val lambda: term -> term -> term
130 val absfree: string * typ * term -> term
131 val list_abs_free: (string * typ) list * term -> term
132 val list_all_free: (string * typ) list * term -> term
133 val list_all: (string * typ) list * term -> term
134 val maxidx_of_typ: typ -> int
135 val maxidx_of_typs: typ list -> int
136 val maxidx_of_term: term -> int
137 val read_radixint: int * string list -> int * string list
138 val read_int: string list -> int * string list
139 val oct_char: string -> string
140 val variant: string list -> string -> string
141 val variantlist: string list * string list -> string list
142 val variant_abs: string * typ * term -> string * term
143 val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
144 val add_new_id: string list * string -> string list
145 val add_typ_classes: typ * class list -> class list
146 val add_typ_ixns: indexname list * typ -> indexname list
147 val add_typ_tfree_names: typ * string list -> string list
148 val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
149 val typ_tfrees: typ -> (string * sort) list
150 val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
151 val typ_tvars: typ -> (indexname * sort) list
152 val add_typ_tycons: typ * string list -> string list
153 val add_typ_varnames: typ * string list -> string list
154 val add_term_classes: term * class list -> class list
155 val add_term_consts: term * string list -> string list
156 val add_term_frees: term * term list -> term list
157 val term_frees: term -> term list
158 val add_term_free_names: term * string list -> string list
159 val add_term_names: term * string list -> string list
160 val add_term_tfree_names: term * string list -> string list
161 val add_term_tfrees: term * (string * sort) list -> (string * sort) list
162 val term_tfrees: term -> (string * sort) list
163 val add_term_tvar_ixns: term * indexname list -> indexname list
164 val add_term_tvarnames: term * string list -> string list
165 val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
166 val term_tvars: term -> (indexname * sort) list
167 val add_term_tycons: term * string list -> string list
168 val add_term_vars: term * term list -> term list
169 val term_vars: term -> term list
170 val exists_Const: (string * typ -> bool) -> term -> bool
171 val exists_subterm: (term -> bool) -> term -> bool
172 val compress_type: typ -> typ
173 val compress_term: term -> term
179 val invent_names: string list -> string -> int -> string list
180 val invent_type_names: string list -> int -> string list
181 val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
182 val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
183 val add_vars: (indexname * typ) list * term -> (indexname * typ) list
184 val add_frees: (string * typ) list * term -> (string * typ) list
185 val indexname_ord: indexname * indexname -> order
186 val typ_ord: typ * typ -> order
187 val typs_ord: typ list * typ list -> order
188 val term_ord: term * term -> order
189 val terms_ord: term list * term list -> order
190 val termless: term * term -> bool
191 val dummy_patternN: string
192 val no_dummy_patterns: term -> term
193 val replace_dummy_patterns: int * term -> int * term
194 val is_replaced_dummy_pattern: indexname -> bool
197 structure Term: TERM =
200 (*Indexnames can be quickly renamed by adding an offset to the integer part,
202 type indexname = string*int;
204 (* Types are classified by sorts. *)
206 type sort = class list;
208 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
209 datatype typ = Type of string * typ list
210 | TFree of string * sort
211 | TVar of indexname * sort;
213 (*Terms. Bound variables are indicated by depth number.
214 Free variables, (scheme) variables and constants have names.
215 An term is "closed" if every bound variable of level "lev"
216 is enclosed by at least "lev" abstractions.
218 It is possible to create meaningless terms containing loose bound vars
219 or type mismatches. But such terms are not allowed in rules. *)
224 Const of string * typ
225 | Free of string * typ
226 | Var of indexname * typ
228 | Abs of string*typ*term
232 (*For errors involving type mismatches*)
233 exception TYPE of string * typ list * term list;
235 (*For system errors involving terms*)
236 exception TERM of string * term list;
239 (*Note variable naming conventions!
241 f,g,h: functions (including terms of function type)
246 A,B,C: term (denoting formulae)
253 fun S --> T = Type("fun",[S,T]);
255 (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*)
256 val op ---> = foldr (op -->);
258 fun dest_Type (Type x) = x
259 | dest_Type T = raise TYPE ("dest_Type", [T], []);
262 (** Discriminators **)
264 fun is_Bound (Bound _) = true
265 | is_Bound _ = false;
267 fun is_Const (Const _) = true
268 | is_Const _ = false;
270 fun is_Free (Free _) = true
273 fun is_Var (Var _) = true
276 fun is_TVar (TVar _) = true
281 fun dest_Const (Const x) = x
282 | dest_Const t = raise TERM("dest_Const", [t]);
284 fun dest_Free (Free x) = x
285 | dest_Free t = raise TERM("dest_Free", [t]);
287 fun dest_Var (Var x) = x
288 | dest_Var t = raise TERM("dest_Var", [t]);
291 fun domain_type (Type("fun", [T,_])) = T
292 and range_type (Type("fun", [_,T])) = T;
294 (* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*)
295 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
296 | binder_types _ = [];
298 (* maps [T1,...,Tn]--->T to T*)
299 fun body_type (Type("fun",[S,T])) = body_type T
302 (* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
303 fun strip_type T : typ list * typ =
304 (binder_types T, body_type T);
307 (*Compute the type of the term, checking that combinations are well-typed
308 Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
309 fun type_of1 (Ts, Const (_,T)) = T
310 | type_of1 (Ts, Free (_,T)) = T
311 | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)
312 handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
313 | type_of1 (Ts, Var (_,T)) = T
314 | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
315 | type_of1 (Ts, f$u) =
316 let val U = type_of1(Ts,u)
317 and T = type_of1(Ts,f)
319 Type("fun",[T1,T2]) =>
320 if T1=U then T2 else raise TYPE
321 ("type_of: type mismatch in application", [T1,U], [f$u])
323 ("type_of: function type is expected in application",
327 fun type_of t : typ = type_of1 ([],t);
329 (*Determines the type of a term, with minimal checking*)
330 fun fastype_of1 (Ts, f$u) =
331 (case fastype_of1 (Ts,f) of
332 Type("fun",[_,T]) => T
333 | _ => raise TERM("fastype_of: expected function type", [f$u]))
334 | fastype_of1 (_, Const (_,T)) = T
335 | fastype_of1 (_, Free (_,T)) = T
336 | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
337 handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
338 | fastype_of1 (_, Var (_,T)) = T
339 | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
341 fun fastype_of t : typ = fastype_of1 ([],t);
344 val list_abs = foldr (fn ((x, T), t) => Abs (x, T, t));
346 (* maps (x1,...,xn)t to t *)
347 fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t
348 | strip_abs_body u = u;
350 (* maps (x1,...,xn)t to [x1, ..., xn] *)
351 fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t
352 | strip_abs_vars u = [] : (string*typ) list;
355 fun strip_qnt_body qnt =
356 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
360 fun strip_qnt_vars qnt =
361 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
362 | strip t = [] : (string*typ) list
366 (* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
367 val list_comb : term * term list -> term = foldl (op $);
370 (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
371 fun strip_comb u : term * term list =
372 let fun stripc (f$t, ts) = stripc (f, t::ts)
377 (* maps f(t1,...,tn) to f , which is never a combination *)
378 fun head_of (f$t) = head_of f
382 (*Number of atoms and abstractions in a term*)
383 fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
384 | size_of_term (f$t) = size_of_term f + size_of_term t
385 | size_of_term _ = 1;
387 fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
388 | map_type_tvar f (T as TFree _) = T
389 | map_type_tvar f (TVar x) = f x;
391 fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
392 | map_type_tfree f (TFree x) = f x
393 | map_type_tfree f (T as TVar _) = T;
395 (* apply a function to all types in a term *)
396 fun map_term_types f =
397 let fun map(Const(a,T)) = Const(a, f T)
398 | map(Free(a,T)) = Free(a, f T)
399 | map(Var(v,T)) = Var(v, f T)
400 | map(t as Bound _) = t
401 | map(Abs(a,T,t)) = Abs(a, f T, map t)
402 | map(f$t) = map f $ map t;
405 (* iterate a function over all types in a term *)
406 fun it_term_types f =
407 let fun iter(Const(_,T), a) = f(T,a)
408 | iter(Free(_,T), a) = f(T,a)
409 | iter(Var(_,T), a) = f(T,a)
410 | iter(Abs(_,T,t), a) = iter(t,f(T,a))
411 | iter(f$u, a) = iter(f, iter(u, a))
412 | iter(Bound _, a) = a
416 (** Connectives of higher order logic **)
418 val logicC: class = "logic";
419 val logicS: sort = [logicC];
421 fun itselfT ty = Type ("itself", [ty]);
422 val a_itselfT = itselfT (TFree ("'a", logicS));
424 val propT : typ = Type("prop",[]);
426 val implies = Const("==>", propT-->propT-->propT);
428 fun all T = Const("all", (T-->propT)-->propT);
430 fun equals T = Const("==", T-->T-->propT);
432 fun flexpair T = Const("=?=", T-->T-->propT);
434 (* maps !!x1...xn. t to t *)
435 fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
436 | strip_all_body t = t;
438 (* maps !!x1...xn. t to [x1, ..., xn] *)
439 fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
440 (a,T) :: strip_all_vars t
441 | strip_all_vars t = [] : (string*typ) list;
443 (*increments a term's non-local bound variables
444 required when moving a term within abstractions
445 inc is increment for bound variables
446 lev is level at which a bound variable is considered 'loose'*)
447 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
448 | incr_bv (inc, lev, Abs(a,T,body)) =
449 Abs(a, T, incr_bv(inc,lev+1,body))
450 | incr_bv (inc, lev, f$t) =
451 incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
452 | incr_bv (inc, lev, u) = u;
454 fun incr_boundvars 0 t = t
455 | incr_boundvars inc t = incr_bv(inc,0,t);
458 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
459 (Bound 0) is loose at level 0 *)
460 fun add_loose_bnos (Bound i, lev, js) =
461 if i<lev then js else (i-lev) ins_int js
462 | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
463 | add_loose_bnos (f$t, lev, js) =
464 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
465 | add_loose_bnos (_, _, js) = js;
467 fun loose_bnos t = add_loose_bnos (t, 0, []);
469 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
470 level k or beyond. *)
471 fun loose_bvar(Bound i,k) = i >= k
472 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
473 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
474 | loose_bvar _ = false;
476 fun loose_bvar1(Bound i,k) = i = k
477 | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
478 | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
479 | loose_bvar1 _ = false;
481 (*Substitute arguments for loose bound variables.
482 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
483 Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
484 and the appropriate call is subst_bounds([b,a], c) .
485 Loose bound variables >=n are reduced by "n" to
486 compensate for the disappearance of lambdas.
488 fun subst_bounds (args: term list, t) : term =
489 let val n = length args;
490 fun subst (t as Bound i, lev) =
491 (if i<lev then t (*var is locally bound*)
492 else incr_boundvars lev (List.nth(args, i-lev))
493 handle Subscript => Bound(i-n) (*loose: change it*))
494 | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
495 | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
497 in case args of [] => t | _ => subst (t,0) end;
499 (*Special case: one argument*)
500 fun subst_bound (arg, t) : term =
501 let fun subst (t as Bound i, lev) =
502 if i<lev then t (*var is locally bound*)
503 else if i=lev then incr_boundvars lev arg
504 else Bound(i-1) (*loose: change it*)
505 | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
506 | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
510 (*beta-reduce if possible, else form application*)
511 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
512 | betapply (f,u) = f$u;
514 (** Equality, membership and insertion of indexnames (string*ints) **)
516 (*optimized equality test for indexnames. Yields a huge gain under Poly/ML*)
517 fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
519 (*membership in a list, optimized version for indexnames*)
520 fun mem_ix (_, []) = false
521 | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
523 (*insertion into list, optimized version for indexnames*)
524 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
526 (*Tests whether 2 terms are alpha-convertible and have same type.
527 Note that constants may have more than one type.*)
528 fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U
529 | (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U
530 | (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U
531 | (Bound i) aconv (Bound j) = i=j
532 | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U
533 | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
536 (** Membership, insertion, union for terms **)
538 fun mem_term (_, []) = false
539 | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
541 fun subset_term ([], ys) = true
542 | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
544 fun eq_set_term (xs, ys) =
545 xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
547 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
549 fun union_term (xs, []) = xs
550 | union_term ([], ys) = ys
551 | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
553 fun inter_term ([], ys) = []
554 | inter_term (x::xs, ys) =
555 if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
557 (** Equality, membership and insertion of sorts (string lists) **)
559 fun eq_sort ([]:sort, []) = true
560 | eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts)
561 | eq_sort (_, _) = false;
563 fun mem_sort (_:sort, []) = false
564 | mem_sort (S, S'::Ss) = eq_sort (S, S') orelse mem_sort(S,Ss);
566 fun ins_sort(S,Ss) = if mem_sort(S,Ss) then Ss else S :: Ss;
568 fun union_sort (xs, []) = xs
569 | union_sort ([], ys) = ys
570 | union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
572 fun subset_sort ([], ys) = true
573 | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
575 fun eq_set_sort (xs, ys) =
576 xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
578 val rems_sort = gen_rems eq_sort;
580 (*are two term lists alpha-convertible in corresponding elements?*)
581 fun aconvs ([],[]) = true
582 | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
585 (*A fast unification filter: true unless the two terms cannot be unified.
586 Terms must be NORMAL. Treats all Vars as distinct. *)
587 fun could_unify (t,u) =
588 let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)
589 | matchrands _ = true
590 in case (head_of t , head_of u) of
593 | (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)
594 | (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)
595 | (Bound i, Bound j) => i=j andalso matchrands(t,u)
596 | (Abs _, _) => true (*because of possible eta equality*)
601 (*Substitute new for free occurrences of old in a term*)
602 fun subst_free [] = (fn t=>t)
605 case gen_assoc (op aconv) (pairs, u) of
607 | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
608 | t$u' => substf t $ substf u'
612 (*a total, irreflexive ordering on index names*)
613 fun xless ((a,i), (b,j): indexname) = i<j orelse (i=j andalso a<b);
616 (*Abstraction of the term "body" over its occurrences of v,
617 which must contain no loose bound variables.
618 The resulting term is ready to become the body of an Abs.*)
619 fun abstract_over (v,body) =
620 let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
622 Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
623 | f$rand => abst(lev,f) $ abst(lev,rand)
628 let val (x, T) = dest_Free v
629 in Abs (x, T, abstract_over (v, t)) end;
631 (*Form an abstraction over a free variable.*)
632 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
634 (*Abstraction over a list of free variables*)
635 fun list_abs_free ([ ] , t) = t
636 | list_abs_free ((a,T)::vars, t) =
637 absfree(a, T, list_abs_free(vars,t));
639 (*Quantification over a list of free variables*)
640 fun list_all_free ([], t: term) = t
641 | list_all_free ((a,T)::vars, t) =
642 (all T) $ (absfree(a, T, list_all_free(vars,t)));
644 (*Quantification over a list of variables (already bound in body) *)
645 fun list_all ([], t) = t
646 | list_all ((a,T)::vars, t) =
647 (all T) $ (Abs(a, T, list_all(vars,t)));
649 (*Replace the ATOMIC term ti by ui; instl = [(t1,u1), ..., (tn,un)].
650 A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
651 fun subst_atomic [] t = t : term
652 | subst_atomic (instl: (term*term) list) t =
653 let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
654 | subst (f$t') = subst f $ subst t'
655 | subst t = if_none (assoc(instl,t)) t
658 (*Substitute for type Vars in a type*)
659 fun typ_subst_TVars iTs T = if null iTs then T else
660 let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
661 | subst(T as TFree _) = T
662 | subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T
665 (*Substitute for type Vars in a term*)
666 val subst_TVars = map_term_types o typ_subst_TVars;
668 (*Substitute for Vars in a term; see also envir/norm_term*)
669 fun subst_Vars itms t = if null itms then t else
670 let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v
671 | subst(Abs(a,T,t)) = Abs(a,T,subst t)
672 | subst(f$t) = subst f $ subst t
676 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
677 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
678 let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
679 | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
680 | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
681 None => Var(ixn,typ_subst_TVars iTs T)
683 | subst(b as Bound _) = b
684 | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
685 | subst(f$t) = subst f $ subst t
689 (*Computing the maximum index of a typ*)
690 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
691 | maxidx_of_typ(TFree _) = ~1
692 | maxidx_of_typ(TVar((_,i),_)) = i
693 and maxidx_of_typs [] = ~1
694 | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
697 (*Computing the maximum index of a term*)
698 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
699 | maxidx_of_term (Bound _) = ~1
700 | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
701 | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
702 | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
703 | maxidx_of_term (f$t) = Int.max(maxidx_of_term f, maxidx_of_term t);
706 (* Increment the index of all Poly's in T by k *)
707 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
710 (**** Syntax-related declarations ****)
713 (*Dummy type for parsing and printing. Will be replaced during type inference. *)
714 val dummyT = Type("dummy",[]);
716 (*read a numeral of the given radix, normally 10*)
717 fun read_radixint (radix: int, cs) : int * string list =
718 let val zero = ord"0"
719 val limit = zero+radix
720 fun scan (num,[]) = (num,[])
721 | scan (num, c::cs) =
722 if zero <= ord c andalso ord c < limit
723 then scan(radix*num + ord c - zero, cs)
727 fun read_int cs = read_radixint (10, cs);
729 fun octal s = #1 (read_radixint (8, explode s));
730 val oct_char = chr o octal;
735 (*Makes a variant of the name c distinct from the names in bs.
736 First attaches the suffix "a" and then increments this;
737 preserves a suffix of underscores "_". *)
738 fun variant bs name =
740 val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
741 fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
742 fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c;
743 in vary1 (if c = "" then "u" else c) ^ u end;
745 (*Create variants of the list of names, with priority to the first ones*)
746 fun variantlist ([], used) = []
747 | variantlist(b::bs, used) =
748 let val b' = variant used b
749 in b' :: variantlist (bs, b'::used) end;
751 fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used);
752 fun invent_type_names used = invent_names used "'";
758 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs)
759 | add_typ_classes (TFree (_, S), cs) = S union cs
760 | add_typ_classes (TVar (_, S), cs) = S union cs;
762 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (Ts, c ins cs)
763 | add_typ_tycons (_, cs) = cs;
765 val add_term_classes = it_term_types add_typ_classes;
766 val add_term_tycons = it_term_types add_typ_tycons;
768 fun add_term_consts (Const (c, _), cs) = c ins_string cs
769 | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
770 | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
771 | add_term_consts (_, cs) = cs;
773 fun exists_Const P t = let
774 fun ex (Const c ) = P c
775 | ex (t $ u ) = ex t orelse ex u
776 | ex (Abs (_, _, t)) = ex t
780 fun exists_subterm P =
781 let fun ex t = P t orelse
783 u $ v => ex u orelse ex v
784 | Abs(_, _, u) => ex u
788 (*map classes, tycons*)
789 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
790 | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
791 | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
793 (*map classes, tycons, consts*)
794 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
795 | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
796 | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
797 | map_term _ _ _ (t as Bound _) = t
798 | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
799 | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
803 (** TFrees and TVars **)
805 (*maps (bs,v) to v'::bs this reverses the identifiers bs*)
806 fun add_new_id (bs, c) : string list = variant bs c :: bs;
808 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
809 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
810 | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
811 | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
812 | add_term_free_names (_, bs) = bs;
814 (*Accumulates the names in the term, suppressing duplicates.
815 Includes Frees and Consts. For choosing unambiguous bound var names.*)
816 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
817 | add_term_names (Free(a,_), bs) = a ins_string bs
818 | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
819 | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
820 | add_term_names (_, bs) = bs;
822 (*Accumulates the TVars in a type, suppressing duplicates. *)
823 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)
824 | add_typ_tvars(TFree(_),vs) = vs
825 | add_typ_tvars(TVar(v),vs) = v ins vs;
827 (*Accumulates the TFrees in a type, suppressing duplicates. *)
828 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)
829 | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
830 | add_typ_tfree_names(TVar(_),fs) = fs;
832 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)
833 | add_typ_tfrees(TFree(f),fs) = f ins fs
834 | add_typ_tfrees(TVar(_),fs) = fs;
836 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms)
837 | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
838 | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
840 (*Accumulates the TVars in a term, suppressing duplicates. *)
841 val add_term_tvars = it_term_types add_typ_tvars;
843 (*Accumulates the TFrees in a term, suppressing duplicates. *)
844 val add_term_tfrees = it_term_types add_typ_tfrees;
845 val add_term_tfree_names = it_term_types add_typ_tfree_names;
847 val add_term_tvarnames = it_term_types add_typ_varnames;
849 (*Non-list versions*)
850 fun typ_tfrees T = add_typ_tfrees(T,[]);
851 fun typ_tvars T = add_typ_tvars(T,[]);
852 fun term_tfrees t = add_term_tfrees(t,[]);
853 fun term_tvars t = add_term_tvars(t,[]);
855 (*special code to enforce left-to-right collection of TVar-indexnames*)
857 fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
858 | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
860 | add_typ_ixns(ixns,TFree(_)) = ixns;
862 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
863 | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
864 | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
865 | add_term_tvar_ixns(Bound _,ixns) = ixns
866 | add_term_tvar_ixns(Abs(_,T,t),ixns) =
867 add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
868 | add_term_tvar_ixns(f$t,ixns) =
869 add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
871 (** Frees and Vars **)
873 (*a partial ordering (not reflexive) for atomic terms*)
874 fun atless (Const (a,_), Const (b,_)) = a<b
875 | atless (Free (a,_), Free (b,_)) = a<b
876 | atless (Var(v,_), Var(w,_)) = xless(v,w)
877 | atless (Bound i, Bound j) = i<j
880 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
881 fun insert_aterm (t,us) =
882 let fun inserta [] = [t]
883 | inserta (us as u::us') =
884 if atless(t,u) then t::us
885 else if t=u then us (*duplicate*)
886 else u :: inserta(us')
889 (*Accumulates the Vars in the term, suppressing duplicates*)
890 fun add_term_vars (t, vars: term list) = case t of
891 Var _ => insert_aterm(t,vars)
892 | Abs (_,_,body) => add_term_vars(body,vars)
893 | f$t => add_term_vars (f, add_term_vars(t, vars))
896 fun term_vars t = add_term_vars(t,[]);
898 (*Accumulates the Frees in the term, suppressing duplicates*)
899 fun add_term_frees (t, frees: term list) = case t of
900 Free _ => insert_aterm(t,frees)
901 | Abs (_,_,body) => add_term_frees(body,frees)
902 | f$t => add_term_frees (f, add_term_frees(t, frees))
905 fun term_frees t = add_term_frees(t,[]);
907 (*Given an abstraction over P, replaces the bound variable by a Free variable
908 having a unique name. *)
909 fun variant_abs (a,T,P) =
910 let val b = variant (add_term_names(P,[])) a
911 in (b, subst_bound (Free(b,T), P)) end;
913 (* renames and reverses the strings in vars away from names *)
914 fun rename_aTs names vars : (string*typ)list =
915 let fun rename_aT (vars,(a,T)) =
916 (variant (map #1 vars @ names) a, T) :: vars
917 in foldl rename_aT ([],vars) end;
919 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
922 (* left-ro-right traversal *)
924 (*foldl atoms of type*)
925 fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts)
926 | foldl_atyps f x_atom = f x_atom;
928 (*foldl atoms of term*)
929 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
930 | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
931 | foldl_aterms f x_atom = f x_atom;
933 fun foldl_map_aterms f (x, t $ u) =
934 let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
935 in (x'', t' $ u') end
936 | foldl_map_aterms f (x, Abs (a, T, t)) =
937 let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
938 | foldl_map_aterms f x_atom = f x_atom;
940 (*foldl types of term*)
941 fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
942 | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
943 | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
944 | foldl_term_types f (x, Bound _) = x
945 | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
946 | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
948 fun foldl_types f = foldl_term_types (fn _ => f);
950 (*collect variables*)
951 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
952 val add_tvars = foldl_types add_tvarsT;
953 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
954 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
958 (** type and term orders **)
960 fun indexname_ord ((x, i), (y, j)) =
961 (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
966 (*assumes that TFrees / TVars with the same name have same sorts*)
967 fun typ_ord (Type (a, Ts), Type (b, Us)) =
968 (case string_ord (a, b) of EQUAL => typs_ord (Ts, Us) | ord => ord)
969 | typ_ord (Type _, _) = GREATER
970 | typ_ord (TFree _, Type _) = LESS
971 | typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b)
972 | typ_ord (TFree _, TVar _) = GREATER
973 | typ_ord (TVar _, Type _) = LESS
974 | typ_ord (TVar _, TFree _) = LESS
975 | typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj)
976 and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
981 (*a linear well-founded AC-compatible ordering for terms:
982 s < t <=> 1. size(s) < size(t) or
983 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
984 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
985 (s1..sn) < (t1..tn) (lexicographically)*)
987 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
988 | dest_hd (Free (a, T)) = (((a, 0), T), 1)
989 | dest_hd (Var v) = (v, 2)
990 | dest_hd (Bound i) = ((("", i), dummyT), 3)
991 | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
993 fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
994 (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
996 (case int_ord (size_of_term t, size_of_term u) of
998 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
999 (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
1003 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
1004 and terms_ord (ts, us) = list_ord term_ord (ts, us);
1006 fun termless tu = (term_ord tu = LESS);
1008 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
1009 structure Termtab = TableFun(type key = term val ord = term_ord);
1011 (*Substitute for type Vars in a type, version using Vartab*)
1012 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
1013 let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
1014 | subst(T as TFree _) = T
1015 | subst(T as TVar(ixn, _)) =
1016 (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U)
1019 (*Substitute for type Vars in a term, version using Vartab*)
1020 val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
1023 (*** Compression of terms and types by sharing common subtrees.
1024 Saves 50-75% on storage requirements. As it is fairly slow,
1025 it is called only for axioms, stored theorems, etc. ***)
1027 (** Sharing of types **)
1029 fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match
1030 | atomic_tag (TFree (a,_)) = a
1031 | atomic_tag (TVar ((a,_),_)) = a;
1033 fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
1034 | type_tag T = atomic_tag T;
1036 val memo_types = ref (Symtab.empty : typ list Symtab.table);
1038 (* special case of library/find_first *)
1039 fun find_type (T, []: typ list) = None
1040 | find_type (T, T'::Ts) =
1041 if T=T' then Some T'
1042 else find_type (T, Ts);
1044 fun compress_type T =
1045 let val tag = type_tag T
1046 val tylist = Symtab.lookup_multi (!memo_types, tag)
1048 case find_type (T,tylist) of
1053 Type (a,Ts) => Type (a, map compress_type Ts)
1055 in memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
1060 let val Type (a,Ts) = T
1061 in Type (a, map compress_type Ts) end;
1063 (** Sharing of atomic terms **)
1065 val memo_terms = ref (Symtab.empty : term list Symtab.table);
1067 (* special case of library/find_first *)
1068 fun find_term (t, []: term list) = None
1069 | find_term (t, t'::ts) =
1070 if t=t' then Some t'
1071 else find_term (t, ts);
1073 fun const_tag (Const (a,_)) = a
1074 | const_tag (Free (a,_)) = a
1075 | const_tag (Var ((a,i),_)) = a
1076 | const_tag (t as Bound _) = ".B.";
1078 fun share_term (t $ u) = share_term t $ share_term u
1079 | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
1081 let val tag = const_tag t
1082 val ts = Symtab.lookup_multi (!memo_terms, tag)
1084 case find_term (t,ts) of
1086 | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
1090 val compress_term = share_term o map_term_types compress_type;
1093 (* dummy patterns *)
1095 val dummy_patternN = "dummy_pattern";
1097 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
1098 | is_dummy_pattern _ = false;
1100 fun no_dummy_patterns tm =
1101 if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
1102 else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
1104 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
1105 (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
1106 | replace_dummy Ts (i, Abs (x, T, t)) =
1107 let val (i', t') = replace_dummy (T :: Ts) (i, t)
1108 in (i', Abs (x, T, t')) end
1109 | replace_dummy Ts (i, t $ u) =
1110 let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
1111 in (i'', t' $ u') end
1112 | replace_dummy _ (i, a) = (i, a);
1114 val replace_dummy_patterns = replace_dummy [];
1116 fun is_replaced_dummy_pattern ("_dummy_", _) = true
1117 | is_replaced_dummy_pattern _ = false;
1122 structure BasicTerm: BASIC_TERM = Term;