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.

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 det_coerce.

Extract Inlined Constant bind => "(|>)".
Extract Inlined Constant has_returned => "(fun k -> let _ = k in true)".

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

Global Opaque t.