Library MetaCoq.Template.TemplateMonad.Core

From MetaCoq.Template Require Import utils Ast AstUtils Common.

Local Set Universe Polymorphism.
Import MCMonadNotation.

The Template Monad

A monad for programming with Template Coq structures. Use Run TemplateProgram on a monad action to produce its side-effects.

Uses a reduction strategy specifier reductionStrategy.

The TemplateMonad type

Cumulative Inductive TemplateMonad@{t u} : Type@{t} → Prop :=

| tmReturn : ∀ {A:Type@{t}}, A → TemplateMonad A
| tmBind : ∀ {A B : Type@{t}}, TemplateMonad A → (A → TemplateMonad B )
→ TemplateMonad B

| tmPrint : ∀ {A:Type@{t}}, A → TemplateMonad unit
| tmMsg : string → TemplateMonad unit
| tmFail : ∀ {A:Type@{t}}, string → TemplateMonad A
| tmEval : reductionStrategy → ∀ {A:Type@{t}}, A → TemplateMonad A

| tmLemma : ident → ∀ A : Type@{t}, TemplateMonad A
| tmDefinitionRed_ : ∀ (opaque : bool), ident → option reductionStrategy → ∀ {A:Type@{t}}, A → TemplateMonad A
| tmAxiomRed : ident → option reductionStrategy → ∀ A : Type@{t}, TemplateMonad A
| tmVariable : ident → Type@{t} → TemplateMonad unit

| tmFreshName : ident → TemplateMonad ident

| tmLocate : qualid → TemplateMonad (list global_reference)
| tmCurrentModPath : unit → TemplateMonad modpath

| tmQuote : ∀ {A:Type@{t}}, A → TemplateMonad Ast.term

| tmQuoteRecTransp : ∀ {A:Type@{t}}, A → bool → TemplateMonad program

| tmQuoteInductive : kername → TemplateMonad mutual_inductive_body
| tmQuoteUniverses : TemplateMonad ConstraintSet.t
| tmQuoteConstant : kername → bool → TemplateMonad constant_body
| tmQuoteModule : qualid → TemplateMonad (list global_reference)

| tmMkInductive : bool → mutual_inductive_entry → TemplateMonad unit
| tmUnquote : Ast.term → TemplateMonad typed_term@{u }
| tmUnquoteTyped : ∀ A : Type@{t}, Ast.term → TemplateMonad A

| tmExistingInstance : global_reference → TemplateMonad unit
| tmInferInstance : option reductionStrategy → ∀ A : Type@{t}, TemplateMonad (option_instance A)
.

This allow to use notations of MonadNotation

Global Instance TemplateMonad_Monad@{t u} : Monad@{t u } TemplateMonad@{t u } :=
  {| ret := @tmReturn ; bind := @tmBind |}.

Polymorphic Definition tmDefinitionRed
: ident → option reductionStrategy → ∀ {A:Type}, A → TemplateMonad A :=
  @tmDefinitionRed_ false.
Polymorphic Definition tmOpaqueDefinitionRed
: ident → option reductionStrategy → ∀ {A:Type}, A → TemplateMonad A :=
  @tmDefinitionRed_ true.

Definition print_nf {A} (msg : A) : TemplateMonad unit
  := tmEval all msg >>= tmPrint.

Definition fail_nf {A} (msg : string) : TemplateMonad A
  := tmEval all msg >>= tmFail.

Definition tmMkInductive' (mind : mutual_inductive_body) : TemplateMonad unit
  := tmMkInductive false (mind_body_to_entry mind).

Definition tmAxiom id := tmAxiomRed id None.
Definition tmDefinition id {A} t := @tmDefinitionRed_ false id None A t.

We keep the original behaviour of tmQuoteRec: it quotes all the dependencies regardless of the opaqueness settings

Definition tmQuoteRec {A} (a : A) := tmQuoteRecTransp a true.

Definition tmLocate1 (q : qualid) : TemplateMonad global_reference :=
  l <- tmLocate q ;;
  match l with
  | [] ⇒ tmFail ("Constant [" ^ q ^ "] not found")
  | x :: _ ⇒ tmReturn x
  end.

Don't remove. Constants used in the implem of the plugin

Definition tmTestQuote {A} (t : A) := tmQuote t >>= tmPrint.

Definition Common_kn (s : ident) :=
  (MPfile ["Common"; "TemplateMonad"; "Template"; "MetaCoq"], s ).
Definition tmTestUnquote (t : term) :=
     t' <- tmUnquote t ;;
     t'' <- tmEval (unfold (Common_kn "my_projT2")) (my_projT2 t') ;;
     tmPrint t''.

Definition tmQuoteDefinition id {A} (t : A) := tmQuote t >>= tmDefinition id.
Definition tmQuoteDefinitionRed id rd {A} (t : A)
  := tmEval rd t >>= tmQuoteDefinition id.
Definition tmQuoteRecDefinition id {A} (t : A)
  := tmQuoteRec t >>= tmDefinition id.

Definition tmMkDefinition (id : ident) (tm : term) : TemplateMonad unit
  := t' <- tmUnquote tm ;;
     t'' <- tmEval (unfold (Common_kn "my_projT2")) (my_projT2 t') ;;
     tmDefinitionRed id (Some (unfold (Common_kn "my_projT1"))) t'' ;;
     tmReturn tt.