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