2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5 Simply typed lambda-calculus: types, terms, and basic operations.
13 signature BASIC_TERM =
15 type indexname = string * int
17 type sort = class list
18 type arity = string * sort list * sort
20 Type of string * typ list |
21 TFree of string * sort |
22 TVar of indexname * sort
24 Const of string * typ |
25 Free of string * typ |
26 Var of indexname * typ |
28 Abs of string * typ * term |
30 exception TYPE of string * typ list * term list
31 exception TERM of string * term list
34 val no_dummyT: typ -> typ
35 val --> : typ * typ -> typ
36 val ---> : typ list * typ -> typ
37 val dest_Type: typ -> string * typ list
38 val dest_TVar: typ -> indexname * sort
39 val dest_TFree: typ -> string * sort
40 val is_Bound: term -> bool
41 val is_Const: term -> bool
42 val is_Free: term -> bool
43 val is_Var: term -> bool
44 val is_TVar: typ -> bool
45 val dest_Const: term -> string * typ
46 val dest_Free: term -> string * typ
47 val dest_Var: term -> indexname * typ
48 val dest_comb: term -> term * term
49 val domain_type: typ -> typ
50 val range_type: typ -> typ
51 val dest_funT: typ -> typ * typ
52 val binder_types: typ -> typ list
53 val body_type: typ -> typ
54 val strip_type: typ -> typ list * typ
55 val type_of1: typ list * term -> typ
56 val type_of: term -> typ
57 val fastype_of1: typ list * term -> typ
58 val fastype_of: term -> typ
59 val list_abs: (string * typ) list * term -> term
60 val strip_abs: term -> (string * typ) list * term
61 val strip_abs_body: term -> term
62 val strip_abs_vars: term -> (string * typ) list
63 val strip_qnt_body: string -> term -> term
64 val strip_qnt_vars: string -> term -> (string * typ) list
65 val list_comb: term * term list -> term
66 val strip_comb: term -> term * term list
67 val head_of: term -> term
68 val size_of_term: term -> int
69 val size_of_typ: typ -> int
70 val map_atyps: (typ -> typ) -> typ -> typ
71 val map_aterms: (term -> term) -> term -> term
72 val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
73 val map_type_tfree: (string * sort -> typ) -> typ -> typ
74 val map_types: (typ -> typ) -> term -> term
75 val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
76 val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
77 val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
78 val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
79 val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
80 val burrow_types: (typ list -> typ list) -> term list -> term list
81 val aconv: term * term -> bool
83 val strip_all_body: term -> term
84 val strip_all_vars: term -> (string * typ) list
85 val incr_bv: int * int * term -> term
86 val incr_boundvars: int -> term -> term
87 val add_loose_bnos: term * int * int list -> int list
88 val loose_bnos: term -> int list
89 val loose_bvar: term * int -> bool
90 val loose_bvar1: term * int -> bool
91 val subst_bounds: term list * term -> term
92 val subst_bound: term * term -> term
93 val betapply: term * term -> term
94 val betapplys: term * term list -> term
95 val subst_free: (term * term) list -> term -> term
96 val abstract_over: term * term -> term
97 val lambda: term -> term -> term
98 val absfree: string * typ * term -> term
99 val absdummy: typ * term -> term
100 val list_abs_free: (string * typ) list * term -> term
101 val list_all_free: (string * typ) list * term -> term
102 val list_all: (string * typ) list * term -> term
103 val subst_atomic: (term * term) list -> term -> term
104 val typ_subst_atomic: (typ * typ) list -> typ -> typ
105 val subst_atomic_types: (typ * typ) list -> term -> term
106 val typ_subst_TVars: (indexname * typ) list -> typ -> typ
107 val subst_TVars: (indexname * typ) list -> term -> term
108 val subst_Vars: (indexname * term) list -> term -> term
109 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
110 val is_first_order: string list -> term -> bool
111 val maxidx_of_typ: typ -> int
112 val maxidx_of_typs: typ list -> int
113 val maxidx_of_term: term -> int
114 val exists_subtype: (typ -> bool) -> typ -> bool
115 val exists_type: (typ -> bool) -> term -> bool
116 val exists_subterm: (term -> bool) -> term -> bool
117 val exists_Const: (string * typ -> bool) -> term -> bool
124 val itselfT: typ -> typ
127 val argument_type_of: term -> int -> typ
128 val add_tvar_namesT: typ -> indexname list -> indexname list
129 val add_tvar_names: term -> indexname list -> indexname list
130 val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
131 val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
132 val add_var_names: term -> indexname list -> indexname list
133 val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
134 val add_tfree_namesT: typ -> string list -> string list
135 val add_tfree_names: term -> string list -> string list
136 val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
137 val add_tfrees: term -> (string * sort) list -> (string * sort) list
138 val add_free_names: term -> string list -> string list
139 val add_frees: term -> (string * typ) list -> (string * typ) list
140 val add_const_names: term -> string list -> string list
141 val add_consts: term -> (string * typ) list -> (string * typ) list
142 val hidden_polymorphism: term -> (indexname * sort) list
143 val declare_typ_names: typ -> Name.context -> Name.context
144 val declare_term_names: term -> Name.context -> Name.context
145 val declare_term_frees: term -> Name.context -> Name.context
146 val variant_frees: term -> (string * 'a) list -> (string * 'a) list
147 val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
148 val eq_ix: indexname * indexname -> bool
149 val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
150 val eq_var: (indexname * typ) * (indexname * typ) -> bool
151 val aconv_untyped: term * term -> bool
152 val could_unify: term * term -> bool
153 val strip_abs_eta: int -> term -> (string * typ) list * term
154 val match_bvars: (term * term) * (string * string) list -> (string * string) list
155 val map_abs_vars: (string -> string) -> term -> term
156 val rename_abs: term -> term -> term -> term option
157 val is_open: term -> bool
158 val is_dependent: term -> bool
159 val lambda_name: string * term -> term -> term
160 val close_schematic_term: term -> term
161 val maxidx_typ: typ -> int -> int
162 val maxidx_typs: typ list -> int -> int
163 val maxidx_term: term -> int -> int
164 val has_abs: term -> bool
165 val dest_abs: string * typ * term -> string * term
166 val dummy_patternN: string
167 val dummy_pattern: typ -> term
168 val is_dummy_pattern: term -> bool
169 val free_dummy_patterns: term -> Name.context -> term * Name.context
170 val no_dummy_patterns: term -> term
171 val replace_dummy_patterns: term -> int -> term * int
172 val is_replaced_dummy_pattern: indexname -> bool
173 val show_dummy_patterns: term -> term
174 val string_of_vname: indexname -> string
175 val string_of_vname': indexname -> string
178 structure Term: TERM =
181 (*Indexnames can be quickly renamed by adding an offset to the integer part,
183 type indexname = string * int;
185 (* Types are classified by sorts. *)
187 type sort = class list;
188 type arity = string * sort list * sort;
190 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
191 datatype typ = Type of string * typ list
192 | TFree of string * sort
193 | TVar of indexname * sort;
195 (*Terms. Bound variables are indicated by depth number.
196 Free variables, (scheme) variables and constants have names.
197 An term is "closed" if every bound variable of level "lev"
198 is enclosed by at least "lev" abstractions.
200 It is possible to create meaningless terms containing loose bound vars
201 or type mismatches. But such terms are not allowed in rules. *)
204 Const of string * typ
205 | Free of string * typ
206 | Var of indexname * typ
208 | Abs of string*typ*term
211 (*Errors involving type mismatches*)
212 exception TYPE of string * typ list * term list;
214 (*Errors errors involving terms*)
215 exception TERM of string * term list;
217 (*Note variable naming conventions!
219 f,g,h: functions (including terms of function type)
224 A,B,C: term (denoting formulae)
231 (*dummies for type-inference etc.*)
233 val dummyT = Type ("dummy", []);
237 fun check (T as Type ("dummy", _)) =
238 raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
239 | check (Type (_, Ts)) = List.app check Ts
241 in check typ; typ end;
243 fun S --> T = Type("fun",[S,T]);
245 (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*)
246 val op ---> = Library.foldr (op -->);
248 fun dest_Type (Type x) = x
249 | dest_Type T = raise TYPE ("dest_Type", [T], []);
250 fun dest_TVar (TVar x) = x
251 | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
252 fun dest_TFree (TFree x) = x
253 | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
256 (** Discriminators **)
258 fun is_Bound (Bound _) = true
259 | is_Bound _ = false;
261 fun is_Const (Const _) = true
262 | is_Const _ = false;
264 fun is_Free (Free _) = true
267 fun is_Var (Var _) = true
270 fun is_TVar (TVar _) = true
276 fun dest_Const (Const x) = x
277 | dest_Const t = raise TERM("dest_Const", [t]);
279 fun dest_Free (Free x) = x
280 | dest_Free t = raise TERM("dest_Free", [t]);
282 fun dest_Var (Var x) = x
283 | dest_Var t = raise TERM("dest_Var", [t]);
285 fun dest_comb (t1 $ t2) = (t1, t2)
286 | dest_comb t = raise TERM("dest_comb", [t]);
289 fun domain_type (Type ("fun", [T, _])) = T;
291 fun range_type (Type ("fun", [_, U])) = U;
293 fun dest_funT (Type ("fun", [T, U])) = (T, U)
294 | dest_funT T = raise TYPE ("dest_funT", [T], []);
297 (* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*)
298 fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
299 | binder_types _ = [];
301 (* maps [T1,...,Tn]--->T to T*)
302 fun body_type (Type ("fun", [_, U])) = body_type U
305 (* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
306 fun strip_type T = (binder_types T, body_type T);
309 (*Compute the type of the term, checking that combinations are well-typed
310 Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
311 fun type_of1 (Ts, Const (_,T)) = T
312 | type_of1 (Ts, Free (_,T)) = T
313 | type_of1 (Ts, Bound i) = (nth Ts i
314 handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
315 | type_of1 (Ts, Var (_,T)) = T
316 | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
317 | type_of1 (Ts, f$u) =
318 let val U = type_of1(Ts,u)
319 and T = type_of1(Ts,f)
321 Type("fun",[T1,T2]) =>
322 if T1=U then T2 else raise TYPE
323 ("type_of: type mismatch in application", [T1,U], [f$u])
325 ("type_of: function type is expected in application",
329 fun type_of t : typ = type_of1 ([],t);
331 (*Determines the type of a term, with minimal checking*)
332 fun fastype_of1 (Ts, f$u) =
333 (case fastype_of1 (Ts,f) of
334 Type("fun",[_,T]) => T
335 | _ => raise TERM("fastype_of: expected function type", [f$u]))
336 | fastype_of1 (_, Const (_,T)) = T
337 | fastype_of1 (_, Free (_,T)) = T
338 | fastype_of1 (Ts, Bound i) = (nth Ts i
339 handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
340 | fastype_of1 (_, Var (_,T)) = T
341 | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
343 fun fastype_of t : typ = fastype_of1 ([],t);
345 (*Determine the argument type of a function*)
346 fun argument_type_of tm k =
348 fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
349 | argT _ T = raise TYPE ("argument_type_of", [T], []);
351 fun arg 0 _ (Abs (_, T, _)) = T
352 | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
353 | arg i Ts (t $ _) = arg (i + 1) Ts t
354 | arg i Ts a = argT i (fastype_of1 (Ts, a));
358 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
360 fun strip_abs (Abs (a, T, t)) =
361 let val (a', t') = strip_abs t
362 in ((a, T) :: a', t') end
363 | strip_abs t = ([], t);
365 (* maps (x1,...,xn)t to t *)
366 fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t
367 | strip_abs_body u = u;
369 (* maps (x1,...,xn)t to [x1, ..., xn] *)
370 fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t
371 | strip_abs_vars u = [] : (string*typ) list;
374 fun strip_qnt_body qnt =
375 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
379 fun strip_qnt_vars qnt =
380 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
381 | strip t = [] : (string*typ) list
385 (* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
386 val list_comb : term * term list -> term = Library.foldl (op $);
389 (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
390 fun strip_comb u : term * term list =
391 let fun stripc (f$t, ts) = stripc (f, t::ts)
396 (* maps f(t1,...,tn) to f , which is never a combination *)
397 fun head_of (f$t) = head_of f
400 (*number of atoms and abstractions in a term*)
401 fun size_of_term tm =
403 fun add_size (t $ u) n = add_size t (add_size u n)
404 | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
405 | add_size _ n = n + 1;
406 in add_size tm 0 end;
408 (*number of atoms and constructors in a type*)
411 fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
412 | add_size _ n = n + 1;
413 in add_size ty 0 end;
415 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
416 | map_atyps f T = f T;
418 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
419 | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
420 | map_aterms f t = f t;
422 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
423 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
427 fun map_aux (Const (a, T)) = Const (a, f T)
428 | map_aux (Free (a, T)) = Free (a, f T)
429 | map_aux (Var (v, T)) = Var (v, f T)
430 | map_aux (Bound i) = Bound i
431 | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
432 | map_aux (t $ u) = map_aux t $ map_aux u;
436 (* fold types and terms *)
438 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
439 | fold_atyps f T = f T;
441 fun fold_atyps_sorts f =
442 fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
444 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
445 | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
446 | fold_aterms f a = f a;
448 fun fold_term_types f (t as Const (_, T)) = f t T
449 | fold_term_types f (t as Free (_, T)) = f t T
450 | fold_term_types f (t as Var (_, T)) = f t T
451 | fold_term_types f (Bound _) = I
452 | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
453 | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
455 fun fold_types f = fold_term_types (K f);
457 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
458 | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
459 | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
460 | replace_types (Bound i) Ts = (Bound i, Ts)
461 | replace_types (Abs (x, _, b)) (T :: Ts) =
462 let val (b', Ts') = replace_types b Ts
463 in (Abs (x, T, b'), Ts') end
464 | replace_types (t $ u) Ts =
466 val (t', Ts') = replace_types t Ts;
467 val (u', Ts'') = replace_types u Ts';
468 in (t' $ u', Ts'') end;
470 fun burrow_types f ts =
472 val Ts = rev (fold (fold_types cons) ts []);
474 val (ts', []) = fold_map replace_types ts Ts';
477 (*collect variables*)
478 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
479 val add_tvar_names = fold_types add_tvar_namesT;
480 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
481 val add_tvars = fold_types add_tvarsT;
482 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
483 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
484 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
485 val add_tfree_names = fold_types add_tfree_namesT;
486 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
487 val add_tfrees = fold_types add_tfreesT;
488 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
489 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
490 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
491 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
493 (*extra type variables in a term, not covered by its type*)
494 fun hidden_polymorphism t =
496 val T = fastype_of t;
497 val tvarsT = add_tvarsT T [];
498 val extra_tvars = fold_types (fold_atyps
499 (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
503 (* renaming variables *)
505 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
507 fun declare_term_names tm =
509 (fn Const (a, _) => Name.declare (Long_Name.base_name a)
510 | Free (a, _) => Name.declare a
512 fold_types declare_typ_names tm;
514 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
516 fun variant_frees t frees =
517 fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
519 fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
523 (** Comparing terms **)
527 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
529 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
530 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
533 (* alpha equivalence *)
536 pointer_eq (tm1, tm2) orelse
538 (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
539 | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
540 | (a1, a2) => a1 = a2);
542 fun aconv_untyped (tm1, tm2) =
543 pointer_eq (tm1, tm2) orelse
545 (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
546 | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
547 | (Const (a, _), Const (b, _)) => a = b
548 | (Free (x, _), Free (y, _)) => x = y
549 | (Var (xi, _), Var (yj, _)) => xi = yj
550 | (Bound i, Bound j) => i = j
554 (*A fast unification filter: true unless the two terms cannot be unified.
555 Terms must be NORMAL. Treats all Vars as distinct. *)
556 fun could_unify (t, u) =
558 fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
559 | matchrands _ _ = true;
561 case (head_of t, head_of u) of
564 | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
565 | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
566 | (Bound i, Bound j) => i = j andalso matchrands t u
567 | (Abs _, _) => true (*because of possible eta equality*)
574 (** Connectives of higher order logic **)
576 fun aT S = TFree (Name.aT, S);
578 fun itselfT ty = Type ("itself", [ty]);
579 val a_itselfT = itselfT (TFree (Name.aT, []));
581 val propT : typ = Type("prop",[]);
583 fun all T = Const("all", (T-->propT)-->propT);
585 (* maps !!x1...xn. t to t *)
586 fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
587 | strip_all_body t = t;
589 (* maps !!x1...xn. t to [x1, ..., xn] *)
590 fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
591 (a,T) :: strip_all_vars t
592 | strip_all_vars t = [] : (string*typ) list;
594 (*increments a term's non-local bound variables
595 required when moving a term within abstractions
596 inc is increment for bound variables
597 lev is level at which a bound variable is considered 'loose'*)
598 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
599 | incr_bv (inc, lev, Abs(a,T,body)) =
600 Abs(a, T, incr_bv(inc,lev+1,body))
601 | incr_bv (inc, lev, f$t) =
602 incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
603 | incr_bv (inc, lev, u) = u;
605 fun incr_boundvars 0 t = t
606 | incr_boundvars inc t = incr_bv(inc,0,t);
608 (*Scan a pair of terms; while they are similar,
609 accumulate corresponding bound vars in "al"*)
610 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
611 match_bvs(s, t, if x="" orelse y="" then al
613 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
614 | match_bvs(_,_,al) = al;
616 (* strip abstractions created by parameters *)
617 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
619 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
620 | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
621 | map_abs_vars f t = t;
623 fun rename_abs pat obj t =
625 val ren = match_bvs (pat, obj, []);
626 fun ren_abs (Abs (x, T, b)) =
627 Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
628 | ren_abs (f $ t) = ren_abs f $ ren_abs t
630 in if null ren then NONE else SOME (ren_abs t) end;
632 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
633 (Bound 0) is loose at level 0 *)
634 fun add_loose_bnos (Bound i, lev, js) =
635 if i<lev then js else insert (op =) (i - lev) js
636 | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
637 | add_loose_bnos (f$t, lev, js) =
638 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
639 | add_loose_bnos (_, _, js) = js;
641 fun loose_bnos t = add_loose_bnos (t, 0, []);
643 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
644 level k or beyond. *)
645 fun loose_bvar(Bound i,k) = i >= k
646 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
647 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
648 | loose_bvar _ = false;
650 fun loose_bvar1(Bound i,k) = i = k
651 | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
652 | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
653 | loose_bvar1 _ = false;
655 fun is_open t = loose_bvar (t, 0);
656 fun is_dependent t = loose_bvar1 (t, 0);
658 (*Substitute arguments for loose bound variables.
659 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
660 Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
661 and the appropriate call is subst_bounds([b,a], c) .
662 Loose bound variables >=n are reduced by "n" to
663 compensate for the disappearance of lambdas.
665 fun subst_bounds (args: term list, t) : term =
668 fun subst (t as Bound i, lev) =
669 (if i < lev then raise Same.SAME (*var is locally bound*)
670 else incr_boundvars lev (nth args (i - lev))
671 handle General.Subscript => Bound (i - n)) (*loose: change it*)
672 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
673 | subst (f $ t, lev) =
674 (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
675 handle Same.SAME => f $ subst (t, lev))
676 | subst _ = raise Same.SAME;
677 in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
679 (*Special case: one argument*)
680 fun subst_bound (arg, t) : term =
682 fun subst (Bound i, lev) =
683 if i < lev then raise Same.SAME (*var is locally bound*)
684 else if i = lev then incr_boundvars lev arg
685 else Bound (i - 1) (*loose: change it*)
686 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
687 | subst (f $ t, lev) =
688 (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
689 handle Same.SAME => f $ subst (t, lev))
690 | subst _ = raise Same.SAME;
691 in subst (t, 0) handle Same.SAME => t end;
693 (*beta-reduce if possible, else form application*)
694 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
695 | betapply (f,u) = f$u;
697 val betapplys = Library.foldl betapply;
700 (*unfolding abstractions with substitution
701 of bound variables and implicit eta-expansion*)
702 fun strip_abs_eta k t =
704 val used = fold_aterms declare_term_frees t Name.context;
705 fun strip_abs t (0, used) = (([], t), (0, used))
706 | strip_abs (Abs (v, T, t)) (k, used) =
708 val ([v'], used') = Name.variants [v] used;
709 val t' = subst_bound (Free (v', T), t);
710 val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
711 in (((v', T) :: vs, t''), (k', used'')) end
712 | strip_abs t (k, used) = (([], t), (k, used));
713 fun expand_eta [] t _ = ([], t)
714 | expand_eta (T::Ts) t used =
716 val ([v], used') = Name.variants [""] used;
717 val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
718 in ((v, T) :: vs, t') end;
719 val ((vs1, t'), (k', used')) = strip_abs t (k, used);
720 val Ts = fst (chop k' (binder_types (fastype_of t')));
721 val (vs2, t'') = expand_eta Ts t' used';
722 in (vs1 @ vs2, t'') end;
725 (*Substitute new for free occurrences of old in a term*)
726 fun subst_free [] = I
729 case AList.lookup (op aconv) pairs u of
731 | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
732 | t$u' => substf t $ substf u'
736 (*Abstraction of the term "body" over its occurrences of v,
737 which must contain no loose bound variables.
738 The resulting term is ready to become the body of an Abs.*)
739 fun abstract_over (v, body) =
742 if v aconv tm then Bound lev
745 Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
747 (abs lev t $ (abs lev u handle Same.SAME => u)
748 handle Same.SAME => t $ abs lev u)
749 | _ => raise Same.SAME);
750 in abs 0 body handle Same.SAME => body end;
752 fun term_name (Const (x, _)) = Long_Name.base_name x
753 | term_name (Free (x, _)) = x
754 | term_name (Var ((x, _), _)) = x
755 | term_name _ = Name.uu;
757 fun lambda_name (x, v) t =
758 Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
760 fun lambda v t = lambda_name ("", v) t;
762 (*Form an abstraction over a free variable.*)
763 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
764 fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
766 (*Abstraction over a list of free variables*)
767 fun list_abs_free ([ ] , t) = t
768 | list_abs_free ((a,T)::vars, t) =
769 absfree(a, T, list_abs_free(vars,t));
771 (*Quantification over a list of free variables*)
772 fun list_all_free ([], t: term) = t
773 | list_all_free ((a,T)::vars, t) =
774 (all T) $ (absfree(a, T, list_all_free(vars,t)));
776 (*Quantification over a list of variables (already bound in body) *)
777 fun list_all ([], t) = t
778 | list_all ((a,T)::vars, t) =
779 (all T) $ (Abs(a, T, list_all(vars,t)));
781 (*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)].
782 A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
783 fun subst_atomic [] tm = tm
784 | subst_atomic inst tm =
786 fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
787 | subst (t $ u) = subst t $ subst u
788 | subst t = the_default t (AList.lookup (op aconv) inst t);
791 (*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*)
792 fun typ_subst_atomic [] ty = ty
793 | typ_subst_atomic inst ty =
795 fun subst (Type (a, Ts)) = Type (a, map subst Ts)
796 | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
799 fun subst_atomic_types [] tm = tm
800 | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
802 fun typ_subst_TVars [] ty = ty
803 | typ_subst_TVars inst ty =
805 fun subst (Type (a, Ts)) = Type (a, map subst Ts)
806 | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
810 fun subst_TVars [] tm = tm
811 | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
813 fun subst_Vars [] tm = tm
814 | subst_Vars inst tm =
816 fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
817 | subst (Abs (a, T, t)) = Abs (a, T, subst t)
818 | subst (t $ u) = subst t $ subst u
822 fun subst_vars ([], []) tm = tm
823 | subst_vars ([], inst) tm = subst_Vars inst tm
824 | subst_vars (instT, inst) tm =
826 fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
827 | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
828 | subst (Var (xi, T)) =
829 (case AList.lookup (op =) inst xi of
830 NONE => Var (xi, typ_subst_TVars instT T)
832 | subst (t as Bound _) = t
833 | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
834 | subst (t $ u) = subst t $ subst u;
837 fun close_schematic_term t =
839 val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
840 val extra_terms = map Var (add_vars t []);
841 in fold lambda (extra_terms @ extra_types) t end;
845 (** Identifying first-order terms **)
847 (*Differs from proofterm/is_fun in its treatment of TVar*)
848 fun is_funtype (Type ("fun", [_, _])) = true
849 | is_funtype _ = false;
851 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
852 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
854 (*First order means in all terms of the form f(t1,...,tn) no argument has a
855 function type. The supplied quantifiers are excluded: their argument always
856 has a function type through a recursive call into its body.*)
857 fun is_first_order quants =
858 let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
859 | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
860 member (op =) quants q andalso (*it is a known quantifier*)
861 not (is_funtype T) andalso first_order1 (T::Ts) body
862 | first_order1 Ts t =
864 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
865 | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
866 | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
867 | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
868 | (Abs _, ts) => false (*not in beta-normal form*)
869 | _ => error "first_order: unexpected case"
870 in first_order1 [] end;
873 (* maximum index of typs and terms *)
875 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
876 | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
877 | maxidx_typ (TFree _) i = i
878 and maxidx_typs [] i = i
879 | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
881 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
882 | maxidx_term (Const (_, T)) i = maxidx_typ T i
883 | maxidx_term (Free (_, T)) i = maxidx_typ T i
884 | maxidx_term (Bound _) i = i
885 | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
886 | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
888 fun maxidx_of_typ T = maxidx_typ T ~1;
889 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
890 fun maxidx_of_term t = maxidx_term t ~1;
894 (** misc syntax operations **)
898 fun exists_subtype P =
900 fun ex ty = P ty orelse
901 (case ty of Type (_, Ts) => exists ex Ts | _ => false);
906 fun ex (Const (_, T)) = P T
907 | ex (Free (_, T)) = P T
908 | ex (Var (_, T)) = P T
909 | ex (Bound _) = false
910 | ex (Abs (_, T, t)) = P T orelse ex t
911 | ex (t $ u) = ex t orelse ex u;
914 fun exists_subterm P =
916 fun ex tm = P tm orelse
918 t $ u => ex t orelse ex u
919 | Abs (_, _, t) => ex t
923 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
925 fun has_abs (Abs _) = true
926 | has_abs (t $ u) = has_abs t orelse has_abs u
930 (* dest abstraction *)
932 fun dest_abs (x, T, body) =
934 fun name_clash (Free (y, _)) = (x = y)
935 | name_clash (t $ u) = name_clash t orelse name_clash u
936 | name_clash (Abs (_, _, t)) = name_clash t
937 | name_clash _ = false;
939 if name_clash body then dest_abs (Name.variant [x] x, T, body) (*potentially slow*)
940 else (x, subst_bound (Free (x, T), body))
946 val dummy_patternN = "dummy_pattern";
948 fun dummy_pattern T = Const (dummy_patternN, T);
950 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
951 | is_dummy_pattern _ = false;
953 fun no_dummy_patterns tm =
954 if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
955 else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
957 fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
958 let val [x] = Name.invents used Name.uu 1
959 in (Free (Name.internal x, T), Name.declare x used) end
960 | free_dummy_patterns (Abs (x, T, b)) used =
961 let val (b', used') = free_dummy_patterns b used
962 in (Abs (x, T, b'), used') end
963 | free_dummy_patterns (t $ u) used =
965 val (t', used') = free_dummy_patterns t used;
966 val (u', used'') = free_dummy_patterns u used';
967 in (t' $ u', used'') end
968 | free_dummy_patterns a used = (a, used);
970 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
971 (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
972 | replace_dummy Ts (Abs (x, T, t)) i =
973 let val (t', i') = replace_dummy (T :: Ts) t i
974 in (Abs (x, T, t'), i') end
975 | replace_dummy Ts (t $ u) i =
977 val (t', i') = replace_dummy Ts t i;
978 val (u', i'') = replace_dummy Ts u i';
979 in (t' $ u', i'') end
980 | replace_dummy _ a i = (a, i);
982 val replace_dummy_patterns = replace_dummy [];
984 fun is_replaced_dummy_pattern ("_dummy_", _) = true
985 | is_replaced_dummy_pattern _ = false;
987 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
988 | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
989 | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
990 | show_dummy_patterns a = a;
993 (* display variables *)
995 fun string_of_vname (x, i) =
997 val idx = string_of_int i;
999 (case rev (Symbol.explode x) of
1000 _ :: "\\<^isub>" :: _ => false
1001 | _ :: "\\<^isup>" :: _ => false
1002 | c :: _ => Symbol.is_digit c
1005 if dot then "?" ^ x ^ "." ^ idx
1006 else if i <> 0 then "?" ^ x ^ idx
1010 fun string_of_vname' (x, ~1) = x
1011 | string_of_vname' xi = string_of_vname xi;
1015 structure Basic_Term: BASIC_TERM = Term;