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