Skip to content

[spectec] Support ~ and ~_ relation symbols #2267

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rossberg merged 1 commit into from
Oct 8, 2026
Merged

[spectec] Support ~ and ~_ relation symbols #2267

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions spectec/src/backend-latex/render.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1078,6 +1078,7 @@ Printf.eprintf "[render_atom %s @ %s] id=%s def=%s macros: %s (%s)\n%!"
| GreaterEqual -> "\\geq"
| Equiv | EquivSub -> "\\equiv"
| Approx | ApproxSub -> "\\approx"
| Sim | SimSub -> "\\sim"
| Arrow | ArrowSub -> "\\rightarrow"
| Arrow2 | Arrow2Sub -> "\\Rightarrow"
| Sub -> "\\leq"
Expand Down
4 changes: 2 additions & 2 deletions spectec/src/frontend/lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,8 +174,8 @@ and token = parse
| "=_" { EQSUB }
| "==_" { EQUIVSUB }
| "~~_" { APPROXSUB }

| "~" { NOT }
| "~_" { SIMSUB }
| "~" { SIM }
| "/\\" { AND }
| "\\/" { OR }
| "(/\\)" { BIGAND }
Expand Down
45 changes: 29 additions & 16 deletions spectec/src/frontend/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ and short_alt_prod' = function
%token COLON SEMICOLON COMMA DOT DOTDOT DOTDOTDOT BAR BARBAR DASH COLONSUB
%token BIGAND BIGOR BIGFORALL BIGEXISTS BIGADD BIGMUL BIGCAT
%token COMMA_NL NL_BAR NL_NL NL_NL_NL
%token EQ NE LT GT LE GE APPROX EQUIV ASSIGN SUB SUP EQCAT EQSUB EQUIVSUB APPROXSUB
%token EQ NE LT GT LE GE APPROX SIM EQUIV ASSIGN SUB SUP EQCAT EQSUB EQUIVSUB APPROXSUB SIMSUB
%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
Expand All @@ -201,7 +201,7 @@ and short_alt_prod' = function
%nonassoc TURNSTILE TURNSTILESUB
%nonassoc TILESTURN TILESTURNSUB
%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 COLON SUB SUP ASSIGN EQUIV APPROX SIM COLONSUB EQUIVSUB APPROXSUB SIMSUB
%left COMMA COMMA_NL
%right EQ NE LT GT LE GE MEM NOTMEM EQSUB
%right ARROW ARROWSUB
Expand Down Expand Up @@ -344,7 +344,7 @@ atom_escape :
| TICK PLUSMINUS { Atom.PlusMinus }
| TICK MINUSPLUS { Atom.MinusPlus }
| TICK STAR { Atom.Times }
| TICK NOT { Atom.Not }
| TICK SIM { Atom.Not }
| TICK AND { Atom.And }
| TICK OR { Atom.Or }
| TICK IMPL { Atom.Arrow2 }
Expand All @@ -353,7 +353,7 @@ atom_escape :
| TICK CAT { Atom.Cat }
| TICK COMMA { Atom.Comma }
| TICK infixop_ { $2 }
| TICK relop_ { $2 }
| TICK relop_prefix_ { $2 }
| BOT { Atom.Bot }
| TOP { Atom.Top }
| INFINITY { Atom.Infinity }
Expand Down Expand Up @@ -391,6 +391,7 @@ check_atom :

%inline unop :
| NOT { `NotOp }
| SIM { `NotOp }
| PLUS { `PlusOp }
| MINUS { `MinusOp }
| PLUSMINUS { `PlusMinusOp }
Expand Down Expand Up @@ -442,9 +443,9 @@ check_atom :
| ARROWSUB { Atom.ArrowSub }
| ARROW2SUB { Atom.Arrow2Sub }

%inline relop :
| relop_ { $1 $$ $sloc }
%inline relop_ :
%inline relop_prefix :
| relop_prefix_ { $1 $$ $sloc }
%inline relop_prefix_ :
| COLON { Atom.Colon }
| SUB { Atom.Sub }
| SUP { Atom.Sup }
Expand All @@ -458,9 +459,15 @@ check_atom :
| TILESTURN { Atom.Tilesturn }
| TURNSTILE { Atom.Turnstile }

%inline relopsub :
| relopsub_ { $1 $$ $sloc }
%inline relopsub_ :
%inline relop :
| relop_ { $1 $$ $sloc }
%inline relop_ :
| relop_prefix_ { $1 }
| SIM { Atom.Sim }

%inline relopsub_prefix :
| relopsub_prefix_ { $1 $$ $sloc }
%inline relopsub_prefix_ :
| EQSUB { Atom.EqualSub }
| COLONSUB { Atom.ColonSub }
| EQUIVSUB { Atom.EquivSub }
Expand All @@ -472,6 +479,12 @@ check_atom :
| TILESTURNSUB { Atom.TilesturnSub }
| TURNSTILESUB { Atom.TurnstileSub }

%inline relopsub :
| relopsub_ { $1 $$ $sloc }
%inline relopsub_ :
| relopsub_prefix_ { $1 }
| SIMSUB { Atom.SimSub }


(* Iteration *)

Expand Down Expand Up @@ -638,8 +651,8 @@ nottyp_bin_ :
nottyp_rel : nottyp_rel_ { $1 $ $sloc }
nottyp_rel_ :
| nottyp_bin_ { $1 }
| relop nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, $2) }
| relopsub nottyp_prim nottyp_rel
| relop_prefix nottyp_rel { InfixT (SeqT [] $ $loc($1), $1, $2) }
| relopsub_prefix nottyp_prim nottyp_rel
{ InfixT (SeqT [] $ $loc($1), $1, cat_seq_typ $2 $3) }
| nottyp_rel relop nottyp_rel { InfixT ($1, $2, $3) }
| nottyp_rel relopsub nottyp_prim nottyp_rel
Expand Down Expand Up @@ -798,8 +811,8 @@ exp_bin_ :
exp_rel : exp_rel_ { $1 $ $sloc }
exp_rel_ :
| exp_bin_ { $1 }
| relop exp_rel { InfixE (SeqE [] $ $loc($1), $1, $2) }
| relopsub exp_prim exp_rel
| relop_prefix exp_rel { InfixE (SeqE [] $ $loc($1), $1, $2) }
| relopsub_prefix exp_prim exp_rel
{ InfixE (SeqE [] $ $loc($1), $1, cat_seq_exp $2 $3) }
| exp_rel relop exp_rel { InfixE ($1, $2, $3) }
| exp_rel relopsub exp_prim exp_rel { InfixE ($1, $2, cat_seq_exp $3 $4) }
Expand All @@ -808,8 +821,8 @@ exp_comma : exp_comma_ { $1 $ $sloc }
exp_comma_ :
| exp_bin_ { $1 }
| comma(exp) exp_comma { CommaE (SeqE [] $ $loc($1), $2) }
| relop exp_comma { InfixE (SeqE [] $ $loc($1), $1, $2) }
| relopsub exp_prim exp_comma
| relop_prefix exp_comma { InfixE (SeqE [] $ $loc($1), $1, $2) }
| relopsub_prefix exp_prim exp_comma
{ InfixE (SeqE [] $ $loc($1), $1, cat_seq_exp $2 $3) }
| exp_comma comma(exp) exp_comma { CommaE ($1, $3) }
| exp_comma relop exp_comma { InfixE ($1, $2, $3) }
Expand Down
4 changes: 2 additions & 2 deletions spectec/src/il2al/preprocess.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,8 +138,8 @@ let rec preprocess_prem prem =
when turnstile.it = Turnstile && colon.it = Colon ->
typing_functions := id.it :: !typing_functions;
Some (lhs, rhs)
(* `lhs` ~~ `rhs` *)
| [[]; [approx]; []], TupE [lhs; rhs] when approx.it = Approx -> Some (lhs, rhs)
(* `lhs` ~~ `rhs` or `lhs` ~ `rhs` *)
| [[]; [op]; []], TupE [lhs; rhs] when op.it = Approx || op.it = Sim -> Some (lhs, rhs)
| _ -> None
in
(match lhs_rhs_opt with
Expand Down
9 changes: 8 additions & 1 deletion spectec/src/xl/atom.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ and atom' =
| EquivSub (* `==_` *)
| Approx (* `~~` *)
| ApproxSub (* `~~_` *)
| Sim (* `~` *)
| SimSub (* `~_` *)
| SqArrow (* `~>` *)
| SqArrowSub (* `~>_` *)
| SqArrowStar (* `~>*` *)
Expand Down Expand Up @@ -85,7 +87,7 @@ let compare atom1 atom2 =
let is_sub atom =
match atom.it with
| Atom id -> id <> "" && id.[String.length id - 1] = '_'
| ArrowSub | Arrow2Sub | ColonSub | EqualSub | EquivSub | ApproxSub
| ArrowSub | Arrow2Sub | ColonSub | EqualSub | EquivSub | ApproxSub | SimSub
| SqArrowSub | SqArrowStarSub | PrecSub | SuccSub
| TurnstileSub | TilesturnSub -> true
| _ -> false
Expand All @@ -99,6 +101,7 @@ let sub atom1 atom2 =
| EqualSub, Equal
| EquivSub, Equiv
| ApproxSub, Approx
| SimSub, Sim
| SqArrowSub, SqArrow
| SqArrowStarSub, SqArrowStar
| PrecSub, Prec
Expand Down Expand Up @@ -143,6 +146,8 @@ let to_string atom =
| EquivSub -> "==_"
| Approx -> "~~"
| ApproxSub -> "~~_"
| Sim -> "~"
| SimSub -> "~_"
| SqArrow -> "~>"
| SqArrowSub -> "~>_"
| SqArrowStar -> "~>*"
Expand Down Expand Up @@ -221,6 +226,8 @@ let name atom =
| EquivSub -> "equiv_"
| Approx -> "approx"
| ApproxSub -> "approx_"
| Sim -> "sim"
| SimSub -> "sim_"
| SqArrow -> "sqarrow" (* Latex: \hookrightarrow *)
| SqArrowSub -> "sqarrow_" (* Latex: \hookrightarrow with subscript *)
| SqArrowStar -> "sqarrowstar" (* Latex: \hookrightarrow^\ast *)
Expand Down
96 changes: 96 additions & 0 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -763,6 +763,10 @@ $\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$

$\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -789,12 +793,28 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\
\end{array}
$$

$\boxed{C \vdash {\mathit{parent}} : \mathsf{ok}}$

$\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$

$\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -821,12 +841,28 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim\_macro}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub\_macro}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\
\end{array}
$$

$\boxed{C \vdash {\mathit{parent}} : \mathsf{ok}}$

$\boxed{C \vdash {\mathit{parent}} \leq {\mathit{parent}}}$

$\boxed{{\mathit{parent}} ; {\mathit{child}} \hookrightarrow {\mathit{parent}} ; {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim {\mathit{child}}}$

$\boxed{{\mathit{parent}} \sim_{C} {\mathit{child}}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -853,6 +889,18 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim\_nomacro}]} \quad & \mathsf{aa} & \sim & \mathsf{bbb} \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub\_nomacro}]} \quad & \mathsf{aa} & {\sim}_{C} {} & \mathsf{bbb} \\
\end{array}
$$

\vspace{1ex}

\vspace{1ex}
Expand Down Expand Up @@ -1938,6 +1986,10 @@ $\boxed{{\C} \vdash {\parent} \leq {\parent}}$

$\boxed{{\parent} ; {\child} \hookrightarrow {\parent} ; {\child}}$

$\boxed{{\parent} \sim {\child}}$

$\boxed{{\parent} \sim_{{\C}} {\child}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -1964,12 +2016,28 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim}]} \quad & \AA & \sim & \BBB \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub}]} \quad & \AA & {\sim}_{{\C}} {} & \BBB \\
\end{array}
$$

$\boxed{{\C} \vdashok {\parent} : \OKok}$

$\boxed{{\C} \vdashsub {\parent} \subsub {\parent}}$

$\boxed{{\parent} ; {\child} \sqarroweval {\parent} ; {\child}}$

$\boxed{{\parent} \simsim {\child}}$

$\boxed{{\parent} \simsim_{{\C}} {\child}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -1996,12 +2064,28 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim\_macro}]} \quad & \AA & \simsim & \BBB \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub\_macro}]} \quad & \AA & {\simsim}_{{\C}} {} & \BBB \\
\end{array}
$$

$\boxed{{\C} \vdash {\parent} : \mathsf{ok}}$

$\boxed{{\C} \vdash {\parent} \leq {\parent}}$

$\boxed{{\parent} ; {\child} \hookrightarrow {\parent} ; {\child}}$

$\boxed{{\parent} \sim {\child}}$

$\boxed{{\parent} \sim_{{\C}} {\child}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
Expand All @@ -2028,6 +2112,18 @@ $$
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsim\_nomacro}]} \quad & \AA & \sim & \BBB \\
\end{array}
$$

$$
\begin{array}[t]{@{}lrcl@{}l@{}}
{[\textsc{\scriptsize Rsimsub\_nomacro}]} \quad & \AA & {\sim}_{{\C}} {} & \BBB \\
\end{array}
$$

\vspace{1ex}

\vspace{1ex}
Expand Down
Loading
Loading