error.v 6.17 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
(* This file is distributed under the terms of the BSD license. *)
3
Require Export prelude.list.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5
Definition error (S E A : Type) : Type := S  E + (A * S).
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
Definition error_eval {S E A} (x : error S E A) (s : S) : E + A :=
  match x s with inl e => inl e | inr (a,_) => inr a end.

Instance error_ret {S E} : MRet (error S E) := λ A x s, inr (x,s).
Instance error_bind {S E} : MBind (error S E) := λ A B f x s,
  match x s with
  | inr (a,s') => f a s'
  | inl e => inl e
  end.
Instance error_fmap {S E} : FMap (error S E) := λ A B f x s,
  match x s with
  | inr (a,s') => inr (f a,s')
  | inl e => inl e
  end.
Definition fail {S E A} (e : E) : error S E A := λ s, inl e.

Definition modify {S E} (f : S  S) : error S E () := λ s, inr ((), f s).
Definition gets {S E A} (f : S  A) : error S E A := λ s, inr (f s, s).

Definition error_guard {E} P {dec : Decision P} {S A}
    (e : E) (f : P  error S E A) : error S E A :=
  match decide P with left H => f H | right _ => fail e end.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  (at level 65, only parsing, right associativity) : C_scope.
31 32
Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
  match x with Some a => mret a | None => fail e end.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
Lemma error_bind_ret {S E A B} (f : A  error S E B) s s'' x b :
  (x = f) s = mret b s''   a s', x s = mret a s'  f a s' = mret b s''.
Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma error_fmap_ret {S E A B} (f : A  B) s s' (x : error S E A) b :
  (f <$> x) s = mret b s'   a, x s = mret a s'  b = f a.
Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
Lemma error_of_option_ret {S E A} (s s' : S) (o : option A) (e : E) a :
  error_of_option o e s = mret a s'  o = Some a  s = s'.
Proof. compute; destruct o; naive_solver. Qed.
Lemma error_guard_ret {S E A} `{dec : Decision P} s s' (x : error S E A) e a :
  (guard P with e ; x) s = mret a s'  P  x s = mret a s'.
Proof. compute; destruct dec; naive_solver. Qed.
Lemma error_fmap_bind {S E A B C} (f : A  B) (g : B  error S E C) x s :
  ((f <$> x) = g) s = (x = g  f) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
49

50
Lemma error_assoc {S E A B C} (f : A  error S E B) (g : B  error S E C) x s :
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
  ((x = f) = g) s = (a  x; f a = g) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_of_option_bind {S E A B} (f : A  option B) o e :
  error_of_option (S := S) (E:=E) (o = f) e
  = a  error_of_option o e; error_of_option (f a) e.
Proof. by destruct o. Qed.

Lemma error_gets_spec {S E A} (g : S  A) s : gets (E:=E) g s = mret (g s) s.
Proof. done. Qed.
Lemma error_modify_spec {S E} (g : S  S) s : modify (E:=E) g s = mret () (g s).
Proof. done. Qed.
Lemma error_left_gets {S E A B} (g : S  A) (f : A  error S E B) s :
  (gets (E:=E) g = f) s = f (g s) s.
Proof. done. Qed.
Lemma error_left_modify {S E B} (g : S  S) (f : unit  error S E B) s :
  (modify (E:=E) g = f) s = f () (g s).
Proof. done. Qed.
Lemma error_left_id {S E A B} (a : A) (f : A  error S E B) :
  (mret a = f) = f a.
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72 73 74 75 76 77 78 79 80 81
Ltac generalize_errors :=
  csimpl;
  let gen_error e :=
    try (is_var e; fail 1); generalize e;
    let x := fresh "err" in intros x in
  repeat match goal with
  | |- appcontext[ fail ?e ] => gen_error e
  | |- appcontext[ error_guard _ ?e ] => gen_error e
  | |- appcontext[ error_of_option _ ?e ] => gen_error e
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
Tactic Notation "simplify_error_equality" :=
  repeat match goal with
84 85 86 87 88 89
  | H : context [ gets _ _ _ ] |- _ => rewrite error_gets_spec in H
  | H : context [ modify _ _ _ ] |- _ => rewrite error_modify_spec in H
  | H : (mret (M:=error _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
  | H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
  | H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
  | H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  | _ => progress simplify_equality'
91 92 93 94 95 96 97
  | H : error_of_option _ _ _ = _ |- _ =>
    apply error_of_option_ret in H; destruct H
  | H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
    apply error_bind_ret in H; destruct H as (?&?&?&?)
  | H : fmap (M:=error _ _) _ _ _ = _ |- _ =>
    apply error_fmap_ret in H; destruct H as (?&?&?)
  | H : mbind (M:=option) _ _ = _ |- _ =>
98
    apply bind_Some in H; destruct H as (?&?&?)
99
  | H : fmap (M:=option) _ _ = _ |- _ =>
100
    apply fmap_Some in H; destruct H as (?&?&?)
101 102 103 104
  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107
  | _ => progress case_decide
  end.

108 109 110 111 112 113 114 115 116
Tactic Notation "error_proceed" :=
  repeat match goal with
  | H : context [ gets _ _ ] |- _ => rewrite error_gets_spec in H
  | H : context [ modify _ _ ] |- _ => rewrite error_modify_spec in H
  | H : context [ error_of_option _ _ ] |- _ => rewrite error_of_option_bind in H
  | H : (mret (M:= _ _) _ = _) _ = _ |- _ => rewrite error_left_id in H
  | H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
  | H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
  | H : ((_ <$> _) = _) _ = _ |- _ => rewrite error_fmap_bind in H
117
  | H : ((_ = _) = _) _ = _ |- _ => rewrite error_assoc in H
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
  | H : (error_guard _ _ _) _ = _ |- _ =>
     let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
  | _ => progress simplify_equality'
  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
  end.
Tactic Notation "error_proceed"
    simple_intropattern(a) "as" simple_intropattern(s) :=
  error_proceed;
  lazymatch goal with
  | H : (error_of_option ?o _ = _) _ = _ |- _ => destruct o as [a|] eqn:?
  | H : error_of_option ?o _ _ = _ |- _ => destruct o as [a|] eqn:?
  | H : (_ = _) _ = _ |- _ => apply error_bind_ret in H; destruct H as (a&s&?&H)
  | H : (_ <$> _) _ = _ |- _ => apply error_fmap_ret in H; destruct H as (a&?&?)
  end;
  error_proceed.