Add PCUIC versions of the template monad

This will allow easier creation of developments that reason about
doubly-quoted terms and judgments.

pcuic/_CoqProject.in

@@ -91,6 +91,7 @@ theories/PCUICSafeLemmata.v
 theories/PCUICEtaExpand.v
 
 theories/PCUICProgram.v
+theories/TemplateMonadToPCUIC.v
 theories/TemplateToPCUIC.v
 theories/TemplateToPCUICCorrectness.v
 theories/TemplateToPCUICWcbvEval.v
@@ -101,6 +102,13 @@ theories/PCUICExpandLets.v
 theories/PCUICExpandLetsCorrectness.v
 theories/PCUICTransform.v
 
+# The Template monad
+theories/Loader.v
+theories/PCUICTemplateMonad.v
+theories/PCUICTemplateMonad/Common.v
+theories/PCUICTemplateMonad/Core.v
+theories/PCUICTemplateMonad/Extractable.v
+
 theories/Bidirectional/BDTyping.v
 theories/Bidirectional/BDToPCUIC.v
 theories/Bidirectional/BDFromPCUIC.v

pcuic/theories/Loader.v

@@ -0,0 +1,7 @@
+(* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require Import Loader.
+From MetaCoq.PCUIC.PCUICTemplateMonad Require Core.
+From MetaCoq.PCUIC Require Import TemplateMonadToPCUIC.
+
+Notation "<% x %>" := (ltac:(let p y := exact y in let p y := run_template_program (@monad_trans Core.TypeInstance Core.TemplateMonad_Monad y) p in quote_term x p))
+  (only parsing).

pcuic/theories/PCUICTemplateMonad.v

@@ -0,0 +1,3 @@
+(* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require Export TemplateMonad.
+From MetaCoq.PCUIC.PCUICTemplateMonad Require Export Common Core.

pcuic/theories/PCUICTemplateMonad/Common.v

@@ -0,0 +1,21 @@
+(* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require Import utils Ast.
+From MetaCoq.Template.TemplateMonad Require Export Common.
+From MetaCoq.PCUIC Require Import PCUICAst TemplateMonadToPCUIC TemplateToPCUIC PCUICToTemplate.
+
+Local Set Universe Polymorphism.
+Import MCMonadNotation.
+
+Section with_tc.
+  Context {TM : TMInstance}.
+  Local Notation TemplateMonad := (@TemplateMonad TM).
+  Context {M : Monad TemplateMonad}.
+
+  Definition tmQuoteInductive (kn : kername) : TemplateMonad mutual_inductive_body := tmQuoteInductive kn.
+  Definition tmQuoteConstant (kn : kername) (bypass_opacity : bool) : TemplateMonad constant_body :=
+    cb <- tmQuoteConstant TM kn bypass_opacity;; monad_trans_constant_body cb.
+  (*
+Definition tmMkInductive (b : bool) (mie : mutual_inductive_entry) : TemplateMonad unit
+  := tmMkInductive b (PCUICToTemplate.trans_mutual_inductive_entry mie).
+   *)
+End with_tc.

pcuic/theories/PCUICTemplateMonad/Core.v

@@ -0,0 +1,27 @@
+(* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require Import utils Ast AstUtils Common.
+From MetaCoq.Template.TemplateMonad Require Export Core.
+From MetaCoq.PCUIC Require Import PCUICAst TemplateMonadToPCUIC TemplateToPCUIC PCUICToTemplate.
+
+Local Set Universe Polymorphism.
+Import MCMonadNotation.
+
+Local Notation monad_trans := (@monad_trans TypeInstance _).
+
+Definition tmQuote {A:Type} (a : A) : TemplateMonad PCUICAst.term := (qa <- tmQuote a;; monad_trans qa).
+Definition tmQuoteRecTransp {A:Type} (a : A) (bypass_opacity : bool) : TemplateMonad PCUICProgram.pcuic_program :=
+  (p <- tmQuoteRecTransp a bypass_opacity;; ret (trans_template_program p)).
+Definition tmQuoteInductive (kn : kername) : TemplateMonad mutual_inductive_body := tmQuoteInductive (TM:=TypeInstance) kn.
+Definition tmQuoteConstant (kn : kername) (bypass_opacity : bool) : TemplateMonad constant_body :=
+  cb <- tmQuoteConstant kn bypass_opacity;; monad_trans_constant_body (TM:=TypeInstance) cb.
+(*
+Definition tmMkInductive (b : bool) (mie : mutual_inductive_entry) : TemplateMonad unit
+  := tmMkInductive b (PCUICToTemplate.trans_mutual_inductive_entry mie).
+ *)
+Definition tmUnquote (t : PCUICAst.term) : TemplateMonad typed_term := tmUnquote (PCUICToTemplate.trans t).
+Definition tmUnquoteTyped A (t : PCUICAst.term) : TemplateMonad A := tmUnquoteTyped A (PCUICToTemplate.trans 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 tmMkDefinition (id : ident) (tm : PCUICAst.term) : TemplateMonad unit := tmMkDefinition id (PCUICToTemplate.trans tm).

pcuic/theories/PCUICToTemplate.v

@@ -111,3 +111,31 @@ Definition trans_global_env (d : PCUICEnvironment.global_env) : global_env :=
 
 Definition trans_global (Σ : PCUICEnvironment.global_env_ext) : global_env_ext :=
   (trans_global_env (fst Σ), snd Σ).
+
+Definition trans_one_inductive_entry (oie : PCUICAst.one_inductive_entry) : one_inductive_entry
+  := {| mind_entry_typename := oie.(PCUICAst.mind_entry_typename);
+       mind_entry_arity := trans oie.(PCUICAst.mind_entry_arity);
+       mind_entry_consnames := oie.(PCUICAst.mind_entry_consnames);
+       mind_entry_lc := List.map trans oie.(PCUICAst.mind_entry_lc); |}.
+
+(*
+(* It would be nice to have this, but it seems to not be possible *)
+Definition trans_mutual_inductive_entry (mie : PCUICAst.mutual_inductive_entry) : mutual_inductive_entry.
+  refine {| mind_entry_record := mie.(PCUICAst.mind_entry_record);
+           mind_entry_finite := mie.(PCUICAst.mind_entry_finite);
+           mind_entry_private := mie.(PCUICAst.mind_entry_private);
+           mind_entry_universes := universes_entry_of_decl mie.(PCUICAst.mind_entry_universes);
+           mind_entry_inds := List.map trans_one_inductive_entry mie.(PCUICAst.mind_entry_inds);
+           mind_entry_params := trans_local
+                                  (* TODO Should this be extracted? *)
+                                  (List.map (fun '(id, le)
+                                             => let dname := {| binder_name := nNamed id ; binder_relevance := _ (* ??? *) |} in
+                                                match le with
+                                                | LocalDef x => {| decl_name := dname ; decl_type := _ (* ??? *) ; decl_body := Some x |}
+                                                | LocalAssum x => {| decl_name := dname ; decl_type := x ; decl_body := None |}
+                                                end)
+                                            mie.(PCUICAst.mind_entry_params));
+           mind_entry_variance := _ (* ??? *);
+           mind_entry_template := false |}.
+Abort.
+*)

pcuic/theories/TemplateMonadToPCUIC.v

@@ -0,0 +1,153 @@
+(* Distributed under the terms of the MIT license. *)
+From Coq Require Import Uint63 FloatOps FloatAxioms.
+From MetaCoq.Template Require Import config utils AstUtils MonadAst MonadBasicAst Primitive EnvMap.
+From MetaCoq.Template Require TemplateProgram.
+From MetaCoq.Template Require Import TemplateMonad.Common monad_utils.
+From MetaCoq.PCUIC Require Import PCUICAst PCUICPrimitive PCUICCases PCUICProgram TemplateToPCUIC.
+
+Import MCMonadNotation.
+
+(** XXX FIXME THIS IS A HACK *)
+Local Unset Guard Checking.
+Fixpoint tmFix' {TM : TMInstance} {A B} (f : (A -> @TemplateMonad TM B) -> (A -> @TemplateMonad TM B)) (dummy : unit) {struct dummy} : A -> @TemplateMonad TM B
+  := f (fun a => tmFix' f tt a).
+Local Set Guard Checking.
+
+Section with_tc.
+  Context {TM : TMInstance}.
+  Local Notation TemplateMonad := (@TemplateMonad TM).
+  Context {M : Monad TemplateMonad}.
+
+  Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
+    := tmFix' f tt.
+
+  Section helpers.
+    Context (monad_trans : Ast.term -> TemplateMonad term).
+
+    Definition monad_trans_decl' (d : Ast.Env.context_decl) :=
+      decl_body <- monad_option_map monad_trans d.(decl_body);;
+      decl_type <- monad_trans d.(decl_type);;
+      ret {| decl_name := d.(decl_name);
+            decl_body := decl_body;
+            decl_type := decl_type |}.
+
+    Definition monad_trans_local' Γ := monad_map monad_trans_decl' Γ.
+
+    Definition monad_trans_constructor_body' (d : Ast.Env.constructor_body) :=
+      cstr_args <- monad_trans_local' d.(Ast.Env.cstr_args);;
+      cstr_indices <- monad_map monad_trans d.(Ast.Env.cstr_indices);;
+      cstr_type <- monad_trans d.(Ast.Env.cstr_type);;
+      ret {| cstr_name := d.(Ast.Env.cstr_name);
+            cstr_args := cstr_args;
+            cstr_indices := cstr_indices;
+            cstr_type := cstr_type;
+            cstr_arity := d.(Ast.Env.cstr_arity) |}.
+    Definition monad_trans_projection_body' (d : Ast.Env.projection_body) :=
+      proj_type <- monad_trans d.(Ast.Env.proj_type);;
+      ret {| proj_name := d.(Ast.Env.proj_name);
+            proj_type := proj_type;
+            proj_relevance := d.(Ast.Env.proj_relevance) |}.
+
+    Definition monad_trans_one_ind_body' (d : Ast.Env.one_inductive_body) :=
+      ind_indices <- monad_trans_local' d.(Ast.Env.ind_indices);;
+      ind_type <- monad_trans d.(Ast.Env.ind_type);;
+      ind_ctors <- monad_map monad_trans_constructor_body' d.(Ast.Env.ind_ctors);;
+      ind_projs <- monad_map monad_trans_projection_body' d.(Ast.Env.ind_projs);;
+      ret {| ind_name := d.(Ast.Env.ind_name);
+            ind_relevance := d.(Ast.Env.ind_relevance);
+            ind_indices := ind_indices;
+            ind_sort := d.(Ast.Env.ind_sort);
+            ind_type := ind_type;
+            ind_kelim := d.(Ast.Env.ind_kelim);
+            ind_ctors := ind_ctors;
+            ind_projs := ind_projs |}.
+
+    Definition monad_trans_constant_body' bd :=
+      cst_type <- monad_trans bd.(Ast.Env.cst_type);;
+      cst_body <- monad_option_map monad_trans bd.(Ast.Env.cst_body);;
+      ret {| cst_type := cst_type;
+            cst_body := cst_body;
+            cst_universes := bd.(Ast.Env.cst_universes);
+            cst_relevance := bd.(Ast.Env.cst_relevance) |}.
+
+    Definition monad_trans_minductive_body' md :=
+      ind_params <- monad_trans_local' md.(Ast.Env.ind_params);;
+      ind_bodies <- monad_map monad_trans_one_ind_body' md.(Ast.Env.ind_bodies);;
+      ret {| ind_finite := md.(Ast.Env.ind_finite);
+            ind_npars := md.(Ast.Env.ind_npars);
+            ind_params := ind_params;
+            ind_bodies := ind_bodies;
+            ind_universes := md.(Ast.Env.ind_universes);
+            ind_variance := md.(Ast.Env.ind_variance) |}.
+
+    Definition monad_trans_global_decl' (d : Ast.Env.global_decl) :=
+      match d with
+      | Ast.Env.ConstantDecl bd => bd <- monad_trans_constant_body' bd;; ret (ConstantDecl bd)
+      | Ast.Env.InductiveDecl bd => bd <- monad_trans_minductive_body' bd;; ret (InductiveDecl bd)
+      end.
+
+    Definition tmQuoteInductive' (mind : kername) : TemplateMonad mutual_inductive_body :=
+      bd <- tmQuoteInductive TM mind;;
+      monad_trans_minductive_body' bd.
+
+    Definition TransLookup_lookup_inductive' (ind : inductive) : TemplateMonad (mutual_inductive_body × one_inductive_body) :=
+      mdecl <- tmQuoteInductive' (inductive_mind ind);;
+      match nth_error (ind_bodies mdecl) (inductive_ind ind) with
+      | Some idecl => ret (mdecl, idecl)
+      | None => tmFail TM "TransLookup.lookup_inductive: nth_error: Not_found"
+      end.
+
+  End helpers.
+
+  Section with_helper.
+    Context (TransLookup_lookup_inductive' : inductive -> TemplateMonad (mutual_inductive_body × one_inductive_body)).
+
+    Fixpoint monad_trans' (t : Ast.term) : TemplateMonad term
+      := match t with
+         | Ast.tRel n => ret (tRel n)
+         | Ast.tVar n => ret (tVar n)
+         | Ast.tEvar ev args => args <- monad_map monad_trans' args;; ret (tEvar ev args)
+         | Ast.tSort u => ret (tSort u)
+         | Ast.tConst c u => ret (tConst c u)
+         | Ast.tInd c u => ret (tInd c u)
+         | Ast.tConstruct c k u => ret (tConstruct c k u)
+         | Ast.tLambda na T M => T <- monad_trans' T;; M <- monad_trans' M;; ret (tLambda na T M)
+         | Ast.tApp u v => u <- monad_trans' u;; v <- monad_map monad_trans' v;; ret (mkApps u v)
+         | Ast.tProd na A B => A <- monad_trans' A;; B <- monad_trans' B;; ret (tProd na A B)
+         | Ast.tCast c kind t => t <- monad_trans' t;; c <- monad_trans' c;; ret (tApp (tLambda (mkBindAnn nAnon Relevant) t (tRel 0)) c)
+         | Ast.tLetIn na b t b' => b <- monad_trans' b;; t <- monad_trans' t;; b' <- monad_trans' b';; ret (tLetIn na b t b')
+         | Ast.tCase ci p c brs =>
+             p' <- monad_map_predicate ret monad_trans' monad_trans' p;;
+             brs' <- monad_map (monad_map_branch monad_trans') brs;;
+             '(mdecl, idecl) <- TransLookup_lookup_inductive' ci.(ci_ind);;
+             let tp := trans_predicate ci.(ci_ind) mdecl idecl p'.(Ast.pparams) p'.(Ast.puinst) p'.(Ast.pcontext) p'.(Ast.preturn) in
+             let tbrs :=
+               map2 (fun cdecl br => trans_branch ci.(ci_ind) mdecl cdecl br.(Ast.bcontext) br.(Ast.bbody))
+                    idecl.(ind_ctors) brs' in
+             c <- monad_trans' c;;
+             ret (tCase ci tp c tbrs)
+         | Ast.tProj p c => c <- monad_trans' c;; ret (tProj p c)
+         | Ast.tFix mfix idx =>
+             mfix' <- monad_map (monad_map_def monad_trans' monad_trans') mfix;;
+             ret (tFix mfix' idx)
+         | Ast.tCoFix mfix idx =>
+             mfix' <- monad_map (monad_map_def monad_trans' monad_trans') mfix;;
+             ret (tCoFix mfix' idx)
+         | Ast.tInt n => ret (tPrim (primInt; primIntModel n))
+         | Ast.tFloat n => ret (tPrim (primFloat; primFloatModel n))
+         end.
+  End with_helper.
+
+  Definition monad_trans : (Ast.term -> TemplateMonad term)
+    := tmFix (fun monad_trans => monad_trans' (TransLookup_lookup_inductive' monad_trans)).
+
+  Definition monad_trans_decl := monad_trans_decl' monad_trans.
+  Definition monad_trans_local := monad_trans_local' monad_trans.
+  Definition monad_trans_constructor_body := monad_trans_constructor_body' monad_trans.
+  Definition monad_trans_projection_body := monad_trans_projection_body' monad_trans.
+  Definition monad_trans_one_ind_body := monad_trans_one_ind_body' monad_trans.
+  Definition monad_trans_constant_body := monad_trans_constant_body' monad_trans.
+  Definition monad_trans_minductive_body := monad_trans_minductive_body' monad_trans.
+  Definition monad_trans_global_decl := monad_trans_global_decl' monad_trans.
+  Definition tmQuoteInductive := tmQuoteInductive' monad_trans.
+End with_tc.

template-coq/_CoqProject

@@ -75,6 +75,10 @@ theories/TemplateMonad/Core.v
 theories/TemplateMonad/Extractable.v
 theories/monad_utils.v
 
+# Extra Template monad
+theories/MonadAst.v
+theories/MonadBasicAst.v
+
 # Bindings of Coq terms to the "metacoq.*" names
 theories/Constants.v
 

template-coq/gen-src/cRelationClasses.mli.orig

@@ -14,6 +14,10 @@ type ('a, 'r) coq_Reflexive = 'a -> 'r
 
 val reflexivity : ('a1, 'a2) coq_Reflexive -> 'a1 -> 'a2
 
+type ('a, 'r) complement = __
+
+type ('a, 'r) coq_Irreflexive = ('a, ('a, 'r) complement) coq_Reflexive
+
 type ('a, 'r) coq_Symmetric = 'a -> 'a -> 'r -> 'r
 
 val symmetry : ('a1, 'a2) coq_Symmetric -> 'a1 -> 'a1 -> 'a2 -> 'a2
@@ -33,9 +37,10 @@ val coq_PreOrder_Reflexive :
 val coq_PreOrder_Transitive :
   ('a1, 'a2) coq_PreOrder -> ('a1, 'a2) coq_Transitive
 
-type ('a, 'r) coq_StrictOrder =
-  ('a, 'r) coq_Transitive
-  (* singleton inductive, whose constructor was Build_StrictOrder *)
+type ('a, 'r) coq_StrictOrder = { coq_StrictOrder_Irreflexive : ('a, 'r)
+                                                                coq_Irreflexive;
+                                  coq_StrictOrder_Transitive : ('a, 'r)
+                                                               coq_Transitive }
 
 val coq_StrictOrder_Transitive :
   ('a1, 'a2) coq_StrictOrder -> ('a1, 'a2) coq_Transitive
@@ -104,19 +109,18 @@ val iff_equivalence : (__, __) coq_Equivalence
 
 val arrow_Reflexive_obligation_1 : ('a1, 'a1) arrow
 
-val arrow_Reflexive : ('a1, 'a1) arrow
+val arrow_Reflexive : (__, __) arrow
 
 val arrow_Transitive_obligation_1 :
   ('a1, 'a2) arrow -> ('a2, 'a3) arrow -> ('a1, 'a3) arrow
 
-val arrow_Transitive :
-  ('a1, 'a2) arrow -> ('a2, 'a3) arrow -> ('a1, 'a3) arrow
+val arrow_Transitive : (__, __) arrow -> (__, __) arrow -> (__, __) arrow
 
-val iffT_Reflexive : ('a1, 'a1) iffT
+val iffT_Reflexive : (__, __) iffT
 
-val iffT_Symmetric : ('a1, 'a2) iffT -> ('a2, 'a1) iffT
+val iffT_Symmetric : (__, __) iffT -> (__, __) iffT
 
-val iffT_Transitive : ('a1, 'a2) iffT -> ('a2, 'a3) iffT -> ('a1, 'a3) iffT
+val iffT_Transitive : (__, __) iffT -> (__, __) iffT -> (__, __) iffT
 
 type ('a, 'x0, 'x) relation_equivalence = 'a -> 'a -> ('x0, 'x) iffT
 

template-coq/theories/MonadAst.v

@@ -0,0 +1,58 @@
+(* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require Import utils.
+From MetaCoq.Template Require Import Ast.
+From MetaCoq.Template Require Import TemplateMonad.Common monad_utils.
+
+Import MCMonadNotation.
+
+Section with_tc.
+  Context {TM : TMInstance}.
+  Local Notation TemplateMonad := (@TemplateMonad TM).
+  Context {M : Monad TemplateMonad}.
+
+  Section map_predicate.
+    Context {term term' : Type}.
+    Context (uf : Instance.t -> TemplateMonad Instance.t).
+    Context (paramf preturnf : term -> TemplateMonad term').
+
+    Definition monad_map_predicate (p : predicate term) :=
+      pparams <- monad_map paramf p.(pparams);;
+      puinst <- uf p.(puinst);;
+      preturn <- preturnf p.(preturn);;
+      ret {| pparams := pparams;
+            puinst := puinst;
+            pcontext := p.(pcontext);
+            preturn := preturn |}.
+  End map_predicate.
+
+  Section map_predicate_k.
+    Context {term : Type}.
+    Context (uf : Instance.t -> TemplateMonad Instance.t).
+    Context (f : nat -> term -> TemplateMonad term).
+
+    Definition monad_map_predicate_k k (p : predicate term) :=
+      pparams <- monad_map (f k) p.(pparams);;
+      puinst <- uf p.(puinst);;
+      preturn <- f (#|p.(pcontext)| + k) p.(preturn);;
+      ret {| pparams := pparams;
+            puinst := puinst;
+            pcontext := p.(pcontext);
+            preturn := preturn |}.
+
+  End map_predicate_k.
+
+  Section map_branch.
+    Context {term term' : Type}.
+    Context (bbodyf : term -> TemplateMonad term').
+
+    Definition monad_map_branch (b : branch term) :=
+      bbody <- bbodyf b.(bbody);;
+      ret {| bcontext := b.(bcontext);
+            bbody := bbody |}.
+  End map_branch.
+
+  Definition monad_map_branches {term B} (f : term -> TemplateMonad B) l := monad_map (monad_map_branch f) l.
+
+  Notation map_branches_k f k brs :=
+    (monad_map (fun b => monad_map_branch (f (#|b.(bcontext)| + k)) b) brs).
+End with_tc.