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