From e7aabf3c7289c0d0d6d16bfdfa5a6b7228dacdc8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 27 Mar 2023 10:05:25 -0700
Subject: [PATCH] Add a kludgy implementation of `tmTry`

Partial work towards #874.  Does not support `tmDefinition`, `tmAxiom`,
etc.
---
 template-coq/theories/Loader.v               |  2 +
 template-coq/theories/TemplateMonad/Common.v |  7 ++++
 template-coq/theories/TemplateMonad/Core.v   |  8 ++++
 test-suite/tmTry.v                           | 43 ++++++++++++++++++++
 4 files changed, 60 insertions(+)
 create mode 100644 test-suite/tmTry.v

diff --git a/template-coq/theories/Loader.v b/template-coq/theories/Loader.v
index 9a7b1e1ede..07d2b9c3ed 100644
--- a/template-coq/theories/Loader.v
+++ b/template-coq/theories/Loader.v
@@ -12,3 +12,5 @@ Notation "<% x %>" := (ltac:(let p y := exact y in quote_term x p))
 (* Use [return _] to avoid running the program twice on failure *)
 Notation "<# x #>" := (match TemplateMonad.Core.tmQuoteRec x return _ with qx => ltac:(let p y := exact y in run_template_program qx p) end)
   (only parsing).
+
+#[global] Hint Extern 0 (Core.tmTryHelper ?run) => run_template_program run (fun v => refine v) : typeclass_instances.
diff --git a/template-coq/theories/TemplateMonad/Common.v b/template-coq/theories/TemplateMonad/Common.v
index 9c5b553260..048a197f9e 100644
--- a/template-coq/theories/TemplateMonad/Common.v
+++ b/template-coq/theories/TemplateMonad/Common.v
@@ -23,6 +23,13 @@ Monomorphic Inductive option_instance (A : Type) : Type := my_Some : A -> option
 Arguments Some {A} a.
 Arguments None {A}.
 
+Monomorphic Variant exn : Set := GenericError.
+
+Variant option_try (A : Type) : Type := my_Value (val : A) | my_Error (err : exn).
+
+Arguments my_Value {A} val.
+Arguments my_Error {A} _.
+
 Record TMInstance@{t u r} :=
 { TemplateMonad : Type@{t} -> Type@{r}
 ; tmReturn : forall {A:Type@{t}}, A -> TemplateMonad A
diff --git a/template-coq/theories/TemplateMonad/Core.v b/template-coq/theories/TemplateMonad/Core.v
index 7e67367142..a463141c33 100644
--- a/template-coq/theories/TemplateMonad/Core.v
+++ b/template-coq/theories/TemplateMonad/Core.v
@@ -181,3 +181,11 @@ Definition tmFix@{a b t u} {A : Type@{a}} {B : Type@{b}} (f : (A -> TemplateMona
             qu <- tmQuoteLevel@{u _ _};;
             let self := tConst (MPfile ["Core"; "TemplateMonad"; "Template"; "MetaCoq"], "tmFix'")%bs [qa;qb;qt;qu] in
             @tmFix'@{a b t u} A B (mkApps self [qA; qB]) f a)).
+
+Class tmTryHelper@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) := tmTry_ret : A.
+Definition tmTry@{t u} {A : Type@{t}} (run : TemplateMonad@{t u} A) : TemplateMonad@{t u} (option_try@{t} A)
+  := tmBind (tmInferInstance None (tmTryHelper run))
+            (fun inst => match inst with
+                         | my_Some x => tmReturn (my_Value x)
+                         | my_None => tmReturn (my_Error GenericError)
+                         end).
diff --git a/test-suite/tmTry.v b/test-suite/tmTry.v
new file mode 100644
index 0000000000..66792515b8
--- /dev/null
+++ b/test-suite/tmTry.v
@@ -0,0 +1,43 @@
+From MetaCoq.Template Require Import All.
+
+Import MCMonadNotation.
+Import bytestring.
+Open Scope bs.
+Open Scope list_scope.
+
+Universes u0 u1.
+Constraint u0 < u1.
+MetaCoq Run (u <- tmQuote Type@{u0};;
+             v <- tmTry (tmUnquoteTyped Type@{u0} u);;
+             match v with
+             | my_Value v => tmPrint (v -> True);; tmFail "first should not succeed"
+             | my_Error _ => v' <- tmUnquoteTyped Type@{u1} u;;
+                             ret (v' -> False)
+             end >>= tmPrint).
+
+(*MetaCoq Run (tmDefinition "a" I;; tmTry (tmDefinition "a" I) >>= tmPrint).*)
+(*a is defined
+
+Error: Anomaly "in Univ.repr: Universe MetaCoq.TestSuite.tmTry.101 undefined." Please report at http://coq.inria.fr/bugs/.*)
+(*MetaCoq Run (tmTry (tmDefinition "b" I);; mp <- tmCurrentModPath tt;; tmUnquote (tConst (mp, "b") []) >>= tmPrint).*)
+(*Error: Anomaly "Constant MetaCoq.TestSuite.tmTry.b does not appear in the environment."
+Please report at http://coq.inria.fr/bugs/.*)
+(*MetaCoq Run (tmDefinition "c" I;; mp <- tmCurrentModPath tt;;
+             v <- tmTry (tmUnquoteTyped False (tConst (mp, "c") []));;
+             match v with
+             | my_Value v => ret (inl v)
+             | my_Error _ => v' <- tmUnquoteTyped True (tConst (mp, "c") []);;
+                             ret (inr v')
+             end >>= tmPrint).*)
+(*Error: Anomaly "in Univ.repr: Universe MetaCoq.TestSuite.tmTry.172 undefined." Please report at http://coq.inria.fr/bugs/.*)
+MetaCoq Run (tmAxiom "a'" True;; tmTry (tmAxiom "a'" True) >>= tmPrint).
+(*MetaCoq Run (tmTry (tmAxiom "b'" True);; mp <- tmCurrentModPath tt;; tmUnquote (tConst (mp, "b'") []) >>= tmPrint).*)
+(*Error: Anomaly "Constant MetaCoq.TestSuite.tmTry.b' does not appear in the environment."
+Please report at http://coq.inria.fr/bugs/.*)
+MetaCoq Run (tmAxiom "c'" True;; mp <- tmCurrentModPath tt;;
+             v <- tmTry (tmUnquoteTyped False (tConst (mp, "c'") []));;
+             match v with
+             | my_Value v => tmPrint v;; tmFail "too early"
+             | my_Error _ => v' <- tmUnquoteTyped True (tConst (mp, "c'") []);;
+                             ret v'
+             end >>= tmPrint).