Patterns: add or and not patterns

These match the new ASL pattern constructors:

- !p matches if the pattern p does not match
- { p1, ... pn } matches if any of the patterns p1 ... pn match

We desugar the set pattern "{p1, ... pn}" into "p1 | (p2 | ... pn)".

ASL does not have pattern binding but Sail does.  The rules at the
moment are that none of the pattern can contain patterns.  This could
be relaxed by allowing "p1 | p2" to bind variables provided p1 and p2
both bind the same variables.

12 files changed, 137 insertions, 7 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 3f5e92a1..781069eb 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -437,6 +437,8 @@ and map_pat_annot f (P_aux (pat, annot)) = P_aux (map_pat_annot_aux f pat, f ann
 and map_pat_annot_aux f = function
   | P_lit lit -> P_lit lit
   | P_wild -> P_wild
+  | P_or (pat1, pat2) -> P_or  (map_pat_annot f pat1, map_pat_annot f pat2)
+  | P_not pat         -> P_not (map_pat_annot f pat)
   | P_as (pat, id) -> P_as (map_pat_annot f pat, id)
   | P_typ (typ, pat) -> P_typ (typ, map_pat_annot f pat)
   | P_id id -> P_id id
@@ -733,6 +735,9 @@ and string_of_pat (P_aux (pat, l)) =
   match pat with
   | P_lit lit -> string_of_lit lit
   | P_wild -> "_"
+  | P_or (pat1, pat2) -> "(" ^ string_of_pat pat1 ^ " | " ^ string_of_pat pat2
+  ^ ")"
+  | P_not pat         -> "(!" ^ string_of_pat pat ^ ")"
   | P_id v -> string_of_id v
   | P_var (pat, tpat) -> string_of_pat pat ^ " as " ^ string_of_typ_pat tpat
   | P_typ (typ, pat) -> string_of_pat pat ^ " : " ^ string_of_typ typ
@@ -790,6 +795,8 @@ let rec pat_ids (P_aux (pat_aux, _)) =
   | P_lit _ | P_wild -> IdSet.empty
   | P_id id -> IdSet.singleton id
   | P_as (pat, id) -> IdSet.add id (pat_ids pat)
+  | P_or (pat1, pat2) -> IdSet.union (pat_ids pat1) (pat_ids pat2)
+  | P_not (pat)       -> pat_ids pat
   | P_var (pat, _) | P_typ (_, pat) -> pat_ids pat
   | P_app (_, pats) | P_tup pats | P_vector pats | P_vector_concat pats | P_list pats ->
      List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 60c22afc..bec9d847 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -133,6 +133,8 @@ let string_of_parse_id_aux = function
   | Parse_ast.Id v -> v
   | Parse_ast.DeIid v -> v
 
+let string_of_parse_id (Parse_ast.Id_aux(id, l)) = string_of_parse_id_aux id
+
 let string_contains str char =
   try (ignore (String.index str char); true) with
   | Not_found -> false
@@ -453,15 +455,18 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
     (match pat with
     | Parse_ast.P_lit(lit) -> P_lit(to_ast_lit lit)
     | Parse_ast.P_wild -> P_wild
+    | Parse_ast.P_or(pat1, pat2) ->
+       P_or (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2)
     | Parse_ast.P_var (pat, Parse_ast.ATyp_aux (Parse_ast.ATyp_id id, _)) ->
        P_as (to_ast_pat k_env def_ord pat, to_ast_id id)
     | Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
     | Parse_ast.P_id(id) -> P_id(to_ast_id id)
     | Parse_ast.P_var (pat, typ) -> P_var (to_ast_pat k_env def_ord pat, to_ast_typ_pat typ)
-    | Parse_ast.P_app(id,pats) ->
-      if pats = []
-      then P_id (to_ast_id id)
-      else P_app(to_ast_id id, List.map (to_ast_pat k_env def_ord) pats)
+    | Parse_ast.P_app(id, []) -> P_id (to_ast_id id)
+    | Parse_ast.P_app(id, pats) ->
+       if List.length pats == 1 && string_of_parse_id id = "~"
+       then P_not (to_ast_pat k_env def_ord (List.hd pats))
+       else P_app(to_ast_id id, List.map (to_ast_pat k_env def_ord) pats)
     | Parse_ast.P_record(fpats,_) ->
       P_record(List.map
                  (fun (Parse_ast.FP_aux(Parse_ast.FP_Fpat(id,fp),l)) ->
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 99d5889a..e4f7faf0 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -593,6 +593,15 @@ and pattern_match env (P_aux (p_aux, _) as pat) value =
   match p_aux with
   | P_lit lit -> eq_value (value_of_lit lit) value, Bindings.empty
   | P_wild -> true, Bindings.empty
+  | P_or(pat1, pat2) ->
+     let (m1, b1) = pattern_match env pat1 value in
+     let (m2, b2) = pattern_match env pat2 value in
+     (* todo: maybe add assertion that bindings are consistent or empty? *)
+     (m1 || m2, Bindings.merge combine b1 b2)
+  | P_not(pat) ->
+     let (m, b) = pattern_match env pat value in
+     (* todo: maybe add assertion that binding is empty *)
+     (not m, b)
   | P_as (pat, id) ->
      let matched, bindings = pattern_match env pat value in
      matched, Bindings.add id value bindings
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d7a0c878..569f497d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -549,6 +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_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'))
@@ -643,6 +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_as (p,id) -> id::(aux_pat p)
     | P_typ (_,p) -> aux_pat p
     | P_id id ->
@@ -983,6 +987,13 @@ let rec freshen_pat_bindings p =
     match p with
     | P_lit _
     | P_wild -> pat, []
+    | 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) ->
+       let (r, vs) = aux p in
+       (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))]
@@ -1761,6 +1772,16 @@ let split_defs all_errors splits defs =
         | P_lit _
         | P_wild
           -> None
+        | 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) ->
+           (* todo: not sure that I can't split - but can't figure out how at
+            * the moment *)
+           raise (Reporting_basic.err_general l
+                    ("Cannot split on 'not' pattern"))
         | P_as (p',id) when id_match id <> None ->
            raise (Reporting_basic.err_general l
                     ("Cannot split " ^ string_of_id id ^ " on 'as' pattern"))
@@ -2455,6 +2476,12 @@ 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) ->
+     (* 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
+      *)
+     pat_eq p1 p2 && pat_eq q1 q2
+  | P_not(p1), P_not(p2) -> pat_eq p1 p2
   | P_as (p1',id1), P_as (p2',id2) -> Id.compare id1 id2 == 0 && pat_eq p1' p2'
   | P_typ (_,p1'), P_typ (_,p2') -> pat_eq p1' p2'
   | P_id id1, P_id id2 -> Id.compare id1 id2 == 0
@@ -3260,6 +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) ->
+         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_as (pat,id) ->
          begin
            let s,v,k = aux pat in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 26cb9df7..49878217 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -241,7 +241,8 @@ typschm =
 type 
 pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
- | P_wild (* wildcard *)
+ | P_wild                (* wildcard        - always 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 0637d61a..2a05c013 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -710,6 +710,8 @@ 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 acd925bf..83264453 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -92,6 +92,10 @@ 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_as (pat, _) -> generalize ctx pat
   | P_typ (_, pat) -> generalize ctx pat (* This will possibly overapproximate how general P_typ is *)
   | P_id id ->
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f3556343..4df6fe75 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -224,6 +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_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 1fb89dee..1fa3bc67 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -291,6 +291,8 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
         (vector_string_to_bit_list l lit) in
     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_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))
@@ -440,6 +442,8 @@ and introduced_vars_le (LEXP_aux(lexp,annot)) exp =
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   { p_lit            : lit -> 'pat_aux
   ; p_wild           : 'pat_aux
+  ; p_or             : 'pat * 'pat -> 'pat_aux
+  ; p_not            : 'pat        -> 'pat_aux
   ; p_as             : 'pat * id -> 'pat_aux
   ; p_typ            : Ast.typ * 'pat -> 'pat_aux
   ; p_id             : id -> 'pat_aux
@@ -461,6 +465,8 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
   function
   | P_lit lit           -> alg.p_lit lit
   | P_wild              -> alg.p_wild
+  | P_or(p1, p2)        -> alg.p_or (fold_pat alg p1, fold_pat alg p2)
+  | P_not(p)            -> alg.p_not (fold_pat alg p)
   | P_id id             -> alg.p_id id
   | P_var (p,tpat)      -> alg.p_var (fold_pat alg p, tpat)
   | P_as (p,id)         -> alg.p_as (fold_pat alg p, id)
@@ -488,6 +494,8 @@ and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'f
 let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   { p_lit            = (fun lit -> P_lit lit)
   ; p_wild           = P_wild
+  ; p_or             = (fun (pat1, pat2) -> P_or(pat1, pat2))
+  ; p_not            = (fun pat -> P_not(pat))
   ; p_as             = (fun (pat,id) -> P_as (pat,id))
   ; p_typ            = (fun (typ,pat) -> P_typ (typ,pat))
   ; p_id             = (fun id -> P_id id)
@@ -721,6 +729,9 @@ let compute_pat_alg bot join =
   let split_join f ps = let (vs,ps) = List.split ps in (join_list vs, f ps) in
   { p_lit            = (fun lit -> (bot, P_lit lit))
   ; p_wild           = (bot, P_wild)
+  (* todo: I have no idea how to combine v1 and v2 in the following *)
+  ; p_or             = (fun ((v1, pat1), (v2, pat2)) -> (v1, P_or(pat1, pat2)))
+  ; p_not            = (fun (v, pat) -> (v, P_not(pat)))
   ; p_as             = (fun ((v,pat),id) -> (v, P_as (pat,id)))
   ; p_typ            = (fun (typ,(v,pat)) -> (v, P_typ (typ,pat)))
   ; p_id             = (fun id -> (bot, P_id id))
@@ -823,6 +834,8 @@ let pure_pat_alg bot join =
   let join_list vs = List.fold_left join bot vs in
   { p_lit            = (fun lit -> bot)
   ; p_wild           = bot
+  ; p_or             = (fun (pat1, pat2) -> bot) (* todo: this is wrong *)
+  ; p_not            = (fun pat -> bot)          (* todo: this is wrong *)
   ; p_as             = (fun (v,id) -> v)
   ; p_typ            = (fun (typ,v) -> v)
   ; p_id             = (fun id -> bot)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index eed22376..3e582071 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -84,6 +84,8 @@ val rewrite_fun : tannot rewriters -> tannot fundef -> tannot fundef
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
   { p_lit            : lit -> 'pat_aux
   ; p_wild           : 'pat_aux
+  ; p_or             : 'pat * 'pat -> 'pat_aux
+  ; p_not            : 'pat        -> 'pat_aux
   ; p_as             : 'pat * id -> 'pat_aux
   ; p_typ            : Ast.typ * 'pat -> 'pat_aux
   ; p_id             : id -> 'pat_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c7e53e88..2729e7cd 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -675,7 +675,13 @@ let remove_vector_concat_pat pat =
     { p_lit = (fun lit -> P_lit lit)
     ; p_typ = (fun (typ,p) -> P_typ (typ,p false)) (* cannot happen *)
     ; p_wild = P_wild
-    ; p_as = (fun (pat,id) -> P_as (pat true,id))
+      (* ToDo: I have no idea what the boolean parameter means so guessed that
+       * "true" was a good value to use.
+       * (Adding a comment explaining the boolean might be useful?)
+       *)
+    ; p_or  = (fun (pat1, pat2) -> P_or (pat1 true, pat2 true))
+    ; p_not = (fun pat -> P_not (pat true))
+    ; p_as  = (fun (pat,id) -> P_as (pat true,id))
     ; p_id  = (fun id -> P_id id)
     ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
@@ -817,6 +823,8 @@ let remove_vector_concat_pat pat =
 
     { p_lit            = (fun lit -> (P_lit lit,[]))
     ; p_wild           = (P_wild,[])
+    ; p_or             = (fun ((pat1, ds1), (pat2, ds2)) -> (P_or(pat1, pat2), ds1 @ ds2))
+    ; p_not            = (fun (pat, ds) -> (P_not(pat), ds))
     ; p_as             = (fun ((pat,decls),id) -> (P_as (pat,id),decls))
     ; p_typ            = (fun (typ,(pat,decls)) -> (P_typ (typ,pat),decls))
     ; p_id             = (fun id -> (P_id id,[]))
@@ -1007,6 +1015,8 @@ let rec is_irrefutable_pattern (P_aux (p,ann)) =
   | P_lit (L_aux (L_unit,_))
   | P_wild
     -> true
+  | P_or(pat1, pat2) -> is_irrefutable_pattern pat1 && is_irrefutable_pattern pat2
+  | P_not(pat) -> is_irrefutable_pattern pat
   | P_lit _ -> false
   | P_as (p1,_)
   | P_typ (_,p1)
@@ -1056,6 +1066,10 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   match p1, p2 with
   | P_lit (L_aux (lit1,_)), P_lit (L_aux (lit2,_)) ->
       if lit1 = lit2 then Some [] else None
+  | P_or(pat1, pat2), _ -> (* todo: possibly not the right answer *) None
+  | _, P_or(pat1, pat2) -> (* todo: possibly not the right answer *) None
+  | P_not(pat), _ -> (* todo: possibly not the right answer *) None
+  | _, P_not(pat) -> (* todo: possibly not the right answer *) None
   | P_as (pat1,_), _ -> subsumes_pat pat1 pat2
   | _, P_as (pat2,_) -> subsumes_pat pat1 pat2
   | P_typ (_,pat1), _ -> subsumes_pat pat1 pat2
@@ -1130,6 +1144,8 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
   | P_lit lit -> rewrap (E_lit lit)
   | P_wild -> raise (Reporting_basic.err_unreachable l
       "pat_to_exp given wildcard pattern")
+  | P_or(pat1, pat2) -> (* todo: insert boolean or *) pat_to_exp pat1 
+  | P_not(pat) -> (* todo: insert boolean not *) pat_to_exp pat
   | P_as (pat,id) -> rewrap (E_id id)
   | P_var (pat, _) -> pat_to_exp pat
   | P_typ (_,pat) -> pat_to_exp pat
@@ -1259,6 +1275,8 @@ let compose_guard_opt g1 g2 = match g1, g2 with
 let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
 | P_lit _ | P_wild | P_id _ -> false
 | P_as (pat,_) | P_typ (_,pat) | P_var (pat,_) -> contains_bitvector_pat pat
+| P_or(pat1, pat2) -> contains_bitvector_pat pat1 || contains_bitvector_pat pat2
+| P_not(pat) -> contains_bitvector_pat pat
 | P_vector _ | P_vector_concat _ ->
     let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
     is_bitvector_typ typ
@@ -1284,7 +1302,12 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
     { p_lit = (fun lit -> P_lit lit)
     ; p_typ = (fun (typ,p) -> P_typ (typ,p false))
     ; p_wild = P_wild
-    ; p_as = (fun (pat,id) -> P_as (pat true,id))
+    (* todo: I have no idea what the boolean parameter means - so I randomly
+     * passed "true".  A comment to explain the bool might be a good idea?
+     *)
+    ; p_or  = (fun (pat1, pat2) -> P_or (pat1 true, pat2 true))
+    ; p_not = (fun pat -> P_not (pat true))
+    ; p_as  = (fun (pat,id) -> P_as (pat true,id))
     ; p_id  = (fun id -> P_id id)
     ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
     ; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
@@ -1431,6 +1454,9 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
 
     { p_lit            = (fun lit -> (P_lit lit, (None, (fun b -> b), [])))
     ; p_wild           = (P_wild, (None, (fun b -> b), []))
+    ; p_or             = (fun ((pat1, gdl1), (pat2, gdl2)) ->
+                              (P_or(pat1, pat2), flatten_guards_decls [gdl1; gdl2]))
+    ; p_not            = (fun (pat, gdl) -> (P_not(pat), gdl))
     ; p_as             = (fun ((pat,gdls),id) -> (P_as (pat,id), gdls))
     ; p_typ            = (fun (typ,(pat,gdls)) -> (P_typ (typ,pat), gdls))
     ; p_id             = (fun id -> (P_id id, (None, (fun b -> b), [])))
@@ -3118,6 +3144,16 @@ let rec rewrite_defs_pat_string_append =
     | P_aux (P_string_append _, _) ->
        failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat pat)
 
+    | P_aux (P_or(pat1, pat2), p_annot) ->
+       (* todo: this is wrong - no idea what is happening here *)
+       let (pat1', guards1, expr1) = rewrite_pat env (pat1, guards, expr) in
+       let (pat2', guards2, expr2) = rewrite_pat env (pat2, guards, expr) in
+       (P_aux (P_or(pat1', pat2'), p_annot), guards1 @ guards2, expr2)
+
+    | P_aux (P_not(pat), p_annot) ->
+       let (pat', guards, expr) = rewrite_pat env (pat, guards, expr) in
+       (P_aux (P_not(pat'), p_annot), guards, expr)
+
     | P_aux (P_as (inner_pat, inner_id), p_annot) ->
        let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in
        P_aux (P_as (inner_pat, inner_id), p_annot), guards, expr
diff --git a/src/type_check.ml b/src/type_check.ml
index dbd01c56..4aaf73bf 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2618,6 +2618,16 @@ 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_cons (hd_pat, tl_pat) ->
      begin
        match Env.expand_synonyms env typ with
@@ -3979,6 +3989,13 @@ and propagate_pat_effect (P_aux (pat, annot)) =
 and propagate_pat_effect_aux = function
   | P_lit lit -> P_lit lit, no_effect
   | P_wild -> P_wild, no_effect
+  | P_or(pat1, pat2) ->
+     let pat1' = propagate_pat_effect pat1 in
+     let pat2' = propagate_pat_effect pat2 in
+     (P_or (pat1', pat2'), union_effects (effect_of_pat pat1') (effect_of_pat pat2'))
+  | P_not(pat) ->
+     let pat' = propagate_pat_effect pat in
+     (P_not(pat'), effect_of_pat pat')
   | P_cons (pat1, pat2) ->
      let p_pat1 = propagate_pat_effect pat1 in
      let p_pat2 = propagate_pat_effect pat2 in