[spectec] Support subscripting prec/succ

Author: rossberg

spectec/doc/Language.md

@@ -163,7 +163,7 @@ atomop ::=
   "`~" | "`/\" | "`\/" | "`==>" | "`<=>"
   "`<-"
   "(/\)" | "(\/)" | "(!)" | "(?)" | "(+)" | "(*)" | "(++)"
-  ":_" | "=_" | "==_" | "~~_" | "->_" | "=>_" | "~>_" | "~>*_" | "|-_" | "-|_"
+  ":_" | "=_" | "==_" | "~~_" | "->_" | "=>_" | "~>_" | "~>*_" | "<<_" | ">>_" | "|-_" | "-|_"
 ```
 
 ##### Type Aliases
@@ -1385,7 +1385,7 @@ atomop ::=
   "`~" | "`/\" | "`\/" | "`==>" | "`<=>"
   "`<-"
   "(/\)" | "(\/)" | "(!)" | "(?)" | "(+)" | "(*)" | "(++)"
-  ":_" | "=_" | "==_" | "~~_" | "->_" | "=>_" | "~>_" | "~>*_" | "|-_" | "-|_"
+  ":_" | "=_" | "==_" | "~~_" | "->_" | "=>_" | "~>_" | "~>*_" | "<<_" | ">>_" | "|-_" | "-|_"
 ```
 
 

spectec/doc/example/output/NanoWasm.pdf

@@ -209,6 +209,8 @@ and token = parse
   | "~>*_" { SQARROWSTARSUB }
   | "<<" { PREC }
   | ">>" { SUCC }
+  | "<<_" { PRECSUB }
+  | ">>_" { SUCCSUB }
   | "|-" { TURNSTILE }
   | "-|" { TILESTURN }
   | "|-_" { TURNSTILESUB }

spectec/src/frontend/lexer.mll

@@ -180,7 +180,7 @@ and short_alt_prod' = function
 %token NOT AND OR IMPL DIMPL
 %token QUEST PLUS MINUS STAR SLASH BACKSLASH UP CAT PLUSMINUS MINUSPLUS
 %token ARROW ARROW2 ARROWSUB ARROW2SUB SQARROW SQARROWSUB SQARROWSTAR SQARROWSTARSUB
-%token MEM NOTMEM PREC SUCC TURNSTILE TILESTURN TURNSTILESUB TILESTURNSUB
+%token MEM NOTMEM PREC SUCC PRECSUB SUCCSUB TURNSTILE TILESTURN TURNSTILESUB TILESTURNSUB
 %token DOLLAR TICK
 %token BOT TOP
 %token HOLE MULTIHOLE NOTHING FUSE FUSEFUSE LATEX
@@ -200,7 +200,7 @@ and short_alt_prod' = function
 %left AND
 %nonassoc TURNSTILE TURNSTILESUB
 %nonassoc TILESTURN TILESTURNSUB
-%right SQARROW SQARROWSUB SQARROWSTAR SQARROWSTARSUB PREC SUCC BIGAND BIGOR BIGFORALL BIGEXISTS BIGADD BIGMUL BIGCAT
+%right SQARROW SQARROWSUB SQARROWSTAR SQARROWSTARSUB PREC SUCC PRECSUB SUCCSUB BIGAND BIGOR BIGFORALL BIGEXISTS BIGADD BIGMUL BIGCAT
 %left COLON SUB SUP ASSIGN EQUIV APPROX COLONSUB EQUIVSUB APPROXSUB
 %left COMMA COMMA_NL
 %right EQ NE LT GT LE GE MEM NOTMEM EQSUB
@@ -467,6 +467,8 @@ check_atom :
   | APPROXSUB { Atom.ApproxSub }
   | SQARROWSUB { Atom.SqArrowSub }
   | SQARROWSTARSUB { Atom.SqArrowStarSub }
+  | PRECSUB { Atom.PrecSub }
+  | SUCCSUB { Atom.SuccSub }
   | TILESTURNSUB { Atom.TilesturnSub }
   | TURNSTILESUB { Atom.TurnstileSub }
 

spectec/src/frontend/parser.mly

@@ -47,6 +47,8 @@ and atom' =
   | SqArrowStarSub               (* `~>*_` *)
   | Prec                         (* `<<` *)
   | Succ                         (* `>>` *)
+  | PrecSub                      (* `<<_` *)
+  | SuccSub                      (* `>>_` *)
   | Turnstile                    (* `|-` *)
   | TurnstileSub                 (* `|-_` *)
   | Tilesturn                    (* `-|` *)
@@ -84,7 +86,8 @@ let is_sub atom =
   match atom.it with
   | Atom id -> id <> "" && id.[String.length id - 1] = '_'
   | ArrowSub | Arrow2Sub | ColonSub | EqualSub | EquivSub | ApproxSub
-  | SqArrowSub | SqArrowStarSub | TurnstileSub | TilesturnSub -> true
+  | SqArrowSub | SqArrowStarSub | PrecSub | SuccSub
+  | TurnstileSub | TilesturnSub -> true
   | _ -> false
 
 let sub atom1 atom2 = 
@@ -98,6 +101,8 @@ let sub atom1 atom2 =
   | ApproxSub, Approx
   | SqArrowSub, SqArrow
   | SqArrowStarSub, SqArrowStar
+  | PrecSub, Prec
+  | SuccSub, Succ
   | TurnstileSub, Turnstile
   | TilesturnSub, Tilesturn -> true
   | _, _ -> false
@@ -144,9 +149,11 @@ let to_string atom =
   | SqArrowStarSub -> "~>*_"
   | Prec -> "<<"
   | Succ -> ">>"
+  | PrecSub -> "<<_"
+  | SuccSub -> ">>_"
   | Tilesturn -> "-|"
-  | TilesturnSub -> "-|_"
   | Turnstile -> "|-"
+  | TilesturnSub -> "-|_"
   | TurnstileSub -> "|-_"
   | Quest -> "^?"
   | Star -> "^*"
@@ -220,9 +227,11 @@ let name atom =
   | SqArrowStarSub -> "sqarrowstar_" (* Latex: \hookrightarrow^\ast with subscript *)
   | Prec -> "prec"
   | Succ -> "succ"
+  | PrecSub -> "prec_"
+  | SuccSub -> "succ_"
   | Tilesturn -> "dashv"
-  | TilesturnSub -> "dashv_"      (* Latex: \dashv with subscript *)
   | Turnstile -> "vdash"
+  | TilesturnSub -> "dashv_"      (* Latex: \dashv with subscript *)
   | TurnstileSub -> "vdash_"      (* Latex: \vdash with subscript *)
   | Quest -> "quest"              (* Latex: ^? *)
   | Star -> "ast"                 (* Latex: ^\ast *)