From 3c33ec31c5a8575c705c7d54de8a02b1f0bbbdc5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Aug 2022 08:45:04 +0100 Subject: Add forest type --- src/hls/Abstr.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 20ba4fa..9c62bde 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -144,11 +144,11 @@ Variant exit_expression : Type := Definition pred_op := @Predicate.pred_op positive. Definition predicate := positive. -Definition apredicated A := NE.non_empty (apred_op * A). Definition predicated A := NE.non_empty (pred_op * A). -Definition apred_expr := apredicated expression. Definition pred_expr := predicated expression. +Definition pred_pexpr := predicated pred_expression. +Definition pred_eexpr := predicated exit_expression. (*| Using ``IMap`` we can create a map from resources to any other type, as @@ -157,7 +157,12 @@ resources can be uniquely identified as positive numbers. Module Rtree := ITree(R_indexed). -Definition forest : Type := Rtree.t apred_expr. +Record forest : Type := + mk_forest { + forest_regs : Rtree.t pred_expr; + forest_preds : PTree.t pred_pexpr; + forest_exit : pred_eexpr + }. Definition get_forest v (f: forest) := match Rtree.get v f with -- cgit