source: src/common/Errors.ma @ 985

Last change on this file since 985 was 797, checked in by campbell, 10 years ago

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

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/list.ma".
19include "common/PreIdentifiers.ma".
20
21(* * Error reporting and the error monad. *)
22
23(* * * Representation of error messages. *)
24
25(* * Compile-time errors produce an error message, represented in Coq
26  as a list of either substrings or positive numbers encoding
27  a source-level identifier (see module AST). *)
28
29inductive errcode: Type[0] :=
30  | MSG: String → errcode
31  | CTX: ∀tag:String. identifier tag → errcode.
32
33definition errmsg: Type[0] ≝ list errcode.
34
35definition msg : String → errmsg ≝ λs. [MSG s].
36
37(* * * The error monad *)
38
39(* * Compilation functions that can fail have return type [res A].
40  The return value is either [OK res] to indicate success,
41  or [Error msg] to indicate failure. *)
42
43inductive res (A: Type[0]) : Type[0] ≝
44| OK: A → res A
45| Error: errmsg → res A.
46
47(*Implicit Arguments Error [A].*)
48
49(* * To automate the propagation of errors, we use a monadic style
50  with the following [bind] operation. *)
51
52definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B.
53  match f with
54  [ OK x ⇒ g x
55  | Error msg ⇒ Error ? msg
56  ].
57
58definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
59  match f with
60  [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
61  | Error msg => Error ? msg
62  ].
63
64definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
65  match f with
66  [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
67  | Error msg => Error ? msg
68  ].
69 
70(* Not sure what level to use *)
71notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
72notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
73notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
74notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
75interpretation "error monad bind" 'bind e f = (bind ?? e f).
76notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
77notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
78notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
79notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
80interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
81notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
82notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
83notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
84notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
85interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f).
86(*interpretation "error monad ret" 'ret e = (ret ? e).
87notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
88
89(*
90(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
91
92Notation "'do' X <- A ; B" := (bind A (fun X => B))
93 (at level 200, X ident, A at level 100, B at level 200)
94 : error_monad_scope.
95
96Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
97 (at level 200, X ident, Y ident, A at level 100, B at level 200)
98 : error_monad_scope.
99*)
100lemma bind_inversion:
101  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
102  bind ?? f g = OK ? y →
103  ∃x. f = OK ? x ∧ g x = OK ? y.
104#A #B #f #g #y cases f;
105[ #a #e %{a} whd in e:(??%?); /2/;
106| #m #H whd in H:(??%?); destruct (H);
107] qed.
108
109lemma bind2_inversion:
110  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
111  bind2 ??? f g = OK ? z →
112  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
113#A #B #C #f #g #z cases f;
114[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
115| #m #H whd in H:(??%?); destruct
116] qed.
117
118(*
119Open Local Scope error_monad_scope.
120
121(** This is the familiar monadic map iterator. *)
122*)
123
124let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝
125  match l with
126  [ nil ⇒ OK ? []
127  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
128  ].
129
130(*
131lemma mmap_inversion:
132  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
133  mmap A B f l = OK ? l' →
134  list_forall2 (fun x y => f x = OK y) l l'.
135Proof.
136  induction l; simpl; intros.
137  inversion_clear H. constructor.
138  destruct (bind_inversion _ _ H) as [hd' [P Q]].
139  destruct (bind_inversion _ _ Q) as [tl' [R S]].
140  inversion_clear S.
141  constructor. auto. auto.
142Qed.
143
144(** * Reasoning over monadic computations *)
145
146(** The [monadInv H] tactic below simplifies hypotheses of the form
147<<
148        H: (do x <- a; b) = OK res
149>>
150    By definition of the bind operation, both computations [a] and
151    [b] must succeed for their composition to succeed.  The tactic
152    therefore generates the following hypotheses:
153
154         x: ...
155        H1: a = OK x
156        H2: b x = OK res
157*)
158
159Ltac monadInv1 H :=
160  match type of H with
161  | (OK _ = OK _) =>
162      inversion H; clear H; try subst
163  | (Error _ = OK _) =>
164      discriminate
165  | (bind ?F ?G = OK ?X) =>
166      let x := fresh "x" in (
167      let EQ1 := fresh "EQ" in (
168      let EQ2 := fresh "EQ" in (
169      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
170      clear H;
171      try (monadInv1 EQ2))))
172  | (bind2 ?F ?G = OK ?X) =>
173      let x1 := fresh "x" in (
174      let x2 := fresh "x" in (
175      let EQ1 := fresh "EQ" in (
176      let EQ2 := fresh "EQ" in (
177      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
178      clear H;
179      try (monadInv1 EQ2)))))
180  | (mmap ?F ?L = OK ?M) =>
181      generalize (mmap_inversion F L H); intro
182  end.
183
184Ltac monadInv H :=
185  match type of H with
186  | (OK _ = OK _) => monadInv1 H
187  | (Error _ = OK _) => monadInv1 H
188  | (bind ?F ?G = OK ?X) => monadInv1 H
189  | (bind2 ?F ?G = OK ?X) => monadInv1 H
190  | (?F _ _ _ _ _ _ _ _ = OK _) =>
191      ((progress simpl in H) || unfold F in H); monadInv1 H
192  | (?F _ _ _ _ _ _ _ = OK _) =>
193      ((progress simpl in H) || unfold F in H); monadInv1 H
194  | (?F _ _ _ _ _ _ = OK _) =>
195      ((progress simpl in H) || unfold F in H); monadInv1 H
196  | (?F _ _ _ _ _ = OK _) =>
197      ((progress simpl in H) || unfold F in H); monadInv1 H
198  | (?F _ _ _ _ = OK _) =>
199      ((progress simpl in H) || unfold F in H); monadInv1 H
200  | (?F _ _ _ = OK _) =>
201      ((progress simpl in H) || unfold F in H); monadInv1 H
202  | (?F _ _ = OK _) =>
203      ((progress simpl in H) || unfold F in H); monadInv1 H
204  | (?F _ = OK _) =>
205      ((progress simpl in H) || unfold F in H); monadInv1 H
206  end.
207*)
208
209
210definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
211lemma opt_OK: ∀A,m,P,e.
212  (∀v. e = Some ? v → P v) →
213  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
214#A #m #P #e elim e; /2/;
215qed.
Note: See TracBrowser for help on using the repository browser.