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