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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
(** Extension of Coq language with some IO and exception-handling operators.
TODO: integration with http://coq.io/ ?
*)
Require Export ImpPrelude.
Import Notations.
Local Open Scope impure.
(** Printing functions *)
Axiom print: pstring -> ?? unit.
Extract Constant print => "ImpIOOracles.print".
Axiom println: pstring -> ?? unit.
Extract Constant println => "ImpIOOracles.println".
Axiom read_line: unit -> ?? pstring.
Extract Constant read_line => "ImpIOOracles.read_line".
Require Import ZArith.
Axiom string_of_Z: Z -> ?? pstring.
Extract Constant string_of_Z => "ImpIOOracles.string_of_Z".
(** timer *)
Axiom timer: forall {A B}, (A -> ?? B)*A -> ?? B.
Extract Constant timer => "ImpIOOracles.timer".
(** Exception Handling *)
Axiom exit_observer: Type.
Extract Constant exit_observer => "((unit -> unit) ref)".
Axiom new_exit_observer: (unit -> ??unit) -> ??exit_observer.
Extract Constant new_exit_observer => "ImpIOOracles.new_exit_observer".
Axiom set_exit_observer: exit_observer * (unit -> ??unit) -> ??unit.
Extract Constant set_exit_observer => "ImpIOOracles.set_exit_observer".
Axiom exn: Type.
Extract Inlined Constant exn => "exn".
Axiom raise: forall {A}, exn -> ?? A.
Extract Constant raise => "raise".
Axiom exn2string: exn -> ?? pstring.
Extract Constant exn2string => "ImpIOOracles.exn2string".
Axiom fail: forall {A}, pstring -> ?? A.
Extract Constant fail => "ImpIOOracles.fail".
Axiom try_with_fail: forall {A}, (unit -> ?? A) * (pstring -> exn -> ??A) -> ??A.
Extract Constant try_with_fail => "ImpIOOracles.try_with_fail".
Axiom try_with_any: forall {A}, (unit -> ?? A) * (exn -> ??A) -> ??A.
Extract Constant try_with_any => "ImpIOOracles.try_with_any".
Notation "'RAISE' e" := (DO r <~ raise (A:=False) e ;; RET (match r with end)) (at level 0): impure_scope.
Notation "'FAILWITH' msg" := (DO r <~ fail (A:=False) msg ;; RET (match r with end)) (at level 0): impure_scope.
Definition _FAILWITH {A:Type} msg: ?? A := FAILWITH msg.
Example _FAILWITH_correct A msg (P: A -> Prop):
WHEN _FAILWITH msg ~> r THEN P r.
Proof.
wlp_simplify.
Qed.
Notation "'TRY' k1 'WITH_FAIL' s ',' e '=>' k2" := (try_with_fail (fun _ => k1, fun s e => k2))
(at level 55, k1 at level 53, right associativity): impure_scope.
Notation "'TRY' k1 'WITH_ANY' e '=>' k2" := (try_with_any (fun _ => k1, fun e => k2))
(at level 55, k1 at level 53, right associativity): impure_scope.
Program Definition assert_b (b: bool) (msg: pstring): ?? b=true :=
match b with
| true => RET _
| false => FAILWITH msg
end.
Lemma assert_wlp_true msg b: WHEN assert_b b msg ~> _ THEN b=true.
Proof.
wlp_simplify.
Qed.
Lemma assert_false_wlp msg (P: Prop): WHEN assert_b false msg ~> _ THEN P.
Proof.
simpl; wlp_simplify.
Qed.
Program Definition try_catch_fail_ensure {A} (k1: unit -> ?? A) (k2: pstring -> exn -> ??A) (P: A -> Prop | wlp (k1 tt) P /\ (forall s e, wlp (k2 s e) P)): ?? { r | P r }
:= TRY
DO r <~ mk_annot (k1 tt);;
RET (exist P r _)
WITH_FAIL s, e =>
DO r <~ mk_annot (k2 s e);;
RET (exist P r _).
Obligation 2.
unfold wlp in * |- *; eauto.
Qed.
Notation "'TRY' k1 'CATCH_FAIL' s ',' e '=>' k2 'ENSURE' P" := (try_catch_fail_ensure (fun _ => k1) (fun s e => k2) (exist _ P _))
(at level 55, k1 at level 53, right associativity): impure_scope.
Definition is_try_post {A} (P: A -> Prop) k1 k2 : Prop :=
wlp (k1 ()) P /\ forall (e:exn), wlp (k2 e) P.
Program Definition try_catch_ensure {A} k1 k2 (P:A->Prop|is_try_post P k1 k2): ?? { r | P r }
:= TRY
DO r <~ mk_annot (k1 ());;
RET (exist P r _)
WITH_ANY e =>
DO r <~ mk_annot (k2 e);;
RET (exist P r _).
Obligation 1.
unfold is_try_post, wlp in * |- *; intuition eauto.
Qed.
Obligation 2.
unfold is_try_post, wlp in * |- *; intuition eauto.
Qed.
Notation "'TRY' k1 'CATCH' e '=>' k2 'ENSURE' P" := (try_catch_ensure (fun _ => k1) (fun e => k2) (exist _ P _))
(at level 55, k1 at level 53, right associativity): impure_scope.
Program Example tryex {A} (x y:A) :=
TRY (RET x)
CATCH _ => (RET y)
ENSURE (fun r => r = x \/ r = y).
Obligation 1.
split; wlp_simplify.
Qed.
Program Example tryex_test {A} (x y:A):
WHEN tryex x y ~> r THEN `r <> x -> `r = y.
Proof.
wlp_simplify. destruct exta as [r [X|X]]; intuition.
Qed.
Program Example try_branch1 {A} (x:A): ?? { r | r = x} :=
TRY (RET x)
CATCH e => (FAILWITH "!")
ENSURE _.
Obligation 1.
split; wlp_simplify.
Qed.
Program Example try_branch2 {A} (x:A): ?? { r | r = x} :=
TRY (FAILWITH "!")
CATCH e => (RET x)
ENSURE _.
Obligation 1.
split; wlp_simplify.
Qed.
|
