Mrec

theories/Core/Utils.v

@@ -11,7 +11,7 @@ Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type :=
   mtrigger : forall {X}, E X -> M X.
 
 Polymorphic Class MonadBr (B : Type -> Type) (M : Type -> Type) : Type :=
-  mbr : forall X (b: B X), M X.
+  mbr : forall {X}, B X -> M X.
 
 Polymorphic Class MonadStep (M : Type -> Type) : Type :=
   mstep : M unit.

theories/Interp/Fold.v

@@ -61,7 +61,7 @@ Definition interp {E B M : Type -> Type}
   {Mstep : MonadStep M}
   {Mbranch : MonadBr B M}
   (h : E ~> M) : ctree E B ~> M :=
-  fold h mbr.
+  fold h (@mbr B M Mbranch).
 
 Arguments interp {E B M FM MM IM _ _ _} h [T].
 

theories/Interp/FoldCTree.v

@@ -122,7 +122,7 @@ Section FoldCTree.
        | GuardF t => Guard (interp h t)
        | StepF  t => Step  (Guard (interp h t))
 	     | VisF e k => bind (h _ e) (fun x => Guard (interp h (k x)))
-	     | BrF c k => bind (mbr _ c) (fun x => Guard (interp h (k x)))
+	     | BrF c k => bind (mbr c) (fun x => Guard (interp h (k x)))
        end)%function.
 
     (** Unfold lemma. *)

theories/Interp/FoldStateT.v

@@ -33,7 +33,7 @@ Arguments fequ : simpl never.
 
 #[global] Instance MonadBr_stateT {S M C} {MM : Monad M} {AM : MonadBr C M}:
   MonadBr C (stateT S M) :=
-  fun X c s => f <- mbr _ c;; ret (s,f).
+  fun X c s => f <- mbr c;; ret (s,f).
 
 #[global] Instance MonadTrigger_stateT {E S M} {MM : Monad M} {MT: MonadTrigger E M} :
   MonadTrigger E (stateT S M) :=
@@ -225,7 +225,7 @@ Section State.
      | GuardF t => Guard (interp_state h t s)
      | StepF t => Step (Guard (interp_state h t s))
  	   | VisF e k => bind (h _ e s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
-	   | BrF c k => bind (mbr (M := stateT _ _) _ c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
+	   | BrF c k => bind (mbr (M := stateT _ _) c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
      end)%function.
 
   Lemma unfold_interp_state `{C-<D} (t : ctree E C R) (s : S) :

theories/Interp/Recursion.v

@@ -0,0 +1,180 @@
+From ExtLib Require Import
+     Structures.Functor
+     Structures.Monad.
+
+From ITree Require Import
+     Basics.Basics
+     Indexed.Sum.
+
+Import ITree.Basics.Basics.Monads.
+
+From CTree Require Import
+  CTree
+  Eq
+  Eq.Epsilon
+  Eq.IterFacts
+  Eq.SSimAlt
+  Misc.Pure
+  Fold.
+
+Import CTreeNotations.
+Open Scope ctree_scope.
+
+(** * General recursion *)
+
+(** *** Mutual recursion *)
+
+(* Implementation of the fixpoint combinator over interaction
+ * trees.
+ *
+ * The implementation is based on the discussion here
+ *   https://gmalecha.github.io/reflections/2018/compositional-coinductive-recursion-in-coq
+ *)
+
+(* The indexed type [D : Type -> Type] gives the signature of
+   a set of functions. For example, a pair of mutually recursive
+   [even : nat -> bool] and [odd : nat -> bool] can be declared
+   as follows:
+
+[[
+   Inductive D : Type -> Type :=
+   | Even : nat -> D bool
+   | Odd  : nat -> D bool.
+]]
+
+   Their mutually recursive definition can then be written finitely
+   (without [Fixpoint]):
+
+[[
+   Definition def : D ~> itree (D +' void1) := fun _ d =>
+     match d with
+     | Even n => match n with
+                 | O => ret true
+                 | S m => trigger (Odd m)
+                 end
+     | Odd n => match n with
+                | O => ret false
+                | S m => trigger (Even m)
+                end
+     end.
+]]
+
+   The function [interp_mrec] below then ties the knot.
+
+[[
+   Definition f : D ~> itree void1 :=
+     interp_mrec def.
+
+   Definition even (n : nat) : itree void1 bool := f _ (Even n).
+   Definition odd  (n : nat) : itree void1 bool := f _ (Odd n).
+]]
+
+   The result is still in the [itree] monad of possibly divergent
+   computations, because [mutfix_itree] doesn't care whether
+   the mutually recursive definition is well-founded.
+
+ *)
+
+(** Interpret an itree in the context of a mutually recursive
+    definition ([ctx]). *)
+Definition interp_mrec {D E B : Type -> Type} 
+           (ctx : D ~> ctree (D +' E) B) : ctree (D +' E) B ~> ctree E B :=
+  fun R =>
+    CTree.iter (fun t : ctree (D +' E) B R =>
+      match observe t with
+      | RetF r => Ret (inr r)
+      | StuckF => Stuck
+      | StepF t => Step (Ret (inl t))
+      | GuardF t => Ret (inl t)
+      | VisF (inl1 d) k => Ret (inl (ctx _ d >>= k))
+      | VisF (inr1 e) k => Vis e (fun x => Ret (inl (k x)))
+      | BrF c k => Br c (fun x => Ret (inl (k x)))
+      end).
+
+Arguments interp_mrec {D E B} ctx [T].
+
+(** Unfold a mutually recursive definition into separate trees,
+    resolving the mutual references. *)
+Definition mrec {D E B : Type -> Type}
+           (ctx : D ~> ctree (D +' E) B) : D ~> ctree E B :=
+  fun R d => interp_mrec ctx (ctx _ d).
+
+Arguments mrec {D E B} ctx [T].
+
+(** Make a recursive call in the handler argument of [mrec]. *)
+Definition trigger_inl1 {D E B : Type -> Type} : D ~> ctree (D +' E) B
+  := fun _ d => CTree.trigger (inl1 d).
+
+Arguments trigger_inl1 {D E B} [T].
+
+(** Here's some syntactic sugar with a notation [mrec-fix]. *)
+
+(** Short for endofunctions, used in [mrec_fix] and [rec_fix]. *)
+(* Local Notation endo T := (T -> T). *)
+
+(* Definition mrec_fix {D E : Type -> Type} *)
+(*            (ctx : endo (D ~> itree (D +' E))) *)
+(*   : D ~> itree E *)
+(*   := mrec (ctx trigger_inl1). *)
+
+(* Notation "'mrec-fix' f d := g" := *)
+(* 	(let D := _ in *)
+(* 	 mrec_fix (D := D) (fun (f : forall T, D T -> _) T (d : D T) => g)) *)
+(*   (at level 200, f ident, d pattern). *)
+(* (* No idea what a good level would be. *) *)
+
+(** *** Simple recursion *)
+
+Inductive callE (A B : Type) : Type -> Type :=
+| Call : A -> callE A B B.
+
+Arguments Call {A B}.
+
+(** Get the [A] contained in a [callE A B]. *)
+Definition unCall {A B T} (e : callE A B T) : A :=
+  match e with
+  | Call a => a
+  end.
+
+(** Lift a function on [A] to a morphism on [callE]. *)
+Definition calling {A B} {F : Type -> Type}
+           (f : A -> F B) : callE A B ~> F :=
+  fun _ e =>
+    match e with
+    | Call a => f a
+    end.
+
+(* TODO: This is identical to [callWith] but [rec] finds a universe
+   inconsistency with [calling], and not with [calling'].
+   The inconsistency now pops up later (currently in [Events.Env]) *)
+Definition calling' {X Y} {F B : Type -> Type}
+           (f : X -> ctree F B Y) : callE X Y ~> ctree F B :=
+  fun _ e =>
+    match e with
+    | Call a => f a
+    end.
+
+(* Interpret a single recursive definition. *)
+Definition rec {E B : Type -> Type} {X Y : Type}
+           (body : X -> ctree (callE X Y +' E) B Y) :
+  X -> ctree E B Y :=
+  fun a => mrec (calling' body) (Call a).
+
+(** An easy way to construct an event suitable for use with [rec].
+    [call] is an event representing the recursive call.  Since in general, the
+    function might have other events of type [E], the resulting itree has
+    type [(callE A B +' E)].
+*)
+Definition call {E B X Y} (x:X) : ctree (callE X Y +' E) B Y :=
+  CTree.trigger (inl1 (Call x)).
+
+(* (** Here's some syntactic sugar with a notation [mrec-fix]. *) *)
+
+(* Definition rec_fix {E : Type -> Type} {A B : Type} *)
+(*            (body : endo (A -> itree (callE A B +' E) B)) *)
+(*   : A -> itree E B *)
+(*   := rec (body call). *)
+
+(* Notation "'rec-fix' f a := g" := (rec_fix (fun f a => g)) *)
+(*   (at level 200, f ident, a pattern). *)
+(* No idea what a good level would be. *)