source: src/common/Errors.ma @ 1214

Last change on this file since 1214 was 1214, checked in by sacerdot, 8 years ago

res_to_opt function added to common/Errors and used in joint/semantics to make
the code look nicer

File size: 9.2 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
145(* A monadic fold_left2 *)
146
147axiom WrongLength: String.
148
149let rec mfold_left2
150  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
151  (left: list B) (right: list C) on left: res A ≝
152  match left with
153  [ nil ⇒
154    match right with
155    [ nil ⇒ accu
156    | cons hd tl ⇒ Error ? (msg WrongLength)
157    ]
158  | cons hd tl ⇒
159    match right with
160    [ nil ⇒ Error ? (msg WrongLength)
161    | cons hd' tl' ⇒
162       do accu ← accu;
163       mfold_left2 … f (f accu hd hd') tl tl'
164    ]
165  ].
166
167(*
168(** * Reasoning over monadic computations *)
169
170(** The [monadInv H] tactic below simplifies hypotheses of the form
171<<
172        H: (do x <- a; b) = OK res
173>>
174    By definition of the bind operation, both computations [a] and
175    [b] must succeed for their composition to succeed.  The tactic
176    therefore generates the following hypotheses:
177
178         x: ...
179        H1: a = OK x
180        H2: b x = OK res
181*)
182
183Ltac monadInv1 H :=
184  match type of H with
185  | (OK _ = OK _) =>
186      inversion H; clear H; try subst
187  | (Error _ = OK _) =>
188      discriminate
189  | (bind ?F ?G = OK ?X) =>
190      let x := fresh "x" in (
191      let EQ1 := fresh "EQ" in (
192      let EQ2 := fresh "EQ" in (
193      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
194      clear H;
195      try (monadInv1 EQ2))))
196  | (bind2 ?F ?G = OK ?X) =>
197      let x1 := fresh "x" in (
198      let x2 := fresh "x" in (
199      let EQ1 := fresh "EQ" in (
200      let EQ2 := fresh "EQ" in (
201      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
202      clear H;
203      try (monadInv1 EQ2)))))
204  | (mmap ?F ?L = OK ?M) =>
205      generalize (mmap_inversion F L H); intro
206  end.
207
208Ltac monadInv H :=
209  match type of H with
210  | (OK _ = OK _) => monadInv1 H
211  | (Error _ = OK _) => monadInv1 H
212  | (bind ?F ?G = OK ?X) => monadInv1 H
213  | (bind2 ?F ?G = OK ?X) => monadInv1 H
214  | (?F _ _ _ _ _ _ _ _ = OK _) =>
215      ((progress simpl in H) || unfold F in H); 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  end.
231*)
232
233
234definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
235lemma opt_OK: ∀A,m,P,e.
236  (∀v. e = Some ? v → P v) →
237  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
238#A #m #P #e elim e; /2/;
239qed.
240
241definition res_to_opt : ∀A:Type[0]. res A → option A ≝
242 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracBrowser for help on using the repository browser.