diff options
| author | Alasdair Armstrong | 2018-01-19 19:15:49 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-19 19:15:49 +0000 |
| commit | 2dac693e02c7f467f4faf5d95cd3017002beb060 (patch) | |
| tree | 1ece7d085e0a842c937bc590434fce7ec258370b | |
| parent | b3cb23aeb3d555b6256fbb027e55378efc2cdc12 (diff) | |
Added C-style single line comments
// is a comment
as well as
/* is a comment */
| -rw-r--r-- | riscv/riscv_types.sail | 10 | ||||
| -rw-r--r-- | src/lexer.mll | 6 |
2 files changed, 10 insertions, 6 deletions
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index b1b070bb..cb2ea794 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -8,7 +8,7 @@ type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} -function regbits_to_regno n = let 'N = unsigned(n) in N +function regbits_to_regno b = let 'r = unsigned(b) in r /* register x0 : regval is hard-wired zero */ register x1 : regval @@ -64,12 +64,10 @@ function rGPR 0 = 0x0000000000000000 and rGPR (r if r > 0) = reg_deref(GPRs[r - 1]) /*val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg}*/ -val wGPR : forall 'n . (atom('n), regval) -> unit effect {wreg, escape} +val wGPR : forall 'n, 0 <= 'n < 32. (regno('n), regval) -> unit effect {wreg} -function wGPR (r, v) = { - assert(constraint('n >= 0 & 'n < 32)); - if (r != 0) then (*GPRs[r - 1]) = v else () -} +function wGPR (r, v) = + if (r != 0) then (*GPRs[r - 1]) = v function check_alignment (addr : bits(64), width : atom('n)) -> forall 'n. unit = if unsigned(addr) % width != 0 then throw(Error_misaligned_access) else () diff --git a/src/lexer.mll b/src/lexer.mll index fb33552b..2f101b8e 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -233,6 +233,7 @@ rule token = parse | "->" { MinusGt } | "=>" { EqGt(r "=>") } | "<=" { (LtEq(r"<=")) } + | "//" { line_comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf } | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } | "infix" ws (digit as p) ws (operator as op) @@ -270,6 +271,11 @@ rule token = parse Lexing.lexeme_start_p lexbuf)) } +and line_comment pos = parse + | "\n" { () } + | _ { line_comment pos lexbuf } + | eof { raise (LexError("File ended before newline in comment", pos)) } + and comment pos depth = parse | "/*" { comment pos (depth+1) lexbuf } | "*/" { if depth = 0 then () |