diff -r 000000000000 -r a5a9c433f639 src/Pure/term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/term.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,549 @@ +(* Title: term.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright Cambridge University 1992 +*) + + +(*Simply typed lambda-calculus: types, terms, and basic operations*) + + +(*Indexnames can be quickly renamed by adding an offset to the integer part, + for resolution.*) +type indexname = string*int; + +(* Types are classified by classes. *) +type class = string; +type sort = class list; + +(* The sorts attached to TFrees and TVars specify the sort of that variable *) +datatype typ = Type of string * typ list + | TFree of string * sort + | TVar of indexname * sort; + +infixr 5 -->; +fun S --> T = Type("fun",[S,T]); + +(*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*) +infixr --->; +val op ---> = foldr (op -->); + + +(*terms. Bound variables are indicated by depth number. + Free variables, (scheme) variables and constants have names. + An term is "closed" if there every bound variable of level "lev" + is enclosed by at least "lev" abstractions. + + It is possible to create meaningless terms containing loose bound vars + or type mismatches. But such terms are not allowed in rules. *) + + + +infix 9 $; (*application binds tightly!*) +datatype term = + Const of string * typ + | Free of string * typ + | Var of indexname * typ + | Bound of int + | Abs of string*typ*term + | op $ of term*term; + + +(*For errors involving type mismatches*) +exception TYPE of string * typ list * term list; + +(*For system errors involving terms*) +exception TERM of string * term list; + + +(*Note variable naming conventions! + a,b,c: string + f,g,h: functions (including terms of function type) + i,j,m,n: int + t,u: term + v,w: indexnames + x,y: any + A,B,C: term (denoting formulae) + T,U: typ +*) + + +(** Discriminators **) + +fun is_Const (Const _) = true + | is_Const _ = false; + +fun is_Free (Free _) = true + | is_Free _ = false; + +fun is_Var (Var _) = true + | is_Var _ = false; + +fun is_TVar (TVar _) = true + | is_TVar _ = false; + +(** Destructors **) + +fun dest_Const (Const x) = x + | dest_Const t = raise TERM("dest_Const", [t]); + +fun dest_Free (Free x) = x + | dest_Free t = raise TERM("dest_Free", [t]); + +fun dest_Var (Var x) = x + | dest_Var t = raise TERM("dest_Var", [t]); + + +(* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*) +fun binder_types (Type("fun",[S,T])) = S :: binder_types T + | binder_types _ = []; + +(* maps [T1,...,Tn]--->T to T*) +fun body_type (Type("fun",[S,T])) = body_type T + | body_type T = T; + +(* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) +fun strip_type T : typ list * typ = + (binder_types T, body_type T); + + +(*Compute the type of the term, checking that combinations are well-typed + Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*) +fun type_of1 (Ts, Const (_,T)) = T + | type_of1 (Ts, Free (_,T)) = T + | type_of1 (Ts, Bound i) = (nth_elem (i,Ts) + handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i])) + | type_of1 (Ts, Var (_,T)) = T + | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body) + | type_of1 (Ts, f$u) = + let val U = type_of1(Ts,u) + and T = type_of1(Ts,f) + in case T of + Type("fun",[T1,T2]) => + if T1=U then T2 else raise TYPE + ("type_of: type mismatch in application", [T1,U], [f$u]) + | _ => raise TYPE ("type_of: Rator must have function type", + [T,U], [f$u]) + end; + + +fun type_of t : typ = type_of1 ([],t); + +(*Determines the type of a term, with minimal checking*) +fun fastype_of(Ts, f$u) = (case fastype_of(Ts,f) of + Type("fun",[_,T]) => T + | _ => raise TERM("fastype_of: expected function type", [f$u])) + | fastype_of(_, Const (_,T)) = T + | fastype_of(_, Free (_,T)) = T + | fastype_of(Ts, Bound i) = (nth_elem(i,Ts) + handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) + | fastype_of(_, Var (_,T)) = T + | fastype_of(Ts, Abs (_,T,u)) = T --> fastype_of(T::Ts, u); + + +(* maps (x1,...,xn)t to t *) +fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t + | strip_abs_body u = u; + + +(* maps (x1,...,xn)t to [x1, ..., xn] *) +fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t + | strip_abs_vars u = [] : (string*typ) list; + + +fun strip_qnt_body qnt = +let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm + | strip t = t +in strip end; + +fun strip_qnt_vars qnt = +let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else [] + | strip t = [] : (string*typ) list +in strip end; + + +(* maps (f, [t1,...,tn]) to f(t1,...,tn) *) +val list_comb : term * term list -> term = foldl (op $); + + +(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) +fun strip_comb u : term * term list = + let fun stripc (f$t, ts) = stripc (f, t::ts) + | stripc x = x + in stripc(u,[]) end; + + +(* maps f(t1,...,tn) to f , which is never a combination *) +fun head_of (f$t) = head_of f + | head_of u = u; + + +(*Number of atoms and abstractions in a term*) +fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body + | size_of_term (f$t) = size_of_term f + size_of_term t + | size_of_term _ = 1; + + +(* apply a function to all types in a term *) +fun map_term_types f = +let fun map(Const(a,T)) = Const(a, f T) + | map(Free(a,T)) = Free(a, f T) + | map(Var(v,T)) = Var(v, f T) + | map(t as Bound _) = t + | map(Abs(a,T,t)) = Abs(a, f T, map t) + | map(f$t) = map f $ map t; +in map end; + +(* iterate a function over all types in a term *) +fun it_term_types f = +let fun iter(Const(_,T), a) = f(T,a) + | iter(Free(_,T), a) = f(T,a) + | iter(Var(_,T), a) = f(T,a) + | iter(Abs(_,T,t), a) = iter(t,f(T,a)) + | iter(f$u, a) = iter(f, iter(u, a)) + | iter(Bound _, a) = a +in iter end + + +(** Connectives of higher order logic **) + +val propT : typ = Type("prop",[]); + +val implies = Const("==>", propT-->propT-->propT); + +fun all T = Const("all", (T-->propT)-->propT); + +fun equals T = Const("==", T-->T-->propT); + +fun flexpair T = Const("=?=", T-->T-->propT); + +(* maps !!x1...xn. t to t *) +fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t + | strip_all_body t = t; + +(* maps !!x1...xn. t to [x1, ..., xn] *) +fun strip_all_vars (Const("all",_)$Abs(a,T,t)) = + (a,T) :: strip_all_vars t + | strip_all_vars t = [] : (string*typ) list; + +(*increments a term's non-local bound variables + required when moving a term within abstractions + inc is increment for bound variables + lev is level at which a bound variable is considered 'loose'*) +fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u + | incr_bv (inc, lev, Abs(a,T,body)) = + Abs(a, T, incr_bv(inc,lev+1,body)) + | incr_bv (inc, lev, f$t) = + incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) + | incr_bv (inc, lev, u) = u; + +fun incr_boundvars 0 t = t + | incr_boundvars inc t = incr_bv(inc,0,t); + + +(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. + (Bound 0) is loose at level 0 *) +fun add_loose_bnos (Bound i, lev, js) = + if i= k + | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) + | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) + | loose_bvar _ = false; + + +(*Substitute arguments for loose bound variables. + Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). + Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 + and the appropriate call is subst_bounds([b,a], c) . + Loose bound variables >=n are reduced by "n" to + compensate for the disappearance of lambdas. +*) +fun subst_bounds (args: term list, t) : term = + let val n = length args; + fun subst (t as Bound i, lev) = + if i Bound(i-n) (*loose: change it*) + | arg::_ => incr_boundvars lev arg) + | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) + | subst (f$t, lev) = subst(f,lev) $ subst(t,lev) + | subst (t,lev) = t + in case args of [] => t | _ => subst (t,0) end; + +(*beta-reduce if possible, else form application*) +fun betapply (Abs(_,_,t), u) = subst_bounds([u],t) + | betapply (f,u) = f$u; + +(*Tests whether 2 terms are alpha-convertible and have same type. + Note that constants and Vars may have more than one type.*) +infix aconv; +fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U + | (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U + | (Var(v,T)) aconv (Var(w,U)) = v=w andalso T=U + | (Bound i) aconv (Bound j) = i=j + | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U + | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) + | _ aconv _ = false; + +(*are two term lists alpha-convertible in corresponding elements?*) +fun aconvs ([],[]) = true + | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us) + | aconvs _ = false; + +(*A fast unification filter: true unless the two terms cannot be unified. + Terms must be NORMAL. Treats all Vars as distinct. *) +fun could_unify (t,u) = + let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g) + | matchrands _ = true + in case (head_of t , head_of u) of + (_, Var _) => true + | (Var _, _) => true + | (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) + | (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u) + | (Bound i, Bound j) => i=j andalso matchrands(t,u) + | (Abs _, _) => true (*because of possible eta equality*) + | (_, Abs _) => true + | _ => false + end; + +(*Substitute new for free occurrences of old in a term*) +fun subst_free [] = (fn t=>t) + | subst_free pairs = + let fun substf u = + case gen_assoc (op aconv) (pairs, u) of + Some u' => u' + | None => (case u of Abs(a,T,t) => Abs(a, T, substf t) + | t$u' => substf t $ substf u' + | _ => u) + in substf end; + +(*a total, irreflexive ordering on index names*) +fun xless ((a,i), (b,j): indexname) = i Abs(a, T, abst(lev+1, t)) + | f$rand => abst(lev,f) $ abst(lev,rand) + | _ => u) + in abst(0,body) end; + + +(*Form an abstraction over a free variable.*) +fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body)); + +(*Abstraction over a list of free variables*) +fun list_abs_free ([ ] , t) = t + | list_abs_free ((a,T)::vars, t) = + absfree(a, T, list_abs_free(vars,t)); + +(*Quantification over a list of free variables*) +fun list_all_free ([], t: term) = t + | list_all_free ((a,T)::vars, t) = + (all T) $ (absfree(a, T, list_all_free(vars,t))); + +(*Quantification over a list of variables (already bound in body) *) +fun list_all ([], t) = t + | list_all ((a,T)::vars, t) = + (all T) $ (Abs(a, T, list_all(vars,t))); + +(*Replace the ATOMIC term ti by ui; instl = [(t1,u1), ..., (tn,un)]. + A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) +fun subst_atomic [] t = t : term + | subst_atomic (instl: (term*term) list) t = + let fun subst (Abs(a,T,body)) = Abs(a, T, subst body) + | subst (f$t') = subst f $ subst t' + | subst t = (case assoc(instl,t) of + Some u => u | None => t) + in subst t end; + +fun typ_subst_TVars iTs T = if null iTs then T else + let fun subst(Type(a,Ts)) = Type(a, map subst Ts) + | subst(T as TFree _) = T + | subst(T as TVar(ixn,_)) = + (case assoc(iTs,ixn) of None => T | Some(U) => U) + in subst T end; + +val subst_TVars = map_term_types o typ_subst_TVars; + +fun subst_Vars itms t = if null itms then t else + let fun subst(v as Var(ixn,_)) = + (case assoc(itms,ixn) of None => v | Some t => t) + | subst(Abs(a,T,t)) = Abs(a,T,subst t) + | subst(f$t) = subst f $ subst t + | subst(t) = t + in subst t end; + +fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else + let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T) + | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T) + | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of + None => Var(ixn,typ_subst_TVars iTs T) + | Some t => t) + | subst(b as Bound _) = b + | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t) + | subst(f$t) = subst f $ subst t + in subst end; + + +(*Computing the maximum index of a typ*) +fun maxidx_of_typ(Type(_,Ts)) = + if Ts=[] then ~1 else max(map maxidx_of_typ Ts) + | maxidx_of_typ(TFree _) = ~1 + | maxidx_of_typ(TVar((_,i),_)) = i; + + +(*Computing the maximum index of a term*) +fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T + | maxidx_of_term (Bound _) = ~1 + | maxidx_of_term (Free(_,T)) = maxidx_of_typ T + | maxidx_of_term (Var ((_,i), T)) = max[i, maxidx_of_typ T] + | maxidx_of_term (Abs (_,T,body)) = max[maxidx_of_term body, maxidx_of_typ T] + | maxidx_of_term (f$t) = max [maxidx_of_term f, maxidx_of_term t]; + + +(* Increment the index of all Poly's in T by k *) +fun incr_tvar k (Type(a,Ts)) = Type(a, map (incr_tvar k) Ts) + | incr_tvar k (T as TFree _) = T + | incr_tvar k (TVar((a,i),rs)) = TVar((a,i+k),rs); + + +(**** Syntax-related declarations ****) + + +(*Dummy type for parsing. Will be replaced during type inference. *) +val dummyT = Type("dummy",[]); + +(*scan a numeral of the given radix, normally 10*) +fun scan_radixint (radix: int, cs) : int * string list = + let val zero = ord"0" + val limit = zero+radix + fun scan (num,[]) = (num,[]) + | scan (num, c::cs) = + if zero <= ord c andalso ord c < limit + then scan(radix*num + ord c - zero, cs) + else (num, c::cs) + in scan(0,cs) end; + +fun scan_int cs = scan_radixint(10,cs); + + +(*** Printing ***) + + +(*Makes a variant of the name c distinct from the names in bs. + First attaches the suffix "a" and then increments this. *) +fun variant bs c : string = + let fun vary2 c = if (c mem bs) then vary2 (bump_string c) else c + fun vary1 c = if (c mem bs) then vary2 (c ^ "a") else c + in vary1 (if c="" then "u" else c) end; + +(*Create variants of the list of names, with priority to the first ones*) +fun variantlist ([], used) = [] + | variantlist(b::bs, used) = + let val b' = variant used b + in b' :: variantlist (bs, b'::used) end; + +(** TFrees and TVars **) + +(*maps (bs,v) to v'::bs this reverses the identifiers bs*) +fun add_new_id (bs, c) : string list = variant bs c :: bs; + +(*Accumulates the names in the term, suppressing duplicates. + Includes Frees and Consts. For choosing unambiguous bound var names.*) +fun add_term_names (Const(a,_), bs) = a ins bs + | add_term_names (Free(a,_), bs) = a ins bs + | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) + | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) + | add_term_names (_, bs) = bs; + +(*Accumulates the TVars in a type, suppressing duplicates. *) +fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs) + | add_typ_tvars(TFree(_),vs) = vs + | add_typ_tvars(TVar(v),vs) = v ins vs; + +(*Accumulates the TFrees in a type, suppressing duplicates. *) +fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs) + | add_typ_tfree_names(TFree(f,_),fs) = f ins fs + | add_typ_tfree_names(TVar(_),fs) = fs; + +fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs) + | add_typ_tfrees(TFree(f),fs) = f ins fs + | add_typ_tfrees(TVar(_),fs) = fs; + +(*Accumulates the TVars in a term, suppressing duplicates. *) +val add_term_tvars = it_term_types add_typ_tvars; +val add_term_tvar_ixns = (map #1) o (it_term_types add_typ_tvars); + +(*Accumulates the TFrees in a term, suppressing duplicates. *) +val add_term_tfrees = it_term_types add_typ_tfrees; +val add_term_tfree_names = it_term_types add_typ_tfree_names; + +(*Non-list versions*) +fun typ_tfrees T = add_typ_tfrees(T,[]); +fun typ_tvars T = add_typ_tvars(T,[]); +fun term_tfrees t = add_term_tfrees(t,[]); +fun term_tvars t = add_term_tvars(t,[]); + +(** Frees and Vars **) + +(*a partial ordering (not reflexive) for atomic terms*) +fun atless (Const (a,_), Const (b,_)) = a insert_aterm(t,vars) + | Abs (_,_,body) => add_term_vars(body,vars) + | f$t => add_term_vars (f, add_term_vars(t, vars)) + | _ => vars; + +fun term_vars t = add_term_vars(t,[]); + +(*Accumulates the Frees in the term, suppressing duplicates*) +fun add_term_frees (t, frees: term list) = case t of + Free _ => insert_aterm(t,frees) + | Abs (_,_,body) => add_term_frees(body,frees) + | f$t => add_term_frees (f, add_term_frees(t, frees)) + | _ => frees; + +fun term_frees t = add_term_frees(t,[]); + +(*Given an abstraction over P, replaces the bound variable by a Free variable + having a unique name. *) +fun variant_abs (a,T,P) = + let val b = variant (add_term_names(P,[])) a + in (b, subst_bounds ([Free(b,T)], P)) end; + +(* renames and reverses the strings in vars away from names *) +fun rename_aTs names vars : (string*typ)list = + let fun rename_aT (vars,(a,T)) = + (variant (map #1 vars @ names) a, T) :: vars + in foldl rename_aT ([],vars) end; + +fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));