blob: dd9785b5aa1f7bc99e0e37458f0940dd36c3e1e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
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.
|
