Merge pull request #998 from MetaCoq/primitive-arrays

Support primitive array terms

.vscode/metacoq.code-workspace

@@ -11,31 +11,68 @@
 
 
 
-			"-R", "safechecker-plugin/theories", "MetaCoq.SafeCheckerPlugin",
 
-			"-R", "utils/theories", "MetaCoq.Utils",
-			"-R", "common/theories", "MetaCoq.Common",
-			"-R", "template-pcuic/theories", "MetaCoq.TemplatePCUIC",
+
+			"-R", "safechecker-plugin/theories","MetaCoq.SafeCheckerPlugin",
+
+			"-R", "utils/theories","MetaCoq.Utils",
+			"-R", "common/theories","MetaCoq.Common",
+			"-R", "template-pcuic/theories","MetaCoq.TemplatePCUIC",
 
 		"-I", "template-coq",
     	//	"-bt", get backtraces from Coq on errors
 		"-I", "template-coq/build",
 		"-R", "template-coq/theories", "MetaCoq.Template",
 		"-R", "examples", "MetaCoq.Examples",
-		"-R", "checker/theories", "MetaCoq.Checker",
-		"-R", "pcuic/theories", "MetaCoq.PCUIC",
+		"-R", "checker/theories" "MetaCoq.Checker",
+		"-R", "pcuic/theories","MetaCoq.PCUIC",
 		"-I", "safechecker/src",
-		"-R", "safechecker/theories", "MetaCoq.SafeChecker",
+		"-R", "safechecker/theories","MetaCoq.SafeChecker",
 		"-I", "erasure/src",
-		"-R", "erasure/theories", "MetaCoq.Erasure",
-		"-R", "erasure-plugin/theories", "MetaCoq.ErasurePlugin",
-		"-R", "translations", "MetaCoq.Translations",
-		"-R", "test-suite/plugin-demo/theories", "MetaCoq.ExtractedPluginDemo",
-		"-R", "test-suite", "MetaCoq.TestSuite"
+		"-R", "erasure/theories","MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories","MetaCoq.ErasurePlugin",
+		"-R", "translations","MetaCoq.Translations",
+		"-R", "test-suite/plugin-demo/theories","MetaCoq.ExtractedPluginDemo",
+		"-R", "test-suite","MetaCoq.TestSuite",
+		"-R", "quotation/theories", "MetaCoq.Quotation",
+
 	    ],
 
 	 // When enabled, will trim trailing whitespace when saving a file.
 	"files.trimTrailingWhitespace": true,
-	"coqtop.binPath": "_opam/bin"
+	"coqtop.binPath": "_opam/bin",
+	"files.exclude": {
+		"**/*.vo": true,
+		"**/*.vok": true,
+		"**/*.vos": true,
+		"**/*.aux": true,
+		"**/*.glob": true,
+		"**/.git": true,
+		"**/.svn": true,
+		"**/.hg": true,
+		"**/CVS": true,
+		"**/.DS_Store": true,
+		"**/Thumbs.db": true
+	},
+	"coq-lsp.args": [
+	"-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin",
+	"-R", "utils/theories,MetaCoq.Utils",
+		"-R", "common/theories,MetaCoq.Common",
+		"-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC",
+
+	"-I", "template-coq",
+		//"-bt", // get backtraces from Coq on errors
+	//"-Itemplate-coq/build",
+	"-R", "template-coq/theories,MetaCoq.Template",
+	"-R", "examples,MetaCoq.Examples",
+	"-R", "pcuic/theories,MetaCoq.PCUIC",
+	"-R", "safechecker/theories,MetaCoq.SafeChecker",
+	"-R", "erasure/theories,MetaCoq.Erasure",
+	"-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin",
+	"-R", "translations,MetaCoq.Translations",
+	"-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo",
+	"-R", "test-suite,MetaCoq.TestSuite"
+	],
+	"coq-lsp.path": "_opam/bin/coq-lsp"
     }
 }

Makefile

@@ -1,5 +1,5 @@
 
-all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker-plugin quotation
+all: printconf template-coq pcuic safechecker erasure erasure-plugin safechecker-plugin # quotation
 
 -include Makefile.conf
 
@@ -12,7 +12,7 @@ ifeq '$(METACOQ_CONFIG)' 'local'
   export OCAMLPATH
 endif
 
-.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations quotation
+.PHONY: printconf all utils template-coq pcuic erasure install uninstall html clean mrproper .merlin test-suite translations # quotation
 
 printconf:
 ifeq '$(METACOQ_CONFIG)' 'local'
@@ -26,14 +26,14 @@ else
 endif
 endif
 
-install: all 
+install: all
 	$(MAKE) -C utils install
 	$(MAKE) -C common install
 	$(MAKE) -C template-coq install
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
 	$(MAKE) -C template-pcuic install
-	$(MAKE) -C quotation install
+# $(MAKE) -C quotation install
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
 	$(MAKE) -C erasure-plugin install
@@ -45,7 +45,7 @@ uninstall:
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
 	$(MAKE) -C template-pcuic uninstall
-	$(MAKE) -C quotation uninstall
+#	$(MAKE) -C quotation uninstall
 	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
 	$(MAKE) -C erasure-plugin uninstall
@@ -74,7 +74,7 @@ clean:
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C template-pcuic clean
-	$(MAKE) -C quotation clean
+#	$(MAKE) -C quotation clean
 	$(MAKE) -C erasure clean
 	$(MAKE) -C erasure-plugin clean
 	$(MAKE) -C examples clean
@@ -88,7 +88,7 @@ vos:
 	$(MAKE) -C pcuic vos
 	$(MAKE) -C safechecker vos
 	$(MAKE) -C template-pcuic vos
-	$(MAKE) -C quotation vos
+#	$(MAKE) -C quotation vos
 	$(MAKE) -C erasure vos
 	$(MAKE) -C erasure-plugin vos
 	$(MAKE) -C translations vos
@@ -100,7 +100,7 @@ quick:
 	$(MAKE) -C pcuic quick
 	$(MAKE) -C safechecker quick
 	$(MAKE) -C template-pcuic quick
-	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
+#	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
 	$(MAKE) -C erasure quick
 	$(MAKE) -C erasure-plugin quick
 	$(MAKE) -C translations quick
@@ -112,7 +112,7 @@ mrproper:
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C template-pcuic mrproper
-	$(MAKE) -C quotation mrproper
+#	$(MAKE) -C quotation mrproper
 	$(MAKE) -C erasure mrproper
 	$(MAKE) -C erasure-plugin mrproper
 	$(MAKE) -C examples mrproper
@@ -126,7 +126,7 @@ mrproper:
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C template-pcuic .merlin
-	$(MAKE) -C quotation .merlin
+#	$(MAKE) -C quotation .merlin
 	$(MAKE) -C erasure .merlin
 	$(MAKE) -C erasure-plugin .merin
 
@@ -148,8 +148,8 @@ safechecker: pcuic
 template-pcuic: template-coq pcuic
 	$(MAKE) -C template-pcuic
 
-quotation: template-coq pcuic template-pcuic
-	$(MAKE) -C quotation
+#quotation: template-coq pcuic template-pcuic
+#	$(MAKE) -C quotation
 
 safechecker-plugin: safechecker template-pcuic
 	$(MAKE) -C safechecker-plugin

common/theories/Environment.v

@@ -40,51 +40,58 @@ Module Retroknowledge.
   Record t := mk_retroknowledge {
     retro_int63 : option kername;
     retro_float64 : option kername;
+    retro_array : option kername;
   }.
 
-  Definition empty := {| retro_int63 := None; retro_float64 := None |}.
+  Definition empty := {| retro_int63 := None; retro_float64 := None; retro_array := None |}.
 
   Definition extends (x y : t) :=
     option_extends x.(retro_int63) y.(retro_int63) /\
-    option_extends x.(retro_float64) y.(retro_float64).
+    option_extends x.(retro_float64) y.(retro_float64) /\
+    option_extends x.(retro_array) y.(retro_array).
   Existing Class extends.
 
   Definition extendsb (x y : t) :=
     option_extendsb x.(retro_int63) y.(retro_int63) &&
-    option_extendsb x.(retro_float64) y.(retro_float64).
+    option_extendsb x.(retro_float64) y.(retro_float64) &&
+    option_extendsb x.(retro_array) y.(retro_array).
 
   Lemma extendsT x y : reflect (extends x y) (extendsb x y).
   Proof.
-    rewrite /extends/extendsb; do 2 case: option_extendsT; cbn; constructor; intuition.
+    rewrite /extends/extendsb; do 3 case: option_extendsT; cbn; constructor; intuition.
   Qed.
 
   Lemma extends_spec x y : extendsb x y <-> extends x y.
   Proof.
     rewrite /extends/extendsb -!option_extends_spec /is_true !Bool.andb_true_iff //=.
+    intuition auto.
   Qed.
 
   #[global] Instance extends_refl x : extends x x.
   Proof.
-    split; apply option_extends_refl.
+    repeat split; apply option_extends_refl.
   Qed.
 
   #[global] Instance extends_trans : RelationClasses.Transitive Retroknowledge.extends.
   Proof.
-    intros x y z [] []; split; cbn; now etransitivity; tea.
+    intros x y z [? []] [? []]; repeat split; cbn; now etransitivity; tea.
   Qed.
 
   #[export,program] Instance reflect_t : ReflectEq t := {
       eqb x y := (x.(retro_int63) == y.(retro_int63)) &&
-                   (x.(retro_float64) == y.(retro_float64))
+                 (x.(retro_float64) == y.(retro_float64)) &&
+                 (x.(retro_array) == y.(retro_array))
     }.
   Next Obligation.
-    do 2 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
+    do 3 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
   Qed.
 
   (** This operation is asymmetric; it perfers the first argument when the arguments are incompatible, but otherwise takes the join *)
   Definition merge (r1 r2 : t) : t
     := {| retro_int63 := match r1.(retro_int63) with Some v => Some v | None => r2.(retro_int63) end
-       ; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end |}.
+       ; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end
+       ; retro_array := match r1.(retro_array) with Some v => Some v | None => r2.(retro_array) end
+        |}.
 
   Lemma extends_l_merge r1 r2
     : extends r1 (merge r1 r2).
@@ -102,7 +109,8 @@ Module Retroknowledge.
 
   Definition compatible (x y : t) : bool
     := match x.(retro_int63), y.(retro_int63) with Some x, Some y => x == y | _, _ => true end
-       && match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end.
+       && match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end
+       && match x.(retro_array), y.(retro_array) with Some x, Some y => x == y | _, _ => true end.
 
   Lemma extends_r_merge r1 r2
     : compatible r1 r2 -> extends r2 (merge r1 r2).
@@ -836,12 +844,25 @@ Module Environment (T : Term).
     match p with
     | primInt => Σ.(retroknowledge).(Retroknowledge.retro_int63)
     | primFloat => Σ.(retroknowledge).(Retroknowledge.retro_float64)
+    | primArray => Σ.(retroknowledge).(Retroknowledge.retro_array)
     end.
 
-  Definition primitive_invariants (cdecl : constant_body) :=
-    ∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None &
-             cdecl.(cst_universes) = Monomorphic_ctx].
+  Definition tImpl (dom codom : term) : term :=
+    tProd {| binder_name := nAnon; binder_relevance := Relevant |}
+      dom (lift 1 0 codom).
 
+  Definition array_uctx := ([nAnon], ConstraintSet.empty).
+
+  Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) :=
+    match p with
+    | primInt | primFloat =>
+     ∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None &
+             cdecl.(cst_universes) = Monomorphic_ctx]
+    | primArray =>
+      let s := Universe.make (Level.lvar 0) in
+      [/\ cdecl.(cst_type) = tImpl (tSort s) (tSort s), cdecl.(cst_body) = None &
+        cdecl.(cst_universes) = Polymorphic_ctx array_uctx]
+    end.
 
   (** A context of global declarations + global universe constraints,
       i.e. a global environment *)

common/theories/Primitive.v

@@ -6,8 +6,8 @@ Local Open Scope bs.
 
 Variant prim_tag :=
   | primInt
-  | primFloat.
-  (* | primArray. *)
+  | primFloat
+  | primArray.
 Derive NoConfusion EqDec for prim_tag.
 
 Definition string_of_prim_int (i:Uint63.int) : string :=

coq-metacoq.opam

@@ -24,7 +24,7 @@ depends: [
   "coq-metacoq-safechecker-plugin" {= version}
   "coq-metacoq-erasure-plugin" {= version}
   "coq-metacoq-translations" {= version}
-  "coq-metacoq-quotation" {= version}
+#  "coq-metacoq-quotation" {= version}
 ]
 build: [
   ["bash" "./configure.sh" ] {with-test}

erasure-plugin/_PluginProject.in

@@ -50,6 +50,8 @@ src/pCUICSafeReduce.ml
 src/pCUICSafeRetyping.ml
 src/pCUICSafeRetyping.mli
 
+src/ePrimitive.mli
+src/ePrimitive.ml
 src/eAst.ml
 src/eAst.mli
 src/eAstUtils.ml

erasure-plugin/src/metacoq_erasure_plugin.mlpack

@@ -39,6 +39,7 @@ PCUICUnivSubst
 PCUICSafeReduce
 PCUICSafeRetyping
 
+EPrimitive
 EAst
 EAstUtils
 ELiftSubst

erasure/_CoqProject.in

@@ -1,5 +1,6 @@
 -R theories MetaCoq.Erasure
 
+theories/EPrimitive.v
 theories/EAst.v
 theories/EAstUtils.v
 theories/EInduction.v

erasure/theories/EAst.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Universes.
-From MetaCoq.PCUIC Require Import PCUICPrimitive.
+From MetaCoq.Erasure Require Import EPrimitive.
 (** * Extracted terms
 
   These are the terms produced by extraction: compared to kernel terms,