Add syntax for SystemVerilog style part selects

src/lib/chunk_ast.ml

@@ -949,19 +949,12 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
       let aligned = is_aligned cases in
       let cases = List.map (chunk_pexp ~delim:"," comments chunks) cases in
       Match { kind; exp = exp_chunks; aligned; cases } |> add_chunk chunks
-  | E_vector_update _ | E_vector_update_subrange _ ->
+  | E_vector_update _ ->
       let vec_chunks, updates = chunk_vector_update comments (E_aux (aux, l)) in
       Queue.add (Vector_updates (vec_chunks, List.rev updates)) chunks
   | E_vector_access (exp, ix) ->
       let exp_chunks = rec_chunk_exp exp in
-      let ix_chunks = rec_chunk_exp ix in
-      Queue.add (Index (exp_chunks, ix_chunks)) chunks
-  | E_vector_subrange (exp, ix1, ix2) ->
-      let exp_chunks = rec_chunk_exp exp in
-      let ix1_chunks = rec_chunk_exp ix1 in
-      let ix2_chunks = rec_chunk_exp ix2 in
-      let ix_chunks = Queue.create () in
-      Queue.add (Binary (ix1_chunks, "..", ix2_chunks)) ix_chunks;
+      let ix_chunks = chunk_vector_index comments ix in
       Queue.add (Index (exp_chunks, ix_chunks)) chunks
   | E_for (var, from_index, to_index, step, order, body) ->
       let decreasing =
@@ -1031,6 +1024,23 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) =
       let exp_chunks = rec_chunk_exp exp in
       Queue.add (App (Id_aux (Id "internal_assume", l), [nc_chunks; exp_chunks])) chunks
 
+and chunk_vector_index comments (VA_aux (aux, l)) =
+  let chunks = Queue.create () in
+  let ix_binop op n m =
+    let n_chunks = Queue.create () in
+    chunk_exp comments n_chunks n;
+    let m_chunks = Queue.create () in
+    chunk_exp comments m_chunks m;
+    Queue.add (Binary (n_chunks, op, m_chunks)) chunks
+  in
+  ( match aux with
+  | VA_index ix -> chunk_exp comments chunks ix
+  | VA_subrange (n, m) -> ix_binop ".." n m
+  | VA_indexed_add (n, m) -> ix_binop "+:" n m
+  | VA_indexed_sub (n, m) -> ix_binop "-:" n m
+  );
+  chunks
+
 and chunk_vector_update comments (E_aux (aux, l) as exp) =
   let rec_chunk_exp exp =
     let chunks = Queue.create () in
@@ -1040,15 +1050,9 @@ and chunk_vector_update comments (E_aux (aux, l) as exp) =
   match aux with
   | E_vector_update (vec, ix, exp) ->
       let vec_chunks, update = chunk_vector_update comments vec in
-      let ix = rec_chunk_exp ix in
+      let ix = chunk_vector_index comments ix in
       let exp = rec_chunk_exp exp in
       (vec_chunks, Binary (ix, "=", exp) :: update)
-  | E_vector_update_subrange (vec, ix1, ix2, exp) ->
-      let vec_chunks, update = chunk_vector_update comments vec in
-      let ix1 = rec_chunk_exp ix1 in
-      let ix2 = rec_chunk_exp ix2 in
-      let exp = rec_chunk_exp exp in
-      (vec_chunks, Ternary (ix1, "..", ix2, "=", exp) :: update)
   | _ ->
       let exp_chunks = Queue.create () in
       chunk_exp comments exp_chunks exp;

src/lib/initial_check.ml

@@ -1257,9 +1257,35 @@ let rec is_config (P.E_aux (aux, _)) =
   | P.E_config root -> Some [root]
   | _ -> None
 
+let sv_vector_indexing_syntax =
+  "Reserved vector indexing syntax.\n\n\
+   This syntax is not currently implemented, but is reserved for future syntax extensions."
+
 let rec to_ast_letbind ctx (P.LB_aux (lb, l) : P.letbind) : uannot letbind =
   LB_aux ((match lb with P.LB_val (pat, exp) -> LB_val (to_ast_pat ctx pat, to_ast_exp ctx exp)), (l, empty_uannot))
 
+and to_ast_vector_access ctx vexp = function
+  | P.VA_aux (P.VA_index exp, _) ->
+      let exp = to_ast_exp ctx exp in
+      E_vector_access (vexp, exp)
+  | P.VA_aux (P.VA_subrange (n, m), _) ->
+      let n = to_ast_exp ctx n in
+      let m = to_ast_exp ctx m in
+      E_vector_subrange (vexp, n, m)
+  | P.VA_aux (_, l) -> raise (Reporting.err_syntax_loc l sv_vector_indexing_syntax)
+
+and to_ast_vector_update ctx vexp exp = function
+  | P.VA_aux (P.VA_index ix, _) ->
+      let ix = to_ast_exp ctx ix in
+      let exp = to_ast_exp ctx exp in
+      E_vector_update (vexp, ix, exp)
+  | P.VA_aux (P.VA_subrange (n, m), _) ->
+      let n = to_ast_exp ctx n in
+      let m = to_ast_exp ctx m in
+      let exp = to_ast_exp ctx exp in
+      E_vector_update_subrange (vexp, n, m, exp)
+  | P.VA_aux (_, l) -> raise (Reporting.err_syntax_loc l sv_vector_indexing_syntax)
+
 and to_ast_exp ctx exp =
   let (P.E_aux (exp, l)) = parse_infix_exp ctx exp in
   match exp with
@@ -1315,13 +1341,12 @@ and to_ast_exp ctx exp =
         | P.E_loop (P.While, m, e1, e2) -> E_loop (While, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
         | P.E_loop (P.Until, m, e1, e2) -> E_loop (Until, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2)
         | P.E_vector exps -> E_vector (List.map (to_ast_exp ctx) exps)
-        | P.E_vector_access (vexp, exp) -> E_vector_access (to_ast_exp ctx vexp, to_ast_exp ctx exp)
-        | P.E_vector_subrange (vex, exp1, exp2) ->
-            E_vector_subrange (to_ast_exp ctx vex, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
-        | P.E_vector_update (vex, exp1, exp2) ->
-            E_vector_update (to_ast_exp ctx vex, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
-        | P.E_vector_update_subrange (vex, e1, e2, e3) ->
-            E_vector_update_subrange (to_ast_exp ctx vex, to_ast_exp ctx e1, to_ast_exp ctx e2, to_ast_exp ctx e3)
+        | P.E_vector_access (vexp, va) ->
+            let vexp = to_ast_exp ctx vexp in
+            to_ast_vector_access ctx vexp va
+        | P.E_vector_update (vexp, va, exp) ->
+            let vexp = to_ast_exp ctx vexp in
+            to_ast_vector_update ctx vexp exp va
         | P.E_vector_append (e1, e2) -> E_vector_append (to_ast_exp ctx e1, to_ast_exp ctx e2)
         | P.E_list exps -> E_list (List.map (to_ast_exp ctx) exps)
         | P.E_cons (e1, e2) -> E_cons (to_ast_exp ctx e1, to_ast_exp ctx e2)
@@ -1381,6 +1406,16 @@ and to_ast_measure ctx (P.Measure_aux (m, l)) : uannot internal_loop_measure =
   in
   Measure_aux (m, l)
 
+and to_ast_vector_lexp ctx vexp = function
+  | P.VA_aux (P.VA_index ix, _) ->
+      let ix = to_ast_exp ctx ix in
+      LE_vector (vexp, ix)
+  | P.VA_aux (P.VA_subrange (n, m), _) ->
+      let n = to_ast_exp ctx n in
+      let m = to_ast_exp ctx m in
+      LE_vector_range (vexp, n, m)
+  | P.VA_aux (_, l) -> raise (Reporting.err_syntax_loc l sv_vector_indexing_syntax)
+
 and to_ast_lexp ctx exp =
   let (P.E_aux (exp, l)) = parse_infix_exp ctx exp in
   let lexp =
@@ -1409,9 +1444,9 @@ and to_ast_lexp ctx exp =
         | _ -> raise (Reporting.err_typ l' "memory call on lefthand side of assignment must begin with an id")
       end
     | P.E_vector_append (exp1, exp2) -> LE_vector_concat (to_ast_lexp ctx exp1 :: to_ast_lexp_vector_concat ctx exp2)
-    | P.E_vector_access (vexp, exp) -> LE_vector (to_ast_lexp ctx vexp, to_ast_exp ctx exp)
-    | P.E_vector_subrange (vexp, exp1, exp2) ->
-        LE_vector_range (to_ast_lexp ctx vexp, to_ast_exp ctx exp1, to_ast_exp ctx exp2)
+    | P.E_vector_access (vexp, va) ->
+        let vexp = to_ast_lexp ctx vexp in
+        to_ast_vector_lexp ctx vexp va
     | P.E_field (fexp, id) -> LE_field (to_ast_lexp ctx fexp, to_ast_id ctx id)
     | _ ->
         raise

src/lib/lexer.mll

@@ -180,6 +180,8 @@ rule token comments = parse
   | ";"                                 { Semi }
   | "*"                                 { Star }
   | "_"                                 { Under }
+  | "+:"                                { PlusColon }
+  | "-:"                                { MinusColon }
   | "[|"                                { LsquareBar }
   | "|]"                                { RsquareBar }
   | "{|"                                { LcurlyBar }

src/lib/parse_ast.ml

@@ -210,6 +210,14 @@ type measure_aux =
 
 and measure = Measure_aux of measure_aux * l
 
+and vector_access_aux =
+  | VA_index of exp (* A single index [N] *)
+  | VA_subrange of exp * exp (* Accessing a range [N .. M] *)
+  | VA_indexed_add of exp * exp (* SystemVerilog-style indexed part select [M +: N] *)
+  | VA_indexed_sub of exp * exp (* SystemVerilog-style indexed part select [M -: N] *)
+
+and vector_access = VA_aux of vector_access_aux * l
+
 and exp_aux =
   (* Expression *)
   | E_block of exp list (* block (parsing conflict with structs?) *)
@@ -226,10 +234,8 @@ and exp_aux =
   | E_loop of loop * measure * exp * exp
   | E_for of id * exp * exp * exp * atyp * exp (* loop *)
   | E_vector of exp list (* vector (indexed from 0) *)
-  | E_vector_access of exp * exp (* vector access *)
-  | E_vector_subrange of exp * exp * exp (* subvector extraction *)
-  | E_vector_update of exp * exp * exp (* vector functional update *)
-  | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
+  | E_vector_access of exp * vector_access
+  | E_vector_update of exp * vector_access * exp (* vector functional update *)
   | E_vector_append of exp * exp (* vector concatenation *)
   | E_list of exp list (* list *)
   | E_cons of exp * exp (* cons *)

src/lib/parser.mly

@@ -157,10 +157,8 @@ type vector_update =
 
 let rec mk_vector_updates input updates n m =
   match updates with
-  | VU_single (idx, value) :: updates ->
+  | (idx, value) :: updates ->
      mk_vector_updates (mk_exp (E_vector_update (input, idx, value)) n m) updates n m
-  | VU_range (high, low, value) :: updates ->
-     mk_vector_updates (mk_exp (E_vector_update_subrange (input, high, low, value)) n m) updates n m
   | [] -> input
 
 let typschm_is_pure (TypSchm_aux (TypSchm_ts (_, ATyp_aux (typ, _)), _)) =
@@ -222,7 +220,7 @@ let set_syntax_deprecated l =
 %nonassoc Then
 %nonassoc Else
 
-%token Bar Comma Dot Eof Minus Semi Under DotDot At ColonColon Caret Star
+%token Bar Comma Dot Eof Minus Semi Under DotDot At ColonColon Caret Star PlusColon MinusColon
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar
 %token MinusGt Bidir
 
@@ -754,6 +752,16 @@ block:
   | pat Eq exp
     { LB_aux (LB_val ($1, $3), loc $startpos $endpos) }
 
+vector_access(E):
+  | exp=E
+    { VA_aux (VA_index exp, loc $startpos $endpos) }
+  | lhs=E; DotDot; rhs=E
+    { VA_aux (VA_subrange (lhs, rhs), loc $startpos $endpos) }
+  | lhs=E; PlusColon; rhs=E
+    { VA_aux (VA_indexed_add (lhs, rhs), loc $startpos $endpos) }
+  | lhs=E; MinusColon; rhs=E
+    { VA_aux (VA_indexed_sub (lhs, rhs), loc $startpos $endpos) }
+
 atomic_exp:
   | atomic_exp Colon atomic_typ
     { mk_exp (E_typ ($3, $1)) $startpos $endpos }
@@ -797,12 +805,8 @@ atomic_exp:
     { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos }
   | Assert Lparen exp Comma exp Rparen
     { mk_exp (E_assert ($3, $5)) $startpos $endpos }
-  | atomic_exp Lsquare exp Rsquare
+  | atomic_exp Lsquare vector_access(exp) Rsquare
     { mk_exp (E_vector_access ($1, $3)) $startpos $endpos }
-  | atomic_exp Lsquare exp DotDot exp Rsquare
-    { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos }
-  | atomic_exp Lsquare exp Comma exp Rsquare
-    { mk_exp (E_app (mk_id (Id "slice") $startpos($2) $endpos, [$1; $3; $5])) $startpos $endpos }
   | Struct id? Lcurly fexp_exp_list Rcurly
     { mk_exp (E_struct ($2, $4)) $startpos $endpos }
   | Lcurly exp With fexp_exp_list Rcurly
@@ -843,12 +847,12 @@ exp_list:
     { $1 :: $3 }
 
 vector_update:
-  | atomic_exp Eq exp
-    { VU_single ($1, $3) }
-  | atomic_exp DotDot atomic_exp Eq exp
-    { VU_range ($1, $3, $5) }
-  | id
-    { VU_single (mk_exp (E_id $1) $startpos $endpos, mk_exp (E_id $1) $startpos $endpos)}
+  | va=vector_access(atomic_exp); Eq; e=exp
+    { (va, e) }
+  | id=id
+    { let l = loc $startpos $endpos in
+      let exp = E_aux (E_id id, l) in
+      (VA_aux (VA_index exp, l), exp) }
 
 vector_update_list:
   | vector_update Comma?

src/sail_doc_backend/html_source.ml

@@ -109,7 +109,8 @@ let highlights ~filename ~contents =
         mark Highlight.TyVar;
         go ()
     | Under | Colon _ | Lcurly | Rcurly | LcurlyBar | RcurlyBar | Lsquare | Rsquare | LsquareBar | RsquareBar | Lparen
-    | Rparen | Dot | DotDot | EqGt _ | At | Unit _ | Bidir | Semi | Comma | Eq _ | TwoCaret | MinusGt ->
+    | Rparen | Dot | DotDot | EqGt _ | At | Unit _ | Bidir | Semi | Comma | Eq _ | TwoCaret | MinusGt | MinusColon
+    | PlusColon ->
         go ()
   in
   go ();