little work on inference

coq/IntervalInference.v

@@ -16,10 +16,10 @@ From Flover
 From Flover
      Require Export IntervalArithQ IntervalArith ssaPrgs RealRangeArith.
 
-Fixpoint inferIntervalbounds (e:expr Q) (A: FloverMap.t intv) (* (P: FloverMap.t intv) *)
-         : (result intv * FloverMap.t intv) :=
+Fixpoint inferIntervalbounds (e:expr Q) (A: analysisResult) (* (P: FloverMap.t intv) *)
+         : (result intv * analysisResult) :=
   match FloverMap.find e A with
-  | Some iv => (Succes iv, A)
+  | Some (iv, _) => (Succes iv, A)
   | None =>
     let (rIv, newA) :=
         match e with
@@ -73,12 +73,12 @@ Fixpoint inferIntervalbounds (e:expr Q) (A: FloverMap.t intv) (* (P: FloverMap.t
         | Downcast _ f1 => inferIntervalbounds f1 A
         | Let _ x f1 f2 =>
           match inferIntervalbounds f1 A with
-          | (Succes iv1, A1) => inferIntervalbounds f2 (FloverMap.add (Var Q x) iv1 A1)
+          | (Succes iv1, A1) => inferIntervalbounds f2 (FloverMap.add (Var Q x) (iv1, 0) A1)
           | fail1 => fail1
           end
         end
     in match rIv with
-       | Succes iv => (rIv, FloverMap.add e iv newA)
+       | Succes iv => (rIv, FloverMap.add e (iv, 0) newA)
        | failInfer => (failInfer, newA)
        end
   end.
@@ -95,38 +95,25 @@ Proof.
 Qed.
 *)
 
-Theorem inferIntervalbounds_sound (f:expr Q) (A newA: FloverMap.t intv) iv
+Theorem inferIntervalbounds_sound (f:expr Q) (A newA: analysisResult) iv
         inVars outVars (E:env) Gamma:
   ssa f inVars outVars ->
   inferIntervalbounds f A = (Succes iv, newA) ->
-  (forall e iv, FloverMap.find e A = Some iv ->
-           exists v, eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL /\
-                (Q2R (fst iv) <= v <= Q2R (snd iv))%R) ->
+  (forall e r, FloverMap.find e A = Some r ->
+           validRanges e A E (toRTMap (toRExpMap Gamma))) ->
   validTypes f Gamma ->
-  exists (iv : intv) (vR : R),
-     FloverMap.find f newA = Some iv /\
-     eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp f)) vR REAL /\
-     (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
-  (* validRanges f newA E (toRTMap (toRExpMap Gamma)). *)
+  validRanges f newA E (toRTMap (toRExpMap Gamma)).
 Proof.
   induction f in E, inVars, A, newA |- *;
     intros ssa_f infer_success init_valid valid_types;
-    cbn in *.
-  - Flover_compute.
-    inversion infer_success; subst.
-    edestruct init_valid as [v [H1 H2]]; eauto.
-  - Flover_compute.
-    + inversion infer_success; subst.
-      edestruct init_valid as [vR [H1 H2]]; eauto.
-    + inversion infer_success; subst.
-      exists (v, v), (Q2R v); repeat split; try (cbn; lra).
-      * rewrite FloverMapFacts.P.F.add_o. admit.
-      * eapply Const_dist'; eauto; try reflexivity.
-        cbn. rewrite Rabs_R0. lra.
-  - Flover_compute.
-    + inversion infer_success; subst.
-      edestruct init_valid as [vR [H1 H2]]; eauto.
-    + destruct r; inversion infer_success; subst.
+    unfold inferIntervalbounds in infer_success; Flover_compute; inversion infer_success; subst;
+      try eapply init_valid; eauto.
+  - split; auto.
+    exists (v, v), 0, (Q2R v); repeat split; try (cbn; lra).
+    + rewrite FloverMapFacts.P.F.add_eq_o; auto. admit.
+    + eapply Const_dist'; eauto; try reflexivity.
+      cbn. rewrite Rabs_R0. lra.
+  - destruct r; inversion infer_success; subst.
   (*
   - destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
     + destruct (valid_definedVars n)
@@ -415,6 +402,7 @@ Proof.
   (* - Flover_compute. congruence. *)
 Qed.
 *)
+Abort.
 
 (*
 Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):

coq/RealRangeArith.v

@@ -497,4 +497,4 @@ Proof.
     simpl.
     rewrite !freeVars_toREval_toRExp_compat; auto.
 *)
-Admitted.
+Abort.