1(*  Title:      Pure/term.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Author:     Makarius
4
5Simply typed lambda-calculus: types, terms, and basic operations.
6*)
7
8infix 9 $;
9infixr 5 -->;
10infixr --->;
11infix aconv;
12
13signature BASIC_TERM =
14sig
15  type indexname = string * int
16  type class = string
17  type sort = class list
18  type arity = string * sort list * sort
19  datatype typ =
20    Type  of string * typ list |
21    TFree of string * sort |
22    TVar  of indexname * sort
23  datatype term =
24    Const of string * typ |
25    Free of string * typ |
26    Var of indexname * typ |
27    Bound of int |
28    Abs of string * typ * term |
29    $ of term * term
30  exception TYPE of string * typ list * term list
31  exception TERM of string * term list
32  val dummyS: sort
33  val dummyT: typ
34  val no_dummyT: typ -> typ
35  val --> : typ * typ -> typ
36  val ---> : typ list * typ -> typ
37  val is_Type: typ -> bool
38  val is_TFree: typ -> bool
39  val is_TVar: typ -> bool
40  val dest_Type: typ -> string * typ list
41  val dest_TFree: typ -> string * sort
42  val dest_TVar: typ -> indexname * sort
43  val is_Bound: term -> bool
44  val is_Const: term -> bool
45  val is_Free: term -> bool
46  val is_Var: term -> bool
47  val dest_Const: term -> string * typ
48  val dest_Free: term -> string * typ
49  val dest_Var: term -> indexname * typ
50  val dest_comb: term -> term * term
51  val domain_type: typ -> typ
52  val range_type: typ -> typ
53  val dest_funT: typ -> typ * typ
54  val binder_types: typ -> typ list
55  val body_type: typ -> typ
56  val strip_type: typ -> typ list * typ
57  val type_of1: typ list * term -> typ
58  val type_of: term -> typ
59  val fastype_of1: typ list * term -> typ
60  val fastype_of: term -> typ
61  val strip_abs: term -> (string * typ) list * term
62  val strip_abs_body: term -> term
63  val strip_abs_vars: term -> (string * typ) list
64  val strip_qnt_body: string -> term -> term
65  val strip_qnt_vars: string -> term -> (string * typ) list
66  val list_comb: term * term list -> term
67  val strip_comb: term -> term * term list
68  val head_of: term -> term
69  val size_of_term: term -> int
70  val size_of_typ: typ -> int
71  val map_atyps: (typ -> typ) -> typ -> typ
72  val map_aterms: (term -> term) -> term -> term
73  val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
74  val map_type_tfree: (string * sort -> typ) -> typ -> typ
75  val map_types: (typ -> typ) -> term -> term
76  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
77  val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
78  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
79  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
80  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
81  val burrow_types: (typ list -> typ list) -> term list -> term list
82  val aconv: term * term -> bool
83  val propT: typ
84  val strip_all_body: term -> term
85  val strip_all_vars: term -> (string * typ) list
86  val incr_bv: int * int * term -> term
87  val incr_boundvars: int -> term -> term
88  val add_loose_bnos: term * int * int list -> int list
89  val loose_bnos: term -> int list
90  val loose_bvar: term * int -> bool
91  val loose_bvar1: term * int -> bool
92  val subst_bounds: term list * term -> term
93  val subst_bound: term * term -> term
94  val betapply: term * term -> term
95  val betapplys: term * term list -> term
96  val subst_free: (term * term) list -> term -> term
97  val abstract_over: term * term -> term
98  val lambda: term -> term -> term
99  val absfree: string * typ -> term -> term
100  val absdummy: typ -> term -> term
101  val subst_atomic: (term * term) list -> term -> term
102  val typ_subst_atomic: (typ * typ) list -> typ -> typ
103  val subst_atomic_types: (typ * typ) list -> term -> term
104  val typ_subst_TVars: (indexname * typ) list -> typ -> typ
105  val subst_TVars: (indexname * typ) list -> term -> term
106  val subst_Vars: (indexname * term) list -> term -> term
107  val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
108  val is_first_order: string list -> term -> bool
109  val maxidx_of_typ: typ -> int
110  val maxidx_of_typs: typ list -> int
111  val maxidx_of_term: term -> int
112  val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
113  val exists_subtype: (typ -> bool) -> typ -> bool
114  val exists_type: (typ -> bool) -> term -> bool
115  val exists_subterm: (term -> bool) -> term -> bool
116  val exists_Const: (string * typ -> bool) -> term -> bool
117end;
118
119signature TERM =
120sig
121  include BASIC_TERM
122  val aT: sort -> typ
123  val itselfT: typ -> typ
124  val a_itselfT: typ
125  val argument_type_of: term -> int -> typ
126  val abs: string * typ -> term -> term
127  val add_tvar_namesT: typ -> indexname list -> indexname list
128  val add_tvar_names: term -> indexname list -> indexname list
129  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
130  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
131  val add_var_names: term -> indexname list -> indexname list
132  val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
133  val add_tfree_namesT: typ -> string list -> string list
134  val add_tfree_names: term -> string list -> string list
135  val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
136  val add_tfrees: term -> (string * sort) list -> (string * sort) list
137  val add_free_names: term -> string list -> string list
138  val add_frees: term -> (string * typ) list -> (string * typ) list
139  val add_const_names: term -> string list -> string list
140  val add_consts: term -> (string * typ) list -> (string * typ) list
141  val hidden_polymorphism: term -> (indexname * sort) list
142  val declare_typ_names: typ -> Name.context -> Name.context
143  val declare_term_names: term -> Name.context -> Name.context
144  val declare_term_frees: term -> Name.context -> Name.context
145  val variant_frees: term -> (string * 'a) list -> (string * 'a) list
146  val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
147  val eq_ix: indexname * indexname -> bool
148  val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
149  val eq_var: (indexname * typ) * (indexname * typ) -> bool
150  val aconv_untyped: term * term -> bool
151  val could_unify: term * term -> bool
152  val strip_abs_eta: int -> term -> (string * typ) list * term
153  val match_bvars: (term * term) -> (string * string) list -> (string * string) list
154  val map_abs_vars: (string -> string) -> term -> term
155  val rename_abs: term -> term -> term -> term option
156  val is_open: term -> bool
157  val is_dependent: term -> bool
158  val term_name: term -> string
159  val dependent_lambda_name: string * term -> term -> term
160  val lambda_name: string * term -> term -> term
161  val close_schematic_term: term -> term
162  val maxidx_typ: typ -> int -> int
163  val maxidx_typs: typ list -> int -> int
164  val maxidx_term: term -> int -> int
165  val could_beta_contract: term -> bool
166  val could_eta_contract: term -> bool
167  val could_beta_eta_contract: term -> bool
168  val dest_abs: string * typ * term -> string * term
169  val dummy_pattern: typ -> term
170  val dummy: term
171  val dummy_prop: term
172  val is_dummy_pattern: term -> bool
173  val free_dummy_patterns: term -> Name.context -> term * Name.context
174  val no_dummy_patterns: term -> term
175  val replace_dummy_patterns: term -> int -> term * int
176  val show_dummy_patterns: term -> term
177  val string_of_vname: indexname -> string
178  val string_of_vname': indexname -> string
179end;
180
181structure Term: TERM =
182struct
183
184(*Indexnames can be quickly renamed by adding an offset to the integer part,
185  for resolution.*)
186type indexname = string * int;
187
188(*Types are classified by sorts.*)
189type class = string;
190type sort  = class list;
191type arity = string * sort list * sort;
192
193(*The sorts attached to TFrees and TVars specify the sort of that variable.*)
194datatype typ = Type  of string * typ list
195             | TFree of string * sort
196             | TVar  of indexname * sort;
197
198(*Terms.  Bound variables are indicated by depth number.
199  Free variables, (scheme) variables and constants have names.
200  An term is "closed" if every bound variable of level "lev"
201  is enclosed by at least "lev" abstractions.
202
203  It is possible to create meaningless terms containing loose bound vars
204  or type mismatches.  But such terms are not allowed in rules. *)
205
206datatype term =
207    Const of string * typ
208  | Free  of string * typ
209  | Var   of indexname * typ
210  | Bound of int
211  | Abs   of string*typ*term
212  | op $  of term*term;
213
214(*Errors involving type mismatches*)
215exception TYPE of string * typ list * term list;
216
217(*Errors errors involving terms*)
218exception TERM of string * term list;
219
220(*Note variable naming conventions!
221    a,b,c: string
222    f,g,h: functions (including terms of function type)
223    i,j,m,n: int
224    t,u: term
225    v,w: indexnames
226    x,y: any
227    A,B,C: term (denoting formulae)
228    T,U: typ
229*)
230
231
232(** Types **)
233
234(*dummies for type-inference etc.*)
235val dummyS = [""];
236val dummyT = Type ("dummy", []);
237
238fun no_dummyT typ =
239  let
240    fun check (T as Type ("dummy", _)) =
241          raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
242      | check (Type (_, Ts)) = List.app check Ts
243      | check _ = ();
244  in check typ; typ end;
245
246fun S --> T = Type("fun",[S,T]);
247
248(*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
249val op ---> = Library.foldr (op -->);
250
251
252(** Discriminators **)
253
254fun is_Type (Type _) = true
255  | is_Type _ = false;
256
257fun is_TFree (TFree _) = true
258  | is_TFree _ = false;
259
260fun is_TVar (TVar _) = true
261  | is_TVar _ = false;
262
263
264(** Destructors **)
265
266fun dest_Type (Type x) = x
267  | dest_Type T = raise TYPE ("dest_Type", [T], []);
268
269fun dest_TFree (TFree x) = x
270  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
271
272fun dest_TVar (TVar x) = x
273  | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
274
275
276(** Discriminators **)
277
278fun is_Bound (Bound _) = true
279  | is_Bound _         = false;
280
281fun is_Const (Const _) = true
282  | is_Const _ = false;
283
284fun is_Free (Free _) = true
285  | is_Free _ = false;
286
287fun is_Var (Var _) = true
288  | is_Var _ = false;
289
290
291(** Destructors **)
292
293fun dest_Const (Const x) =  x
294  | dest_Const t = raise TERM("dest_Const", [t]);
295
296fun dest_Free (Free x) =  x
297  | dest_Free t = raise TERM("dest_Free", [t]);
298
299fun dest_Var (Var x) =  x
300  | dest_Var t = raise TERM("dest_Var", [t]);
301
302fun dest_comb (t1 $ t2) = (t1, t2)
303  | dest_comb t = raise TERM("dest_comb", [t]);
304
305
306fun domain_type (Type ("fun", [T, _])) = T;
307
308fun range_type (Type ("fun", [_, U])) = U;
309
310fun dest_funT (Type ("fun", [T, U])) = (T, U)
311  | dest_funT T = raise TYPE ("dest_funT", [T], []);
312
313
314(*maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
315fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
316  | binder_types _ = [];
317
318(*maps  [T1,...,Tn]--->T  to T*)
319fun body_type (Type ("fun", [_, U])) = body_type U
320  | body_type T = T;
321
322(*maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)*)
323fun strip_type T = (binder_types T, body_type T);
324
325
326(*Compute the type of the term, checking that combinations are well-typed
327  Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
328fun type_of1 (Ts, Const (_,T)) = T
329  | type_of1 (Ts, Free  (_,T)) = T
330  | type_of1 (Ts, Bound i) = (nth Ts i
331        handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
332  | type_of1 (Ts, Var (_,T)) = T
333  | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
334  | type_of1 (Ts, f$u) =
335      let val U = type_of1(Ts,u)
336          and T = type_of1(Ts,f)
337      in case T of
338            Type("fun",[T1,T2]) =>
339              if T1=U then T2  else raise TYPE
340                    ("type_of: type mismatch in application", [T1,U], [f$u])
341          | _ => raise TYPE
342                    ("type_of: function type is expected in application",
343                     [T,U], [f$u])
344      end;
345
346fun type_of t : typ = type_of1 ([],t);
347
348(*Determines the type of a term, with minimal checking*)
349fun fastype_of1 (Ts, f$u) =
350    (case fastype_of1 (Ts,f) of
351        Type("fun",[_,T]) => T
352        | _ => raise TERM("fastype_of: expected function type", [f$u]))
353  | fastype_of1 (_, Const (_,T)) = T
354  | fastype_of1 (_, Free (_,T)) = T
355  | fastype_of1 (Ts, Bound i) = (nth Ts i
356         handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
357  | fastype_of1 (_, Var (_,T)) = T
358  | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
359
360fun fastype_of t : typ = fastype_of1 ([],t);
361
362(*Determine the argument type of a function*)
363fun argument_type_of tm k =
364  let
365    fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
366      | argT _ T = raise TYPE ("argument_type_of", [T], []);
367
368    fun arg 0 _ (Abs (_, T, _)) = T
369      | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
370      | arg i Ts (t $ _) = arg (i + 1) Ts t
371      | arg i Ts a = argT i (fastype_of1 (Ts, a));
372  in arg k [] tm end;
373
374
375fun abs (x, T) t = Abs (x, T, t);
376
377fun strip_abs (Abs (a, T, t)) =
378      let val (a', t') = strip_abs t
379      in ((a, T) :: a', t') end
380  | strip_abs t = ([], t);
381
382(*maps  (x1,...,xn)t   to   t*)
383fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
384  | strip_abs_body u  =  u;
385
386(*maps  (x1,...,xn)t   to   [x1, ..., xn]*)
387fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
388  | strip_abs_vars u  =  [] : (string*typ) list;
389
390
391fun strip_qnt_body qnt =
392let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
393      | strip t = t
394in strip end;
395
396fun strip_qnt_vars qnt =
397let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
398      | strip t  =  [] : (string*typ) list
399in strip end;
400
401
402(*maps   (f, [t1,...,tn])  to  f(t1,...,tn)*)
403val list_comb : term * term list -> term = Library.foldl (op $);
404
405
406(*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
407fun strip_comb u : term * term list =
408    let fun stripc (f$t, ts) = stripc (f, t::ts)
409        |   stripc  x =  x
410    in  stripc(u,[])  end;
411
412
413(*maps   f(t1,...,tn)  to  f , which is never a combination*)
414fun head_of (f$t) = head_of f
415  | head_of u = u;
416
417(*number of atoms and abstractions in a term*)
418fun size_of_term tm =
419  let
420    fun add_size (t $ u) n = add_size t (add_size u n)
421      | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
422      | add_size _ n = n + 1;
423  in add_size tm 0 end;
424
425(*number of atoms and constructors in a type*)
426fun size_of_typ ty =
427  let
428    fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
429      | add_size _ n = n + 1;
430  in add_size ty 0 end;
431
432fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
433  | map_atyps f T = f T;
434
435fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
436  | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
437  | map_aterms f t = f t;
438
439fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
440fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
441
442fun map_types f =
443  let
444    fun map_aux (Const (a, T)) = Const (a, f T)
445      | map_aux (Free (a, T)) = Free (a, f T)
446      | map_aux (Var (v, T)) = Var (v, f T)
447      | map_aux (Bound i) = Bound i
448      | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
449      | map_aux (t $ u) = map_aux t $ map_aux u;
450  in map_aux end;
451
452
453(* fold types and terms *)
454
455fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
456  | fold_atyps f T = f T;
457
458fun fold_atyps_sorts f =
459  fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
460
461fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
462  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
463  | fold_aterms f a = f a;
464
465fun fold_term_types f (t as Const (_, T)) = f t T
466  | fold_term_types f (t as Free (_, T)) = f t T
467  | fold_term_types f (t as Var (_, T)) = f t T
468  | fold_term_types f (Bound _) = I
469  | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
470  | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
471
472fun fold_types f = fold_term_types (K f);
473
474fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
475  | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
476  | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
477  | replace_types (Bound i) Ts = (Bound i, Ts)
478  | replace_types (Abs (x, _, b)) (T :: Ts) =
479      let val (b', Ts') = replace_types b Ts
480      in (Abs (x, T, b'), Ts') end
481  | replace_types (t $ u) Ts =
482      let
483        val (t', Ts') = replace_types t Ts;
484        val (u', Ts'') = replace_types u Ts';
485      in (t' $ u', Ts'') end;
486
487fun burrow_types f ts =
488  let
489    val Ts = rev ((fold o fold_types) cons ts []);
490    val Ts' = f Ts;
491    val (ts', []) = fold_map replace_types ts Ts';
492  in ts' end;
493
494(*collect variables*)
495val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
496val add_tvar_names = fold_types add_tvar_namesT;
497val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
498val add_tvars = fold_types add_tvarsT;
499val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
500val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
501val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
502val add_tfree_names = fold_types add_tfree_namesT;
503val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
504val add_tfrees = fold_types add_tfreesT;
505val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
506val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
507val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
508val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
509
510(*extra type variables in a term, not covered by its type*)
511fun hidden_polymorphism t =
512  let
513    val T = fastype_of t;
514    val tvarsT = add_tvarsT T [];
515    val extra_tvars = fold_types (fold_atyps
516      (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
517  in extra_tvars end;
518
519
520(* renaming variables *)
521
522val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
523
524fun declare_term_names tm =
525  fold_aterms
526    (fn Const (a, _) => Name.declare (Long_Name.base_name a)
527      | Free (a, _) => Name.declare a
528      | _ => I) tm #>
529  fold_types declare_typ_names tm;
530
531val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
532
533fun variant_frees t frees =
534  fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
535    map snd frees;
536
537fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
538
539
540
541(** Comparing terms **)
542
543(* variables *)
544
545fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
546
547fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
548fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
549
550
551(* alpha equivalence *)
552
553fun tm1 aconv tm2 =
554  pointer_eq (tm1, tm2) orelse
555    (case (tm1, tm2) of
556      (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
557    | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
558    | (a1, a2) => a1 = a2);
559
560fun aconv_untyped (tm1, tm2) =
561  pointer_eq (tm1, tm2) orelse
562    (case (tm1, tm2) of
563      (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
564    | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
565    | (Const (a, _), Const (b, _)) => a = b
566    | (Free (x, _), Free (y, _)) => x = y
567    | (Var (xi, _), Var (yj, _)) => xi = yj
568    | (Bound i, Bound j) => i = j
569    | _ => false);
570
571
572(*A fast unification filter: true unless the two terms cannot be unified.
573  Terms must be NORMAL.  Treats all Vars as distinct. *)
574fun could_unify (t, u) =
575  let
576    fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
577      | matchrands _ _ = true;
578  in
579    case (head_of t, head_of u) of
580      (_, Var _) => true
581    | (Var _, _) => true
582    | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
583    | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
584    | (Bound i, Bound j) => i = j andalso matchrands t u
585    | (Abs _, _) => true   (*because of possible eta equality*)
586    | (_, Abs _) => true
587    | _ => false
588  end;
589
590
591
592(** Connectives of higher order logic **)
593
594fun aT S = TFree (Name.aT, S);
595
596fun itselfT ty = Type ("itself", [ty]);
597val a_itselfT = itselfT (TFree (Name.aT, []));
598
599val propT : typ = Type ("prop",[]);
600
601(*maps  \<And>x1...xn. t   to   t*)
602fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
603  | strip_all_body t = t;
604
605(*maps  \<And>x1...xn. t   to   [x1, ..., xn]*)
606fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
607  | strip_all_vars t = [];
608
609(*increments a term's non-local bound variables
610  required when moving a term within abstractions
611     inc is  increment for bound variables
612     lev is  level at which a bound variable is considered 'loose'*)
613fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
614  | incr_bv (inc, lev, Abs(a,T,body)) =
615        Abs(a, T, incr_bv(inc,lev+1,body))
616  | incr_bv (inc, lev, f$t) =
617      incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
618  | incr_bv (inc, lev, u) = u;
619
620fun incr_boundvars  0  t = t
621  | incr_boundvars inc t = incr_bv(inc,0,t);
622
623(*Scan a pair of terms; while they are similar,
624  accumulate corresponding bound vars in "al"*)
625fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
626      match_bvs(s, t, if x="" orelse y="" then al
627                                          else (x,y)::al)
628  | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
629  | match_bvs(_,_,al) = al;
630
631(* strip abstractions created by parameters *)
632fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
633
634fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
635  | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
636  | map_abs_vars f t = t;
637
638fun rename_abs pat obj t =
639  let
640    val ren = match_bvs (pat, obj, []);
641    fun ren_abs (Abs (x, T, b)) =
642          Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
643      | ren_abs (f $ t) = ren_abs f $ ren_abs t
644      | ren_abs t = t
645  in if null ren then NONE else SOME (ren_abs t) end;
646
647(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
648   (Bound 0) is loose at level 0 *)
649fun add_loose_bnos (Bound i, lev, js) =
650        if i<lev then js else insert (op =) (i - lev) js
651  | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
652  | add_loose_bnos (f$t, lev, js) =
653        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
654  | add_loose_bnos (_, _, js) = js;
655
656fun loose_bnos t = add_loose_bnos (t, 0, []);
657
658(* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
659   level k or beyond. *)
660fun loose_bvar(Bound i,k) = i >= k
661  | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
662  | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
663  | loose_bvar _ = false;
664
665fun loose_bvar1(Bound i,k) = i = k
666  | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
667  | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
668  | loose_bvar1 _ = false;
669
670fun is_open t = loose_bvar (t, 0);
671fun is_dependent t = loose_bvar1 (t, 0);
672
673(*Substitute arguments for loose bound variables.
674  Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
675  Note that for ((\<lambda>x y. c) a b), the bound vars in c are x=1 and y=0
676        and the appropriate call is  subst_bounds([b,a], c) .
677  Loose bound variables >=n are reduced by "n" to
678     compensate for the disappearance of lambdas.
679*)
680fun subst_bounds (args: term list, t) : term =
681  let
682    val n = length args;
683    fun subst (t as Bound i, lev) =
684         (if i < lev then raise Same.SAME   (*var is locally bound*)
685          else incr_boundvars lev (nth args (i - lev))
686            handle General.Subscript => Bound (i - n))  (*loose: change it*)
687      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
688      | subst (f $ t, lev) =
689          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
690            handle Same.SAME => f $ subst (t, lev))
691      | subst _ = raise Same.SAME;
692  in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
693
694(*Special case: one argument*)
695fun subst_bound (arg, t) : term =
696  let
697    fun subst (Bound i, lev) =
698          if i < lev then raise Same.SAME   (*var is locally bound*)
699          else if i = lev then incr_boundvars lev arg
700          else Bound (i - 1)   (*loose: change it*)
701      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
702      | subst (f $ t, lev) =
703          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
704            handle Same.SAME => f $ subst (t, lev))
705      | subst _ = raise Same.SAME;
706  in subst (t, 0) handle Same.SAME => t end;
707
708(*beta-reduce if possible, else form application*)
709fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
710  | betapply (f,u) = f$u;
711
712val betapplys = Library.foldl betapply;
713
714
715(*unfolding abstractions with substitution
716  of bound variables and implicit eta-expansion*)
717fun strip_abs_eta k t =
718  let
719    val used = fold_aterms declare_term_frees t Name.context;
720    fun strip_abs t (0, used) = (([], t), (0, used))
721      | strip_abs (Abs (v, T, t)) (k, used) =
722          let
723            val (v', used') = Name.variant v used;
724            val t' = subst_bound (Free (v', T), t);
725            val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
726          in (((v', T) :: vs, t''), (k', used'')) end
727      | strip_abs t (k, used) = (([], t), (k, used));
728    fun expand_eta [] t _ = ([], t)
729      | expand_eta (T::Ts) t used =
730          let
731            val (v, used') = Name.variant "" used;
732            val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
733          in ((v, T) :: vs, t') end;
734    val ((vs1, t'), (k', used')) = strip_abs t (k, used);
735    val Ts = fst (chop k' (binder_types (fastype_of t')));
736    val (vs2, t'') = expand_eta Ts t' used';
737  in (vs1 @ vs2, t'') end;
738
739
740(*Substitute new for free occurrences of old in a term*)
741fun subst_free [] = I
742  | subst_free pairs =
743      let fun substf u =
744            case AList.lookup (op aconv) pairs u of
745                SOME u' => u'
746              | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
747                                 | t$u' => substf t $ substf u'
748                                 | _ => u)
749      in  substf  end;
750
751(*Abstraction of the term "body" over its occurrences of v,
752    which must contain no loose bound variables.
753  The resulting term is ready to become the body of an Abs.*)
754fun abstract_over (v, body) =
755  let
756    fun abs lev tm =
757      if v aconv tm then Bound lev
758      else
759        (case tm of
760          Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
761        | t $ u =>
762            (abs lev t $ (abs lev u handle Same.SAME => u)
763              handle Same.SAME => t $ abs lev u)
764        | _ => raise Same.SAME);
765  in abs 0 body handle Same.SAME => body end;
766
767fun term_name (Const (x, _)) = Long_Name.base_name x
768  | term_name (Free (x, _)) = x
769  | term_name (Var ((x, _), _)) = x
770  | term_name _ = Name.uu;
771
772fun dependent_lambda_name (x, v) t =
773  let val t' = abstract_over (v, t)
774  in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
775
776fun lambda_name (x, v) t =
777  Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
778
779fun lambda v t = lambda_name ("", v) t;
780
781fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
782fun absdummy T body = Abs (Name.uu_, T, body);
783
784(*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
785  A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
786fun subst_atomic [] tm = tm
787  | subst_atomic inst tm =
788      let
789        fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
790          | subst (t $ u) = subst t $ subst u
791          | subst t = the_default t (AList.lookup (op aconv) inst t);
792      in subst tm end;
793
794(*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
795fun typ_subst_atomic [] ty = ty
796  | typ_subst_atomic inst ty =
797      let
798        fun subst (Type (a, Ts)) = Type (a, map subst Ts)
799          | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
800      in subst ty end;
801
802fun subst_atomic_types [] tm = tm
803  | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
804
805fun typ_subst_TVars [] ty = ty
806  | typ_subst_TVars inst ty =
807      let
808        fun subst (Type (a, Ts)) = Type (a, map subst Ts)
809          | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
810          | subst T = T;
811      in subst ty end;
812
813fun subst_TVars [] tm = tm
814  | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
815
816fun subst_Vars [] tm = tm
817  | subst_Vars inst tm =
818      let
819        fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
820          | subst (Abs (a, T, t)) = Abs (a, T, subst t)
821          | subst (t $ u) = subst t $ subst u
822          | subst t = t;
823      in subst tm end;
824
825fun subst_vars ([], []) tm = tm
826  | subst_vars ([], inst) tm = subst_Vars inst tm
827  | subst_vars (instT, inst) tm =
828      let
829        fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
830          | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
831          | subst (Var (xi, T)) =
832              (case AList.lookup (op =) inst xi of
833                NONE => Var (xi, typ_subst_TVars instT T)
834              | SOME t => t)
835          | subst (t as Bound _) = t
836          | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
837          | subst (t $ u) = subst t $ subst u;
838      in subst tm end;
839
840fun close_schematic_term t =
841  let
842    val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t);
843    val extra_terms = map Var (add_vars t []);
844  in fold lambda (extra_terms @ extra_types) t end;
845
846
847
848(** Identifying first-order terms **)
849
850(*Differs from proofterm/is_fun in its treatment of TVar*)
851fun is_funtype (Type ("fun", [_, _])) = true
852  | is_funtype _ = false;
853
854(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
855fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
856
857(*First order means in all terms of the form f(t1,...,tn) no argument has a
858  function type. The supplied quantifiers are excluded: their argument always
859  has a function type through a recursive call into its body.*)
860fun is_first_order quants =
861  let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
862        | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
863            member (op =) quants q  andalso   (*it is a known quantifier*)
864            not (is_funtype T)   andalso first_order1 (T::Ts) body
865        | first_order1 Ts t =
866            case strip_comb t of
867                 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
868               | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
869               | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
870               | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
871               | (Abs _, ts) => false (*not in beta-normal form*)
872               | _ => error "first_order: unexpected case"
873    in  first_order1 []  end;
874
875
876(* maximum index of typs and terms *)
877
878fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
879  | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
880  | maxidx_typ (TFree _) i = i
881and maxidx_typs [] i = i
882  | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
883
884fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
885  | maxidx_term (Const (_, T)) i = maxidx_typ T i
886  | maxidx_term (Free (_, T)) i = maxidx_typ T i
887  | maxidx_term (Bound _) i = i
888  | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
889  | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
890
891fun maxidx_of_typ T = maxidx_typ T ~1;
892fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
893fun maxidx_of_term t = maxidx_term t ~1;
894
895
896
897(** misc syntax operations **)
898
899(* substructure *)
900
901fun fold_subtypes f =
902  let
903    fun iter ty =
904      (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty);
905  in iter end;
906
907fun exists_subtype P =
908  let
909    fun ex ty = P ty orelse
910      (case ty of Type (_, Ts) => exists ex Ts | _ => false);
911  in ex end;
912
913fun exists_type P =
914  let
915    fun ex (Const (_, T)) = P T
916      | ex (Free (_, T)) = P T
917      | ex (Var (_, T)) = P T
918      | ex (Bound _) = false
919      | ex (Abs (_, T, t)) = P T orelse ex t
920      | ex (t $ u) = ex t orelse ex u;
921  in ex end;
922
923fun exists_subterm P =
924  let
925    fun ex tm = P tm orelse
926      (case tm of
927        t $ u => ex t orelse ex u
928      | Abs (_, _, t) => ex t
929      | _ => false);
930  in ex end;
931
932fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
933
934
935(* contraction *)
936
937fun could_beta_contract (Abs _ $ _) = true
938  | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u
939  | could_beta_contract (Abs (_, _, b)) = could_beta_contract b
940  | could_beta_contract _ = false;
941
942fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true
943  | could_eta_contract (Abs (_, _, b)) = could_eta_contract b
944  | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u
945  | could_eta_contract _ = false;
946
947fun could_beta_eta_contract (Abs _ $ _) = true
948  | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true
949  | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b
950  | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u
951  | could_beta_eta_contract _ = false;
952
953
954(* dest abstraction *)
955
956fun dest_abs (x, T, body) =
957  let
958    fun name_clash (Free (y, _)) = (x = y)
959      | name_clash (t $ u) = name_clash t orelse name_clash u
960      | name_clash (Abs (_, _, t)) = name_clash t
961      | name_clash _ = false;
962  in
963    if name_clash body then
964      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
965    else (x, subst_bound (Free (x, T), body))
966  end;
967
968
969(* dummy patterns *)
970
971fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
972val dummy = dummy_pattern dummyT;
973val dummy_prop = dummy_pattern propT;
974
975fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
976  | is_dummy_pattern _ = false;
977
978fun no_dummy_patterns tm =
979  if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
980  else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
981
982fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
983      let val [x] = Name.invent used Name.uu 1
984      in (Free (Name.internal x, T), Name.declare x used) end
985  | free_dummy_patterns (Abs (x, T, b)) used =
986      let val (b', used') = free_dummy_patterns b used
987      in (Abs (x, T, b'), used') end
988  | free_dummy_patterns (t $ u) used =
989      let
990        val (t', used') = free_dummy_patterns t used;
991        val (u', used'') = free_dummy_patterns u used';
992      in (t' $ u', used'') end
993  | free_dummy_patterns a used = (a, used);
994
995fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
996      (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
997  | replace_dummy Ts (Abs (x, T, t)) i =
998      let val (t', i') = replace_dummy (T :: Ts) t i
999      in (Abs (x, T, t'), i') end
1000  | replace_dummy Ts (t $ u) i =
1001      let
1002        val (t', i') = replace_dummy Ts t i;
1003        val (u', i'') = replace_dummy Ts u i';
1004      in (t' $ u', i'') end
1005  | replace_dummy _ a i = (a, i);
1006
1007val replace_dummy_patterns = replace_dummy [];
1008
1009fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
1010  | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
1011  | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
1012  | show_dummy_patterns a = a;
1013
1014
1015(* display variables *)
1016
1017fun string_of_vname (x, i) =
1018  let
1019    val idx = string_of_int i;
1020    val dot =
1021      (case rev (Symbol.explode x) of
1022        _ :: "\<^sub>" :: _ => false
1023      | c :: _ => Symbol.is_digit c
1024      | _ => true);
1025  in
1026    if dot then "?" ^ x ^ "." ^ idx
1027    else if i <> 0 then "?" ^ x ^ idx
1028    else "?" ^ x
1029  end;
1030
1031fun string_of_vname' (x, ~1) = x
1032  | string_of_vname' xi = string_of_vname xi;
1033
1034end;
1035
1036structure Basic_Term: BASIC_TERM = Term;
1037open Basic_Term;
1038