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