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.

7 files changed, 43 insertions, 36 deletions

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 569f497d..9acb6052 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -549,8 +549,8 @@ let nexp_subst_fns substs =
     let re p = P_aux (p,(l,s_tannot annot)) in
     match p with
     | P_lit _ | P_wild | P_id _ -> re p
-    | P_or(p1, p2) -> re (P_or(s_pat p1, s_pat p2))
-    | P_not(p) -> re (P_not(s_pat p))
+    | P_or (p1, p2) -> re (P_or (s_pat p1, s_pat p2))
+    | P_not (p) -> re (P_not (s_pat p))
     | P_var (p',tpat) -> re (P_var (s_pat p',tpat))
     | P_as (p',id) -> re (P_as (s_pat p', id))
     | P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
@@ -645,8 +645,8 @@ let bindings_from_pat p =
     | P_lit _
     | P_wild
       -> []
-    | P_or(p1, p2) -> aux_pat p1 @ aux_pat p2
-    | P_not(p) -> aux_pat p
+    | P_or (p1, p2) -> aux_pat p1 @ aux_pat p2
+    | P_not (p) -> aux_pat p
     | P_as (p,id) -> id::(aux_pat p)
     | P_typ (_,p) -> aux_pat p
     | P_id id ->
@@ -987,13 +987,13 @@ let rec freshen_pat_bindings p =
     match p with
     | P_lit _
     | P_wild -> pat, []
-    | P_or(p1, p2) ->
+    | P_or (p1, p2) ->
        let (r1, vs1) = aux p1 in
        let (r2, vs2) = aux p2 in
-       (mkp (P_or(r1, r2)), vs1 @ vs2)
-    | P_not(p) ->
+       (mkp (P_or (r1, r2)), vs1 @ vs2)
+    | P_not p ->
        let (r, vs) = aux p in
-       (mkp (P_not(r)), vs)
+       (mkp (P_not r), vs)
     | P_as (p,_) -> aux p
     | P_typ (typ,p) -> let p',vs = aux p in mkp (P_typ (typ,p')),vs
     | P_id id -> let id' = freshen_id id in mkp (P_id id'),[id,E_aux (E_id id',(Generated Unknown,None))]
@@ -1772,12 +1772,12 @@ let split_defs all_errors splits defs =
         | P_lit _
         | P_wild
           -> None
-        | P_or(p1, p2) ->
+        | P_or (p1, p2) ->
            (* Todo: I am not proud of this abuse of relist - but creating a special
             * version of re just for two entries did not seem worth it
             *)
-           relist spl (fun [p1'; p2'] -> P_or(p1', p2')) [p1; p2]
-        | P_not(p) ->
+           relist spl (fun [p1'; p2'] -> P_or (p1', p2')) [p1; p2]
+        | P_not p ->
            (* todo: not sure that I can't split - but can't figure out how at
             * the moment *)
            raise (Reporting_basic.err_general l
@@ -2471,12 +2471,12 @@ let rec typ_pat_eq (TP_aux (tp1, _)) (TP_aux (tp2, _)) =
   | TP_app (f1, args1), TP_app (f2, args2) when List.length args1 = List.length args2 ->
      Id.compare f1 f2 = 0 && List.for_all2 typ_pat_eq args1 args2
   | _, _ -> false
-                                           
+
 let rec pat_eq (P_aux (p1,_)) (P_aux (p2,_)) =
   match p1, p2 with
   | P_lit lit1, P_lit lit2 -> lit_eq' lit1 lit2
   | P_wild, P_wild -> true
-  | P_or(p1, q1), P_or(p2, q2) ->
+  | P_or (p1, q1), P_or (p2, q2) ->
      (* ToDo: A case could be made for flattening trees of P_or nodes and
       * comparing the lists so that we treat P_or as associative
       *)
@@ -3287,11 +3287,11 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
       | P_lit _
       | P_wild
         -> ArgSplits.empty,Bindings.empty,KBindings.empty
-      | P_or(p1, p2) ->
+      | P_or (p1, p2) ->
          let (s1, v1, k1) = aux p1 in
          let (s2, v2, k2) = aux p2 in
          (ArgSplits.merge merge_detail s1 s2, dep_bindings_merge v1 v2, dep_kbindings_merge k1 k2)
-      | P_not(p) -> aux p
+      | P_not p -> aux p
       | P_as (pat,id) ->
          begin
            let s,v,k = aux pat in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 49878217..b5875ea7 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -242,7 +242,7 @@ type
 pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild                (* wildcard        - always matches *)
- | P_or  of ( pat * pat) (* choice pattern  - P|Q matches if P matches or Q matches *)
+ | P_or of pat * pat (* choice pattern  - P|Q matches if P matches or Q matches *)
  | P_typ of atyp * pat (* typed pattern *)
  | P_id of id (* identifier *)
  | P_var of pat * atyp (* bind pat to type variable *)
diff --git a/src/parser.mly b/src/parser.mly
index 2a05c013..694a4669 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -676,6 +676,8 @@ pat_string_append:
 pat1:
   | atomic_pat
     { $1 }
+  | atomic_pat Bar pat1
+    { mk_pat (P_or ($1, $3)) $startpos $endpos }
   | atomic_pat At pat_concat
     { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
   | atomic_pat ColonColon pat1
@@ -710,8 +712,6 @@ atomic_pat:
     { mk_pat (P_lit $1) $startpos $endpos }
   | id
     { mk_pat (P_id $1) $startpos $endpos }
-  | pat Bar pat
-    { mk_pat (P_or ($1, $3)) $startpos $endpos }
   | kid
     { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos,
 		     mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
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) =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 4df6fe75..9d9b4b4e 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -224,8 +224,8 @@ let doc_lit (L_aux(l,_)) =
 let rec doc_pat (P_aux (p_aux, _) as pat) =
   match p_aux with
   | P_id id -> doc_id id
-  | P_or(pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2)
-  | P_not(pat)       -> parens (doc_pat pat)
+  | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2)
+  | P_not pat -> string "~" ^^ parens (doc_pat pat)
   | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
   | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ]
   | P_lit lit -> doc_lit lit
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 1fa3bc67..f072f91f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -292,7 +292,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
     rewrap (P_vector ps)
   | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat
   | P_or(pat1, pat2) -> rewrap (P_or(rewrite pat1, rewrite pat2))
-  | P_not(pat)       -> rewrap (P_not(rewrite pat))
+  | P_not(pat) -> rewrap (P_not(rewrite pat))
   | P_as(pat,id) -> rewrap (P_as(rewrite pat, id))
   | P_typ(typ,pat) -> rewrap (P_typ(typ, rewrite pat))
   | P_app(id ,pats) -> rewrap (P_app(id, List.map rewrite pats))
diff --git a/src/type_check.ml b/src/type_check.ml
index 4aaf73bf..28e0f930 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -406,6 +406,9 @@ module Env : sig
   val have_smt_op : id -> t -> bool
   val allow_unknowns : t -> bool
   val set_allow_unknowns : bool -> t -> t
+
+  val no_bindings : t -> t
+
   (* Well formedness-checks *)
   val wf_typ : ?exs:KidSet.t -> t -> typ -> unit
   val wf_nexp : ?exs:KidSet.t -> t -> nexp -> unit
@@ -443,6 +446,7 @@ end = struct
       smt_ops : string Bindings.t;
       casts : id list;
       allow_casts : bool;
+      allow_bindings : bool;
       constraints : n_constraint list;
       default_order : order option;
       ret_typ : typ option;
@@ -470,6 +474,7 @@ end = struct
       externs = Bindings.empty;
       smt_ops = Bindings.empty;
       casts = [];
+      allow_bindings = true;
       allow_casts = true;
       constraints = [];
       default_order = None;
@@ -971,6 +976,7 @@ end = struct
 
   let add_local id mtyp env =
     begin
+      if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context" else ();
       wf_typ env (snd mtyp);
       if Bindings.mem id env.top_val_specs then
         typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
@@ -1099,6 +1105,8 @@ end = struct
   let no_casts env = { env with allow_casts = false }
   let enable_casts env = { env with allow_casts = true }
 
+  let no_bindings env = { env with allow_bindings = false }
+
   let add_cast cast env =
     typ_print (lazy ("Adding cast " ^ string_of_id cast));
     { env with casts = cast :: env.casts }
@@ -2618,16 +2626,13 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      let typed_pat, env, guards = bind_pat env pat typ in
      annot_pat (P_var (typed_pat, typ_pat)) typ, env, guards
   | P_wild -> annot_pat P_wild typ, env, []
-  | P_or(pat1, pat2) ->
-     let tpat1, env1, guards1 = bind_pat env pat1 typ in
-     let tpat2, env2, guards2 = bind_pat env pat2 typ in
-     (* todo: report error if env != env1 or env != env2 *)
-     (* todo: not sure I am doing the right thing with guards1 @ guards2 *)
-     (annot_pat (P_or(tpat1, tpat2)) typ, env, guards1 @ guards2)
-  | P_not(pat) ->
-     let tpat, env', guards = bind_pat env pat typ in
-     (* todo: report error if env != env' *)
-     (annot_pat (P_not(tpat)) typ, env, guards)
+  | P_or (pat1, pat2) ->
+     let tpat1, env1, guards1 = bind_pat (Env.no_bindings env) pat1 typ in
+     let tpat2, env2, guards2 = bind_pat (Env.no_bindings env) pat2 typ in
+     annot_pat (P_or (tpat1, tpat2)) typ, env, guards1 @ guards2
+  | P_not pat ->
+     let tpat, env', guards = bind_pat (Env.no_bindings env) pat typ in
+     annot_pat (P_not(tpat)) typ, env, guards
   | P_cons (hd_pat, tl_pat) ->
      begin
        match Env.expand_synonyms env typ with