source: src/common/Errors.ma @ 1651

Last change on this file since 1651 was 1647, checked in by tranquil, 8 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 8.5 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16include "basics/types.ma".
17include "basics/logic.ma".
18include "basics/lists/list.ma".
19include "common/PreIdentifiers.ma".
20include "basics/russell.ma".
21include "utilities/monad.ma".
22
23(* * Error reporting and the error monad. *)
24
25(* * * Representation of error messages. *)
26
27(* * Compile-time errors produce an error message, represented in Coq
28  as a list of either substrings or positive numbers encoding
29  a source-level identifier (see module AST). *)
30
31inductive errcode: Type[0] :=
32  | MSG: String → errcode
33  | CTX: ∀tag:String. identifier tag → errcode.
34
35definition errmsg: Type[0] ≝ list errcode.
36
37definition msg : String → errmsg ≝ λs. [MSG s].
38
39(* * * The error monad *)
40
41(* * Compilation functions that can fail have return type [res A].
42  The return value is either [OK res] to indicate success,
43  or [Error msg] to indicate failure. *)
44
45inductive res (A: Type[0]) : Type[0] ≝
46| OK: A → res A
47| Error: errmsg → res A.
48
49(*Implicit Arguments Error [A].*)
50
51definition Res ≝ MakeMonadProps
52  (* the monad *)
53  res
54  (* return *)
55  (λX.OK X)
56  (* bind *)
57  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
58  ???.
59//
60[(* bind_ret *)
61 #X*normalize //
62|(* bind_bind *)
63 #X#Y#Z*normalize //
64]
65qed.
66
67include "hints_declaration.ma".
68unification hint 0 ≔ X;
69N ≟ max_def Res, M ≟ m_def N
70(*---------------*) ⊢
71res X ≡ monad M X
72.
73
74(*(* Dependent pair version. *)
75notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
76  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
77
78lemma Prod_extensionality:
79  ∀a, b: Type[0].
80  ∀p: a × b.
81    p = 〈fst … p, snd … p〉.
82  #a #b #p //
83qed.
84
85definition 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 ≝
86λA,B,C,P,e,f.
87  match e with
88  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
89  | Error msg ⇒ Error ? msg
90  ].
91  <(Prod_extensionality A B v')
92  assumption
93qed.
94
95notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
96interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
97
98lemma bind_inversion:
99  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
100  (f »= g = return y) →
101  ∃x. (f = return x) ∧ (g x = return y).
102#A #B #f #g #y cases f normalize
103[ #a #e %{a} /2 by conj/
104| #m #H destruct (H)
105] qed.
106
107lemma bind2_inversion:
108  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
109  m_bind2 ???? f g = return z →
110  ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z.
111#A #B #C #f #g #z cases f normalize
112[ * #a #b normalize #e %{a} %{b} /2 by conj/
113| #m #H destruct (H)
114] qed.
115
116(*
117Open Local Scope error_monad_scope.*)
118
119(*
120lemma mmap_inversion:
121  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
122  mmap A B f l = OK ? l' →
123  list_forall2 (fun x y => f x = OK y) l l'.
124Proof.
125  induction l; simpl; intros.
126  inversion_clear H. constructor.
127  destruct (bind_inversion _ _ H) as [hd' [P Q]].
128  destruct (bind_inversion _ _ Q) as [tl' [R S]].
129  inversion_clear S.
130  constructor. auto. auto.
131Qed.
132*)
133
134(* A monadic fold_lefti *)
135let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
136                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
137  match l with
138    [ nil ⇒ x
139    | cons hd tl ⇒
140       ! x ← x ;
141       mfold_left_i_aux A B f (f i x hd) (S i) tl
142    ].
143
144definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
145
146
147(* A monadic fold_left2 *)
148
149axiom WrongLength: String.
150
151let rec mfold_left2
152  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
153  (left: list B) (right: list C) on left: res A ≝
154  match left with
155  [ nil ⇒
156    match right with
157    [ nil ⇒ accu
158    | cons hd tl ⇒ Error ? (msg WrongLength)
159    ]
160  | cons hd tl ⇒
161    match right with
162    [ nil ⇒ Error ? (msg WrongLength)
163    | cons hd' tl' ⇒
164       ! accu ← accu;
165       mfold_left2 … f (f accu hd hd') tl tl'
166    ]
167  ].
168
169(*
170(** * Reasoning over monadic computations *)
171
172(** The [monadInv H] tactic below simplifies hypotheses of the form
173<<
174        H: (do x <- a; b) = OK res
175>>
176    By definition of the bind operation, both computations [a] and
177    [b] must succeed for their composition to succeed.  The tactic
178    therefore generates the following hypotheses:
179
180         x: ...
181        H1: a = OK x
182        H2: b x = OK res
183*)
184
185Ltac monadInv1 H :=
186  match type of H with
187  | (OK _ = OK _) =>
188      inversion H; clear H; try subst
189  | (Error _ = OK _) =>
190      discriminate
191  | (bind ?F ?G = OK ?X) =>
192      let x := fresh "x" in (
193      let EQ1 := fresh "EQ" in (
194      let EQ2 := fresh "EQ" in (
195      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
196      clear H;
197      try (monadInv1 EQ2))))
198  | (bind2 ?F ?G = OK ?X) =>
199      let x1 := fresh "x" in (
200      let x2 := fresh "x" in (
201      let EQ1 := fresh "EQ" in (
202      let EQ2 := fresh "EQ" in (
203      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
204      clear H;
205      try (monadInv1 EQ2)))))
206  | (mmap ?F ?L = OK ?M) =>
207      generalize (mmap_inversion F L H); intro
208  end.
209
210Ltac monadInv H :=
211  match type of H with
212  | (OK _ = OK _) => monadInv1 H
213  | (Error _ = OK _) => monadInv1 H
214  | (bind ?F ?G = OK ?X) => monadInv1 H
215  | (bind2 ?F ?G = OK ?X) => monadInv1 H
216  | (?F _ _ _ _ _ _ _ _ = OK _) =>
217      ((progress simpl in H) || unfold F in H); monadInv1 H
218  | (?F _ _ _ _ _ _ _ = OK _) =>
219      ((progress simpl in H) || unfold F in H); monadInv1 H
220  | (?F _ _ _ _ _ _ = OK _) =>
221      ((progress simpl in H) || unfold F in H); monadInv1 H
222  | (?F _ _ _ _ _ = OK _) =>
223      ((progress simpl in H) || unfold F in H); monadInv1 H
224  | (?F _ _ _ _ = OK _) =>
225      ((progress simpl in H) || unfold F in H); monadInv1 H
226  | (?F _ _ _ = OK _) =>
227      ((progress simpl in H) || unfold F in H); monadInv1 H
228  | (?F _ _ = OK _) =>
229      ((progress simpl in H) || unfold F in H); monadInv1 H
230  | (?F _ = OK _) =>
231      ((progress simpl in H) || unfold F in H); monadInv1 H
232  end.
233*)
234
235
236definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
237lemma opt_OK: ∀A,m,P,e.
238  (∀v. e = Some ? v → P v) →
239  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
240#A #m #P #e elim e; /2/;
241qed.
242
243(* A variation of bind and its notation that provides an equality proof for
244   later use. *)
245
246definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
247  match f return λx. f = x → ? with
248  [ OK x ⇒ g x
249  | Error msg ⇒ λ_. Error ? msg
250  ] (refl ? f).
251
252notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
253
254definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
255  match f return λx. f = x → ? with
256  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
257  | Error msg ⇒ λ_. Error ? msg
258  ] (refl ? f).
259
260notation > "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'})}.
261
262definition res_to_opt : ∀A:Type[0]. res A → option A ≝
263 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
264
265(* aliases for backward compatibility *)
266definition bind ≝ m_bind Res.
267definition bind2 ≝ m_bind2 Res.
268definition bind3 ≝ m_bind3 Res.
269definition mmap ≝ m_mmap Res.
270definition mmap_sigma ≝ m_mmap_sigma Res.
Note: See TracBrowser for help on using the repository browser.