source: src/common/Errors.ma @ 793

Last change on this file since 793 was 764, checked in by campbell, 9 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.