Add simple_word_enum command to performantly register large flat enum types - #266
Merged
Merged
Conversation
Num_Case_Expression imports only Main and provides the `ncase _ of _` selector, which is generic infrastructure rather than anything specific to the shallow Micro Rust embedding. It belongs in Misc, and it needs to live there for anything in the Misc session to use it: Shallow_Micro_Rust already depends on Misc, so a Misc theory importing Shallow_Micro_Rust.Num_Case_Expression would close a session dependency cycle and make the Misc session unbuildable. Its only in-tree consumer outside Misc, Shallow_Micro_Rust.Core_Syntax, now reaches it as Misc.Num_Case_Expression. Verified: `isabelle build -n -d . AutoCorrode` resolves the whole session tree, and a full `isabelle build -d . Misc` checks every theory in the session. (Document generation fails for want of a lualatex binary, both here and at the pre-existing baseline -- unrelated to this change.) Signed-off-by: Ike Mulder <ikemul@amazon.com>
Add a `simple_word_enum` command that generates the boilerplate for a type
whose inhabitants correspond one-to-one to a fixed list of distinct machine
words:
simple_word_enum (32) my_enum =
Answer = \<open>0x42\<close>
| Best = \<open>0x72\<close>
For a type T it generates T_variants (the word list) and
T_variants_distinct; the typedef of T over `set (map unat T_variants)` with
setup_lifting applied; one lifted constant per variant, with the transfer
rules collected in the named theorem bundles T_rep_defs (rep_eq) and T_defs
(abs_eq); T_all with T_all_concrete [code], T_all_distinct and T_all_total;
and finally everything setup_case_for_typedef provides, so that
`case _ of _ \<Rightarrow> _` works on the new type.
Values are ordinary terms, but note that hexadecimal literals need a
cartouche: the outer syntax lexes 0x42 as a Nat token followed by an
identifier, and Parse.term consumes a single token. Plain decimal numerals
need no cartouche.
Two supporting lemmas, simple_word_enum_distinct and
simple_word_enum_total, are stated once over an abstract
`type_definition Rep Abs (set (map unat ws))` so that the generated
T_all_distinct / T_all_total are single rule applications rather than metis
searches, as they were in the hand-written version this replaces.
Conversion functions between T and its representation word type are not
generated; the tests show how they are built on top.
To support this, setup_case_for_typedef's implementation is lifted out of
its `local` block in Case_for_Typedefs.thy into `structure
Case_For_Typedef`, exposing a thm-taking entry point plus a `verbose` flag,
so simple_word_enum can hand it freshly-proved theorems without a
theorem-name round-trip. The behaviour of the setup_case_for_typedef
command itself is unchanged.
Performance, measured on a 120-variant 64-bit enum (4.5s elapsed, 7.3s
cpu): the distinctness proof and the 120 lift_definition calls cost ~2s
each and dominate; everything else is under 0.3s, with all of define_all
at 0.03s. The distinctness proof deliberately uses the default simp set —
reducing `unat` of a numeral needs the word simp rules, no hand-picked
[simp only:] set was found that discharges it, and code_simp does not
terminate on a few dozen variants.
Verified: Misc.Simple_Word_Enums and Misc.Case_for_Typedefs check clean
(0 errors, 0 warnings) via ic2.
Signed-off-by: Ike Mulder <ikemul@amazon.com>
Two more plugins for the simple_word_enum plugin mechanism, both on by default and suppressible with `plugins del:`. generate_debug emits the generate_debug class instance, rendering each variant as its own name. The case arms carry the bare names rather than whole log_data lists, so the defining term holds one `str` application instead of one per variant. No per-variant equations are generated: generate_debug_T_def plus the case simproc reduces a concrete variant in a fixed number of rewrites. The instance has to go into the background theory, since classes are global. The fact it declares there is not reliably reachable from the target the declaration appeared in, and the namespace it lands in differs between a fresh declaration and the retro-application the plugin mechanism performs over already-declared enums at registration time. So the background fact gets a concealed name and the exported theorem is noted into the local target, as the other plugins do. variant_equality registers a simproc deciding Ci = Cj on concrete variants. Previously simp could not settle `Red = Blue`: T_all_distinct states pairwise distinctness, but reaching a particular pair took a T_index detour by hand. The simproc is built like the case_T one in Case_for_Typedefs: it fires from the term net, guards on both sides being concrete variants of the right type, and leaves anything else alone. Identical variants go by refl; differing ones push T_index across the assumed equation via a pre-instantiated arg_cong, reduce by T_indices_concrete, and discharge the resulting numeral equation. Cost per firing is independent of the variant count, and registration is 0ms at every benchmarked size. Also refreshes two comments that described superseded code: the to_uN_pure_alt tactic notes (the by-cases proof and its quadratic pitfalls are gone, the uniform proof is ~9ms at 64 variants) and the benchmark prose (variants and variant_consts dominate now).
…imple_word_enum
Three changes to simple_word_enum, the last two coupled by a new
`urust: "Name"` clause.
Variants are now reachable type-qualified as `T.Ci`, not just bare, the
way datatype constructors are. This is a Local_Theory.const_alias under
`Binding.qualify false type_name` --- the same non-mandatory qualification
ctr_sugar gives datatype's constructors, so both spellings resolve to the
identical constant and neither shadows the other. typedef does the same
for Rep_T/Abs_T.
The declaration accepts an optional `urust: "Name"` clause after the type
name. Misc.Simple_Word_Enums does nothing with it: the name is recorded
on the enum_info handed to plugins, for a plugin to act on. The benchmark
command passes NONE, since a notation registration is a global effect that
would outlive its discarded local theory.
Two plugins in the new Shallow_Micro_Rust.Simple_Word_Enum_uRust consume
that name, independently selectable:
urust_notation -- each variant Ci as the uRust literal `Name::Ci`,
the registration StdLib_Ordering makes by hand for
the ordering datatype
urust_conversion -- word_conversion's to/try_from functions lifted with
lift_fun1 into function_body form and registered as
calls, `Name::to_uN` / `Name::try_from`, mirroring
word_try_from_fun in Numeric_Types
Both are no-ops without a `urust:` clause. The lifted `_def` facts are
deliberately not tagged [micro_rust_simps]: whether a call unfolds to its
pure function during uRust reasoning is the caller's choice.
These live downstream rather than beside the command because
micro_rust_notation belongs to Shallow_Micro_Rust, which depends on Misc
--- registering a plugin from a downstream theory is what the plugin
mechanism is for (cf. bnf_lfp_size.ML against datatype). That dependency
also fixes the execution order: plugin.ML applies interpretations in
registration order (cons + fold_rev), and Misc is fully loaded before this
theory's ML runs, so word_conversion always precedes urust_conversion.
Only `plugins del: word_conversion` with urust_conversion left enabled can
break that, since the pure functions never get defined. It errors, naming
the missing constant and the contradictory pair, rather than silently doing
nothing; a test drives the failure through simple_word_enum_core under
Exn.capture and asserts on the message.
The uRust names are required to be plain identifiers: `Name::Ci` is a
::-path the frontend grammar already parses, so no bespoke production is
needed, but only if Name itself is an identifier. Rejecting at declaration
beats a registration whose use sites could never parse.
A case expression on a simple_word_enum was not code-exportable: case_T reduces through match_T to find_index, which needs equality on T, so export_code failed with "Type T not of sort equal". The new equal_instance plugin supplies the instance as `equal_T x y == Rep_T x = Rep_T y`, proved by Rep_T_inject. Constant cost: 13-15ms from 4 through 64 variants. A plugin rather than part of setup_case_for_typedef, because that command runs on an existing typedef which may already be an equal instance, and a class instance is global and unconditional. simple_word_enum creates the typedef itself, so it knows the slot is free. Separately, the generated constants had no code equations at all, so exporting anything reaching T_variants or either conversion function failed with "No code equations". They were defined via Local_Theory.define, which attaches none; they now go through Specification.definition, which attaches a default one. Being a default, T_all_concrete's explicit [code] still supersedes it for T_all, as a test asserts. Tests evaluate equality and a case-based function, export the variants, T_all, and the pure and uRust-lifted conversions to OCaml and SML, and check that `plugins del: equal_instance` omits the instance.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add
simple_word_enumcommand to create an enum type backed by words. For example,creates an Isabelle type
my_enum, with variantsAnswerandBest, with conversion functionsmy_enum_to_u32_pure : my_enum => 32 wordandmy_enum_try_from_u32_pure : 32 word => (my_enum, unit) result, uRust versions of these, properties of these conversion functions, support for case analysis onmy_enum, support for code extraction, and registers uRust notationMyEnum::Answer.The only slow proof in this construction is
distinct (variant_representation_values), which is quadratic. Tests show that enums with 128 variants take about ~5s locally to construct, which is a drastic improvement over Isabelle's nativedatatypeand for theenumcommand already available in AutoCorrode. On the other hand,simple_word_enumcan only handle flat enums.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.