(* Title: Pure/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. *) infix 9 $; infixr 5 -->; infixr --->; infix aconv; signature BASIC_TERM = sig type indexname type class type sort type arity datatype typ = Type of string * typ list | TFree of string * sort | TVar of indexname * sort datatype term = Const of string * typ | Free of string * typ | Var of indexname * typ | Bound of int | Abs of string * typ * term | $ of term * term exception TYPE of string * typ list * term list exception TERM of string * term list val dummyT: typ val no_dummyT: typ -> typ val --> : typ * typ -> typ val ---> : typ list * typ -> typ val dest_Type: typ -> string * typ list val dest_TVar: typ -> indexname * sort val dest_TFree: typ -> string * sort val is_Bound: term -> bool val is_Const: term -> bool val is_Free: term -> bool val is_Var: term -> bool val is_TVar: typ -> bool val is_funtype: typ -> bool val dest_Const: term -> string * typ val dest_Free: term -> string * typ val dest_Var: term -> indexname * typ val domain_type: typ -> typ val range_type: typ -> typ val binder_types: typ -> typ list val body_type: typ -> typ val strip_type: typ -> typ list * typ val type_of1: typ list * term -> typ val type_of: term -> typ val fastype_of1: typ list * term -> typ val fastype_of: term -> typ val list_abs: (string * typ) list * term -> term val strip_abs_body: term -> term val strip_abs_vars: term -> (string * typ) list val strip_qnt_body: string -> term -> term val strip_qnt_vars: string -> term -> (string * typ) list val list_comb: term * term list -> term val strip_comb: term -> term * term list val head_of: term -> term val size_of_term: term -> int val map_atyps: (typ -> typ) -> typ -> typ val map_aterms: (term -> term) -> term -> term val map_type_tvar: (indexname * sort -> typ) -> typ -> typ val map_type_tfree: (string * sort -> typ) -> typ -> typ val map_term_types: (typ -> typ) -> term -> term val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a val add_term_names: term * string list -> string list val add_term_varnames: term -> indexname list -> indexname list val term_varnames: term -> indexname list val find_free: term -> string -> term option val aconv: term * term -> bool val aconvs: term list * term list -> bool structure Vartab: TABLE structure Typtab: TABLE structure Termtab: TABLE val itselfT: typ -> typ val a_itselfT: typ val propT: typ val implies: term val all: typ -> term val equals: typ -> term val strip_all_body: term -> term val strip_all_vars: term -> (string * typ) list val incr_bv: int * int * term -> term val incr_boundvars: int -> term -> term val add_loose_bnos: term * int * int list -> int list val loose_bnos: term -> int list val loose_bvar: term * int -> bool val loose_bvar1: term * int -> bool val subst_bounds: term list * term -> term val subst_bound: term * term -> term val betapply: term * term -> term val betapplys: term * term list -> term val eq_ix: indexname * indexname -> bool val ins_ix: indexname * indexname list -> indexname list val mem_ix: indexname * indexname list -> bool val mem_term: term * term list -> bool val ins_term: term * term list -> term list val could_unify: term * term -> bool val subst_free: (term * term) list -> term -> term val xless: (string * int) * indexname -> bool val abstract_over: term * term -> term val lambda: term -> term -> term val absfree: string * typ * term -> term val absdummy: typ * term -> term val list_abs_free: (string * typ) list * term -> term val list_all_free: (string * typ) list * term -> term val list_all: (string * typ) list * term -> term val subst_atomic: (term * term) list -> term -> term val typ_subst_atomic: (typ * typ) list -> typ -> typ val subst_atomic_types: (typ * typ) list -> term -> term val typ_subst_TVars: (indexname * typ) list -> typ -> typ val subst_TVars: (indexname * typ) list -> term -> term val subst_Vars: (indexname * term) list -> term -> term val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term val is_first_order: string list -> term -> bool val maxidx_of_typ: typ -> int val maxidx_of_typs: typ list -> int val maxidx_of_term: term -> int val variant: string list -> string -> string val variantlist: string list * string list -> string list (*note reversed order of args wrt. variant!*) val add_typ_classes: typ * class list -> class list val add_typ_tycons: typ * string list -> string list val add_term_classes: term * class list -> class list val add_term_tycons: term * string list -> string list val add_term_consts: term * string list -> string list val term_consts: term -> string list val exists_subterm: (term -> bool) -> term -> bool val exists_Const: (string * typ -> bool) -> term -> bool val add_term_free_names: term * string list -> string list val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list val add_typ_tfree_names: typ * string list -> string list val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list val add_typ_varnames: typ * string list -> string list val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list val add_term_tfrees: term * (string * sort) list -> (string * sort) list val add_term_tfree_names: term * string list -> string list val add_term_tvarnames: term * string list -> string list val typ_tfrees: typ -> (string * sort) list val typ_tvars: typ -> (indexname * sort) list val term_tfrees: term -> (string * sort) list val term_tvars: term -> (indexname * sort) list val add_typ_ixns: indexname list * typ -> indexname list val add_term_tvar_ixns: term * indexname list -> indexname list val add_term_vars: term * term list -> term list val term_vars: term -> term list val add_term_frees: term * term list -> term list val term_frees: term -> term list val variant_abs: string * typ * term -> string * term val rename_wrt_term: term -> (string * typ) list -> (string * typ) list val show_question_marks: bool ref end; signature TERM = sig include BASIC_TERM val argument_type_of: term -> typ val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list val add_vars: term -> (indexname * typ) list -> (indexname * typ) list val add_tfreesT: typ -> (string * sort) list -> (string * sort) list val add_tfrees: term -> (string * sort) list -> (string * sort) list val add_frees: term -> (string * typ) list -> (string * typ) list val fast_indexname_ord: indexname * indexname -> order val indexname_ord: indexname * indexname -> order val sort_ord: sort * sort -> order val typ_ord: typ * typ -> order val fast_term_ord: term * term -> order val term_ord: term * term -> order val hd_ord: term * term -> order val termless: term * term -> bool val term_lpo: (string -> int) -> term * term -> order val match_bvars: (term * term) * (string * string) list -> (string * string) list val rename_abs: term -> term -> term -> term option val eq_tvar: (indexname * sort) * (indexname * sort) -> bool val eq_var: (indexname * typ) * (indexname * typ) -> bool val tvar_ord: (indexname * sort) * (indexname * sort) -> order val var_ord: (indexname * typ) * (indexname * typ) -> order val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term val instantiateT: ((indexname * sort) * typ) list -> typ -> typ val maxidx_typ: typ -> int -> int val maxidx_typs: typ list -> int -> int val maxidx_term: term -> int -> int val invent_names: string list -> string -> int -> string list val map_typ: (string -> string) -> (string -> string) -> typ -> typ val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term val dest_abs: string * typ * term -> string * term val bound: int -> string val is_bound: string -> bool val zero_var_indexesT: typ -> typ val zero_var_indexes: term -> term val zero_var_indexes_inst: term -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list val dummy_patternN: string val dummy_pattern: typ -> term val no_dummy_patterns: term -> term val replace_dummy_patterns: int * term -> int * term val is_replaced_dummy_pattern: indexname -> bool val show_dummy_patterns: term -> term val adhoc_freeze_vars: term -> term * string list val string_of_vname: indexname -> string val string_of_vname': indexname -> string val str_of_term: term -> string end; structure Term: TERM = struct (*Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.*) type indexname = string * int; (* Types are classified by sorts. *) type class = string; type sort = class list; type arity = string * sort list * sort; (* 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; (*Terms. Bound variables are indicated by depth number. Free variables, (scheme) variables and constants have names. An term is "closed" if 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. *) 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; (*Errors involving type mismatches*) exception TYPE of string * typ list * term list; (*Errors 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 *) (** Types **) (*dummy type for parsing and printing etc.*) val dummyT = Type ("dummy", []); fun no_dummyT typ = let fun check (T as Type ("dummy", _)) = raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) | check (Type (_, Ts)) = List.app check Ts | check _ = (); in check typ; typ end; fun S --> T = Type("fun",[S,T]); (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*) val op ---> = Library.foldr (op -->); fun dest_Type (Type x) = x | dest_Type T = raise TYPE ("dest_Type", [T], []); fun dest_TVar (TVar x) = x | dest_TVar T = raise TYPE ("dest_TVar", [T], []); fun dest_TFree (TFree x) = x | dest_TFree T = raise TYPE ("dest_TFree", [T], []); (** Discriminators **) fun is_Bound (Bound _) = true | is_Bound _ = false; 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; (*Differs from proofterm/is_fun in its treatment of TVar*) fun is_funtype (Type("fun",[_,_])) = true | is_funtype _ = 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]); fun domain_type (Type("fun", [T,_])) = T and range_type (Type("fun", [_,T])) = 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) = (List.nth (Ts,i) handle Subscript => 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: function type is expected in application", [T,U], [f$u]) end; fun type_of t : typ = type_of1 ([],t); (*Determines the type of a term, with minimal checking*) fun fastype_of1 (Ts, f$u) = (case fastype_of1 (Ts,f) of Type("fun",[_,T]) => T | _ => raise TERM("fastype_of: expected function type", [f$u])) | fastype_of1 (_, Const (_,T)) = T | fastype_of1 (_, Free (_,T)) = T | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i) handle Subscript => raise TERM("fastype_of: Bound", [Bound i])) | fastype_of1 (_, Var (_,T)) = T | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u); fun fastype_of t : typ = fastype_of1 ([],t); (*Determine the argument type of a function*) fun argument_type_of tm = let fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U | argT _ T = raise TYPE ("argument_type_of", [T], []); fun arg 0 _ (Abs (_, T, _)) = T | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t | arg i Ts (t $ _) = arg (i + 1) Ts t | arg i Ts a = argT i (fastype_of1 (Ts, a)); in arg 0 [] tm end; val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t)); (* 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 = Library.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 tm = let fun add_size (t $ u, n) = add_size (t, add_size (u, n)) | add_size (Abs (_ ,_, t), n) = add_size (t, n + 1) | add_size (_, n) = n + 1; in add_size (tm, 0) end; fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) | map_atyps f T = T; fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t) | map_aterms f t = f t; fun map_type_tvar f = let fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) | map_aux (TVar x) = f x | map_aux T = T; in map_aux end; fun map_type_tfree f = let fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) | map_aux (TFree x) = f x | map_aux T = T; in map_aux end; fun map_term_types f = let fun map_aux (Const (a, T)) = Const (a, f T) | map_aux (Free (a, T)) = Free (a, f T) | map_aux (Var (v, T)) = Var (v, f T) | map_aux (t as Bound _) = t | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t) | map_aux (t $ u) = map_aux t $ map_aux u; in map_aux 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 (* fold types and terms *) (*fold atoms of type*) fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts | fold_atyps f T = f T; (*fold atoms of term*) fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u | fold_aterms f (Abs (_, _, t)) = fold_aterms f t | fold_aterms f a = f a; (*fold types of term*) fun fold_term_types f (t as Const (_, T)) = f t T | fold_term_types f (t as Free (_, T)) = f t T | fold_term_types f (t as Var (_, T)) = f t T | fold_term_types f (Bound _) = I | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u; fun fold_types f = fold_term_types (K f); (*collect variables*) val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I); val add_tvars = fold_types add_tvarsT; val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I); val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I); val add_tfrees = fold_types add_tfreesT; val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); (*collect variable names*) val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I); fun term_varnames t = add_term_varnames t []; fun find_free t x = let exception Found of term; fun find (t as Free (x', _)) = if x = x' then raise Found t else I | find _ = I; in (fold_aterms find t (); NONE) handle Found v => SOME v end; (** Comparing terms, types, sorts etc. **) (* fast syntactic comparison *) fun fast_indexname_ord ((x, i), (y, j)) = (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord); fun sort_ord SS = if pointer_eq SS then EQUAL else dict_ord fast_string_ord SS; local fun cons_nr (TVar _) = 0 | cons_nr (TFree _) = 1 | cons_nr (Type _) = 2; in fun typ_ord TU = if pointer_eq TU then EQUAL else (case TU of (Type (a, Ts), Type (b, Us)) => (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord) | (TFree (a, S), TFree (b, S')) => (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord) | (TVar (xi, S), TVar (yj, S')) => (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord) | (T, U) => int_ord (cons_nr T, cons_nr U)); end; local fun cons_nr (Const _) = 0 | cons_nr (Free _) = 1 | cons_nr (Var _) = 2 | cons_nr (Bound _) = 3 | cons_nr (Abs _) = 4 | cons_nr (_ $ _) = 5; fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) | struct_ord (t1 $ t2, u1 $ u2) = (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) | atoms_ord (t1 $ t2, u1 $ u2) = (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) | atoms_ord (Bound i, Bound j) = int_ord (i, j) | atoms_ord _ = sys_error "atoms_ord"; fun types_ord (Abs (_, T, t), Abs (_, U, u)) = (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) | types_ord (t1 $ t2, u1 $ u2) = (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) | types_ord (Bound _, Bound _) = EQUAL | types_ord _ = sys_error "types_ord"; in fun fast_term_ord tu = if pointer_eq tu then EQUAL else (case struct_ord tu of EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord) | ord => ord); fun op aconv tu = (fast_term_ord tu = EQUAL); fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL); structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord); structure Typtab = TableFun(type key = typ val ord = typ_ord); structure Termtab = TableFun(type key = term val ord = fast_term_ord); end; (* term_ord *) (*a linear well-founded AC-compatible ordering for terms: s < t <=> 1. size(s) < size(t) or 2. size(s) = size(t) and s=f(...) and t=g(...) and f string_ord (x, y) | ord => ord); local fun hd_depth (t $ _, n) = hd_depth (t, n + 1) | hd_depth p = p; fun dest_hd (Const (a, T)) = (((a, 0), T), 0) | dest_hd (Free (a, T)) = (((a, 0), T), 1) | dest_hd (Var v) = (v, 2) | dest_hd (Bound i) = ((("", i), dummyT), 3) | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4); in fun term_ord tu = if pointer_eq tu then EQUAL else (case tu of (Abs (_, T, t), Abs(_, U, u)) => (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (t, u) => (case int_ord (size_of_term t, size_of_term u) of EQUAL => (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of EQUAL => args_ord (t, u) | ord => ord) | ord => ord)) and hd_ord (f, g) = prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) and args_ord (f $ t, g $ u) = (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord) | args_ord _ = EQUAL; fun termless tu = (term_ord tu = LESS); end; (** Lexicographic path order on terms **) (* See Baader & Nipkow, Term rewriting, CUP 1998. Without variables. Const, Var, Bound, Free and Abs are treated all as constants. f_ord maps strings to integers and serves two purposes: - Predicate on constant symbols. Those that are not recognised by f_ord must be mapped to ~1. - Order on the recognised symbols. These must be mapped to distinct integers >= 0. *) local fun dest_hd f_ord (Const (a, T)) = let val ord = f_ord a in if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) end | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0) | dest_hd _ (Var v) = ((1, v), 1) | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2) | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3); fun term_lpo f_ord (s, t) = let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in if forall (fn si => term_lpo f_ord (si, t) = LESS) ss then case hd_ord f_ord (f, g) of GREATER => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then GREATER else LESS | EQUAL => if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts then list_ord (term_lpo f_ord) (ss, ts) else LESS | LESS => LESS else GREATER end and hd_ord f_ord (f, g) = case (f, g) of (Abs (_, T, t), Abs (_, U, u)) => (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) | (_, _) => prod_ord (prod_ord int_ord (prod_ord indexname_ord typ_ord)) int_ord (dest_hd f_ord f, dest_hd f_ord g) in val term_lpo = term_lpo end; (** Connectives of higher order logic **) fun itselfT ty = Type ("itself", [ty]); val a_itselfT = itselfT (TFree ("'a", [])); 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); (* 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); (*Scan a pair of terms; while they are similar, accumulate corresponding bound vars in "al"*) fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s, t, if x="" orelse y="" then al else (x,y)::al) | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) | match_bvs(_,_,al) = al; (* strip abstractions created by parameters *) fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); fun rename_abs pat obj t = let val ren = match_bvs (pat, obj, []); fun ren_abs (Abs (x, T, b)) = Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b) | ren_abs (f $ t) = ren_abs f $ ren_abs t | ren_abs t = t in if null ren then NONE else SOME (ren_abs t) end; (*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; fun loose_bvar1(Bound i,k) = i = k | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1) | loose_bvar1 _ = 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*)) | 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; (*Special case: one argument*) fun subst_bound (arg, t) : term = let fun subst (t as Bound i, lev) = if i 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 AList.lookup (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, abs (lev + 1) t) | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u) | _ => raise SAME); in abs 0 body handle SAME => body end; fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t)) | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) | lambda (v as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t)) | lambda v t = raise TERM ("lambda", [v, t]); (*Form an abstraction over a free variable.*) fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body)); fun absdummy (T, body) = Abs ("uu", 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; inst = [(t1,u1), ..., (tn,un)]. A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) fun subst_atomic [] tm = tm | subst_atomic inst tm = let fun subst (Abs (a, T, body)) = Abs (a, T, subst body) | subst (t $ u) = subst t $ subst u | subst t = if_none (AList.lookup (op aconv) inst t) t; in subst tm end; (*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*) fun typ_subst_atomic [] ty = ty | typ_subst_atomic inst ty = let fun subst (Type (a, Ts)) = Type (a, map subst Ts) | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T; in subst ty end; fun subst_atomic_types [] tm = tm | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; fun typ_subst_TVars [] ty = ty | typ_subst_TVars inst ty = let fun subst (Type (a, Ts)) = Type (a, map subst Ts) | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T | subst T = T; in subst ty end; fun subst_TVars [] tm = tm | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; (*see also Envir.norm_term*) fun subst_Vars [] tm = tm | subst_Vars inst tm = let fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t | subst (Abs (a, T, t)) = Abs (a, T, subst t) | subst (t $ u) = subst t $ subst u | subst t = t; in subst tm end; (*see also Envir.norm_term*) fun subst_vars ([], []) tm = tm | subst_vars ([], inst) tm = subst_Vars inst tm | subst_vars (instT, inst) tm = let fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) | subst (t as Var (xi, T)) = (case AList.lookup (op =) inst xi of NONE => Var (xi, typ_subst_TVars instT T) | SOME t => t) | subst (t as Bound _) = t | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t) | subst (t $ u) = subst t $ subst u; in subst tm end; (* instantiation of schematic variables (types before terms) *) local exception SAME in fun instantiateT_same [] _ = raise SAME | instantiateT_same instT ty = let fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) | subst_typ (TVar v) = (case AList.lookup eq_tvar instT v of SOME T => T | NONE => raise SAME) | subst_typ _ = raise SAME and subst_typs (T :: Ts) = (subst_typ T :: (subst_typs Ts handle SAME => Ts) handle SAME => T :: subst_typs Ts) | subst_typs [] = raise SAME; in subst_typ ty end; fun instantiate ([], []) tm = tm | instantiate (instT, inst) tm = let val substT = instantiateT_same instT; fun subst (Const (c, T)) = Const (c, substT T) | subst (Free (x, T)) = Free (x, substT T) | subst (Var (xi, T)) = let val (T', same) = (substT T, false) handle SAME => (T, true) in (case AList.lookup eq_var inst (xi, T') of SOME t => t | NONE => if same then raise SAME else Var (xi, T')) end | subst (Bound _) = raise SAME | subst (Abs (x, T, t)) = (Abs (x, substT T, subst t handle SAME => t) handle SAME => Abs (x, T, subst t)) | subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u); in subst tm handle SAME => tm end; fun instantiateT instT ty = instantiateT_same instT ty handle SAME => ty; end; (** Identifying first-order terms **) (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); (*First order means in all terms of the form f(t1,...,tn) no argument has a function type. The supplied quantifiers are excluded: their argument always has a function type through a recursive call into its body.*) fun is_first_order quants = let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = q mem_string quants andalso (*it is a known quantifier*) not (is_funtype T) andalso first_order1 (T::Ts) body | first_order1 Ts t = case strip_comb t of (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts | (Abs _, ts) => false (*not in beta-normal form*) | _ => error "first_order: unexpected case" in first_order1 [] end; (* maximum index of typs and terms *) fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j) | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i | maxidx_typ (TFree _) i = i and maxidx_typs [] i = i | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i); fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j)) | maxidx_term (Const (_, T)) i = maxidx_typ T i | maxidx_term (Free (_, T)) i = maxidx_typ T i | maxidx_term (Bound _) i = i | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i) | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i); fun maxidx_of_typ T = maxidx_typ T ~1; fun maxidx_of_typs Ts = maxidx_typs Ts ~1; fun maxidx_of_term t = maxidx_term t ~1; (**** Syntax-related declarations ****) (*** Printing ***) (*Makes a variant of a name distinct from the names in 'used'. First attaches the suffix and then increments this; preserves a suffix of underscores "_". *) fun variant used name = let val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c; fun vary1 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_init c) else c; in vary1 (if c = "" then "u" else c) ^ u 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; (*Invent fresh names*) fun invent_names _ _ 0 = [] | invent_names used a n = let val b = Symbol.bump_string a in if a mem_string used then invent_names used b n else a :: invent_names used b (n - 1) end; (** Consts etc. **) fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts | add_typ_classes (TFree (_, S), cs) = S union cs | add_typ_classes (TVar (_, S), cs) = S union cs; fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts | add_typ_tycons (_, cs) = cs; val add_term_classes = it_term_types add_typ_classes; val add_term_tycons = it_term_types add_typ_tycons; fun add_term_consts (Const (c, _), cs) = c ins_string cs | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs)) | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs) | add_term_consts (_, cs) = cs; fun term_consts t = add_term_consts(t,[]); fun exists_subterm P = let fun ex tm = P tm orelse (case tm of t $ u => ex t orelse ex u | Abs (_, _, t) => ex t | _ => false); in ex end; fun exists_Const P = exists_subterm (fn Const c => P c | _ => false); (*map classes, tycons*) fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) | map_typ f _ (TFree (x, S)) = TFree (x, map f S) | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); (*map classes, tycons, consts*) fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) | map_term _ _ _ (t as Bound _) = t | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; (** TFrees and TVars **) (*Accumulates the names of Frees in the term, suppressing duplicates.*) fun add_term_free_names (Free(a,_), bs) = a ins_string bs | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs)) | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs) | add_term_free_names (_, bs) = 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) = NameSpace.base a ins_string bs | add_term_names (Free(a,_), bs) = a ins_string 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 vs Ts | add_typ_tvars(TFree(_),vs) = vs | add_typ_tvars(TVar(v),vs) = insert (op =) v vs; (*Accumulates the TFrees in a type, suppressing duplicates. *) fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs | add_typ_tfree_names(TVar(_),fs) = fs; fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs | add_typ_tfrees(TVar(_),fs) = fs; fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms; (*Accumulates the TVars in a term, suppressing duplicates. *) val add_term_tvars = 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; val add_term_tvarnames = it_term_types add_typ_varnames; (*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,[]); (*special code to enforce left-to-right collection of TVar-indexnames*) fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) | add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns else ixns@[ixn] | add_typ_ixns(ixns,TFree(_)) = ixns; fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T) | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T) | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T) | add_term_tvar_ixns(Bound _,ixns) = ixns | add_term_tvar_ixns(Abs(_,T,t),ixns) = add_term_tvar_ixns(t,add_typ_ixns(ixns,T)) | add_term_tvar_ixns(f$t,ixns) = add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns)); (** Frees and Vars **) (*Accumulates the Vars in the term, suppressing duplicates*) fun add_term_vars (t, vars: term list) = case t of Var _ => OrdList.insert term_ord 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 _ => OrdList.insert term_ord 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 -- SLOW!*) fun variant_abs (a,T,P) = let val b = variant (add_term_names(P,[])) a in (b, subst_bound (Free(b,T), P)) end; fun dest_abs (x, T, body) = let fun name_clash (Free (y, _)) = (x = y) | name_clash (t $ u) = name_clash t orelse name_clash u | name_clash (Abs (_, _, t)) = name_clash t | name_clash _ = false; in if name_clash body then dest_abs (variant [x] x, T, body) (*potentially slow, but rarely happens*) else (x, subst_bound (Free (x, T), body)) end; (*names for numbered variables -- preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*) local val small_int = Vector.tabulate (1000, fn i => let val leading = if i < 10 then "00" else if i < 100 then "0" else "" in ":" ^ leading ^ string_of_int i end); in fun bound n = if n < 1000 then Vector.sub (small_int, n) else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000); end; val is_bound = String.isPrefix ":"; (* 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 Library.foldl rename_aT ([],vars) end; fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); (* zero var indexes *) fun zero_var_inst vars = fold (fn v as ((x, i), X) => fn (used, inst) => let val x' = variant used (if is_bound x then "u" else x); val used' = x' :: used; in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end) vars ([], []) |> #2; fun zero_var_indexesT ty = instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty; fun zero_var_indexes_inst tm = let val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm []))); val inst = add_vars tm [] |> map (apsnd (instantiateT instT)) |> sort var_ord |> zero_var_inst |> map (apsnd Var); in (instT, inst) end; fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm; (* dummy patterns *) val dummy_patternN = "dummy_pattern"; fun dummy_pattern T = Const (dummy_patternN, T); fun is_dummy_pattern (Const ("dummy_pattern", _)) = true | is_dummy_pattern _ = false; fun no_dummy_patterns tm = if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); fun replace_dummy Ts (i, Const ("dummy_pattern", T)) = (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1))) | replace_dummy Ts (i, Abs (x, T, t)) = let val (i', t') = replace_dummy (T :: Ts) (i, t) in (i', Abs (x, T, t')) end | replace_dummy Ts (i, t $ u) = let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u) in (i'', t' $ u') end | replace_dummy _ (i, a) = (i, a); val replace_dummy_patterns = replace_dummy []; fun is_replaced_dummy_pattern ("_dummy_", _) = true | is_replaced_dummy_pattern _ = false; fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T) | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t) | show_dummy_patterns a = a; (* adhoc freezing *) fun adhoc_freeze_vars tm = let fun mk_inst (var as Var ((a, i), T)) = let val x = a ^ Library.gensym "_" ^ string_of_int i in ((var, Free(x, T)), x) end; val (insts, xs) = split_list (map mk_inst (term_vars tm)); in (subst_atomic insts tm, xs) end; (* string_of_vname *) val show_question_marks = ref true; fun string_of_vname (x, i) = let val question_mark = if ! show_question_marks then "?" else ""; val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of _ :: "\\<^isub>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true); in if dot then question_mark ^ x ^ "." ^ idx else if i <> 0 then question_mark ^ x ^ idx else question_mark ^ x end; fun string_of_vname' (x, ~1) = x | string_of_vname' xi = string_of_vname xi; (* str_of_term *) fun str_of_term (Const (c, _)) = c | str_of_term (Free (x, _)) = x | str_of_term (Var (xi, _)) = string_of_vname xi | str_of_term (Bound i) = string_of_int i | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")"; end; structure BasicTerm: BASIC_TERM = Term; open BasicTerm;