trying to merge egraph-less parts from egraphs branch #284
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
to egg, which manages to simplify the goal to True
and feed some examples to cvc5
defining disjoint union (du) in terms of disjointb instead of dput and map.fold, which makes associativity much simpler to prove
which splits off an address range from a record
but casting from `interp_type tp1` to `interp_type tp1'` where tp1 and tp1' only differ in presence flags seems cumbersome
using Inductive presence{P: Type} := PPresent | PAbsent | PPartial(p: P)
However, this creates redundant respresentations for all-present and
all-absent (they could also be represented as PPartial), and after merging
a piece back into a record, we'd have to simplify all-present PPartials into
PPresent, and after removing all fields of a record, also simplify all-absent
PPartials into PAbsent, so it seems better to record presence information
only at the leaves.
define type_presence_sub, wip new split_off_from_type
but no generic rep appearing in sepclauses, because that would have to be used very pervasively in all lemmas, so array lemmmas would all be stated in terms of rep instead of array, and unfolding/ folding rep also is a bit more complicated
(needed inside sepapps, because there are no addresses there)
and match hyp clauses to them
order of then/else branch, reorder file
min3_mem example goes through
… work with mem_hyp
rewrite in type of mem_hyp does not work if there is also a proj_mem of this hyp, which basically always exists
creating an evar for the frame, but instead implicitly instantiate the frame with (wand calleePost callerPost) which can be thought of as "callerPost minus calleePost" which solves the problem that variables introduced during cancellation are not in the evar context of the frame evar.
instead of having to restate all function specs using wand
Quite lightweight because it does not include the wand+ramification trick (which is done at the end of cancellation)
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.
No description provided.