Remove unnecessary files and proofs

7 files changed, 19 insertions, 16 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 0706d79..aa5309a 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -93,7 +93,7 @@ let compile_c_file sourcename ifile ofile =
   end else begin
     let verilog =
       let translation = if !option_hls_schedule
-                        then Vericert.Compiler0.transf_hls_temp
+                        then Vericert.Compiler0.transf_hls
                         else Vericert.Compiler0.transf_hls
       in
       match translation csyntax with
diff --git a/src/Compiler.v b/src/Compiler.v
index 268f451..de29889 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -216,7 +216,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
 
 (* This is an unverified version of transf_hls with some experimental additions such as scheduling
 that aren't completed yet. *)
-Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
+(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   OK p
   @@@ SimplExpr.transl_program
   @@@ SimplLocals.transf_program
@@ -245,7 +245,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   @@@ RTLPargen.transl_program
   @@@ HTLPargen.transl_program
    @@ print print_HTL
-   @@ Veriloggen.transl_program.
+   @@ Veriloggen.transl_program.*)
 
 (*|
 Correctness Proof
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 00a1f00..6abe4e0 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
 Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline".
 Extract Constant RTLBlockgen.partition => "Partition.partition".
-Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".
+(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*)
 
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
@@ -187,11 +187,11 @@ Set Extraction AccessOpaque.
 Cd "src/extraction".
 Separate Extraction
          Verilog.module vericert.Compiler.transf_hls
-         vericert.Compiler.transf_hls_temp
-         RTLBlockgen.transl_program RTLBlockInstr.successors_instr
+(*         vericert.Compiler.transf_hls_temp*)
+(*         RTLBlockgen.transl_program RTLBlockInstr.successors_instr*)
          HTLgen.tbl_to_case_expr
          Pipeline.pipeline
-         RTLBlockInstr.sat_pred_temp
+(*         RTLBlockInstr.sat_pred_temp*)
          Verilog.stmnt_to_list
 
    Compiler.transf_c_program Compiler.transf_cminor_program
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.
+*)