Some tweaks to not and or patterns

- Fix ambiguities in parser.mly

- Ensure that no new identifiers are bound in or-patterns and
  not-patterns, by adding a no_bindings switch to the
  environment. These patterns shouldn't generate any bogus flow typing
  constraints because we just pass through the original environment
  without adding any possible constraints (although this does mean we
  don't get any flow typing from negated numeric literals right now,
  which is a TODO).

- Reformat some code to match surrounding code.

- Add a typechecking test case for not patterns

- Add a typechecking test case for or patterns

At least at the front end everything should work now, but we need to
do a little bit more to rewrite these patterns away for lem etc.

1 files changed, 7 insertions, 5 deletions

diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 83264453..c6fb5308 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -66,6 +66,7 @@ type gpat =
   | GP_tup of gpat list
   | GP_list of gpat list
   | GP_cons of gpat * gpat
+  | GP_or of gpat * gpat
   | GP_app of (gpat Bindings.t)
   | GP_record of (gpat Bindings.t)
   | GP_string_append of gpat list
@@ -78,6 +79,7 @@ let rec string_of_gpat = function
   | GP_tup gpats -> "(" ^ Util.string_of_list ", " string_of_gpat gpats ^ ")"
   | GP_list gpats -> "[|" ^ Util.string_of_list ", " string_of_gpat gpats ^ "|]"
   | GP_cons (gpat1, gpat2) -> string_of_gpat gpat1 ^ " :: " ^ string_of_gpat gpat2
+  | GP_or (gpat1, gpat2) -> string_of_gpat gpat1 ^ " | " ^ string_of_gpat gpat2
   | GP_app app ->
      Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app)
   | GP_record _ -> "GP RECORD"
@@ -88,14 +90,11 @@ let is_wild = function
   | _ -> false
 
 let rec generalize ctx (P_aux (p_aux, _) as pat) =
-
   match p_aux with
   | P_lit lit -> GP_lit lit
   | P_wild -> GP_wild
-  (* todo: define GP_or/GP_not? or desugar at this stage?
-  | P_or(pat1, pat2) -> P_or(generalize ctx pat1, generalize ctx pat2)
-  | P_not(pat)       -> P_not(generalize ctx pat)
-  *)
+  | P_or (pat1, pat2) -> GP_or (generalize ctx pat1, generalize ctx pat2)
+  | P_not(pat)       -> GP_wild (* TODO: How to generalize negated patterns? *)
   | P_as (pat, _) -> generalize ctx pat
   | P_typ (_, pat) -> generalize ctx pat (* This will possibly overapproximate how general P_typ is *)
   | P_id id ->
@@ -256,6 +255,9 @@ let rec join ctx gpat1 gpat2 =
      else
        GP_app ctors
 
+  | GP_or (gpat1, gpat2), gpat3 -> join ctx (join ctx gpat1 gpat2) gpat3
+  | gpat1, GP_or (gpat2, gpat3) -> join ctx gpat1 (join ctx gpat2 gpat3)
+
   | _, _ -> GP_wild
 
 let combine ctx gpat (l, pat) =