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

Last change on this file since 492 was 487, checked in by campbell, 9 years ago

Port Clight semantics to the new-new matita syntax.

File size: 7.4 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".
18
19(* * Error reporting and the error monad. *)
20(*
21(** * Representation of error messages. *)
22
23(** Compile-time errors produce an error message, represented in Coq
24  as a list of either substrings or positive numbers encoding
25  a source-level identifier (see module AST). *)
26
27Inductive errcode: Type :=
28  | MSG: string -> errcode
29  | CTX: positive -> errcode.
30
31Definition errmsg: Type := list errcode.
32
33Definition msg (s: string) : errmsg := MSG s :: nil.
34*)
35(* * * The error monad *)
36
37(* * Compilation functions that can fail have return type [res A].
38  The return value is either [OK res] to indicate success,
39  or [Error msg] to indicate failure. *)
40
41inductive res (A: Type[0]) : Type[0] ≝
42| OK: A → res A
43| Error: (* FIXME errmsg →*) res A.
44
45(*Implicit Arguments Error [A].*)
46
47(* * To automate the propagation of errors, we use a monadic style
48  with the following [bind] operation. *)
49
50definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B.
51  match f with
52  [ OK x ⇒ g x
53  | Error (*msg*) ⇒ Error ? (*msg*)
54  ].
55
56definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
57  match f with
58  [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
59  | Error (*msg*) => Error ? (*msg*)
60  ].
61
62(* Not sure what level to use *)
63notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
64notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
65notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
66notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
67interpretation "error monad bind" 'bind e f = (bind ?? e f).
68notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
69notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
70notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
71notation < "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'})}.
72interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
73(*interpretation "error monad ret" 'ret e = (ret ? e).
74notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
75
76(*
77(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
78
79Notation "'do' X <- A ; B" := (bind A (fun X => B))
80 (at level 200, X ident, A at level 100, B at level 200)
81 : error_monad_scope.
82
83Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
84 (at level 200, X ident, Y ident, A at level 100, B at level 200)
85 : error_monad_scope.
86*)
87lemma bind_inversion:
88  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
89  bind ?? f g = OK ? y →
90  ∃x. f = OK ? x ∧ g x = OK ? y.
91#A #B #f #g #y cases f;
92[ #a #e %{a} whd in e:(??%?); /2/;
93| #H whd in H:(??%?); destruct (H);
94] qed.
95
96lemma bind2_inversion:
97  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
98  bind2 ??? f g = OK ? z →
99  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
100#A #B #C #f #g #z cases f;
101[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
102| #H whd in H:(??%?); destruct
103] qed.
104
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*)
193
194
195definition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
196lemma opt_OK: ∀A,P,e.
197  (∀v. e = Some ? v → P v) →
198  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
199#A #P #e elim e; /2/;
200qed.
Note: See TracBrowser for help on using the repository browser.