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