diff options
Diffstat (limited to 'src/hls/GibleSeq.v')
-rw-r--r-- | src/hls/GibleSeq.v | 19 |
1 files changed, 6 insertions, 13 deletions
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. |