Add pattern-variables.md

proposals/pattern-variables.md

@@ -2,157 +2,69 @@
 
 ## Summary  
 
-## Motivation
-
-## Specification
-
-### Scope
-
-#### Pattern variable redeclaration
-
-Introducing a new concept similar to *name hiding*, but these names can possibly reference either of variables based on the result of the pattern-matching at runtime.
-
-There's two degrees of enforcement as to whether variables may be redeclared:
-
-- Pattern variables within pattern boundaries *must* be redeclared because assignment of such variables depend on the order of evaluation which is undefined for patterns.
-- Pattern variables outside pattern boundaries *can* be redeclared, definitive assignment rules for the containing expression specify where such variables are usable.
-
-For a *disjunctive_pattern* of the form `left_pattern or right_pattern`:
-- Pattern variables declared in the *left_pattern* **must be redeclared** in the *right_pattern*; permitting:
-
-  ```cs
-  e is (0, var x) or (var x, 0)
-  ```
-
-For a *logical_or_expression* of the form `left_expr || right_expr`:
-- Pattern variables declared in *left_expr* **can be redeclared** in the *right_expr*; permitting:
-
-  ```cs
-  e is (0, var x) || e is (var x, 0)
-  ```
-  Note: This is the expression variation of the previous case.
-
-For a *negated_pattern* of the form `not pattern_operand`:
-- Pattern variables declared in the *pattern_operand* **must be redeclared** inside any other *negated_pattern* in the containing pattern; permitting:
-
-  ```cs
-  e is not (0, var x) and not (var x, 0)
-  ```
-   Note: This is the DeMorgan's transformation of the previous case.
-- Pattern variables declared in the *pattern_operand* **can be redeclared** anywhere in the containing expression; permitting:
+Allow variable declarations under `or` patterns and across `case` labels in a `switch` section.
 
-  ```cs
-  e is not (0, var x) && e is not (var x, 0)
-  ```
-  Note: This is the expression variation of the previous case.
-
-For a *logical_not_expression* of the form `!expr_operand`:
-- Pattern variables declared in the *expr_operand* **can be redeclared** anywhere in the containing expression; permitting:
-
-  ```cs
-  !(e is (0, var x)) && !(e is (var x, 0))
-  ```
-  Note: This is the expression variation of the previous case.
-
-For a *switch_case_label* of the form `case case_pattern when when_expr`:
-- Pattern variables declared in the *case_pattern* or *when_expr* **can be redeclared** in other case labels; permitting:
-
-	```cs
-	case (var x, 0) when e is int i:
-	case (0, var x) when a is int i:
-	```
-
-	Note: This rule is currently defined for each individual *switch_section* only.
-
-For a *conditional_expression* of the form `expr_cond ? expr_true : expr_false`:
-- Pattern variables declared in *expr_true* **can be redeclared** in *expr_false*; permitting:
+## Motivation
 
-	```cs
-	b ? x is int i : y is int i
-	```
+This feature would reduce code duplication where we could use the same piece of code if either of patterns is satisfied. For instance:
+```cs
+if (e is (int x, 0) or (0, int x))
+    Use(x);
+
+switch (e)
+{
+    case (int x, 0):
+    case (0, int x):
+	Use(x);
+	break;
+}
+```
+Instead of:
+
+```cs
+if (e is (int x, 0))
+    Use(x);
+else
+    Use(x)
+
+switch (e)
+{
+    case (int x, 0):
+        Use(x);
+        break;
+    case (0, int x):
+        Use(x);
+        break;
+}
+```
+
+## Detailed design
+
+Variables *must* be redeclared under all disjuncitve patterns because assignment of such variables depend on the order of evaluation which is undefined in the context of pattern-matching.
+
+- In a *disjunctive_pattern*, pattern variables declared under the left-hand-side must be redeclared under the right-hand-side.
+- In a *switch_section*, pattern variables declared under each case label must be redeclared under every other case label.
+
+In any other case, variable declaration follows the usual scoping rules and is disallowed.
+
+These names can reference either of variables based on the result of the pattern-matching at runtime. Under the hood, it's the same local being assigned in each pattern.
 
 Redeclaring pattern variables is only permitted for variables of the same type.
 
-> **Open question**: How identical these types should be?
-
-Redeclaring pattern variables in any other case follows the usual scoping rules and is disallowed.
-
-### Definite assignment
-
-Note: This section is unchanged and included for the sake of completeness.
-
-For an *is_pattern_expression* of the form `e is pattern`:
-
-- The definite assignment state of *v* after *is_pattern_expression* is determined by:
-
-    - The state of *v* after *is_pattern_expression* is definitely assigned, if the *pattern* is irrefutable. permitting use after:
-
-        ```cs
-        _ = x is var x;
-        _ = 1 is int x;
-        _ = (1, 2) is var (x, y) and var z;
-       ```
-
-    - Otherwise, the state of *v* after *is_pattern_expression* is the same as the state of *v* after *pattern*.
-
-For a *var_pattern* of the form `var variable_designation`:
-
-- The definite assignment state of *v* after *var_pattern* is determined by:
-
-    - The state of *v* after *var_pattern* is definitely assigned if *variable_designation* is a *single_variable_designation*.
-    - Otherwise, the state of *v* after *var_pattern* is "definitely assigned when true".
-
-#### General rules for pattern variables in simple patterns 
-
-Note: This section is unchanged and included for the sake of completeness.
-
-The following rules applies to any *primary_pattern* that declares a variable:
-
-- The state of *v* is "definitely assigned when true" after *primary_pattern*; permitting use after:
-
-    ```cs
-    if (o is int x)
-    ```
-
-#### Definite assignment rules for pattern variables in pattern combinators
-
-Note: This section is derived by definite assignment rules for expressions.
-
-For a *disjunctive_pattern* of the form `left_pattern or right_pattern`:
-
-- The definite assignment state of *v* after *disjunctive_pattern* is determined by:
-    - If the state of *v* after *left_pattern* is definitely assigned, then the state of *v* after *disjunctive_pattern* is definitely assigned.
-    - Otherwise, if the state of *v* after *right_pattern* is definitely assigned, and the state of *v* after *left_pattern* is "definitely assigned when true", then the state of *v* after *disjunctive_pattern* is definitely assigned.
-    - Otherwise, if the state of *v* after *right_pattern* is definitely assigned or "definitely assigned when false", then the state of *v* after *disjunctive_pattern* is "definitely assigned when false".
-    - Otherwise, if the state of *v* after *left_pattern* is "definitely assigned when true", and the state of *v* after *right_pattern* is "definitely assigned when true", then the state of *v* after *disjunctive_pattern* is "definitely assigned when true".
-    - Otherwise, the state of *v* after *disjunctive_pattern* is not definitely assigned.
-
-For a *conjunctive_pattern* of the form `left_pattern and right_pattern`:
-
-- The definite assignment state of *v* after *conjunctive_pattern* is determined by:
-    - If the state of *v* after *left_pattern* is definitely assigned, then the state of *v* after *conjunctive_pattern* is definitely assigned.
-    - Otherwise, if the state of *v* after *right_pattern* is definitely assigned, and the state of *v* after *left_pattern* is "definitely assigned when false", then the state of *v* after *conjunctive_pattern* is definitely assigned.
-    - Otherwise, if the state of *v* after *right_pattern* is definitely assigned or "definitely assigned when true", then the state of *v* after *conjunctive_pattern* is "definitely assigned when true".
-    - Otherwise, if the state of *v* after *left_pattern* is "definitely assigned when false", and the state of *v* after *right_pattern* is "definitely assigned when false", then the state of *v* after *conjunctive_pattern* is "definitely assigned when false".
-    - Otherwise, the state of *v* after *conjunctive_pattern* is not definitely assigned.
-
-For a *negated_pattern* of the form `not pattern_operand`:
-
-- The definite assignment state of *v* after *negated_pattern* is determined by:
-    - If the state of *v* after *pattern_operand* is "definitely assigned when true", then the state of *v* after *negated_pattern* is "definitely assigned when false".
-    - If the state of *v* after *pattern_operand* is "definitely assigned when false", then the state of *v* after *negated_pattern* is "definitely assigned when true".
-    - If the state of *v* after *pattern_operand* is definitely assigned, then the state of *v* after *negated_pattern* is definitely assigned.
-
-Note that these rules cover the existing top-level `is not` patterns. However, in other cases instead of a hard error, the variables will be left unassigned.
-
-### Remarks
-
-Definite assignment specification in any other case is unchanged. For instance, for a *conditional_expression*:
-
-- If *expr_cond* is a constant expression with value `true` then the state of *v* after *expr* is the same as the state of *v* after *expr_true*; permitting use after:
+## Unresolved questions
 
+- How identical these types should be?
+- Could we support variable declarations under `not` patterns?
+- Could we relax the scoping rules beyond pattern boundaries?
+ 	```cs
+	  if (e is (int x, 0) || a is (0, int x))
+	```
+- Could we relax the redeclaration requirement in a switch section? 
 	```cs
-	if (true ? x is int i : y is int i)
+	  case (int x, 0) a when Use(x, a): // ok
+	  case (0, int x) b when Use(x, b): // ok
+	     Use(x); // ok
+	     Use(a); // error; not definitely assigned
+	     Use(b); // error; not definitely assigned
+	     break;
 	```
-
-This document does not propose any changes to definite assignment rules for a *conditional_expression* to propagate conditional states when *cond_expr* is not a constant as it is covered by [improved definite assignment](https://github.com/dotnet/csharplang/blob/main/proposals/improved-definite-assignment.md#specification) proposal.