src/Pure/term.ML
author wenzelm
Tue Feb 07 19:57:00 2006 +0100 (2006-02-07)
changeset 18975 78d650a7e99a
parent 18942 9228bbe9cd4e
child 18976 4efb82669880
permissions -rw-r--r--
lambda: base name of Const;
     1 (*  Title:      Pure/term.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Simply typed lambda-calculus: types, terms, and basic operations.
     7 *)
     8 
     9 infix 9  $;
    10 infixr 5 -->;
    11 infixr --->;
    12 infix aconv;
    13 
    14 signature BASIC_TERM =
    15 sig
    16   type indexname
    17   type class
    18   type sort
    19   type arity
    20   datatype typ =
    21     Type  of string * typ list |
    22     TFree of string * sort |
    23     TVar  of indexname * sort
    24   datatype term =
    25     Const of string * typ |
    26     Free of string * typ |
    27     Var of indexname * typ |
    28     Bound of int |
    29     Abs of string * typ * term |
    30     $ of term * term
    31   exception TYPE of string * typ list * term list
    32   exception TERM of string * term list
    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 is_funtype: typ -> bool
    46   val dest_Const: term -> string * typ
    47   val dest_Free: term -> string * typ
    48   val dest_Var: term -> indexname * typ
    49   val domain_type: typ -> typ
    50   val range_type: typ -> typ
    51   val binder_types: typ -> typ list
    52   val body_type: typ -> typ
    53   val strip_type: typ -> typ list * typ
    54   val type_of1: typ list * term -> typ
    55   val type_of: term -> typ
    56   val fastype_of1: typ list * term -> typ
    57   val fastype_of: term -> typ
    58   val list_abs: (string * typ) list * term -> term
    59   val strip_abs: term -> (string * typ) list * term
    60   val strip_abs_body: term -> term
    61   val strip_abs_vars: term -> (string * typ) list
    62   val strip_qnt_body: string -> term -> term
    63   val strip_qnt_vars: string -> term -> (string * typ) list
    64   val list_comb: term * term list -> term
    65   val strip_comb: term -> term * term list
    66   val head_of: term -> term
    67   val size_of_term: term -> 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_term_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 it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    78   val add_term_names: term * string list -> string list
    79   val add_term_varnames: term -> indexname list -> indexname list
    80   val term_varnames: term -> indexname list
    81   val find_free: term -> string -> term option
    82   val aconv: term * term -> bool
    83   val aconvs: term list * term list -> bool
    84   structure Vartab: TABLE
    85   structure Typtab: TABLE
    86   structure Termtab: TABLE
    87   val itselfT: typ -> typ
    88   val a_itselfT: typ
    89   val propT: typ
    90   val implies: term
    91   val all: typ -> term
    92   val equals: typ -> term
    93   val strip_all_body: term -> term
    94   val strip_all_vars: term -> (string * typ) list
    95   val incr_bv: int * int * term -> term
    96   val incr_boundvars: int -> term -> term
    97   val add_loose_bnos: term * int * int list -> int list
    98   val loose_bnos: term -> int list
    99   val loose_bvar: term * int -> bool
   100   val loose_bvar1: term * int -> bool
   101   val subst_bounds: term list * term -> term
   102   val subst_bound: term * term -> term
   103   val betapply: term * term -> term
   104   val betapplys: term * term list -> term
   105   val eq_ix: indexname * indexname -> bool
   106   val ins_ix: indexname * indexname list -> indexname list
   107   val mem_ix: indexname * indexname list -> bool
   108   val mem_term: term * term list -> bool
   109   val ins_term: term * term list -> term list
   110   val could_unify: term * term -> bool
   111   val subst_free: (term * term) list -> term -> term
   112   val xless: (string * int) * indexname -> bool
   113   val abstract_over: term * term -> term
   114   val lambda: term -> term -> term
   115   val absfree: string * typ * term -> term
   116   val absdummy: typ * term -> term
   117   val list_abs_free: (string * typ) list * term -> term
   118   val list_all_free: (string * typ) list * term -> term
   119   val list_all: (string * typ) list * term -> term
   120   val subst_atomic: (term * term) list -> term -> term
   121   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   122   val subst_atomic_types: (typ * typ) list -> term -> term
   123   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   124   val subst_TVars: (indexname * typ) list -> term -> term
   125   val subst_Vars: (indexname * term) list -> term -> term
   126   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   127   val is_first_order: string list -> term -> bool
   128   val maxidx_of_typ: typ -> int
   129   val maxidx_of_typs: typ list -> int
   130   val maxidx_of_term: term -> int
   131   val variant: string list -> string -> string
   132   val variantlist: string list * string list -> string list
   133     (*note reversed order of args wrt. variant!*)
   134   val add_typ_classes: typ * class list -> class list
   135   val add_typ_tycons: typ * string list -> string list
   136   val add_term_classes: term * class list -> class list
   137   val add_term_tycons: term * string list -> string list
   138   val add_term_consts: term * string list -> string list
   139   val term_consts: term -> string list
   140   val exists_subterm: (term -> bool) -> term -> bool
   141   val exists_Const: (string * typ -> bool) -> term -> bool
   142   val add_term_free_names: term * string list -> string list
   143   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   144   val add_typ_tfree_names: typ * string list -> string list
   145   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   146   val add_typ_varnames: typ * string list -> string list
   147   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   148   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   149   val add_term_tfree_names: term * string list -> string list
   150   val add_term_tvarnames: term * string list -> string list
   151   val typ_tfrees: typ -> (string * sort) list
   152   val typ_tvars: typ -> (indexname * sort) list
   153   val term_tfrees: term -> (string * sort) list
   154   val term_tvars: term -> (indexname * sort) list
   155   val add_typ_ixns: indexname list * typ -> indexname list
   156   val add_term_tvar_ixns: term * indexname list -> indexname list
   157   val add_term_vars: term * term list -> term list
   158   val term_vars: term -> term list
   159   val add_term_frees: term * term list -> term list
   160   val term_frees: term -> term list
   161   val variant_abs: string * typ * term -> string * term
   162   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   163   val show_question_marks: bool ref
   164 end;
   165 
   166 signature TERM =
   167 sig
   168   include BASIC_TERM
   169   val argument_type_of: term -> typ
   170   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   171   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   172   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   173   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   174   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   175   val add_frees: term -> (string * typ) list -> (string * typ) list
   176   val fast_indexname_ord: indexname * indexname -> order
   177   val indexname_ord: indexname * indexname -> order
   178   val sort_ord: sort * sort -> order
   179   val typ_ord: typ * typ -> order
   180   val fast_term_ord: term * term -> order
   181   val term_ord: term * term -> order
   182   val hd_ord: term * term -> order
   183   val termless: term * term -> bool
   184   val term_lpo: (string -> int) -> term * term -> order
   185   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   186   val rename_abs: term -> term -> term -> term option
   187   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   188   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   189   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   190   val var_ord: (indexname * typ) * (indexname * typ) -> order
   191   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   192     -> term -> term
   193   val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
   194   val maxidx_typ: typ -> int -> int
   195   val maxidx_typs: typ list -> int -> int
   196   val maxidx_term: term -> int -> int
   197   val invent_names: string list -> string -> int -> string list
   198   val dest_abs: string * typ * term -> string * term
   199   val bound: int -> string
   200   val is_bound: string -> bool
   201   val zero_var_indexesT: typ -> typ
   202   val zero_var_indexes: term -> term
   203   val zero_var_indexes_inst: term ->
   204     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   205   val dummy_patternN: string
   206   val dummy_pattern: typ -> term
   207   val no_dummy_patterns: term -> term
   208   val replace_dummy_patterns: int * term -> int * term
   209   val is_replaced_dummy_pattern: indexname -> bool
   210   val show_dummy_patterns: term -> term
   211   val adhoc_freeze_vars: term -> term * string list
   212   val string_of_vname: indexname -> string
   213   val string_of_vname': indexname -> string
   214   val str_of_term: term -> string
   215 end;
   216 
   217 structure Term: TERM =
   218 struct
   219 
   220 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   221   for resolution.*)
   222 type indexname = string * int;
   223 
   224 (* Types are classified by sorts. *)
   225 type class = string;
   226 type sort  = class list;
   227 type arity = string * sort list * sort;
   228 
   229 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   230 datatype typ = Type  of string * typ list
   231              | TFree of string * sort
   232              | TVar  of indexname * sort;
   233 
   234 (*Terms.  Bound variables are indicated by depth number.
   235   Free variables, (scheme) variables and constants have names.
   236   An term is "closed" if every bound variable of level "lev"
   237   is enclosed by at least "lev" abstractions.
   238 
   239   It is possible to create meaningless terms containing loose bound vars
   240   or type mismatches.  But such terms are not allowed in rules. *)
   241 
   242 datatype term =
   243     Const of string * typ
   244   | Free  of string * typ
   245   | Var   of indexname * typ
   246   | Bound of int
   247   | Abs   of string*typ*term
   248   | op $  of term*term;
   249 
   250 (*Errors involving type mismatches*)
   251 exception TYPE of string * typ list * term list;
   252 
   253 (*Errors errors involving terms*)
   254 exception TERM of string * term list;
   255 
   256 (*Note variable naming conventions!
   257     a,b,c: string
   258     f,g,h: functions (including terms of function type)
   259     i,j,m,n: int
   260     t,u: term
   261     v,w: indexnames
   262     x,y: any
   263     A,B,C: term (denoting formulae)
   264     T,U: typ
   265 *)
   266 
   267 
   268 (** Types **)
   269 
   270 (*dummy type for parsing and printing etc.*)
   271 val dummyT = Type ("dummy", []);
   272 
   273 fun no_dummyT typ =
   274   let
   275     fun check (T as Type ("dummy", _)) =
   276           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   277       | check (Type (_, Ts)) = List.app check Ts
   278       | check _ = ();
   279   in check typ; typ end;
   280 
   281 fun S --> T = Type("fun",[S,T]);
   282 
   283 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   284 val op ---> = Library.foldr (op -->);
   285 
   286 fun dest_Type (Type x) = x
   287   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   288 fun dest_TVar (TVar x) = x
   289   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   290 fun dest_TFree (TFree x) = x
   291   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   292 
   293 
   294 (** Discriminators **)
   295 
   296 fun is_Bound (Bound _) = true
   297   | is_Bound _         = false;
   298 
   299 fun is_Const (Const _) = true
   300   | is_Const _ = false;
   301 
   302 fun is_Free (Free _) = true
   303   | is_Free _ = false;
   304 
   305 fun is_Var (Var _) = true
   306   | is_Var _ = false;
   307 
   308 fun is_TVar (TVar _) = true
   309   | is_TVar _ = false;
   310 
   311 (*Differs from proofterm/is_fun in its treatment of TVar*)
   312 fun is_funtype (Type("fun",[_,_])) = true
   313   | is_funtype _ = false;
   314 
   315 
   316 (** Destructors **)
   317 
   318 fun dest_Const (Const x) =  x
   319   | dest_Const t = raise TERM("dest_Const", [t]);
   320 
   321 fun dest_Free (Free x) =  x
   322   | dest_Free t = raise TERM("dest_Free", [t]);
   323 
   324 fun dest_Var (Var x) =  x
   325   | dest_Var t = raise TERM("dest_Var", [t]);
   326 
   327 
   328 fun domain_type (Type("fun", [T,_])) = T
   329 and range_type  (Type("fun", [_,T])) = T;
   330 
   331 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   332 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   333   | binder_types _   =  [];
   334 
   335 (* maps  [T1,...,Tn]--->T  to T*)
   336 fun body_type (Type("fun",[S,T])) = body_type T
   337   | body_type T   =  T;
   338 
   339 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   340 fun strip_type T : typ list * typ =
   341   (binder_types T, body_type T);
   342 
   343 
   344 (*Compute the type of the term, checking that combinations are well-typed
   345   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   346 fun type_of1 (Ts, Const (_,T)) = T
   347   | type_of1 (Ts, Free  (_,T)) = T
   348   | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
   349         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   350   | type_of1 (Ts, Var (_,T)) = T
   351   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   352   | type_of1 (Ts, f$u) =
   353       let val U = type_of1(Ts,u)
   354           and T = type_of1(Ts,f)
   355       in case T of
   356             Type("fun",[T1,T2]) =>
   357               if T1=U then T2  else raise TYPE
   358                     ("type_of: type mismatch in application", [T1,U], [f$u])
   359           | _ => raise TYPE
   360                     ("type_of: function type is expected in application",
   361                      [T,U], [f$u])
   362       end;
   363 
   364 fun type_of t : typ = type_of1 ([],t);
   365 
   366 (*Determines the type of a term, with minimal checking*)
   367 fun fastype_of1 (Ts, f$u) =
   368     (case fastype_of1 (Ts,f) of
   369         Type("fun",[_,T]) => T
   370         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   371   | fastype_of1 (_, Const (_,T)) = T
   372   | fastype_of1 (_, Free (_,T)) = T
   373   | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
   374          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   375   | fastype_of1 (_, Var (_,T)) = T
   376   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   377 
   378 fun fastype_of t : typ = fastype_of1 ([],t);
   379 
   380 (*Determine the argument type of a function*)
   381 fun argument_type_of tm =
   382   let
   383     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   384       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   385 
   386     fun arg 0 _ (Abs (_, T, _)) = T
   387       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   388       | arg i Ts (t $ _) = arg (i + 1) Ts t
   389       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   390   in arg 0 [] tm end;
   391 
   392 
   393 val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
   394 
   395 fun strip_abs (Abs (a, T, t)) =
   396       let val (a', t') = strip_abs t
   397       in ((a, T) :: a', t') end
   398   | strip_abs t = ([], t);
   399 
   400 (* maps  (x1,...,xn)t   to   t  *)
   401 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   402   | strip_abs_body u  =  u;
   403 
   404 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   405 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   406   | strip_abs_vars u  =  [] : (string*typ) list;
   407 
   408 
   409 fun strip_qnt_body qnt =
   410 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   411       | strip t = t
   412 in strip end;
   413 
   414 fun strip_qnt_vars qnt =
   415 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   416       | strip t  =  [] : (string*typ) list
   417 in strip end;
   418 
   419 
   420 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   421 val list_comb : term * term list -> term = Library.foldl (op $);
   422 
   423 
   424 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   425 fun strip_comb u : term * term list =
   426     let fun stripc (f$t, ts) = stripc (f, t::ts)
   427         |   stripc  x =  x
   428     in  stripc(u,[])  end;
   429 
   430 
   431 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   432 fun head_of (f$t) = head_of f
   433   | head_of u = u;
   434 
   435 
   436 (*number of atoms and abstractions in a term*)
   437 fun size_of_term tm =
   438   let
   439     fun add_size (t $ u, n) = add_size (t, add_size (u, n))
   440       | add_size (Abs (_ ,_, t), n) = add_size (t, n + 1)
   441       | add_size (_, n) = n + 1;
   442   in add_size (tm, 0) end;
   443 
   444 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   445   | map_atyps f T = T;
   446 
   447 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   448   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   449   | map_aterms f t = f t;
   450 
   451 fun map_type_tvar f =
   452   let
   453     fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
   454       | map_aux (TVar x) = f x
   455       | map_aux T = T;
   456   in map_aux end;
   457 
   458 fun map_type_tfree f =
   459   let
   460     fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
   461       | map_aux (TFree x) = f x
   462       | map_aux T = T;
   463   in map_aux end;
   464 
   465 fun map_term_types f =
   466   let
   467     fun map_aux (Const (a, T)) = Const (a, f T)
   468       | map_aux (Free (a, T)) = Free (a, f T)
   469       | map_aux (Var (v, T)) = Var (v, f T)
   470       | map_aux (t as Bound _)  = t
   471       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   472       | map_aux (t $ u) = map_aux t $ map_aux u;
   473   in map_aux end;
   474 
   475 (* iterate a function over all types in a term *)
   476 fun it_term_types f =
   477 let fun iter(Const(_,T), a) = f(T,a)
   478       | iter(Free(_,T), a) = f(T,a)
   479       | iter(Var(_,T), a) = f(T,a)
   480       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   481       | iter(f$u, a) = iter(f, iter(u, a))
   482       | iter(Bound _, a) = a
   483 in iter end
   484 
   485 
   486 (* fold types and terms *)
   487 
   488 (*fold atoms of type*)
   489 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   490   | fold_atyps f T = f T;
   491 
   492 (*fold atoms of term*)
   493 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   494   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   495   | fold_aterms f a = f a;
   496 
   497 (*fold types of term*)
   498 fun fold_term_types f (t as Const (_, T)) = f t T
   499   | fold_term_types f (t as Free (_, T)) = f t T
   500   | fold_term_types f (t as Var (_, T)) = f t T
   501   | fold_term_types f (Bound _) = I
   502   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   503   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   504 
   505 fun fold_types f = fold_term_types (K f);
   506 
   507 (*collect variables*)
   508 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   509 val add_tvars = fold_types add_tvarsT;
   510 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   511 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   512 val add_tfrees = fold_types add_tfreesT;
   513 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   514 
   515 (*collect variable names*)
   516 val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   517 fun term_varnames t = add_term_varnames t [];
   518 
   519 fun find_free t x =
   520   let
   521     exception Found of term;
   522     fun find (t as Free (x', _)) = if x = x' then raise Found t else I
   523       | find _ = I;
   524   in (fold_aterms find t (); NONE) handle Found v => SOME v end;
   525 
   526 
   527 
   528 (** Comparing terms, types, sorts etc. **)
   529 
   530 (* fast syntactic comparison *)
   531 
   532 fun fast_indexname_ord ((x, i), (y, j)) =
   533   (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   534 
   535 fun sort_ord SS =
   536   if pointer_eq SS then EQUAL
   537   else dict_ord fast_string_ord SS;
   538 
   539 local
   540 
   541 fun cons_nr (TVar _) = 0
   542   | cons_nr (TFree _) = 1
   543   | cons_nr (Type _) = 2;
   544 
   545 in
   546 
   547 fun typ_ord TU =
   548   if pointer_eq TU then EQUAL
   549   else
   550     (case TU of
   551       (Type (a, Ts), Type (b, Us)) =>
   552         (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   553     | (TFree (a, S), TFree (b, S')) =>
   554         (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   555     | (TVar (xi, S), TVar (yj, S')) =>
   556         (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
   557     | (T, U) => int_ord (cons_nr T, cons_nr U));
   558 
   559 end;
   560 
   561 local
   562 
   563 fun cons_nr (Const _) = 0
   564   | cons_nr (Free _) = 1
   565   | cons_nr (Var _) = 2
   566   | cons_nr (Bound _) = 3
   567   | cons_nr (Abs _) = 4
   568   | cons_nr (_ $ _) = 5;
   569 
   570 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   571   | struct_ord (t1 $ t2, u1 $ u2) =
   572       (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   573   | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
   574 
   575 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   576   | atoms_ord (t1 $ t2, u1 $ u2) =
   577       (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   578   | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   579   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   580   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   581   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   582   | atoms_ord _ = sys_error "atoms_ord";
   583 
   584 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
   585       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   586   | types_ord (t1 $ t2, u1 $ u2) =
   587       (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   588   | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   589   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   590   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   591   | types_ord (Bound _, Bound _) = EQUAL
   592   | types_ord _ = sys_error "types_ord";
   593 
   594 in
   595 
   596 fun fast_term_ord tu =
   597   if pointer_eq tu then EQUAL
   598   else
   599     (case struct_ord tu of
   600       EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
   601     | ord => ord);
   602 
   603 fun op aconv tu = (fast_term_ord tu = EQUAL);
   604 fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL);
   605 
   606 structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
   607 structure Typtab = TableFun(type key = typ val ord = typ_ord);
   608 structure Termtab = TableFun(type key = term val ord = fast_term_ord);
   609 
   610 end;
   611 
   612 
   613 (* term_ord *)
   614 
   615 (*a linear well-founded AC-compatible ordering for terms:
   616   s < t <=> 1. size(s) < size(t) or
   617             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   618             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   619                (s1..sn) < (t1..tn) (lexicographically)*)
   620 
   621 fun indexname_ord ((x, i), (y, j)) =
   622   (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   623 
   624 local
   625 
   626 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
   627   | hd_depth p = p;
   628 
   629 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   630   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   631   | dest_hd (Var v) = (v, 2)
   632   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   633   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   634 
   635 in
   636 
   637 fun term_ord tu =
   638   if pointer_eq tu then EQUAL
   639   else
   640     (case tu of
   641       (Abs (_, T, t), Abs(_, U, u)) =>
   642         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   643     | (t, u) =>
   644         (case int_ord (size_of_term t, size_of_term u) of
   645           EQUAL =>
   646             (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
   647               EQUAL => args_ord (t, u) | ord => ord)
   648         | ord => ord))
   649 and hd_ord (f, g) =
   650   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   651 and args_ord (f $ t, g $ u) =
   652       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   653   | args_ord _ = EQUAL;
   654 
   655 fun termless tu = (term_ord tu = LESS);
   656 
   657 end;
   658 
   659 
   660 (** Lexicographic path order on terms **)
   661 
   662 (*
   663   See Baader & Nipkow, Term rewriting, CUP 1998.
   664   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   665   constants.
   666 
   667   f_ord maps strings to integers and serves two purposes:
   668   - Predicate on constant symbols.  Those that are not recognised by f_ord
   669     must be mapped to ~1.
   670   - Order on the recognised symbols.  These must be mapped to distinct
   671     integers >= 0.
   672 
   673 *)
   674 
   675 local
   676 fun dest_hd f_ord (Const (a, T)) =
   677       let val ord = f_ord a in
   678         if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
   679       end
   680   | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
   681   | dest_hd _ (Var v) = ((1, v), 1)
   682   | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
   683   | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
   684 
   685 fun term_lpo f_ord (s, t) =
   686   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
   687     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
   688     then case hd_ord f_ord (f, g) of
   689         GREATER =>
   690           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   691           then GREATER else LESS
   692       | EQUAL =>
   693           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   694           then list_ord (term_lpo f_ord) (ss, ts)
   695           else LESS
   696       | LESS => LESS
   697     else GREATER
   698   end
   699 and hd_ord f_ord (f, g) = case (f, g) of
   700     (Abs (_, T, t), Abs (_, U, u)) =>
   701       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   702   | (_, _) => prod_ord (prod_ord int_ord
   703                   (prod_ord indexname_ord typ_ord)) int_ord
   704                 (dest_hd f_ord f, dest_hd f_ord g)
   705 in
   706 val term_lpo = term_lpo
   707 end;
   708 
   709 
   710 (** Connectives of higher order logic **)
   711 
   712 fun itselfT ty = Type ("itself", [ty]);
   713 val a_itselfT = itselfT (TFree ("'a", []));
   714 
   715 val propT : typ = Type("prop",[]);
   716 
   717 val implies = Const("==>", propT-->propT-->propT);
   718 
   719 fun all T = Const("all", (T-->propT)-->propT);
   720 
   721 fun equals T = Const("==", T-->T-->propT);
   722 
   723 (* maps  !!x1...xn. t   to   t  *)
   724 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   725   | strip_all_body t  =  t;
   726 
   727 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   728 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   729                 (a,T) :: strip_all_vars t
   730   | strip_all_vars t  =  [] : (string*typ) list;
   731 
   732 (*increments a term's non-local bound variables
   733   required when moving a term within abstractions
   734      inc is  increment for bound variables
   735      lev is  level at which a bound variable is considered 'loose'*)
   736 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   737   | incr_bv (inc, lev, Abs(a,T,body)) =
   738         Abs(a, T, incr_bv(inc,lev+1,body))
   739   | incr_bv (inc, lev, f$t) =
   740       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   741   | incr_bv (inc, lev, u) = u;
   742 
   743 fun incr_boundvars  0  t = t
   744   | incr_boundvars inc t = incr_bv(inc,0,t);
   745 
   746 (*Scan a pair of terms; while they are similar,
   747   accumulate corresponding bound vars in "al"*)
   748 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   749       match_bvs(s, t, if x="" orelse y="" then al
   750                                           else (x,y)::al)
   751   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   752   | match_bvs(_,_,al) = al;
   753 
   754 (* strip abstractions created by parameters *)
   755 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   756 
   757 fun rename_abs pat obj t =
   758   let
   759     val ren = match_bvs (pat, obj, []);
   760     fun ren_abs (Abs (x, T, b)) =
   761           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   762       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   763       | ren_abs t = t
   764   in if null ren then NONE else SOME (ren_abs t) end;
   765 
   766 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   767    (Bound 0) is loose at level 0 *)
   768 fun add_loose_bnos (Bound i, lev, js) =
   769         if i<lev then js  else  (i-lev) ins_int js
   770   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   771   | add_loose_bnos (f$t, lev, js) =
   772         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   773   | add_loose_bnos (_, _, js) = js;
   774 
   775 fun loose_bnos t = add_loose_bnos (t, 0, []);
   776 
   777 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   778    level k or beyond. *)
   779 fun loose_bvar(Bound i,k) = i >= k
   780   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   781   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   782   | loose_bvar _ = false;
   783 
   784 fun loose_bvar1(Bound i,k) = i = k
   785   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   786   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   787   | loose_bvar1 _ = false;
   788 
   789 (*Substitute arguments for loose bound variables.
   790   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   791   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   792         and the appropriate call is  subst_bounds([b,a], c) .
   793   Loose bound variables >=n are reduced by "n" to
   794      compensate for the disappearance of lambdas.
   795 *)
   796 fun subst_bounds (args: term list, t) : term =
   797   let val n = length args;
   798       fun subst (t as Bound i, lev) =
   799            (if i<lev then  t    (*var is locally bound*)
   800             else  incr_boundvars lev (List.nth(args, i-lev))
   801                     handle Subscript => Bound(i-n)  (*loose: change it*))
   802         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   803         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   804         | subst (t,lev) = t
   805   in   case args of [] => t  | _ => subst (t,0)  end;
   806 
   807 (*Special case: one argument*)
   808 fun subst_bound (arg, t) : term =
   809   let fun subst (t as Bound i, lev) =
   810             if i<lev then  t    (*var is locally bound*)
   811             else  if i=lev then incr_boundvars lev arg
   812                            else Bound(i-1)  (*loose: change it*)
   813         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   814         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   815         | subst (t,lev) = t
   816   in  subst (t,0)  end;
   817 
   818 (*beta-reduce if possible, else form application*)
   819 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   820   | betapply (f,u) = f$u;
   821 
   822 val betapplys = Library.foldl betapply;
   823 
   824 
   825 (** Specialized equality, membership, insertion etc. **)
   826 
   827 (* indexnames *)
   828 
   829 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   830 
   831 fun mem_ix (_, []) = false
   832   | mem_ix (x, y :: ys) = eq_ix (x, y) orelse mem_ix (x, ys);
   833 
   834 fun ins_ix (x, xs) = if mem_ix (x, xs) then xs else x :: xs;
   835 
   836 
   837 (* variables *)
   838 
   839 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   840 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   841 
   842 val tvar_ord = prod_ord indexname_ord sort_ord;
   843 val var_ord = prod_ord indexname_ord typ_ord;
   844 
   845 
   846 (* terms *)
   847 
   848 fun mem_term (_, []) = false
   849   | mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts);
   850 
   851 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   852 
   853 
   854 (*A fast unification filter: true unless the two terms cannot be unified.
   855   Terms must be NORMAL.  Treats all Vars as distinct. *)
   856 fun could_unify (t,u) =
   857   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   858         | matchrands _ = true
   859   in case (head_of t , head_of u) of
   860         (_, Var _) => true
   861       | (Var _, _) => true
   862       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   863       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   864       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   865       | (Abs _, _) =>  true   (*because of possible eta equality*)
   866       | (_, Abs _) =>  true
   867       | _ => false
   868   end;
   869 
   870 (*Substitute new for free occurrences of old in a term*)
   871 fun subst_free [] = (fn t=>t)
   872   | subst_free pairs =
   873       let fun substf u =
   874             case AList.lookup (op aconv) pairs u of
   875                 SOME u' => u'
   876               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   877                                  | t$u' => substf t $ substf u'
   878                                  | _ => u)
   879       in  substf  end;
   880 
   881 (*a total, irreflexive ordering on index names*)
   882 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   883 
   884 
   885 (*Abstraction of the term "body" over its occurrences of v,
   886     which must contain no loose bound variables.
   887   The resulting term is ready to become the body of an Abs.*)
   888 fun abstract_over (v, body) =
   889   let
   890     exception SAME;
   891     fun abs lev tm =
   892       if v aconv tm then Bound lev
   893       else
   894         (case tm of
   895           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   896         | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
   897         | _ => raise SAME);
   898   in abs 0 body handle SAME => body end;
   899 
   900 fun lambda (v as Const (x, T)) t = Abs (NameSpace.base x, T, abstract_over (v, t))
   901   | lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   902   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   903   | lambda v t = raise TERM ("lambda", [v, t]);
   904 
   905 (*Form an abstraction over a free variable.*)
   906 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   907 fun absdummy (T, body) = Abs ("uu", T, body);
   908 
   909 (*Abstraction over a list of free variables*)
   910 fun list_abs_free ([ ] ,     t) = t
   911   | list_abs_free ((a,T)::vars, t) =
   912       absfree(a, T, list_abs_free(vars,t));
   913 
   914 (*Quantification over a list of free variables*)
   915 fun list_all_free ([], t: term) = t
   916   | list_all_free ((a,T)::vars, t) =
   917         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   918 
   919 (*Quantification over a list of variables (already bound in body) *)
   920 fun list_all ([], t) = t
   921   | list_all ((a,T)::vars, t) =
   922         (all T) $ (Abs(a, T, list_all(vars,t)));
   923 
   924 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   925   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   926 fun subst_atomic [] tm = tm
   927   | subst_atomic inst tm =
   928       let
   929         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   930           | subst (t $ u) = subst t $ subst u
   931           | subst t = the_default t (AList.lookup (op aconv) inst t);
   932       in subst tm end;
   933 
   934 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   935 fun typ_subst_atomic [] ty = ty
   936   | typ_subst_atomic inst ty =
   937       let
   938         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   939           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   940       in subst ty end;
   941 
   942 fun subst_atomic_types [] tm = tm
   943   | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
   944 
   945 fun typ_subst_TVars [] ty = ty
   946   | typ_subst_TVars inst ty =
   947       let
   948         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   949           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   950           | subst T = T;
   951       in subst ty end;
   952 
   953 fun subst_TVars [] tm = tm
   954   | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
   955 
   956 (*see also Envir.norm_term*)
   957 fun subst_Vars [] tm = tm
   958   | subst_Vars inst tm =
   959       let
   960         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   961           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   962           | subst (t $ u) = subst t $ subst u
   963           | subst t = t;
   964       in subst tm end;
   965 
   966 (*see also Envir.norm_term*)
   967 fun subst_vars ([], []) tm = tm
   968   | subst_vars ([], inst) tm = subst_Vars inst tm
   969   | subst_vars (instT, inst) tm =
   970       let
   971         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   972           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   973           | subst (t as Var (xi, T)) =
   974               (case AList.lookup (op =) inst xi of
   975                 NONE => Var (xi, typ_subst_TVars instT T)
   976               | SOME t => t)
   977           | subst (t as Bound _) = t
   978           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   979           | subst (t $ u) = subst t $ subst u;
   980       in subst tm end;
   981 
   982 
   983 (* instantiation of schematic variables (types before terms) *)
   984 
   985 local exception SAME in
   986 
   987 fun instantiateT_same [] _ = raise SAME
   988   | instantiateT_same instT ty =
   989       let
   990         fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
   991           | subst_typ (TVar v) =
   992               (case AList.lookup eq_tvar instT v of
   993                 SOME T => T
   994               | NONE => raise SAME)
   995           | subst_typ _ = raise SAME
   996         and subst_typs (T :: Ts) =
   997             (subst_typ T :: (subst_typs Ts handle SAME => Ts)
   998               handle SAME => T :: subst_typs Ts)
   999           | subst_typs [] = raise SAME;
  1000       in subst_typ ty end;
  1001 
  1002 fun instantiate ([], []) tm = tm
  1003   | instantiate (instT, inst) tm =
  1004       let
  1005         val substT = instantiateT_same instT;
  1006         fun subst (Const (c, T)) = Const (c, substT T)
  1007           | subst (Free (x, T)) = Free (x, substT T)
  1008           | subst (Var (xi, T)) =
  1009               let val (T', same) = (substT T, false) handle SAME => (T, true) in
  1010                 (case AList.lookup eq_var inst (xi, T') of
  1011                    SOME t => t
  1012                  | NONE => if same then raise SAME else Var (xi, T'))
  1013               end
  1014           | subst (Bound _) = raise SAME
  1015           | subst (Abs (x, T, t)) =
  1016               (Abs (x, substT T, subst t handle SAME => t)
  1017                 handle SAME => Abs (x, T, subst t))
  1018           | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u);
  1019       in subst tm handle SAME => tm end;
  1020 
  1021 fun instantiateT instT ty =
  1022   instantiateT_same instT ty handle SAME => ty;
  1023 
  1024 end;
  1025 
  1026 
  1027 (** Identifying first-order terms **)
  1028 
  1029 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
  1030 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
  1031 
  1032 (*First order means in all terms of the form f(t1,...,tn) no argument has a
  1033   function type. The supplied quantifiers are excluded: their argument always
  1034   has a function type through a recursive call into its body.*)
  1035 fun is_first_order quants =
  1036   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
  1037         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
  1038             q mem_string quants  andalso   (*it is a known quantifier*)
  1039             not (is_funtype T)   andalso first_order1 (T::Ts) body
  1040         | first_order1 Ts t =
  1041             case strip_comb t of
  1042                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1043                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1044                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1045                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1046                | (Abs _, ts) => false (*not in beta-normal form*)
  1047                | _ => error "first_order: unexpected case"
  1048     in  first_order1 []  end;
  1049 
  1050 
  1051 (* maximum index of typs and terms *)
  1052 
  1053 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
  1054   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
  1055   | maxidx_typ (TFree _) i = i
  1056 and maxidx_typs [] i = i
  1057   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
  1058 
  1059 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
  1060   | maxidx_term (Const (_, T)) i = maxidx_typ T i
  1061   | maxidx_term (Free (_, T)) i = maxidx_typ T i
  1062   | maxidx_term (Bound _) i = i
  1063   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
  1064   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
  1065 
  1066 fun maxidx_of_typ T = maxidx_typ T ~1;
  1067 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
  1068 fun maxidx_of_term t = maxidx_term t ~1;
  1069 
  1070 
  1071 
  1072 (**** Syntax-related declarations ****)
  1073 
  1074 (*** Printing ***)
  1075 
  1076 (*Makes a variant of a name distinct from the names in 'used'.
  1077   First attaches the suffix and then increments this;
  1078   preserves a suffix of underscores "_". *)
  1079 fun variant used name =
  1080   let
  1081     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
  1082     fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c;
  1083     fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c;
  1084   in vary1 (if c = "" then "u" else c) ^ u end;
  1085 
  1086 (*Create variants of the list of names, with priority to the first ones*)
  1087 fun variantlist ([], used) = []
  1088   | variantlist(b::bs, used) =
  1089       let val b' = variant used b
  1090       in  b' :: variantlist (bs, b'::used)  end;
  1091 
  1092 (*Invent fresh names*)
  1093 fun invent_names _ _ 0 = []
  1094   | invent_names used a n =
  1095       let val b = Symbol.bump_string a in
  1096         if a mem_string used then invent_names used b n
  1097         else a :: invent_names used b (n - 1)
  1098       end;
  1099 
  1100 
  1101 (** Consts etc. **)
  1102 
  1103 fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
  1104   | add_typ_classes (TFree (_, S), cs) = S union cs
  1105   | add_typ_classes (TVar (_, S), cs) = S union cs;
  1106 
  1107 fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
  1108   | add_typ_tycons (_, cs) = cs;
  1109 
  1110 val add_term_classes = it_term_types add_typ_classes;
  1111 val add_term_tycons = it_term_types add_typ_tycons;
  1112 
  1113 fun add_term_consts (Const (c, _), cs) = c ins_string cs
  1114   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
  1115   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
  1116   | add_term_consts (_, cs) = cs;
  1117 
  1118 fun term_consts t = add_term_consts(t,[]);
  1119 
  1120 fun exists_subterm P =
  1121   let
  1122     fun ex tm = P tm orelse
  1123       (case tm of
  1124         t $ u => ex t orelse ex u
  1125       | Abs (_, _, t) => ex t
  1126       | _ => false);
  1127   in ex end;
  1128 
  1129 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
  1130 
  1131 
  1132 (** TFrees and TVars **)
  1133 
  1134 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
  1135 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
  1136   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  1137   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  1138   | add_term_free_names (_, bs) = bs;
  1139 
  1140 (*Accumulates the names in the term, suppressing duplicates.
  1141   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  1142 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
  1143   | add_term_names (Free(a,_), bs) = a ins_string bs
  1144   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  1145   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  1146   | add_term_names (_, bs) = bs;
  1147 
  1148 (*Accumulates the TVars in a type, suppressing duplicates. *)
  1149 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
  1150   | add_typ_tvars(TFree(_),vs) = vs
  1151   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  1152 
  1153 (*Accumulates the TFrees in a type, suppressing duplicates. *)
  1154 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
  1155   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
  1156   | add_typ_tfree_names(TVar(_),fs) = fs;
  1157 
  1158 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
  1159   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  1160   | add_typ_tfrees(TVar(_),fs) = fs;
  1161 
  1162 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
  1163   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
  1164   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
  1165 
  1166 (*Accumulates the TVars in a term, suppressing duplicates. *)
  1167 val add_term_tvars = it_term_types add_typ_tvars;
  1168 
  1169 (*Accumulates the TFrees in a term, suppressing duplicates. *)
  1170 val add_term_tfrees = it_term_types add_typ_tfrees;
  1171 val add_term_tfree_names = it_term_types add_typ_tfree_names;
  1172 
  1173 val add_term_tvarnames = it_term_types add_typ_varnames;
  1174 
  1175 (*Non-list versions*)
  1176 fun typ_tfrees T = add_typ_tfrees(T,[]);
  1177 fun typ_tvars T = add_typ_tvars(T,[]);
  1178 fun term_tfrees t = add_term_tfrees(t,[]);
  1179 fun term_tvars t = add_term_tvars(t,[]);
  1180 
  1181 (*special code to enforce left-to-right collection of TVar-indexnames*)
  1182 
  1183 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
  1184   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
  1185                                      else ixns@[ixn]
  1186   | add_typ_ixns(ixns,TFree(_)) = ixns;
  1187 
  1188 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1189   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1190   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1191   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1192   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1193       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1194   | add_term_tvar_ixns(f$t,ixns) =
  1195       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1196 
  1197 
  1198 (** Frees and Vars **)
  1199 
  1200 (*Accumulates the Vars in the term, suppressing duplicates*)
  1201 fun add_term_vars (t, vars: term list) = case t of
  1202     Var   _ => OrdList.insert term_ord t vars
  1203   | Abs (_,_,body) => add_term_vars(body,vars)
  1204   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1205   | _ => vars;
  1206 
  1207 fun term_vars t = add_term_vars(t,[]);
  1208 
  1209 (*Accumulates the Frees in the term, suppressing duplicates*)
  1210 fun add_term_frees (t, frees: term list) = case t of
  1211     Free   _ => OrdList.insert term_ord t frees
  1212   | Abs (_,_,body) => add_term_frees(body,frees)
  1213   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1214   | _ => frees;
  1215 
  1216 fun term_frees t = add_term_frees(t,[]);
  1217 
  1218 (*Given an abstraction over P, replaces the bound variable by a Free variable
  1219   having a unique name -- SLOW!*)
  1220 fun variant_abs (a,T,P) =
  1221   let val b = variant (add_term_names(P,[])) a
  1222   in  (b,  subst_bound (Free(b,T), P))  end;
  1223 
  1224 fun dest_abs (x, T, body) =
  1225   let
  1226     fun name_clash (Free (y, _)) = (x = y)
  1227       | name_clash (t $ u) = name_clash t orelse name_clash u
  1228       | name_clash (Abs (_, _, t)) = name_clash t
  1229       | name_clash _ = false;
  1230   in
  1231     if name_clash body then
  1232       dest_abs (variant [x] x, T, body)    (*potentially slow, but rarely happens*)
  1233     else (x, subst_bound (Free (x, T), body))
  1234   end;
  1235 
  1236 (*names for numbered variables --
  1237   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
  1238 local
  1239   val small_int = Vector.tabulate (1000, fn i =>
  1240     let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
  1241     in ":" ^ leading ^ string_of_int i end);
  1242 in
  1243   fun bound n =
  1244     if n < 1000 then Vector.sub (small_int, n)
  1245     else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
  1246 end;
  1247 
  1248 val is_bound = String.isPrefix ":";
  1249 
  1250 (* renames and reverses the strings in vars away from names *)
  1251 fun rename_aTs names vars : (string*typ)list =
  1252   let fun rename_aT (vars,(a,T)) =
  1253                 (variant (map #1 vars @ names) a, T) :: vars
  1254   in Library.foldl rename_aT ([],vars) end;
  1255 
  1256 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
  1257 
  1258 
  1259 (* zero var indexes *)
  1260 
  1261 fun zero_var_inst vars =
  1262   fold (fn v as ((x, i), X) => fn (used, inst) =>
  1263     let
  1264       val x' = variant used (if is_bound x then "u" else x);
  1265       val used' = x' :: used;
  1266     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
  1267   vars ([], []) |> #2;
  1268 
  1269 fun zero_var_indexesT ty =
  1270   instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
  1271 
  1272 fun zero_var_indexes_inst tm =
  1273   let
  1274     val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm [])));
  1275     val inst =
  1276       add_vars tm [] |> map (apsnd (instantiateT instT))
  1277       |> sort var_ord |> zero_var_inst |> map (apsnd Var);
  1278   in (instT, inst) end;
  1279 
  1280 fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm;
  1281 
  1282 
  1283 (* dummy patterns *)
  1284 
  1285 val dummy_patternN = "dummy_pattern";
  1286 
  1287 fun dummy_pattern T = Const (dummy_patternN, T);
  1288 
  1289 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1290   | is_dummy_pattern _ = false;
  1291 
  1292 fun no_dummy_patterns tm =
  1293   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  1294   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1295 
  1296 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1297       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1298   | replace_dummy Ts (i, Abs (x, T, t)) =
  1299       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1300       in (i', Abs (x, T, t')) end
  1301   | replace_dummy Ts (i, t $ u) =
  1302       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1303       in (i'', t' $ u') end
  1304   | replace_dummy _ (i, a) = (i, a);
  1305 
  1306 val replace_dummy_patterns = replace_dummy [];
  1307 
  1308 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1309   | is_replaced_dummy_pattern _ = false;
  1310 
  1311 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1312   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1313   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1314   | show_dummy_patterns a = a;
  1315 
  1316 
  1317 (* adhoc freezing *)
  1318 
  1319 fun adhoc_freeze_vars tm =
  1320   let
  1321     fun mk_inst (var as Var ((a, i), T)) =
  1322       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1323       in ((var,  Free(x, T)), x) end;
  1324     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1325   in (subst_atomic insts tm, xs) end;
  1326 
  1327 
  1328 (* string_of_vname *)
  1329 
  1330 val show_question_marks = ref true;
  1331 
  1332 fun string_of_vname (x, i) =
  1333   let
  1334     val question_mark = if ! show_question_marks then "?" else "";
  1335     val idx = string_of_int i;
  1336     val dot =
  1337       (case rev (Symbol.explode x) of
  1338         _ :: "\\<^isub>" :: _ => false
  1339       | _ :: "\\<^isup>" :: _ => false
  1340       | c :: _ => Symbol.is_digit c
  1341       | _ => true);
  1342   in
  1343     if dot then question_mark ^ x ^ "." ^ idx
  1344     else if i <> 0 then question_mark ^ x ^ idx
  1345     else question_mark ^ x
  1346   end;
  1347 
  1348 fun string_of_vname' (x, ~1) = x
  1349   | string_of_vname' xi = string_of_vname xi;
  1350 
  1351 
  1352 (* str_of_term *)
  1353 
  1354 fun str_of_term (Const (c, _)) = c
  1355   | str_of_term (Free (x, _)) = x
  1356   | str_of_term (Var (xi, _)) = string_of_vname xi
  1357   | str_of_term (Bound i) = string_of_int i
  1358   | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
  1359   | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
  1360 
  1361 end;
  1362 
  1363 structure BasicTerm: BASIC_TERM = Term;
  1364 open BasicTerm;