From 0a44da6a7037d9eb270386eeef4f929177c4ec0d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 27 May 2022 01:05:32 +0100
Subject: Rewrite a lot fixing scheduling of Gible

---
 src/hls/RICtransf.v | 86 -----------------------------------------------------
 1 file changed, 86 deletions(-)
 delete mode 100644 src/hls/RICtransf.v

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

diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
deleted file mode 100644
index 886c23d..0000000
--- a/src/hls/RICtransf.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-Require Import compcert.common.AST.
-Require Import compcert.common.Errors.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.Predicate.
-
-(*|
-=====================
-Reverse If-Conversion
-=====================
-
-This transformation takes a scheduling RTLPar block and removes any predicates
-from it.  It can then be trivially transformed into linear code again.  It works
-by iteratively selecting a predicate, then creating a branch based on it and
-placing subsequent instructions in one branch or the other.
-|*)
-
-Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
-  match l with
-  | nil => None
-  | a :: l0 =>
-      match f a, existsb_val f l0 with
-      | _, Some v => Some v
-      | Some v, _ => Some v
-      | _, _ => None
-      end
-  end.
-
-Definition includes_setpred (bb: bb) :=
-  existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb.
-
-Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) :=
-  match bbc with
-  | (a, b) => if should_split then (a, i::b) else (i::a, b)
-  end.
-
-Fixpoint first_split (saw_pred: bool) (bb: list bb) :=
-  match bb with
-  | a :: b =>
-      match includes_setpred a with
-      | Some v =>
-          let (_, res) := first_split true b in
-          (Some v, add_bb saw_pred a res)
-      | _ =>
-          let (v, res) := first_split saw_pred b in
-          (v, add_bb saw_pred a res)
-      end
-  | nil => (None, (nil, nil))
-  end.
-
-Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb :=
-  match first_split false b with
-  | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
-  | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
-  end.
-
-Definition transf_function (f: function) : function := f.
-
-Definition transf_fundef (fd: fundef) : fundef :=
-  transf_fundef transf_function fd.
-
-Definition transf_program (p: program) : program :=
-  transform_program transf_fundef p.
-- 
cgit