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