Library MetaRocq.Template.TemplateMonad.Common

From MetaRocq.Utils Require Import utils.
From MetaRocq.Template Require Import Ast.

Local Set Universe Polymorphism.

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

Monomorphic Variant hint_locality : Set :=
  local | export | global.

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

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)
; tmLocateModule : qualid → TemplateMonad (list modpath)
; tmLocateModType : qualid → TemplateMonad (list modpath)
; 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 : hint_locality → global_reference → TemplateMonad unit
}.

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

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