From MetaCoq.Utils Require Import utils MCList.
From MetaCoq.Template Require Import MonadBasicAst MonadAst TemplateMonad Ast Loader.
Require Import Equations.Prop.Classes.
Require Import Coq.Lists.List.
Import ListNotations.

Local Set Primitive Projections.
Local Open Scope bs.
Import MCMonadNotation.

Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
Class ground_quotable T := quote_ground : forall t : T, quotation_of t.
Class inductive_quotation_of {T} (t : T)
  := { qinductive : inductive
     ; qinst : Instance.t
     ; qquotation : quotation_of t := tInd qinductive qinst }.

Require Import MSetPositive.
Definition tmMakeQuotationOfModule (m : qualid) : TemplateMonad _
  := cs <- tmQuoteModule m;;
     let dummy_inst := [] (* XXX FIXME cf https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/global_reference.20-.3E.20term.20in.20the.20template.20monad/near/327682609 *) in
     ps <- monad_map
             (fun r
              => match r with
                 | ConstRef ((mp, name) as c)
                   => let c := tConst c dummy_inst in
                      '{| my_projT2 := cv |} <- tmUnquote c;;
                      let ty := quotation_of cv in
                      n <- @tmDefinition ("q" ++ name) ty c;;
                      tmReturn (Some (existT (fun T => T) ty n))
                 | IndRef ind
                   => let '(mp, name) := ind.(inductive_mind) in
                      let inst := dummy_inst in
                      let c := tInd ind inst in
                      '{| my_projT2 := cv |} <- tmUnquote c;;
                      let ty := inductive_quotation_of cv in
                      let v : ty := {| qinductive := ind ; qinst := inst |} in
                      n <- @tmDefinition ("q" ++ name) ty v;;
                      tmReturn (Some (existT (fun T => T) ty n))
                 | ConstructRef _ _ | VarRef _ => tmReturn None
                 end)
             cs;;
     tmReturn ps.
MetaCoq Run (tmMakeQuotationOfModule "Coq.MSets.MSetPositive.PositiveSet"%bs).
(* Error: Illegal application:
The term "@quotation_of" of type "forall T : Type, T -> Type"
cannot be applied to the terms
 "Type" : "Type"
 "PositiveSet.elt" : "Type"
The 1st term has type "Type@{MetaCoq.Quotation.ToTemplate.test.86+1}"
which should be coercible to "Type@{quotation_of.u0}".
*)