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