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