From 287b32603ebc8f0cb11ae13ecc3fcf71078e7837 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2023 08:57:11 -0700 Subject: [PATCH] Fix `tmOptimizedBind` to avoid quadratic blowup Oops. Maybe now we can actually use it by default. --- template-coq/theories/TemplateMonad/Core.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/template-coq/theories/TemplateMonad/Core.v b/template-coq/theories/TemplateMonad/Core.v index f32d7c66c..f06d419a8 100644 --- a/template-coq/theories/TemplateMonad/Core.v +++ b/template-coq/theories/TemplateMonad/Core.v @@ -70,17 +70,25 @@ Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop := . (** This version of [tmBind] flattens nesting structure; using it in deeply recursive template programs can speed things up drastically *) +(** We use [tmBind] in the recursive position to avoid quadratic blowup in the number of [tmOptimizedBind]s *) Fixpoint tmOptimizedBind@{t u} {A B : Type@{t}} (v : TemplateMonad@{t u} A) : (A -> TemplateMonad@{t u} B) -> TemplateMonad@{t u} B := match v with | tmReturn x => fun f => f x - | tmBind v k => fun f => tmOptimizedBind v (fun v => tmOptimizedBind (k v) f) + | tmBind v k => fun f => tmOptimizedBind v (fun v => tmBind (k v) f) | tmFail msg => fun _ => tmFail msg | v => tmBind v end. (** Flatten nested [tmBind] *) +Fixpoint tmOptimize'@{t u} {A B : Type@{t}} (v : TemplateMonad@{t u} A) : (A -> TemplateMonad@{t u} B) -> TemplateMonad@{t u} B + := match v with + | tmReturn x => fun f => f x + | tmBind v k => fun f => tmOptimize' v (fun v => tmOptimize' (k v) f) + | tmFail msg => fun _ => tmFail msg + | v => tmBind v + end. Definition tmOptimize@{t u} {A : Type@{t}} (v : TemplateMonad@{t u} A) : TemplateMonad@{t u} A - := tmOptimizedBind v tmReturn. + := tmOptimize' v tmReturn. (** This allow to use notations of MonadNotation *) Definition TemplateMonad_UnoptimizedMonad@{t u} : Monad@{t u} TemplateMonad@{t u} :=