Update Coq version to 8.14.1

7 files changed, 65 insertions, 86 deletions

diff --git a/Makefile b/Makefile
index 9c40941..218598a 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ ifeq ($(UNAME_S),Darwin)
 	ARCH := verilog-macosx
 endif
 
-COMPCERTRECDIRS := lib common verilog backend cfrontend driver exportclight cparser
+COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
 
 COQINCLUDES := -R src/common vericert.common \
                -R src/extraction vericert.extraction \
diff --git a/default.nix b/default.nix
index eabd3d3..e3ce09b 100644
--- a/default.nix
+++ b/default.nix
@@ -1,7 +1,7 @@
-with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {};
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/00197eff36bb8f7dd7f53a59f730e1fd8e11b1f4.tar.gz") {};
 let
-  ncoq = coq_8_13;
-  ncoqPackages = coqPackages_8_13;
+  ncoq = coq_8_14;
+  ncoqPackages = coqPackages_8_14;
 in
 stdenv.mkDerivation {
   name = "vericert";
@@ -11,12 +11,6 @@ stdenv.mkDerivation {
                   ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
                   ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin
                   ncoq.ocamlPackages.menhirLib
-
-                  ncoqPackages.serapi
-                  python3 python3Packages.docutils python3Packages.pygments
-                  python3Packages.dominate
-                  python3Packages.pelican
-                  python3Packages.alectryon
                 ];
 
   enableParallelBuilding = true;
diff --git a/lib/CompCert b/lib/CompCert
-Subproject 1daf96cdca4d828c333cea5c9a314ef86134298
+Subproject 4f467596f8674f5f4fbf84a793cb8fcfc35a44a
diff --git a/src/common/Maps.v b/src/common/Maps.v
index f0f264d..13ca276 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -17,7 +17,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Set Implicit Arguments.
+(*Set Implicit Arguments.
 
 Require Export compcert.lib.Maps.
 
@@ -62,3 +62,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m
 Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f).
 
 End PTree.
+*)
diff --git a/src/common/Show.v b/src/common/Show.v
index 4c66725..20c07e7 100644
--- a/src/common/Show.v
+++ b/src/common/Show.v
@@ -1,4 +1,4 @@
-(* 
+(*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -24,15 +24,11 @@ From Coq Require Import
 
 Local Open Scope string.
 
-Class Show A : Type :=
-  {
-  show : A -> string
-  }.
+Class Show A : Type := { show : A -> string }.
 
+#[export]
 Instance showBool : Show bool :=
-  {
-  show := fun b:bool => if b then "true" else "false"
-  }.
+  { show := fun b:bool => if b then "true" else "false" }.
 
 Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
   let d := match n mod 10 with
@@ -52,17 +48,11 @@ Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
 Definition string_of_nat (n : nat) : string :=
   string_of_nat_aux n n "".
 
-Instance showNat : Show nat :=
-  {
-  show := string_of_nat
-  }.
+#[export]
+Instance showNat : Show nat := { show := string_of_nat }.
 
-Instance showZ : Show Z :=
-  {
-  show a := show (Z.to_nat a)
-  }.
+#[export]
+Instance showZ : Show Z := { show a := show (Z.to_nat a) }.
 
-Instance showPositive : Show positive :=
-  {
-  show a := show (Zpos a)
-  }.
+#[export]
+Instance showPositive : Show positive := { show a := show (Zpos a) }.
diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v
index 62ca54d..3a27cc6 100644
--- a/src/common/ZExtra.v
+++ b/src/common/ZExtra.v
@@ -45,12 +45,6 @@ Proof.
   - apply Z.mod_divide; assumption.
 Qed.
 
-Lemma mod_0_r: forall (m: Z),
-    m mod 0 = 0.
-Proof.
-  intros. destruct m; reflexivity.
-Qed.
-
 Lemma sub_mod_0: forall (a b m: Z),
     a mod m = 0 ->
     b mod m = 0 ->
@@ -89,18 +83,6 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma mod_pow2_same_cases: forall a n,
-    a mod 2 ^ n = a ->
-    2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n.
-Proof.
-  intros.
-  assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C].
-  - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto.
-  - right.
-    rewrite <- H. apply Z.mod_pos_bound.
-    apply Z.pow_pos_nonneg; lia.
-Qed.
-
 Lemma mod_pow2_same_bounds: forall a n,
     a mod 2 ^ n = a ->
     0 <= n ->
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 8dbc6b2..10bd8eb 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -42,63 +42,75 @@ Module AssocMapExt.
       | Some v => v
       end.
 
-    Fixpoint merge (m1 m2 : t A) : t A :=
-      match m1, m2 with
-      | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2)
-      | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2)
-      | Leaf, _ => m2
-      | _, _ => m1
+    Definition merge_atom (new : option A) (old : option A) : option A :=
+      match new, old with
+      | Some _, _ => new
+      | _, _ => old
       end.
 
+    Definition merge (m1 m2 : t A) : t A :=
+      PTree.combine merge_atom m1 m2.
+
     Lemma merge_base_1 :
-      forall am,
-      merge (empty A) am = am.
-    Proof. auto. Qed.
+      forall am x,
+      (merge (empty A) am) ! x = am ! x.
+    Proof using.
+      unfold merge; intros.
+      rewrite PTree.gcombine; eauto.
+    Qed.
 
     Lemma merge_base_2 :
-      forall am,
-      merge am (empty A) = am.
-    Proof.
-      unfold merge.
-      destruct am; trivial.
-      destruct o; trivial.
+      forall am x,
+      (merge am (empty A)) ! x = am ! x.
+    Proof using.
+      unfold merge; intros.
+      rewrite PTree.gcombine; eauto.
+      cbv [merge_atom]. destruct_match; crush.
     Qed.
 
     Lemma merge_add_assoc :
-      forall r am am' v,
-      merge (set r v am) am' = set r v (merge am am').
-    Proof.
-      induction r; intros; destruct am; destruct am'; try (destruct o); simpl;
-        try rewrite IHr; try reflexivity.
+      forall r am am' v x,
+      (merge (set r v am) am') ! x = (set r v (merge am am')) ! x.
+    Proof using.
+      unfold merge. intros; rewrite PTree.gcombine by auto.
+      unfold merge_atom. destruct_match.
+      destruct (peq r x); subst.
+      rewrite PTree.gss in Heqo. inv Heqo. rewrite PTree.gss. auto.
+      rewrite PTree.gso in Heqo by auto. rewrite PTree.gso by auto.
+      rewrite PTree.gcombine by auto. rewrite Heqo. auto.
+      destruct (peq r x); subst.
+      rewrite PTree.gss in Heqo. inv Heqo.
+      rewrite PTree.gso in Heqo by auto. rewrite PTree.gso by auto.
+      rewrite PTree.gcombine by auto. rewrite Heqo. auto.
     Qed.
 
     Lemma merge_correct_1 :
       forall am bm k v,
-      get k am = Some v ->
-      get k (merge am bm) = Some v.
-    Proof.
-      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
-        try rewrite gempty in H; try discriminate; try assumption; auto.
+      am ! k = Some v ->
+      (merge am bm) ! k = Some v.
+    Proof using.
+      unfold merge; intros. rewrite PTree.gcombine by auto.
+      rewrite H; auto.
     Qed.
 
     Lemma merge_correct_2 :
       forall am bm k v,
-      get k am = None ->
-      get k bm = Some v ->
-      get k (merge am bm) = Some v.
-    Proof.
-      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
-        try rewrite gempty in H; try discriminate; try assumption; auto.
+      am ! k = None ->
+      bm ! k = Some v ->
+      (merge am bm) ! k = Some v.
+    Proof using.
+      unfold merge; intros. rewrite PTree.gcombine by auto.
+      rewrite H. rewrite H0. auto.
     Qed.
 
     Lemma merge_correct_3 :
       forall am bm k,
-      get k am = None ->
-      get k bm = None ->
-      get k (merge am bm) = None.
-    Proof.
-      induction am; intros; destruct k; destruct bm; try (destruct o); simpl;
-        try rewrite gempty in H; try discriminate; try assumption; auto.
+      am ! k = None ->
+      bm ! k = None ->
+      (merge am bm) ! k = None.
+    Proof using.
+      unfold merge; intros. rewrite PTree.gcombine by auto.
+      rewrite H. rewrite H0. auto.
     Qed.
 
     Definition merge_fold (am bm : t A) : t A :=