src/Pure/term.ML
author paulson
Tue Nov 12 11:40:41 1996 +0100 (1996-11-12)
changeset 2176 43e5c20a593c
parent 2146 6854b692f1fe
child 2182 29e56f003599
permissions -rw-r--r--
Changed some mem and ins calls to be monomorphic
     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 
    15 structure Term =
    16 struct
    17 
    18 (*Indexnames can be quickly renamed by adding an offset to the integer part,
    19   for resolution.*)
    20 type indexname = string*int;
    21 
    22 (* Types are classified by classes. *)
    23 type class = string;
    24 type sort  = class list;
    25 
    26 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
    27 datatype typ = Type  of string * typ list
    28              | TFree of string * sort
    29 	     | TVar  of indexname * sort;
    30 
    31 fun S --> T = Type("fun",[S,T]);
    32 
    33 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
    34 val op ---> = foldr (op -->);
    35 
    36 
    37 (*terms.  Bound variables are indicated by depth number.
    38   Free variables, (scheme) variables and constants have names.
    39   An term is "closed" if there every bound variable of level "lev"
    40   is enclosed by at least "lev" abstractions. 
    41 
    42   It is possible to create meaningless terms containing loose bound vars
    43   or type mismatches.  But such terms are not allowed in rules. *)
    44 
    45 
    46 
    47 datatype term = 
    48     Const of string * typ
    49   | Free  of string * typ 
    50   | Var   of indexname * typ
    51   | Bound of int
    52   | Abs   of string*typ*term
    53   | op $  of term*term;
    54 
    55 
    56 (*For errors involving type mismatches*)
    57 exception TYPE of string * typ list * term list;
    58 
    59 fun raise_type msg tys ts = raise TYPE (msg, tys, ts);
    60 
    61 (*For system errors involving terms*)
    62 exception TERM of string * term list;
    63 
    64 fun raise_term msg ts = raise TERM (msg, ts);
    65 
    66 
    67 (*Note variable naming conventions!
    68     a,b,c: string
    69     f,g,h: functions (including terms of function type)
    70     i,j,m,n: int
    71     t,u: term
    72     v,w: indexnames
    73     x,y: any
    74     A,B,C: term (denoting formulae)
    75     T,U: typ
    76 *)
    77 
    78 
    79 (** Discriminators **)
    80 
    81 fun is_Const (Const _) = true
    82   | is_Const _ = false;
    83 
    84 fun is_Free (Free _) = true
    85   | is_Free _ = false;
    86 
    87 fun is_Var (Var _) = true
    88   | is_Var _ = false;
    89 
    90 fun is_TVar (TVar _) = true
    91   | is_TVar _ = false;
    92 
    93 (** Destructors **)
    94 
    95 fun dest_Const (Const x) =  x
    96   | dest_Const t = raise TERM("dest_Const", [t]);
    97 
    98 fun dest_Free (Free x) =  x
    99   | dest_Free t = raise TERM("dest_Free", [t]);
   100 
   101 fun dest_Var (Var x) =  x
   102   | dest_Var t = raise TERM("dest_Var", [t]);
   103 
   104 
   105 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   106 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   107   | binder_types _   =  [];
   108 
   109 (* maps  [T1,...,Tn]--->T  to T*)
   110 fun body_type (Type("fun",[S,T])) = body_type T
   111   | body_type T   =  T;
   112 
   113 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   114 fun strip_type T : typ list * typ =
   115   (binder_types T, body_type T);
   116 
   117 
   118 (*Compute the type of the term, checking that combinations are well-typed
   119   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   120 fun type_of1 (Ts, Const (_,T)) = T
   121   | type_of1 (Ts, Free  (_,T)) = T
   122   | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)  
   123   	handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   124   | type_of1 (Ts, Var (_,T)) = T
   125   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   126   | type_of1 (Ts, f$u) = 
   127       let val U = type_of1(Ts,u)
   128           and T = type_of1(Ts,f)
   129       in case T of
   130 	    Type("fun",[T1,T2]) =>
   131 	      if T1=U then T2  else raise TYPE
   132 	            ("type_of: type mismatch in application", [T1,U], [f$u])
   133 	  | _ => raise TYPE 
   134 		    ("type_of: function type is expected in application",
   135 		     [T,U], [f$u])
   136       end;
   137 
   138 fun type_of t : typ = type_of1 ([],t);
   139 
   140 (*Determines the type of a term, with minimal checking*)
   141 fun fastype_of1 (Ts, f$u) = 
   142     (case fastype_of1 (Ts,f) of
   143 	Type("fun",[_,T]) => T
   144 	| _ => raise TERM("fastype_of: expected function type", [f$u]))
   145   | fastype_of1 (_, Const (_,T)) = T
   146   | fastype_of1 (_, Free (_,T)) = T
   147   | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
   148   	 handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   149   | fastype_of1 (_, Var (_,T)) = T 
   150   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   151 
   152 fun fastype_of t : typ = fastype_of1 ([],t);
   153 
   154 
   155 (* maps  (x1,...,xn)t   to   t  *)
   156 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t  
   157   | strip_abs_body u  =  u;
   158 
   159 
   160 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   161 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t 
   162   | strip_abs_vars u  =  [] : (string*typ) list;
   163 
   164 
   165 fun strip_qnt_body qnt =
   166 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   167       | strip t = t
   168 in strip end;
   169 
   170 fun strip_qnt_vars qnt =
   171 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   172       | strip t  =  [] : (string*typ) list
   173 in strip end;
   174 
   175 
   176 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   177 val list_comb : term * term list -> term = foldl (op $);
   178 
   179 
   180 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   181 fun strip_comb u : term * term list = 
   182     let fun stripc (f$t, ts) = stripc (f, t::ts)
   183         |   stripc  x =  x 
   184     in  stripc(u,[])  end;
   185 
   186 
   187 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   188 fun head_of (f$t) = head_of f
   189   | head_of u = u;
   190 
   191 
   192 (*Number of atoms and abstractions in a term*)
   193 fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
   194   | size_of_term (f$t) = size_of_term f  +  size_of_term t
   195   | size_of_term _ = 1;
   196 
   197 fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
   198   | map_type_tvar f (T as TFree _) = T
   199   | map_type_tvar f (TVar x) = f x;
   200 
   201 fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts)
   202   | map_type_tfree f (TFree x) = f x
   203   | map_type_tfree f (T as TVar _) = T;
   204 
   205 (* apply a function to all types in a term *)
   206 fun map_term_types f =
   207 let fun map(Const(a,T)) = Const(a, f T)
   208       | map(Free(a,T)) = Free(a, f T)
   209       | map(Var(v,T)) = Var(v, f T)
   210       | map(t as Bound _)  = t
   211       | map(Abs(a,T,t)) = Abs(a, f T, map t)
   212       | map(f$t) = map f $ map t;
   213 in map end;
   214 
   215 (* iterate a function over all types in a term *)
   216 fun it_term_types f =
   217 let fun iter(Const(_,T), a) = f(T,a)
   218       | iter(Free(_,T), a) = f(T,a)
   219       | iter(Var(_,T), a) = f(T,a)
   220       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   221       | iter(f$u, a) = iter(f, iter(u, a))
   222       | iter(Bound _, a) = a
   223 in iter end
   224 
   225 
   226 (** Connectives of higher order logic **)
   227 
   228 val logicC: class = "logic";
   229 val logicS: sort = [logicC];
   230 
   231 fun itselfT ty = Type ("itself", [ty]);
   232 val a_itselfT = itselfT (TFree ("'a", logicS));
   233 
   234 val propT : typ = Type("prop",[]);
   235 
   236 val implies = Const("==>", propT-->propT-->propT);
   237 
   238 fun all T = Const("all", (T-->propT)-->propT);
   239 
   240 fun equals T = Const("==", T-->T-->propT);
   241 
   242 fun flexpair T = Const("=?=", T-->T-->propT);
   243 
   244 (* maps  !!x1...xn. t   to   t  *)
   245 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t  
   246   | strip_all_body t  =  t;
   247 
   248 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   249 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   250 		(a,T) :: strip_all_vars t 
   251   | strip_all_vars t  =  [] : (string*typ) list;
   252 
   253 (*increments a term's non-local bound variables
   254   required when moving a term within abstractions
   255      inc is  increment for bound variables
   256      lev is  level at which a bound variable is considered 'loose'*)
   257 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   258   | incr_bv (inc, lev, Abs(a,T,body)) =
   259 	Abs(a, T, incr_bv(inc,lev+1,body))
   260   | incr_bv (inc, lev, f$t) = 
   261       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   262   | incr_bv (inc, lev, u) = u;
   263 
   264 fun incr_boundvars  0  t = t
   265   | incr_boundvars inc t = incr_bv(inc,0,t);
   266 
   267 
   268 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   269    (Bound 0) is loose at level 0 *)
   270 fun add_loose_bnos (Bound i, lev, js) = 
   271 	if i<lev then js  else  (i-lev) ins_int js
   272   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   273   | add_loose_bnos (f$t, lev, js) =
   274 	add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   275   | add_loose_bnos (_, _, js) = js;
   276 
   277 fun loose_bnos t = add_loose_bnos (t, 0, []);
   278 
   279 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   280    level k or beyond. *)
   281 fun loose_bvar(Bound i,k) = i >= k
   282   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   283   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   284   | loose_bvar _ = false;
   285 
   286 
   287 (*Substitute arguments for loose bound variables.
   288   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   289   Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
   290 	and the appropriate call is  subst_bounds([b,a], c) .
   291   Loose bound variables >=n are reduced by "n" to
   292      compensate for the disappearance of lambdas.
   293 *)
   294 fun subst_bounds (args: term list, t) : term = 
   295   let val n = length args;
   296       fun subst (t as Bound i, lev) =
   297  	    if i<lev then  t    (*var is locally bound*)
   298 	    else  (case (drop (i-lev,args)) of
   299 		  []     => Bound(i-n)  (*loose: change it*)
   300 	        | arg::_ => incr_boundvars lev arg)
   301 	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   302 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   303 	| subst (t,lev) = t
   304   in   case args of [] => t  | _ => subst (t,0)  end;
   305 
   306 (*beta-reduce if possible, else form application*)
   307 fun betapply (Abs(_,_,t), u) = subst_bounds([u],t)
   308   | betapply (f,u) = f$u;
   309 
   310 (*Tests whether 2 terms are alpha-convertible and have same type.
   311   Note that constants and Vars may have more than one type.*)
   312 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   313   | (Free(a,T)) aconv (Free(b,U)) = a=b  andalso  T=U
   314   | (Var(v,T)) aconv (Var(w,U)) =   v=w  andalso  T=U
   315   | (Bound i) aconv (Bound j)  =   i=j
   316   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   317   | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
   318   | _ aconv _  =  false;
   319 
   320 (** Membership, insertion, union for terms **)
   321 
   322 fun mem_term (_, []) = false
   323   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   324 
   325 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   326 
   327 fun union_term (xs, []) = xs
   328   | union_term ([], ys) = ys
   329   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   330 
   331 (** Equality, membership and insertion of indexnames (string*ints) **)
   332 
   333 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
   334 fun eq_ix ((a:string, i:int), (a',i')) = (a=a') andalso i=i';
   335 
   336 (*membership in a list, optimized version for indexnames*)
   337 fun mem_ix (x:string*int, []) = false
   338   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
   339 
   340 (*insertion into list, optimized version for indexnames*)
   341 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   342 
   343 (** Equality, membership and insertion of sorts (string lists) **)
   344 
   345 fun eq_sort ([]:sort, []) = true
   346   | eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts)
   347   | eq_sort (_, _) = false;
   348 
   349 fun mem_sort (_:sort, []) = false
   350   | mem_sort (S, S'::Ss) = eq_sort (S, S') orelse mem_sort(S,Ss);
   351 
   352 fun ins_sort(S,Ss) = if mem_sort(S,Ss) then Ss else S :: Ss;
   353 
   354 fun union_sort (xs, []) = xs
   355   | union_sort ([], ys) = ys
   356   | union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
   357 
   358 (*are two term lists alpha-convertible in corresponding elements?*)
   359 fun aconvs ([],[]) = true
   360   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   361   | aconvs _ = false;
   362 
   363 (*A fast unification filter: true unless the two terms cannot be unified. 
   364   Terms must be NORMAL.  Treats all Vars as distinct. *)
   365 fun could_unify (t,u) =
   366   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   367 	| matchrands _ = true
   368   in case (head_of t , head_of u) of
   369 	(_, Var _) => true
   370       | (Var _, _) => true
   371       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   372       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   373       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   374       | (Abs _, _) =>  true   (*because of possible eta equality*)
   375       | (_, Abs _) =>  true
   376       | _ => false
   377   end;
   378 
   379 (*Substitute new for free occurrences of old in a term*)
   380 fun subst_free [] = (fn t=>t)
   381   | subst_free pairs =
   382       let fun substf u = 
   383 	    case gen_assoc (op aconv) (pairs, u) of
   384 		Some u' => u'
   385 	      | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   386 				 | t$u' => substf t $ substf u'
   387 				 | _ => u)
   388       in  substf  end;
   389 
   390 (*a total, irreflexive ordering on index names*)
   391 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   392 
   393 
   394 (*Abstraction of the term "body" over its occurrences of v, 
   395     which must contain no loose bound variables.
   396   The resulting term is ready to become the body of an Abs.*)
   397 fun abstract_over (v,body) =
   398   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   399       (case u of
   400           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   401 	| f$rand => abst(lev,f) $ abst(lev,rand)
   402 	| _ => u)
   403   in  abst(0,body)  end;
   404 
   405 
   406 (*Form an abstraction over a free variable.*)
   407 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   408 
   409 (*Abstraction over a list of free variables*)
   410 fun list_abs_free ([ ] ,     t) = t
   411   | list_abs_free ((a,T)::vars, t) = 
   412       absfree(a, T, list_abs_free(vars,t));
   413 
   414 (*Quantification over a list of free variables*)
   415 fun list_all_free ([], t: term) = t
   416   | list_all_free ((a,T)::vars, t) = 
   417         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   418 
   419 (*Quantification over a list of variables (already bound in body) *)
   420 fun list_all ([], t) = t
   421   | list_all ((a,T)::vars, t) = 
   422         (all T) $ (Abs(a, T, list_all(vars,t)));
   423 
   424 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)]. 
   425   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   426 fun subst_atomic [] t = t : term
   427   | subst_atomic (instl: (term*term) list) t =
   428       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   429 	    | subst (f$t') = subst f $ subst t'
   430 	    | subst t = (case assoc(instl,t) of
   431 		           Some u => u  |  None => t)
   432       in  subst t  end;
   433 
   434 (*Substitute for type Vars in a type*)
   435 fun typ_subst_TVars iTs T = if null iTs then T else
   436   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   437 	| subst(T as TFree _) = T
   438 	| subst(T as TVar(ixn,_)) =
   439             (case assoc(iTs,ixn) of None => T | Some(U) => U)
   440   in subst T end;
   441 
   442 (*Substitute for type Vars in a term*)
   443 val subst_TVars = map_term_types o typ_subst_TVars;
   444 
   445 (*Substitute for Vars in a term; see also envir/norm_term*)
   446 fun subst_Vars itms t = if null itms then t else
   447   let fun subst(v as Var(ixn,_)) =
   448             (case assoc(itms,ixn) of None => v | Some t => t)
   449         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   450         | subst(f$t) = subst f $ subst t
   451         | subst(t) = t
   452   in subst t end;
   453 
   454 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
   455 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   456   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   457         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   458         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   459             None   => Var(ixn,typ_subst_TVars iTs T)
   460           | Some t => t)
   461         | subst(b as Bound _) = b
   462         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   463         | subst(f$t) = subst f $ subst t
   464   in subst end;
   465 
   466 
   467 (*Computing the maximum index of a typ*)
   468 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   469   | maxidx_of_typ(TFree _) = ~1
   470   | maxidx_of_typ(TVar((_,i),_)) = i
   471 and maxidx_of_typs [] = ~1
   472   | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   473 
   474 
   475 (*Computing the maximum index of a term*)
   476 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   477   | maxidx_of_term (Bound _) = ~1
   478   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   479   | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   480   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   481   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   482 
   483 
   484 (* Increment the index of all Poly's in T by k *)
   485 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
   486 
   487 
   488 (**** Syntax-related declarations ****)
   489 
   490 
   491 (*Dummy type for parsing.  Will be replaced during type inference. *)
   492 val dummyT = Type("dummy",[]);
   493 
   494 (*scan a numeral of the given radix, normally 10*)
   495 fun scan_radixint (radix: int, cs) : int * string list =
   496   let val zero = ord"0"
   497       val limit = zero+radix
   498       fun scan (num,[]) = (num,[])
   499 	| scan (num, c::cs) =
   500 	      if  zero <= ord c  andalso  ord c < limit
   501 	      then scan(radix*num + ord c - zero, cs)
   502 	      else (num, c::cs)
   503   in  scan(0,cs)  end;
   504 
   505 fun scan_int cs = scan_radixint(10,cs);
   506 
   507 
   508 (*** Printing ***)
   509 
   510 
   511 (*Makes a variant of the name c distinct from the names in bs.
   512   First attaches the suffix "a" and then increments this. *)
   513 fun variant bs c : string =
   514   let fun vary2 c = if (c mem_string bs) then  vary2 (bump_string c)  else  c
   515       fun vary1 c = if (c mem_string bs) then  vary2 (c ^ "a")  else  c
   516   in  vary1 (if c="" then "u" else c)  end;
   517 
   518 (*Create variants of the list of names, with priority to the first ones*)
   519 fun variantlist ([], used) = []
   520   | variantlist(b::bs, used) = 
   521       let val b' = variant used b
   522       in  b' :: variantlist (bs, b'::used)  end;
   523 
   524 (** TFrees and TVars **)
   525 
   526 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   527 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   528 
   529 (*Accumulates the names in the term, suppressing duplicates.
   530   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   531 fun add_term_names (Const(a,_), bs) = a ins_string bs
   532   | add_term_names (Free(a,_), bs) = a ins_string bs
   533   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   534   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   535   | add_term_names (_, bs) = bs;
   536 
   537 (*Accumulates the TVars in a type, suppressing duplicates. *)
   538 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)
   539   | add_typ_tvars(TFree(_),vs) = vs
   540   | add_typ_tvars(TVar(v),vs) = v ins vs;
   541 
   542 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   543 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)
   544   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   545   | add_typ_tfree_names(TVar(_),fs) = fs;
   546 
   547 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)
   548   | add_typ_tfrees(TFree(f),fs) = f ins fs
   549   | add_typ_tfrees(TVar(_),fs) = fs;
   550 
   551 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms)
   552   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   553   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   554 
   555 (*Accumulates the TVars in a term, suppressing duplicates. *)
   556 val add_term_tvars = it_term_types add_typ_tvars;
   557 
   558 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   559 val add_term_tfrees = it_term_types add_typ_tfrees;
   560 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   561 
   562 val add_term_tvarnames = it_term_types add_typ_varnames;
   563 
   564 (*Non-list versions*)
   565 fun typ_tfrees T = add_typ_tfrees(T,[]);
   566 fun typ_tvars T = add_typ_tvars(T,[]);
   567 fun term_tfrees t = add_term_tfrees(t,[]);
   568 fun term_tvars t = add_term_tvars(t,[]);
   569 
   570 (*special code to enforce left-to-right collection of TVar-indexnames*)
   571 
   572 fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
   573   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
   574 				     else ixns@[ixn]
   575   | add_typ_ixns(ixns,TFree(_)) = ixns;
   576 
   577 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
   578   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
   579   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
   580   | add_term_tvar_ixns(Bound _,ixns) = ixns
   581   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
   582       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
   583   | add_term_tvar_ixns(f$t,ixns) =
   584       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   585 
   586 (** Frees and Vars **)
   587 
   588 (*a partial ordering (not reflexive) for atomic terms*)
   589 fun atless (Const (a,_), Const (b,_))  =  a<b
   590   | atless (Free (a,_), Free (b,_)) =  a<b
   591   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   592   | atless (Bound i, Bound j)  =   i<j
   593   | atless _  =  false;
   594 
   595 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   596 fun insert_aterm (t,us) =
   597   let fun inserta [] = [t]
   598         | inserta (us as u::us') = 
   599 	      if atless(t,u) then t::us
   600 	      else if t=u then us (*duplicate*)
   601 	      else u :: inserta(us')
   602   in  inserta us  end;
   603 
   604 (*Accumulates the Vars in the term, suppressing duplicates*)
   605 fun add_term_vars (t, vars: term list) = case t of
   606     Var   _ => insert_aterm(t,vars)
   607   | Abs (_,_,body) => add_term_vars(body,vars)
   608   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   609   | _ => vars;
   610 
   611 fun term_vars t = add_term_vars(t,[]);
   612 
   613 (*Accumulates the Frees in the term, suppressing duplicates*)
   614 fun add_term_frees (t, frees: term list) = case t of
   615     Free   _ => insert_aterm(t,frees)
   616   | Abs (_,_,body) => add_term_frees(body,frees)
   617   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   618   | _ => frees;
   619 
   620 fun term_frees t = add_term_frees(t,[]);
   621 
   622 (*Given an abstraction over P, replaces the bound variable by a Free variable
   623   having a unique name. *)
   624 fun variant_abs (a,T,P) =
   625   let val b = variant (add_term_names(P,[])) a
   626   in  (b,  subst_bounds ([Free(b,T)], P))  end;
   627 
   628 (* renames and reverses the strings in vars away from names *)
   629 fun rename_aTs names vars : (string*typ)list =
   630   let fun rename_aT (vars,(a,T)) =
   631 		(variant (map #1 vars @ names) a, T) :: vars
   632   in foldl rename_aT ([],vars) end;
   633 
   634 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   635 
   636 
   637 
   638 (*** Compression of terms and types by sharing common subtrees.  
   639      Saves 50-75% on storage requirements.  As it is fairly slow, 
   640      it is called only for axioms, stored theorems, etc. ***)
   641 
   642 (** Sharing of types **)
   643 
   644 fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match
   645   | atomic_tag (TFree (a,_)) = a
   646   | atomic_tag (TVar ((a,_),_)) = a;
   647 
   648 fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
   649   | type_tag T = atomic_tag T;
   650 
   651 val memo_types = ref (Symtab.null : typ list Symtab.table);
   652 
   653 fun find_type (T, []: typ list) = None
   654   | find_type (T, T'::Ts) =
   655        if T=T' then Some T'
   656        else find_type (T, Ts);
   657 
   658 fun compress_type T =
   659   let val tag = type_tag T
   660       val tylist = the (Symtab.lookup (!memo_types, tag))
   661 	           handle _ => []
   662   in  
   663       case find_type (T,tylist) of
   664 	Some T' => T'
   665       | None => 
   666 	    let val T' =
   667 		case T of
   668 		    Type (a,Ts) => Type (a, map compress_type Ts)
   669 		  | _ => T
   670 	    in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
   671 		T
   672 	    end
   673   end
   674   handle Match =>
   675       let val Type (a,Ts) = T
   676       in  Type (a, map compress_type Ts)  end;
   677 
   678 (** Sharing of atomic terms **)
   679 
   680 val memo_terms = ref (Symtab.null : term list Symtab.table);
   681 
   682 fun find_term (t, []: term list) = None
   683   | find_term (t, t'::ts) =
   684        if t=t' then Some t'
   685        else find_term (t, ts);
   686 
   687 fun const_tag (Const (a,_)) = a
   688   | const_tag (Free (a,_))  = a
   689   | const_tag (Var ((a,i),_)) = a
   690   | const_tag (t as Bound _)  = ".B.";
   691 
   692 fun share_term (t $ u) = share_term t $ share_term u
   693   | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
   694   | share_term t =
   695       let val tag = const_tag t
   696 	  val ts = the (Symtab.lookup (!memo_terms, tag))
   697 	               handle _ => []
   698       in 
   699 	  case find_term (t,ts) of
   700 	      Some t' => t'
   701 	    | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
   702 		       t)
   703       end;
   704 
   705 val compress_term = share_term o map_term_types compress_type;
   706 
   707 end;
   708 
   709 open Term;