source: src/common/Errors.ma @ 1910

Last change on this file since 1910 was 1882, checked in by tranquil, 9 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 9.7 KB
Line 
1include "basics/types.ma".
2include "basics/logic.ma".
3include "basics/lists/list.ma".
4include "common/PreIdentifiers.ma".
5include "basics/russell.ma".
6include "utilities/monad.ma".
7include "utilities/option.ma".
8
9(* first, generic exception monad *)
10
11inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝
12  | raise : E → except E X
13  | success : X → except E X.
14
15definition Except ≝ λE.MakeMonadProps
16  (except E)
17  (success E)
18  (λX,Y,m,f.match m with [raise e ⇒ raise … e | success x ⇒ f x])
19  ????.
20//
21[ #X * #x %
22| #X#Y#Z * #x#f#g %
23| #X#Y normalize * #x #f #g #H // normalize @H
24]
25qed.
26
27unification hint 0 ≔ E,X;
28O ≟ Except E, N ≟ max_def O
29(*--------------------------------------*) ⊢
30except E X ≡ monad N X.
31
32definition try_catch : ∀E,X.except E X → (E → X) → X ≝
33  λE,X,m,f.match m with
34  [ success x ⇒ x
35  | raise e ⇒ f e
36  ].
37
38interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).
39
40definition except_elim : ∀E,X.∀m : except E X.∀P : ? → Prop.
41  (∀x.m = success ?? x → P (success ?? x)) →
42  (∀e.m = raise ?? e → P (raise ?? e)) →
43  P m.
44#E #X * /2/
45qed.
46
47definition except_success ≝ λE,X.λm : except E X.
48  match m with [success _ ⇒ True | _ ⇒ False].
49
50definition except_safe ≝
51  λE,X.λm : except E X.
52    match m return λx.except_success ?? x → X with
53    [ success y ⇒ λ_.y
54    | _ ⇒ λprf.match prf in False with []
55    ].
56
57definition Except_P ≝ λE.λP_e : E → Prop.mk_MonadPred (Except E)
58  (λX,P,m. Try ! x ← m ; return P x catch e ⇒ P_e e) ???.
59[ //
60| #X#Y #P1 #P2 * #x normalize /2/
61| #X #P #Q #H * #y normalize /2/
62]
63qed.
64
65definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).
66
67definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝
68  λE : Type[0].except_P E (λe.True).
69
70definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝
71  λE : Type[0].except_P E (λe.False).
72
73definition except_rel ≝ λE,F.λrel_e : E → F → Prop.mk_MonadRel (Except E) (Except F)
74  (λX,Y,rel,m,n.
75    match m with
76    [ success x ⇒ match n with [success y ⇒ rel x y | _ ⇒ False]
77    | raise e ⇒ match n with [raise f ⇒ rel_e e f | _ ⇒ False]
78    ]) ???.
79[ //
80|*: #X#Y[#Z#W] #rel1 #rel2 [2: #H] * #x * #y normalize /2/ *
81]
82qed.
83
84(* * Error reporting and the error monad. *)
85
86(* * * Representation of error messages. *)
87
88(* * Compile-time errors produce an error message, represented in Coq
89  as a list of either substrings or positive numbers encoding
90  a source-level identifier (see module AST). *)
91
92inductive errcode: Type[0] :=
93  | MSG: String → errcode
94  | CTX: ∀tag:String. identifier tag → errcode.
95
96definition errmsg: Type[0] ≝ list errcode.
97
98definition msg : String → errmsg ≝ λs. [MSG s].
99
100(* * * The error monad *)
101
102(* * Compilation functions that can fail have return type [res A].
103  The return value is either [OK res] to indicate success,
104  or [Error msg] to indicate failure. *)
105
106(* Paolo: not using except for backward compatbility
107  (would break Error ? msg) *)
108
109inductive res (A: Type[0]) : Type[0] ≝
110| OK: A → res A
111| Error: errmsg → res A.
112
113(*Implicit Arguments Error [A].*)
114
115definition Res ≝ MakeMonadProps
116  (* the monad *)
117  res
118  (* return *)
119  (λX.OK X)
120  (* bind *)
121  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
122  ????.
123//
124[(* bind_ret *)
125 #X*normalize //
126|(* bind_bind *)
127 #X#Y#Z*normalize //
128| normalize #X #Y * normalize /2/
129]
130qed.
131
132include "hints_declaration.ma".
133unification hint 0 ≔ X;
134N ≟ max_def Res
135(*---------------*) ⊢
136res X ≡ monad N X
137.
138
139(*(* Dependent pair version. *)
140notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
141  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
142
143lemma Prod_extensionality:
144  ∀a, b: Type[0].
145  ∀p: a × b.
146    p = 〈fst … p, snd … p〉.
147  #a #b #p //
148qed.
149
150definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
151λA,B,C,P,e,f.
152  match e with
153  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
154  | Error msg ⇒ Error ? msg
155  ].
156  <(Prod_extensionality A B v')
157  assumption
158qed.
159
160notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
161interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
162
163lemma bind_inversion:
164  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
165  (f »= g = return y) →
166  ∃x. (f = return x) ∧ (g x = return y).
167#A #B #f #g #y cases f normalize
168[ #a #e %{a} /2 by conj/
169| #m #H destruct (H)
170] qed.
171
172lemma bind2_inversion:
173  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
174  m_bind2 ???? f g = return z →
175  ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z.
176#A #B #C #f #g #z cases f normalize
177[ * #a #b normalize #e %{a} %{b} /2 by conj/
178| #m #H destruct (H)
179] qed.
180
181(*
182Open Local Scope error_monad_scope.*)
183
184(*
185lemma mmap_inversion:
186  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
187  mmap A B f l = OK ? l' →
188  list_forall2 (fun x y => f x = OK y) l l'.
189Proof.
190  induction l; simpl; intros.
191  inversion_clear H. constructor.
192  destruct (bind_inversion _ _ H) as [hd' [P Q]].
193  destruct (bind_inversion _ _ Q) as [tl' [R S]].
194  inversion_clear S.
195  constructor. auto. auto.
196Qed.
197*)
198
199(* A monadic fold_lefti *)
200let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
201                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
202  match l with
203    [ nil ⇒ x
204    | cons hd tl ⇒
205       ! x ← x ;
206       mfold_left_i_aux A B f (f i x hd) (S i) tl
207    ].
208
209definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
210
211
212(* A monadic fold_left2 *)
213
214axiom WrongLength: String.
215
216let rec mfold_left2
217  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
218  (left: list B) (right: list C) on left: res A ≝
219  match left with
220  [ nil ⇒
221    match right with
222    [ nil ⇒ accu
223    | cons hd tl ⇒ Error ? (msg WrongLength)
224    ]
225  | cons hd tl ⇒
226    match right with
227    [ nil ⇒ Error ? (msg WrongLength)
228    | cons hd' tl' ⇒
229       ! accu ← accu;
230       mfold_left2 … f (f accu hd hd') tl tl'
231    ]
232  ].
233
234(*
235(** * Reasoning over monadic computations *)
236
237(** The [monadInv H] tactic below simplifies hypotheses of the form
238<<
239        H: (do x <- a; b) = OK res
240>>
241    By definition of the bind operation, both computations [a] and
242    [b] must succeed for their composition to succeed.  The tactic
243    therefore generates the following hypotheses:
244
245         x: ...
246        H1: a = OK x
247        H2: b x = OK res
248*)
249
250Ltac monadInv1 H :=
251  match type of H with
252  | (OK _ = OK _) =>
253      inversion H; clear H; try subst
254  | (Error _ = OK _) =>
255      discriminate
256  | (bind ?F ?G = OK ?X) =>
257      let x := fresh "x" in (
258      let EQ1 := fresh "EQ" in (
259      let EQ2 := fresh "EQ" in (
260      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
261      clear H;
262      try (monadInv1 EQ2))))
263  | (bind2 ?F ?G = OK ?X) =>
264      let x1 := fresh "x" in (
265      let x2 := fresh "x" in (
266      let EQ1 := fresh "EQ" in (
267      let EQ2 := fresh "EQ" in (
268      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
269      clear H;
270      try (monadInv1 EQ2)))))
271  | (mmap ?F ?L = OK ?M) =>
272      generalize (mmap_inversion F L H); intro
273  end.
274
275Ltac monadInv H :=
276  match type of H with
277  | (OK _ = OK _) => monadInv1 H
278  | (Error _ = OK _) => monadInv1 H
279  | (bind ?F ?G = OK ?X) => monadInv1 H
280  | (bind2 ?F ?G = OK ?X) => monadInv1 H
281  | (?F _ _ _ _ _ _ _ _ = OK _) =>
282      ((progress simpl in H) || unfold F in H); monadInv1 H
283  | (?F _ _ _ _ _ _ _ = OK _) =>
284      ((progress simpl in H) || unfold F in H); monadInv1 H
285  | (?F _ _ _ _ _ _ = OK _) =>
286      ((progress simpl in H) || unfold F in H); monadInv1 H
287  | (?F _ _ _ _ _ = OK _) =>
288      ((progress simpl in H) || unfold F in H); monadInv1 H
289  | (?F _ _ _ _ = OK _) =>
290      ((progress simpl in H) || unfold F in H); monadInv1 H
291  | (?F _ _ _ = OK _) =>
292      ((progress simpl in H) || unfold F in H); monadInv1 H
293  | (?F _ _ = OK _) =>
294      ((progress simpl in H) || unfold F in H); monadInv1 H
295  | (?F _ = OK _) =>
296      ((progress simpl in H) || unfold F in H); monadInv1 H
297  end.
298*)
299
300
301definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
302lemma opt_OK: ∀A,m,P,e.
303  (∀v. e = Some ? v → P v) →
304  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
305#A #m #P #e elim e; /2/;
306qed.
307
308(* A variation of bind and its notation that provides an equality proof for
309   later use. *)
310
311definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
312  match f return λx. f = x → ? with
313  [ OK x ⇒ g x
314  | Error msg ⇒ λ_. Error ? msg
315  ] (refl ? f).
316
317notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
318
319definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
320  match f return λx. f = x → ? with
321  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
322  | Error msg ⇒ λ_. Error ? msg
323  ] (refl ? f).
324
325notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
326
327definition res_to_opt : ∀A:Type[0]. res A → option A ≝
328 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
329
330(* aliases for backward compatibility *)
331definition bind ≝ m_bind Res.
332definition bind2 ≝ m_bind2 Res.
333definition bind3 ≝ m_bind3 Res.
334definition mmap ≝ m_list_map Res.
335definition mmap_sigma ≝ m_list_map_sigma Res.
Note: See TracBrowser for help on using the repository browser.