Dynamic layout for inexhaustive case/indeterminately match case #1125
Conversation
| @@ -271,7 +272,11 @@ let rec dhexp_of_uexp = | |||
| | InHole( | |||
| InexhaustiveMatch(Some(Common(Inconsistent(Internal(_))))), | |||
| ) => | |||
| // TODO: review | |||
There was a problem hiding this comment.
Not problematic for now since currently DHExp.InexhaustiveCase behaves exactly the same as DHExp.InconsistentBranches
| @@ -33,6 +33,7 @@ module rec DHExp: { | |||
| | Prj(t, int) | |||
| | Constructor(string) | |||
| | ConsistentCase(case) | |||
| | InexhaustiveCase(MetaVar.t, HoleInstanceId.t, case) | |||
There was a problem hiding this comment.
Instead of having three different case constructs in DHExp, let's merge them into one with an additional flag parameter for when there is an error.
cyrus-
added
the
needs-polish
|
@pigumar1 I don't recall the precise purpose of this PR -- what is it and what is the status? |
@cyrus- I have updated the purpose of this PR at the top. The expected behavior has already been implemented, but some code simplifications can be done, as suggested by the comment above. #1154 was introduced for this code simplification, but it has its own relevant concerns, which are mentioned at the top of that PR. |
This pull request implements the functionality of visually crossing out mismatched rules during evaluation. It's possible for the evaluation of an indeterminately exhaustive case expression to get stuck when we cannot determine whether a rule is matched or mismatched. In this case, the rules preceding this rule are crossed out.
