source: C-semantics/Errors.ma @ 189

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

Rework monad notation so that it is displayed well in proof mode.

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