Commit 74d267d9 authored by Dan Frumin's avatar Dan Frumin

Add multiplication to the language

parent c8680ca9
......@@ -11,7 +11,7 @@ Module lang.
Instance loc_dec_eq : EqDecision loc := _.
(** ** Expressions *)
Inductive binop := Add | Sub | Eq | Le | Lt | Xor.
Inductive binop := Mul | Add | Sub | Eq | Le | Lt | Xor.
Instance binop_dec_eq : EqDecision binop.
Proof. solve_decision. Defined.
......@@ -105,6 +105,7 @@ Module lang.
(* Notation for bool and nat *)
Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val :=
match op,v1,v2 with
| Mul, 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))
| Eq, LitV (Nat a), LitV (Nat b) => Some $ if decide (a = b) then LitV (Bool true) else LitV (Bool false)
......@@ -180,9 +181,9 @@ Module lang.
Instance binop_countable : Countable binop.
Proof.
refine (inj_countable' (λ op, match op with
| Add => 0 | Sub => 1 | Eq => 2 | Le => 3 | Lt => 4 | Xor => 5
| Mul => 0 | Add => 1 | Sub => 2 | Eq => 3 | Le => 4 | Lt => 5 | Xor => 6
end) (λ n, match n with
| 0 => Add | 1 => Sub | 2 => Eq | 3 => Le | 4 => Lt | _ => Xor
| 0 => Mul | 1 => Add | 2 => Sub | 3 => Eq | 4 => Le | 5 => Lt | _ => Xor
end) _); by intros [].
Qed.
......
......@@ -44,6 +44,8 @@ Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E)
(at level 30, right associativity) : expr_scope.
Notation "e1 × e2" := (BinOp Mul e1%E e2%E)
(at level 50, left associativity) : expr_scope.
Notation "e1 + e2" := (BinOp Add e1%E e2%E)
(at level 50, left associativity) : expr_scope.
Notation "e1 - e2" := (BinOp Sub e1%E e2%E)
......
......@@ -22,7 +22,7 @@ Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Fixpoint binop_nat_res_type (op : binop) : option type :=
match op with
| Add => Some TNat | Sub => Some TNat
| Mul => Some TNat | Add => Some TNat | Sub => Some TNat
| Eq => Some TBool | Le => Some TBool | Lt => Some TBool
| _ => None
end.
......
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