Add general tmFixpoint combinator to the template monad

This is a hack, presumably there's a better way to do this?
MetaCoq · Nov 21, 2022 · 5a9ede6 · 5a9ede6
1 parent 075e6a7
commit 5a9ede6
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 0 deletions.
diff --git a/template-coq/theories/TemplateMonad/Common.v b/template-coq/theories/TemplateMonad/Common.v
@@ -52,3 +52,10 @@ Monomorphic Variant import_status : Set :=
 Monomorphic Variant locality :=
 | Discharge
 | Global (_ : import_status).
+
+(** XXX FIXME THIS IS A HACK *)
+Local Unset Guard Checking.
+Definition tmFix (TM : TMInstance) {A B} (f : (A -> TemplateMonad TM B) -> (A -> TemplateMonad TM B)) : A -> TemplateMonad TM B
+  := (fix tmFix (dummy : unit) {struct dummy} : A -> @TemplateMonad TM B
+      := f (fun a => tmFix tt a)) tt.
+Local Set Guard Checking.
diff --git a/template-coq/theories/TemplateMonad/Core.v b/template-coq/theories/TemplateMonad/Core.v
@@ -133,3 +133,6 @@ Definition TypeInstance : Common.TMInstance :=
    ; Common.tmMkInductive:=@tmMkInductive
    ; Common.tmExistingInstance:=@tmExistingInstance
    |}.
+
+Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
+  := @tmFix TypeInstance A B f.
diff --git a/template-coq/theories/TemplateMonad/Extractable.v b/template-coq/theories/TemplateMonad/Extractable.v
@@ -108,3 +108,6 @@ Definition tmDefinitionRed (opaque : bool) (i : ident) (rd : reductionStrategy)
 Definition tmInferInstanceRed (rd : reductionStrategy) (type : Ast.term)
   : TM (option Ast.term) :=
   tmBind (tmEval rd type) (fun type => tmInferInstance type).
+
+Definition tmFix {A B} (f : (A -> TM B) -> (A -> TM B)) : A -> TM B
+  := @tmFix TypeInstance A B f.