Commit b8cdcecd authored by Heiko Becker's avatar Heiko Becker

Add equality on booleans for expressions

parent 916cbfba
(**
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith.
Require Import Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
Set Implicit Arguments.
(**
......@@ -9,6 +9,15 @@ Set Implicit Arguments.
Define them first
**)
Inductive binop : Type := Plus | Sub | Mult | Div.
Definition binop_eq_bool (b1:binop) (b2:binop) :=
match b1 with
Plus => match b2 with Plus => true |_ => false end
| Sub => match b2 with Sub => true |_ => false end
| Mult => match b2 with Mult => true |_ => false end
| Div => match b2 with Div => true |_ => false end
end.
(**
Next define an evaluation function for binary operators on reals.
Errors are added on the expression evaluation level later.
......@@ -33,6 +42,30 @@ Inductive exp (V:Type): Type :=
| Const: V -> exp V
| Binop: binop -> exp V -> exp V -> exp V.
Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) :=
match e1 with
|Var _ v1 =>
match e2 with
|Var _ v2 => v1 =? v2
| _=> false
end
|Param _ v1 =>
match e2 with
|Param _ v2 => v1 =? v2
| _=> false
end
|Const n1 =>
match e2 with
|Const n2 => Qeq_bool n1 n2
| _=> false
end
|Binop b1 e11 e12 =>
match e2 with
|Binop b2 e21 e22 => andb (binop_eq_bool b1 b2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
|_ => false
end
end.
(**
Define a perturbation function to ease writing of basic definitions
**)
......
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