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