From 247abe93e7c9a83160b55f17044f79d247eadbf9 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 12 Jun 2025 17:41:53 +0100 Subject: [PATCH] Add syntax for SystemVerilog style part selects This commits adds syntax to the parser for SystemVerilog-style part select operators, `v[n +: m]` and `v[n -: m]`. Currently these are allowed in both expressions and L-expressions. More work is needed to support these in bitfield definitions. Right now these aren't implemented, so any attempt to use results in ``` REPL:2> v[n -: m] Syntax error: REPL:2.2-8: 2 |v[n -: m] | ^----^ | Reserved vector indexing syntax. | | This syntax is not currently implemented, but is reserved for future syntax extensions. ``` To push further into the language I think the L-expression type needs to be re-factored so backends can handle all these operators in a clean way. This also potentially opens the door to parsing half-open ranges, which is another requested feature - although the exact syntax for that would require more consideration. --- src/lib/chunk_ast.ml | 36 ++++++++++--------- src/lib/initial_check.ml | 55 +++++++++++++++++++++++------ src/lib/lexer.mll | 2 ++ src/lib/parse_ast.ml | 14 +++++--- src/lib/parser.mly | 34 ++++++++++-------- src/sail_doc_backend/html_source.ml | 3 +- 6 files changed, 98 insertions(+), 46 deletions(-) diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index 7fc09c2b4..58dca3e40 100644 --- a/src/lib/chunk_ast.ml +++ b/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; diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index c3011b16b..c2b119c12 100644 --- a/src/lib/initial_check.ml +++ b/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 diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index b68403bfd..fac8c8e57 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -180,6 +180,8 @@ rule token comments = parse | ";" { Semi } | "*" { Star } | "_" { Under } + | "+:" { PlusColon } + | "-:" { MinusColon } | "[|" { LsquareBar } | "|]" { RsquareBar } | "{|" { LcurlyBar } diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 5804685df..13b8102bc 100644 --- a/src/lib/parse_ast.ml +++ b/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 *) diff --git a/src/lib/parser.mly b/src/lib/parser.mly index 0b1422c36..3d186e4a3 100644 --- a/src/lib/parser.mly +++ b/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? diff --git a/src/sail_doc_backend/html_source.ml b/src/sail_doc_backend/html_source.ml index 6ec381858..a402a4dc1 100644 --- a/src/sail_doc_backend/html_source.ml +++ b/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 ();