From 178a7c4781c96857fe0a33c777da83e769516152 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 11 Jul 2021 15:59:21 +0200
Subject: Remove unnecessary files and proofs

---
 src/hls/HTLPargen.v      | 5 +++--
 src/hls/RTLBlockInstr.v  | 6 +++---
 src/hls/RTLPargen.v      | 7 ++++---
 src/hls/RTLPargenproof.v | 3 ++-
 4 files changed, 12 insertions(+), 9 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index eda597a..9e1f156 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -643,7 +643,7 @@ Definition add_control_instr_force_state_incr :
        (AssocMap.set n st s.(st_controllogic))).
 Abort.
 
-Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
+(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
   fun s =>
     OK tt (mkstate
       s.(st_st)
@@ -708,7 +708,7 @@ Lemma create_new_state_state_incr:
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
-Admitted.
+Abort.
 
 Definition create_new_state (p: node): mon node :=
   fun s => OK s.(st_freshstate)
@@ -876,3 +876,4 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program :
   if main_is_internal p
   then transform_partial_program transl_fundef p
   else Errors.Error (Errors.msg "Main function is not Internal.").
+*)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 86f8eba..5e123a3 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -211,9 +211,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
   - apply orb_true_intro.
     apply satFormula_mult2 in H. inv H. apply i in H0. auto.
     apply i0 in H0. auto.
-Admitted.
+Abort.
 
-Definition sat_pred (bound: nat) (p: pred_op) :
+(*Definition sat_pred (bound: nat) (p: pred_op) :
   option ({al : alist | sat_predicate p (interp_alist al) = true}
           + {forall a : asgn, sat_predicate p a = false}).
   refine
@@ -243,7 +243,7 @@ Definition sat_pred_temp (bound: nat) (p: pred_op) :=
   match trans_pred_temp bound p with
   | Some fm => boundedSatSimple bound fm
   | None => None
-  end.
+  end.*)
 
 Inductive instr : Type :=
 | RBnop : instr
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index e2e9a90..5ad3f90 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -473,9 +473,9 @@ Lemma sems_det:
   forall v v' mv mv',
   (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\
   (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv').
-Proof. Admitted.
+Proof. Abort.
 
-Lemma sem_value_det:
+(*Lemma sem_value_det:
   forall A ge tge sp st f v v',
   ge_preserved ge tge ->
   sem_value A ge sp st f v ->
@@ -657,7 +657,7 @@ Lemma abstract_execution_correct:
     RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') ->
     exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m')
                  /\ regs_lessdef rs' rs''.
-Proof. Admitted.
+Proof. Abort.
 
 (*|
 Top-level functions
@@ -689,3 +689,4 @@ Definition transl_fundef := transf_partial_fundef transl_function_temp.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
+*)
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index eb7931e..a0c01fa 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import compcert.backend.Registers.
+(*Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
@@ -286,3 +286,4 @@ Section CORRECTNESS.
   Qed.*)
 
 End CORRECTNESS.
+*)
-- 
cgit