Library language
Require Export ZArith.
Require Export Coq.Lists.List.
Require Export Coq.Bool.Bool.
Require Export Coq.Lists.List.
Require Export Coq.Bool.Bool.
This file contains the language. It includes
syntax
syntactic equality (which we need for subtraction and subset in some of the
two implication rules)
substitution functions
free variable functions
a function to determine modified variables
It also contains some of the semantics rules. It needs these because they are required for expression evaluation which is required by the two assertions and the evidence.
Finally there are functions that evaluate expressions given a state.
It also contains some of the semantics rules. It needs these because they are required for expression evaluation which is required by the two assertions and the evidence.
Finally there are functions that evaluate expressions given a state.
following is for conveninece in declarations and proofs
Ltac inv H := inversion H; subst; clear H.
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Three types of skal variables, A B and H
Skalvar is union of the three
Inductive ASkal:Type :=
AId : Z -> ASkal.
Inductive BSkal:Type :=
BId : Z -> BSkal.
Inductive HSkal:Type :=
HId : Z -> HSkal.
Inductive SkalVar: Type :=
ASkalVar: ASkal -> SkalVar
|BSkalVar: BSkal -> SkalVar
|HSkalVar: HSkal -> SkalVar.
Definition beq_SkalVar var1 var2 : bool :=
match (var1, var2) with
(ASkalVar (AId n1), ASkalVar (AId n2)) => Zeq_bool n1 n2
| (BSkalVar (BId n1), BSkalVar (BId n2)) => Zeq_bool n1 n2
| (HSkalVar (HId n1), HSkalVar (HId n2)) => Zeq_bool n1 n2
| _ => false
end.
Definition HArray := list (prod Z Z).
Definition AVal:Type := Z.
Definition BVal: Type := bool.
Definition HVal:Type := HArray.
Inductive Val :=
AValue: AVal->Val
| BValue: BVal->Val
| HValue: HVal->Val.
Inductive AOp :=
aplus
| aminus
| amult.
Definition AOp_Eq o1 o2:=
match o1,o2 with
aplus, aplus => true
| aminus,aminus => true
| amult, amult => true
| _, _ => false end.
Lemma AOp_Eq_Eq : forall o1 o2, AOp_Eq o1 o2 = true <-> o1 = o2.
Proof.
intros. split; intros. destruct o1; destruct o2; inv H; auto.
subst. destruct o2; auto.
Qed.
Definition AopInter (a:AOp)(v w: AVal) : AVal:=
match a with
aplus => Zplus v w
| aminus => Zminus v w
| amult => Zmult v w
end.
Inductive BOp :=
| blt
| bgt
| ble
| bge
| beql
| bneql.
Definition BEqCompare c1 c2 :=
match c1, c2 with
Eq, Eq => true
| Lt, Lt => true
| Gt, Gt => true
| _, _ => false
end.
Definition BOpInter b v w :=
match b with
| blt => BEqCompare (Zcompare v w) Lt
| bgt => BEqCompare (Zcompare v w) Gt
| ble => negb (BEqCompare (Zcompare v w) Gt)
| bge => negb (BEqCompare (Zcompare v w) Lt)
| beql => (BEqCompare (Zcompare v w) Eq)
| bneql => negb ((BEqCompare (Zcompare v w) Eq))
end.
Definition BOp_Eq o1 o2 :=
match o1, o2 with
blt, blt => true
| bgt, bgt => true
| ble, ble => true
| bge, bge => true
| beql, beql => true
| bneql, bneql => true
| _, _ => false
end.
Lemma BOp_Eq_Eq : forall o1 o2, BOp_Eq o1 o2 = true <-> o1 = o2.
Proof.
intros. split; intros. destruct o1; destruct o2; inv H; auto.
subst. destruct o2; auto.
Qed.
AId : Z -> ASkal.
Inductive BSkal:Type :=
BId : Z -> BSkal.
Inductive HSkal:Type :=
HId : Z -> HSkal.
Inductive SkalVar: Type :=
ASkalVar: ASkal -> SkalVar
|BSkalVar: BSkal -> SkalVar
|HSkalVar: HSkal -> SkalVar.
Definition beq_SkalVar var1 var2 : bool :=
match (var1, var2) with
(ASkalVar (AId n1), ASkalVar (AId n2)) => Zeq_bool n1 n2
| (BSkalVar (BId n1), BSkalVar (BId n2)) => Zeq_bool n1 n2
| (HSkalVar (HId n1), HSkalVar (HId n2)) => Zeq_bool n1 n2
| _ => false
end.
Definition HArray := list (prod Z Z).
Definition AVal:Type := Z.
Definition BVal: Type := bool.
Definition HVal:Type := HArray.
Inductive Val :=
AValue: AVal->Val
| BValue: BVal->Val
| HValue: HVal->Val.
Inductive AOp :=
aplus
| aminus
| amult.
Definition AOp_Eq o1 o2:=
match o1,o2 with
aplus, aplus => true
| aminus,aminus => true
| amult, amult => true
| _, _ => false end.
Lemma AOp_Eq_Eq : forall o1 o2, AOp_Eq o1 o2 = true <-> o1 = o2.
Proof.
intros. split; intros. destruct o1; destruct o2; inv H; auto.
subst. destruct o2; auto.
Qed.
Definition AopInter (a:AOp)(v w: AVal) : AVal:=
match a with
aplus => Zplus v w
| aminus => Zminus v w
| amult => Zmult v w
end.
Inductive BOp :=
| blt
| bgt
| ble
| bge
| beql
| bneql.
Definition BEqCompare c1 c2 :=
match c1, c2 with
Eq, Eq => true
| Lt, Lt => true
| Gt, Gt => true
| _, _ => false
end.
Definition BOpInter b v w :=
match b with
| blt => BEqCompare (Zcompare v w) Lt
| bgt => BEqCompare (Zcompare v w) Gt
| ble => negb (BEqCompare (Zcompare v w) Gt)
| bge => negb (BEqCompare (Zcompare v w) Lt)
| beql => (BEqCompare (Zcompare v w) Eq)
| bneql => negb ((BEqCompare (Zcompare v w) Eq))
end.
Definition BOp_Eq o1 o2 :=
match o1, o2 with
blt, blt => true
| bgt, bgt => true
| ble, ble => true
| bge, bge => true
| beql, beql => true
| bneql, bneql => true
| _, _ => false
end.
Lemma BOp_Eq_Eq : forall o1 o2, BOp_Eq o1 o2 = true <-> o1 = o2.
Proof.
intros. split; intros. destruct o1; destruct o2; inv H; auto.
subst. destruct o2; auto.
Qed.
Expression declarations. H and A can contain eachother so we
need to generate a new inductive hypothesis for them
Inductive HExpr :=
HvarExpr : HSkal -> HExpr
| HemptyExpr : HExpr
| HupdateExpr : HExpr -> AExpr -> AExpr -> HExpr
with
AExpr :=
SvarExpr: ASkal -> AExpr
| IntExpr: AVal -> AExpr
| AopExpr: AExpr -> AOp -> AExpr -> AExpr
| ArrayAccess : HExpr -> AExpr -> AExpr.
Inductive BExpr :=
BvarExpr: BSkal -> BExpr
| BvalExpr:BVal -> BExpr
| BopExpr: AExpr -> BOp -> AExpr -> BExpr
| AndExpr: BExpr -> BExpr -> BExpr
| OrExpr: BExpr -> BExpr -> BExpr
| NotExpr: BExpr -> BExpr.
Scheme HExpr_ind_mut := Induction for HExpr Sort Type
with
AExpr_ind_mut := Induction for AExpr Sort Type.
Notation "x 'b&&' y" := (AndExpr x y) (at level 80, right associativity).
Notation "x 'b||' y" := (OrExpr x y) (at level 80, right associativity).
Notation "! x" := (NotExpr x) (at level 70).
Inductive Expr :=
| AExp : AExpr -> Expr
| BExp : BExpr -> Expr
| HExp : HExpr -> Expr.
Commands and their notations
Inductive Command :=
Skip: Command
| Seq: Command -> Command -> Command
| Assign: SkalVar -> Expr -> Command
| Assert: BExpr -> Command
| Cond: BExpr -> Command -> Command -> Command
| While : BExpr -> Command -> Command
| For : ASkal -> ASkal -> Command -> Command .
Notation "l '::=' a" :=
(Assign l a) (at level 60).
Notation "c1 ; c2" :=
(Seq c1 c2) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(Cond e1 e2 e3) (at level 80, right associativity).
Notation "'ASSERT' x" := (Assert x) (at level 50).
Notation "'WHILE' b 'DO' c" := (While b c) (at level 50).
Notation "'FOR' b '=1TO' z 'DO' c" := (For b z c) (at level 50).
Fixpoint hValToHExpr (v :HVal) : HExpr :=
match v with
(a,b)::t => HupdateExpr (hValToHExpr t) (IntExpr a) (IntExpr b)
| [] => HemptyExpr end.
Skip: Command
| Seq: Command -> Command -> Command
| Assign: SkalVar -> Expr -> Command
| Assert: BExpr -> Command
| Cond: BExpr -> Command -> Command -> Command
| While : BExpr -> Command -> Command
| For : ASkal -> ASkal -> Command -> Command .
Notation "l '::=' a" :=
(Assign l a) (at level 60).
Notation "c1 ; c2" :=
(Seq c1 c2) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
(Cond e1 e2 e3) (at level 80, right associativity).
Notation "'ASSERT' x" := (Assert x) (at level 50).
Notation "'WHILE' b 'DO' c" := (While b c) (at level 50).
Notation "'FOR' b '=1TO' z 'DO' c" := (For b z c) (at level 50).
Fixpoint hValToHExpr (v :HVal) : HExpr :=
match v with
(a,b)::t => HupdateExpr (hValToHExpr t) (IntExpr a) (IntExpr b)
| [] => HemptyExpr end.
Substitution. We need a function to substitute each type into each other type
Fixpoint ASubstA (e:AExpr) (a: AExpr) (x:SkalVar) : AExpr :=
match e with
SvarExpr y => if beq_SkalVar x (ASkalVar y) then a
else e
| IntExpr _ => e
| AopExpr A1 op A2 => AopExpr (ASubstA A1 a x) op (ASubstA A2 a x)
| ArrayAccess h a1 => ArrayAccess (HSubstA h a x) (ASubstA a1 a x)
end
with
HSubstA (e:HExpr) (a: AExpr) (x:SkalVar) : HExpr :=
match e with
HvarExpr v => e
| HemptyExpr => e
| HupdateExpr h a1 a2 => HupdateExpr (HSubstA h a x) (ASubstA a1 a x) (ASubstA a2 a x)
end.
Fixpoint ASubstH (e:AExpr) (h:HExpr) (x:SkalVar) :=
match e with
ArrayAccess h1 a => ArrayAccess (HSubstH h1 h x) (ASubstH a h x)
| AopExpr A1 op A2 => AopExpr (ASubstH A1 h x) op (ASubstH A2 h x)
| _ => e
end
with HSubstH (e:HExpr) (h:HExpr) (x:SkalVar) :=
match e with
HvarExpr v => if beq_SkalVar x (HSkalVar v) then h else e
| HemptyExpr => e
| HupdateExpr h1 a a1 => HupdateExpr (HSubstH h1 h x) (ASubstH a h x) (ASubstH a1 h x)
end.
Fixpoint BSubstB (e:BExpr) (a: BExpr) (x:SkalVar) : BExpr :=
match e with
BvarExpr v => if beq_SkalVar x (BSkalVar v) then a else e
| BvalExpr b => e
| BopExpr a1 op a2 => e
| AndExpr b1 b2 => AndExpr (BSubstB b1 a x) (BSubstB b2 a x)
| OrExpr b1 b2 => OrExpr (BSubstB b1 a x) (BSubstB b2 a x)
| NotExpr b => NotExpr (BSubstB b a x)
end.
Fixpoint BSubstA (e:BExpr) (a: AExpr) (x:SkalVar) : BExpr :=
match e with
BvarExpr v => e
| BvalExpr b => e
| BopExpr a1 op a2 => BopExpr (ASubstA a1 a x) op (ASubstA a2 a x)
| AndExpr b1 b2 => AndExpr (BSubstA b1 a x) (BSubstA b2 a x)
| OrExpr b1 b2 => OrExpr (BSubstA b1 a x) (BSubstA b2 a x)
| NotExpr b => NotExpr (BSubstA b a x)
end.
Fixpoint BSubstH (e:BExpr) (h:HExpr) (x:SkalVar) : BExpr :=
match e with
BvarExpr v => e
| BvalExpr b => e
| BopExpr a1 op a2 => BopExpr (ASubstH a1 h x) op (ASubstH a2 h x)
| AndExpr b1 b2 => AndExpr (BSubstH b1 h x) (BSubstH b2 h x)
| OrExpr b1 b2 => OrExpr (BSubstH b1 h x) (BSubstH b2 h x)
| NotExpr b => NotExpr (BSubstH b h x)
end.
Definition SubstH (e:Expr) (h: HExpr) (x:SkalVar) : Expr :=
match e with
AExp ae => AExp (ASubstH ae h x)
| BExp be => BExp (BSubstH be h x)
| HExp he => HExp (HSubstH he h x)
end.
Definition SubstA (e:Expr) (a: AExpr) (x:SkalVar) : Expr :=
match e with
AExp ae => AExp (ASubstA ae a x)
| BExp be => BExp (BSubstA be a x)
| HExp he => HExp (HSubstA he a x)
end.
Definition SubstB (e:Expr) (B: BExpr) (x:SkalVar) : Expr :=
match e with
| BExp be => BExp (BSubstB be B x)
| _ => e
end.
Mods takes a command and determines what variables are
modified by the command. This is all of the variables on the
left hand side of an assign. We use this function instead of
the mods only evidence.
Fixpoint Mods (cmd: Command) : list SkalVar :=
match cmd with
| Skip => nil
| Seq c1 c2 => (Mods c1) ++ (Mods c2)
| Assign x _ => [x]
| Assert _ => []
| Cond _ c1 c2 => (Mods c1) ++ (Mods c2)
| While _ c => Mods c
| For av _ c => [ASkalVar av] ++ Mods c
end.
match cmd with
| Skip => nil
| Seq c1 c2 => (Mods c1) ++ (Mods c2)
| Assign x _ => [x]
| Assert _ => []
| Cond _ c1 c2 => (Mods c1) ++ (Mods c2)
| While _ c => Mods c
| For av _ c => [ASkalVar av] ++ Mods c
end.
Calculates free variables in expressions. One for each type
Fixpoint AFv (exp: AExpr) : list SkalVar :=
match exp with
| SvarExpr x => [ASkalVar x]
| IntExpr _ => []
| AopExpr e1 _ e2 => (AFv e1) ++ (AFv e2)
| ArrayAccess h a => (HFv h) ++ (AFv a) end
with
HFv exp :=
match exp with
| HvarExpr x => [HSkalVar x]
| HemptyExpr => []
| HupdateExpr h a1 a2 => (HFv h) ++ (AFv a1) ++ (AFv a2)
end.
Fixpoint BFv (exp: BExpr) : list SkalVar :=
match exp with
| BvarExpr x => [BSkalVar x]
| BvalExpr _ => []
| BopExpr e1 _ e2 => (AFv e1) ++ (AFv e2)
| AndExpr e1 e2 => (BFv e1) ++ (BFv e2)
| OrExpr e1 e2 => (BFv e1) ++ (BFv e2)
| NotExpr e => BFv e end.
Definition fv (exp: Expr) : list SkalVar :=
match exp with
| AExp ae => AFv ae
| BExp be => BFv be
| HExp he => HFv he
end.
Fixpoint AFvList A :=
match A with
[] => []
| h::t => AFv h ++ (AFvList t)
end.
match exp with
| SvarExpr x => [ASkalVar x]
| IntExpr _ => []
| AopExpr e1 _ e2 => (AFv e1) ++ (AFv e2)
| ArrayAccess h a => (HFv h) ++ (AFv a) end
with
HFv exp :=
match exp with
| HvarExpr x => [HSkalVar x]
| HemptyExpr => []
| HupdateExpr h a1 a2 => (HFv h) ++ (AFv a1) ++ (AFv a2)
end.
Fixpoint BFv (exp: BExpr) : list SkalVar :=
match exp with
| BvarExpr x => [BSkalVar x]
| BvalExpr _ => []
| BopExpr e1 _ e2 => (AFv e1) ++ (AFv e2)
| AndExpr e1 e2 => (BFv e1) ++ (BFv e2)
| OrExpr e1 e2 => (BFv e1) ++ (BFv e2)
| NotExpr e => BFv e end.
Definition fv (exp: Expr) : list SkalVar :=
match exp with
| AExp ae => AFv ae
| BExp be => BFv be
| HExp he => HFv he
end.
Fixpoint AFvList A :=
match A with
[] => []
| h::t => AFv h ++ (AFvList t)
end.
Collects all fre variables in a command's expressions
Fixpoint varsUsedIn (C: Command) : list SkalVar :=
match C with
Skip => []
| Seq C1 C2 => (varsUsedIn C1) ++ (varsUsedIn C2)
| Assign _ e => (fv e)
| Assert e => (fv (BExp e))
| Cond b C1 C2 => (fv (BExp b)) ++
(varsUsedIn C1) ++
(varsUsedIn C2)
| While b C => (BFv b) ++ (varsUsedIn C)
| For a _ C => [ASkalVar a] ++ varsUsedIn C
end.
Fixpoint skalVarIn (x: SkalVar) (vs :list SkalVar) : bool :=
match vs with
| h::t => if beq_SkalVar x h then true else (skalVarIn x t)
| [] => false end.
Fixpoint allVarsIn (v1 : list SkalVar) (v2 : list SkalVar) : bool :=
match v1 with
| h::t => if (skalVarIn h v2) then allVarsIn t v2 else false
| [] => true end.
match C with
Skip => []
| Seq C1 C2 => (varsUsedIn C1) ++ (varsUsedIn C2)
| Assign _ e => (fv e)
| Assert e => (fv (BExp e))
| Cond b C1 C2 => (fv (BExp b)) ++
(varsUsedIn C1) ++
(varsUsedIn C2)
| While b C => (BFv b) ++ (varsUsedIn C)
| For a _ C => [ASkalVar a] ++ varsUsedIn C
end.
Fixpoint skalVarIn (x: SkalVar) (vs :list SkalVar) : bool :=
match vs with
| h::t => if beq_SkalVar x h then true else (skalVarIn x t)
| [] => false end.
Fixpoint allVarsIn (v1 : list SkalVar) (v2 : list SkalVar) : bool :=
match v1 with
| h::t => if (skalVarIn h v2) then allVarsIn t v2 else false
| [] => true end.
We define a state as a triple with three functions from skalVars to options
of their respective valuse. We update by adding a function around the
old state. If the variable doesn't exist we get none.
Definition AState: Type := ASkal -> option AVal.
Definition BState: Type := BSkal -> option BVal.
Definition HState: Type := HSkal -> option HVal.
Definition State: Type := prod (prod AState BState) HState.
Definition aUpdate (S: State)(x: ASkal)(v:AVal): State :=
match S with
| ((aS, bS), hS) =>
((fun y => (if beq_SkalVar (ASkalVar x) (ASkalVar y) then Some v else aS y),bS),hS)
end.
Definition bUpdate (S: State)(x: BSkal)(v:BVal): State :=
match S with
| ((aS, bS),hS) => ((aS, fun y => (if beq_SkalVar (BSkalVar x) (BSkalVar y) then Some v else bS y)),hS)
end.
Definition hUpdate (S:State)(x:HSkal)(v:HVal) : State :=
match S with
| ((aS, bS),hS) => ((aS,bS), fun y => (if beq_SkalVar (HSkalVar x) (HSkalVar y) then Some v else hS y))
end.
Definition lookup (S:State)(x:SkalVar): option Val :=
match x with
| ASkalVar a => match ((fst (fst S)) a) with Some v => Some (AValue v) | None => None end
| BSkalVar b => match ((snd (fst S)) b) with Some v => Some (BValue v) | None => None end
| HSkalVar h => match ((snd S) h) with Some v => Some (HValue v) | None => None end
end.
Lemma lookupNeqa : forall s x y v, beq_SkalVar (ASkalVar y) (x) = false -> lookup (aUpdate s y v) (x) = lookup s x.
Proof.
intros.
destruct s. destruct p. simpl. destruct x; simpl; auto. rewrite H. auto.
Qed.
Lemma lookupNeqb : forall s x y v, beq_SkalVar (BSkalVar y) (x) = false -> lookup (bUpdate s y v) (x) = lookup s x.
Proof.
intros.
destruct s. destruct p. simpl. destruct x; simpl; auto. rewrite H. auto.
Qed.
Lemma lookupNeqh : forall s x y v, beq_SkalVar (HSkalVar y) (x) = false -> lookup (hUpdate s y v) (x) = lookup s x.
Proof.
intros.
destruct s. destruct p. simpl. destruct x; simpl; auto. rewrite H. auto.
Qed.
Fixpoint allInDomain X s :=
match X with
| [] => true
| h::t => match (lookup s h) with
| Some _ => allInDomain t s
| None => false
end
end.
Our representation of an array is a list of pairs of two AValues. When we
modify a value we just put a new value at the front of the list. When
we access the array we take the first key that matches
Fixpoint AccessArray (h: HArray) (z:Z) :=
match h with
(a,b)::t => if (Z_eq_dec z a) then b else AccessArray t z
| [] => 0%Z
end.
Definition UpdateArray (h: HArray) a a1 :=
(a,a1)::h.
match h with
(a,b)::t => if (Z_eq_dec z a) then b else AccessArray t z
| [] => 0%Z
end.
Definition UpdateArray (h: HArray) a a1 :=
(a,a1)::h.
Evaluation function
Fixpoint AEval (A:AExpr)(s:State) : option AVal :=
match A with
SvarExpr x => match ((fst (fst s)) x) with Some (v) => Some v | _ => None end
| IntExpr i => Some i
| AopExpr A1 op A2 => match (AEval A1 s), (AEval A2 s) with
Some v1, Some v2 => Some (AopInter op v1 v2)
| _ , _ => None
end
| ArrayAccess h a => match (AEval a s), (HEval h s) with Some v, Some v1 => Some (AccessArray v1 v) | _, _ => None end
end
with HEval (H:HExpr)(s:State) : option HVal :=
match H with
| HvarExpr x => (snd s) x
| HemptyExpr => Some []
| HupdateExpr h a a1 => match (AEval a s), (AEval a1 s), (HEval h s) with
Some v, Some v1, Some v3 => Some (UpdateArray v3 v v1)
| _, _, _ => None end
end.
Fixpoint BEval (B:BExpr)(s:State) : option BVal :=
match B with
BvarExpr x => match ((snd (fst s)) x) with Some (v) => Some v | _ => None end
| BvalExpr b => Some b
| BopExpr a1 op a2 => (match (AEval a1 s, AEval a2 s) with
(Some v1, Some v2) => Some (BOpInter op v1 v2)
| _ => None end )
| AndExpr b1 b2 => (match (BEval b1 s, BEval b2 s) with
(Some t1, Some t2) => Some((t1 && t2)%bool)
| _ => None end)
| OrExpr b1 b2 => (match (BEval b1 s, BEval b2 s) with
(Some t1, Some t2) => Some((t1 || t2)%bool)
| _ => None end)
| NotExpr b => (match BEval b s with Some t => Some (negb t) | None => None end)
end.
Fixpoint Eval E s : option Val :=
match E with
AExp A => (match AEval A s with
Some a => Some (AValue a)
| None => None end)
| BExp B => (match BEval B s with
Some b => Some (BValue b)
| None => None end)
| HExp H => (match HEval H s with
Some h => Some (HValue h)
| None => None end)
end.
match A with
SvarExpr x => match ((fst (fst s)) x) with Some (v) => Some v | _ => None end
| IntExpr i => Some i
| AopExpr A1 op A2 => match (AEval A1 s), (AEval A2 s) with
Some v1, Some v2 => Some (AopInter op v1 v2)
| _ , _ => None
end
| ArrayAccess h a => match (AEval a s), (HEval h s) with Some v, Some v1 => Some (AccessArray v1 v) | _, _ => None end
end
with HEval (H:HExpr)(s:State) : option HVal :=
match H with
| HvarExpr x => (snd s) x
| HemptyExpr => Some []
| HupdateExpr h a a1 => match (AEval a s), (AEval a1 s), (HEval h s) with
Some v, Some v1, Some v3 => Some (UpdateArray v3 v v1)
| _, _, _ => None end
end.
Fixpoint BEval (B:BExpr)(s:State) : option BVal :=
match B with
BvarExpr x => match ((snd (fst s)) x) with Some (v) => Some v | _ => None end
| BvalExpr b => Some b
| BopExpr a1 op a2 => (match (AEval a1 s, AEval a2 s) with
(Some v1, Some v2) => Some (BOpInter op v1 v2)
| _ => None end )
| AndExpr b1 b2 => (match (BEval b1 s, BEval b2 s) with
(Some t1, Some t2) => Some((t1 && t2)%bool)
| _ => None end)
| OrExpr b1 b2 => (match (BEval b1 s, BEval b2 s) with
(Some t1, Some t2) => Some((t1 || t2)%bool)
| _ => None end)
| NotExpr b => (match BEval b s with Some t => Some (negb t) | None => None end)
end.
Fixpoint Eval E s : option Val :=
match E with
AExp A => (match AEval A s with
Some a => Some (AValue a)
| None => None end)
| BExp B => (match BEval B s with
Some b => Some (BValue b)
| None => None end)
| HExp H => (match HEval H s with
Some h => Some (HValue h)
| None => None end)
end.