source: src/common/Errors.ma @ 2755

Last change on this file since 2755 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 8.7 KB
Line 
1include "basics/types.ma".
2include "basics/logic.ma".
3include "basics/lists/list.ma".
4include "common/PreIdentifiers.ma".
5include "basics/russell.ma".
6include "utilities/monad.ma".
7include "utilities/option.ma".
8include "common/ErrorMessages.ma".
9
10(* * Error reporting and the error monad. *)
11
12(* * * Representation of error messages. *)
13
14(* * Compile-time errors produce an error message, represented in Coq
15  as a list of either substrings or positive numbers encoding
16  a source-level identifier (see module AST). *)
17
18inductive errcode: Type[0] :=
19  | MSG: ErrorMessage → errcode
20  | CTX: ∀tag:identifierTag. identifier tag → errcode.
21
22definition errmsg: Type[0] ≝ list errcode.
23
24definition msg : ErrorMessage → errmsg ≝ λs. [MSG s].
25
26(* * * The error monad *)
27
28(* * Compilation functions that can fail have return type [res A].
29  The return value is either [OK res] to indicate success,
30  or [Error msg] to indicate failure. *)
31
32(* Paolo: not using except for backward compatbility
33  (would break Error ? msg) *)
34
35inductive res (A: Type[0]) : Type[0] ≝
36| OK: A → res A
37| Error: errmsg → res A.
38
39(*Implicit Arguments Error [A].*)
40
41definition Res ≝ MakeMonadProps
42  (* the monad *)
43  res
44  (* return *)
45  (λX.OK X)
46  (* bind *)
47  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
48  ????.
49//
50[(* bind_ret *)
51 #X*normalize //
52|(* bind_bind *)
53 #X#Y#Z*normalize //
54| normalize #X #Y * normalize /2/
55]
56qed.
57
58include "hints_declaration.ma".
59alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
60unification hint 0 ≔ X;
61N ≟ max_def Res
62(*---------------*) ⊢
63res X ≡ monad N X
64.
65
66(*(* Dependent pair version. *)
67notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
68  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
69
70lemma Prod_extensionality:
71  ∀a, b: Type[0].
72  ∀p: a × b.
73    p = 〈fst … p, snd … p〉.
74  #a #b #p //
75qed.
76
77definition 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 ≝
78λA,B,C,P,e,f.
79  match e with
80  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
81  | Error msg ⇒ Error ? msg
82  ].
83  <(Prod_extensionality A B v')
84  assumption
85qed.
86
87notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
88interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
89
90lemma bind_inversion:
91  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
92  (! x ← f ; g x = return y) →
93  ∃x. (f = return x) ∧ (g x = return y).
94#A #B #f #g #y cases f normalize
95[ #a #e %{a} /2 by conj/
96| #m #H destruct (H)
97] qed.
98
99lemma bind2_inversion:
100  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
101  m_bind2 ???? f g = return z →
102  ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z.
103#A #B #C #f #g #z cases f normalize
104[ * #a #b normalize #e %{a} %{b} /2 by conj/
105| #m #H destruct (H)
106] qed.
107
108(*
109Open Local Scope error_monad_scope.*)
110
111(*
112lemma mmap_inversion:
113  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
114  mmap A B f l = OK ? l' →
115  list_forall2 (fun x y => f x = OK y) l l'.
116Proof.
117  induction l; simpl; intros.
118  inversion_clear H. constructor.
119  destruct (bind_inversion _ _ H) as [hd' [P Q]].
120  destruct (bind_inversion _ _ Q) as [tl' [R S]].
121  inversion_clear S.
122  constructor. auto. auto.
123Qed.
124*)
125
126(* A monadic fold_lefti *)
127let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
128                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
129  match l with
130    [ nil ⇒ x
131    | cons hd tl ⇒
132       ! x ← x ;
133       mfold_left_i_aux A B f (f i x hd) (S i) tl
134    ].
135
136definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
137
138
139(* A monadic fold_left2 *)
140
141let rec mfold_left2
142  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
143  (left: list B) (right: list C) on left: res A ≝
144  match left with
145  [ nil ⇒
146    match right with
147    [ nil ⇒ accu
148    | cons hd tl ⇒ Error ? (msg WrongLength)
149    ]
150  | cons hd tl ⇒
151    match right with
152    [ nil ⇒ Error ? (msg WrongLength)
153    | cons hd' tl' ⇒
154       ! accu ← accu;
155       mfold_left2 … f (f accu hd hd') tl tl'
156    ]
157  ].
158
159(*
160(** * Reasoning over monadic computations *)
161
162(** The [monadInv H] tactic below simplifies hypotheses of the form
163<<
164        H: (do x <- a; b) = OK res
165>>
166    By definition of the bind operation, both computations [a] and
167    [b] must succeed for their composition to succeed.  The tactic
168    therefore generates the following hypotheses:
169
170         x: ...
171        H1: a = OK x
172        H2: b x = OK res
173*)
174
175Ltac monadInv1 H :=
176  match type of H with
177  | (OK _ = OK _) =>
178      inversion H; clear H; try subst
179  | (Error _ = OK _) =>
180      discriminate
181  | (bind ?F ?G = OK ?X) =>
182      let x := fresh "x" in (
183      let EQ1 := fresh "EQ" in (
184      let EQ2 := fresh "EQ" in (
185      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
186      clear H;
187      try (monadInv1 EQ2))))
188  | (bind2 ?F ?G = OK ?X) =>
189      let x1 := fresh "x" in (
190      let x2 := fresh "x" in (
191      let EQ1 := fresh "EQ" in (
192      let EQ2 := fresh "EQ" in (
193      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
194      clear H;
195      try (monadInv1 EQ2)))))
196  | (mmap ?F ?L = OK ?M) =>
197      generalize (mmap_inversion F L H); intro
198  end.
199
200Ltac monadInv H :=
201  match type of H with
202  | (OK _ = OK _) => monadInv1 H
203  | (Error _ = OK _) => monadInv1 H
204  | (bind ?F ?G = OK ?X) => monadInv1 H
205  | (bind2 ?F ?G = OK ?X) => monadInv1 H
206  | (?F _ _ _ _ _ _ _ _ = OK _) =>
207      ((progress simpl in H) || unfold F in H); monadInv1 H
208  | (?F _ _ _ _ _ _ _ = OK _) =>
209      ((progress simpl in H) || unfold F in H); monadInv1 H
210  | (?F _ _ _ _ _ _ = OK _) =>
211      ((progress simpl in H) || unfold F in H); monadInv1 H
212  | (?F _ _ _ _ _ = OK _) =>
213      ((progress simpl in H) || unfold F in H); monadInv1 H
214  | (?F _ _ _ _ = OK _) =>
215      ((progress simpl in H) || unfold F in H); monadInv1 H
216  | (?F _ _ _ = OK _) =>
217      ((progress simpl in H) || unfold F in H); monadInv1 H
218  | (?F _ _ = OK _) =>
219      ((progress simpl in H) || unfold F in H); monadInv1 H
220  | (?F _ = OK _) =>
221      ((progress simpl in H) || unfold F in H); monadInv1 H
222  end.
223*)
224
225
226definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
227lemma opt_OK: ∀A,m,P,e.
228  (∀v. e = Some ? v → P v) →
229  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
230#A #m #P #e elim e; /2/;
231qed.
232
233lemma opt_eq_from_res : ∀T,m,e,v.
234  opt_to_res T m e = return v →
235  e = Some T v.
236#T #m * [ #v #E normalize in E; destruct | #e' #v #E normalize in E; destruct % ]
237qed.
238
239coercion opt_eq_from_res :
240  ∀T,m,e,v. ∀E:opt_to_res T m e = return v. e = Some T v ≝ opt_eq_from_res
241  on _E:eq (res ?) ?? to eq (option ?) ??.
242
243(* A variation of bind and its notation that provides an equality proof for
244   later use. *)
245
246definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
247  match f return λx. f = x → ? with
248  [ OK x ⇒ g x
249  | Error msg ⇒ λ_. Error ? msg
250  ] (refl ? f).
251
252notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
253
254lemma bind_as_inversion:
255  ∀A,B: Type[0]. ∀f: res A. ∀g: ∀a:A. f = OK A a → res B. ∀y: B.
256  (do x as E ← f; g x E = return y) →
257  ∃x. ∃E:f = return x. g x E = return y.
258#A #B #f cases f normalize
259[ #a #g #y #e %{a} /2/
260| #m #g #y #H destruct (H)
261] qed.
262
263definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
264  match f return λx. f = x → ? with
265  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
266  | Error msg ⇒ λ_. Error ? msg
267  ] (refl ? f).
268
269notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
270
271lemma bind2_eq_inversion:
272  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
273  bind2_eq ??? f g = return z →
274  ∃x. ∃y. ∃Eq. g x y Eq = return z.
275#A #B #C #f cases f
276[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? (OK ? 〈a,b〉))} @Heq
277| #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
278qed.
279
280definition res_to_opt : ∀A:Type[0]. res A → option A ≝
281 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
282
283(* aliases for backward compatibility *)
284definition bind ≝ m_bind Res.
285definition bind2 ≝ m_bind2 Res.
286definition bind3 ≝ m_bind3 Res.
287definition mmap ≝ m_list_map Res.
288definition mmap_sigma ≝ m_list_map_sigma Res.
Note: See TracBrowser for help on using the repository browser.