Error reporting and the error monad.
Require Import String.
Require Import Coqlib.
Close Scope string_scope.
Set Implicit Arguments.
Representation of error messages.
Compile-time errors produce an error message, represented in Coq
as a list of either substrings or positive numbers encoding
a source-level identifier (see module AST).
Inductive errcode:
Type :=
|
MSG:
string ->
errcode
|
CTX:
positive ->
errcode
|
POS:
positive ->
errcode.
Definition errmsg:
Type :=
list errcode.
Definition msg (
s:
string) :
errmsg :=
MSG s ::
nil.
The error monad
Compilation functions that can fail have return type res A.
The return value is either OK res to indicate success,
or Error msg to indicate failure.
Inductive res (
A:
Type) :
Type :=
|
OK:
A ->
res A
|
Error:
errmsg ->
res A.
Arguments Error [
A].
To automate the propagation of errors, we use a monadic style
with the following bind operation.
Definition bind (
A B:
Type) (
f:
res A) (
g:
A ->
res B) :
res B :=
match f with
|
OK x =>
g x
|
Error msg =>
Error msg
end.
Definition bind2 (
A B C:
Type) (
f:
res (
A *
B)) (
g:
A ->
B ->
res C) :
res C :=
match f with
|
OK (
x,
y) =>
g x y
|
Error msg =>
Error msg
end.
The do notation, inspired by Haskell's, keeps the code readable.
Declare Scope error_monad_scope.
Notation "'
do'
X <-
A ;
B" := (
bind A (
fun X =>
B))
(
at level 200,
X ident,
A at level 100,
B at level 200)
:
error_monad_scope.
Notation "'
do' (
X ,
Y ) <-
A ;
B" := (
bind2 A (
fun X Y =>
B))
(
at level 200,
X ident,
Y ident,
A at level 100,
B at level 200)
:
error_monad_scope.
Remark bind_inversion:
forall (
A B:
Type) (
f:
res A) (
g:
A ->
res B) (
y:
B),
bind f g =
OK y ->
exists x,
f =
OK x /\
g x =
OK y.
Proof.
intros until y. destruct f; simpl; intros.
exists a; auto.
discriminate.
Qed.
Remark bind2_inversion:
forall (
A B C:
Type) (
f:
res (
A*
B)) (
g:
A ->
B ->
res C) (
z:
C),
bind2 f g =
OK z ->
exists x,
exists y,
f =
OK (
x,
y) /\
g x y =
OK z.
Proof.
intros until z. destruct f; simpl.
destruct p; simpl; intros. exists a; exists b; auto.
intros; discriminate.
Qed.
Assertions
Definition assertion_failed {
A:
Type} :
res A :=
Error(
msg "
Assertion failed").
Notation "'
assertion'
A ;
B" := (
if A then B else assertion_failed)
(
at level 200,
A at level 100,
B at level 200)
:
error_monad_scope.
This is the familiar monadic map iterator.
Local Open Scope error_monad_scope.
Section mmap.
Context (
A B:
Type).
Variable (
f:
A ->
res B).
Fixpoint mmap (
l:
list A) {
struct l} :
res (
list B) :=
match l with
|
nil =>
OK nil
|
hd ::
tl =>
do hd' <-
f hd;
do tl' <-
mmap tl;
OK (
hd' ::
tl')
end.
Remark mmap_inversion:
forall (
l:
list A) (
l':
list B),
mmap l =
OK l' ->
list_forall2 (
fun x y =>
f x =
OK y)
l l'.
Proof.
induction l;
simpl;
intros.
inversion_clear H.
constructor.
destruct (
bind_inversion _ _ H)
as [
hd' [
P Q]].
destruct (
bind_inversion _ _ Q)
as [
tl' [
R S]].
inversion_clear S.
constructor.
auto.
auto.
Qed.
End mmap.
Reasoning over monadic computations
The
monadInv H tactic below simplifies hypotheses of the form
H: (do x <- a; b) = OK res
By definition of the bind operation, both computations
a and
b must succeed for their composition to succeed. The tactic
therefore generates the following hypotheses:
x: ...
H1: a = OK x
H2: b x = OK res
:=
match type of H with
| (
OK _ =
OK _) =>
inversion H;
clear H;
try subst
| (
Error _ =
OK _) =>
discriminate
| (
bind ?
F ?
G =
OK ?
X) =>
let x :=
fresh "
x"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind_inversion F G H)
as [
x [
EQ1 EQ2]];
clear H;
try (
monadInv1 EQ2))))
| (
bind2 ?
F ?
G =
OK ?
X) =>
let x1 :=
fresh "
x"
in (
let x2 :=
fresh "
x"
in (
let EQ1 :=
fresh "
EQ"
in (
let EQ2 :=
fresh "
EQ"
in (
destruct (
bind2_inversion F G H)
as [
x1 [
x2 [
EQ1 EQ2]]];
clear H;
try (
monadInv1 EQ2)))))
| (
match ?
X with left _ =>
_ |
right _ =>
assertion_failed end =
OK _) =>
destruct X; [
try (
monadInv1 H) |
discriminate]
| (
match (
negb ?
X)
with true =>
_ |
false =>
assertion_failed end =
OK _) =>
destruct X as []
eqn:?;
simpl negb in H; [
discriminate |
try (
monadInv1 H)]
| (
match ?
X with true =>
_ |
false =>
assertion_failed end =
OK _) =>
destruct X as []
eqn:?; [
try (
monadInv1 H) |
discriminate]
| (
mmap ?
F ?
L =
OK ?
M) =>
generalize (
mmap_inversion F L H);
intro
end.
Ltac monadInv H :=
monadInv1 H ||
match type of H with
| (?
F _ _ _ _ _ _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
| (?
F _ =
OK _) =>
((
progress simpl in H) ||
unfold F in H);
monadInv1 H
end.