| Monads for state and failure handling |
Set Implicit Arguments.
Require Import Asm.Util.Specif.
Section sig_option.
Variable T : Set.
Variable P : T -> Prop.
Section sig_option_sig_option.
Variable T' : Set.
Variable P' : T' -> Prop.
Definition try_sig_option_sig_option (o : sig_option P) (f : forall x, P x -> sig_option P') :=
match o with
| SNone => SNone _
| SSome x pf => f x pf
end.
End sig_option_sig_option.
Section sig_option_pred_option.
Variable P' : Prop.
Definition try_sig_option_pred_option (o : sig_option P) (f : forall x, P x -> pred_option P') :=
match o with
| SNone => PNone _
| SSome x pf => f x pf
end.
End sig_option_pred_option.
End sig_option.
Section pred_option.
Variable P : Prop.
Section pred_option_sig_option.
Variable T : Set.
Variable P' : T -> Prop.
Definition try_pred_option_sig_option (o : pred_option P) (f : P -> sig_option P') :=
match o with
| PNone => SNone _
| PSome pf => f pf
end.
End pred_option_sig_option.
Section pred_option_pred_option.
Variable P' : Prop.
Definition try_pred_option_pred_option (o : pred_option P) (f : P -> pred_option P') :=
match o with
| PNone => PNone _
| PSome pf => f pf
end.
End pred_option_pred_option.
End pred_option.
Section sig.
Variable T : Set.
Variable P : T -> Prop.
Section sig_anything.
Variable T' : Set.
Definition try_sig_anything (o : sig P) (f : forall x, P x -> T') :=
match o with
| exist x pf => f x pf
end.
End sig_anything.
End sig.
Notation "x ::: pf <- o ; f" := (try_sig_anything o (fun x => fun pf => f))
(at level 60, right associativity).
Notation "x ::: pf <- o ;; f" := (try_sig_anything o (fun x => fun pf => f))
(at level 60, right associativity).
Notation "x <-- o ; f" := (try_pred_option_sig_option o (fun x => f))
(at level 60, right associativity).
Notation "x <-- o ;; f" := (try_pred_option_pred_option o (fun x => f))
(at level 60, right associativity).
Notation "x :: pf <- o ; f" := (try_sig_option_sig_option o (fun x => fun pf => f))
(at level 60, right associativity).
Notation "x :: pf <- o ;; f" := (try_sig_option_pred_option o (fun x => fun pf => f))
(at level 60, right associativity).