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