Implement grep and prove spec #239
Merged
Conversation
This file contains 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
Also rename {testing,all} -> tests, and move target{Sem,Props} to
backend/semantics. These are changes towards the desired directory
structure expressed at https://wiki.cakeml.org/Conventions.
Tweak target{Sem,Props} script files so they build again after the move.
I don't entirely understand why this is necessary, or, more precisely, what I should be changing (set_grammar_ancestry? Holmakefiles? overloads?) since multiple fixes would work but the correct policy is not clear.
followup to 1cb4c1e
This is half of #226
Now that the relevant theorem is exported by regexp_compilerTheory
Use Basis functions where possible. Use MEMBER_INTRO to avoid translating LIST_TO_SET. Avoid name clashes. Extend from ioProg and prepare to translate parser.
These functions are useful for rewriting away shifts in definitions to be translated. The translator could perhaps be modified to support variable-length shifts directly (either using these rewrites or some other method).
Disturbingly, the interactive and non-interactive behaviour of the parser seems to be quite different. I think it gets the overloads wrong non-interactively, since preferring a constant in the current theory is surely desirable.
for grep this was trickier than I expected
This is work in progress. Bogged down in the spec, trying to prove things about FIELDS (which I am using to split a string into lines).
Even if one is committed to including every possible ancestral theory from HOL (via misc and/or preamble), one need not let their parsing context influence the current one. Currently, it's clearly far from ideal to depend on regexp_compiler for the definition of the vector type; doing so brings in balanced_map (which has its own notion of fromList).
Also define splitlines and prove some lemmas about it too. The specification for operating over lines in a file is complicated because file contents (string) might be empty and/or might not have a trailing newline.
Lots of hacking to work around CF's poor support for higher-order
functions. I found a way to prove a custom specification for a partially
applied function, which maybe should be revisited on the original
(nicer) grep implementation.
The cheats are:
1. regexp_matcher corresponds to regexp_lang
This should have been proved as part of the regexp matching theory,
but does not seem to be packaged up nicely.
2. termination of the regexp matching algorithm. if we do not prove
termination, then this will need to bubble up into the
specification somehow.
Also fix the open'd theories list
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Initial version of grep example (no compilation yet, and maybe the implementation can still be tweaked). The initial translation was done by @IlmariReissumies.