error.v 6.19 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 3 4
(* This file is distributed under the terms of the BSD license. *)
Require Export list.

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 30
Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
  (at level 65, next at level 35, 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 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
Lemma error_associative {S E A B C} (f : A  error S E B) (g : B  error S E C) x s :
  ((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 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
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
  | H : ((_ = _) = _) _ = _ |- _ => rewrite error_associative in H
  | 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.