source: src/common/Errors.ma @ 764

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

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

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