source: src/common/Errors.ma @ 1626

Last change on this file since 1626 was 1626, checked in by campbell, 8 years ago

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File size: 11.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 "basics/types.ma".
17include "basics/logic.ma".
18include "basics/lists/list.ma".
19include "common/PreIdentifiers.ma".
20include "basics/russell.ma".
21
22(* * Error reporting and the error monad. *)
23
24(* * * Representation of error messages. *)
25
26(* * Compile-time errors produce an error message, represented in Coq
27  as a list of either substrings or positive numbers encoding
28  a source-level identifier (see module AST). *)
29
30inductive errcode: Type[0] :=
31  | MSG: String → errcode
32  | CTX: ∀tag:String. identifier tag → errcode.
33
34definition errmsg: Type[0] ≝ list errcode.
35
36definition msg : String → errmsg ≝ λs. [MSG s].
37
38(* * * The error monad *)
39
40(* * Compilation functions that can fail have return type [res A].
41  The return value is either [OK res] to indicate success,
42  or [Error msg] to indicate failure. *)
43
44inductive res (A: Type[0]) : Type[0] ≝
45| OK: A → res A
46| Error: errmsg → res A.
47
48(*Implicit Arguments Error [A].*)
49
50(* * To automate the propagation of errors, we use a monadic style
51  with the following [bind] operation. *)
52
53definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B.
54  match f with
55  [ OK x ⇒ g x
56  | Error msg ⇒ Error ? msg
57  ].
58
59definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
60  match f with
61  [ OK v ⇒ g (fst … v) (snd … v)
62  | Error msg => Error ? msg
63  ].
64
65definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
66  match f with
67  [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v)
68  | Error msg => Error ? msg
69  ].
70 
71(* Not sure what level to use *)
72notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
73notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
74notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
75notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
76interpretation "error monad bind" 'bind e f = (bind ?? e f).
77notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
78notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
79notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
80notation < "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'})}.
81interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
82notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
83notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
84notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
85notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
86interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f).
87(*interpretation "error monad ret" 'ret e = (ret ? e).
88notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
89
90(* Dependent pair version. *)
91notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
92  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
93
94lemma Prod_extensionality:
95  ∀a, b: Type[0].
96  ∀p: a × b.
97    p = 〈fst … p, snd … p〉.
98  #a #b #p //
99qed.
100
101definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
102λA,B,C,P,e,f.
103  match e with
104  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
105  | Error msg ⇒ Error ? msg
106  ].
107  <(Prod_extensionality A B v')
108  assumption
109qed.
110
111notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
112interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
113
114(*
115(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
116
117Notation "'do' X <- A ; B" := (bind A (fun X => B))
118 (at level 200, X ident, A at level 100, B at level 200)
119 : error_monad_scope.
120
121Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
122 (at level 200, X ident, Y ident, A at level 100, B at level 200)
123 : error_monad_scope.
124*)
125lemma bind_inversion:
126  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
127  bind ?? f g = OK ? y →
128  ∃x. f = OK ? x ∧ g x = OK ? y.
129#A #B #f #g #y cases f;
130[ #a #e %{a} whd in e:(??%?); /2/;
131| #m #H whd in H:(??%?); destruct (H);
132] qed.
133
134lemma bind2_inversion:
135  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
136  bind2 ??? f g = OK ? z →
137  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
138#A #B #C #f #g #z cases f;
139[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
140| #m #H whd in H:(??%?); destruct
141] qed.
142
143(*
144Open Local Scope error_monad_scope.
145
146(** This is the familiar monadic map iterator. *)
147*)
148
149let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝
150  match l with
151  [ nil ⇒ OK ? []
152  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
153  ].
154
155(* And mmap coupled with proofs. *)
156
157let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
158match l with
159[ nil ⇒ OK ? «nil B, ?»
160| cons h t ⇒
161    do h' ← f h;
162    do t' ← mmap_sigma A B P f t;
163    OK ? «cons B h' t', ?»
164].
165whd // %
166[ @(pi2 … h')
167| cases t' #l' #p @p
168] qed.
169
170(*
171lemma mmap_inversion:
172  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
173  mmap A B f l = OK ? l' →
174  list_forall2 (fun x y => f x = OK y) l l'.
175Proof.
176  induction l; simpl; intros.
177  inversion_clear H. constructor.
178  destruct (bind_inversion _ _ H) as [hd' [P Q]].
179  destruct (bind_inversion _ _ Q) as [tl' [R S]].
180  inversion_clear S.
181  constructor. auto. auto.
182Qed.
183*)
184
185(* A monadic fold_lefti *)
186let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
187                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
188  match l with
189    [ nil ⇒ x
190    | cons hd tl ⇒
191       do x ← x ;
192       mfold_left_i_aux A B f (f i x hd) (S i) tl
193    ].
194
195definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
196
197
198(* A monadic fold_left2 *)
199
200axiom WrongLength: String.
201
202let rec mfold_left2
203  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
204  (left: list B) (right: list C) on left: res A ≝
205  match left with
206  [ nil ⇒
207    match right with
208    [ nil ⇒ accu
209    | cons hd tl ⇒ Error ? (msg WrongLength)
210    ]
211  | cons hd tl ⇒
212    match right with
213    [ nil ⇒ Error ? (msg WrongLength)
214    | cons hd' tl' ⇒
215       do accu ← accu;
216       mfold_left2 … f (f accu hd hd') tl tl'
217    ]
218  ].
219
220(*
221(** * Reasoning over monadic computations *)
222
223(** The [monadInv H] tactic below simplifies hypotheses of the form
224<<
225        H: (do x <- a; b) = OK res
226>>
227    By definition of the bind operation, both computations [a] and
228    [b] must succeed for their composition to succeed.  The tactic
229    therefore generates the following hypotheses:
230
231         x: ...
232        H1: a = OK x
233        H2: b x = OK res
234*)
235
236Ltac monadInv1 H :=
237  match type of H with
238  | (OK _ = OK _) =>
239      inversion H; clear H; try subst
240  | (Error _ = OK _) =>
241      discriminate
242  | (bind ?F ?G = OK ?X) =>
243      let x := fresh "x" in (
244      let EQ1 := fresh "EQ" in (
245      let EQ2 := fresh "EQ" in (
246      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
247      clear H;
248      try (monadInv1 EQ2))))
249  | (bind2 ?F ?G = OK ?X) =>
250      let x1 := fresh "x" in (
251      let x2 := fresh "x" in (
252      let EQ1 := fresh "EQ" in (
253      let EQ2 := fresh "EQ" in (
254      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
255      clear H;
256      try (monadInv1 EQ2)))))
257  | (mmap ?F ?L = OK ?M) =>
258      generalize (mmap_inversion F L H); intro
259  end.
260
261Ltac monadInv H :=
262  match type of H with
263  | (OK _ = OK _) => monadInv1 H
264  | (Error _ = OK _) => monadInv1 H
265  | (bind ?F ?G = OK ?X) => monadInv1 H
266  | (bind2 ?F ?G = OK ?X) => monadInv1 H
267  | (?F _ _ _ _ _ _ _ _ = OK _) =>
268      ((progress simpl in H) || unfold F in H); monadInv1 H
269  | (?F _ _ _ _ _ _ _ = OK _) =>
270      ((progress simpl in H) || unfold F in H); monadInv1 H
271  | (?F _ _ _ _ _ _ = OK _) =>
272      ((progress simpl in H) || unfold F in H); monadInv1 H
273  | (?F _ _ _ _ _ = OK _) =>
274      ((progress simpl in H) || unfold F in H); monadInv1 H
275  | (?F _ _ _ _ = OK _) =>
276      ((progress simpl in H) || unfold F in H); monadInv1 H
277  | (?F _ _ _ = OK _) =>
278      ((progress simpl in H) || unfold F in H); monadInv1 H
279  | (?F _ _ = OK _) =>
280      ((progress simpl in H) || unfold F in H); monadInv1 H
281  | (?F _ = OK _) =>
282      ((progress simpl in H) || unfold F in H); monadInv1 H
283  end.
284*)
285
286
287definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
288lemma opt_OK: ∀A,m,P,e.
289  (∀v. e = Some ? v → P v) →
290  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
291#A #m #P #e elim e; /2/;
292qed.
293
294(* A variation of bind and its notation that provides an equality proof for
295   later use. *)
296
297definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
298  match f return λx. f = x → ? with
299  [ OK x ⇒ g x
300  | Error msg ⇒ λ_. Error ? msg
301  ] (refl ? f).
302
303notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
304
305definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
306  match f return λx. f = x → ? with
307  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
308  | Error msg ⇒ λ_. Error ? msg
309  ] (refl ? f).
310
311notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
312
313definition res_to_opt : ∀A:Type[0]. res A → option A ≝
314 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
315
Note: See TracBrowser for help on using the repository browser.