Check mapping completeness #647
Open
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
trdthg
force-pushed
the
mapping-match-complete
branch
3 times, most recently
from
78a0c43 to
5fb2a22
Compare
trdthg
commented
Jul 29, 2024
Comment on lines
80
to
85
| let ast, env = Type_error.check env ast in | ||
| let ast = Scattered.descatter ast in | ||
| let ast, env = Type_error.check Type_check.initial_env (Type_check.strip_ast ast) in | ||
| let side_effects = Effects.infer_side_effects asserts_termination ast in | ||
| Effects.check_side_effects side_effects ast; | ||
| let () = if !opt_ddump_tc_ast then Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast) else () in |
There was a problem hiding this comment.
type_check again to add_attrs after scattered mapdefs get together
trdthg
commented
Jul 29, 2024
Comment on lines
+1049
to
+1064
| (* TODO: handle unsupported syntax *) | ||
| try | ||
| (* prepare left *) | ||
| let lpats = List.map (fun mapcl -> lpat_of_mapcl mapcl true) mapcls in | ||
| let _, lpats = opt_cases_to_pats 0 have_guard lpats in | ||
| let lmatrix = | ||
| Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typl) pat])) lpats) | ||
| in | ||
| (* prepare right *) | ||
| let rpats = List.map (fun mapcl -> lpat_of_mapcl mapcl false) mapcls in | ||
| let _, rpats = opt_cases_to_pats 0 have_guard rpats in | ||
| let rmatrix = | ||
| Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some typr) pat])) rpats) | ||
| in | ||
| is_complete_matrixs ~keyword:"mapping" l ctx have_guard [(typl, lmatrix); (typr, rmatrix)] | ||
| with _ -> false |
There was a problem hiding this comment.
Some syntaxes are not supported in match, but are allowed by mapping
example: test/c/poly_mapping2.sail
mapping test2m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) : bits(2) @ v }
When encountering this kind of syntax, an exception will be thrown, so here fallback to false.
trdthg
force-pushed
the
mapping-match-complete
branch
from
2f18442 to
bd229e9
Compare
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.
fix #424
Add basic mapdef completeness check