source: C-semantics/Errors.ma @ 4

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

Some experimental work on executable Clight semantics.

File size: 6.3 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 "ident v ← e;: e'" right associative with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
63interpretation "error monad bind" 'bind e f = (bind ? ? e f).
64notation "〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
65interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
66(*interpretation "error monad ret" 'ret e = (ret ? e).
67notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
68
69(*
70(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
71
72Notation "'do' X <- A ; B" := (bind A (fun X => B))
73 (at level 200, X ident, A at level 100, B at level 200)
74 : error_monad_scope.
75
76Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
77 (at level 200, X ident, Y ident, A at level 100, B at level 200)
78 : error_monad_scope.
79
80Remark bind_inversion:
81  forall (A B: Type) (f: res A) (g: A -> res B) (y: B),
82  bind f g = OK y ->
83  exists x, f = OK x /\ g x = OK y.
84Proof.
85  intros until y. destruct f; simpl; intros.
86  exists a; auto.
87  discriminate.
88Qed.
89
90Remark bind2_inversion:
91  forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C),
92  bind2 f g = OK z ->
93  exists x, exists y, f = OK (x, y) /\ g x y = OK z.
94Proof.
95  intros until z. destruct f; simpl.
96  destruct p; simpl; intros. exists a; exists b; auto.
97  intros; discriminate.
98Qed.
99
100Open Local Scope error_monad_scope.
101
102(** This is the familiar monadic map iterator. *)
103
104Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
105  match l with
106  | nil => OK nil
107  | hd :: tl => do hd' <- f hd; do tl' <- mmap f tl; OK (hd' :: tl')
108  end.
109
110Remark mmap_inversion:
111  forall (A B: Type) (f: A -> res B) (l: list A) (l': list B),
112  mmap f l = OK l' ->
113  list_forall2 (fun x y => f x = OK y) l l'.
114Proof.
115  induction l; simpl; intros.
116  inversion_clear H. constructor.
117  destruct (bind_inversion _ _ H) as [hd' [P Q]].
118  destruct (bind_inversion _ _ Q) as [tl' [R S]].
119  inversion_clear S.
120  constructor. auto. auto.
121Qed.
122
123(** * Reasoning over monadic computations *)
124
125(** The [monadInv H] tactic below simplifies hypotheses of the form
126<<
127        H: (do x <- a; b) = OK res
128>>
129    By definition of the bind operation, both computations [a] and
130    [b] must succeed for their composition to succeed.  The tactic
131    therefore generates the following hypotheses:
132
133         x: ...
134        H1: a = OK x
135        H2: b x = OK res
136*)
137
138Ltac monadInv1 H :=
139  match type of H with
140  | (OK _ = OK _) =>
141      inversion H; clear H; try subst
142  | (Error _ = OK _) =>
143      discriminate
144  | (bind ?F ?G = OK ?X) =>
145      let x := fresh "x" in (
146      let EQ1 := fresh "EQ" in (
147      let EQ2 := fresh "EQ" in (
148      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
149      clear H;
150      try (monadInv1 EQ2))))
151  | (bind2 ?F ?G = OK ?X) =>
152      let x1 := fresh "x" in (
153      let x2 := fresh "x" in (
154      let EQ1 := fresh "EQ" in (
155      let EQ2 := fresh "EQ" in (
156      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
157      clear H;
158      try (monadInv1 EQ2)))))
159  | (mmap ?F ?L = OK ?M) =>
160      generalize (mmap_inversion F L H); intro
161  end.
162
163Ltac monadInv H :=
164  match type of H with
165  | (OK _ = OK _) => monadInv1 H
166  | (Error _ = OK _) => monadInv1 H
167  | (bind ?F ?G = OK ?X) => monadInv1 H
168  | (bind2 ?F ?G = OK ?X) => monadInv1 H
169  | (?F _ _ _ _ _ _ _ _ = OK _) =>
170      ((progress simpl in H) || unfold F in H); monadInv1 H
171  | (?F _ _ _ _ _ _ _ = OK _) =>
172      ((progress simpl in H) || unfold F in H); monadInv1 H
173  | (?F _ _ _ _ _ _ = OK _) =>
174      ((progress simpl in H) || unfold F in H); 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  end.
186*)
Note: See TracBrowser for help on using the repository browser.