source: C-semantics/Errors.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 11 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

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