# HG changeset patch # User haftmann # Date 1220590222 -7200 # Node ID e5c6c4aac52ce247645e37d8e89f9fade5122caf # Parent cf8da9bbc58413f02771cef7652d06bd8aa0800a different bookkeeping for code equations diff -r cf8da9bbc584 -r e5c6c4aac52c NEWS --- a/NEWS Fri Sep 05 06:50:20 2008 +0200 +++ b/NEWS Fri Sep 05 06:50:22 2008 +0200 @@ -19,6 +19,15 @@ *** Pure *** +* Different bookkeeping for code equations: + a) On theory merge, the last set of code equations for a particular constant + is taken (in accordance with the policy applied by other parts of the + code generator framework). + b) Code equations stemming from explicit declarations (e.g. code attribute) + gain priority over default code equations stemming from definition, primrec, + fun etc. + INCOMPATIBILITY. + * Global versions of theorems stemming from classes do not carry a parameter prefix any longer. INCOMPATIBILITY. diff -r cf8da9bbc584 -r e5c6c4aac52c doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Sep 05 06:50:20 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Sep 05 06:50:22 2008 +0200 @@ -310,32 +310,18 @@ \lstsml{Thy/examples/pick1.ML} - \noindent It might be convenient to remove the pointless original - equation, using the \emph{func del} attribute: -*} - -declare pick.simps [code func del] - -export_code pick (*<*)in SML(*>*) in SML file "examples/pick2.ML" - -text {* - \lstsml{Thy/examples/pick2.ML} - - \noindent Syntactic redundancies are implicitly dropped. For example, + \noindent The policy is that \emph{default equations} stemming from + @{text "\"}, + @{text "\"}, @{text "\"}, + @{text "\"}, @{text "\"}, + @{text "\"} statements are discarded as soon as an + equation is explicitly selected by means of \emph{code func}. + Further applications of \emph{code func} add theorems incrementally, + but syntactic redundancies are implicitly dropped. For example, using a modified version of the @{const fac} function as defining equation, the then redundant (since syntactically subsumed) original defining equations - are dropped, resulting in a warning: -*} - -lemma [code func]: - "fac n = (case n of 0 \ 1 | Suc m \ n * fac m)" - by (cases n) simp_all - -export_code fac (*<*)in SML(*>*)in SML file "examples/fac_case.ML" - -text {* - \lstsml{Thy/examples/fac_case.ML} + are dropped. \begin{warn} The attributes \emph{code} and \emph{code del} diff -r cf8da9bbc584 -r e5c6c4aac52c doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Sep 05 06:50:20 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Fri Sep 05 06:50:22 2008 +0200 @@ -381,48 +381,18 @@ \lstsml{Thy/examples/pick1.ML} - \noindent It might be convenient to remove the pointless original - equation, using the \emph{func del} attribute:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemmas}\isamarkupfalse% -\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\ {\isacharequal}\ pick{\isachardot}simps\ \isanewline -\isanewline -\isacommand{export{\isacharunderscore}code}\isamarkupfalse% -\ pick\ \ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{2}}{\isachardot}ML{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\lstsml{Thy/examples/pick2.ML} - - \noindent Syntactic redundancies are implicitly dropped. For example, + \noindent The policy is that \emph{default equations} stemming from + \isa{{\isasymDEFINITION}}, + \isa{{\isasymPRIMREC}}, \isa{{\isasymFUN}}, + \isa{{\isasymFUNCTION}}, \isa{{\isasymCONSTDEFS}}, + \isa{{\isasymRECDEF}} statements are discarded as soon as an + equation is explicitly selected by means of \emph{code func}. + Further applications of \emph{code func} add theorems incrementally, + but syntactic redundancies are implicitly dropped. For example, using a modified version of the \isa{fac} function as defining equation, the then redundant (since syntactically subsumed) original defining equations - are dropped, resulting in a warning:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{lemma}\isamarkupfalse% -\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline -\ \ {\isachardoublequoteopen}fac\ n\ {\isacharequal}\ {\isacharparenleft}case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ n\ {\isacharasterisk}\ fac\ m{\isacharparenright}{\isachardoublequoteclose}\isanewline -% -\isadelimproof -\ \ % -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}cases\ n{\isacharparenright}\ simp{\isacharunderscore}all% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\isacommand{export{\isacharunderscore}code}\isamarkupfalse% -\ fac\ \isakeyword{in}\ SML\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}fac{\isacharunderscore}case{\isachardot}ML{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\lstsml{Thy/examples/fac_case.ML} + are dropped. \begin{warn} The attributes \emph{code} and \emph{code del} @@ -620,7 +590,7 @@ The \emph{simpset} allows to employ the full generality of the Isabelle simplifier. Due to the interpretation of theorems - of defining equations, rewrites are applied to the right + as defining equations, rewrites are applied to the right hand side and the arguments of the left hand side of an equation, but never to the constant heading the left hand side. An important special case are \emph{inline theorems} which may be @@ -703,7 +673,7 @@ list of function theorems, provided that neither the heading constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc} pattern elimination implemented in - theory \isa{Efficient{\isacharunderscore}Nat} (\secref{eff_nat}) uses this + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this interface. \noindent The current setup of the preprocessor may be inspected using @@ -984,7 +954,7 @@ extend this table; as an example, we will develope an alternative representation of natural numbers as binary digits, whose size does increase logarithmically with its value, not linear - \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory \ref{eff_nat} + \footnote{Indeed, the \isa{Efficient{\isacharunderscore}Nat} theory (see \ref{eff_nat}) does something similar}. First, the digit representation:% \end{isamarkuptext}% \isamarkuptrue% @@ -1422,7 +1392,7 @@ pretty serializations for expressions like lists, numerals and characters; these are monolithic stubs and should only be used with the - theories introduces in \secref{sec:library}.% + theories introduced in \secref{sec:library}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1537,7 +1507,7 @@ \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes the preprocessor simpset. - \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds + \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds function transformer \isa{f} (named \isa{name}) to executable content; \isa{f} is a transformer of the defining equations belonging to a certain function definition, depending on the @@ -1580,20 +1550,20 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{CodeUnit.read\_const}\verb|CodeUnit.read_const: theory -> string -> string| \\ - \indexml{CodeUnit.head\_func}\verb|CodeUnit.head_func: thm -> string * ((string * sort) list * typ)| \\ - \indexml{CodeUnit.rewrite\_func}\verb|CodeUnit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\ + \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ + \indexml{Code\_Unit.head\_func}\verb|Code_Unit.head_func: thm -> string * ((string * sort) list * typ)| \\ + \indexml{Code\_Unit.rewrite\_func}\verb|Code_Unit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\ \end{mldecls} \begin{description} - \item \verb|CodeUnit.read_const|~\isa{thy}~\isa{s} + \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. - \item \verb|CodeUnit.head_func|~\isa{thm} + \item \verb|Code_Unit.head_func|~\isa{thm} extracts the constant and its type from a defining equation \isa{thm}. - \item \verb|CodeUnit.rewrite_func|~\isa{ss}~\isa{thm} + \item \verb|Code_Unit.rewrite_func|~\isa{ss}~\isa{thm} rewrites a defining equation \isa{thm} with a simpset \isa{ss}; only arguments and right hand side are rewritten, not the head of the defining equation. diff -r cf8da9bbc584 -r e5c6c4aac52c doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Sep 05 06:50:20 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Fri Sep 05 06:50:22 2008 +0200 @@ -3,10 +3,10 @@ datatype nat = Suc of nat | Zero_nat; -fun eq_nat Zero_nat Zero_nat = true +fun eq_nat (Suc a) Zero_nat = false + | eq_nat Zero_nat (Suc a) = false | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat' - | eq_nat Zero_nat (Suc a) = false - | eq_nat (Suc a) Zero_nat = false; + | eq_nat Zero_nat Zero_nat = true; end; (*struct Nat*) diff -r cf8da9bbc584 -r e5c6c4aac52c doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Sep 05 06:50:20 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML Fri Sep 05 06:50:22 2008 +0200 @@ -31,10 +31,10 @@ datatype nat = Suc of nat | Zero_nat; -fun eq_nat Zero_nat Zero_nat = true +fun eq_nat (Suc a) Zero_nat = false + | eq_nat Zero_nat (Suc a) = false | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat' - | eq_nat Zero_nat (Suc a) = false - | eq_nat (Suc a) Zero_nat = false; + | eq_nat Zero_nat Zero_nat = true; val eq_nata = {eq = eq_nat} : nat HOL.eq; @@ -63,23 +63,23 @@ Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree | Leaf of 'a * 'b; -fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = - (if HOL.less_eq - ((Orderings.ord_preorder o Orderings.preorder_order o - Orderings.order_linorder) - A2_) - it key - then Branch (update (A1_, A2_) (it, entry) t1, key, t2) - else Branch (t1, key, update (A1_, A2_) (it, entry) t2)) - | update (A1_, A2_) (it, entry) (Leaf (key, vala)) = - (if HOL.eqop A1_ it key then Leaf (key, entry) - else (if HOL.less_eq - ((Orderings.ord_preorder o Orderings.preorder_order o - Orderings.order_linorder) - A2_) - it key - then Branch (Leaf (it, entry), it, Leaf (key, vala)) - else Branch (Leaf (key, vala), it, Leaf (it, entry)))); +fun update (A1_, A2_) (it, entry) (Leaf (key, vala)) = + (if HOL.eqop A1_ it key then Leaf (key, entry) + else (if HOL.less_eq + ((Orderings.ord_preorder o Orderings.preorder_order o + Orderings.order_linorder) + A2_) + it key + then Branch (Leaf (it, entry), it, Leaf (key, vala)) + else Branch (Leaf (key, vala), it, Leaf (it, entry)))) + | update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) = + (if HOL.less_eq + ((Orderings.ord_preorder o Orderings.preorder_order o + Orderings.order_linorder) + A2_) + it key + then Branch (update (A1_, A2_) (it, entry) t1, key, t2) + else Branch (t1, key, update (A1_, A2_) (it, entry) t2)); val example : (Nat.nat, (Nat.nat list)) searchtree = update (Nat.eq_nata, Nat.linorder_nat) diff -r cf8da9bbc584 -r e5c6c4aac52c src/HOL/ex/NormalForm.thy --- a/src/HOL/ex/NormalForm.thy Fri Sep 05 06:50:20 2008 +0200 +++ b/src/HOL/ex/NormalForm.thy Fri Sep 05 06:50:22 2008 +0200 @@ -32,8 +32,9 @@ "add2 Z n = n" "add2 (S m) n = S(add2 m n)" +declare add2.simps [code] lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)" - by(induct n) auto + by (induct n) auto lemma [code]: "add2 n (S m) = S (add2 n m)" by(induct n) auto lemma [code]: "add2 n Z = n" diff -r cf8da9bbc584 -r e5c6c4aac52c src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Sep 05 06:50:20 2008 +0200 +++ b/src/Pure/Isar/code.ML Fri Sep 05 06:50:22 2008 +0200 @@ -113,11 +113,9 @@ end; -(** certificate theorems **) +(** logical and syntactical specification of executable code **) -fun string_of_lthms r = case Susp.peek r - of SOME thms => (map Display.string_of_thm o rev) thms - | NONE => ["[...]"]; +(* defining equations with default flag and lazy theorems *) fun pretty_lthms ctxt r = case Susp.peek r of SOME thms => map (ProofContext.pretty_thm ctxt) thms @@ -130,15 +128,11 @@ val thy_ref = Theory.check_thy thy; in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end; - -(** logical and syntactical specification of executable code **) - -(* pairs of (selected, deleted) defining equations *) - -type sdthms = thm list Susp.T * thm list; - -fun add_drop_redundant thm (sels, dels) = +fun add_drop_redundant verbose thm thms = let + fun warn thm' = (if verbose + then warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm') + else (); true); val thy = Thm.theory_of_thm thm; val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; val args = args_of thm; @@ -146,76 +140,40 @@ | matches (Var _ :: xs) [] = matches xs [] | matches (_ :: _) [] = false | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; - fun drop thm' = not (matches args (args_of thm')) - orelse (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false); - val (keeps, drops) = List.partition drop sels; - in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end; - -fun add_thm thm (sels, dels) = - apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels)); + fun drop thm' = matches args (args_of thm') andalso warn thm'; + in thm :: filter_out drop thms end; -fun add_lthms lthms (sels, []) = - (Susp.delay (fn () => fold add_drop_redundant - (Susp.force lthms) (Susp.force sels, []) |> fst), []) - (*FIXME*) - | add_lthms lthms (sels, dels) = - fold add_thm (Susp.force lthms) (sels, dels); - -fun del_thm thm (sels, dels) = - (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels); - -fun del_thms (sels, dels) = - let - val all_sels = Susp.force sels; - in (Susp.value [], rev all_sels @ dels) end; - -fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels; +fun add_thm _ thm (false, thms) = (false, Susp.value (add_drop_redundant true thm (Susp.force thms))) + | add_thm true thm (true, thms) = (true, Susp.value (Susp.force thms @ [thm])) + | add_thm false thm (true, thms) = (false, Susp.value [thm]); -fun melt _ ([], []) = (false, []) - | melt _ ([], ys) = (true, ys) - | melt eq (xs, ys) = fold_rev - (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs); +fun add_lthms lthms _ = (false, lthms); -val melt_thms = melt Thm.eq_thm_prop; +fun del_thm thm = apsnd (Susp.value o remove Thm.eq_thm_prop thm o Susp.force); -fun melt_lthms (r1, r2) = - if Susp.same (r1, r2) - then (false, r1) - else case Susp.peek r1 - of SOME [] => (true, r2) - | _ => case Susp.peek r2 - of SOME [] => (true, r1) - | _ => (apsnd (Susp.delay o K)) (melt_thms (Susp.force r1, Susp.force r2)); - -fun melt_sdthms ((sels1, dels1), (sels2, dels2)) = - let - val (dels_t, dels) = melt_thms (dels1, dels2); - in if dels_t - then let - val (_, sels) = melt_thms - (subtract Thm.eq_thm_prop dels2 (Susp.force sels1), Susp.force sels2); - val (_, dels) = melt_thms - (subtract Thm.eq_thm_prop (Susp.force sels2) dels1, dels2); - in ((Susp.delay o K) sels, dels) end - else let - val (_, sels) = melt_lthms (sels1, sels2); - in (sels, dels) end - end; +fun merge_defthms ((true, _), defthms2) = defthms2 + | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1 + | merge_defthms ((false, _), defthms2 as (false, _)) = defthms2; -(* specification data *) +(* syntactic datatypes *) val eq_string = op = : string * string -> bool; + fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) andalso gen_eq_set (eq_fst eq_string) (cs1, cs2); + fun merge_dtyps (tabs as (tab1, tab2)) = let fun join _ (cos as (_, cos2)) = if eq_dtyp cos then raise Symtab.SAME else cos2; in Symtab.join join tabs end; + +(* specification data *) + datatype spec = Spec of { - funcs: sdthms Symtab.table, + funcs: (bool * thm list Susp.T) Symtab.table, dtyps: ((string * sort) list * (string * typ list) list) Symtab.table, cases: (int * string list) Symtab.table * unit Symtab.table }; @@ -227,7 +185,7 @@ fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) }, Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) = let - val funcs = Symtab.join (K melt_sdthms) (funcs1, funcs2); + val funcs = Symtab.join (K merge_defthms) (funcs1, funcs2); val dtyps = merge_dtyps (dtyps1, dtyps2); val cases = (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2)); @@ -259,6 +217,9 @@ spec: spec }; + +(* code setup data *) + fun mk_exec (thmproc, spec) = Exec { thmproc = thmproc, spec = spec }; fun map_exec f (Exec { thmproc = thmproc, spec = spec }) = @@ -398,9 +359,9 @@ let val ctxt = ProofContext.init thy; val exec = the_exec thy; - fun pretty_func (s, lthms) = + fun pretty_func (s, (_, lthms)) = (Pretty.block o Pretty.fbreaks) ( - Pretty.str s :: pretty_sdthms ctxt lthms + Pretty.str s :: pretty_lthms ctxt lthms ); fun pretty_dtyp (s, []) = Pretty.str s @@ -518,9 +479,9 @@ val funcs = classparams |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco)) |> map (Symtab.lookup ((the_funcs o the_exec) thy)) - |> (map o Option.map) (Susp.force o fst) + |> (map o Option.map) (Susp.force o snd) |> maps these - |> map (Thm.transfer thy) + |> map (Thm.transfer thy); fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys | sorts_of tys = map (snd o dest_TVar) tys; val sorts = map (sorts_of o Sign.const_typargs thy o const_of thy) funcs; @@ -643,8 +604,7 @@ val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func); val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func); -end; - +end; (*local*) (** interfaces and attributes **) @@ -681,70 +641,49 @@ val is_undefined = Symtab.defined o snd o the_cases o the_exec; -fun add_func thm thy = - let - val func = mk_func thm; - val c = const_of_func thy func; - val _ = if (is_some o AxClass.class_of_param thy) c - then error ("Rejected polymorphic equation for overloaded constant:\n" - ^ Display.string_of_thm thm) - else (); - val _ = if (is_some o get_datatype_of_constr thy) c - then error ("Rejected equation for datatype constructor:\n" - ^ Display.string_of_thm func) - else (); - in - (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default - (c, (Susp.value [], [])) (add_thm func)) thy - end; - -fun add_liberal_func thm thy = - case mk_liberal_func thm - of SOME func => let - val c = const_of_func thy func - in if (is_some o AxClass.class_of_param thy) c - orelse (is_some o get_datatype_of_constr thy) c - then thy - else map_exec_purge (SOME [c]) (map_funcs - (Symtab.map_default - (c, (Susp.value [], [])) (add_thm func))) thy +fun gen_add_func strict default thm thy = + case (if strict then SOME o mk_func else mk_liberal_func) thm + of SOME func => + let + val c = const_of_func thy func; + val _ = if strict andalso (is_some o AxClass.class_of_param thy) c + then error ("Rejected polymorphic equation for overloaded constant:\n" + ^ Display.string_of_thm thm) + else (); + val _ = if strict andalso (is_some o get_datatype_of_constr thy) c + then error ("Rejected equation for datatype constructor:\n" + ^ Display.string_of_thm func) + else (); + in + (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default + (c, (true, Susp.value [])) (add_thm default func)) thy end | NONE => thy; -fun add_default_func thm thy = - case mk_default_func thm - of SOME func => let - val c = const_of_func thy func - in if (is_some o AxClass.class_of_param thy) c - orelse (is_some o get_datatype_of_constr thy) c - then thy - else map_exec_purge (SOME [c]) (map_funcs - (Symtab.map_default - (c, (Susp.value [], [])) (add_thm func))) thy - end - | NONE => thy; +val add_func = gen_add_func true false; +val add_liberal_func = gen_add_func false false; +val add_default_func = gen_add_func false true; -fun del_func thm thy = - case mk_liberal_func thm - of SOME func => let - val c = const_of_func thy func; - in map_exec_purge (SOME [c]) (map_funcs - (Symtab.map_entry c (del_thm func))) thy - end - | NONE => thy; +fun del_func thm thy = case mk_liberal_func thm + of SOME func => let + val c = const_of_func thy func; + in map_exec_purge (SOME [c]) (map_funcs + (Symtab.map_entry c (del_thm func))) thy + end + | NONE => thy; -fun del_funcs const = map_exec_purge (SOME [const]) - (map_funcs (Symtab.map_entry const del_thms)); +fun del_funcs c = map_exec_purge (SOME [c]) + (map_funcs (Symtab.map_entry c (K (false, Susp.value [])))); -fun add_funcl (const, lthms) thy = +fun add_funcl (c, lthms) thy = let - val lthms' = certificate thy (fn thy => certify_const thy const) lthms; + val lthms' = certificate thy (fn thy => certify_const thy c) lthms; (*FIXME must check compatibility with sort algebra; alas, naive checking results in non-termination!*) in - map_exec_purge (SOME [const]) - (map_funcs (Symtab.map_default (const, (Susp.value [], [])) - (add_lthms lthms'))) thy + map_exec_purge (SOME [c]) + (map_funcs (Symtab.map_default (c, (true, Susp.value [])) + (add_lthms lthms'))) thy end; val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute @@ -906,7 +845,7 @@ fun get_funcs thy const = Symtab.lookup ((the_funcs o the_exec) thy) const - |> Option.map (Susp.force o fst) + |> Option.map (Susp.force o snd) |> these |> map (Thm.transfer thy); @@ -953,9 +892,4 @@ end; -structure Code : CODE = -struct - -open Code; - -end; +structure Code : CODE = struct open Code; end;