ITree.Interp.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 : Type → Type}
(ctx : D ~> itree (D +' E)) : itree (D +' E) ~> itree E :=
fun R ⇒
ITree.iter (fun t : itree (D +' E) R ⇒
match observe t with
| RetF r ⇒ Ret (inr r)
| TauF 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)))
end).
Arguments interp_mrec {D E} & ctx [T].
(ctx : D ~> itree (D +' E)) : itree (D +' E) ~> itree E :=
fun R ⇒
ITree.iter (fun t : itree (D +' E) R ⇒
match observe t with
| RetF r ⇒ Ret (inr r)
| TauF 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)))
end).
Arguments interp_mrec {D E} & ctx [T].
Unfold a mutually recursive definition into separate trees,
resolving the mutual references.
Definition mrec {D E : Type → Type}
(ctx : D ~> itree (D +' E)) : D ~> itree E :=
fun R d ⇒ interp_mrec ctx (ctx _ d).
Arguments mrec {D E} & ctx [T].
(ctx : D ~> itree (D +' E)) : D ~> itree E :=
fun R d ⇒ interp_mrec ctx (ctx _ d).
Arguments mrec {D E} & ctx [T].
Make a recursive call in the handler argument of mrec.
Definition trigger_inl1 {D E : Type → Type} : D ~> itree (D +' E)
:= fun _ d ⇒ ITree.trigger (inl1 d).
Arguments trigger_inl1 {D E} [T].
:= fun _ d ⇒ ITree.trigger (inl1 d).
Arguments trigger_inl1 {D E} [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).
Arguments mrec_fix {D E} &.
Notation "'mrec-fix' f d := g" :=
(let D := _ in
mrec_fix (D := D) (fun (f : ∀ T, D T → _) T (d : D T) ⇒ g))
(at level 200, f name, d pattern).
(* No idea what a good level would be. *)
Definition mrec_fix {D E : Type → Type}
(ctx : endo (D ~> itree (D +' E)))
: D ~> itree E
:= mrec (ctx trigger_inl1).
Arguments mrec_fix {D E} &.
Notation "'mrec-fix' f d := g" :=
(let D := _ in
mrec_fix (D := D) (fun (f : ∀ T, D T → _) T (d : D T) ⇒ g))
(at level 200, f name, d pattern).
(* No idea what a good level would be. *)
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' {A B} {F : Type → Type}
(f : A → itree F B) : callE A B ~> itree F :=
fun _ e ⇒
match e with
| Call a ⇒ f a
end.
(* Interpret a single recursive definition. *)
Definition rec {E : Type → Type} {A B : Type}
(body : A → itree (callE A B +' E) B) :
A → itree E B :=
fun a ⇒ mrec (calling' body) (Call a).
Arguments rec {E A B} &.
(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' {A B} {F : Type → Type}
(f : A → itree F B) : callE A B ~> itree F :=
fun _ e ⇒
match e with
| Call a ⇒ f a
end.
(* Interpret a single recursive definition. *)
Definition rec {E : Type → Type} {A B : Type}
(body : A → itree (callE A B +' E) B) :
A → itree E B :=
fun a ⇒ mrec (calling' body) (Call a).
Arguments rec {E A B} &.
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).
Here's some syntactic sugar with a notation mrec-fix.