diff options
Diffstat (limited to 'lib/Impure/ImpConfig.v')
-rw-r--r-- | lib/Impure/ImpConfig.v | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/lib/Impure/ImpConfig.v b/lib/Impure/ImpConfig.v new file mode 100644 index 00000000..dd9785b5 --- /dev/null +++ b/lib/Impure/ImpConfig.v @@ -0,0 +1,85 @@ +(** 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. + +(* WARNING: THIS IS REALLY UNSAFE TO DECOMMENT THE "UnsafeImpure" module ! + + unsafe_coerce coerces an impure computation into a pure one ! + +*) + +(* START COMMENT *) + 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 COMMENT *) + + +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 ! + +*) +(* +Module Impure: MayReturnMonad := PowerSetMonad. +*) + +Export Impure. + +Extraction Inline ret mk_annot. + + +(* WARNING. The following directive is unsound. + + Extraction Inline bind + +For example, it may lead to extract the following code as "true" (instead of an error raising code) + failwith "foo";;true + +*) + +Extract Inlined Constant bind => "(|>)". + + +Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *) +Extraction Inline t. + +Global Opaque t. |