src/Pure/term.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2752 74a9aead96c8
child 2959 071bfb16586f
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     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 fun loose_bvar1(Bound i,k) = i = k
   287   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   288   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   289   | loose_bvar1 _ = false;
   290 
   291 (*Substitute arguments for loose bound variables.
   292   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   293   Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
   294 	and the appropriate call is  subst_bounds([b,a], c) .
   295   Loose bound variables >=n are reduced by "n" to
   296      compensate for the disappearance of lambdas.
   297 *)
   298 fun subst_bounds (args: term list, t) : term = 
   299   let val n = length args;
   300       fun subst (t as Bound i, lev) =
   301  	   (if i<lev then  t    (*var is locally bound*)
   302 	    else  incr_boundvars lev (List.nth(args, i-lev))
   303 		    handle Subscript => Bound(i-n)  (*loose: change it*))
   304 	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   305 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   306 	| subst (t,lev) = t
   307   in   case args of [] => t  | _ => subst (t,0)  end;
   308 
   309 (*Special case: one argument*)
   310 fun subst_bound (arg, t) : term = 
   311   let fun subst (t as Bound i, lev) =
   312  	    if i<lev then  t    (*var is locally bound*)
   313 	    else  if i=lev then incr_boundvars lev arg
   314 		           else Bound(i-1)  (*loose: change it*)
   315 	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   316 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   317 	| subst (t,lev) = t
   318   in  subst (t,0)  end;
   319 
   320 (*beta-reduce if possible, else form application*)
   321 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   322   | betapply (f,u) = f$u;
   323 
   324 (** Equality, membership and insertion of indexnames (string*ints) **)
   325 
   326 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
   327 fun eq_ix ((a:string, i:int), (a',i')) = (a=a') andalso i=i';
   328 
   329 (*membership in a list, optimized version for indexnames*)
   330 fun mem_ix (x:string*int, []) = false
   331   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
   332 
   333 (*insertion into list, optimized version for indexnames*)
   334 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs;
   335 
   336 (*Tests whether 2 terms are alpha-convertible and have same type.
   337   Note that constants and Vars may have more than one type.*)
   338 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   339   | (Free(a,T))  aconv (Free(b,U))  = a=b  andalso  T=U
   340   | (Var(v,T))   aconv (Var(w,U))   = eq_ix(v,w)  andalso  T=U
   341   | (Bound i)    aconv (Bound j)    = i=j
   342   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   343   | (f$t)        aconv (g$u)        = (f aconv g) andalso (t aconv u)
   344   | _ aconv _  =  false;
   345 
   346 (** Membership, insertion, union for terms **)
   347 
   348 fun mem_term (_, []) = false
   349   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   350 
   351 fun subset_term ([], ys) = true
   352   | subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys);
   353 
   354 fun eq_set_term (xs, ys) =
   355     xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs));
   356 
   357 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   358 
   359 fun union_term (xs, []) = xs
   360   | union_term ([], ys) = ys
   361   | union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys));
   362 
   363 (** Equality, membership and insertion of sorts (string lists) **)
   364 
   365 fun eq_sort ([]:sort, []) = true
   366   | eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts)
   367   | eq_sort (_, _) = false;
   368 
   369 fun mem_sort (_:sort, []) = false
   370   | mem_sort (S, S'::Ss) = eq_sort (S, S') orelse mem_sort(S,Ss);
   371 
   372 fun ins_sort(S,Ss) = if mem_sort(S,Ss) then Ss else S :: Ss;
   373 
   374 fun union_sort (xs, []) = xs
   375   | union_sort ([], ys) = ys
   376   | union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys));
   377 
   378 fun subset_sort ([], ys) = true
   379   | subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys);
   380 
   381 fun eq_set_sort (xs, ys) =
   382     xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs));
   383 
   384 (*are two term lists alpha-convertible in corresponding elements?*)
   385 fun aconvs ([],[]) = true
   386   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   387   | aconvs _ = false;
   388 
   389 (*A fast unification filter: true unless the two terms cannot be unified. 
   390   Terms must be NORMAL.  Treats all Vars as distinct. *)
   391 fun could_unify (t,u) =
   392   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   393 	| matchrands _ = true
   394   in case (head_of t , head_of u) of
   395 	(_, Var _) => true
   396       | (Var _, _) => true
   397       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   398       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   399       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   400       | (Abs _, _) =>  true   (*because of possible eta equality*)
   401       | (_, Abs _) =>  true
   402       | _ => false
   403   end;
   404 
   405 (*Substitute new for free occurrences of old in a term*)
   406 fun subst_free [] = (fn t=>t)
   407   | subst_free pairs =
   408       let fun substf u = 
   409 	    case gen_assoc (op aconv) (pairs, u) of
   410 		Some u' => u'
   411 	      | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   412 				 | t$u' => substf t $ substf u'
   413 				 | _ => u)
   414       in  substf  end;
   415 
   416 (*a total, irreflexive ordering on index names*)
   417 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   418 
   419 
   420 (*Abstraction of the term "body" over its occurrences of v, 
   421     which must contain no loose bound variables.
   422   The resulting term is ready to become the body of an Abs.*)
   423 fun abstract_over (v,body) =
   424   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   425       (case u of
   426           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   427 	| f$rand => abst(lev,f) $ abst(lev,rand)
   428 	| _ => u)
   429   in  abst(0,body)  end;
   430 
   431 
   432 (*Form an abstraction over a free variable.*)
   433 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   434 
   435 (*Abstraction over a list of free variables*)
   436 fun list_abs_free ([ ] ,     t) = t
   437   | list_abs_free ((a,T)::vars, t) = 
   438       absfree(a, T, list_abs_free(vars,t));
   439 
   440 (*Quantification over a list of free variables*)
   441 fun list_all_free ([], t: term) = t
   442   | list_all_free ((a,T)::vars, t) = 
   443         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   444 
   445 (*Quantification over a list of variables (already bound in body) *)
   446 fun list_all ([], t) = t
   447   | list_all ((a,T)::vars, t) = 
   448         (all T) $ (Abs(a, T, list_all(vars,t)));
   449 
   450 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)]. 
   451   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   452 fun subst_atomic [] t = t : term
   453   | subst_atomic (instl: (term*term) list) t =
   454       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   455 	    | subst (f$t') = subst f $ subst t'
   456 	    | subst t = (case assoc(instl,t) of
   457 		           Some u => u  |  None => t)
   458       in  subst t  end;
   459 
   460 (*Substitute for type Vars in a type*)
   461 fun typ_subst_TVars iTs T = if null iTs then T else
   462   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   463 	| subst(T as TFree _) = T
   464 	| subst(T as TVar(ixn,_)) =
   465             (case assoc(iTs,ixn) of None => T | Some(U) => U)
   466   in subst T end;
   467 
   468 (*Substitute for type Vars in a term*)
   469 val subst_TVars = map_term_types o typ_subst_TVars;
   470 
   471 (*Substitute for Vars in a term; see also envir/norm_term*)
   472 fun subst_Vars itms t = if null itms then t else
   473   let fun subst(v as Var(ixn,_)) =
   474             (case assoc(itms,ixn) of None => v | Some t => t)
   475         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   476         | subst(f$t) = subst f $ subst t
   477         | subst(t) = t
   478   in subst t end;
   479 
   480 (*Substitute for type/term Vars in a term; see also envir/norm_term*)
   481 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   482   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   483         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   484         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   485             None   => Var(ixn,typ_subst_TVars iTs T)
   486           | Some t => t)
   487         | subst(b as Bound _) = b
   488         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   489         | subst(f$t) = subst f $ subst t
   490   in subst end;
   491 
   492 
   493 (*Computing the maximum index of a typ*)
   494 fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   495   | maxidx_of_typ(TFree _) = ~1
   496   | maxidx_of_typ(TVar((_,i),_)) = i
   497 and maxidx_of_typs [] = ~1
   498   | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
   499 
   500 
   501 (*Computing the maximum index of a term*)
   502 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   503   | maxidx_of_term (Bound _) = ~1
   504   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   505   | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
   506   | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
   507   | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
   508 
   509 
   510 (* Increment the index of all Poly's in T by k *)
   511 fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S));
   512 
   513 
   514 (**** Syntax-related declarations ****)
   515 
   516 
   517 (*Dummy type for parsing.  Will be replaced during type inference. *)
   518 val dummyT = Type("dummy",[]);
   519 
   520 (*scan a numeral of the given radix, normally 10*)
   521 fun scan_radixint (radix: int, cs) : int * string list =
   522   let val zero = ord"0"
   523       val limit = zero+radix
   524       fun scan (num,[]) = (num,[])
   525 	| scan (num, c::cs) =
   526 	      if  zero <= ord c  andalso  ord c < limit
   527 	      then scan(radix*num + ord c - zero, cs)
   528 	      else (num, c::cs)
   529   in  scan(0,cs)  end;
   530 
   531 fun scan_int cs = scan_radixint(10,cs);
   532 
   533 
   534 (*** Printing ***)
   535 
   536 
   537 (*Makes a variant of the name c distinct from the names in bs.
   538   First attaches the suffix "a" and then increments this. *)
   539 fun variant bs c : string =
   540   let fun vary2 c = if (c mem_string bs) then  vary2 (bump_string c)  else  c
   541       fun vary1 c = if (c mem_string bs) then  vary2 (c ^ "a")  else  c
   542   in  vary1 (if c="" then "u" else c)  end;
   543 
   544 (*Create variants of the list of names, with priority to the first ones*)
   545 fun variantlist ([], used) = []
   546   | variantlist(b::bs, used) = 
   547       let val b' = variant used b
   548       in  b' :: variantlist (bs, b'::used)  end;
   549 
   550 (** TFrees and TVars **)
   551 
   552 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   553 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   554 
   555 (*Accumulates the names in the term, suppressing duplicates.
   556   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   557 fun add_term_names (Const(a,_), bs) = a ins_string bs
   558   | add_term_names (Free(a,_), bs) = a ins_string bs
   559   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   560   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   561   | add_term_names (_, bs) = bs;
   562 
   563 (*Accumulates the TVars in a type, suppressing duplicates. *)
   564 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)
   565   | add_typ_tvars(TFree(_),vs) = vs
   566   | add_typ_tvars(TVar(v),vs) = v ins vs;
   567 
   568 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   569 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)
   570   | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   571   | add_typ_tfree_names(TVar(_),fs) = fs;
   572 
   573 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)
   574   | add_typ_tfrees(TFree(f),fs) = f ins fs
   575   | add_typ_tfrees(TVar(_),fs) = fs;
   576 
   577 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms)
   578   | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   579   | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   580 
   581 (*Accumulates the TVars in a term, suppressing duplicates. *)
   582 val add_term_tvars = it_term_types add_typ_tvars;
   583 
   584 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   585 val add_term_tfrees = it_term_types add_typ_tfrees;
   586 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   587 
   588 val add_term_tvarnames = it_term_types add_typ_varnames;
   589 
   590 (*Non-list versions*)
   591 fun typ_tfrees T = add_typ_tfrees(T,[]);
   592 fun typ_tvars T = add_typ_tvars(T,[]);
   593 fun term_tfrees t = add_term_tfrees(t,[]);
   594 fun term_tvars t = add_term_tvars(t,[]);
   595 
   596 (*special code to enforce left-to-right collection of TVar-indexnames*)
   597 
   598 fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts)
   599   | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
   600 				     else ixns@[ixn]
   601   | add_typ_ixns(ixns,TFree(_)) = ixns;
   602 
   603 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
   604   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
   605   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
   606   | add_term_tvar_ixns(Bound _,ixns) = ixns
   607   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
   608       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
   609   | add_term_tvar_ixns(f$t,ixns) =
   610       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
   611 
   612 (** Frees and Vars **)
   613 
   614 (*a partial ordering (not reflexive) for atomic terms*)
   615 fun atless (Const (a,_), Const (b,_))  =  a<b
   616   | atless (Free (a,_), Free (b,_)) =  a<b
   617   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   618   | atless (Bound i, Bound j)  =   i<j
   619   | atless _  =  false;
   620 
   621 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   622 fun insert_aterm (t,us) =
   623   let fun inserta [] = [t]
   624         | inserta (us as u::us') = 
   625 	      if atless(t,u) then t::us
   626 	      else if t=u then us (*duplicate*)
   627 	      else u :: inserta(us')
   628   in  inserta us  end;
   629 
   630 (*Accumulates the Vars in the term, suppressing duplicates*)
   631 fun add_term_vars (t, vars: term list) = case t of
   632     Var   _ => insert_aterm(t,vars)
   633   | Abs (_,_,body) => add_term_vars(body,vars)
   634   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   635   | _ => vars;
   636 
   637 fun term_vars t = add_term_vars(t,[]);
   638 
   639 (*Accumulates the Frees in the term, suppressing duplicates*)
   640 fun add_term_frees (t, frees: term list) = case t of
   641     Free   _ => insert_aterm(t,frees)
   642   | Abs (_,_,body) => add_term_frees(body,frees)
   643   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   644   | _ => frees;
   645 
   646 fun term_frees t = add_term_frees(t,[]);
   647 
   648 (*Given an abstraction over P, replaces the bound variable by a Free variable
   649   having a unique name. *)
   650 fun variant_abs (a,T,P) =
   651   let val b = variant (add_term_names(P,[])) a
   652   in  (b,  subst_bound (Free(b,T), P))  end;
   653 
   654 (* renames and reverses the strings in vars away from names *)
   655 fun rename_aTs names vars : (string*typ)list =
   656   let fun rename_aT (vars,(a,T)) =
   657 		(variant (map #1 vars @ names) a, T) :: vars
   658   in foldl rename_aT ([],vars) end;
   659 
   660 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
   661 
   662 
   663 
   664 (*** Compression of terms and types by sharing common subtrees.  
   665      Saves 50-75% on storage requirements.  As it is fairly slow, 
   666      it is called only for axioms, stored theorems, etc. ***)
   667 
   668 (** Sharing of types **)
   669 
   670 fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match
   671   | atomic_tag (TFree (a,_)) = a
   672   | atomic_tag (TVar ((a,_),_)) = a;
   673 
   674 fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
   675   | type_tag T = atomic_tag T;
   676 
   677 val memo_types = ref (Symtab.null : typ list Symtab.table);
   678 
   679 fun find_type (T, []: typ list) = None
   680   | find_type (T, T'::Ts) =
   681        if T=T' then Some T'
   682        else find_type (T, Ts);
   683 
   684 fun compress_type T =
   685   let val tag = type_tag T
   686       val tylist = the (Symtab.lookup (!memo_types, tag))
   687 	           handle _ => []
   688   in  
   689       case find_type (T,tylist) of
   690 	Some T' => T'
   691       | None => 
   692 	    let val T' =
   693 		case T of
   694 		    Type (a,Ts) => Type (a, map compress_type Ts)
   695 		  | _ => T
   696 	    in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
   697 		T
   698 	    end
   699   end
   700   handle Match =>
   701       let val Type (a,Ts) = T
   702       in  Type (a, map compress_type Ts)  end;
   703 
   704 (** Sharing of atomic terms **)
   705 
   706 val memo_terms = ref (Symtab.null : term list Symtab.table);
   707 
   708 fun find_term (t, []: term list) = None
   709   | find_term (t, t'::ts) =
   710        if t=t' then Some t'
   711        else find_term (t, ts);
   712 
   713 fun const_tag (Const (a,_)) = a
   714   | const_tag (Free (a,_))  = a
   715   | const_tag (Var ((a,i),_)) = a
   716   | const_tag (t as Bound _)  = ".B.";
   717 
   718 fun share_term (t $ u) = share_term t $ share_term u
   719   | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
   720   | share_term t =
   721       let val tag = const_tag t
   722 	  val ts = the (Symtab.lookup (!memo_terms, tag))
   723 	               handle _ => []
   724       in 
   725 	  case find_term (t,ts) of
   726 	      Some t' => t'
   727 	    | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
   728 		       t)
   729       end;
   730 
   731 val compress_term = share_term o map_term_types compress_type;
   732 
   733 end;
   734 
   735 open Term;