Support for Coq 8.20

.github/workflows/build.yml

@@ -18,7 +18,7 @@ jobs:
         opam_file:
           - 'coq-certicoq.opam'
         image:
-          - 'mattam82/metacoq:metacoq-1.3.2-coq-8.19'
+          - 'mattam82/metacoq:metacoq-1.3.4-coq-8.20'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3

Makefile

@@ -2,8 +2,8 @@
 
 
 all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile
-	$(MAKE) -C libraries -j1
-	$(MAKE) -C theories -j1
+	$(MAKE) -C libraries 
+	$(MAKE) -C theories 
 
 theories/Makefile: theories/_CoqProject
 	cd theories;coq_makefile -f _CoqProject -o Makefile

benchmarks/certicoq_eval_issue.v

@@ -32,7 +32,7 @@ Import ListNotations.
 Definition l : list nat := map (fun x => x * x) (repeat 3 4000).
 
 Lemma nth_l : 3000 < length l.
-Proof. unfold l. rewrite map_length. rewrite repeat_length. Admitted.
+Proof. unfold l. rewrite length_map. rewrite repeat_length. Admitted.
 
 Definition test : nat := (nth l (3000; nth_l)).
 (* Time Eval vm_compute in test. *)

benchmarks/lib/Color.v

@@ -230,9 +230,9 @@ Proof.
 intros.
 do 2 rewrite M.cardinal_1.
 transitivity (length (map (@fst _ _) (M.elements (M.map f g)))).
-rewrite map_length; auto.
+rewrite length_map; auto.
 transitivity (length (map (@fst _ _) (M.elements g))).
-2: rewrite map_length; auto.
+2: rewrite length_map; auto.
 apply eqlistA_length with E.eq.
 apply SortE_equivlistE_eqlistE; auto.
 generalize (M.elements_3 (M.map f g)).

benchmarks/lib/vs.v

@@ -425,9 +425,9 @@ pure atoms *)
 
 Inductive pure_atom := Eqv : expr -> expr -> pure_atom.
 
-Let var1 : var := Z2id 1.
-Let var0 : var := Z2id 0.
-Let var2 : var := Z2id 2.
+Definition var1 : var := Z2id 1.
+Definition var0 : var := Z2id 0.
+Definition var2 : var := Z2id 2.
 
 Fixpoint list_prio {A} (weight: var) (l: list A) (p: var) : var :=
   match l with

benchmarks/metacoq_erasure/certiCoqErase.ml

@@ -58,7 +58,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   let open List in
   let rec aux p = 
   match p with
-  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ -> p
+  | Coq_tRel _ | Coq_tVar _ | Coq_tConst _ | Coq_tInd _ | Coq_tConstruct _ | Coq_tInt _ | Coq_tFloat _ | tString _ -> p
   | Coq_tEvar (k, l) -> Coq_tEvar (k, map aux l)
   | Coq_tSort u -> Coq_tSort (fix_universe u)
   | Coq_tCast (t, k, t') -> Coq_tCast (aux t, k, aux t')
@@ -136,4 +136,4 @@ let erase ~bypass env evm c =
   debug (fun () -> str"Quoting");
   let prog = time (str"Quoting") (quote_term_rec ~bypass ~with_universes:false env) evm (EConstr.to_constr evm c) in
   let prog = fix_quoted_program prog in
-  time (str"Erasure") certicoq_erase prog
+  time (str"Erasure") certicoq_erase prog

bootstrap/certicoqc/Makefile

@@ -56,7 +56,7 @@ COQLIB = $(shell coqc -where)
 COQLIBINSTALL = $(COQLIB)/user-contrib/CertiCoq/CertiCoqC
 OCAMLLIB = $(shell ocamlc -where)
 OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_plugin -package coq-certicoq-vanilla.plugin -open Certicoq_vanilla_plugin \
-	-I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  -w -8
+	-I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68   -safe-string -strict-sequence -w -33  -w -34  -w -32  -w -39  -w -20  -w -60  
 GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 CFILES = certicoqc_wrapper.c $(GENCFILES)
 
@@ -86,7 +86,7 @@ test.vo: test.v
 	mkdir -p tests
 	ulimit -a
 	ulimit -H -a
-	ulimit -Ss 65500 && coqc $(TESTCOQOPTS) test.v
+	ulimit -Ss unlimited && ulimit -s unlimited && coqc $(TESTCOQOPTS) test.v
 
 clean: Makefile.certicoqc
 	make -f Makefile.certicoqc clean

bootstrap/certicoqc/certicoqc_plugin_wrapper.ml

@@ -79,6 +79,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
   | Coq_tInt i -> Coq_tInt i
   | Coq_tFloat f -> Coq_tFloat f
+  | Coq_tString f -> Coq_tString f
   | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty)
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
@@ -171,4 +172,4 @@ let compile opts prog =
   let res = certicoq_pipeline opts prog in
   info "Certicoq pipeline ran";
   (* print_obj 10 (Obj.repr (fst res)); *)
-  res
+  res

bootstrap/certicoqc/test.v

@@ -47,4 +47,6 @@ CertiCoqC Eval demo2. *)
 
 (* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *)
 
+Require Import Coq.Strings.PrimString.
+
 Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc.

bootstrap/certicoqchk/Makefile

@@ -37,7 +37,7 @@ GENCFILES = glue.c CertiCoq.CertiCoqCheck.compile.certicoqchk.c
 CFILES = certicoqchk_wrapper.c ${GENCFILES}
 
 RUNTIME_DIR = ../../runtime
-RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o
+RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_string.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o
 
 CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2
 # ccomp: CCOMPILEROPTS = -g -c -I . -I ${OCAMLLIB} -O2
@@ -103,4 +103,4 @@ install: Loader.vo certicoqchk_plugin.cmxs
 
 .PHONY: plugin test
 
-.NOTPARALLEL:
+.NOTPARALLEL:

coq-certicoq.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev+8.19"
+version: "dev+8.20"
 maintainer: "The CertiCoq Team"
 homepage: "https://certicoq.org/"
 dev-repo: "git+https://github.com/CertiCoq/certicoq"
@@ -31,11 +31,11 @@ depends: [
   "ocaml" {>= "4.13"}
   "conf-clang"
   "stdlib-shims"
-  "coq" {>= "8.19" & < "8.20~"}
+  "coq" {>= "8.20" & < "8.21~"}
   "coq-compcert" {= "3.13.1"}
-  "coq-equations" {= "1.3+8.19"}
-  "coq-metacoq-erasure-plugin" {= "1.3.2+8.19"}
-  "coq-metacoq-safechecker-plugin" {= "1.3.2+8.19"}
+  "coq-equations" {= "1.3.1+8.20"}
+  "coq-metacoq-erasure-plugin" {= "1.3.4+8.20"}
+  "coq-metacoq-safechecker-plugin" {= "1.3.4+8.20"}
   "coq-ext-lib" {>= "0.12"}
 ]
 

cplugin/CertiCoqVanilla.v

@@ -1,2 +1,2 @@
 From CertiCoq.VanillaPlugin Require Import Loader.
-From CertiCoq.VanillaPlugin Require Export CoqMsgFFI PrimInt63 PrimFloats.
+From CertiCoq.VanillaPlugin Require Export CoqMsgFFI PrimInt63 PrimFloats PrimString.                            

cplugin/PrimString.v

@@ -0,0 +1,10 @@
+From CertiCoq.VanillaPlugin Require Import Loader.
+From Coq Require Import PString.
+
+CertiCoq Register [
+  Coq.Strings.PrimString.compare => "prim_string_compare",
+  Coq.Strings.PrimString.get => "prim_string_get",
+  Coq.Strings.PrimString.length => "prim_string_length"
+]
+Include [ Library "prim_string.h" ].
+

cplugin/_CoqProject

@@ -19,6 +19,7 @@ Loader.v
 CoqMsgFFI.v
 PrimInt63.v
 PrimFloats.v
+PrimString.v
 CertiCoqVanilla.v
 
 static/caml_option.mli
@@ -389,6 +390,10 @@ extraction/primFloat.ml
 extraction/primFloat.mli
 extraction/primInt63.ml
 extraction/primInt63.mli
+extraction/primString.ml
+extraction/primString.mli
+extraction/primStringAxioms.ml
+extraction/primStringAxioms.mli
 extraction/primitive.ml
 extraction/primitive.mli
 extraction/proto_util.ml

cplugin/certicoq.ml

@@ -427,6 +427,7 @@ let fix_term (p : Ast0.term) : Ast0.term =
   | Coq_tCoFix (mfix, i) -> Coq_tCoFix (map aux_def mfix, i)
   | Coq_tInt i -> p
   | Coq_tFloat f -> p
+  | Coq_tString s -> p
   | Coq_tArray (u, v, def, ty) -> Coq_tArray (u, map aux v, aux def, aux ty)
   and aux_pred { puinst = puinst; pparams = pparams; pcontext = pcontext; preturn = preturn } =
     { puinst; pparams = map aux pparams; pcontext; preturn = aux preturn }
@@ -782,7 +783,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
   let check_reifyable env sigma ty =
     (* We might have bound universes though. It's fine! *)
     try let (hd, u), args = Inductiveops.find_inductive env sigma ty in
-      IsInductive (hd, EConstr.EInstance.kind sigma u, args)
+      IsInductive (hd, EConstr.EInstance.kind sigma u, List.map (EConstr.to_constr sigma) args)
     with Not_found -> 
       let hnf = Reductionops.whd_all env sigma ty in
       let hd, args = EConstr.decompose_app sigma hnf in
@@ -856,7 +857,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let spec = lookup_mind_specif env hd in
       let npars = inductive_params spec in
       let params, _indices = CList.chop npars args in
-      let indfam = make_ind_family ((hd, u), params) in
+      let indfam = make_ind_family ((hd, EConstr.EInstance.make u), List.map (EConstr.of_constr) params) in
       let cstrs = get_constructors env indfam in
       let cstrs = apply_reordering qhd im cstrs in
       if Obj.is_block v then
@@ -868,7 +869,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
         in
         let cstr = cstrs.(coqidx) in
         let coqidx = find_reverse_mapping qhd im coqidx in
-        let ctx = Vars.smash_rel_context cstr.cs_args in
+        let ctx = Vars.smash_rel_context (EConstr.to_rel_context sigma cstr.cs_args) in
         let vargs = List.init (List.length ctx) (Obj.field v) in
         let args' = List.map2 (fun decl v -> 
           let argty = check_reifyable env sigma 

cplugin/certicoq_vanilla_plugin.mlpack

@@ -23,6 +23,8 @@ BinNat
 BinInt
 PrimInt63
 Uint0
+PrimString
+PrimStringAxioms
 Int0
 Int63
 Byte

plugin/CertiCoq.v

@@ -1,2 +1,2 @@
 From CertiCoq.Plugin Require Export Loader.
-From CertiCoq.Plugin Require Export CoqMsgFFI PrimInt63 PrimFloats.
+From CertiCoq.Plugin Require Export CoqMsgFFI PrimInt63 PrimFloats PrimString.

plugin/PrimString.v

@@ -0,0 +1,10 @@
+From CertiCoq.Plugin Require Import Loader.
+From Coq Require Import PString.
+
+CertiCoq Register [
+    Coq.Strings.PrimString.compare => "prim_string_compare",
+      Coq.Strings.PrimString.get => "prim_string_get",
+      Coq.Strings.PrimString.length => "prim_string_length"
+  ]
+  Include [ Library "prim_string.h" ].
+

plugin/_CoqProject

@@ -19,6 +19,7 @@ Loader.v
 CoqMsgFFI.v
 PrimInt63.v
 PrimFloats.v
+PrimString.v
 CertiCoq.v
 
 static/caml_nat.mli
@@ -386,6 +387,10 @@ extraction/primInt63.ml
 extraction/primInt63.mli
 extraction/primitive.ml
 extraction/primitive.mli
+extraction/primString.ml
+extraction/primString.mli
+extraction/primStringAxioms.ml
+extraction/primStringAxioms.mli
 extraction/proto_util.ml
 extraction/proto_util.mli
 extraction/prototype.ml

plugin/certicoq.ml

@@ -644,7 +644,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
   let check_reifyable env sigma ty =
     (* We might have bound universes though. It's fine! *)
     try let (hd, u), args = Inductiveops.find_inductive env sigma ty in
-      IsInductive (hd, EConstr.EInstance.kind sigma u, args)
+      IsInductive (hd, EConstr.EInstance.kind sigma u, List.map (EConstr.to_constr sigma) args)
     with Not_found -> 
       let hnf = Reductionops.whd_all env sigma ty in
       let hd, args = EConstr.decompose_app sigma hnf in
@@ -718,7 +718,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
       let spec = lookup_mind_specif env hd in
       let npars = inductive_params spec in
       let params, _indices = CList.chop npars args in
-      let indfam = make_ind_family ((hd, u), params) in
+      let indfam = make_ind_family ((hd, EConstr.EInstance.make u), List.map (EConstr.of_constr) params) in
       let cstrs = get_constructors env indfam in
       let cstrs = apply_reordering qhd im cstrs in
       if Obj.is_block v then
@@ -730,7 +730,7 @@ module CompileFunctor (CI : CompilerInterface) = struct
         in
         let cstr = cstrs.(coqidx) in
         let coqidx = find_reverse_mapping qhd im coqidx in
-        let ctx = Vars.smash_rel_context cstr.cs_args in
+        let ctx = Vars.smash_rel_context (EConstr.to_rel_context sigma cstr.cs_args) in
         let vargs = List.init (List.length ctx) (Obj.field v) in
         let args' = List.map2 (fun decl v -> 
           let argty = check_reifyable env sigma 

plugin/certicoq_plugin.mlpack

@@ -23,6 +23,8 @@ PrimInt63
 Uint0
 Int0
 Int63
+PrimString
+PrimStringAxioms
 Byte
 Caml_byte
 Ascii

runtime/prim_int63.c

@@ -7,7 +7,7 @@ typedef value primbool;
 typedef value primintcarry;
 typedef value primintpair;
 
-#define trace(...) // printf(__VA_ARGS__)
+#define trace(...) printf(__VA_ARGS__)
 
 #define maxuint63 0x7FFFFFFFFFFFFFFF
 

runtime/prim_string.c

@@ -0,0 +1,47 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "gc_stack.h"
+#include "prim_int63.h"
+
+typedef value primstring;
+
+#define trace(...) printf(__VA_ARGS__)
+
+value prim_string_compare(primstring x, primstring y)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_compare\n");
+  /* trace("Calling prim_string_compare on %llu and %llu: %lli \n", x, y); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+    return 1;
+}
+
+primint prim_string_get(primstring x, primint y)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_get\n");
+  /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+    return 97;
+}
+
+primint prim_string_length(primstring x)
+{
+  /* register signed long long xr = Unsigned_long_val(x); */
+  /* register signed long long yr = Unsigned_long_val(y); */
+  /* register signed long long result = xr - yr; */
+  trace("Calling prim_string_length\n");
+  /* trace("Calling prim_int63_compare on %llu and %llu: %lli \n", xr, yr, result); */
+  /* if (result == 0) return 1; */
+  /* else if (result < 0) return 3; */
+  /* else */
+  return 0;
+}

runtime/prim_string.h

@@ -0,0 +1,8 @@
+#include "values.h"
+#include "prim_int63.h"
+
+typedef value primstring;
+
+extern value prim_string_compare(primstring x);
+extern primint prim_string_get(primstring x, primint y);
+extern value prim_string_length(primstring x);

theories/Codegen/LambdaANF_to_Clight_correct.v

@@ -7842,8 +7842,8 @@ Proof.
                        destruct H2.
                        * revert H2. apply H_not_in_L.
                          int_red.
-                         rewrite app_length.
-                         rewrite rev_length.
+                         rewrite length_app.
+                         rewrite length_rev.
                          simpl length.
                          rewrite Nat2Z.inj_add.
                          rewrite Nat2Z.inj_succ. chunk_red; omega.                         

theories/Extraction/extraction.v

@@ -16,7 +16,7 @@ Require Glue.glue
 
 From MetaCoq.ErasurePlugin Require Import Erasure.
 (* Standard lib *)
-Require Import ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
+Require Import ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63 ExtrOCamlPString.
 Require Import Coq.extraction.Extraction.
 Require Import ZArith NArith.
 

theories/ExtractionVanilla/extraction.v

@@ -15,7 +15,7 @@ Require Glue.glue
         Compiler.pipeline.
 
 Require Import Coq.extraction.Extraction.
-Require Import VanillaExtrOCamlInt63 VanillaExtrOCamlFloats.
+Require Import VanillaExtrOCamlInt63 VanillaExtrOCamlFloats ExtrOCamlPString.
 (* Standard lib *)
 
 (** Extraction to Ocaml : use of basic Ocaml types: be careful that this should