diff --git a/src/Pure/term.ML b/src/Pure/term.ML --- a/src/Pure/term.ML +++ b/src/Pure/term.ML @@ -1,1050 +1,1051 @@ (* Title: Pure/term.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Makarius Simply typed lambda-calculus: types, terms, and basic operations. *) infix 9 $; infixr 5 -->; infixr --->; infix aconv; signature BASIC_TERM = sig type indexname = string * int type class = string type sort = class list type arity = string * sort list * sort 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 dummyS: sort val dummyT: typ val no_dummyT: typ -> typ val --> : typ * typ -> typ val ---> : typ list * typ -> typ val is_Type: typ -> bool val is_TFree: typ -> bool val is_TVar: typ -> bool val dest_Type: typ -> string * typ list val dest_TFree: typ -> string * sort val dest_TVar: typ -> indexname * sort val is_Bound: term -> bool val is_Const: term -> bool val is_Free: term -> bool val is_Var: term -> bool val dest_Const: term -> string * typ val dest_Free: term -> string * typ val dest_Var: term -> indexname * typ val dest_comb: term -> term * term val domain_type: typ -> typ val range_type: typ -> typ val dest_funT: typ -> 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 strip_abs: term -> (string * typ) list * 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 size_of_typ: typ -> 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_types: (typ -> typ) -> term -> term val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val fold_atyps_sorts: (typ * sort -> '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 burrow_types: (typ list -> typ list) -> term list -> term list val aconv: term * term -> bool val propT: typ 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 subst_free: (term * term) list -> term -> term val abstract_over: term * term -> term val lambda: term -> term -> term val absfree: string * typ -> term -> term val absdummy: typ -> 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 fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a val exists_subtype: (typ -> bool) -> typ -> bool val exists_type: (typ -> bool) -> term -> bool val exists_subterm: (term -> bool) -> term -> bool val exists_Const: (string * typ -> bool) -> term -> bool end; signature TERM = sig include BASIC_TERM val aT: sort -> typ val itselfT: typ -> typ val a_itselfT: typ val argument_type_of: term -> int -> typ val abs: string * typ -> term -> term val add_tvar_namesT: typ -> indexname list -> indexname list val add_tvar_names: term -> indexname list -> indexname list val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list val add_var_names: term -> indexname list -> indexname list val add_vars: term -> (indexname * typ) list -> (indexname * typ) list val add_tfree_namesT: typ -> string list -> string list val add_tfree_names: term -> string list -> string list val add_tfreesT: typ -> (string * sort) list -> (string * sort) list val add_tfrees: term -> (string * sort) list -> (string * sort) list val add_free_names: term -> string list -> string list val add_frees: term -> (string * typ) list -> (string * typ) list val add_const_names: term -> string list -> string list val add_consts: term -> (string * typ) list -> (string * typ) list val hidden_polymorphism: term -> (indexname * sort) list val declare_typ_names: typ -> Name.context -> Name.context val declare_term_names: term -> Name.context -> Name.context val declare_term_frees: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list val eq_ix: indexname * indexname -> bool val eq_tvar: (indexname * sort) * (indexname * sort) -> bool val eq_var: (indexname * typ) * (indexname * typ) -> bool val aconv_untyped: term * term -> bool val could_unify: term * term -> bool val strip_abs_eta: int -> term -> (string * typ) list * term val match_bvars: (term * term) -> (string * string) list -> (string * string) list val map_abs_vars: (string -> string) -> term -> term val rename_abs: term -> term -> term -> term option val is_open: term -> bool val is_dependent: term -> bool val term_name: term -> string val dependent_lambda_name: string * term -> term -> term val lambda_name: string * term -> term -> term val close_schematic_term: term -> term val maxidx_typ: typ -> int -> int val maxidx_typs: typ list -> int -> int val maxidx_term: term -> int -> int val could_beta_contract: term -> bool val could_eta_contract: term -> bool val could_beta_eta_contract: term -> bool + val used_free: string -> term -> bool val dest_abs: string * typ * term -> string * term val dummy_pattern: typ -> term val dummy: term val dummy_prop: term val is_dummy_pattern: term -> bool val free_dummy_patterns: term -> Name.context -> term * Name.context val no_dummy_patterns: term -> term val replace_dummy_patterns: term -> int -> term * int val show_dummy_patterns: term -> term val string_of_vname: indexname -> string val string_of_vname': indexname -> 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 **) (*dummies for type-inference etc.*) val dummyS = [""]; 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 -->); (** Discriminators **) fun is_Type (Type _) = true | is_Type _ = false; fun is_TFree (TFree _) = true | is_TFree _ = false; fun is_TVar (TVar _) = true | is_TVar _ = false; (** Destructors **) fun dest_Type (Type x) = x | dest_Type T = raise TYPE ("dest_Type", [T], []); fun dest_TFree (TFree x) = x | dest_TFree T = raise TYPE ("dest_TFree", [T], []); fun dest_TVar (TVar x) = x | dest_TVar T = raise TYPE ("dest_TVar", [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; (** 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 dest_comb (t1 $ t2) = (t1, t2) | dest_comb t = raise TERM("dest_comb", [t]); fun domain_type (Type ("fun", [T, _])) = T; fun range_type (Type ("fun", [_, U])) = U; fun dest_funT (Type ("fun", [T, U])) = (T, U) | dest_funT T = raise TYPE ("dest_funT", [T], []); (*maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*) fun binder_types (Type ("fun", [T, U])) = T :: binder_types U | binder_types _ = []; (*maps [T1,...,Tn]--->T to T*) fun body_type (Type ("fun", [_, U])) = body_type U | body_type T = T; (*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*) fun strip_type T = (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 Ts i handle General.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); (*Determine the type of a term, with minimal checking*) local fun fastype_of_term Ts (Abs (_, T, t)) = T --> fastype_of_term (T :: Ts) t | fastype_of_term Ts (t $ _) = range_type_of Ts t | fastype_of_term Ts a = fastype_of_atom Ts a and fastype_of_atom _ (Const (_, T)) = T | fastype_of_atom _ (Free (_, T)) = T | fastype_of_atom _ (Var (_, T)) = T | fastype_of_atom Ts (Bound i) = fastype_of_bound Ts i and fastype_of_bound (T :: Ts) i = if i = 0 then T else fastype_of_bound Ts (i - 1) | fastype_of_bound [] i = raise TERM ("fastype_of: Bound", [Bound i]) and range_type_of Ts (Abs (_, T, u)) = fastype_of_term (T :: Ts) u | range_type_of Ts (t $ u) = range_type_ofT (t $ u) (range_type_of Ts t) | range_type_of Ts a = range_type_ofT a (fastype_of_atom Ts a) and range_type_ofT _ (Type ("fun", [_, T])) = T | range_type_ofT t _ = raise TERM ("fastype_of: expected function type", [t]); in val fastype_of1 = uncurry fastype_of_term; val fastype_of = fastype_of_term []; end; (*Determine the argument type of a function*) fun argument_type_of tm k = 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 k [] tm end; fun abs (x, T) t = Abs (x, T, t); fun strip_abs (Abs (a, T, t)) = let val (a', t') = strip_abs t in ((a, T) :: a', t') end | strip_abs 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; (*number of atoms and constructors in a type*) fun size_of_typ ty = let fun add_size (Type (_, tys)) n = fold add_size tys (n + 1) | add_size _ n = n + 1; in add_size ty 0 end; fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) | map_atyps f T = f 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 = map_atyps (fn TVar x => f x | T => T); fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T); fun map_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 (Bound i) = Bound i | 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; (* fold types and terms *) fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts | fold_atyps f T = f T; fun fold_atyps_sorts f = fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S)); 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; 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); fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts) | replace_types (Bound i) Ts = (Bound i, Ts) | replace_types (Abs (x, _, b)) (T :: Ts) = let val (b', Ts') = replace_types b Ts in (Abs (x, T, b'), Ts') end | replace_types (t $ u) Ts = let val (t', Ts') = replace_types t Ts; val (u', Ts'') = replace_types u Ts'; in (t' $ u', Ts'') end; fun burrow_types f ts = let val Ts = rev ((fold o fold_types) cons ts []); val Ts' = f Ts; val (ts', []) = fold_map replace_types ts Ts'; in ts' end; (*collect variables*) val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I); val add_tvar_names = fold_types add_tvar_namesT; val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I); val add_tvars = fold_types add_tvarsT; val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I); val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I); val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I); val add_tfree_names = fold_types add_tfree_namesT; val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I); val add_tfrees = fold_types add_tfreesT; val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I); val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I); val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I); (*extra type variables in a term, not covered by its type*) fun hidden_polymorphism t = let val T = fastype_of t; val tvarsT = add_tvarsT T []; val extra_tvars = fold_types (fold_atyps (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t []; in extra_tvars end; (* renaming variables *) val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); fun declare_term_names tm = fold_aterms (fn Const (a, _) => Name.declare (Long_Name.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> fold_types declare_typ_names tm; val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); fun variant_frees t frees = fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) (** Comparing terms **) (* variables *) fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; (* alpha equivalence *) fun tm1 aconv tm2 = pointer_eq (tm1, tm2) orelse (case (tm1, tm2) of (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2 | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2 | (a1, a2) => a1 = a2); fun aconv_untyped (tm1, tm2) = pointer_eq (tm1, tm2) orelse (case (tm1, tm2) of (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2) | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2) | (Const (a, _), Const (b, _)) => a = b | (Free (x, _), Free (y, _)) => x = y | (Var (xi, _), Var (yj, _)) => xi = yj | (Bound i, Bound j) => i = j | _ => 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; (** Connectives of higher order logic **) fun aT S = TFree (Name.aT, S); fun itselfT ty = Type ("itself", [ty]); val a_itselfT = itselfT (TFree (Name.aT, [])); val propT : typ = Type ("prop",[]); (*maps \x1...xn. t to t*) fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t | strip_all_body t = t; (*maps \x1...xn. t to [x1, ..., xn]*) fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t | strip_all_vars t = []; (*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 map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) | map_abs_vars f t = t; fun rename_abs pat obj t = let val ren = match_bvs (pat, obj, []); fun ren_abs (Abs (x, T, b)) = Abs (the_default x (AList.lookup (op =) ren 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; fun is_open t = loose_bvar (t, 0); fun is_dependent t = loose_bvar1 (t, 0); (*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 < lev then raise Same.SAME (*var is locally bound*) else incr_boundvars lev (nth args (i - lev)) handle General.Subscript => 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) handle Same.SAME => t) handle Same.SAME => f $ subst (t, lev)) | subst _ = raise Same.SAME; in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end; (*Special case: one argument*) fun subst_bound (arg, t) : term = let fun subst (Bound i, lev) = if i < lev then raise Same.SAME (*var is locally bound*) else if i = lev then incr_boundvars lev arg else Bound (i - 1) (*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) handle Same.SAME => t) handle Same.SAME => f $ subst (t, lev)) | subst _ = raise Same.SAME; in subst (t, 0) handle Same.SAME => t end; (*beta-reduce if possible, else form application*) fun betapply (Abs(_,_,t), u) = subst_bound (u,t) | betapply (f,u) = f$u; val betapplys = Library.foldl betapply; (*unfolding abstractions with substitution of bound variables and implicit eta-expansion*) fun strip_abs_eta k t = let val used = fold_aterms declare_term_frees t Name.context; fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let val (v', used') = Name.variant v used; val t' = subst_bound (Free (v', T), t); val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used'); in (((v', T) :: vs, t''), (k', used'')) end | strip_abs t (k, used) = (([], t), (k, used)); fun expand_eta [] t _ = ([], t) | expand_eta (T::Ts) t used = let val (v, used') = Name.variant "" used; val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; in ((v, T) :: vs, t') end; val ((vs1, t'), (k', used')) = strip_abs t (k, used); val Ts = fst (chop k' (binder_types (fastype_of t'))); val (vs2, t'') = expand_eta Ts t' used'; in (vs1 @ vs2, t'') end; (*Substitute new for free occurrences of old in a term*) fun subst_free [] = I | 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; (*Abstraction of the term "body" over its occurrences of v, which must contain no loose bound variables. The resulting term is ready to become the body of an Abs.*) fun abstract_over (v, body) = let fun abs lev tm = if v aconv tm then Bound lev else (case tm of Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) | t $ u => (abs lev t $ (abs lev u handle Same.SAME => u) handle Same.SAME => t $ abs lev u) | _ => raise Same.SAME); in abs 0 body handle Same.SAME => body end; fun term_name (Const (x, _)) = Long_Name.base_name x | term_name (Free (x, _)) = x | term_name (Var ((x, _), _)) = x | term_name _ = Name.uu; fun dependent_lambda_name (x, v) t = let val t' = abstract_over (v, t) in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end; fun lambda_name (x, v) t = Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t)); fun lambda v t = lambda_name ("", v) t; fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body)); fun absdummy T body = Abs (Name.uu_, T, body); (*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 = the_default t (AList.lookup (op aconv) inst 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 = the_default T (AList.lookup (op = : typ * typ -> bool) inst T); in subst ty end; fun subst_atomic_types [] tm = tm | subst_atomic_types inst tm = map_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, _)) = the_default T (AList.lookup (op =) inst xi) | subst T = T; in subst ty end; fun subst_TVars [] tm = tm | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; fun subst_Vars [] tm = tm | subst_Vars inst tm = let fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi) | subst (Abs (a, T, t)) = Abs (a, T, subst t) | subst (t $ u) = subst t $ subst u | subst t = t; in subst tm end; 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 (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; fun close_schematic_term t = let val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t); val extra_terms = map Var (add_vars t []); in fold lambda (extra_terms @ extra_types) t end; (** Identifying first-order terms **) (*Differs from proofterm/is_fun in its treatment of TVar*) fun is_funtype (Type ("fun", [_, _])) = true | is_funtype _ = false; (*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)) = member (op =) quants q 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; (** misc syntax operations **) (* substructure *) fun fold_subtypes f = let fun iter ty = (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty); in iter end; fun exists_subtype P = let fun ex ty = P ty orelse (case ty of Type (_, Ts) => exists ex Ts | _ => false); in ex end; fun exists_type P = let fun ex (Const (_, T)) = P T | ex (Free (_, T)) = P T | ex (Var (_, T)) = P T | ex (Bound _) = false | ex (Abs (_, T, t)) = P T orelse ex t | ex (t $ u) = ex t orelse ex u; in ex end; 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); (* contraction *) fun could_beta_contract (Abs _ $ _) = true | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u | could_beta_contract (Abs (_, _, b)) = could_beta_contract b | could_beta_contract _ = false; fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true | could_eta_contract (Abs (_, _, b)) = could_eta_contract b | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u | could_eta_contract _ = false; fun could_beta_eta_contract (Abs _ $ _) = true | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u | could_beta_eta_contract _ = false; (* dest abstraction *) fun used_free x = let fun used (Free (y, _)) = (x = y) | used (t $ u) = used t orelse used u | used (Abs (_, _, t)) = used t | used _ = false; in used end; fun dest_abs (x, T, b) = if used_free x b then let val (x', _) = Name.variant x (declare_term_frees b Name.context); in (x', subst_bound (Free (x', T), b)) end else (x, subst_bound (Free (x, T), b)); (* dummy patterns *) fun dummy_pattern T = Const ("Pure.dummy_pattern", T); val dummy = dummy_pattern dummyT; val dummy_prop = dummy_pattern propT; fun is_dummy_pattern (Const ("Pure.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 free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used = let val [x] = Name.invent used Name.uu 1 in (Free (Name.internal x, T), Name.declare x used) end | free_dummy_patterns (Abs (x, T, b)) used = let val (b', used') = free_dummy_patterns b used in (Abs (x, T, b'), used') end | free_dummy_patterns (t $ u) used = let val (t', used') = free_dummy_patterns t used; val (u', used'') = free_dummy_patterns u used'; in (t' $ u', used'') end | free_dummy_patterns a used = (a, used); fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i = (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1) | replace_dummy Ts (Abs (x, T, t)) i = let val (t', i') = replace_dummy (T :: Ts) t i in (Abs (x, T, t'), i') end | replace_dummy Ts (t $ u) i = let val (t', i') = replace_dummy Ts t i; val (u', i'') = replace_dummy Ts u i'; in (t' $ u', i'') end | replace_dummy _ a i = (a, i); val replace_dummy_patterns = replace_dummy []; fun show_dummy_patterns (Var (("_dummy_", _), T)) = 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; (* display variables *) fun string_of_vname (x, i) = let val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of _ :: "\<^sub>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true); in if dot then "?" ^ x ^ "." ^ idx else if i <> 0 then "?" ^ x ^ idx else "?" ^ x end; fun string_of_vname' (x, ~1) = x | string_of_vname' xi = string_of_vname xi; end; structure Basic_Term: BASIC_TERM = Term; open Basic_Term; diff --git a/src/Tools/Code/code_thingol.ML b/src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML +++ b/src/Tools/Code/code_thingol.ML @@ -1,1043 +1,1042 @@ (* Title: Tools/Code/code_thingol.ML Author: Florian Haftmann, TU Muenchen Intermediate language ("Thin-gol") representing executable code. Representation and translation. *) infix 8 `%%; infix 4 `$; infix 4 `$$; infixr 3 `->; infixr 3 `|=>; infixr 3 `|==>; signature BASIC_CODE_THINGOL = sig type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; val `-> : itype * itype -> itype; val `$$ : iterm * iterm list -> iterm; val `|==> : (vname option * itype) list * iterm -> iterm; type typscheme = (vname * sort) list * itype; end; signature CODE_THINGOL = sig include BASIC_CODE_THINGOL val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a val unfold_fun: itype -> itype list * itype val unfold_fun_n: int -> itype -> itype list * itype val unfold_app: iterm -> iterm * iterm list val unfold_abs: iterm -> (vname option * itype) list * iterm val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) list * iterm val split_pat_abs: iterm -> ((iterm * itype) * iterm) option val unfold_pat_abs: iterm -> (iterm * itype) list * iterm val unfold_const_app: iterm -> (const * iterm list) option val is_IVar: iterm -> bool val is_IAbs: iterm -> bool val eta_expand: int -> const * iterm list -> iterm val contains_dict_var: iterm -> bool val unambiguous_dictss: dict list list -> bool val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list val add_tyconames: iterm -> string list -> string list val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a datatype stmt = NoStmt | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option | Datatype of vname list * ((string * vname list (*type argument wrt. canonical order*)) * itype list) list | Datatypecons of string | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T val unimplemented: program -> string list val implemented_deps: program -> string list val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt val is_constr: program -> Code_Symbol.T -> bool val is_case: stmt -> bool val group_stmts: Proof.context -> program -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list val read_const_exprs: Proof.context -> string list -> string list val consts_program: Proof.context -> string list -> program val dynamic_conv: Proof.context -> (program -> typscheme * iterm -> Code_Symbol.T list -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> term -> 'a val static_conv_thingol: { ctxt: Proof.context, consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv) -> Proof.context -> conv val static_conv_isa: { ctxt: Proof.context, consts: string list } -> (program -> Proof.context -> term -> conv) -> Proof.context -> conv val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list } -> ({ program: program, deps: string list } -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> Proof.context -> term -> 'a end; structure Code_Thingol : CODE_THINGOL = struct open Basic_Code_Symbol; (** auxiliary **) fun unfoldl dest x = case dest x of NONE => (x, []) | SOME (x1, x2) => let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; fun unfoldr dest x = case dest x of NONE => ([], x) | SOME (x1, x2) => let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end; (** language core - types, terms **) type vname = string; datatype dict = Dict of (class * class) list * plain_dict and plain_dict = Dict_Const of (string * class) * dict list list | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }; datatype itype = `%% of string * itype list | ITyVar of vname; fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; val unfold_fun = unfoldr (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) | _ => NONE); fun unfold_fun_n n ty = let val (tys1, ty1) = unfold_fun ty; val (tys3, tys2) = chop n tys1; val ty3 = Library.foldr (op `->) (tys2, ty1); in (tys3, ty3) end; type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list, dom: itype list, annotation: itype option }; datatype iterm = IConst of const | IVar of vname option | `$ of iterm * iterm | `|=> of (vname option * itype) * iterm | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm }; (*see also signature*) fun is_IVar (IVar _) = true | is_IVar _ = false; fun is_IAbs (_ `|=> _) = true | is_IAbs _ = false; val op `$$ = Library.foldl (op `$); val op `|==> = Library.foldr (op `|=>); val unfold_app = unfoldl (fn op `$ t => SOME t | _ => NONE); val unfold_abs = unfoldr (fn op `|=> t => SOME t | _ => NONE); val split_let = (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body) | _ => NONE); val split_let_no_pat = (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body) | _ => NONE); val unfold_let = unfoldr split_let; val unfold_let_no_pat = unfoldr split_let_no_pat; fun unfold_const_app t = case unfold_app t of (IConst c, ts) => SOME (c, ts) | _ => NONE; fun fold_constexprs f = let fun fold' (IConst c) = f c | fold' (IVar _) = I | fold' (t1 `$ t2) = fold' t1 #> fold' t2 | fold' (_ `|=> t) = fold' t | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t #> fold (fn (p, body) => fold' p #> fold' body) clauses in fold' end; val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym); fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys | add_tycos (ITyVar _) = I; val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys); fun fold_varnames f = let fun fold_aux add_vars f = let fun fold_term _ (IConst _) = I | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v | fold_term _ (IVar NONE) = I | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2 | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t | fold_term vs ((NONE, _) `|=> t) = fold_term vs t | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_clause vs) clauses and fold_clause vs (p, t) = fold_term (add_vars p vs) t; in fold_term [] end fun add_vars t = fold_aux add_vars (insert (op =)) t; in fold_aux add_vars f end; fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t) | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } => if v = w andalso (exists_var p v orelse not (exists_var body v)) then ((p, ty), body) else ((IVar (SOME v), ty), t) | _ => ((IVar (SOME v), ty), t)) | split_pat_abs _ = NONE; val unfold_pat_abs = unfoldr split_pat_abs; fun unfold_abs_eta [] t = ([], t) | unfold_abs_eta (_ :: tys) (v_ty `|=> t) = let val (vs_tys, t') = unfold_abs_eta tys t; in (v_ty :: vs_tys, t') end | unfold_abs_eta tys t = let val ctxt = fold_varnames Name.declare t Name.context; val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; fun eta_expand k (const as { dom = tys, ... }, ts) = let val j = length ts; val l = k - j; val _ = if l > length tys then error "Impossible eta-expansion" else (); val vars = (fold o fold_varnames) Name.declare ts Name.context; val vs_tys = (map o apfst) SOME (Name.invent_names vars "a" ((take l o drop j) tys)); in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end; fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss | exists_plain_dict_var_pred f (Dict_Var x) = f x and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss; fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss | contains_dict_var (IVar _) = false | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2 | contains_dict_var (_ `|=> t) = contains_dict_var t | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t; val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique); (** statements, abstract programs **) type typscheme = (vname * sort) list * itype; datatype stmt = NoStmt | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option | Datatype of vname list * ((string * vname list) * itype list) list | Datatypecons of string | Class of vname * ((class * class) list * (string * itype) list) | Classrel of class * class | Classparam of class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * dict list list) list, inst_params: ((string * (const * int)) * (thm * bool)) list, superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Code_Symbol.Graph.T; fun unimplemented program = Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program []; fun implemented_deps program = Code_Symbol.Graph.keys program |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program))) |> map_filter (fn Constant c => SOME c | _ => NONE); fun map_terms_bottom_up f (t as IConst _) = f t | map_terms_bottom_up f (t as IVar _) = f t | map_terms_bottom_up f (t1 `$ t2) = f (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) | map_terms_bottom_up f ((v, ty) `|=> t) = f ((v, ty) `|=> map_terms_bottom_up f t) | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f (ICase { term = map_terms_bottom_up f t, typ = ty, clauses = (map o apply2) (map_terms_bottom_up f) clauses, primitive = map_terms_bottom_up f t0 }); fun map_classparam_instances_as_term f = (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const') fun map_terms_stmt f NoStmt = NoStmt | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst) (fn (ts, t) => (map f ts, f t)) eqs), case_cong) | map_terms_stmt f (stmt as Datatype _) = stmt | map_terms_stmt f (stmt as Datatypecons _) = stmt | map_terms_stmt f (stmt as Class _) = stmt | map_terms_stmt f (stmt as Classrel _) = stmt | map_terms_stmt f (stmt as Classparam _) = stmt | map_terms_stmt f (Classinst { class, tyco, vs, superinsts, inst_params, superinst_params }) = Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = map_classparam_instances_as_term f inst_params, superinst_params = map_classparam_instances_as_term f superinst_params }; fun is_constr program sym = case Code_Symbol.Graph.get_node program sym of Datatypecons _ => true | _ => false; fun is_case (Fun (_, SOME _)) = true | is_case _ = false; fun linear_stmts program = rev (Code_Symbol.Graph.strong_conn program) |> map (AList.make (Code_Symbol.Graph.get_node program)); fun group_stmts ctxt program = let fun is_fun (_, Fun _) = true | is_fun _ = false; fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; fun is_datatype (_, Datatype _) = true | is_datatype _ = false; fun is_class (_, Class _) = true | is_class _ = false; fun is_classrel (_, Classrel _) = true | is_classrel _ = false; fun is_classparam (_, Classparam _) = true | is_classparam _ = false; fun is_classinst (_, Classinst _) = true | is_classinst _ = false; fun group stmts = if forall (is_datatypecons orf is_datatype) stmts then (filter is_datatype stmts, [], ([], [])) else if forall (is_class orf is_classrel orf is_classparam) stmts then ([], filter is_class stmts, ([], [])) else if forall (is_fun orf is_classinst) stmts then ([], [], List.partition is_fun stmts) else error ("Illegal mutual dependencies: " ^ (commas o map (Code_Symbol.quote ctxt o fst)) stmts); in linear_stmts program |> map group end; (** translation kernel **) (* generic mechanisms *) fun ensure_stmt symbolize generate x (deps, program) = let val sym = symbolize x; val add_dep = case deps of [] => I | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym); in if can (Code_Symbol.Graph.get_node program) sym then program |> add_dep |> pair deps |> pair x else program |> Code_Symbol.Graph.default_node (sym, NoStmt) |> add_dep |> curry generate (sym :: deps) ||> snd |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt)) |> pair deps |> pair x end; exception PERMISSIVE of unit; fun translation_error ctxt permissive some_thm deps msg sub_msg = if permissive then raise PERMISSIVE () else let val thm_msg = Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm; val dep_msg = if null (tl deps) then NONE else SOME ("with dependency " ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps))); val thm_dep_msg = case (thm_msg, dep_msg) of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")" | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")" | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")" | (NONE, NONE) => "" in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end; fun maybe_permissive f prgrm = f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm); fun not_wellsorted ctxt permissive some_thm deps ty sort e = let val err_class = Sorts.class_error (Context.Proof ctxt) e; val err_typ = "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ Syntax.string_of_sort ctxt sort; in translation_error ctxt permissive some_thm deps "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end; (* inference of type annotations for disambiguation with type classes *) fun mk_tagged_type (true, T) = Type ("", [T]) | mk_tagged_type (false, T) = T; fun dest_tagged_type (Type ("", [T])) = (true, T) | dest_tagged_type T = (false, T); val untag_term = map_types (snd o dest_tagged_type); fun tag_term (proj_sort, _) eqngr = let val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr; fun tag (Const (_, T')) (Const (c, T)) = Const (c, mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T)) | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t) | tag (Free _) (t as Free _) = t | tag (Var _) (t as Var _) = t | tag (Bound _) (t as Bound _) = t; in tag end fun annotate ctxt algbr eqngr (c, ty) args rhs = let val erase = map_types (fn _ => Type_Infer.anyT []); val reinfer = singleton (Type_Infer_Context.infer_types ctxt); val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args); val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs)))); in tag_term algbr eqngr reinferred_rhs rhs end fun annotate_eqns ctxt algbr eqngr (c, ty) eqns = let val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global |> Config.put Type_Infer_Context.const_sorts false; (*avoid spurious fixed variables: there is no eigen context for equations*) in map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns end; (* abstract dictionary construction *) datatype typarg_witness = Weakening of (class * class) list * plain_typarg_witness and plain_typarg_witness = Global of (string * class) * typarg_witness list list | Local of { var: string, index: int, sort: sort, unique: bool }; fun brand_unique unique (w as Global _) = w | brand_unique unique (Local { var, index, sort, unique = _ }) = Local { var = var, index = index, sort = sort, unique = unique }; fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) = let fun class_relation unique (Weakening (classrels, x), sub_class) super_class = Weakening ((sub_class, super_class) :: classrels, brand_unique unique x); fun type_constructor (tyco, _) dss class = Weakening ([], Global ((tyco, class), (map o map) fst dss)); fun type_variable (TFree (v, sort)) = let val sort' = proj_sort sort; in map_index (fn (n, class) => (Weakening ([], Local { var = v, index = n, sort = sort', unique = true }), class)) sort' end; val typarg_witnesses = Sorts.of_sort_derivation algebra {class_relation = fn _ => fn unique => Sorts.classrel_derivation algebra (class_relation unique), type_constructor = type_constructor, type_variable = type_variable} (ty, proj_sort sort) handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e; in (typarg_witnesses, (deps, program)) end; (* translation *) fun ensure_tyco ctxt algbr eqngr permissive tyco = let val thy = Proof_Context.theory_of ctxt; val ((vs, cos), _) = Code.get_type thy tyco; val stmt_datatype = fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs #>> map fst ##>> fold_map (fn (c, (vs, tys)) => ensure_const ctxt algbr eqngr permissive c ##>> pair (map (unprefix "'" o fst) vs) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos #>> Datatype; in ensure_stmt Type_Constructor stmt_datatype tyco end and ensure_const ctxt algbr eqngr permissive c = let val thy = Proof_Context.theory_of ctxt; fun stmt_datatypecons tyco = ensure_tyco ctxt algbr eqngr permissive tyco #>> Datatypecons; fun stmt_classparam class = ensure_class ctxt algbr eqngr permissive class #>> Classparam; fun stmt_fun cert = case Code.equations_of_cert thy cert of (_, NONE) => pair NoStmt | ((vs, ty), SOME eqns) => let val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns val some_case_cong = Code.get_case_cong thy c; in fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> translate_eqns ctxt algbr eqngr permissive eqns' #>> (fn (_, NONE) => NoStmt | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong)) end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco | NONE => (case Axclass.class_of_param thy c of SOME class => stmt_classparam class | NONE => stmt_fun (Code_Preproc.cert eqngr c)) in ensure_stmt Constant stmt_const c end and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val cs = #params (Axclass.get_info thy class); val stmt_class = fold_map (fn super_class => ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c ##>> translate_typ ctxt algbr eqngr permissive ty) cs #>> (fn info => Class (unprefix "'" Name.aT, info)) in ensure_stmt Type_Class stmt_class class end and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) = let val stmt_classrel = ensure_class ctxt algbr eqngr permissive sub_class ##>> ensure_class ctxt algbr eqngr permissive super_class #>> Classrel; in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) = let val thy = Proof_Context.theory_of ctxt; val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; val these_class_params = these o try (#params o Axclass.get_info thy); val class_params = these_class_params class; val superclass_params = maps these_class_params ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class); val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; val vs' = map2 (fn (v, sort1) => fn sort2 => (v, Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; val arity_typ = Type (tyco, map TFree vs); val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); fun translate_super_instance super_class = ensure_class ctxt algbr eqngr permissive super_class ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class]) #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss)); fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); val dom_length = length (fst (strip_type ty)) val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in ensure_const ctxt algbr eqngr permissive c ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE) #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true))) end; val stmt_inst = ensure_class ctxt algbr eqngr permissive class ##>> ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs ##>> fold_map translate_super_instance super_classes ##>> fold_map translate_classparam_instance class_params ##>> fold_map translate_classparam_instance superclass_params #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) => Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params }); in ensure_stmt Class_Instance stmt_inst (tyco, class) end and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) = pair (ITyVar (unprefix "'" v)) | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) = ensure_tyco ctxt algbr eqngr permissive tyco ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys #>> (fn (tyco, tys) => tyco `%% tys) and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) = translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs) | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) = pair (IVar (SOME v)) | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) = let val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t); - val v'' = if member (op =) (Term.add_free_names t' []) v' - then SOME v' else NONE + val v'' = if Term.used_free v' t' then SOME v' else NONE in translate_typ ctxt algbr eqngr permissive ty ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) #>> (fn (ty, t) => (v'', ty) `|=> t) end | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) = case strip_comb t of (Const (c, ty), ts) => translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs) | (t', ts) => translate_term ctxt algbr eqngr permissive some_thm (t', some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) = fold_map (translate_term ctxt algbr eqngr permissive some_thm) args ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs) #>> rpair (some_thm, proper) and translate_eqns ctxt algbr eqngr permissive eqns = maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns) and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) = let val thy = Proof_Context.theory_of ctxt; val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) andalso Code.is_abstr thy c then translation_error ctxt permissive some_thm deps "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) = let val thy = Proof_Context.theory_of ctxt; val (annotate, ty') = dest_tagged_type ty; val typargs = Sign.const_typargs thy (c, ty'); val sorts = Code_Preproc.sortargs eqngr c; val (dom, range) = Term.strip_type ty'; in ensure_const ctxt algbr eqngr permissive c ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts) ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom) #>> (fn (((c, typargs), dss), annotation :: dom) => IConst { sym = Constant c, typargs = typargs, dicts = dss, dom = dom, annotation = if annotate then SOME annotation else NONE }) end and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (t, ts) => t `$$ ts) and translate_case ctxt algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) = let val thy = Proof_Context.theory_of ctxt; fun arg_types num_args ty = fst (chop num_args (binder_types ty)); val tys = arg_types num_args (snd c_ty); val ty = nth tys t_pos; fun mk_constr NONE t = NONE | mk_constr (SOME c) t = let val n = Code.args_number thy c; in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end; val constrs = if null case_pats then [] else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts)); fun disjunctive_varnames ts = let val vs = (fold o fold_varnames) (insert (op =)) ts []; in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end; fun purge_unused_vars_in t = let val vs = fold_varnames (insert (op =)) t []; in map_terms_bottom_up (fn IVar (SOME v) => IVar (if member (op =) vs v then SOME v else NONE) | t => t) end; fun collapse_clause vs_map ts body = case body of IConst { sym = Constant c, ... } => if Code.is_undefined thy c then [] else [(ts, body)] | ICase { term = IVar (SOME v), clauses = clauses, ... } => if forall (fn (pat', body') => exists_var pat' v orelse not (exists_var body' v)) clauses andalso forall (disjunctive_varnames ts o fst) clauses then case AList.lookup (op =) vs_map v of SOME i => maps (fn (pat', body') => collapse_clause (AList.delete (op =) v vs_map) (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses | NONE => [(ts, body)] else [(ts, body)] | _ => [(ts, body)]; fun mk_clause mk tys t = let val (vs, body) = unfold_abs_eta tys t; val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs []; val ts = map (IVar o fst) vs; in map mk (collapse_clause vs_map ts body) end; fun casify constrs ty t_app ts = let val t = nth ts t_pos; val ts_clause = nth_drop t_pos ts; val clauses = if null case_pats then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) else maps (fn ((constr as IConst { dom = tys, ... }, n), t) => mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t) (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause))); in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end; in translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE) ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE) #>> rpair n) constrs ##>> translate_typ ctxt algbr eqngr permissive ty ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts #>> (fn (((t, constrs), ty), ts) => casify constrs ty t ts) end and translate_app_case ctxt algbr eqngr permissive some_thm (case_schema as (num_args, _)) ((c, ty), ts) = if length ts < num_args then let val k = length ts; val tys = (take (num_args - k) o drop k o fst o strip_type) ty; val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees); val vs = Name.invent_names names "a" tys; in fold_map (translate_typ ctxt algbr eqngr permissive) tys ##>> translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), ts @ map Free vs) #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) end else if length ts > num_args then translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), take num_args ts) ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts) #>> (fn (t, ts) => t `$$ ts) else translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), ts) and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) = case Code.get_case_schema (Proof_Context.theory_of ctxt) c of SOME case_schema => translate_app_case ctxt algbr eqngr permissive some_thm case_schema c_ty_ts | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs) and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) = fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort) #>> (fn sort => (unprefix "'" v, sort)) and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) = let fun mk_dict (Weakening (classrels, d)) = fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels ##>> mk_plain_dict d #>> Dict and mk_plain_dict (Global (inst, dss)) = ensure_inst ctxt algbr eqngr permissive inst ##>> (fold_map o fold_map) mk_dict dss #>> Dict_Const | mk_plain_dict (Local { var, index, sort, unique }) = ensure_class ctxt algbr eqngr permissive (nth sort index) #>> (fn class => Dict_Var { var = unprefix "'" var, index = index, length = length sort, class = class, unique = unique }) in construct_dictionaries ctxt algbr permissive some_thm (ty, sort) #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses) end; (* store *) structure Program = Code_Data ( type T = program; val empty = Code_Symbol.Graph.empty; ); fun invoke_generation ignore_cache ctxt generate thing = Program.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) (fn program => ([], program) |> generate thing |-> (fn thing => fn (_, program) => (thing, program))); (* program generation *) fun check_abstract_constructors thy consts = case filter (Code.is_abstr thy) consts of [] => () | abstrs => error ("Cannot export abstract constructor(s): " ^ commas (map (Code.string_of_const thy) abstrs)); fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts = let val thy = Proof_Context.theory_of ctxt; val _ = if permissive then () else check_abstract_constructors thy consts; in Code_Preproc.timed "translating program" #ctxt (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt (fold_map (ensure_const ctxt algebra eqngr permissive)) consts) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts } end; fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts = invoke_generation_for_consts ctxt { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive } (Code_Preproc.obtain ignore_cache_and_permissive { ctxt = ctxt, consts = consts, terms = []}) consts |> snd; fun invoke_generation_for_consts'' ctxt algebra_eqngr = invoke_generation_for_consts ctxt { ignore_cache = true, permissive = false } algebra_eqngr #> (fn (deps, program) => { deps = deps, program = program }); fun consts_program_permissive ctxt = invoke_generation_for_consts' ctxt true; fun consts_program ctxt consts = let fun project program = Code_Symbol.Graph.restrict (member (op =) (Code_Symbol.Graph.all_succs program (map Constant consts))) program; in invoke_generation_for_consts' ctxt false consts |> project end; (* value evaluation *) fun ensure_value ctxt algbr eqngr t = let val ty = fastype_of t; val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) o dest_TFree))) t []; val t' = annotate ctxt algbr eqngr (\<^const_name>\Pure.dummy_pattern\, ty) [] t; val dummy_constant = Constant \<^const_name>\Pure.dummy_pattern\; val stmt_value = fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs ##>> translate_typ ctxt algbr eqngr false ty ##>> translate_term ctxt algbr eqngr false NONE (t', NONE) #>> (fn ((vs, ty), t) => Fun (((vs, ty), [(([], t), (NONE, true))]), NONE)); fun term_value (_, program1) = let val Fun ((vs_ty, [(([], t), _)]), _) = Code_Symbol.Graph.get_node program1 dummy_constant; val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant; val program2 = Code_Symbol.Graph.del_node dummy_constant program1; val deps_all = Code_Symbol.Graph.all_succs program2 deps'; val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2; in ((program3, ((vs_ty, t), deps')), (deps', program2)) end; in ensure_stmt Constant stmt_value \<^const_name>\Pure.dummy_pattern\ #> snd #> term_value end; fun dynamic_evaluation comp ctxt algebra eqngr t = let val ((program, (vs_ty_t', deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, algebra, eqngr, t } => invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t) { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t }; in comp program t vs_ty_t' deps end; fun dynamic_conv ctxt conv = Code_Preproc.dynamic_conv ctxt (dynamic_evaluation (fn program => fn _ => conv program) ctxt); fun dynamic_value ctxt postproc comp = Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluation comp ctxt); fun static_evaluation ctxt consts algebra_eqngr static_eval = static_eval (invoke_generation_for_consts'' ctxt algebra_eqngr consts); fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval = let fun evaluation program dynamic_eval ctxt t = let val ((_, ((vs_ty', t'), deps)), _) = Code_Preproc.timed "translating term" #ctxt (fn { ctxt, t } => ensure_value ctxt algebra eqngr t ([], program)) { ctxt = ctxt, t = t }; in dynamic_eval ctxt t (vs_ty', t') deps end; in static_evaluation ctxt consts algebra_eqngr (fn program_deps => evaluation (#program program_deps) (static_eval program_deps)) end; fun static_evaluation_isa ctxt consts algebra_eqngr static_eval = static_evaluation ctxt consts algebra_eqngr (fn program_deps => (static_eval (#program program_deps))); fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr (fn program_deps => let val static_conv = conv program_deps; in fn ctxt => fn _ => fn vs_ty => fn deps => static_conv ctxt vs_ty deps end)); fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv = Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr => static_evaluation_isa ctxt consts algebra_eqngr conv); fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp = Code_Preproc.static_value ctxt_postproc_consts (fn algebra_eqngr => static_evaluation_thingol ctxt consts algebra_eqngr comp); (** constant expressions **) fun read_const_exprs_internal ctxt = let val thy = Proof_Context.theory_of ctxt; fun this_theory name = if Context.theory_name thy = name then thy else Context.get_theory {long = false} thy name; fun consts_of thy' = fold (fn (c, (_, NONE)) => cons c | _ => I) (#constants (Consts.dest (Sign.consts_of thy'))) [] |> filter_out (Code.is_abstr thy); fun belongs_here thy' c = forall (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); fun read_const_expr str = (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of SOME "_" => ([], consts_of thy) | SOME s => (case try (unsuffix "._") s of SOME name => ([], consts_of_select (this_theory name)) | NONE => ([Code.read_const thy str], [])) | NONE => ([Code.read_const thy str], [])); in apply2 flat o split_list o map read_const_expr end; fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt; fun read_const_exprs ctxt const_exprs = let val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs; val consts' = consts_program_permissive ctxt consts_permissive |> implemented_deps |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt)); in union (op =) consts' consts end; (** diagnostic commands **) fun code_depgr ctxt consts = let val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = consts, terms = [] }; val all_consts = Graph.all_succs eqngr consts; in Graph.restrict (member (op =) all_consts) eqngr end; fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt; fun coalesce_strong_conn gr = let val xss = Graph.strong_conn gr; val xss_ys = map (fn xs => (xs, commas xs)) xss; val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys); fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs |> subtract (op =) xs |> map y_for |> distinct (op =); val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; in map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys end; fun code_deps ctxt consts = let val thy = Proof_Context.theory_of ctxt; fun mk_entry ((name, consts), (ps, deps)) = let val label = commas (map (Code.string_of_const thy) consts); in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end; in code_depgr ctxt consts |> Graph.map (K (Code.pretty_cert thy o snd)) |> coalesce_strong_conn |> map mk_entry |> Graph_Display.display_graph end; local fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt; fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt; in val _ = Outer_Syntax.command \<^command_keyword>\code_thms\ "print system of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs))); val _ = Outer_Syntax.command \<^command_keyword>\code_deps\ "visualize dependencies of code equations for code" (Scan.repeat1 Parse.term >> (fn cs => Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs))); end; end; (*struct*) structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;