From d0bea38e9559c25c7dcd2fa5bc7b4beaeb1e5f33 Mon Sep 17 00:00:00 2001
From: Ben Nott <0xdrfff@gmail.com>
Date: Fri, 28 Jun 2024 14:39:14 +1000
Subject: [PATCH] Adds mrec and interp combinators

---
 src/coalgebras/itreeTauScript.sml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/src/coalgebras/itreeTauScript.sml b/src/coalgebras/itreeTauScript.sml
index c744db5841..0687681c6e 100644
--- a/src/coalgebras/itreeTauScript.sml
+++ b/src/coalgebras/itreeTauScript.sml
@@ -740,6 +740,30 @@ Definition itree_loop_def:
                      (INR seed)
 End
 
+Definition interp_body_def:
+  interp_body rh (Ret r) = Ret (INR r) ∧
+  interp_body rh (Tau t) = Ret (INL t) ∧
+  interp_body rh (Vis e k) = itree_bind (rh e) (\a. Ret (INL (k a)))
+End
+
+Definition itree_interp_def:
+  itree_interp rh t = itree_iter (interp_body rh) t
+End
+
+Definition mrec_iter_body_def:
+  mrec_iter_body rh t =
+  case t of
+   | Ret r => Ret (INR r)
+   | Tau t => Ret (INL t)
+   | Vis (INL seed') k => Ret (INL (itree_bind (rh seed') k))
+   | Vis (INR e) k => Vis e (Ret o INL o k)
+End
+
+Definition itree_mrec_def:
+  itree_mrec rh seed =
+  itree_iter (mrec_iter_body rh) (rh seed)
+End
+
 (* weak termination-sensitive bisimulation *)
 
 Inductive strip_tau: