From 0a44da6a7037d9eb270386eeef4f929177c4ec0d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 27 May 2022 01:05:32 +0100
Subject: Rewrite a lot fixing scheduling of Gible

---
 src/hls/GibleSeq.v | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

(limited to 'src/hls/GibleSeq.v')

diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index 1ba28bc..9444f28 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -36,13 +36,13 @@ RTLBlock
 ========
 |*)
 
-Module BB <: BlockType.
+Module SeqBB <: BlockType.
 
   Definition t := list instr.
 
-  Section RELSEM.
+  Definition foldl {A: Type}: (A -> instr -> A) -> t -> A -> A := @fold_left A instr.
 
-    Context {A B: Type} (ge: Genv.t A B).
+  Definition length : t -> nat := @length instr.
 
 (*|
 Instruction list step
@@ -56,16 +56,9 @@ This is simply using the high-level function ``step_list``, which is a general
 function that can execute lists of things, given their execution rule.
 |*)
 
-    Definition step := step_list (step_instr ge).
-
-  End RELSEM.
-
-  Definition max_reg (m : positive) (n: node) (i : t) : positive :=
-    fold_left max_reg_instr i m.
-
-  Definition length : t -> nat := @length instr.
+  Definition step {A B: Type} (ge: Genv.t A B) := step_list (step_instr ge).
 
-End BB.
+End SeqBB.
 
-Module GibleSeq := Gible(BB).
+Module GibleSeq := Gible(SeqBB).
 Export GibleSeq.
-- 
cgit