fixing a potential inconsistency from unsafe_coerce

Now, unsafe_coerce axioms are clearly consistent (for any interpretation of may-return monads).
But, the extraction is still unsafe...

2 files changed, 13 insertions, 7 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index c4c1bbf1..8bc1112f 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1636,11 +1636,17 @@ Hint Resolve bblock_simu_test_correct: wlp.
 
 Import UnsafeImpure.
 
-Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2).
+Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := 
+  match unsafe_coerce (bblock_simu_test verb p1 p2) with
+  | Some b => b
+  | None => false
+  end.
 
 Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
 Proof.
-   intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto.
+   unfold pure_bblock_simu_test. 
+   destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate.
+   intros; subst. eapply bblock_simu_test_correct; eauto.
    apply unsafe_coerce_not_really_correct; eauto.
 Qed.
 
diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v
index 1bd93d4c..e49a4611 100644
--- a/mppa_k1c/abstractbb/Impure/ImpConfig.v
+++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v
@@ -22,9 +22,9 @@ Module Type ImpureView.
 (* START COMMENT *)
  Module UnsafeImpure.
 
- Parameter unsafe_coerce: forall {A}, t A -> A.
+ Parameter unsafe_coerce: forall {A}, t A -> option A.
 
- Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. 
+ Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x.
 
  Extraction Inline unsafe_coerce.
 
@@ -41,11 +41,11 @@ Module Impure: ImpureView.
 
   Module UnsafeImpure.
 
-  Definition unsafe_coerce {A} (x:t A) := x.
+  Definition unsafe_coerce {A} (x:t A) := Some x.
 
-  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=x -> mayRet k x.
+  Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x.
   Proof.
-    unfold unsafe_coerce, mayRet; auto.
+    unfold unsafe_coerce, mayRet; congruence.
   Qed.
 
   End UnsafeImpure.