Library MetaCoq.Template.TemplateMonad.Common

From MetaCoq.Template Require Import utils Ast.

Local Set Universe Polymorphism.

Reduction strategy to apply, beware cbv, cbn and lazy are strong.

Monomorphic Variant reductionStrategy : Set :=
  cbv | cbn | hnf | all | lazy | unfold (i : kername).

Record typed_term : Type := existT_typed_term
{ my_projT1 : Type
; my_projT2 : my_projT1
}.

Monomorphic Inductive option_instance (A : Type) : Type := my_Some : A option_instance A | my_None : option_instance A.

Arguments Some {A} a.
Arguments None {A}.

Record TMInstance@{t u r} :=
{ TemplateMonad : Type@{t} Type@{r}
; tmReturn : {A:Type@{t}}, A TemplateMonad A
; tmBind : {A B : Type@{t}}, TemplateMonad A (A TemplateMonad B)
                                    TemplateMonad B


; tmFail : {A:Type@{t}}, string TemplateMonad A


; tmFreshName : ident TemplateMonad ident

; tmLocate : qualid TemplateMonad (list global_reference)
; tmCurrentModPath : unit TemplateMonad modpath


; tmQuoteInductive : kername TemplateMonad mutual_inductive_body
; tmQuoteUniverses : TemplateMonad ConstraintSet.t
; tmQuoteConstant : kername bool TemplateMonad constant_body


; tmMkInductive : bool mutual_inductive_entry TemplateMonad unit

; tmExistingInstance : global_reference TemplateMonad unit
}.

Monomorphic Variant import_status : Set :=
| ImportDefaultBehavior
| ImportNeedQualified.

Monomorphic Variant locality :=
| Discharge
| Global (_ : import_status).