src/Pure/term.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15573 cf53c2dcf440
permissions -rw-r--r--
Move towards standard functions.
     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   val --> : typ * typ -> typ
    25   val ---> : typ list * typ -> typ
    26   val is_TVar: typ -> bool
    27   val domain_type: typ -> typ
    28   val range_type: typ -> typ
    29   val binder_types: typ -> typ list
    30   val body_type: typ -> typ
    31   val strip_type: typ -> typ list * typ
    32   datatype term =
    33     Const of string * typ |
    34     Free of string * typ |
    35     Var of indexname * typ |
    36     Bound of int |
    37     Abs of string * typ * term |
    38     $ of term * term
    39   structure Vartab : TABLE
    40   structure Typtab : TABLE
    41   structure Termtab : TABLE
    42   exception TYPE of string * typ list * term list
    43   exception TERM of string * term list
    44   val is_Bound: term -> bool
    45   val is_Const: term -> bool
    46   val is_Free: term -> bool
    47   val is_Var: term -> bool
    48   val dest_Type: typ -> string * typ list
    49   val dest_Const: term -> string * typ
    50   val dest_Free: term -> string * typ
    51   val dest_Var: term -> indexname * typ
    52   val type_of: term -> typ
    53   val type_of1: typ list * term -> typ
    54   val fastype_of: term -> typ
    55   val fastype_of1: typ list * term -> typ
    56   val list_abs: (string * typ) list * term -> term
    57   val strip_abs_body: term -> term
    58   val strip_abs_vars: term -> (string * typ) list
    59   val strip_qnt_body: string -> term -> term
    60   val strip_qnt_vars: string -> term -> (string * typ) list
    61   val list_comb: term * term list -> term
    62   val strip_comb: term -> term * term list
    63   val head_of: term -> term
    64   val size_of_term: term -> int
    65   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    66   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    67   val map_term_types: (typ -> typ) -> term -> term
    68   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    69   val map_typ: (class -> class) -> (string -> string) -> typ -> typ
    70   val map_term:
    71      (class -> class) ->
    72      (string -> string) -> (string -> string) -> term -> term
    73   val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    74   val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    75   val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    76   val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
    77   val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
    78   val add_term_varnames: indexname list * term -> indexname list
    79   val term_varnames: term -> indexname list
    80   val dummyT: typ
    81   val itselfT: typ -> typ
    82   val a_itselfT: typ
    83   val propT: typ
    84   val implies: term
    85   val all: typ -> term
    86   val equals: typ -> term
    87   val strip_all_body: term -> term
    88   val strip_all_vars: term -> (string * typ) list
    89   val incr_bv: int * int * term -> term
    90   val incr_boundvars: int -> term -> term
    91   val add_loose_bnos: term * int * int list -> int list
    92   val loose_bnos: term -> int list
    93   val loose_bvar: term * int -> bool
    94   val loose_bvar1: term * int -> bool
    95   val subst_bounds: term list * term -> term
    96   val subst_bound: term * term -> term
    97   val subst_TVars: (indexname * typ) list -> term -> term
    98   val subst_TVars_Vartab: typ Vartab.table -> term -> term
    99   val betapply: term * term -> term
   100   val eq_ix: indexname * indexname -> bool
   101   val ins_ix: indexname * indexname list -> indexname list
   102   val mem_ix: indexname * indexname list -> bool
   103   val aconv: term * term -> bool
   104   val aconvs: term list * term list -> bool
   105   val mem_term: term * term list -> bool
   106   val subset_term: term list * term list -> bool
   107   val eq_set_term: term list * term list -> bool
   108   val ins_term: term * term list -> term list
   109   val union_term: term list * term list -> term list
   110   val inter_term: term list * term list -> term list
   111   val could_unify: term * term -> bool
   112   val subst_free: (term * term) list -> term -> term
   113   val subst_atomic: (term * term) list -> term -> term
   114   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   115   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   116   val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ
   117   val subst_Vars: (indexname * term) list -> term -> term
   118   val incr_tvar: int -> typ -> typ
   119   val xless: (string * int) * indexname -> bool
   120   val atless: term * term -> bool
   121   val insert_aterm: term * term list -> term list
   122   val abstract_over: term * term -> term
   123   val lambda: term -> term -> term
   124   val absfree: string * typ * term -> term
   125   val list_abs_free: (string * typ) list * term -> term
   126   val list_all_free: (string * typ) list * term -> term
   127   val list_all: (string * typ) list * term -> term
   128   val maxidx_of_typ: typ -> int
   129   val maxidx_of_typs: typ list -> int
   130   val maxidx_of_term: term -> int
   131   val maxidx_of_terms: term list -> int
   132   val variant: string list -> string -> string
   133   val variantlist: string list * string list -> string list
   134   val variant_abs: string * typ * term -> string * term
   135   val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
   136   val add_new_id: string list * string -> string list
   137   val add_typ_classes: typ * class list -> class list
   138   val add_typ_ixns: indexname list * typ -> indexname list
   139   val add_typ_tfree_names: typ * string list -> string list
   140   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   141   val typ_tfrees: typ -> (string * sort) list
   142   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   143   val typ_tvars: typ -> (indexname * sort) list
   144   val add_typ_tycons: typ * string list -> string list
   145   val add_typ_varnames: typ * string list -> string list
   146   val add_term_classes: term * class list -> class list
   147   val add_term_consts: term * string list -> string list
   148   val term_consts: term -> string list
   149   val add_term_frees: term * term list -> term list
   150   val term_frees: term -> term list
   151   val add_term_free_names: term * string list -> string list
   152   val add_term_names: term * string list -> string list
   153   val add_term_tfree_names: term * string list -> string list
   154   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   155   val term_tfrees: term -> (string * sort) list
   156   val add_term_tvar_ixns: term * indexname list -> indexname list
   157   val add_term_tvarnames: term * string list -> string list
   158   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   159   val term_tvars: term -> (indexname * sort) list
   160   val add_term_tycons: term * string list -> string list
   161   val add_term_vars: term * term list -> term list
   162   val term_vars: term -> term list
   163   val exists_Const: (string * typ -> bool) -> term -> bool
   164   val exists_subterm: (term -> bool) -> term -> bool
   165   val compress_type: typ -> typ
   166   val compress_term: term -> term
   167   val show_var_qmarks: bool ref
   168 end;
   169 
   170 signature TERM =
   171 sig
   172   include BASIC_TERM
   173   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   174   val rename_abs: term -> term -> term -> term option
   175   val invent_names: string list -> string -> int -> string list
   176   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   177   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   178   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   179   val add_frees: (string * typ) list * term -> (string * typ) list
   180   val indexname_ord: indexname * indexname -> order
   181   val typ_ord: typ * typ -> order
   182   val typs_ord: typ list * typ list -> order
   183   val term_ord: term * term -> order
   184   val terms_ord: term list * term list -> order
   185   val hd_ord: term * term -> order
   186   val termless: term * term -> bool
   187   val no_dummyT: typ -> typ
   188   val dummy_patternN: string
   189   val no_dummy_patterns: term -> term
   190   val replace_dummy_patterns: int * term -> int * term
   191   val is_replaced_dummy_pattern: indexname -> bool
   192   val adhoc_freeze_vars: term -> term * string list
   193   val string_of_vname: indexname -> string
   194   val string_of_vname': indexname -> string
   195 end;
   196 
   197 structure Term: TERM =
   198 struct
   199 
   200 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   201   for resolution.*)
   202 type indexname = string*int;
   203 
   204 (* Types are classified by sorts. *)
   205 type class = string;
   206 type sort  = class list;
   207 type arity = string * sort list * sort;
   208 
   209 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   210 datatype typ = Type  of string * typ list
   211              | TFree of string * sort
   212              | TVar  of indexname * sort;
   213 
   214 (*Terms.  Bound variables are indicated by depth number.
   215   Free variables, (scheme) variables and constants have names.
   216   An term is "closed" if every bound variable of level "lev"
   217   is enclosed by at least "lev" abstractions.
   218 
   219   It is possible to create meaningless terms containing loose bound vars
   220   or type mismatches.  But such terms are not allowed in rules. *)
   221 
   222 
   223 
   224 datatype term =
   225     Const of string * typ
   226   | Free  of string * typ
   227   | Var   of indexname * typ
   228   | Bound of int
   229   | Abs   of string*typ*term
   230   | op $  of term*term;
   231 
   232 
   233 (*For errors involving type mismatches*)
   234 exception TYPE of string * typ list * term list;
   235 
   236 (*For system errors involving terms*)
   237 exception TERM of string * term list;
   238 
   239 
   240 (*Note variable naming conventions!
   241     a,b,c: string
   242     f,g,h: functions (including terms of function type)
   243     i,j,m,n: int
   244     t,u: term
   245     v,w: indexnames
   246     x,y: any
   247     A,B,C: term (denoting formulae)
   248     T,U: typ
   249 *)
   250 
   251 
   252 (** Types **)
   253 
   254 fun S --> T = Type("fun",[S,T]);
   255 
   256 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   257 val op ---> = Library.foldr (op -->);
   258 
   259 fun dest_Type (Type x) = x
   260   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   261 
   262 
   263 (** Discriminators **)
   264 
   265 fun is_Bound (Bound _) = true
   266   | is_Bound _         = false;
   267 
   268 fun is_Const (Const _) = true
   269   | is_Const _ = false;
   270 
   271 fun is_Free (Free _) = true
   272   | is_Free _ = false;
   273 
   274 fun is_Var (Var _) = true
   275   | is_Var _ = false;
   276 
   277 fun is_TVar (TVar _) = true
   278   | is_TVar _ = false;
   279 
   280 (** Destructors **)
   281 
   282 fun dest_Const (Const x) =  x
   283   | dest_Const t = raise TERM("dest_Const", [t]);
   284 
   285 fun dest_Free (Free x) =  x
   286   | dest_Free t = raise TERM("dest_Free", [t]);
   287 
   288 fun dest_Var (Var x) =  x
   289   | dest_Var t = raise TERM("dest_Var", [t]);
   290 
   291 
   292 fun domain_type (Type("fun", [T,_])) = T
   293 and range_type  (Type("fun", [_,T])) = T;
   294 
   295 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   296 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   297   | binder_types _   =  [];
   298 
   299 (* maps  [T1,...,Tn]--->T  to T*)
   300 fun body_type (Type("fun",[S,T])) = body_type T
   301   | body_type T   =  T;
   302 
   303 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   304 fun strip_type T : typ list * typ =
   305   (binder_types T, body_type T);
   306 
   307 
   308 (*Compute the type of the term, checking that combinations are well-typed
   309   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   310 fun type_of1 (Ts, Const (_,T)) = T
   311   | type_of1 (Ts, Free  (_,T)) = T
   312   | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
   313         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   314   | type_of1 (Ts, Var (_,T)) = T
   315   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   316   | type_of1 (Ts, f$u) =
   317       let val U = type_of1(Ts,u)
   318           and T = type_of1(Ts,f)
   319       in case T of
   320             Type("fun",[T1,T2]) =>
   321               if T1=U then T2  else raise TYPE
   322                     ("type_of: type mismatch in application", [T1,U], [f$u])
   323           | _ => raise TYPE
   324                     ("type_of: function type is expected in application",
   325                      [T,U], [f$u])
   326       end;
   327 
   328 fun type_of t : typ = type_of1 ([],t);
   329 
   330 (*Determines the type of a term, with minimal checking*)
   331 fun fastype_of1 (Ts, f$u) =
   332     (case fastype_of1 (Ts,f) of
   333         Type("fun",[_,T]) => T
   334         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   335   | fastype_of1 (_, Const (_,T)) = T
   336   | fastype_of1 (_, Free (_,T)) = T
   337   | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
   338          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   339   | fastype_of1 (_, Var (_,T)) = T
   340   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   341 
   342 fun fastype_of t : typ = fastype_of1 ([],t);
   343 
   344 
   345 val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t));
   346 
   347 (* maps  (x1,...,xn)t   to   t  *)
   348 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   349   | strip_abs_body u  =  u;
   350 
   351 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   352 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   353   | strip_abs_vars u  =  [] : (string*typ) list;
   354 
   355 
   356 fun strip_qnt_body qnt =
   357 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   358       | strip t = t
   359 in strip end;
   360 
   361 fun strip_qnt_vars qnt =
   362 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   363       | strip t  =  [] : (string*typ) list
   364 in strip end;
   365 
   366 
   367 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   368 val list_comb : term * term list -> term = Library.foldl (op $);
   369 
   370 
   371 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   372 fun strip_comb u : term * term list =
   373     let fun stripc (f$t, ts) = stripc (f, t::ts)
   374         |   stripc  x =  x
   375     in  stripc(u,[])  end;
   376 
   377 
   378 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   379 fun head_of (f$t) = head_of f
   380   | head_of u = u;
   381 
   382 
   383 (*Number of atoms and abstractions in a term*)
   384 fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
   385   | size_of_term (f$t) = size_of_term f  +  size_of_term t
   386   | size_of_term _ = 1;
   387 
   388 fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
   389   | map_type_tvar f (T as TFree _) = T
   390   | map_type_tvar f (TVar x) = f x;
   391 
   392 fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
   393   | map_type_tfree f (TFree x) = f x
   394   | map_type_tfree f (T as TVar _) = T;
   395 
   396 (* apply a function to all types in a term *)
   397 fun map_term_types f =
   398 let fun map(Const(a,T)) = Const(a, f T)
   399       | map(Free(a,T)) = Free(a, f T)
   400       | map(Var(v,T)) = Var(v, f T)
   401       | map(t as Bound _)  = t
   402       | map(Abs(a,T,t)) = Abs(a, f T, map t)
   403       | map(f$t) = map f $ map t;
   404 in map end;
   405 
   406 (* iterate a function over all types in a term *)
   407 fun it_term_types f =
   408 let fun iter(Const(_,T), a) = f(T,a)
   409       | iter(Free(_,T), a) = f(T,a)
   410       | iter(Var(_,T), a) = f(T,a)
   411       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   412       | iter(f$u, a) = iter(f, iter(u, a))
   413       | iter(Bound _, a) = a
   414 in iter end
   415 
   416 
   417 (** Connectives of higher order logic **)
   418 
   419 fun itselfT ty = Type ("itself", [ty]);
   420 val a_itselfT = itselfT (TFree ("'a", []));
   421 
   422 val propT : typ = Type("prop",[]);
   423 
   424 val implies = Const("==>", propT-->propT-->propT);
   425 
   426 fun all T = Const("all", (T-->propT)-->propT);
   427 
   428 fun equals T = Const("==", T-->T-->propT);
   429 
   430 (* maps  !!x1...xn. t   to   t  *)
   431 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   432   | strip_all_body t  =  t;
   433 
   434 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   435 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   436                 (a,T) :: strip_all_vars t
   437   | strip_all_vars t  =  [] : (string*typ) list;
   438 
   439 (*increments a term's non-local bound variables
   440   required when moving a term within abstractions
   441      inc is  increment for bound variables
   442      lev is  level at which a bound variable is considered 'loose'*)
   443 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   444   | incr_bv (inc, lev, Abs(a,T,body)) =
   445         Abs(a, T, incr_bv(inc,lev+1,body))
   446   | incr_bv (inc, lev, f$t) =
   447       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   448   | incr_bv (inc, lev, u) = u;
   449 
   450 fun incr_boundvars  0  t = t
   451   | incr_boundvars inc t = incr_bv(inc,0,t);
   452 
   453 (*Scan a pair of terms; while they are similar,
   454   accumulate corresponding bound vars in "al"*)
   455 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   456       match_bvs(s, t, if x="" orelse y="" then al
   457                                           else (x,y)::al)
   458   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   459   | match_bvs(_,_,al) = al;
   460 
   461 (* strip abstractions created by parameters *)
   462 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   463 
   464 fun rename_abs pat obj t =
   465   let
   466     val ren = match_bvs (pat, obj, []);
   467     fun ren_abs (Abs (x, T, b)) =
   468           Abs (getOpt (assoc_string (ren, x), x), T, ren_abs b)
   469       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   470       | ren_abs t = t
   471   in if null ren then NONE else SOME (ren_abs t) end;
   472 
   473 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   474    (Bound 0) is loose at level 0 *)
   475 fun add_loose_bnos (Bound i, lev, js) =
   476         if i<lev then js  else  (i-lev) ins_int js
   477   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   478   | add_loose_bnos (f$t, lev, js) =
   479         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   480   | add_loose_bnos (_, _, js) = js;
   481 
   482 fun loose_bnos t = add_loose_bnos (t, 0, []);
   483 
   484 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   485    level k or beyond. *)
   486 fun loose_bvar(Bound i,k) = i >= k
   487   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   488   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   489   | loose_bvar _ = false;
   490 
   491 fun loose_bvar1(Bound i,k) = i = k
   492   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   493   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   494   | loose_bvar1 _ = false;
   495 
   496 (*Substitute arguments for loose bound variables.
   497   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   498   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   499         and the appropriate call is  subst_bounds([b,a], c) .
   500   Loose bound variables >=n are reduced by "n" to
   501      compensate for the disappearance of lambdas.
   502 *)
   503 fun subst_bounds (args: term list, t) : term =
   504   let val n = length args;
   505       fun subst (t as Bound i, lev) =
   506            (if i<lev then  t    (*var is locally bound*)
   507             else  incr_boundvars lev (List.nth(args, i-lev))
   508                     handle Subscript => Bound(i-n)  (*loose: change it*))
   509         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   510         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   511         | subst (t,lev) = t
   512   in   case args of [] => t  | _ => subst (t,0)  end;
   513 
   514 (*Special case: one argument*)
   515 fun subst_bound (arg, t) : term =
   516   let fun subst (t as Bound i, lev) =
   517             if i<lev then  t    (*var is locally bound*)
   518             else  if i=lev then incr_boundvars lev arg
   519                            else Bound(i-1)  (*loose: change it*)
   520         | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   521         | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   522         | subst (t,lev) = t
   523   in  subst (t,0)  end;
   524 
   525 (*beta-reduce if possible, else form application*)
   526 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   527   | betapply (f,u) = f$u;
   528 
   529 
   530 (** Equality, membership and insertion of indexnames (string*ints) **)
   531 
   532 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
   533 fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
   534 
   535 (*membership in a list, optimized version for indexnames*)
   536 fun mem_ix (_, []) = false
   537   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
   538 
   539 (*insertion into list, optimized version for indexnames*)
   540 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   541 
   542 (*Tests whether 2 terms are alpha-convertible and have same type.
   543   Note that constants may have more than one type.*)
   544 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   545   | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
   546   | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
   547   | (Bound i)    aconv (Bound j)    = i=j
   548   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   549   | (f$t)        aconv (g$u)        = (f aconv g) andalso (t aconv u)
   550   | _ aconv _  =  false;
   551 
   552 (** Membership, insertion, union for terms **)
   553 
   554 fun mem_term (_, []) = false
   555   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   556 
   557 fun subset_term ([], ys) = true
   558   | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
   559 
   560 fun eq_set_term (xs, ys) =
   561     xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
   562 
   563 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   564 
   565 fun union_term (xs, []) = xs
   566   | union_term ([], ys) = ys
   567   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   568 
   569 fun inter_term ([], ys) = []
   570   | inter_term (x::xs, ys) =
   571       if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys);
   572 
   573 (*are two term lists alpha-convertible in corresponding elements?*)
   574 fun aconvs ([],[]) = true
   575   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   576   | aconvs _ = false;
   577 
   578 (*A fast unification filter: true unless the two terms cannot be unified.
   579   Terms must be NORMAL.  Treats all Vars as distinct. *)
   580 fun could_unify (t,u) =
   581   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   582         | matchrands _ = true
   583   in case (head_of t , head_of u) of
   584         (_, Var _) => true
   585       | (Var _, _) => true
   586       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   587       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   588       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   589       | (Abs _, _) =>  true   (*because of possible eta equality*)
   590       | (_, Abs _) =>  true
   591       | _ => false
   592   end;
   593 
   594 (*Substitute new for free occurrences of old in a term*)
   595 fun subst_free [] = (fn t=>t)
   596   | subst_free pairs =
   597       let fun substf u =
   598             case gen_assoc (op aconv) (pairs, u) of
   599                 SOME u' => u'
   600               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   601                                  | t$u' => substf t $ substf u'
   602                                  | _ => u)
   603       in  substf  end;
   604 
   605 (*a total, irreflexive ordering on index names*)
   606 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   607 
   608 
   609 (*Abstraction of the term "body" over its occurrences of v,
   610     which must contain no loose bound variables.
   611   The resulting term is ready to become the body of an Abs.*)
   612 fun abstract_over (v,body) =
   613   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   614       (case u of
   615           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   616         | f$rand => abst(lev,f) $ abst(lev,rand)
   617         | _ => u)
   618   in  abst(0,body)  end;
   619 
   620 fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   621   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   622   | lambda v t = raise TERM ("lambda", [v, t]);
   623 
   624 (*Form an abstraction over a free variable.*)
   625 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   626 
   627 (*Abstraction over a list of free variables*)
   628 fun list_abs_free ([ ] ,     t) = t
   629   | list_abs_free ((a,T)::vars, t) =
   630       absfree(a, T, list_abs_free(vars,t));
   631 
   632 (*Quantification over a list of free variables*)
   633 fun list_all_free ([], t: term) = t
   634   | list_all_free ((a,T)::vars, t) =
   635         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   636 
   637 (*Quantification over a list of variables (already bound in body) *)
   638 fun list_all ([], t) = t
   639   | list_all ((a,T)::vars, t) =
   640         (all T) $ (Abs(a, T, list_all(vars,t)));
   641 
   642 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)].
   643   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   644 fun subst_atomic [] t = t : term
   645   | subst_atomic (instl: (term*term) list) t =
   646       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   647             | subst (f$t') = subst f $ subst t'
   648             | subst t = getOpt (assoc(instl,t),t)
   649       in  subst t  end;
   650 
   651 (*Substitute for type Vars in a type*)
   652 fun typ_subst_TVars iTs T = if null iTs then T else
   653   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   654         | subst(T as TFree _) = T
   655         | subst(T as TVar(ixn,_)) = getOpt (assoc(iTs,ixn),T)
   656   in subst T end;
   657 
   658 (*Substitute for type Vars in a term*)
   659 val subst_TVars = map_term_types o typ_subst_TVars;
   660 
   661 (*Substitute for Vars in a term; see also envir/norm_term*)
   662 fun subst_Vars itms t = if null itms then t else
   663   let fun subst(v as Var(ixn,_)) = getOpt (assoc(itms,ixn),v)
   664         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   665         | subst(f$t) = subst f $ subst t
   666         | subst(t) = t
   667   in subst t end;
   668 
   669 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
   670 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   671   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   672         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   673         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   674             NONE   => Var(ixn,typ_subst_TVars iTs T)
   675           | SOME t => t)
   676         | subst(b as Bound _) = b
   677         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   678         | subst(f$t) = subst f $ subst t
   679   in subst end;
   680 
   681 
   682 (*Computing the maximum index of a typ*)
   683 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   684   | maxidx_of_typ(TFree _) = ~1
   685   | maxidx_of_typ(TVar((_,i),_)) = i
   686 and maxidx_of_typs [] = ~1
   687   | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   688 
   689 
   690 (*Computing the maximum index of a term*)
   691 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   692   | maxidx_of_term (Bound _) = ~1
   693   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   694   | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   695   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   696   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   697 
   698 fun maxidx_of_terms ts = Library.foldl Int.max (~1, map maxidx_of_term ts);
   699 
   700 
   701 (* Increment the index of all Poly's in T by k *)
   702 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
   703 
   704 
   705 (**** Syntax-related declarations ****)
   706 
   707 
   708 (*Dummy type for parsing and printing.  Will be replaced during type inference. *)
   709 val dummyT = Type("dummy",[]);
   710 
   711 fun no_dummyT typ =
   712   let
   713     fun check (T as Type ("dummy", _)) =
   714           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   715       | check (Type (_, Ts)) = List.app check Ts
   716       | check _ = ();
   717   in check typ; typ end;
   718 
   719 
   720 (*** Printing ***)
   721 
   722 (*Makes a variant of a name distinct from the names in bs.
   723   First attaches the suffix and then increments this;
   724   preserves a suffix of underscores "_". *)
   725 fun variant bs name =
   726   let
   727     val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name));
   728     fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c;
   729     fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c;
   730   in vary1 (if c = "" then "u" else c) ^ u end;
   731 
   732 (*Create variants of the list of names, with priority to the first ones*)
   733 fun variantlist ([], used) = []
   734   | variantlist(b::bs, used) =
   735       let val b' = variant used b
   736       in  b' :: variantlist (bs, b'::used)  end;
   737 
   738 (*Invent fresh names*)
   739 fun invent_names _ _ 0 = []
   740   | invent_names used a n =
   741       let val b = Symbol.bump_string a in
   742         if a mem_string used then invent_names used b n
   743         else a :: invent_names used b (n - 1)
   744       end;
   745 
   746 
   747 
   748 (** Consts etc. **)
   749 
   750 fun add_typ_classes (Type (_, Ts), cs) = Library.foldr add_typ_classes (Ts, cs)
   751   | add_typ_classes (TFree (_, S), cs) = S union cs
   752   | add_typ_classes (TVar (_, S), cs) = S union cs;
   753 
   754 fun add_typ_tycons (Type (c, Ts), cs) = Library.foldr add_typ_tycons (Ts, c ins cs)
   755   | add_typ_tycons (_, cs) = cs;
   756 
   757 val add_term_classes = it_term_types add_typ_classes;
   758 val add_term_tycons = it_term_types add_typ_tycons;
   759 
   760 fun add_term_consts (Const (c, _), cs) = c ins_string cs
   761   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   762   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   763   | add_term_consts (_, cs) = cs;
   764 
   765 fun term_consts t = add_term_consts(t,[]);
   766 
   767 fun exists_Const P t = let
   768         fun ex (Const c      ) = P c
   769         |   ex (t $ u        ) = ex t orelse ex u
   770         |   ex (Abs (_, _, t)) = ex t
   771         |   ex _               = false
   772     in ex t end;
   773 
   774 fun exists_subterm P =
   775   let fun ex t = P t orelse
   776                  (case t of
   777                     u $ v        => ex u orelse ex v
   778                   | Abs(_, _, u) => ex u
   779                   | _            => false)
   780   in ex end;
   781 
   782 (*map classes, tycons*)
   783 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   784   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   785   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
   786 
   787 (*map classes, tycons, consts*)
   788 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
   789   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
   790   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
   791   | map_term _ _ _ (t as Bound _) = t
   792   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   793   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   794 
   795 
   796 
   797 (** TFrees and TVars **)
   798 
   799 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   800 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   801 
   802 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   803 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   804   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   805   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   806   | add_term_free_names (_, bs) = bs;
   807 
   808 (*Accumulates the names in the term, suppressing duplicates.
   809   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   810 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   811   | add_term_names (Free(a,_), bs) = a ins_string bs
   812   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   813   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   814   | add_term_names (_, bs) = bs;
   815 
   816 (*Accumulates the TVars in a type, suppressing duplicates. *)
   817 fun add_typ_tvars(Type(_,Ts),vs) = Library.foldr add_typ_tvars (Ts,vs)
   818   | add_typ_tvars(TFree(_),vs) = vs
   819   | add_typ_tvars(TVar(v),vs) = v ins vs;
   820 
   821 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   822 fun add_typ_tfree_names(Type(_,Ts),fs) = Library.foldr add_typ_tfree_names (Ts,fs)
   823   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   824   | add_typ_tfree_names(TVar(_),fs) = fs;
   825 
   826 fun add_typ_tfrees(Type(_,Ts),fs) = Library.foldr add_typ_tfrees (Ts,fs)
   827   | add_typ_tfrees(TFree(f),fs) = f ins fs
   828   | add_typ_tfrees(TVar(_),fs) = fs;
   829 
   830 fun add_typ_varnames(Type(_,Ts),nms) = Library.foldr add_typ_varnames (Ts,nms)
   831   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   832   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   833 
   834 (*Accumulates the TVars in a term, suppressing duplicates. *)
   835 val add_term_tvars = it_term_types add_typ_tvars;
   836 
   837 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   838 val add_term_tfrees = it_term_types add_typ_tfrees;
   839 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   840 
   841 val add_term_tvarnames = it_term_types add_typ_varnames;
   842 
   843 (*Non-list versions*)
   844 fun typ_tfrees T = add_typ_tfrees(T,[]);
   845 fun typ_tvars T = add_typ_tvars(T,[]);
   846 fun term_tfrees t = add_term_tfrees(t,[]);
   847 fun term_tvars t = add_term_tvars(t,[]);
   848 
   849 (*special code to enforce left-to-right collection of TVar-indexnames*)
   850 
   851 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
   852   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
   853                                      else ixns@[ixn]
   854   | add_typ_ixns(ixns,TFree(_)) = ixns;
   855 
   856 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
   857   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
   858   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
   859   | add_term_tvar_ixns(Bound _,ixns) = ixns
   860   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
   861       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
   862   | add_term_tvar_ixns(f$t,ixns) =
   863       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   864 
   865 (** Frees and Vars **)
   866 
   867 (*a partial ordering (not reflexive) for atomic terms*)
   868 fun atless (Const (a,_), Const (b,_))  =  a<b
   869   | atless (Free (a,_), Free (b,_)) =  a<b
   870   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   871   | atless (Bound i, Bound j)  =   i<j
   872   | atless _  =  false;
   873 
   874 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   875 fun insert_aterm (t,us) =
   876   let fun inserta [] = [t]
   877         | inserta (us as u::us') =
   878               if atless(t,u) then t::us
   879               else if t=u then us (*duplicate*)
   880               else u :: inserta(us')
   881   in  inserta us  end;
   882 
   883 (*Accumulates the Vars in the term, suppressing duplicates*)
   884 fun add_term_vars (t, vars: term list) = case t of
   885     Var   _ => insert_aterm(t,vars)
   886   | Abs (_,_,body) => add_term_vars(body,vars)
   887   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   888   | _ => vars;
   889 
   890 fun term_vars t = add_term_vars(t,[]);
   891 
   892 (*Accumulates the Frees in the term, suppressing duplicates*)
   893 fun add_term_frees (t, frees: term list) = case t of
   894     Free   _ => insert_aterm(t,frees)
   895   | Abs (_,_,body) => add_term_frees(body,frees)
   896   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   897   | _ => frees;
   898 
   899 fun term_frees t = add_term_frees(t,[]);
   900 
   901 (*Given an abstraction over P, replaces the bound variable by a Free variable
   902   having a unique name. *)
   903 fun variant_abs (a,T,P) =
   904   let val b = variant (add_term_names(P,[])) a
   905   in  (b,  subst_bound (Free(b,T), P))  end;
   906 
   907 (* renames and reverses the strings in vars away from names *)
   908 fun rename_aTs names vars : (string*typ)list =
   909   let fun rename_aT (vars,(a,T)) =
   910                 (variant (map #1 vars @ names) a, T) :: vars
   911   in Library.foldl rename_aT ([],vars) end;
   912 
   913 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   914 
   915 
   916 (* left-ro-right traversal *)
   917 
   918 (*foldl atoms of type*)
   919 fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
   920   | foldl_atyps f x_atom = f x_atom;
   921 
   922 (*foldl atoms of term*)
   923 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
   924   | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
   925   | foldl_aterms f x_atom = f x_atom;
   926 
   927 fun foldl_map_aterms f (x, t $ u) =
   928       let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
   929       in (x'', t' $ u') end
   930   | foldl_map_aterms f (x, Abs (a, T, t)) =
   931       let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
   932   | foldl_map_aterms f x_atom = f x_atom;
   933 
   934 (*foldl types of term*)
   935 fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
   936   | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
   937   | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
   938   | foldl_term_types f (x, Bound _) = x
   939   | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
   940   | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
   941 
   942 fun foldl_types f = foldl_term_types (fn _ => f);
   943 
   944 (*collect variables*)
   945 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
   946 val add_tvars = foldl_types add_tvarsT;
   947 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
   948 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   949 
   950 (*collect variable names*)
   951 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   952 fun term_varnames t = add_term_varnames ([], t);
   953 
   954 
   955 (** type and term orders **)
   956 
   957 fun indexname_ord ((x, i), (y, j)) =
   958   (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
   959 
   960 val sort_ord = list_ord String.compare;
   961 
   962 
   963 (* typ_ord *)
   964 
   965 fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
   966   | typ_ord (Type _, _) = GREATER
   967   | typ_ord (TFree _, Type _) = LESS
   968   | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
   969   | typ_ord (TFree _, TVar _) = GREATER
   970   | typ_ord (TVar _, Type _) = LESS
   971   | typ_ord (TVar _, TFree _) = LESS
   972   | typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y)
   973 and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
   974 
   975 
   976 (* term_ord *)
   977 
   978 (*a linear well-founded AC-compatible ordering for terms:
   979   s < t <=> 1. size(s) < size(t) or
   980             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   981             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   982                (s1..sn) < (t1..tn) (lexicographically)*)
   983 
   984 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   985   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   986   | dest_hd (Var v) = (v, 2)
   987   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   988   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   989 
   990 fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
   991       (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   992   | term_ord (t, u) =
   993       (case Int.compare (size_of_term t, size_of_term u) of
   994         EQUAL =>
   995           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   996             (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
   997           end
   998       | ord => ord)
   999 and hd_ord (f, g) =
  1000   prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
  1001 and terms_ord (ts, us) = list_ord term_ord (ts, us);
  1002 
  1003 fun termless tu = (term_ord tu = LESS);
  1004 
  1005 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
  1006 structure Typtab = TableFun(type key = typ val ord = typ_ord);
  1007 structure Termtab = TableFun(type key = term val ord = term_ord);
  1008 
  1009 (*Substitute for type Vars in a type, version using Vartab*)
  1010 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else
  1011   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
  1012         | subst(T as TFree _) = T
  1013         | subst(T as TVar(ixn, _)) =
  1014             (case Vartab.lookup (iTs, ixn) of NONE => T | SOME(U) => U)
  1015   in subst T end;
  1016 
  1017 (*Substitute for type Vars in a term, version using Vartab*)
  1018 val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab;
  1019 
  1020 
  1021 (*** Compression of terms and types by sharing common subtrees.
  1022      Saves 50-75% on storage requirements.  As it is a bit slow,
  1023      it should be called only for axioms, stored theorems, etc.
  1024      Recorded term and type fragments are never disposed. ***)
  1025 
  1026 (** Sharing of types **)
  1027 
  1028 val memo_types = ref (Typtab.empty: typ Typtab.table);
  1029 
  1030 fun compress_type T =
  1031   (case Typtab.lookup (! memo_types, T) of
  1032     SOME T' => T'
  1033   | NONE =>
  1034       let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
  1035       in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
  1036 
  1037 
  1038 (** Sharing of atomic terms **)
  1039 
  1040 val memo_terms = ref (Termtab.empty : term Termtab.table);
  1041 
  1042 fun share_term (t $ u) = share_term t $ share_term u
  1043   | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
  1044   | share_term t =
  1045       (case Termtab.lookup (! memo_terms, t) of
  1046         SOME t' => t'
  1047       | NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
  1048 
  1049 val compress_term = share_term o map_term_types compress_type;
  1050 
  1051 
  1052 (* dummy patterns *)
  1053 
  1054 val dummy_patternN = "dummy_pattern";
  1055 
  1056 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1057   | is_dummy_pattern _ = false;
  1058 
  1059 fun no_dummy_patterns tm =
  1060   if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
  1061   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1062 
  1063 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1064       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1065   | replace_dummy Ts (i, Abs (x, T, t)) =
  1066       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1067       in (i', Abs (x, T, t')) end
  1068   | replace_dummy Ts (i, t $ u) =
  1069       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1070       in (i'', t' $ u') end
  1071   | replace_dummy _ (i, a) = (i, a);
  1072 
  1073 val replace_dummy_patterns = replace_dummy [];
  1074 
  1075 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1076   | is_replaced_dummy_pattern _ = false;
  1077 
  1078 
  1079 (* adhoc freezing *)
  1080 
  1081 fun adhoc_freeze_vars tm =
  1082   let
  1083     fun mk_inst (var as Var ((a, i), T)) =
  1084       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1085       in ((var,  Free(x, T)), x) end;
  1086     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1087   in (subst_atomic insts tm, xs) end;
  1088 
  1089 
  1090 (* string_of_vname *)
  1091 
  1092 val show_var_qmarks = ref true;
  1093 
  1094 fun string_of_vname (x, i) =
  1095   let
  1096     val si = string_of_int i;
  1097     val dot = getOpt (try (Symbol.is_digit o List.last o Symbol.explode) x, true);
  1098     val qmark = if !show_var_qmarks then "?" else "";
  1099   in
  1100     if dot then qmark ^ x ^ "." ^ si
  1101     else if i = 0 then qmark ^ x
  1102     else qmark ^ x ^ si
  1103   end;
  1104 
  1105 fun string_of_vname' (x, ~1) = x
  1106   | string_of_vname' xi = string_of_vname xi;
  1107 
  1108 end;
  1109 
  1110 structure BasicTerm: BASIC_TERM = Term;
  1111 open BasicTerm;