WIP

Author: trdthg

language/sail.ott

@@ -558,7 +558,9 @@ pexp :: 'Pat_' ::=
   {{ com pattern match }}
   {{ aux _ annot }} {{ auxparam 'a }}
   | pat => exp                        :: :: exp
+  | pat1 ... patn => exp              :: :: or
   | pat if exp1 => exp                :: :: when
+
 % apparently could use -> or => for this.
 
 %% % psexp :: 'Pats' ::=

src/lib/ast_util.ml

@@ -1295,6 +1295,9 @@ and string_of_fexp (FE_aux (FE_fexp (field, exp), _)) = string_of_id field ^ " =
 and string_of_pexp (Pat_aux (pexp, _)) =
   match pexp with
   | Pat_exp (pat, exp) -> string_of_pat pat ^ " => " ^ string_of_exp exp
+  | Pat_or (pats, exp) ->
+      let pat_strings = List.map (fun pat -> string_of_pat pat) pats in
+      String.concat ", " pat_strings ^ " => " ^ string_of_exp exp
   | Pat_when (pat, guard, exp) -> string_of_pat pat ^ " if " ^ string_of_exp guard ^ " => " ^ string_of_exp exp
 
 and string_of_typ_pat (TP_aux (tpat_aux, _)) =
@@ -1804,6 +1807,7 @@ and subst_pexp id value (Pat_aux (pexp_aux, annot)) =
     match pexp_aux with
     | Pat_exp (pat, exp) when IdSet.mem id (pat_ids pat) -> Pat_exp (pat, exp)
     | Pat_exp (pat, exp) -> Pat_exp (pat, subst id value exp)
+    | Pat_or (pats, exp) -> Pat_or (pats, subst id value exp)
     | Pat_when (pat, guard, exp) when IdSet.mem id (pat_ids pat) -> Pat_when (pat, guard, exp)
     | Pat_when (pat, guard, exp) -> Pat_when (pat, subst id value guard, subst id value exp)
   in
@@ -2296,6 +2300,7 @@ struct
     else (
       match aux with
       | Pat_exp (pat, exp) -> option_chain (find_annot_pat sl pat) (find_annot_exp sl exp)
+      | Pat_or (pats, exp) -> option_chain (find_annot_pat sl (List.hd pats)) (find_annot_exp sl exp)
       | Pat_when (pat, guard, exp) -> option_chain (find_annot_pat sl pat) (option_mapm (find_annot_exp sl) [guard; exp])
     )
 

src/lib/chunk_ast.ml

@@ -746,6 +746,7 @@ let is_aligned pexps =
   let rec pexp_exp_column = function
     | Pat_aux (Pat_attribute (_, _, pexp), _) -> pexp_exp_column pexp
     | Pat_aux (Pat_exp (_, E_aux (_, l)), _) -> starting_column_num l
+    | Pat_aux (Pat_or (_, E_aux (_, l)), _) -> starting_column_num l
     | Pat_aux (Pat_when (_, _, E_aux (_, l)), _) -> starting_column_num l
   in
   List.fold_left
@@ -1068,6 +1069,7 @@ and chunk_pexp ?delim comments chunks (Pat_aux (aux, l)) =
       (match delim with Some d -> Queue.add (Delim d) exp_chunks | _ -> ());
       ignore (pop_trailing_comment comments exp_chunks (ending_line_num l));
       { funcl_space; pat = pat_chunks; guard = None; body = exp_chunks }
+  | Pat_or (pats, exp) -> raise (Reporting.err_unreachable l __POS__ "Pattern or is not supported in this context")
   | Pat_when (pat, guard, exp) ->
       let pat_chunks = Queue.create () in
       chunk_pat comments pat_chunks pat;

src/lib/initial_check.ml

@@ -716,6 +716,9 @@ module KindInference = struct
     | P.Pat_exp (pat, exp) ->
         let* pat = infer_pat ctx pat in
         wrap (P.Pat_exp (pat, exp))
+    | P.Pat_or (pats, exp) ->
+        let* pats = mapM (infer_pat ctx) pats in
+        wrap (P.Pat_or (pats, exp))
     | P.Pat_when (pat, guard, exp) ->
         let* pat = infer_pat ctx pat in
         wrap (P.Pat_when (pat, guard, exp))
@@ -1304,7 +1307,7 @@ and to_ast_exp ctx exp =
             | _ -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none")
           )
         | P.E_field (exp, id) -> E_field (to_ast_exp ctx exp, to_ast_id ctx id)
-        | P.E_match (exp, pexps) -> E_match (to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps)
+        | P.E_match (exp, pexps) -> E_match (to_ast_exp ctx exp, List.mapi (to_ast_match_case_i ctx) pexps)
         | P.E_try (exp, pexps) -> E_try (to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps)
         | P.E_let (leb, exp) -> E_let (to_ast_letbind ctx leb, to_ast_exp ctx exp)
         | P.E_assign (lexp, exp) -> E_assign (to_ast_lexp ctx lexp, to_ast_exp ctx exp)
@@ -1391,9 +1394,27 @@ and to_ast_case ctx (P.Pat_aux (pexp_aux, l) : P.pexp) : uannot pexp =
       let annot = add_attribute l attr arg annot in
       Pat_aux (pexp, (pexp_l, annot))
   | P.Pat_exp (pat, exp) -> Pat_aux (Pat_exp (to_ast_pat ctx pat, to_ast_exp ctx exp), (l, empty_uannot))
+  | P.Pat_or (pats, exp) -> raise (Reporting.err_typ l "Only Match supports pat_list")
   | P.Pat_when (pat, guard, exp) ->
       Pat_aux (Pat_when (to_ast_pat ctx pat, to_ast_exp ctx guard, to_ast_exp ctx exp), (l, empty_uannot))
 
+and to_ast_match_case_i ctx i ((P.Pat_aux (pexp_aux, l) : P.pexp) as pat) : uannot pexp =
+  match pexp_aux with
+  | P.Pat_or (pats, exp) ->
+      let id = mk_id ("p#" ^ string_of_int i) in
+      let p = mk_pat (P_id id) in
+      let guard =
+        mk_exp
+          (E_match
+             ( mk_exp (E_id id),
+               List.mapi (fun i p -> mk_pexp (Pat_exp (to_ast_pat ctx p, mk_exp (E_lit (mk_lit L_true))))) pats
+               @ [mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_lit (mk_lit L_false))))]
+             )
+          )
+      in
+      Pat_aux (Pat_when (p, guard, to_ast_exp ctx exp), (l, empty_uannot))
+  | _ -> to_ast_case ctx pat
+
 and to_ast_fexps (fail_on_error : bool) ctx (exps : P.exp list) : uannot fexp list option =
   match exps with
   | [] -> Some []

src/lib/lint.ml

@@ -51,6 +51,7 @@ open Ast_util
 let scan_exp_in_pexp f (Pat_aux (aux, _)) =
   match aux with
   | Pat_exp (_, exp) -> f exp
+  | Pat_or (_, exp) -> f exp
   | Pat_when (_, guard, exp) ->
       f guard;
       f exp

src/lib/parse_ast.ml

@@ -260,6 +260,7 @@ and opt_default = Def_val_aux of opt_default_aux * l
 and pexp_aux =
   (* Pattern match *)
   | Pat_exp of pat * exp
+  | Pat_or of pat list * exp
   | Pat_when of pat * exp * exp
   | Pat_attribute of string * attribute_data option * pexp
 

src/lib/parser.mly

@@ -724,6 +724,8 @@ exp0:
 case:
   | p = pat; EqGt; body = exp
     { mk_pexp (Pat_exp (p, body)) $startpos $endpos }
+  | ps = pat_list; EqGt; body = exp
+    { mk_pexp (Pat_or (ps, body)) $startpos $endpos }
   | p = pat; If_; guard = exp; EqGt; body = exp
     { mk_pexp (Pat_when (p, guard, body)) $startpos $endpos }
   | a = attribute; Lparen; c = case; Rparen

src/lib/pattern_completeness.ml

@@ -944,6 +944,7 @@ module Make (C : Config) = struct
         )
     (* We also don't consider guarded cases *)
     | Pat_aux (Pat_when _, _) :: cases -> cases_to_pats ctx from ~have_guard:true ~have_mapping cases
+    | Pat_aux (Pat_or _, _) :: cases -> cases_to_pats ctx from ~have_guard:true ~have_mapping cases
 
   let rec update_cases l new_pats cases =
     match (new_pats, cases) with

src/lib/rewriter.ml

@@ -151,6 +151,8 @@ let rewrite_pexp rewriters =
   let rewrite = rewriters.rewrite_exp rewriters in
   function
   | Pat_aux (Pat_exp (p, e), pannot) -> Pat_aux (Pat_exp (rewriters.rewrite_pat rewriters p, rewrite e), pannot)
+  | Pat_aux (Pat_or (ps, e), pannot) ->
+      Pat_aux (Pat_or (List.map (rewriters.rewrite_pat rewriters) ps, rewrite e), pannot)
   | Pat_aux (Pat_when (p, e, e'), pannot) ->
       Pat_aux (Pat_when (rewriters.rewrite_pat rewriters p, rewrite e, rewrite e'), pannot)
 
@@ -603,6 +605,18 @@ and fold_fexp alg (FE_aux (fexp_aux, annot)) = alg.fe_aux (fold_fexp_aux alg fex
 
 and fold_pexp_aux alg = function
   | Pat_exp (pat, e) -> alg.pat_exp (fold_pat alg.pat_alg pat, fold_exp alg e)
+  | Pat_or (pats, e) ->
+      let id = mk_id "p" in
+      let guard =
+        mk_exp
+          (E_match
+             ( mk_exp (E_id id),
+               List.mapi (fun i p -> mk_pexp (Pat_exp (p, mk_exp (E_lit (mk_lit L_true))))) pats
+               @ [mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_lit (mk_lit L_false))))]
+             )
+          )
+      in
+      alg.pat_when (mk_pat (P_id id), guard, fold_exp alg e)
   | Pat_when (pat, e, e') -> alg.pat_when (fold_pat alg.pat_alg pat, fold_exp alg e, fold_exp alg e')
 
 and fold_pexp alg (Pat_aux (pexp_aux, annot)) = alg.pat_aux (fold_pexp_aux alg pexp_aux, annot)
@@ -923,6 +937,9 @@ let default_fold_pexp f x (Pat_aux (pe, ann)) =
     | Pat_exp (p, e) ->
         let x, e = f x e in
         (x, Pat_exp (p, e))
+    | Pat_or (ps, e) ->
+        let x, e = f x e in
+        (x, Pat_or (ps, e))
     | Pat_when (p, e1, e2) ->
         let x, e1 = f x e1 in
         let x, e2 = f x e2 in

src/lib/rewrites.ml

@@ -627,6 +627,10 @@ let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp, (l, annot)) as f
         | Pat_aux (Pat_exp (pat, body), annot') ->
             let pat, _, decls = remove_vector_concat_pat pat in
             Pat_aux (Pat_exp (pat, decls (rewrite_rec body)), annot')
+        | Pat_aux (Pat_or (pats, body), annot') ->
+            raise (Reporting.err_unreachable l __POS__ "Pat_or should have been rewritten away")
+            (* let pat, _, decls = remove_vector_concat_pat pat in
+               Pat_aux (Pat_exp (pat, decls (rewrite_rec body)), annot') *)
         | Pat_aux (Pat_when (pat, guard, body), annot') ->
             let pat, _, decls = remove_vector_concat_pat pat in
             Pat_aux (Pat_when (pat, decls (rewrite_rec guard), decls (rewrite_rec body)), annot')
@@ -1053,7 +1057,8 @@ let rec contains_bitvector_pat (P_aux (pat, annot)) =
 
 let contains_bitvector_pexp = function
   | Pat_aux (Pat_exp (pat, _), _) | Pat_aux (Pat_when (pat, _, _), _) -> contains_bitvector_pat pat
-
+  | Pat_aux (Pat_or (pats, body), annot') ->
+      raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Pat_or should have been rewritten away")
 (* Rewrite bitvector patterns to guarded patterns *)
 
 let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
@@ -1284,6 +1289,8 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp, (l, annot)) as full_
             | Some guard' -> Pat_aux (Pat_when (pat', guard', body'), annot')
             | None -> Pat_aux (Pat_exp (pat', body'), annot')
           )
+        | Pat_aux (Pat_or (pats, body), annot') ->
+            raise (Reporting.err_unreachable l __POS__ "Pat_or should have been rewritten away")
         | Pat_aux (Pat_when (pat, guard, body), annot') -> (
             let pat', (guard', decls, _) = remove_bitvector_pat pat in
             let guard'' = rewrite_rec guard in
@@ -1440,6 +1447,9 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp, (l, annot)) as full_exp) =
       in
       let clause = function
         | Pat_aux (Pat_exp (pat, body), annot) -> (pat, None, rewrite_rec body, annot)
+        | Pat_aux (Pat_or (pat, body), annot) ->
+            (* TODO *)
+            raise (Reporting.err_unreachable l __POS__ "Pat_or should have been rewritten away")
         | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot)
       in
       let clauses =
@@ -1460,6 +1470,8 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp, (l, annot)) as full_exp) =
       let e = rewrite_rec e in
       let clause = function
         | Pat_aux (Pat_exp (pat, body), annot) -> (pat, None, rewrite_rec body, annot)
+        | Pat_aux (Pat_or (pats, body), annot') ->
+            raise (Reporting.err_unreachable l __POS__ "Pat_or should have been rewritten away")
         | Pat_aux (Pat_when (pat, guard, body), annot) -> (pat, Some (rewrite_rec guard), rewrite_rec body, annot)
       in
       let clauses =
@@ -1647,15 +1659,19 @@ let rewrite_ast_early_return effect_info env ast =
   in
 
   let e_case (e, pes) =
-    let is_return_pexp (Pat_aux (pexp, _)) = match pexp with Pat_exp (_, e) | Pat_when (_, _, e) -> is_return e in
+    let is_return_pexp (Pat_aux (pexp, _)) =
+      match pexp with Pat_exp (_, e) | Pat_or (_, e) | Pat_when (_, _, e) -> is_return e
+    in
     let get_return_pexp (Pat_aux (pexp, a)) =
       match pexp with
       | Pat_exp (p, e) -> Pat_aux (Pat_exp (p, get_return e), a)
+      | Pat_or (ps, e) -> Pat_aux (Pat_or (ps, get_return e), a)
       | Pat_when (p, g, e) -> Pat_aux (Pat_when (p, g, get_return e), a)
     in
     let annot =
       match List.map get_return_pexp pes with
       | Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
+      | Pat_aux (Pat_or (_, E_aux (_, annot)), _) :: _ -> annot
       | Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
       | [] -> (Parse_ast.Unknown, empty_tannot)
     in
@@ -1705,6 +1721,7 @@ let rewrite_ast_early_return effect_info env ast =
     | E_match (e, pes) ->
         let add_final_return_pexp = function
           | Pat_aux (Pat_exp (p, e), a) -> Pat_aux (Pat_exp (p, add_final_return true e), a)
+          | Pat_aux (Pat_or (p, e), a) -> Pat_aux (Pat_or (p, add_final_return true e), a)
           | Pat_aux (Pat_when (p, g, e), a) -> Pat_aux (Pat_when (p, g, add_final_return true e), a)
         in
         rewrap (E_match (e, List.map add_final_return_pexp pes))
@@ -1953,6 +1970,8 @@ let rewrite_split_fun_ctor_pats fun_name effect_info env ast =
                                match pexp with
                                | Pat_exp (pat, exp) ->
                                    FCL_aux (FCL_funcl (id, Pat_aux (Pat_exp (pat, optimize_exp exp), pann)), fannot)
+                               | Pat_or (pats, exp) ->
+                                   FCL_aux (FCL_funcl (id, Pat_aux (Pat_or (pats, optimize_exp exp), pann)), fannot)
                                | Pat_when (pat, guard, exp) ->
                                    FCL_aux
                                      ( FCL_funcl
@@ -2273,6 +2292,7 @@ let rewrite_ast_letbind_effects effect_info env =
    fun newreturn pexp k ->
     match pexp with
     | Pat_aux (Pat_exp (pat, exp), annot) -> k (Pat_aux (Pat_exp (pat, n_exp_term newreturn exp), annot))
+    | Pat_aux (Pat_or (pats, exp), annot) -> k (Pat_aux (Pat_or (pats, n_exp_term newreturn exp), annot))
     | Pat_aux (Pat_when (pat, guard, exp), annot) ->
         k (Pat_aux (Pat_when (pat, n_exp_term newreturn guard, n_exp_term newreturn exp), annot))
   and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp =
@@ -2579,6 +2599,9 @@ let rewrite_ast_pat_lits rewrite_lit env ast =
                 annot
               )
       end
+    | Pat_or (pats, exp) ->
+        (* TODO *)
+        raise (Reporting.err_todo Parse_ast.Unknown "Pat_or should have been rewritten away")
     | Pat_when (pat, guard, exp) -> begin
         let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
         let guard_annot = (fst annot, mk_tannot (env_of exp) bool_typ) in
@@ -2818,7 +2841,8 @@ let rec rewrite_var_updates (E_aux (expaux, ((l, _) as annot)) as exp) =
         let is_case = match expaux with E_match _ -> true | _ -> false in
         let vars, varpats =
           (* for E_match, e1 needs no rewriting after rewrite_ast_letbind_effects *)
-          (if is_case then [] else [e1]) @ List.map (fun (Pat_aux ((Pat_exp (_, e) | Pat_when (_, _, e)), _)) -> e) ps
+          (if is_case then [] else [e1])
+          @ List.map (fun (Pat_aux ((Pat_exp (_, e) | Pat_or (_, e) | Pat_when (_, _, e)), _)) -> e) ps
           |> List.map find_updated_vars |> List.fold_left IdSet.union IdSet.empty |> IdSet.inter used_vars
           |> mk_var_exps_pats pl env
         in
@@ -2828,6 +2852,7 @@ let rec rewrite_var_updates (E_aux (expaux, ((l, _) as annot)) as exp) =
             List.map
               (function
                 | Pat_aux (Pat_exp (p, e), a) -> Pat_aux (Pat_exp (p, rewrite_var_updates e), a)
+                | Pat_aux (Pat_or (p, e), a) -> Pat_aux (Pat_or (p, rewrite_var_updates e), a)
                 | Pat_aux (Pat_when (p, g, e), a) -> Pat_aux (Pat_when (p, g, rewrite_var_updates e), a)
                 )
               ps
@@ -2842,7 +2867,7 @@ let rec rewrite_var_updates (E_aux (expaux, ((l, _) as annot)) as exp) =
                 let exp = rewrite_var_updates (add_vars overwrite exp vars) in
                 let pannot = (l, mk_tannot (env_of exp) (typ_of exp)) in
                 Pat_aux (Pat_exp (pat, exp), pannot)
-            | Pat_when _ ->
+            | Pat_or _ | Pat_when _ ->
                 raise (Reporting.err_unreachable l __POS__ "Guarded patterns should have been rewritten already")
           in
           let ps = List.map rewrite_pexp ps in
@@ -3057,6 +3082,10 @@ let rewrite_ast_not_pats env =
     in
     match pexp_aux with
     | Pat_exp (pat, exp) -> rewrite_pexp' pat exp None
+    | Pat_or (pats, exp) ->
+        (* TODO *)
+        raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Pat_or should have been rewritten away")
+        (* rewrite_pexp' pats exp None *)
     | Pat_when (pat, guard, exp) -> rewrite_pexp' pat exp (Some (strip_exp guard))
   in
   let rw_exp = { id_exp_alg with pat_aux = rewrite_pexp } in
@@ -3222,6 +3251,7 @@ let rewrite_ast_realize_mappings effect_info env ast =
   in
   let true_pexp = function
     | Pat_aux (Pat_exp (pat, _), annot) -> Pat_aux (Pat_exp (pat, mk_lit_exp L_true), annot)
+    | Pat_aux (Pat_or (pats, _), annot) -> Pat_aux (Pat_or (pats, mk_lit_exp L_true), annot)
     | Pat_aux (Pat_when (pat, guard, _), annot) -> Pat_aux (Pat_when (pat, guard, mk_lit_exp L_true), annot)
   in
   let annotate_pat ~last = function
@@ -3679,7 +3709,7 @@ module MakeExhaustive = struct
       | Pat_aux (Pat_exp (p, _), _) ->
           let rps, progress = List.split (List.map (remove_clause_from_pattern ctx p) rps) in
           (List.concat rps, List.exists (fun b -> b) progress)
-      | Pat_aux (Pat_when _, (l, _)) ->
+      | Pat_aux (Pat_or _, (l, _)) | Pat_aux (Pat_when _, (l, _)) ->
           raise (Reporting.err_unreachable l __POS__ "Guarded pattern should have been rewritten away")
 
   let check_cases process is_wild loc_of cases =
@@ -3701,13 +3731,22 @@ module MakeExhaustive = struct
 
   let not_enum env id = match Env.lookup_id id env with Enum _ -> false | _ -> true
 
+  let paux_is_wild = function
+    | P_aux (P_wild, _) -> true
+    | P_aux (P_id id, ann) when not_enum (env_of_annot ann) id -> true
+    | _ -> false
+
   let pexp_is_wild = function
-    | Pat_aux (Pat_exp (P_aux (P_wild, _), _), _) -> true
-    | Pat_aux (Pat_exp (P_aux (P_id id, ann), _), _) when not_enum (env_of_annot ann) id -> true
+    | Pat_aux (Pat_exp (p, _), _) -> paux_is_wild p
+    | Pat_aux (Pat_or (ps, _), _) -> List.exists paux_is_wild ps
     | _ -> false
 
   let pexp_loc = function
     | Pat_aux (Pat_exp (P_aux (_, (l, _)), _), _) -> l
+    | Pat_aux (Pat_or (ps, _), _) ->
+        let (P_aux (_, (l, _))) = List.hd ps in
+        (* TODO: make l to range *)
+        l
     | Pat_aux (Pat_when (P_aux (_, (l, _)), _, _), _) -> l
 
   let funcl_is_wild = function FCL_aux (FCL_funcl (_, pexp), _) -> pexp_is_wild pexp