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