Use Sigma for sum

Wasm-DSL · Jul 1, 2024 · f8301b2 · f8301b2
1 parent 7ff829a
commit f8301b2
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/spectec/doc/Language.md b/spectec/doc/Language.md
@@ -152,7 +152,6 @@ exp ::=
   hole                                 hole (for syntax rewrites in hints)
   exp "#" exp                          token concatenation (for syntax rewrites in hints)
   "##" exp                             remove possible parentheses (for syntax rewrites in hints)
-  "latex" "(" text* ")"                literal latex (for syntax rewrites)
 
 unop  ::= notop | "+" | "-"
 binop ::= logop | "+" | "-" | "*" | "/" | "\" | "^"
@@ -181,6 +180,7 @@ hole ::=
   "%"digit*                            use numbered operand
   "%%"                                 use all operands
   "!%"                                 empty expression
+  "%latex" "(" text* ")"               literal latex
 ```
 
 The various meta notations for lists, records, and tuples mirror the syntactic conventions defined in the Wasm spec.

diff --git a/spectec/spec/wasm-3.0/0-aux.watsup b/spectec/spec/wasm-3.0/0-aux.watsup
@@ -30,7 +30,7 @@ def $min(0, j) = 0
 def $min(i, 0) = 0
 def $min($(i+1), $(j+1)) = $min(i, j)
 
-def $sum(nat*) : nat  ;; TODO(2, rossberg): hint to use sigma?
+def $sum(nat*) : nat  hint(show %latex("\\Sigma\\,")#%)
 def $sum(eps) = 0
 def $sum(n n'*) = $(n + $sum(n'*))
 

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -1009,7 +1009,7 @@ and render_exp env e =
   | NatE (AtomOp, n) ->
     let atom = {it = Atom.Atom (Z.to_string n); at = e.at; note = Atom.info "nat"} in
     render_atom (without_macros true env) atom
-  | TextE t -> "``" ^ t ^ "''"
+  | TextE t -> "\\mbox{\\tt`" ^ t ^ "'}"
   | UnE (op, e2) -> "{" ^ render_unop op ^ render_exp env e2 ^ "}"
   | BinE (e1, ExpOp, ({it = ParenE (e2, _); _ } | e2)) ->
     "{" ^ render_exp env e1 ^ "^{" ^ render_exp env e2 ^ "}}"

diff --git a/spectec/src/frontend/lexer.mll b/spectec/src/frontend/lexer.mll
@@ -207,6 +207,7 @@ and token = parse
   | "!%" { NOTHING }
   | "#" { FUSE }
   | "##" { FUSEFUSE }
+  | "%latex" { LATEX }
 
   | "`" { TICK }
 
@@ -227,7 +228,6 @@ and token = parse
   | "if" { IF }
   | "otherwise" { OTHERWISE }
   | "hint(" { HINT_LPAREN }
-  | "latex" { LATEX }
 
   | "eps" { EPS }
   | "true" { BOOLLIT true }