source: Deliverables/D3.1/C-semantics/Errors.ma @ 473

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

Begin separating soundness from executable semantics.

File size: 7.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 "datatypes/pairs.ma".
17include "Plogic/equality.ma".
18include "Plogic/connectives.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
42ninductive res (A: Type) : Type ≝
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
51ndefinition bind ≝ λA,B:Type. λf: res A. λg: A → res B.
52  match f with
53  [ OK x ⇒ g x
54  | Error (*msg*) ⇒ Error ? (*msg*)
55  ].
56
57ndefinition bind2 ≝ λA,B,C: Type. λf: res (A × B). λg: A → B → res C.
58  match f with
59  [ OK v ⇒ match v with [ mk_pair x y ⇒ g x y ]
60  | Error (*msg*) => Error ? (*msg*)
61  ].
62
63(* Not sure what level to use *)
64notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
65notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
66notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
67notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
68interpretation "error monad bind" 'bind e f = (bind ?? e f).
69notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
70notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
71notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
72notation < "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'})}.
73interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
74(*interpretation "error monad ret" 'ret e = (ret ? e).
75notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
76
77(*
78(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
79
80Notation "'do' X <- A ; B" := (bind A (fun X => B))
81 (at level 200, X ident, A at level 100, B at level 200)
82 : error_monad_scope.
83
84Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
85 (at level 200, X ident, Y ident, A at level 100, B at level 200)
86 : error_monad_scope.
87*)
88nremark bind_inversion:
89  ∀A,B: Type. ∀f: res A. ∀g: A → res B. ∀y: B.
90  bind ?? f g = OK ? y →
91  ∃x. f = OK ? x ∧ g x = OK ? y.
92#A B f g y; ncases f;
93##[ #a e; @a; nwhd in e:(??%?); /2/;
94##| #H; nwhd in H:(??%?); ndestruct (H);
95##] nqed.
96
97nremark bind2_inversion:
98  ∀A,B,C: Type. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
99  bind2 ??? f g = OK ? z →
100  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
101#A B C f g z; ncases f;
102##[ #ab; ncases ab; #a b e; @a; @b; nwhd in e:(??%?); /2/;
103##| #H; nwhd in H:(??%?); ndestruct
104##] nqed.
105
106(*
107Open Local Scope error_monad_scope.
108
109(** This is the familiar monadic map iterator. *)
110
111Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
112  match l with
113  | nil => OK nil
114  | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
115  end.
116
117Remark mmap_inversion:
118  forall (A B: Type) (f: A -> res B) (l: list A) (l': list B),
119  mmap f l = OK l' ->
120  list_forall2 (fun x y => f x = OK y) l l'.
121Proof.
122  induction l; simpl; intros.
123  inversion_clear H. constructor.
124  destruct (bind_inversion _ _ H) as [hd' [P Q]].
125  destruct (bind_inversion _ _ Q) as [tl' [R S]].
126  inversion_clear S.
127  constructor. auto. auto.
128Qed.
129
130(** * Reasoning over monadic computations *)
131
132(** The [monadInv H] tactic below simplifies hypotheses of the form
133<<
134        H: (do x <- a; b) = OK res
135>>
136    By definition of the bind operation, both computations [a] and
137    [b] must succeed for their composition to succeed.  The tactic
138    therefore generates the following hypotheses:
139
140         x: ...
141        H1: a = OK x
142        H2: b x = OK res
143*)
144
145Ltac monadInv1 H :=
146  match type of H with
147  | (OK _ = OK _) =>
148      inversion H; clear H; try subst
149  | (Error _ = OK _) =>
150      discriminate
151  | (bind ?F ?G = OK ?X) =>
152      let x := fresh "x" in (
153      let EQ1 := fresh "EQ" in (
154      let EQ2 := fresh "EQ" in (
155      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
156      clear H;
157      try (monadInv1 EQ2))))
158  | (bind2 ?F ?G = OK ?X) =>
159      let x1 := fresh "x" in (
160      let x2 := fresh "x" in (
161      let EQ1 := fresh "EQ" in (
162      let EQ2 := fresh "EQ" in (
163      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
164      clear H;
165      try (monadInv1 EQ2)))))
166  | (mmap ?F ?L = OK ?M) =>
167      generalize (mmap_inversion F L H); intro
168  end.
169
170Ltac monadInv H :=
171  match type of H with
172  | (OK _ = OK _) => monadInv1 H
173  | (Error _ = OK _) => monadInv1 H
174  | (bind ?F ?G = OK ?X) => monadInv1 H
175  | (bind2 ?F ?G = OK ?X) => monadInv1 H
176  | (?F _ _ _ _ _ _ _ _ = OK _) =>
177      ((progress simpl in H) || unfold F in H); monadInv1 H
178  | (?F _ _ _ _ _ _ _ = OK _) =>
179      ((progress simpl in H) || unfold F in H); monadInv1 H
180  | (?F _ _ _ _ _ _ = OK _) =>
181      ((progress simpl in H) || unfold F in H); monadInv1 H
182  | (?F _ _ _ _ _ = OK _) =>
183      ((progress simpl in H) || unfold F in H); monadInv1 H
184  | (?F _ _ _ _ = OK _) =>
185      ((progress simpl in H) || unfold F in H); monadInv1 H
186  | (?F _ _ _ = OK _) =>
187      ((progress simpl in H) || unfold F in H); monadInv1 H
188  | (?F _ _ = OK _) =>
189      ((progress simpl in H) || unfold F in H); monadInv1 H
190  | (?F _ = OK _) =>
191      ((progress simpl in H) || unfold F in H); monadInv1 H
192  end.
193*)
Note: See TracBrowser for help on using the repository browser.