From 489b93c3e257e37f45c1f0eafeff950b97249c3f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 11 Jan 2021 18:45:18 +0000 Subject: Improve definition of forest for infinite registers --- src/hls/Scheduleoracle.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'src/hls/Scheduleoracle.v') diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v index 785c1ef..2c60e96 100644 --- a/src/hls/Scheduleoracle.v +++ b/src/hls/Scheduleoracle.v @@ -185,14 +185,20 @@ Using IMap we can create a map from resources to any other type, as resources ca identified as positive numbers. |*) -Module Rmap := Maps.IMap(R_indexed). +Module Rtree := Maps.ITree(R_indexed). -Definition forest : Type := Rmap.t expression. +Definition forest : Type := Rtree.t expression. Definition regset := Registers.Regmap.t val. -Notation "a # b" := (Rmap.get b a) (at level 1). -Notation "a # b <- c" := (Rmap.set b c a) (at level 1, b at next level). +Definition get_forest v f := + match Rtree.get v f with + | None => Ebase v + | Some v' => v' + end. + +Notation "a # b" := (get_forest b a) (at level 1). +Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). Record sem_state := mk_sem_state { sem_state_stackp : val; -- cgit