Port to work with metacoq-1.0

extra/docker/ConCert-deps-8.14/Dockerfile

@@ -3,7 +3,7 @@ FROM coqorg/coq:8.14
 # build dependencies
 RUN ["/bin/bash", "--login", "-c", "set -x \
   && eval $(opam env --switch=${COMPILER} --set-switch) \
-  && opam repository add --all-switches --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git \
+  && opam repository add --all-switches --set-default coq-released https://coq.inria.fr/opam/released \
   && opam update -y -u \
   && opam install -y -v -j ${NJOBS} coq-equations.1.3+8.14 coq-stdpp.1.6.0 coq-quickchick.1.5.1 \
   && opam pin -y -j ${NJOBS} add https://github.com/MetaCoq/metacoq.git#f47a91c63206d01b853d8abb016e7f04165cd518 \

extraction/plugin/_CoqProject

@@ -46,6 +46,8 @@ src/fin.ml
 src/fin.mli
 src/init0.ml
 src/init0.mli
+src/mCProd.ml
+src/mCProd.mli
 src/optimize.ml
 src/optimize.mli
 src/optimizePropDiscr.ml

extraction/plugin/src/concert_extraction_plugin.mlpack

@@ -13,6 +13,7 @@ UGraph0
 OrderedTypeAlt
 Kernames
 Reflect
+MCProd
 
 PCUICPrimitive
 PCUICAst

extraction/plugin/src/mCProd.ml

@@ -0,0 +1,11 @@
+open Datatypes
+
+(** val on_snd : ('a2 -> 'a3) -> ('a1 * 'a2) -> 'a1 * 'a3 **)
+
+let on_snd f p =
+  ((fst p), (f (snd p)))
+
+(** val test_snd : ('a2 -> bool) -> ('a1 * 'a2) -> bool **)
+
+let test_snd f p =
+  f (snd p)

extraction/plugin/src/mCProd.mli

@@ -0,0 +1,5 @@
+open Datatypes
+
+val on_snd : ('a2 -> 'a3) -> ('a1 * 'a2) -> 'a1 * 'a3
+
+val test_snd : ('a2 -> bool) -> ('a1 * 'a2) -> bool

extraction/plugin/template-coq-files.txt

@@ -99,8 +99,6 @@ mCList.ml
 mCList.mli
 mCOption.ml
 mCOption.mli
-mCProd.ml
-mCProd.mli
 mCRelations.ml
 mCRelations.mli
 mCReflect.mli

extraction/tests/TypeAnnotationTests.v

@@ -68,9 +68,10 @@ Section printing.
         "(" ^ print_term_annotated Γ hd hda ^ ") "
         ^ "(" ^ print_term_annotated Γ arg arga ^ ") : " ^ print_box_type bt
     | tConst s => fun bt => s.2 ^ " : "  ^ print_box_type bt
-    | tConstruct ind c =>
+    | tConstruct ind c [] =>
       fun bt =>
         print_ind_ctor ind c ^ " : " ^ print_box_type bt
+    | tConstruct ind c (_ :: _) => fun _ => "Error(constructors_as_blocks_not_supported)"
     | _ => fun _ => "error: cannot print"
     end.
 

extraction/theories/CameLIGOPretty.v

@@ -397,7 +397,7 @@ Section PPTerm.
 
   Definition is_record_constr (t : term) : option ExAst.one_inductive_body := 
     match t with
-    | tConstruct (mkInd mind j as ind) i =>
+    | tConstruct (mkInd mind j as ind) i _ =>
       match lookup_ind_decl mind i with
       (* Check if it has only 1 constructor, and projections are specified *)
       | Some oib => match ExAst.ind_projs oib, Nat.eqb 1 (List.length oib.(ExAst.ind_ctors)) with
@@ -557,7 +557,7 @@ Section PPTerm.
           else if nm =? "snd" then
             (String.concat " " (map (parens true) apps)) ++ ".1"
           else parens (top || inapp) (nm ++ " " ++ (String.concat " " (map (parens true) apps)))
-        | tConstruct (mkInd mind j as ind) i =>
+        | tConstruct (mkInd mind j as ind) i [] =>
           let nm := get_constr_name ind i in
              (* is it a pair ? *)
             if (uncapitalize nm =? "pair") then
@@ -599,8 +599,7 @@ Section PPTerm.
         "(Map.empty: " ++ print_box_type ty_ctx TT bt ++ ")"
       else
         nm_tt
-    | tConstruct
-        ind l => fun bt =>
+    | tConstruct ind l [] => fun bt =>
       let nm := get_constr_name ind l in
       match print_num_literal TT t with
       | Some lit => lit
@@ -664,6 +663,7 @@ Section PPTerm.
                   ++ MCString.string_of_list (fun b => string_of_term (snd b)) brs ++ ")"
         end
       end
+    | tConstruct ind l (_ :: _) => fun _ => "Error(constructors_as_blocks_not_supported)"
     | tProj (Kernames.mkProjection (mkInd mind i) pars k) c => fun bt =>
       let ind := mkInd mind i in
       match lookup_ind_decl mind i with

extraction/theories/ClosedAux.v

@@ -89,6 +89,12 @@ Proof.
     erewrite <- IHt2 by easy.
     easy.
   - easy.
+  - apply forallb_Forall in clos.
+    rewrite forallb_map.
+    apply forallb_Forall.
+    apply All_Forall in X.
+    rewrite Forall_forall in *.
+    intros. eapply X;eauto. now apply clos.
   - split; [easy|].
     destruct clos as (_ & clos).
     induction X; cbn in *; propify;auto.
@@ -146,6 +152,16 @@ Proof.
     + f_equal; lia.
     + rewrite <- (proj2 clos); f_equal; lia.
   - easy.
+  - apply forallb_Forall in clos.
+    rewrite forallb_map.
+    apply forallb_Forall.
+    apply All_Forall in X.
+    clear X.
+    induction clos;auto.
+    constructor.
+    rewrite <- closedn_subst_eq by now apply forallb_Forall.
+    assumption.
+    apply IHclos.
   - split; [easy|].
     induction X; cbn in *; propify;auto.
     replace (#|x.1| + (k + k' + #|s|)) with (k + (#|x.1| + k') + #|s|) in * by lia.

extraction/theories/Common.v

@@ -175,7 +175,7 @@ Definition iota_body (Σ : global_env) (body : term) : term :=
 
 Fixpoint nat_syn_to_nat (t : EAst.term) : option nat :=
   match t with
-  | EAst.tApp (EAst.tConstruct ind i) t0 =>
+  | EAst.tApp (EAst.tConstruct ind i []) t0 =>
     if eq_kername ind.(inductive_mind) <%% nat %%> then
       match i with
       | 1 => match nat_syn_to_nat t0 with
@@ -185,35 +185,35 @@ Fixpoint nat_syn_to_nat (t : EAst.term) : option nat :=
       | _ => None
       end
     else None
-  | EAst.tConstruct ind 0 =>
+  | EAst.tConstruct ind 0 [] =>
     if eq_kername ind.(inductive_mind) <%% nat %%> then
       Some 0
     else None
   | _ => None
   end.
 
 Definition _xI :=
-  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 0.
+  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 0 [].
 
 Definition _xO :=
-  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 1.
+  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 1 [].
 
 Definition _xH :=
-  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 2.
+  EAst.tConstruct {| inductive_mind := <%% positive %%>; inductive_ind := 0 |} 2 [].
 
-Definition _N0 := EAst.tConstruct {| inductive_mind := <%% N %%>; inductive_ind := 0 |} 0.
+Definition _N0 := EAst.tConstruct {| inductive_mind := <%% N %%>; inductive_ind := 0 |} 0 [].
 
-Definition _Npos := EAst.tConstruct {| inductive_mind := <%% N %%>; inductive_ind := 0 |} 1.
+Definition _Npos := EAst.tConstruct {| inductive_mind := <%% N %%>; inductive_ind := 0 |} 1 [].
 
-Definition _Z0 :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 0.
+Definition _Z0 :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 0 [].
 
-Definition _Zpos :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 1.
+Definition _Zpos :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 1 [].
 
-Definition _Zneg :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 2.
+Definition _Zneg :=  EAst.tConstruct {| inductive_mind := <%% Z %%>; inductive_ind := 0 |} 2 [].
 
 Fixpoint pos_syn_to_nat_aux (n : nat) (t : EAst.term) : option nat :=
   match t with
-  | EAst.tApp (EAst.tConstruct ind i) t0 =>
+  | EAst.tApp (EAst.tConstruct ind i []) t0 =>
     if eq_kername ind.(inductive_mind) <%% positive %%> then
       match i with
       | 0 => match pos_syn_to_nat_aux (n + n) t0 with
@@ -225,7 +225,7 @@ Fixpoint pos_syn_to_nat_aux (n : nat) (t : EAst.term) : option nat :=
       end
     else None
   | EAst.tApp _xO t0 => pos_syn_to_nat_aux (n + n) t0
-  | EAst.tConstruct ind 2 =>
+  | EAst.tConstruct ind 2 [] =>
     if eq_kername ind.(inductive_mind) <%% positive %%> then Some n
     else None
   | _ => None
@@ -235,10 +235,10 @@ Definition pos_syn_to_nat := pos_syn_to_nat_aux 1.
 
 Definition N_syn_to_nat (t : EAst.term) : option nat :=
   match t with
-  | EAst.tConstruct ind 0 =>
+  | EAst.tConstruct ind 0 [] =>
     if eq_kername ind.(inductive_mind) <%% N %%> then Some 0
     else None
-  | EAst.tApp (EAst.tConstruct ind 1) t0 =>
+  | EAst.tApp (EAst.tConstruct ind 1 []) t0 =>
     if eq_kername ind.(inductive_mind) <%% N %%> then
       match pos_syn_to_nat t0 with
       | Some v => Some v
@@ -250,10 +250,10 @@ Definition N_syn_to_nat (t : EAst.term) : option nat :=
 
 Definition Z_syn_to_Z (t : EAst.term) : option Z :=
   match t with
-  | EAst.tConstruct ind 0 =>
+  | EAst.tConstruct ind 0 [] =>
     if eq_kername ind.(inductive_mind) <%% Z %%> then Some 0%Z
     else None
-  | EAst.tApp (EAst.tConstruct ind i) t0 =>
+  | EAst.tApp (EAst.tConstruct ind i []) t0 =>
     if eq_kername ind.(inductive_mind) <%% Z %%> then
       match i with
       | 1 => match pos_syn_to_nat t0 with

extraction/theories/ElmExtract.v

@@ -376,7 +376,10 @@ Fixpoint print_term (Γ : list ident) (t : term) : PrettyPrinter unit :=
     print_parenthesized (parenthesize_app_arg arg) (print_term Γ arg)
 
   | tConst name => append (get_fun_name name)
-  | tConstruct ind i => print_ind_ctor ind i
+  | tConstruct ind i [] => print_ind_ctor ind i
+  | tConstruct ind i (_ :: _) =>
+           printer_fail ("Costructors-as-blocks is not supported: "
+                         ^ bs_to_s (string_of_kername ind.(inductive_mind)))
 
   | tCase (ind, npars) discriminee branches =>
     match branches with

extraction/theories/ExtractionCorrectness.v

@@ -126,7 +126,7 @@ Proof.
   intros cl_t cl_env wfg ev.
   rewrite OptimizePropDiscr.trans_env_optimize_env.
   remember (EEnvMap.GlobalContextMap.make _ _) as Σ0.
-  eapply (EOptimizePropDiscr.optimize_correct (fl:=default_wcbv_flags) (Σ:=Σ0)) with (t0:=t) (v0:=v);subst;cbn;eauto.
+  unshelve eapply (EOptimizePropDiscr.optimize_correct (fl:=default_wcbv_flags) (Σ:=Σ0)) with (t0:=t) (v0:=v);subst;cbn;eauto.
 Qed.
 
 
@@ -143,7 +143,7 @@ Theorem extract_correct
   extract_pcuic_env
     (pcuic_args extract_within_coq)
     Σ (wf_squash wfΣ) (KernameSet.singleton kn) ignored = Ok exΣ ->
-  ∥trans_env exΣ e⊢ E.tConst kn ▷ E.tConstruct ind c∥.
+  ∥trans_env exΣ e⊢ E.tConst kn ▷ E.tConstruct ind c []∥.
 Proof.
   intros ax [T wt] ev not_erasable no_ignores ex.
   cbn -[dearg_transform] in *.
@@ -157,7 +157,7 @@ Proof.
     constructor.
     eapply dearg_transform_correct; eauto.
     clear dt.
-    eapply (@OptimizePropDiscr.optimize_correct _ default_wcbv_flags _ _ (tConst kn) (tConstruct ind c));eauto.
+    eapply (@OptimizePropDiscr.optimize_correct _ default_wcbv_flags _ _ (tConst kn) (tConstruct ind c []));eauto.
     * remember (Erasure.erase_global_decls_deps_recursive _ _ _ _ _) as eΣ.
       assert (EWellformed.wf_glob (trans_env eΣ)) by now subst eΣ;eapply wf_erase_global_decls_recursive.
       now apply EWellformed.wellformed_closed_env.

extraction/theories/LPretty.v

@@ -346,7 +346,7 @@ Section print_term.
                               (projs : list (ident * ExAst.one_inductive_body))
                               : option ExAst.one_inductive_body := 
     match t with
-    | tConstruct (mkInd mind j as ind) i =>
+    | tConstruct (mkInd mind j as ind) i [] =>
       match lookup_ind_decl mind i with
       (* Check if it has only 1 constructor, and projections are specified, and > 1 projections *)
       | Some oib => if is_one_constructor_inductive_and_not_record oib
@@ -510,7 +510,7 @@ Definition get_record_projs (oib : ExAst.one_inductive_body) : list string :=
           else (concat " " (map (parens true) apps)) ++ "." ++ proj_na
         | None => parens (top || inapp) (nm ++ " " ++ (concat " " (map (parens true) apps)))
         end
-    | tConstruct ind i =>
+    | tConstruct ind i [] =>
       let nm := get_constr_name ind i in
       (* is it an natural number literal? *)
       if (nm =? "Z") || (nm =? "S") then
@@ -550,21 +550,13 @@ Definition get_record_projs (oib : ExAst.one_inductive_body) : list string :=
       | None => let nm' := with_default ((capitalize prefix) ++ nm) (look TT nm) in
                 parens top (print_uncurried nm' apps)
       end
-
-      (* else match is_name_remapped nm TT, is_record_constr b projs with
-        | false, Some oib => let projs_and_apps := combine (map fst oib.(ExAst.ind_projs)) apps in 
-        let field_decls_printed := projs_and_apps |> map (fun '(proj, e) => proj ++ " = " ++ e) 
-                                                  |> concat "; " in
-        "{" ++ field_decls_printed ++ "}"
-        | _,_     => let nm' := with_default (look TT nm) ((capitalize prefix) ++ nm) in
-                      parens top (print_uncurried nm' apps)
-        end *)
+    | tConstruct ind l (_ :: _) => "Error(constructors_as_blocks_not_supported)"
     | _ =>  parens (top || inapp) (print_term prefix FT TT Γ false true f ++ " " ++ print_term prefix FT TT Γ false false l)
     end
   | tConst c =>
     let cst_name := string_of_kername c in
     with_default (prefix ++ c.2) (look TT cst_name)
-  | tConstruct ind l =>
+  | tConstruct ind l [] =>
     (* if it is a inductive with one constructor, and not a record, then it is an alias, so we don't print the constructor *)
     match lookup_ind_decl ind.(inductive_mind) ind.(inductive_ind) with
     (* Check if it has only 1 constructor, and projections are specified, and > 1 projections *) 
@@ -575,6 +567,7 @@ Definition get_record_projs (oib : ExAst.one_inductive_body) : list string :=
       let nm := get_constr_name ind l in
       with_default (capitalize prefix ++ capitalize nm) (look TT nm)
     end
+  | tConstruct ind l (_ :: _) => "Error(constructors_as_blocks_not_supported)"
   | tCase (mkInd mind i as ind, nparam) t brs =>
     match brs with
     | [] => "failwith () (* absurd case *)"

extraction/theories/Optimize.v

@@ -221,7 +221,10 @@ Definition dearg_proj (ind : inductive) (npars arg : nat) (discr : term) : term
 Fixpoint dearg_aux (args : list term) (t : term) : term :=
   match t with
   | tApp hd arg => dearg_aux (dearg_aux [] arg :: args) hd
-  | tConstruct ind c => dearg_single (get_ctor_mask ind c) t args
+  | tConstruct ind c _ =>
+      (* NOTE: we don't support constructors-as-blocks at the moment,
+         Therefore, we ignore the block argument list assuming it's empty *)
+      dearg_single (get_ctor_mask ind c) t args
   | tConst kn => dearg_single (get_const_mask kn) t args
   | tCase (ind, npars) discr brs =>
     let discr := dearg_aux [] discr in
@@ -298,6 +301,7 @@ Fixpoint is_dead (rel : nat) (t : term) : bool :=
   | tProj _ t => is_dead rel t
   | tFix defs _
   | tCoFix defs _ => forallb (is_dead (#|defs| + rel) ∘ EAst.dbody) defs
+  | tConstruct _ _ args => forallb (is_dead rel) args
   | _ => true
   end.
 
@@ -341,7 +345,8 @@ Definition valid_proj (ind : inductive) (npars arg : nat) : bool :=
    to the masks. They must have the proper number of parameters, and
    1. For cases, their branches must be compatible with the masks,
       i.e. when "true" appears in the mask, the parameter is unused
-   2. For projections, the projected argument must not be removed *)
+   2. For projections, the projected argument must not be removed
+   3. For constructors, that they are not blocks *)
 Fixpoint valid_cases (t : term) : bool :=
   match t with
   | tEvar _ ts => forallb valid_cases ts
@@ -353,6 +358,7 @@ Fixpoint valid_cases (t : term) : bool :=
   | tProj (mkProjection ind npars arg) t => valid_cases t && valid_proj ind npars arg
   | tFix defs _
   | tCoFix defs _  => forallb (valid_cases ∘ EAst.dbody) defs
+  | tConstruct _ _ (_ :: _) => false (* check whether constructors are not blocks*)
   | _ => true
   end.
 
@@ -375,7 +381,7 @@ Definition valid_masks_decl (p : kername * bool * global_decl) : bool :=
 Definition valid_masks_env (Σ : global_env) : bool :=
   forallb valid_masks_decl Σ.
 
-(* Check if all applications are applied enough to be deboxed without eta expansion *)
+(* Check if all applications are applied enough to be deboxed without eta expansion. *)
 Fixpoint is_expanded_aux (nargs : nat) (t : term) : bool :=
   match t with
   | tBox => true
@@ -386,7 +392,10 @@ Fixpoint is_expanded_aux (nargs : nat) (t : term) : bool :=
   | tLetIn _ val body => is_expanded_aux 0 val && is_expanded_aux 0 body
   | tApp hd arg => is_expanded_aux 0 arg && is_expanded_aux (S nargs) hd
   | tConst kn => #|get_const_mask kn| <=? nargs
-  | tConstruct ind c => #|get_ctor_mask ind c| <=? nargs
+  | tConstruct ind c _ =>
+      (* NOTE: we don't support constructors-as-blocks at the moment,
+         Therefore, we ignore the block argument list assuming it's empty *)
+      #|get_ctor_mask ind c| <=? nargs
   | tCase _ discr brs => is_expanded_aux 0 discr && forallb (is_expanded_aux 0 ∘ snd) brs
   | tProj _ t => is_expanded_aux 0 t
   | tFix defs _
@@ -581,6 +590,9 @@ Section AnalyzeTop.
     end.
 End AnalyzeTop.
 
+
+(* NOTE: analysis assumes that constructors are in the form [tConstruct ind i [] ],
+   that is, constructors-as-blocks is disabled *)
 Fixpoint analyze (state : analyze_state) (t : term) {struct t} : analyze_state :=
   match t with
   | tBox => state
@@ -591,7 +603,10 @@ Fixpoint analyze (state : analyze_state) (t : term) {struct t} : analyze_state :
   | tLetIn _ val body => remove_var (analyze (new_var (analyze state val)) body)
   | tApp hd arg => analyze (analyze state hd) arg
   | tConst _ => state
-  | tConstruct _ _ => state
+  | tConstruct _ _ _ =>
+      (* NOTE: we don't support constructors-as-blocks at the moment,
+         Therefore, we ignore the block argument list assuming it's empty *)
+      state
   | tCase (ind, npars) discr brs =>
     let state := analyze state discr in
     match get_mib_masks state.2 (inductive_mind ind) with