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