From 6a74d2e648903e54300f276a024e396978629b30 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 17 Sep 2023 12:09:25 +0100
Subject: Add unhashed functions for comparisons

---
 src/hls/GiblePargen.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

(limited to 'src/hls/GiblePargen.v')

diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index e3cfcda..61b9819 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -411,11 +411,26 @@ Definition check_evaluability1 a b :=
     ) a
   ) b.
 
+Definition check_evaluability1_unhashed p p' a b :=
+  forallb (fun be =>
+    existsb (fun ae =>
+      resource_eq (fst ae) (fst be) 
+      && HN.beq_pred_expr_unhashed p p' (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 nil ae be
                                      && check_mutexcl HN.pred_Ht_dec ae
                                      && check_mutexcl HN.pred_Ht_dec be) a) b.
 
+Definition check_evaluability2_unhashed p p' a b :=
+  forallb (fun be => existsb (fun ae => HN.beq_pred_expr_unhashed p p' 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) =>
@@ -425,8 +440,19 @@ Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   | _, _ => false
   end.
 
+Definition schedule_oracle_unhashed (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_unhashed nil bb' bbt' && empty_trees bb bbt
+      && check_evaluability1_unhashed bb'.(forest_preds) bbt'.(forest_preds) reg_expr reg_expr_t
+      && check_evaluability2_unhashed bb'.(forest_preds) bbt'.(forest_preds) m_expr m_expr_t
+  | _, _ => false
+  end.
+
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
+Definition check_scheduled_trees_unhashed := beq2 schedule_oracle_unhashed.
+
 Ltac solve_scheduled_trees_correct :=
   intros; unfold check_scheduled_trees in *;
   match goal with
@@ -468,7 +494,25 @@ Definition transl_function (f: GibleSeq.function)
     Err.Error
       (Err.msg "GiblePargen: Could not prove the blocks equivalent.").
 
+Definition transl_function_unhashed (f: GibleSeq.function)
+  : Err.res GiblePar.function :=
+  let tfcode := fn_code (schedule f) in
+  if check_scheduled_trees_unhashed f.(GibleSeq.fn_code) tfcode then
+    Err.OK (mkfunction f.(GibleSeq.fn_sig)
+                          f.(GibleSeq.fn_params)
+                          f.(GibleSeq.fn_stacksize)
+                          tfcode
+                          f.(GibleSeq.fn_entrypoint))
+  else
+    Err.Error
+      (Err.msg "GiblePargen: Could not prove the blocks equivalent.").
+
 Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : GibleSeq.program) : Err.res GiblePar.program :=
   transform_partial_program transl_fundef p.
+
+Definition transl_fundef_unhashed := transf_partial_fundef transl_function_unhashed.
+
+Definition transl_program_unhashed (p : GibleSeq.program) : Err.res GiblePar.program :=
+  transform_partial_program transl_fundef_unhashed p.
-- 
cgit