src/Pure/term.ML
author kleing
Mon May 16 08:28:16 2005 +0200 (2005-05-16)
changeset 15962 a3288211965a
parent 15954 dd516176043a
child 15986 db3cd4fa9b19
permissions -rw-r--r--
line wrap
     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 add_term_frees: term * term list -> term list
   154   val term_frees: term -> term list
   155   val add_term_free_names: term * string list -> string list
   156   val add_term_names: term * string list -> string list
   157   val add_term_tfree_names: term * string list -> string list
   158   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   159   val term_tfrees: term -> (string * sort) list
   160   val add_term_tvar_ixns: term * indexname list -> indexname list
   161   val add_term_tvarnames: term * string list -> string list
   162   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   163   val term_tvars: term -> (indexname * sort) list
   164   val add_term_tycons: term * string list -> string list
   165   val add_term_vars: term * term list -> term list
   166   val term_vars: term -> term list
   167   val exists_Const: (string * typ -> bool) -> term -> bool
   168   val exists_subterm: (term -> bool) -> term -> bool
   169   val compress_type: typ -> typ
   170   val compress_term: term -> term
   171   val show_var_qmarks: bool ref
   172 end;
   173 
   174 signature TERM =
   175 sig
   176   include BASIC_TERM
   177   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   178   val rename_abs: term -> term -> term -> term option
   179   val invent_names: string list -> string -> int -> string list
   180   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   181   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   182   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   183   val add_frees: (string * typ) list * term -> (string * typ) list
   184   val indexname_ord: indexname * indexname -> order
   185   val typ_ord: typ * typ -> order
   186   val typs_ord: typ list * typ list -> order
   187   val term_ord: term * term -> order
   188   val terms_ord: term list * term list -> order
   189   val hd_ord: term * term -> order
   190   val termless: term * term -> bool
   191   val no_dummyT: typ -> typ
   192   val dummy_patternN: string
   193   val no_dummy_patterns: term -> term
   194   val replace_dummy_patterns: int * term -> int * term
   195   val is_replaced_dummy_pattern: indexname -> bool
   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 
   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 term_consts t = add_term_consts(t,[]);
   806 
   807 fun exists_Const P t = let
   808         fun ex (Const c      ) = P c
   809         |   ex (t $ u        ) = ex t orelse ex u
   810         |   ex (Abs (_, _, t)) = ex t
   811         |   ex _               = false
   812     in ex t end;
   813 
   814 fun exists_subterm P =
   815   let fun ex t = P t orelse
   816                  (case t of
   817                     u $ v        => ex u orelse ex v
   818                   | Abs(_, _, u) => ex u
   819                   | _            => false)
   820   in ex end;
   821 
   822 (*map classes, tycons*)
   823 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
   824   | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
   825   | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
   826 
   827 (*map classes, tycons, consts*)
   828 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
   829   | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
   830   | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
   831   | map_term _ _ _ (t as Bound _) = t
   832   | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
   833   | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
   834 
   835 
   836 (** TFrees and TVars **)
   837 
   838 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   839 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   840 
   841 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   842 fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   843   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   844   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   845   | add_term_free_names (_, bs) = bs;
   846 
   847 (*Accumulates the names in the term, suppressing duplicates.
   848   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   849 fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   850   | add_term_names (Free(a,_), bs) = a ins_string bs
   851   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   852   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   853   | add_term_names (_, bs) = bs;
   854 
   855 (*Accumulates the TVars in a type, suppressing duplicates. *)
   856 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
   857   | add_typ_tvars(TFree(_),vs) = vs
   858   | add_typ_tvars(TVar(v),vs) = v ins vs;
   859 
   860 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   861 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
   862   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   863   | add_typ_tfree_names(TVar(_),fs) = fs;
   864 
   865 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
   866   | add_typ_tfrees(TFree(f),fs) = f ins fs
   867   | add_typ_tfrees(TVar(_),fs) = fs;
   868 
   869 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
   870   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   871   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   872 
   873 (*Accumulates the TVars in a term, suppressing duplicates. *)
   874 val add_term_tvars = it_term_types add_typ_tvars;
   875 
   876 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   877 val add_term_tfrees = it_term_types add_typ_tfrees;
   878 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   879 
   880 val add_term_tvarnames = it_term_types add_typ_varnames;
   881 
   882 (*Non-list versions*)
   883 fun typ_tfrees T = add_typ_tfrees(T,[]);
   884 fun typ_tvars T = add_typ_tvars(T,[]);
   885 fun term_tfrees t = add_term_tfrees(t,[]);
   886 fun term_tvars t = add_term_tvars(t,[]);
   887 
   888 (*special code to enforce left-to-right collection of TVar-indexnames*)
   889 
   890 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
   891   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns
   892                                      else ixns@[ixn]
   893   | add_typ_ixns(ixns,TFree(_)) = ixns;
   894 
   895 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
   896   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
   897   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
   898   | add_term_tvar_ixns(Bound _,ixns) = ixns
   899   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
   900       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
   901   | add_term_tvar_ixns(f$t,ixns) =
   902       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   903 
   904 (** Frees and Vars **)
   905 
   906 (*a partial ordering (not reflexive) for atomic terms*)
   907 fun atless (Const (a,_), Const (b,_))  =  a<b
   908   | atless (Free (a,_), Free (b,_)) =  a<b
   909   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   910   | atless (Bound i, Bound j)  =   i<j
   911   | atless _  =  false;
   912 
   913 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   914 fun insert_aterm (t,us) =
   915   let fun inserta [] = [t]
   916         | inserta (us as u::us') =
   917               if atless(t,u) then t::us
   918               else if t=u then us (*duplicate*)
   919               else u :: inserta(us')
   920   in  inserta us  end;
   921 
   922 (*Accumulates the Vars in the term, suppressing duplicates*)
   923 fun add_term_vars (t, vars: term list) = case t of
   924     Var   _ => insert_aterm(t,vars)
   925   | Abs (_,_,body) => add_term_vars(body,vars)
   926   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   927   | _ => vars;
   928 
   929 fun term_vars t = add_term_vars(t,[]);
   930 
   931 (*Accumulates the Frees in the term, suppressing duplicates*)
   932 fun add_term_frees (t, frees: term list) = case t of
   933     Free   _ => insert_aterm(t,frees)
   934   | Abs (_,_,body) => add_term_frees(body,frees)
   935   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   936   | _ => frees;
   937 
   938 fun term_frees t = add_term_frees(t,[]);
   939 
   940 (*Given an abstraction over P, replaces the bound variable by a Free variable
   941   having a unique name. *)
   942 fun variant_abs (a,T,P) =
   943   let val b = variant (add_term_names(P,[])) a
   944   in  (b,  subst_bound (Free(b,T), P))  end;
   945 
   946 (* renames and reverses the strings in vars away from names *)
   947 fun rename_aTs names vars : (string*typ)list =
   948   let fun rename_aT (vars,(a,T)) =
   949                 (variant (map #1 vars @ names) a, T) :: vars
   950   in Library.foldl rename_aT ([],vars) end;
   951 
   952 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   953 
   954 
   955 (* left-ro-right traversal *)
   956 
   957 (*foldl atoms of type*)
   958 fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
   959   | foldl_atyps f x_atom = f x_atom;
   960 
   961 (*foldl atoms of term*)
   962 fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
   963   | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
   964   | foldl_aterms f x_atom = f x_atom;
   965 
   966 fun foldl_map_aterms f (x, t $ u) =
   967       let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u);
   968       in (x'', t' $ u') end
   969   | foldl_map_aterms f (x, Abs (a, T, t)) =
   970       let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end
   971   | foldl_map_aterms f x_atom = f x_atom;
   972 
   973 (*foldl types of term*)
   974 fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
   975   | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
   976   | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
   977   | foldl_term_types f (x, Bound _) = x
   978   | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
   979   | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
   980 
   981 fun foldl_types f = foldl_term_types (fn _ => f);
   982 
   983 (*collect variables*)
   984 val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
   985 val add_tvars = foldl_types add_tvarsT;
   986 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
   987 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
   988 
   989 (*collect variable names*)
   990 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   991 fun term_varnames t = add_term_varnames ([], t);
   992 
   993 
   994 (** type and term orders **)
   995 
   996 fun indexname_ord ((x, i), (y, j)) =
   997   (case Int.compare (i, j) of EQUAL => String.compare (x, y) | ord => ord);
   998 
   999 val sort_ord = list_ord String.compare;
  1000 
  1001 
  1002 (* typ_ord *)
  1003 
  1004 fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y)
  1005   | typ_ord (Type _, _) = GREATER
  1006   | typ_ord (TFree _, Type _) = LESS
  1007   | typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y)
  1008   | typ_ord (TFree _, TVar _) = GREATER
  1009   | typ_ord (TVar _, Type _) = LESS
  1010   | typ_ord (TVar _, TFree _) = LESS
  1011   | typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y)
  1012 and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
  1013 
  1014 
  1015 (* term_ord *)
  1016 
  1017 (*a linear well-founded AC-compatible ordering for terms:
  1018   s < t <=> 1. size(s) < size(t) or
  1019             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
  1020             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
  1021                (s1..sn) < (t1..tn) (lexicographically)*)
  1022 
  1023 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
  1024   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
  1025   | dest_hd (Var v) = (v, 2)
  1026   | dest_hd (Bound i) = ((("", i), dummyT), 3)
  1027   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
  1028 
  1029 fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
  1030       (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
  1031   | term_ord (t, u) =
  1032       (case Int.compare (size_of_term t, size_of_term u) of
  1033         EQUAL =>
  1034           let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
  1035             (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
  1036           end
  1037       | ord => ord)
  1038 and hd_ord (f, g) =
  1039   prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g)
  1040 and terms_ord (ts, us) = list_ord term_ord (ts, us);
  1041 
  1042 fun termless tu = (term_ord tu = LESS);
  1043 
  1044 structure Vartab = TableFun(type key = indexname val ord = indexname_ord);
  1045 structure Typtab = TableFun(type key = typ val ord = typ_ord);
  1046 structure Termtab = TableFun(type key = term val ord = term_ord);
  1047 
  1048 
  1049 (*** Compression of terms and types by sharing common subtrees.
  1050      Saves 50-75% on storage requirements.  As it is a bit slow,
  1051      it should be called only for axioms, stored theorems, etc.
  1052      Recorded term and type fragments are never disposed. ***)
  1053 
  1054 (** Sharing of types **)
  1055 
  1056 val memo_types = ref (Typtab.empty: typ Typtab.table);
  1057 
  1058 fun compress_type T =
  1059   (case Typtab.lookup (! memo_types, T) of
  1060     SOME T' => T'
  1061   | NONE =>
  1062       let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts) | _ => T)
  1063       in memo_types := Typtab.update ((T', T'), ! memo_types); T' end);
  1064 
  1065 
  1066 (** Sharing of atomic terms **)
  1067 
  1068 val memo_terms = ref (Termtab.empty : term Termtab.table);
  1069 
  1070 fun share_term (t $ u) = share_term t $ share_term u
  1071   | share_term (Abs (a, T, u)) = Abs (a, T, share_term u)
  1072   | share_term t =
  1073       (case Termtab.lookup (! memo_terms, t) of
  1074         SOME t' => t'
  1075       | NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t));
  1076 
  1077 val compress_term = share_term o map_term_types compress_type;
  1078 
  1079 
  1080 (* dummy patterns *)
  1081 
  1082 val dummy_patternN = "dummy_pattern";
  1083 
  1084 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1085   | is_dummy_pattern _ = false;
  1086 
  1087 fun no_dummy_patterns tm =
  1088   if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
  1089   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1090 
  1091 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1092       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1093   | replace_dummy Ts (i, Abs (x, T, t)) =
  1094       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1095       in (i', Abs (x, T, t')) end
  1096   | replace_dummy Ts (i, t $ u) =
  1097       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1098       in (i'', t' $ u') end
  1099   | replace_dummy _ (i, a) = (i, a);
  1100 
  1101 val replace_dummy_patterns = replace_dummy [];
  1102 
  1103 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1104   | is_replaced_dummy_pattern _ = false;
  1105 
  1106 
  1107 (* adhoc freezing *)
  1108 
  1109 fun adhoc_freeze_vars tm =
  1110   let
  1111     fun mk_inst (var as Var ((a, i), T)) =
  1112       let val x = a ^ Library.gensym "_" ^ string_of_int i
  1113       in ((var,  Free(x, T)), x) end;
  1114     val (insts, xs) = split_list (map mk_inst (term_vars tm));
  1115   in (subst_atomic insts tm, xs) end;
  1116 
  1117 
  1118 (* string_of_vname *)
  1119 
  1120 val show_var_qmarks = ref true;
  1121 
  1122 fun string_of_vname (x, i) =
  1123   let
  1124     val si = string_of_int i;
  1125     val dot = getOpt (try (Symbol.is_digit o List.last o Symbol.explode) x, true);
  1126     val qmark = if !show_var_qmarks then "?" else "";
  1127   in
  1128     if dot then qmark ^ x ^ "." ^ si
  1129     else if i = 0 then qmark ^ x
  1130     else qmark ^ x ^ si
  1131   end;
  1132 
  1133 fun string_of_vname' (x, ~1) = x
  1134   | string_of_vname' xi = string_of_vname xi;
  1135 
  1136 fun string_of_term (Const(s,_)) = s
  1137   | string_of_term (Free(s,_)) = s
  1138   | string_of_term (Var(ix,_)) = string_of_vname ix
  1139   | string_of_term (Bound i) = string_of_int i
  1140   | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t
  1141   | string_of_term (s $ t) =
  1142       "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")"
  1143 
  1144 end;
  1145 
  1146 structure BasicTerm: BASIC_TERM = Term;
  1147 open BasicTerm;