Commit 8294ac2d authored by Dan Frumin's avatar Dan Frumin

Add quot and rem operations

parent f1a8bd8d
...@@ -11,7 +11,8 @@ Module lang. ...@@ -11,7 +11,8 @@ Module lang.
Instance loc_dec_eq : EqDecision loc := _. Instance loc_dec_eq : EqDecision loc := _.
(** ** Expressions *) (** ** Expressions *)
Inductive binop := Mul | Add | Sub | Eq | Le | Lt | Xor. Inductive binop :=
Mul | Add | Sub | Quot | Rem | Eq | Le | Lt | Xor.
Instance binop_dec_eq : EqDecision binop. Instance binop_dec_eq : EqDecision binop.
Proof. solve_decision. Defined. Proof. solve_decision. Defined.
...@@ -108,6 +109,8 @@ Module lang. ...@@ -108,6 +109,8 @@ Module lang.
| Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b)) | Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b))
| Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b)) | Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b))
| Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b)) | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
| Quot, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a / b)%nat)
| Rem, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a `mod` b))
| Eq, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if decide (a = b) then true else false)) | Eq, LitV (Nat a), LitV (Nat b) => Some $ LitV (Bool (if decide (a = b) then true else false))
| Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b)) | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
| Eq, LitV (Loc l1), LitV (Loc l2) => Some $ LitV (Bool (if decide (l1 = l2) then true else false)) | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ LitV (Bool (if decide (l1 = l2) then true else false))
...@@ -181,9 +184,9 @@ Module lang. ...@@ -181,9 +184,9 @@ Module lang.
Instance binop_countable : Countable binop. Instance binop_countable : Countable binop.
Proof. Proof.
refine (inj_countable' (λ op, match op with refine (inj_countable' (λ op, match op with
| Mul => 0 | Add => 1 | Sub => 2 | Eq => 3 | Le => 4 | Lt => 5 | Xor => 6 | Mul => 0 | Add => 1 | Sub => 2 | Eq => 3 | Le => 4 | Lt => 5 | Xor => 6 | Quot => 7 | Rem => 8
end) (λ n, match n with end) (λ n, match n with
| 0 => Mul | 1 => Add | 2 => Sub | 3 => Eq | 4 => Le | 5 => Lt | _ => Xor | 0 => Mul | 1 => Add | 2 => Sub | 3 => Eq | 4 => Le | 5 => Lt | 6 => Xor | 7 => Quot | _ => Rem
end) _); by intros []. end) _); by intros [].
Qed. Qed.
......
...@@ -61,6 +61,9 @@ Notation "e1 = e2" := (BinOp Eq e1%E e2%E) (at level 70) : expr_scope. ...@@ -61,6 +61,9 @@ Notation "e1 = e2" := (BinOp Eq e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope. Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope.
Notation "¬ e" := (BinOp Xor e%E (Lit (Bool true))) (at level 75, right associativity) : expr_scope. Notation "¬ e" := (BinOp Xor e%E (Lit (Bool true))) (at level 75, right associativity) : expr_scope.
Notation "e1 / e2" := (BinOp Quot e1%E e2%E) : expr_scope.
Notation "e1 `mod` e2" := (BinOp Rem e1%E e2%E) : expr_scope.
(* The unicode is already part of the notation "_ ← _; _" for bind. *) (* The unicode is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment