diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-08-01 08:45:04 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-08-01 08:45:04 +0100 |
| commit | 3c33ec31c5a8575c705c7d54de8a02b1f0bbbdc5 (patch) | |
| tree | 7bb00b8805170588e7b37a0e9fd5c3916448cce0 | |
| parent | c0ef6778d1279f9733a57cb024bbc7d4f819eff5 (diff) | |
| download | vericert-3c33ec31c5a8575c705c7d54de8a02b1f0bbbdc5.tar.gz vericert-3c33ec31c5a8575c705c7d54de8a02b1f0bbbdc5.zip | |
Add forest type
| -rw-r--r-- | src/hls/Abstr.v | 11 |
1 files 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 |