Commit 77737f5f authored by Raphaël Monat's avatar Raphaël Monat

Adding typing of expression (WIP)

parent 8768d1b7
(**
Right now, we need to know the types of each expression in the
~validErrorbound~ function (otherwise, it is impossible to know which
epsilon to use to check the error bounds). For now, expressions are
only typed for the variables and downcasting operators.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.RealRationalProps Daisy.Expressions.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
(**
Now we want a TypeEnv function, taking an expression and returning a exp -> option mType
Soundness property is: TypeEnv e = T -> eval_exp e E v m -> T e = m.
**)
(** A good function computing a map of expression types **)
Fixpoint typeExpression (e:exp Q) (e':exp Q) : option mType :=
match e with
| Var _ m n => if expEqBool e e' then Some m else None
| Const m n => if expEqBool e e' then Some m else None
| Unop u e1 =>
let tE1 := typeExpression e1 in
if expEqBool e e' then (tE1 e1)
else (tE1 e')
| Binop b e1 e2 =>
let tE1 := typeExpression e1 in
let tE2 := typeExpression e2 in
let m := match (tE1 e1), (tE2 e2) with
|Some m1, Some m2 => Some (computeJoin m1 m2)
|_, _ => None
end in
if expEqBool e e' then m
else match (tE1 e'), (tE2 e') with
|Some m1, Some m2 => if (mTypeEqBool m1 m2) then
Some m1
else
None
|Some m1, None => Some m1
|None, Some m2 => Some m2
|None, None => None
end
| Downcast m e1 =>
let tE1 := typeExpression e1 in
let m := match (tE1 e1) with
| Some m1 => if (isMorePrecise m1 m) then Some m else None
| _ => None
end in
if expEqBool e e' then m
else (tE1 e')
end.
Lemma detTypingBinop (f1 f2: exp Q) (b:binop) (m m0 m1 m2: mType) x:
typeExpression (Binop b f1 f2) (Var Q m0 x) = Some m ->
typeExpression f1 (Var Q m0 x) = Some m1 ->
typeExpression f2 (Var Q m0 x) = Some m2 ->
m = m1 /\ m = m2.
Proof.
intros.
split; simpl in *; rewrite H0, H1 in H.
- case_eq (mTypeEqBool m1 m2); intros; auto; rewrite H2 in H.
+ apply EquivEqBoolEq in H2; subst.
assert (mTypeEqBool m2 m2 = true) by (apply EquivEqBoolEq; auto).
inversion H; auto.
+ inversion H.
- case_eq (mTypeEqBool m1 m2); intros; auto; rewrite H2 in H.
+ apply EquivEqBoolEq in H2; subst.
assert (mTypeEqBool m2 m2 = true) by (apply EquivEqBoolEq; auto).
inversion H; auto.
+ inversion H.
Qed.
Eval compute in (typeExpression (Binop Plus (Unop Neg (Var Q M32 1)) (Var Q M64 2)) (Var Q M32 1)).
Lemma typeExpressionIsSound e E v m:
eval_exp E (toRExp e) v m ->
(typeExpression e) e = Some m.
Proof.
revert e E v m; induction e; intros; inversion H; simpl in *; subst.
- assert (mTypeEqBool m0 m0 && (n =? n) = true) by (apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto).
rewrite H0.
trivial.
- assert (mTypeEqBool m0 m0 && Qeq_bool v v = true).
apply andb_true_iff; split; [apply EquivEqBoolEq; auto | apply Qeq_bool_iff; lra].
rewrite H0.
auto.
- rewrite expEqBool_refl.
eapply IHe; eauto.
- rewrite expEqBool_refl.
eapply IHe; eauto.
- rewrite expEqBool_refl; simpl.
rewrite expEqBool_refl; simpl.
rewrite andb_true_r.
rewrite binopEqBool_refl; simpl.
pose proof (IHe1 E v1 m1 H7).
pose proof (IHe2 E v2 m2 H8).
rewrite H0, H1.
assert (m = computeJoin m1 m2) by (apply isJoinComputeJoin; auto); subst.
auto.
- rewrite expEqBool_refl.
assert (mTypeEqBool m0 m0 = true) by (apply EquivEqBoolEq; auto).
rewrite H0; simpl.
pose proof (IHe E v1 m2 H6).
rewrite H1,H2; auto.
Qed.
(* (** A function computing a correct typing of expressions (option needed in case of error) **) *)
(* Fixpoint typeExpression (e:exp Q) : option mType := *)
(* match e with *)
(* |Var _ m n => Some m *)
(* |Const m n => Some m *)
(* |Unop o e1 => *)
(* match (typeExpression e1) with *)
(* | None => None *)
(* | Some m => Some m *)
(* end *)
(* |Binop b e1 e2 => *)
(* match (typeExpression e1), (typeExpression e2) with *)
(* | Some m1, Some m2 => Some (computeJoin m1 m2) *)
(* | _, _ => None *)
(* end *)
(* |Downcast m e1 => *)
(* match (typeExpression e1) with *)
(* | Some m1 => if isMorePrecise m1 m then Some m else None *)
(* | None => None *)
(* end *)
(* end. *)
(* (** A soundness theorem for typing **) *)
(* (** TODO: equivalence? **) *)
(* Theorem typingIsSound (e:exp Q): *)
(* forall v E M, *)
(* eval_exp E (toRExp e) v M -> *)
(* typeExpression e = Some M. *)
(* Proof. *)
(* revert e; induction e; intros; inversion H; subst; simpl; try auto. *)
(* - remember (typeExpression e) as te; destruct te; eapply IHe; eauto. *)
(* - remember (typeExpression e) as te; destruct te; eapply IHe; eauto. *)
(* - remember (typeExpression e1) as te1; destruct te1; *)
(* remember (typeExpression e2) as te2; destruct te2; *)
(* pose proof (IHe1 v1 E m1 H7); *)
(* pose proof (IHe2 v2 E m2 H8); *)
(* inversion H0; inversion H1; subst. *)
(* assert (computeJoin m1 m2 = M) by (symmetry; apply isJoinComputeJoin; auto). *)
(* rewrite H2; auto. *)
(* - remember (typeExpression e) as te; destruct te; *)
(* pose proof (IHe v1 E m1 H6); inversion H0; subst. *)
(* rewrite H2; auto. *)
(* Qed. *)
(* (** Fully typed Expression **) *)
(* Inductive typedExp (V:Type): Type := *)
(* | tVar: mType -> nat -> typedExp V *)
(* | tConst: mType -> V -> typedExp V *)
(* | tUnop: mType -> unop -> typedExp V -> typedExp V *)
(* | tBinop: mType -> binop -> typedExp V -> typedExp V -> typedExp V *)
(* | tDowncast: mType -> typedExp V -> typedExp V. *)
(* Fixpoint getTypeR (e: typedExp R) : mType := *)
(* match e with *)
(* | tVar _ m _ => m *)
(* | tConst m _ => m *)
(* | tUnop m _ _ => m *)
(* | tBinop m _ _ _ => m *)
(* | tDowncast m _ => m *)
(* end. *)
(* Fixpoint getTypeQ (e: typedExp Q) : mType := *)
(* match e with *)
(* | tVar _ m _ => m *)
(* | tConst m _ => m *)
(* | tUnop m _ _ => m *)
(* | tBinop m _ _ _ => m *)
(* | tDowncast m _ => m *)
(* end. *)
(* Fixpoint toRTExp (e: typedExp Q) : typedExp R := *)
(* match e with *)
(* | tVar _ m n => tVar R m n *)
(* | tConst m n => tConst m (Q2R n) *)
(* | tUnop m o e1 => tUnop m o (toRTExp e1) *)
(* | tBinop m o e1 e2 => tBinop m o (toRTExp e1) (toRTExp e2) *)
(* | tDowncast m e1 => tDowncast m (toRTExp e1) *)
(* end. *)
(* Fixpoint texpEquivBool (e1:typedExp Q) (e2:typedExp Q) := *)
(* match e1,e2 with *)
(* |tVar _ m1 v1, tVar _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2) *)
(* |tConst m1 n1, tConst m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) *)
(* |tUnop _ o1 e11, tUnop _ o2 e22 => andb (unopEqBool o1 o2) (texpEquivBool e11 e22) *)
(* |tBinop _ o1 e11 e12, tBinop _ o2 e21 e22 => andb (binopEqBool o1 o2) (andb (texpEquivBool e11 e21) (texpEquivBool e12 e22)) *)
(* |tDowncast m1 f1, tDowncast m2 f2 => andb (mTypeEqBool m1 m2) (texpEquivBool f1 f2) *)
(* |_, _ => false *)
(* end. *)
(* (** Eval_exp for typed expressions **) *)
(* (** TODO: not the same as eval_exp (binop_dist, and var_load?) **) *)
(* Inductive eval_exp_t (E:env) : typedExp R -> R -> Prop := *)
(* | tVar_load m m1 x v: *)
(* isMorePrecise m m1 = true -> *)
(* E x = Some (v, m1) -> *)
(* eval_exp_t E (tVar R m x) v *)
(* | tConst_dist m n delta: *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E (tConst m n) (perturb n delta) *)
(* | tUnop_neg m f1 v1: *)
(* m = getTypeR f1 -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tUnop m Neg f1) (evalUnop Neg v1) *)
(* | tUnop_inv m m1 f1 v1 delta: *)
(* m1 = getTypeR f1 -> *)
(* isMorePrecise m m1 = true -> *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tUnop m Inv f1) (perturb (evalUnop Inv v1) delta) *)
(* | tBinop_dist m m1 m2 op f1 f2 v1 v2 delta: *)
(* m1 = getTypeR f1 -> *)
(* m2 = getTypeR f2 -> *)
(* isJoinOf m m1 m2 = true -> *)
(* (* isMorePrecise m m1 = true -> *) *)
(* (* isMorePrecise m m2 = true -> *) *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E f2 v2 -> *)
(* eval_exp_t E (tBinop m op f1 f2) (perturb (evalBinop op v1 v2) delta) *)
(* | tDowncast_dist m m1 f1 v1 delta: *)
(* (* Qle_bool (meps m1) (meps m) = true ->*) *)
(* isMorePrecise m1 m = true -> *)
(* Rle (Rabs delta) (Q2R (meps m)) -> *)
(* eval_exp_t E f1 v1 -> *)
(* eval_exp_t E (tDowncast m f1) (perturb v1 delta). *)
(* (** A function computing a correct typing of expressions (option needed in case of error) **) *)
(* Fixpoint typeExpression (e:exp Q) : option (typedExp Q) := *)
(* match e with *)
(* |Var _ m n => Some (tVar Q m n) *)
(* |Const m n => Some (tConst m n) *)
(* |Unop o e1 => *)
(* match (typeExpression e1) with *)
(* | None => None *)
(* | Some te1 => Some (tUnop (getTypeQ te1) o te1) *)
(* end *)
(* |Binop b e1 e2 => *)
(* match (typeExpression e1), (typeExpression e2) with *)
(* | Some te1, Some te2 => *)
(* let prec := computeJoin (getTypeQ te1) (getTypeQ te2) in *)
(* Some (tBinop prec b te1 te2) *)
(* | _, _ => None *)
(* end *)
(* |Downcast m e1 => *)
(* match (typeExpression e1) with *)
(* | Some te1 => *)
(* Some (tDowncast m te1) *)
(* | None => None *)
(* end *)
(* end. *)
(* Lemma convQR (e: typedExp Q): *)
(* getTypeQ e = getTypeR (toRTExp e). *)
(* Proof. *)
(* revert e; induction e; try (simpl in *; auto). *)
(* Qed. *)
(* (** A soundness theorem for typing **) *)
(* (** TODO: equivalence? **) *)
(* Theorem typing_sound (e:exp Q) (e': typedExp Q): *)
(* forall v E M, *)
(* typeExpression e = Some e' -> *)
(* eval_exp E (toRExp e) v M -> *)
(* eval_exp_t E (toRTExp e') v /\ (getTypeQ e' = M). *)
(* Proof. *)
(* revert e e'. *)
(* induction e; intros; inversion H; subst; inversion H0; subst. *)
(* - split; try auto. *)
(* econstructor; eauto. *)
(* - split; try auto. *)
(* constructor; auto. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = M) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split; try auto. *)
(* constructor; try auto. *)
(* apply convQR. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = M) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split; try auto. *)
(* econstructor; try auto. *)
(* rewrite convQR; apply isMorePrecise_refl. *)
(* - remember (typeExpression e1) as te1; destruct te1; inversion H2; *)
(* remember (typeExpression e2) as te2; destruct te2; inversion H2; subst; *)
(* assert (Some t = Some t) as St by auto; assert (Some t0 = Some t0) as St0 by auto; *)
(* destruct (IHe1 t v1 E m1 St H9) as [Hi1e Hi1m]; *)
(* destruct (IHe2 t0 v2 E m2 St0 H10) as [Hi2e Hi2m]. *)
(* split. *)
(* + econstructor; eauto. *)
(* * rewrite <- convQR. *)
(* rewrite <- convQR. *)
(* apply computeJoinIsJoin. *)
(* * assert (M = computeJoin m1 m2). *)
(* unfold computeJoin. *)
(* case_eq (isMorePrecise m1 m2); intros; auto; unfold isJoinOf in H5; rewrite H1 in H5; *)
(* apply EquivEqBoolEq; auto. *)
(* rewrite Hi1m; rewrite Hi2m; rewrite <- H1; auto. *)
(* + rewrite Hi1m; rewrite Hi2m. *)
(* unfold getTypeQ. *)
(* unfold computeJoin. *)
(* case_eq (isMorePrecise m1 m2); intros; auto; unfold isJoinOf in H5; rewrite H1 in H5; symmetry; apply EquivEqBoolEq; auto. *)
(* - remember (typeExpression e) as te; destruct te; inversion H2; subst; *)
(* assert (eval_exp_t E (toRTExp t) v1 /\ getTypeQ t = m1) as [Hi1 Hi2] by (apply IHe; auto); subst. *)
(* split. *)
(* + econstructor; eauto. *)
(* + simpl; trivial. *)
(* Qed. *)
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