fail and nondet free monads, fastproduct with free monads

free.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import all_ssreflect classical_sets.
 Require Import monad_lib hierarchy.
 
 (* WIP
@@ -64,24 +64,53 @@ End monadfree.
 End MonadFree.
 Notation freeMonad := MonadFree.t.
 
-Section state_monad.
-Variable S : Type.
+Module freeFail.
+Inductive Cmd : Type := Abort : Cmd.
+Definition Res (c : Cmd) : Type := let Abort := c in False.
+Definition t : monad := freeMonad Res.
+Definition abort (A : pointedType) := @Step _ Res A Abort (fun _ => Ret point : t _).
+Definition defaultHandler (A : pointedType) (x : t A) : A :=
+  match x with
+  | Pure y => y
+  | Step Abort _ => point
+  end.
+End freeFail.
 
-Inductive Cmd :=
-| Get
-| Put : S -> Cmd.
+Require Import fail_lib.
 
+Canonical nat_pointedType := PointedType nat O.
+
+Section example.
+Local Open Scope mprog.
+Fixpoint freefastprod (s : seq nat) : freeFail.t nat :=
+  match s with
+  | [::] => Ret 1
+  | O :: _ => freeFail.abort nat_pointedType
+  | h :: t => fmap (fun x => x * h) (freefastprod t)
+end.
+Example is6 :  freeFail.defaultHandler (freefastprod [:: 1; 2; 3]) = 6.
+Proof. by[]. Qed.
+Example isO :  freeFail.defaultHandler (freefastprod [:: 1; O; 3]) = O.
+Proof. by[]. Qed.
+End example.
+
+Module freeState.
+Section free_state.
+Variable S : Type.
+Inductive Cmd := Get | Put : S -> Cmd.
 Definition Res (c : Cmd) :=
   match c with
   | Get => S
   | Put _ => unit
   end.
-
-Definition State : monad := freeMonad Res.
-Definition get : State S := Step Get (@RET State _).
-Definition put : S -> State unit := fun s => Step (Put s) (fun _ => Ret tt : State _).
-
-End state_monad.
+Definition t : monad := freeMonad Res.
+Definition get : t S := Step Get (@RET t _).
+Definition put : S -> t unit := fun s => Step (Put s) (fun _ => Ret tt : t _).
+End free_state.
+End freeState.
+Notation State := freeState.t.
+Notation get := freeState.get.
+Notation put := freeState.put.
 
 Local Open Scope monae_scope.
 Definition incr' : State nat unit := @get _ >>= (@put _ \o (fun n => n.+1)).
@@ -92,8 +121,10 @@ Record mixin_of (S : Type) := Mixin {
   r1 : forall A (a : A) s, run (Pure a) s = (a, s) ;
   r2 : forall A B (m : State S A) (f : A -> State S B) s,
     run (m >>= f) s = let: (x, s') := run m s in run (f x) s';
-  r3 : forall A (k : _ -> Free (@Res S) A) s, run (@Step _ (@Res S) _ (@Get S) k) s = run (k s) s ;
-  r4 : forall A (k : _ -> Free (@Res S) A) s' s, run (@Step _ (@Res S) _ (@Put S s) k) s' = @run A (k tt) s }.
+  r3 : forall A (k : _ -> Free (@freeState.Res S) A) s,
+      run (@Step _ (@freeState.Res S) _ (@freeState.Get S) k) s = run (k s) s ;
+  r4 : forall A (k : _ -> Free (@freeState.Res S) A) s' s,
+      run (@Step _ (@freeState.Res S) _ (@freeState.Put S s) k) s' = @run A (k tt) s }.
 Structure t (S : Type) := Pack { carrier : Type ; class : mixin_of S }.
 Module Exports.
 Definition fRun (S : Type) (M : t S) : forall A : Type, State S A -> S -> A * S :=
@@ -112,11 +143,11 @@ Proof. by case: M => ? []. Qed.
 Lemma runfreestate_bind A B (m : State S A) (f : A -> State S B) s :
     fRun M (m >>= f) s = let: (x, s') := fRun M m s in fRun M (f x) s'.
 Proof. by case: M => ? []. Qed.
-Lemma runfreestate_Get A (k : _ -> Free (@Res S) A) s :
-  fRun M (@Step _ (@Res S) _ (@Get S) k) s = fRun M (k s) s.
+Lemma runfreestate_Get A (k : _ -> Free (@freeState.Res S) A) s :
+  fRun M (@Step _ (@freeState.Res S) _ (@freeState.Get S) k) s = fRun M (k s) s.
 Proof. by case: M => ? []. Qed.
-Lemma runfreestate_Put A (k : _ -> Free (@Res S) A) s' s :
-  fRun M (@Step _ (@Res S) _ (@Put S s) k) s' = fRun M (k tt) s.
+Lemma runfreestate_Put A (k : _ -> Free (@freeState.Res S) A) s' s :
+  fRun M (@Step _ (@freeState.Res S) _ (@freeState.Put S s) k) s' = fRun M (k tt) s.
 Proof. by case: M => ? []. Qed.
 End monadrunfreestate_lemmas.
 
@@ -134,6 +165,25 @@ by rewrite runfreestate_Pure /=.
 Abort.
 End example.
 
+Module freeNondet.
+Inductive Cmd : Type := Fail | Choice.
+Definition Res (c : Cmd) : Type :=
+  match c with
+  | Fail => False
+  | Choice => bool
+  end.
+Definition t : monad := freeMonad Res.
+Definition fail (A : pointedType) := @Step _ _ A Fail (fun _ => Ret point : t _).
+Definition choice A (m1 m2 : t A) : t A :=
+  Step Choice (fun b : bool => if b then m1 else m2).
+Fixpoint run A (m : t A) :=
+  match m with
+  | Pure x => [:: x]
+  | Step Fail _ => [::]
+  | Step Choice k => run (k true) ++ run (k false)
+  end.
+End freeNondet.
+
 (* WIP
   reference
   Seynaeve, Pauwels, Schrijvers, Sate will do, TFP 2020