diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 15:45:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-07-11 16:25:09 +0100 |
| commit | 93117b6e766c25c5aeecdc20a963d5114fb91e59 (patch) | |
| tree | 60e77f4d09548b3fa077d96e7d0e26fd8b0ad1ef /src/hls/GiblePargen.v | |
| parent | 6cdb6490437b9e609afbf5e8749b24d31c02fce1 (diff) | |
| download | vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.tar.gz vericert-93117b6e766c25c5aeecdc20a963d5114fb91e59.zip | |
Add equivalence classes
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 23 |
1 files changed, 3 insertions, 20 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 3cf2401..57e067d 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -221,23 +221,6 @@ Definition is_initial_pred_and_notin (f: forest) (p: positive) (p_next: pred_op) | _ => false end. -Definition predicated_not_in {A} (p: Gible.predicate) (l: predicated A): bool := - NE.fold_right (fun (a: pred_op * A) (b: bool) => - b && negb (predin peq p (fst a)) - ) true l. - -Definition predicated_not_in_pred_expr (p: Gible.predicate) (tree: RTree.t pred_expr) := - PTree.fold (fun b _ a => - b && predicated_not_in p a - ) tree true. - -Definition predicated_not_in_pred_eexpr (p: Gible.predicate) (l: pred_eexpr) := - predicated_not_in p l. - -Definition predicated_not_in_forest (p: Gible.predicate) (f: forest) := - predicated_not_in_pred_expr p f.(forest_regs) - && predicated_not_in p f.(forest_exit). - Definition pred_expr_dec: forall a b: pred_op * pred_expression, {a = b} + {a <> b}. Proof. intros. destruct a, b. @@ -422,21 +405,21 @@ Definition check_evaluability1 a b := forallb (fun be => existsb (fun ae => resource_eq (fst ae) (fst be) - && HN.beq_pred_expr (snd ae) (snd be) + && HN.beq_pred_expr nil (snd ae) (snd be) && check_mutexcl HN.pred_Ht_dec (snd ae) && check_mutexcl HN.pred_Ht_dec (snd be) ) a ) b. Definition check_evaluability2 a b := - forallb (fun be => existsb (fun ae => HN.beq_pred_expr ae be + forallb (fun be => existsb (fun ae => HN.beq_pred_expr nil ae be && check_mutexcl HN.pred_Ht_dec ae && check_mutexcl HN.pred_Ht_dec be) a) b. Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool := match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) => - check bb' bbt' && empty_trees bb bbt + check nil bb' bbt' && empty_trees bb bbt && check_evaluability1 reg_expr reg_expr_t && check_evaluability2 m_expr m_expr_t | _, _ => false |