new typing done with heiko

/ ! \ not compiling

coq/Commands.v

@@ -14,6 +14,12 @@ Inductive cmd (V:Type) :Type :=
 Let: mType -> nat -> exp V -> cmd V -> cmd V
 | Ret: exp V -> cmd V.
 
+Fixpoint getRetExp (V:Type) (f:cmd V) :=
+  match f with
+  |Let m x e g => getRetExp g
+  | Ret e => e
+  end.
+
 
 Fixpoint toRCmd (f:cmd Q) :=
   match f with
@@ -46,15 +52,27 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
   Define big step semantics for the Daisy language, terminating on a "returned"
   result value
  **)
+
+(* meaning of this -> mType ??? *)
+(* Inductive bstep : cmd R -> env -> R -> mType -> Prop := *)
+(*   let_b m x e s E v res: *)
+(*     eval_exp E e v m -> *)
+(*     bstep s (updEnv x m v E) res m -> *)
+(*     bstep (Let m x e s) E res m *)
+(*  |ret_b m e E v: *)
+(*     eval_exp E e v m -> *)
+(*     bstep (Ret e) E v m. *)
 Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
-  let_b m x e s E v res:
+  let_b m m' x e s E v res:
     eval_exp E e v m ->
-    bstep s (updEnv x m v E) res m ->
-    bstep (Let m x e s) E res m
+    bstep s (updEnv x m v E) res m' ->
+    bstep (Let m x e s) E res m'
  |ret_b m e E v:
     eval_exp E e v m ->
     bstep (Ret e) E v m.
 
+
+
 (**
   The free variables of a command are all used variables of expressions
   without the let bound variables

coq/ErrorValidation.v

@@ -2665,7 +2665,10 @@ Qed.
 Fixpoint typeExpressionCmd (f:cmd Q) (f':exp Q) : option mType :=
   match f with
   |Let m n e c => if expEqBool f' (Var Q m n) then
-                    Some m
+                    match typeExpression e f' with
+                    |None => None
+                    |Some m1 => if mTypeEqBool m1 m then Some m else None
+                    end
                   else
                     let te := typeExpression e in
                     let tc := typeExpressionCmd c in
@@ -2678,6 +2681,29 @@ Fixpoint typeExpressionCmd (f:cmd Q) (f':exp Q) : option mType :=
   |Ret e => (typeExpression e) f'
   end.
 
+
+(* Lemma soundnessTypeCmd f n m0 m1 fV dV oV: *)
+(*   ssaPrg f (NatSet.union fV dV) oV -> *)
+(*   (typeExpressionCmd f) (Var Q m1 n) = Some m1 -> *)
+(*   (typeExpressionCmd f) (Var Q m0 n) = Some m0 -> *)
+(*   m1 = m0. *)
+(* Proof. *)
+(*   revert f; induction f; intros. *)
+(*   - simpl in H0,H1. *)
+(*     case_eq (n =? n0); intros; rewrite H2 in H0, H1. *)
+(*     + admit. *)
+(*     + rewrite andb_false_r in H0, H1. *)
+(*       case_eq (typeExpression e (Var Q m1 n)); intros; case_eq (typeExpression e (Var Q m0 n)); intros; rewrite H3 in H0; rewrite H4 in H1. *)
+(*       * case_eq (typeExpressionCmd f (Var Q m1 n)); intros; case_eq (typeExpressionCmd f (Var Q m0 n)); intros; rewrite H5 in H0; rewrite H6 in H1. *)
+(*         {  *)
+
+(*           } *)
+        
+(*       case_eq (mTypeEqBool m1 m); intros; case_eq (mTypeEqBool m0 m); intros; rewrite H3 in H0; rewrite H in H1. *)
+(*     +  *)
+
+
+      
 Fixpoint cmdEqBool (f f': cmd Q): bool :=
   match f, f' with
   |Let m1 n1 e1 c1, Let m2 n2 e2 c2 =>
@@ -2696,7 +2722,8 @@ Fixpoint isSubCmd (f':cmd Q) (f:cmd Q): bool :=
 
 
 Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
-  forall E1 E2 outVars fVars dVars vR vF elo ehi err P m,
+  forall E1 E2 outVars fVars dVars vR vF elo ehi err P m tEnv,
+    tEnv = typeExpressionCmd f ->
     approxEnv E1 absenv fVars dVars E2 ->
     ssaPrg f (NatSet.union fVars dVars) outVars ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
@@ -2704,8 +2731,8 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
     bstep (toRCmd f) E2 vF m ->
     validErrorboundCmd f (* (typeExpressionCmd f) *) absenv dVars = true ->
     validIntervalboundsCmd f absenv P dVars = true ->
-    (forall e1 v1 m1, NatSet.mem v1 dVars = true ->
-                   (typeExpressionCmd e1) (Var Q m1 v1) = Some m1 ->
+    (forall v1 m1, NatSet.mem v1 dVars = true ->
+                   tEnv (Var Q m1 v1) = Some m1 ->
                    exists vR, E1 v1 = Some (vR, M0) /\
                               (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
     (forall v, NatSet.mem v fVars= true ->
@@ -2715,7 +2742,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
     (Rabs (vR - vF) <= (Q2R err))%R.
 Proof.
   induction f;
-    intros * (*type_f*) approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res.
+    intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res.
   - simpl in eval_real, eval_float.
     inversion eval_float; inversion eval_real; subst.  
     inversion ssa_f; subst.
@@ -2761,9 +2788,10 @@ Proof.
           -
 
             intros e0 v1 m2 natset typeexpr.
-            specialize (fVars_sound (Ret e0) v1 m2 natset).
-            assert (typeExpressionCmd (Ret e0) (Var Q m2 v1) = Some m2) by (simpl; auto).
-            apply fVars_sound; auto.
+            specialize (fVars_sound  v1 m2 natset).
+            admit.
+            (*assert (typeExpressionCmd (Ret e0) (Var Q m2 v1) = Some m2) by (simpl; auto).
+            apply fVars_sound; auto.*)
           - instantiate (1 := q0). instantiate (1 := q).
             rewrite absenv_e; auto. }
       (* * inversion ssa_f; subst.
@@ -2805,7 +2833,7 @@ Proof.
         simpl.
         rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
         split; try auto.
-      * intros e1 v1 m1 v1_mem typing_e1.
+      * intros v1 m1 v1_mem typing_e1.
         unfold updEnv.
         case_eq (v1 =? n); intros v1_eq.
         { rename R1 into eq_lo;
@@ -2817,6 +2845,11 @@ Proof.
           apply Nat.eqb_eq in v1_eq; subst.
           exists v0; split; try auto.
 
+          (* Let n:m0 = e in f *)
+          (*  typeExpressionCmd f (Var Q m1 n) = Some m1 *)
+          (* Want to prove: typeExpressionCmd f (Var Q m0 n) = Some m0 /\ m1 = m0. (because variable n is used in f).                       *)
+          
+
           
           admit.
           

coq/IntervalValidation.v

@@ -195,12 +195,6 @@ Proof.
   apply le_neq_bool_to_lt_prop; auto.
 Qed.
 
-Fixpoint getRetExp (V:Type) (f:cmd V) :=
-  match f with
-  |Let m x e g => getRetExp g
-  | Ret e => e
-  end.
-
 Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
   (typeExpression (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
   (forall (v : NatSet.elt) (m : mType),

coq/Typing.v

 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets.
-Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs.
+Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs.
 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 
+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 :=
+Definition updTEnv (e:exp Q) (t:mType) (cont:exp Q-> option mType) :=
+  (fun e' =>
+     if expEqBool e e'
+     then Some t
+     else cont e').
+
+Definition emptyTEnv :exp Q -> option mType := fun e => None.
+
+Fixpoint typeExpression_trec e (cont:exp Q -> option mType) : 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
+  | Var _ m v => updTEnv e m cont
+  | Const m n => updTEnv e m cont
   | Unop u e1 =>
-    let tE1 := typeExpression e1 in
-    if expEqBool e e' then (tE1 e1)
-    else (tE1 e')
+   let tEnv := typeExpression_trec e1 cont in
+   let t := tEnv e1 in
+   match t with
+   | Some m => updTEnv e m tEnv
+   | None => emptyTEnv
+   end
   | 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
+   let tEnv_e1 := typeExpression_trec e1 cont in
+   let tEnv_e2 := typeExpression_trec e2 tEnv_e1 in (* TODO: This may cause trouble e.g. in (x:F) + (x:D) *)
+   let (t_e1,t_e2) := (tEnv_e2 e1, tEnv_e2 e2) in
+   match t_e1, t_e2 with
+   |Some m, Some m' => updTEnv e (computeJoin m m') tEnv_e2
+   | _, _ => emptyTEnv
+   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')
+    let tEnv_e1 := typeExpression_trec e1 cont in
+    let t := tEnv_e1 e1 in
+    match t with
+    |Some m1 => if (isMorePrecise m1 m) then updTEnv e m tEnv_e1
+               else emptyTEnv
+    |_ => emptyTEnv
+    end
+  end.
+
+Definition typeExpression e := typeExpression_trec e emptyTEnv.
+
+Definition updNatEnv (x:nat) (m:mType) (env: nat -> option mType) :=
+  (fun n => if (n =? x) then Some m else (env n)).
+
+Definition emptyNatEnv :nat -> option mType := fun n => None.
+
+
+
+Fixpoint typeCmd_trec1 (f:cmd Q) (cont: exp Q -> option mType) (env: nat -> option mType) :=
+  match f with
+  | Let m x e g => (* check that env x = None ? or this is already done by ssa ? *)
+    let gamma := typeExpression_trec e cont in
+    match (gamma e) with
+    | Some m' => if mTypeEqBool m m' then
+                   (* hum. Should we just return tEnv_g ? *)
+                   typeCmd_trec1 g gamma (updNatEnv x m' env)
+                 else
+                   emptyTEnv
+    | None => emptyTEnv
+    end
+  | Ret e =>
+    typeExpression_trec e cont
   end.
 
+(* Definition typeCmd f := typeCmd_trec1 f emptyTEnv emptyNatEnv. *)
+
+(* Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))). *)
+(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))). *)
+(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))). *)
+
+
+
+(* do we need this env:nat -> option mType ? The updTEnv does the same kind of thing I guess... *)
+(* issue here is that we may have (Var Q m x) and (Var Q m' x). But this should not happen... *)
+Fixpoint typeCmd_trec2 (f:cmd Q) (cont: exp Q -> option mType) :=
+  match f with
+  | Let m x e g =>
+    let gamma := typeExpression_trec e cont in
+    match (gamma e) with
+    | Some m' => if mTypeEqBool m m' then
+                   let newCont := updTEnv (Var Q m x) m gamma in
+                   typeCmd_trec2 g newCont
+                 else
+                   emptyTEnv
+    | None => emptyTEnv
+    end
+  | Ret e =>
+    typeExpression_trec e cont
+  end.
+
+Definition typeCmd f := typeCmd_trec2 f emptyTEnv.
+
+Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))).
+Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))).
+Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))).
+
+Eval compute in typeCmd (Let M32 1 (Const M32 (1#1))
+                             (Let M64 1 (Const M64 (1#1))
+                             (Ret (Binop Plus (Var Q M32 1) (Var Q M64 1))))). 
+
+
+Theorem typeCmd_sound (f:cmd Q) inVars E v m:
+  validSSA f inVars = true ->
+  bstep (toRCmd f) E v m ->
+  typeCmd f (getRetExp f) = Some m.
+Proof.
+Admitted.
+
+
+
+
 
 (* NB: one might be tempted to prove the following lemma: *)
 (*   Lemma typeExpressionPropagatesNone e e0: *)
@@ -83,7 +156,7 @@ Proof.
   - 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). 
+  - 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.
@@ -131,7 +204,7 @@ Proof.
   - apply IHe.
     simpl in H.
     auto.
-Qed.    
+Qed.
 
 Lemma typingConstDet (e:exp Q) m m0 v:
   typeExpression e (Const m v) = Some m0 ->
@@ -157,18 +230,18 @@ Proof.
   - apply IHe.
     simpl in H.
     auto.
-Qed.    
+Qed.
 
 Fixpoint isSubExpression (e':exp Q) (e:exp Q) :=
   orb (expEqBool e e') (
   match e with
   |Var _ _ _ => false
-  |Const _ _ => false 
+  |Const _ _ => false
   |Unop o1 e1 => isSubExpression e' e1
   |Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2)
   |Downcast m e1 => isSubExpression e' e1
   end).
-    
+
 Lemma typeNotSubExpr e e1:
   isSubExpression e1 e = false -> typeExpression e e1 = None.
 Proof.
@@ -216,9 +289,9 @@ Proof.
       specialize (IHe1 H0).
       simpl; rewrite IHe1; auto.
     + specialize (IHe1 H0); simpl; rewrite IHe1; auto.
-    + specialize (IHe2 H1); simpl; rewrite IHe2. apply orb_true_r. 
+    + specialize (IHe2 H1); simpl; rewrite IHe2. apply orb_true_r.
   - simpl; apply IHe; auto.
-Qed.      
+Qed.
 
 Lemma typedIsSubExpr e f m:
   typeExpression e f = Some m ->
@@ -261,13 +334,13 @@ Proof.
       simpl.
       rewrite IHe.
       apply orb_true_r.
-Qed.      
+Qed.
 
 Lemma typedVarIsUsed e m m0 v:
  typeExpression e (Var Q m0 v) = Some m ->
  NatSet.In v (usedVars e).
 Proof.
-  intros; induction e. 
+  intros; induction e.
   - simpl in *.
     case_eq (mTypeEqBool m1 m0 && (n =? v)); intros; auto; rewrite H0 in H.
     + andb_to_prop H0.
@@ -290,7 +363,7 @@ Proof.
     + simpl in H; rewrite H1, H2 in H.
       inversion H.
   - apply IHe; auto.
-Qed.    
+Qed.
 
 
 Lemma binop_type_unfolding b f1 f2 mf:
@@ -312,7 +385,7 @@ Lemma binary_type_unfolding b e1 e2 f m:
   (typeExpression e1 f = Some m \/ typeExpression e2 f = Some m).
 Proof.
   intros notEq typeBinop.
-  assert (isSubExpression f (Binop b e1 e2) = true) as isSubExpr by (eapply typedIsSubExpr; eauto).  
+  assert (isSubExpression f (Binop b e1 e2) = true) as isSubExpr by (eapply typedIsSubExpr; eauto).
   simpl in *. rewrite notEq in *.
   case_eq (typeExpression e1 f); intros; rewrite H in typeBinop.
   - case_eq (typeExpression e2 f); intros; rewrite H0 in typeBinop.
@@ -361,7 +434,7 @@ Proof.
     case_eq (typeExpression e' e'); intros; rewrite H0 in H1; inversion H1; clear H5.
     case_eq (isMorePrecise m0 m1); intros; rewrite H4 in H1; inversion H1; subst; clear H1;
       auto.
-Qed.                
+Qed.
 
 (* Lemma subExprRewriting e f1 f2: *)
 (*   expEqBool f1 f2 = true -> *)
@@ -447,14 +520,14 @@ Qed.
 (*   - admit. *)
 (*   - simpl; auto. *)
 (* Admitted. *)
-    
+
 (* Lemma unary_type_unfolding u e f m: *)
 (*   isSubExpression f e = true -> *)
 (*   typeExpression (Unop u e) f = Some m -> *)
 (*   typeExpression e f = Some m. *)
 (* Proof. *)
 (* Admitted. *)
-  
+
 
 (* Lemma weakRewritingInTypeExpr e e' f m m': *)
 (*   expEqBool e e' = true -> *)
@@ -546,7 +619,7 @@ Proof.
       * case_eq (typeExpression f2 (Binop b e1 e2)); intros; rewrite H3 in H0; inversion H0; subst.
         apply IHf2; auto.
   - apply IHf; auto.
-Qed.        
+Qed.
 
 
 
@@ -609,4 +682,3 @@ Proof.
       rewrite (stupid _ _ H1).
       apply orb_true_r.
 Qed.
-    
\ No newline at end of file

coq/ssaPrgs.v

@@ -235,16 +235,16 @@ Proof.
 revert E1 E2 vR.
   induction f; intros E1 E2 vR agree_on_vars.
   - split; intros bstep_Let; inversion bstep_Let; subst.
-    + erewrite shadowing_free_rewriting_exp in H5; auto.
+    + erewrite shadowing_free_rewriting_exp in H6; auto.
       econstructor; eauto.
       rewrite <- IHf.
-      apply H6.
+      apply H7.
       intros n'; unfold updEnv.
       case_eq (n' =? n); auto.
-    + erewrite <- shadowing_free_rewriting_exp in H5; auto.
+    + erewrite <- shadowing_free_rewriting_exp in H6; auto.
       econstructor; eauto.
       rewrite IHf.
-      apply H6.
+      apply H7.
       intros n'; unfold updEnv.
       case_eq (n' =? n); auto.
   - split; intros bstep_Ret; inversion bstep_Ret; subst.
@@ -436,8 +436,8 @@ Proof.
       * eapply ssa_shadowing_free.
         apply ssa_f.
         apply x_free.
-        apply H5.
-      * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H6; try eauto.
+        apply H6.
+      * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H7; try eauto.
         simpl in *.
         econstructor; eauto.
         { rewrite <- exp_subst_correct; eauto. }
@@ -450,10 +450,10 @@ Proof.
       inversion ssa_f; subst.
       econstructor; try auto.