source: src/common/Errors.ma @ 2428

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

Initial state is in the labelling simulation
(modulo global envs results).

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