From 9434e9223a67ce2d38e1f1de4e3d8129552ce4cc Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 11 Nov 2021 12:29:50 +0000
Subject: Add simplify operation and simplify IfConversion

---
 src/hls/IfConversion.v |  6 ++----
 src/hls/Predicate.v    | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 4 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 7221c28..b397d43 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -105,10 +105,8 @@ Definition find_blocks_with_cond (c: code) : list (node * bblock) :=
               ) (PTree.elements c).
 
 Definition if_convert_code (p: nat * code) (nb: node * bblock) :=
-  let (n, bb) := nb in
-  let (p', c) := p in
-  let nbb := if_convert_block c (Pos.of_nat p') bb in
-  (S p', PTree.set n nbb c).
+  let nbb := if_convert_block (snd p) (Pos.of_nat (fst p)) (snd nb) in
+  (S (fst p), PTree.set (fst nb) nbb (snd p)).
 
 Definition transf_function (f: function) : function :=
   let (_, c) := List.fold_left if_convert_code
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index dc70010..a2b5400 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -443,3 +443,61 @@ Proof.
   simplify. repeat rewrite negate_correct. rewrite H0. rewrite H.
   auto.
 Qed.
+
+Definition simplify' (p: pred_op) :=
+  match p with
+  | A ∧ T => A
+  | T ∧ A => A
+  | _ ∧ ⟂ => ⟂
+  | ⟂ ∧ _ => ⟂
+  | _ ∨ T => T
+  | T ∨ _ => T
+  | A ∨ ⟂ => A
+  | ⟂ ∨ A => A
+  | A => A
+  end.
+
+Lemma pred_op_dec :
+  forall p1 p2: pred_op,
+  { p1 = p2 } + { p1 <> p2 }.
+Proof. pose proof Pos.eq_dec. repeat decide equality. Qed.
+
+Fixpoint simplify (p: pred_op) :=
+  match p with
+  | A ∧ B =>
+    let A' := simplify A in
+    let B' := simplify B in
+    simplify' (A' ∧ B')
+  | A ∨ B =>
+    let A' := simplify A in
+    let B' := simplify B in
+    simplify' (A' ∨ B')
+  | T => T
+  | ⟂ => ⟂
+  | Plit a => Plit a
+  end.
+
+Lemma simplify'_correct :
+  forall h a,
+    sat_predicate (simplify' h) a = sat_predicate h a.
+Proof.
+  destruct h; crush; repeat destruct_match; crush;
+  solve [rewrite andb_true_r; auto | rewrite orb_false_r; auto].
+Qed.
+
+Lemma simplify_correct :
+  forall h a,
+    sat_predicate (simplify h) a = sat_predicate h a.
+Proof.
+  Local Opaque simplify'.
+  induction h; crush.
+  - replace (sat_predicate h1 a && sat_predicate h2 a)
+      with (sat_predicate (simplify h1) a && sat_predicate (simplify h2) a)
+      by crush.
+    rewrite simplify'_correct. crush.
+  - replace (sat_predicate h1 a || sat_predicate h2 a)
+      with (sat_predicate (simplify h1) a || sat_predicate (simplify h2) a)
+      by crush.
+    rewrite simplify'_correct. crush.
+    Local Transparent simplify'.
+Qed.
-- 
cgit