diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index fe1dc3ee53..8439dd4c9f 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -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" diff --git a/spectec/src/frontend/lexer.mll b/spectec/src/frontend/lexer.mll index c10765b6c0..50605fec44 100644 --- a/spectec/src/frontend/lexer.mll +++ b/spectec/src/frontend/lexer.mll @@ -174,8 +174,8 @@ and token = parse | "=_" { EQSUB } | "==_" { EQUIVSUB } | "~~_" { APPROXSUB } - - | "~" { NOT } + | "~_" { SIMSUB } + | "~" { SIM } | "/\\" { AND } | "\\/" { OR } | "(/\\)" { BIGAND } diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly index 94f5ab086b..40d4721136 100644 --- a/spectec/src/frontend/parser.mly +++ b/spectec/src/frontend/parser.mly @@ -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 @@ -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 @@ -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 } @@ -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 } @@ -391,6 +391,7 @@ check_atom : %inline unop : | NOT { `NotOp } + | SIM { `NotOp } | PLUS { `PlusOp } | MINUS { `MinusOp } | PLUSMINUS { `PlusMinusOp } @@ -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 } @@ -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 } @@ -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 *) @@ -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 @@ -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) } @@ -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) } diff --git a/spectec/src/il2al/preprocess.ml b/spectec/src/il2al/preprocess.ml index 8c44dc02a3..ca13e5e6cc 100644 --- a/spectec/src/il2al/preprocess.ml +++ b/spectec/src/il2al/preprocess.ml @@ -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 diff --git a/spectec/src/xl/atom.ml b/spectec/src/xl/atom.ml index 73920e7ca3..2f1461a71a 100644 --- a/spectec/src/xl/atom.ml +++ b/spectec/src/xl/atom.ml @@ -41,6 +41,8 @@ and atom' = | EquivSub (* `==_` *) | Approx (* `~~` *) | ApproxSub (* `~~_` *) + | Sim (* `~` *) + | SimSub (* `~_` *) | SqArrow (* `~>` *) | SqArrowSub (* `~>_` *) | SqArrowStar (* `~>*` *) @@ -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 @@ -99,6 +101,7 @@ let sub atom1 atom2 = | EqualSub, Equal | EquivSub, Equiv | ApproxSub, Approx + | SimSub, Sim | SqArrowSub, SqArrow | SqArrowStarSub, SqArrowStar | PrecSub, Prec @@ -143,6 +146,8 @@ let to_string atom = | EquivSub -> "==_" | Approx -> "~~" | ApproxSub -> "~~_" + | Sim -> "~" + | SimSub -> "~_" | SqArrow -> "~>" | SqArrowSub -> "~>_" | SqArrowStar -> "~>*" @@ -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 *) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index c8ffe3263f..79bede2ef8 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -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{ @@ -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{ @@ -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{ @@ -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} @@ -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{ @@ -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{ @@ -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{ @@ -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} diff --git a/spectec/test-latex/test.spectec b/spectec/test-latex/test.spectec index a5e323673f..c1bd04f8e0 100644 --- a/spectec/test-latex/test.spectec +++ b/spectec/test-latex/test.spectec @@ -597,26 +597,38 @@ syntax C = {} relation Rok: C |- parent : OK relation Rsub: C |- parent <: parent relation Reval: parent; child ~> parent; child hint(tabular) +relation Rsim: parent ~ child hint(tabular) +relation Rsimsub: parent ~_C child hint(tabular) rule Rok: C |- AA : OK rule Rsub: C |- parent <: AA rule Reval: parent; child ~> AA; BB +rule Rsim: AA ~ BB +rule Rsimsub: AA ~_C BB relation Rok_macro: C |- parent : OK hint(macro "%ok") relation Rsub_macro: C |- parent <: parent hint(macro "%sub") relation Reval_macro: parent; child ~> parent; child hint(macro "%eval") hint(tabular) +relation Rsim_macro: parent ~ child hint(macro "%sim") hint(tabular) +relation Rsimsub_macro: parent ~_C child hint(macro "%sim_") hint(tabular) rule Rok_macro: C |- AA : OK rule Rsub_macro: C |- parent <: AA rule Reval_macro: parent; child ~> AA; BB +rule Rsim_macro: AA ~ BB +rule Rsimsub_macro: AA ~_C BB relation Rok_nomacro: C |- parent : OK hint(macro none) relation Rsub_nomacro: C |- parent <: parent hint(macro none) relation Reval_nomacro: parent; child ~> parent; child hint(macro none) hint(tabular) +relation Rsim_nomacro: parent ~ child hint(macro none) hint(tabular) +relation Rsimsub_nomacro: parent ~_C child hint(macro none) hint(tabular) rule Rok_nomacro: C |- AA : OK rule Rsub_nomacro: C |- parent <: AA rule Reval_nomacro: parent; child ~> AA; BB +rule Rsim_nomacro: AA ~ BB +rule Rsimsub_nomacro: AA ~_C BB ;;