Skip to content

Commit

Permalink
Allow iteration in arithmetic expressions
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Nov 28, 2023
1 parent 613c768 commit d2966be
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 3 deletions.
2 changes: 2 additions & 0 deletions spectec/doc/Language.md
Original file line number Diff line number Diff line change
Expand Up @@ -161,8 +161,10 @@ arith ::=
arith cmpop arith comparison
exp "[" arith "]" list indexing
"(" arith ")" parentheses
"(" arith iter ")" iteration (must not be "^exp")
"|" exp "|" list length
"$" defid exp? function invocation
"$" "(" exp ")" escape back to general expression syntax
path ::=
path? "[" arith "]" list element
Expand Down
30 changes: 29 additions & 1 deletion spectec/src/frontend/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ let strip_ticks id =
String.sub id 0 !i


(* Parentheses Role *)
(* Parentheses Role etc *)

type prec = Op | Seq | Post | Prim

Expand All @@ -86,6 +86,18 @@ let signify_pars prec = function
| ParenE (exp, false) -> ParenE (exp, prec < prec_of_exp exp.it)
| exp' -> exp'

let is_post_exp e =
match e.it with
| VarE _ | AtomE _
| BoolE _ | NatE _ | HexE _ | CharE _
| EpsE
| ParenE _ | TupE _ | BrackE _
| IdxE _ | SliceE _ | ExtE _
| StrE _ | DotE _
| IterE _ | CallE _
| HoleE _ -> true
| _ -> false

%}

%token LPAR RPAR LBRACK RBRACK LBRACE RBRACE
Expand Down Expand Up @@ -517,6 +529,22 @@ arith_prim_ :
| INT { VarE ("int" $ at $sloc) }
| TEXT { VarE ("text" $ at $sloc) }
| LPAR arith RPAR { ParenE ($2, false) }
| LPAR arith_bin STAR RPAR
{ (* HACK: to allow "(s*)" as arithmetic expression. *)
if not (is_post_exp $2) then
Source.error (at $loc($3)) "syntax" "misplaced token";
IterE ($2, List) }
| LPAR arith_bin PLUS RPAR
{ (* HACK: to allow "(s+)" as arithmetic expression. *)
if not (is_post_exp $2) then
Source.error (at $loc($3)) "syntax" "misplaced token";
IterE ($2, List1) }
| LPAR arith_bin QUEST RPAR
{ (* HACK: to allow "(s?)" as arithmetic expression. *)
if not (is_post_exp $2) then
Source.error (at $loc($3)) "syntax" "misplaced token";
IterE ($2, Opt) }
| DOLLAR LPAR exp RPAR { $3.it }
| DOLLAR defid { CallE ($2, TupE [] $ at $sloc) }
| DOLLAR defid_lpar exp_list RPAR { CallE ($2, tup_exp $3 $loc($3)) }
Expand Down
2 changes: 1 addition & 1 deletion spectec/test-latex/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ EXT = $(NAME)

OWNDIR = $(PWD)
SPECDIR = ../spec
SPECS = $(shell ls $(SPECDIR))
SPECS = $(shell cd $(SPECDIR) && ls -d wasm-*)
SPECFILES = $(shell ls $(SPECS:%=$(SPECDIR)/%/*.$(EXT)))

SPEC =
Expand Down
2 changes: 1 addition & 1 deletion spectec/test-prose/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ EXT = $(NAME)

OWNDIR = $(PWD)
SPECDIR = ../spec
SPECS = $(shell ls $(SPECDIR))
SPECS = $(shell cd $(SPECDIR) && ls -d wasm-*)
TESTS = $(SPECS:%=test-%)


Expand Down

0 comments on commit d2966be

Please sign in to comment.