Update MetaCoq

README.md

@@ -17,7 +17,7 @@ opam switch create . 4.07.1
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam install -j 4 coq.8.11.2 coq-bignums coq-stdpp coq-quickchick
-opam pin -j 4 add https://github.com/MetaCoq/metacoq.git#abc736f20020156e520e7ca4ef0557ce5f8b7db0
+opam pin -j 4 add https://github.com/MetaCoq/metacoq.git#77adb13585d2f357b78642c16b6c4da817f35eff
 ```
 
 After completing the procedures above, run `make` to build the development, and

embedding/examples/Demo.v

@@ -33,7 +33,7 @@ Print id_nat_syn.
 
 (* Unquote *)
 MetaCoq Unquote Definition plus_one :=
-  (MC.tLambda (nNamed "x")
+  (MC.tLambda (aRelevant (nNamed "x"))
               (MC.tInd (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) nil)
               (MC.tApp (MC.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 1 nil)
                        (MC.tRel 0 :: nil))).

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -488,7 +488,7 @@ Definition lpat_to_lam : term -> list term -> list (BasicTC.ident * term) -> ter
          lambda introduces a binder, we need also to lift free
          variables in [ty_params] *)
          let lam_type := subst (map (lift0 #|tys'|) ty_params) 0 ty in
-         rec (tLambda (BasicTC.nNamed n) lam_type body) ty_params tys'
+         rec (tLambda (aRelevant (nNamed n)) lam_type body) ty_params tys'
        end.
 
 
@@ -508,7 +508,7 @@ Qed.
 
 Lemma pat_to_lam_unfold b tys n ty params :
   lpat_to_lam b params (tys ++ [(n,ty)]) =
-  tLambda (BasicTC.nNamed n) (subst0 params ty) (lpat_to_lam b (map (lift0 1) params) tys).
+  tLambda (aRelevant (nNamed n)) (subst0 params ty) (lpat_to_lam b (map (lift0 1) params) tys).
 Proof.
   revert b params.
   induction tys;intros.
@@ -1766,7 +1766,7 @@ Qed.
 
 
 Lemma from_vConstr_not_lambda :
-  forall (Σ : global_env) (i : Ast.inductive) (n0 : ename) (na : BasicAst.name) (t0 b : term) l,
+  forall (Σ : global_env) (i : Ast.inductive) (n0 : ename) (na : aname) (t0 b : term) l,
     tLambda na t0 b = t⟦ of_val_i (vConstr i n0 l) ⟧ Σ -> False.
 Proof.
   intros Σ i n0 na t0 b l H.

embedding/theories/pcuic/PCUICTranslate.v

@@ -64,17 +64,20 @@ Fixpoint string_of_modpath (mp : modpath) : string :=
 Definition string_of_kername (kn : kername) :=
   (string_of_modpath kn.1 ++ "@" ++ kn.2)%string.
 
+Definition aRelevant (n : name) :=
+  {| binder_name := n; binder_relevance := Relevant |}.
+
 (** Translation of types to PCUIC terms. Universal types become Pi-types with the first argument being of type [Set]. Keeping them in [Set] is crucial, since we don't have to deal with universe levels *)
 Fixpoint type_to_term (ty : type) : term :=
   match ty with
   | tyInd i => tInd (mkInd (kername_of_string i) 0) []
-  | tyForall nm ty => tProd (nNamed nm) (tSort Universe.type0) T⟦ty⟧
+  | tyForall nm ty => tProd (aRelevant (nNamed nm)) (tSort Universe.type0) T⟦ty⟧
   | tyVar nm => tVar nm
   | tyApp ty1 ty2 => tApp T⟦ty1⟧ T⟦ty2⟧
   | tyArr ty1 ty2 =>
     (* NOTE: we have to lift indices for the codomain,
        since in Coq arrows are Pi types and introduce an binder *)
-    tProd nAnon T⟦ty1⟧ (lift0 1 T⟦ty2⟧)
+    tProd (aRelevant nAnon) T⟦ty1⟧ (lift0 1 T⟦ty2⟧)
   | tyRel i => tRel i
   end
 where "T⟦ ty ⟧ " := (type_to_term ty).
@@ -91,7 +94,7 @@ Definition pat_to_lam (body : term)
       introduces a binder, we need also to lift free variables in
       [ty_params] *)
       let lam_type := subst ty_params 0 ty in
-      tLambda (BasicTC.nNamed n) lam_type (rec (map (lift0 1) ty_params) tys')
+      tLambda (aRelevant (nNamed n)) lam_type (rec (map (lift0 1) ty_params) tys')
     end).
 
 (** Translating branches of the [eCase] construct. Note that MetaCoq uses indices to represent constructors. Indices are corresponding positions in the list of constructors for a particular inductive type *)
@@ -121,9 +124,9 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   match e with
   | eRel i => tRel i
   | eVar nm => tVar nm
-  | eLambda nm ty b => tLambda (nNamed nm) T⟦ty⟧ t⟦b⟧Σ
-  | eTyLam nm b => tLambda (nNamed nm) (tSort Universe.type0) t⟦b⟧Σ
-  | eLetIn nm e1 ty e2 => tLetIn (nNamed nm) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
+  | eLambda nm ty b => tLambda (aRelevant (nNamed nm)) T⟦ty⟧ t⟦b⟧Σ
+  | eTyLam nm b => tLambda (aRelevant (nNamed nm)) (tSort Universe.type0) t⟦b⟧Σ
+  | eLetIn nm e1 ty e2 => tLetIn (aRelevant (nNamed nm)) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
   | eApp e1 e2 => tApp t⟦e1⟧Σ t⟦e2⟧Σ
   | eConstr i t =>
     match (resolve_constr Σ i t) with
@@ -133,8 +136,9 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eConst nm => tConst (kername_of_string nm) []
   | eCase nm_i ty2 e bs =>
     let (nm, params) := nm_i in
-    let typeInfo := tLambda nAnon (mkApps (tInd (mkInd (kername_of_string nm) 0) [])
-                                          (map type_to_term params))
+    let typeInfo := tLambda (aRelevant nAnon)
+                            (mkApps (tInd (mkInd (kername_of_string nm) 0) [])
+                                    (map type_to_term params))
                             (lift0 1 (type_to_term ty2)) in
     match (resolve_inductive Σ nm) with
     | Some v =>
@@ -149,11 +153,11 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eFix nm nv ty1 ty2 b =>
     let tty1 := T⟦ty1⟧ in
     let tty2 := T⟦ty2⟧ in
-    let ty := tProd nAnon tty1 (lift0 1 tty2) in
+    let ty := tProd (aRelevant nAnon) tty1 (lift0 1 tty2) in
     (* NOTE: we have to lift the indices in [tty1] because [tRel 0]
              corresponds to the recursive call *)
-    let body := tLambda (nNamed nv) (lift0 1 tty1) t⟦b⟧Σ in
-    tFix [(mkdef _ (nNamed nm) ty body 0)] 0
+    let body := tLambda (aRelevant (nNamed nv)) (lift0 1 tty1) t⟦b⟧Σ in
+    tFix [(mkdef _ (aRelevant (nNamed nm)) ty body 0)] 0
   | eTy ty => T⟦ty⟧
   end
 where "t⟦ e ⟧ Σ":= (expr_to_term Σ e).
@@ -163,12 +167,12 @@ where "t⟦ e ⟧ Σ":= (expr_to_term Σ e).
 
 Import Basics.
 
-Definition of_ename (e : option ename) : BasicTC.name :=
+Definition of_ename (e : option ename) : aname :=
   match e with
   | Some e' =>
     let (mp,unqualified_nm) := kername_of_string e' in
-    BasicTC.nNamed unqualified_nm
-  | None => BasicTC.nAnon
+    aRelevant (nNamed unqualified_nm)
+  | None => aRelevant nAnon
   end.
 
 (** Translation of constructors of parameterised inductive types requires

embedding/theories/pcuic/PCUICtoTemplate.v

@@ -3,52 +3,17 @@ From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From MetaCoq.Template Require Import All.
      (* config utils AstUtils BasicAst Ast. *)
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGeneration.
+From MetaCoq.PCUIC Require Export PCUICToTemplate.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
 
 Module TC := Ast.
 Module P := PCUICAst.
 
-Fixpoint trans (t : P.term) : TC.term :=
-  match t with
-  | P.tRel n => TC.tRel n
-  | P.tVar n => TC.tVar n
-  | P.tEvar ev args => TC.tEvar ev (List.map trans args)
-  | P.tSort u => TC.tSort u
-  | P.tConst c u => TC.tConst c u
-  | P.tInd c u => TC.tInd c u
-  | P.tConstruct c k u => TC.tConstruct c k u
-  | P.tLambda na T M => TC.tLambda na (trans T) (trans M)
-  | P.tApp u v => TC.mkApps (trans u) [trans v]
-  | P.tProd na A B => TC.tProd na (trans A) (trans B)
-  | P.tLetIn na b t b' => TC.tLetIn na (trans b) (trans t) (trans b')
-  | P.tCase ind p c brs =>
-    let brs' := List.map (on_snd trans) brs in
-    TC.tCase ind (trans p) (trans c) brs'
-  | P.tProj p c => TC.tProj p (trans c)
-  | P.tFix mfix idx =>
-    let mfix' := List.map (map_def trans trans) mfix in
-    TC.tFix mfix' idx
-  | P.tCoFix mfix idx =>
-    let mfix' := List.map (map_def trans trans) mfix in
-    TC.tCoFix mfix' idx
-  end.
-
-Definition trans_decl (d : P.context_decl) :=
-  let 'P.mkdecl na b t := d in
-  {| TC.decl_name := na;
-     TC.decl_body := option_map trans b;
-     TC.decl_type := trans t |}.
-
-Definition trans_local Γ := List.map trans_decl Γ.
-
-Definition trans_one_ind_body (d : P.one_inductive_body) :=
-  {| TC.ind_name := d.(P.ind_name);
-     TC.ind_type := trans d.(P.ind_type);
-     TC.ind_kelim := d.(P.ind_kelim);
-     TC.ind_ctors := List.map (fun '(x, y, z) => (x, trans y, z)) d.(P.ind_ctors);
-     TC.ind_projs := List.map (fun '(x, y) => (x, trans y)) d.(P.ind_projs) |}.
+Definition aRelevant (n : name) : aname :=
+  {| binder_name := n;
+     binder_relevance := Relevant |}.
 
 Definition trans_local_entry (nle : ident * P.local_entry) : TC.context_decl :=
   let (nm, le) := nle in
@@ -58,9 +23,9 @@ Definition trans_local_entry (nle : ident * P.local_entry) : TC.context_decl :=
        bodies as parameters, so we produce a dummy value here.
        To produce an actual decalaration with a body we need its type,
        and it's not available it this point*)
-    TC.mkdecl (nNamed nm) None (TC.tVar "not supported")
+    TC.mkdecl (aRelevant (nNamed nm)) None (TC.tVar "not supported")
   | P.LocalAssum la =>
-    TC.mkdecl (nNamed nm) None (trans la)
+    TC.mkdecl (aRelevant (nNamed nm)) None (trans la)
   end.
 
 Definition trans_one_ind_entry (d : P.one_inductive_entry) : TC.one_inductive_entry :=
@@ -84,28 +49,3 @@ Definition trans_minductive_entry (e : P.mutual_inductive_entry) :  TC.mutual_in
      TC.mind_entry_universes := trans_universes_decl e.(P.mind_entry_universes);
      TC.mind_entry_variance := None;
      TC.mind_entry_private := e.(P.mind_entry_private) |}.
-
-Definition trans_constant_body (bd : P.constant_body) : TC.constant_body :=
-  {| TC.cst_type := trans bd.(P.cst_type);
-     TC.cst_body := option_map trans bd.(P.cst_body);
-     TC.cst_universes := bd.(P.cst_universes) |}.
-
-Definition trans_minductive_body md :=
-  {| TC.ind_finite := md.(P.ind_finite);
-     TC.ind_npars := md.(P.ind_npars);
-     TC.ind_params := trans_local md.(P.ind_params);
-     TC.ind_bodies := map trans_one_ind_body md.(P.ind_bodies);
-     TC.ind_variance := md.(ind_variance);
-     TC.ind_universes := md.(P.ind_universes) |}.
-
-Definition trans_global_decl (d : P.global_decl) : TC.global_decl :=
-  match d with
-  | P.ConstantDecl bd => TC.ConstantDecl (trans_constant_body bd)
-  | P.InductiveDecl bd => TC.InductiveDecl (trans_minductive_body bd)
-  end.
-
-Definition trans_global_env (d : P.global_env) :=
-  List.map (on_snd trans_global_decl) d.
-
-Definition trans_global (Σ : P.global_env_ext) : TC.global_env_ext :=
-  (trans_global_env (fst Σ), snd Σ).

extra/docker/ConCert-8.11/Dockerfile

@@ -9,7 +9,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam install -y -v -j ${NJOBS} coq-equations.1.2.1+8.11 coq-stdpp coq-quickchick \
   && git clone https://github.com/MetaCoq/metacoq.git \
   && cd metacoq \
-  && git checkout coq-8.11 \
+  && git checkout 77adb13585d2f357b78642c16b6c4da817f35eff \
   && opam install -y -v -j ${NJOBS} . \
   && opam clean -a -c -s --logs \
   && opam config list \

extraction/examples/ErasureTests.v

@@ -7,7 +7,6 @@ From Coq Require Import Ascii.
 From Coq Require Import Bool.
 From Coq Require Import List.
 From Coq Require Import String.
-From MetaCoq.Erasure Require Import SafeTemplateErasure.
 From MetaCoq.PCUIC Require Import PCUICAst.
 From MetaCoq.PCUIC Require Import PCUICTyping.
 From MetaCoq.PCUIC Require Import TemplateToPCUIC.
@@ -24,6 +23,8 @@ Import ListNotations.
 Import MonadNotation.
 Set Equations Transparent.
 
+Local Existing Instance extraction_checker_flags.
+
 Module flag_of_type_tests.
 Record type_flag_squashed :=
   { is_logical : bool;

extraction/examples/ForPaper.v

@@ -11,9 +11,8 @@ From ConCert.Extraction Require Import Erasure.
 
 From MetaCoq.Template Require Import Kernames.
 From MetaCoq.Template Require Import Loader.
-From MetaCoq.Erasure Require Import SafeTemplateErasure Loader.
+From MetaCoq.Erasure Require Import Loader.
 From MetaCoq.Erasure Require ErasureFunction.
-From MetaCoq.Erasure Require SafeErasureFunction.
 From MetaCoq.Template Require Import config.
 From MetaCoq.SafeChecker Require Import PCUICSafeReduce PCUICSafeChecker
      SafeTemplateChecker.

extraction/plugin/_CoqProject

@@ -93,8 +93,8 @@ src/resultMonad.ml
 src/resultMonad.mli
 src/rustExtract.ml
 src/rustExtract.mli
-src/safeErasureFunction.ml
-src/safeErasureFunction.mli
+src/erasureFunction.ml
+src/erasureFunction.mli
 src/safeTemplateChecker.ml
 src/safeTemplateChecker.mli
 src/ssrbool.ml

extraction/plugin/src/.gitignore

@@ -82,8 +82,8 @@ resultMonad.ml
 resultMonad.mli
 rustExtract.ml
 rustExtract.mli
-safeErasureFunction.ml
-safeErasureFunction.mli
+erasureFunction.ml
+erasureFunction.mli
 safeTemplateChecker.ml
 safeTemplateChecker.mli
 ssrbool.ml

extraction/plugin/src/concert_extraction_plugin.mlpack

@@ -40,7 +40,7 @@ ETyping
 EPretty
 Extract
 EOptimizePropDiscr
-SafeErasureFunction
+ErasureFunction
 Typing0
 SafeTemplateChecker
 

extraction/process_extraction.sh

@@ -21,10 +21,6 @@ then
   files=`cat ../template-coq-files.txt`
   echo "Removing files linked in template-coq:" $files
   rm -f $files
-
-  echo "Fixing extraction bugs"
-  sed -i "s/Coq__2/Coq__1/g" common1.mli
-  sed -i "s/Coq__3/Coq__1/g" common1.mli
 else
   echo "Extraction up to date"
 fi