Skip to content

Commit

Permalink
Add a kludgy implementation of tmTry
Browse files Browse the repository at this point in the history
Partial work towards MetaCoq#874.  Does not support `tmDefinition`, `tmAxiom`,
etc.
  • Loading branch information
JasonGross committed Apr 2, 2023
1 parent 9608862 commit e7aabf3
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 0 deletions.
2 changes: 2 additions & 0 deletions template-coq/theories/Loader.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
7 changes: 7 additions & 0 deletions template-coq/theories/TemplateMonad/Common.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions template-coq/theories/TemplateMonad/Core.v
Original file line number Diff line number Diff line change
Expand Up @@ -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).
43 changes: 43 additions & 0 deletions test-suite/tmTry.v
Original file line number Diff line number Diff line change
@@ -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).

0 comments on commit e7aabf3

Please sign in to comment.