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