Module ImpConfig

Impure Config for UNTRUSTED backend !!!

Require Import ImpMonads.
Require Extraction.

Pure computations (used for extraction !) We keep module Impure opaque in order to check that Coq proof do not depend on the implementation of Impure.

Module Type ImpureView.

Include MayReturnMonad.

Module UnsafeImpure.

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)=Some x -> mayRet k x.

Extraction Inline unsafe_coerce.

End UnsafeImpure.

End ImpureView.

Module Impure: ImpureView.

  Include IdentityMonad.

  Module UnsafeImpure.

  Definition unsafe_coerce {A} (x:t A) := Some 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; congruence.
Qed.

End UnsafeImpure.

End Impure.

Comment the above code and decomment this to test that coq proofs still work with an impure monad !

this should fail only on extraction or if unsafe_coerce is used !

Export Impure.

Extraction Inline ret mk_annot.

Extract Inlined Constant bind => "(|>)".

Extract Constant t "" => "".
Extraction Inline t.

Global Opaque t.