From a835a0ece8fe73261ae2c2725549fb8f9097bf93 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 30 May 2024 14:06:23 +0200 Subject: [PATCH] Add modulo operator --- spectec/doc/Language.md | 2 +- spectec/src/al/ast.ml | 1 + spectec/src/al/print.ml | 1 + spectec/src/backend-interpreter/interpreter.ml | 1 + spectec/src/backend-latex/render.ml | 1 + spectec/src/backend-prose/render.ml | 2 ++ spectec/src/el/ast.ml | 1 + spectec/src/el/print.ml | 1 + spectec/src/frontend/elab.ml | 1 + spectec/src/frontend/eval.ml | 3 +++ spectec/src/frontend/parser.mly | 1 + spectec/src/il/ast.ml | 1 + spectec/src/il/eval.ml | 3 +++ spectec/src/il/print.ml | 1 + spectec/src/il/valid.ml | 2 +- spectec/src/il2al/translate.ml | 1 + 16 files changed, 21 insertions(+), 2 deletions(-) diff --git a/spectec/doc/Language.md b/spectec/doc/Language.md index f8cfd761fe..ea739d04e4 100644 --- a/spectec/doc/Language.md +++ b/spectec/doc/Language.md @@ -154,7 +154,7 @@ exp ::= "##" exp remove possible parentheses (for syntax rewrites in hints) unop ::= notop | "+" | "-" -binop ::= logop | "+" | "-" | "*" | "/" | "^" +binop ::= logop | "+" | "-" | "*" | "/" | "\" | "^" arith ::= varid meta variable atom token diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml index 7fb553814e..f0d657e4cc 100644 --- a/spectec/src/al/ast.ml +++ b/spectec/src/al/ast.ml @@ -49,6 +49,7 @@ type binop = | SubOp (* `-` *) | MulOp (* `*` *) | DivOp (* `/` *) + | ModOp (* `\` *) | ExpOp (* `^` *) (* logical operation *) | ImplOp (* `=>` *) diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml index ad73ff6afe..5f7a7920fa 100644 --- a/spectec/src/al/print.ml +++ b/spectec/src/al/print.ml @@ -91,6 +91,7 @@ let string_of_binop = function | SubOp -> "-" | MulOp -> "ยท" | DivOp -> "/" + | ModOp -> "\\" | ExpOp -> "^" | EqOp -> "is" | NeOp -> "is not" diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml index d6575500a0..770e5adbdb 100644 --- a/spectec/src/backend-interpreter/interpreter.ml +++ b/spectec/src/backend-interpreter/interpreter.ml @@ -136,6 +136,7 @@ and eval_expr env expr = | SubOp, NumV i1, NumV i2 -> Z.sub i1 i2 |> numV | MulOp, NumV i1, NumV i2 -> Z.mul i1 i2 |> numV | DivOp, NumV i1, NumV i2 -> Z.div i1 i2 |> numV + | ModOp, NumV i1, NumV i2 -> Z.rem i1 i2 |> numV | ExpOp, NumV i1, NumV i2 -> Z.pow i1 (Z.to_int i2) |> numV | AndOp, BoolV b1, BoolV b2 -> boolV (b1 && b2) | OrOp, BoolV b1, BoolV b2 -> boolV (b1 || b2) diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index daa3c0112d..3ebc907f8f 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -830,6 +830,7 @@ let render_binop = function | SubOp -> "-" | MulOp -> "\\cdot" | DivOp -> "/" + | ModOp -> "\\mathbin{mod}" | ExpOp -> assert false let render_cmpop = function diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml index 3f4f78aac0..2d5060874b 100644 --- a/spectec/src/backend-prose/render.ml +++ b/spectec/src/backend-prose/render.ml @@ -44,6 +44,7 @@ let al_to_el_binop = function | Al.Ast.SubOp -> Some El.Ast.SubOp | Al.Ast.MulOp -> Some El.Ast.MulOp | Al.Ast.DivOp -> Some El.Ast.DivOp + | Al.Ast.ModOp -> Some El.Ast.ModOp | Al.Ast.ExpOp -> Some El.Ast.ExpOp | _ -> None @@ -247,6 +248,7 @@ let render_al_binop = function | Al.Ast.SubOp -> "minus" | Al.Ast.MulOp -> "multiplied by" | Al.Ast.DivOp -> "divided by" + | Al.Ast.ModOp -> "modulo" | Al.Ast.ExpOp -> "to the power of" | Al.Ast.EqOp -> "is" | Al.Ast.NeOp -> "is not" diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml index 3c9f771900..233c607f47 100644 --- a/spectec/src/el/ast.ml +++ b/spectec/src/el/ast.ml @@ -86,6 +86,7 @@ and binop = | SubOp (* `-` *) | MulOp (* `*` *) | DivOp (* `/` *) + | ModOp (* `\` *) | ExpOp (* `^` *) and cmpop = diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml index e2fbd3e643..7b6529923a 100644 --- a/spectec/src/el/print.ml +++ b/spectec/src/el/print.ml @@ -41,6 +41,7 @@ let string_of_binop = function | SubOp -> "-" | MulOp -> "*" | DivOp -> "/" + | ModOp -> "\\" | ExpOp -> "^" let string_of_cmpop = function diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index ff7672392d..48193d981b 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -511,6 +511,7 @@ let infer_binop' = function | SubOp -> infer_numop (fun t -> Il.SubOp t) numtyps | MulOp -> infer_numop (fun t -> Il.MulOp t) numtyps | DivOp -> infer_numop (fun t -> Il.DivOp t) numtyps + | ModOp -> infer_numop (fun t -> Il.ModOp t) numtyps | ExpOp -> infer_numop (fun t -> Il.ExpOp t) numtyps let infer_cmpop' = function diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml index f29bbd82b8..71bd70484a 100644 --- a/spectec/src/frontend/eval.ml +++ b/spectec/src/frontend/eval.ml @@ -174,6 +174,9 @@ and reduce_exp env e : exp = | DivOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.(n1 / n2)) $ e.at | DivOp, NatE (_, z0), _ when z0 = Z.zero -> e1' | DivOp, _, NatE (_, z1) when z1 = Z.one -> e1' + | ModOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.rem n1 n2) $ e.at + | ModOp, NatE (_, z0), _ when z0 = Z.zero -> e1' + | ModOp, _, NatE (op, z1) when z1 = Z.one -> NatE (op, Z.zero) $ e.at | ExpOp, NatE (op, n1), NatE (_, n2) -> NatE (op, Z.(n1 ** to_int n2)) $ e.at | ExpOp, NatE (_, z01), _ when z01 = Z.zero || z01 = Z.one -> e1' | ExpOp, _, NatE (op, z0) when z0 = Z.zero -> NatE (op, Z.one) $ e.at diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly index 84d39c7822..fe9615196f 100644 --- a/spectec/src/frontend/parser.mly +++ b/spectec/src/frontend/parser.mly @@ -293,6 +293,7 @@ check_atom : | MINUS { SubOp } | STAR { MulOp } | SLASH { DivOp } + | BACKSLASH { ModOp } %inline cmpop : | EQ { EqOp } diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml index 88c3d5003f..1d7720d001 100644 --- a/spectec/src/il/ast.ml +++ b/spectec/src/il/ast.ml @@ -67,6 +67,7 @@ and binop = | SubOp of numtyp (* `-` *) | MulOp of numtyp (* `*` *) | DivOp of numtyp (* `/` *) + | ModOp of numtyp (* `\` *) | ExpOp of numtyp (* `^` *) and cmpop = diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index 92eef52474..9bc378e4ea 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml @@ -160,6 +160,9 @@ and reduce_exp env e : exp = | DivOp _, NatE n1, NatE n2 -> NatE Z.(n1 / n2) $> e | DivOp _, NatE z0, _ when z0 = Z.zero -> e1' | DivOp _, _, NatE z1 when z1 = Z.one -> e1' + | ModOp _, NatE n1, NatE n2 -> NatE Z.(rem n1 n2) $> e + | ModOp _, NatE z0, _ when z0 = Z.zero -> e1' + | ModOp _, _, NatE z1 when z1 = Z.one -> NatE Z.zero $> e | ExpOp _, NatE n1, NatE n2 -> NatE Z.(n1 ** to_int n2) $> e | ExpOp _, NatE z01, _ when z01 = Z.zero || z01 = Z.one -> e1' | ExpOp _, _, NatE z0 when z0 = Z.zero -> NatE Z.one $> e diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index 062b8962cf..7f5a479b21 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -28,6 +28,7 @@ let string_of_binop = function | SubOp _ -> "-" | MulOp _ -> "*" | DivOp _ -> "/" + | ModOp _ -> "\\" | ExpOp _ -> "^" let string_of_cmpop = function diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml index 45ba90c446..8fac3f1483 100644 --- a/spectec/src/il/valid.ml +++ b/spectec/src/il/valid.ml @@ -149,7 +149,7 @@ let infer_unop = function let infer_binop = function | AndOp | OrOp | ImplOp | EquivOp -> BoolT, BoolT, BoolT - | AddOp t | SubOp t | MulOp t | DivOp t -> NumT t, NumT t, NumT t + | AddOp t | SubOp t | MulOp t | DivOp t | ModOp t -> NumT t, NumT t, NumT t | ExpOp t -> NumT t, NumT NatT, NumT t let infer_cmpop = function diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index bb4d28ccb8..469de4dd1a 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -159,6 +159,7 @@ and translate_exp exp = | Il.SubOp _ -> SubOp | Il.MulOp _ -> MulOp | Il.DivOp _ -> DivOp + | Il.ModOp _ -> ModOp | Il.ExpOp _ -> ExpOp | Il.AndOp -> AndOp | Il.OrOp -> OrOp