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