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