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
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.