Fix imports to remove warnings when compiling

7 files changed, 101 insertions, 49 deletions

diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 51afed7..1d1b77f 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -17,8 +17,10 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From vericert Require Import Vericertlib ValueInt.
-From compcert Require Import Maps.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
 
 Definition reg := positive.
 
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index d1c901f..c8a0041 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -17,11 +17,20 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import FSets.FMapPositive.
-From vericert Require Import Vericertlib ValueInt AssocMap Array.
-From vericert Require Verilog.
-From compcert Require Events Globalenvs Smallstep Integers Values.
-From compcert Require Import Maps.
+Require Import Coq.FSets.FMapPositive.
+
+Require compcert.common.Events.
+Require compcert.common.Globalenvs.
+Require compcert.common.Smallstep.
+Require compcert.common.Values.
+Require compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
+Require vericert.hls.Verilog.
 
 (** The purpose of the hardware transfer language (HTL) is to create a more
 hardware-like layout that is still similar to the register transfer language
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 4c49828..f1e6b2a 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -17,10 +17,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Maps.
-From compcert Require Errors Globalenvs Integers.
-From compcert Require Import AST RTL.
-From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad.
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.lib.Maps.
+Require compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.common.AST.
+Require Import compcert.backend.RTL.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
@@ -557,8 +568,8 @@ Proof.
   rewrite PTree.gempty. congruence.
   (* inductive case *)
   intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
-  inv H2. xomega.
-  apply Ple_trans with a. auto. xomega.
+  inv H2. unfold Ple; lia.
+  apply Ple_trans with a. auto. unfold Ple; lia.
 Qed.
 
 Lemma max_pc_wf :
@@ -572,7 +583,7 @@ Proof.
   simplify. transitivity (Z.pos (max_pc_map m)); eauto.
 Qed.
 
-Definition transf_module (f: function) : mon module :=
+Definition transf_module (f: function) : mon HTL.module :=
   if stack_correct f.(fn_stacksize) then
     do fin <- create_reg (Some Voutput) 1;
     do rtrn <- create_reg (Some Voutput) 32;
@@ -586,7 +597,7 @@ Definition transf_module (f: function) : mon module :=
     match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,
           zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with
     | left LEDATA, left LECTRL =>
-        ret (mkmodule
+        ret (HTL.mkmodule
            f.(RTL.fn_params)
            current_state.(st_datapath)
            current_state.(st_controllogic)
@@ -616,7 +627,7 @@ Definition max_state (f: function) : state :=
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
 
-Definition transl_module (f : function) : Errors.res module :=
+Definition transl_module (f : function) : Errors.res HTL.module :=
   run_mon (max_state f) (transf_module f).
 
 Definition transl_fundef := transf_partial_fundef transl_module.
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 2bd1a2a..845b1d5 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -17,10 +17,20 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require RTL Op Maps Errors.
-From compcert Require Import Maps Integers.
-From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap.
-Require Import Lia.
+Require Import Coq.micromega.Lia.
+
+Require compcert.backend.RTL.
+Require compcert.common.Errors.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require compcert.verilog.Op.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.HTLgen.
+Require Import vericert.hls.AssocMap.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
 Hint Resolve Maps.PTree.elements_correct : htlspec.
diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v
index ea0c32e..7f1485a 100644
--- a/src/hls/Pipeline.v
+++ b/src/hls/Pipeline.v
@@ -1,7 +1,24 @@
-From compcert Require Import
-     Maps
-     AST
-     RTL.
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import compcert.lib.Maps.
+Require Import compcert.common.AST.
+Require Import compcert.backend.RTL.
 
 Parameter pipeline : function -> function.
 
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 6b3e9c3..889e104 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -16,13 +16,11 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require
-     RTL.
-From compcert Require Import
-     AST
-     Maps.
-From vericert Require Import
-     RTLBlock.
+Require compcert.backend.RTL.
+Require Import compcert.common.AST.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.hls.RTLBlock.
 
 Parameter partition : RTL.function -> Errors.res function.
 
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index a0be0fa..80c0669 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -16,10 +16,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Maps.
-From compcert Require Errors.
-From compcert Require Import AST.
-From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt.
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
 
 Definition transl_list_fun (a : node * Verilog.stmnt) :=
   let (n, stmnt) := a in
@@ -41,23 +46,23 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
   let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
-                                               (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
-                                               (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
-      :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
+      Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1)))
+                                               (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint))))
+                                               (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip)))
+      :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip))
       :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
-  Verilog.mkmodule m.(mod_start)
-                   m.(mod_reset)
-                   m.(mod_clk)
-                   m.(mod_finish)
-                   m.(mod_return)
-                   m.(mod_st)
-                   m.(mod_stk)
-                   m.(mod_stk_len)
-                   m.(mod_params)
+  Verilog.mkmodule m.(HTL.mod_start)
+                   m.(HTL.mod_reset)
+                   m.(HTL.mod_clk)
+                   m.(HTL.mod_finish)
+                   m.(HTL.mod_return)
+                   m.(HTL.mod_st)
+                   m.(HTL.mod_stk)
+                   m.(HTL.mod_stk_len)
+                   m.(HTL.mod_params)
                    body
-                   m.(mod_entrypoint).
+                   m.(HTL.mod_entrypoint).
 
 Definition transl_fundef := transf_fundef transl_module.