Revert changes relating to instance generation

Revert "Add todo for missing logic around instantiations"
This reverts commit 303a45374643f75698c61f062899973d2c297831.

Revert "Add wires and use them for output of instances"
This reverts commit a72f26319dabca414a2b576424b9f72afaca161c.

Revert "Separate HTL instantiations from Verilog ones"
This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047.

Revert "Translate instantiations from HTL to verilog"
This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d.

Revert "Print instantiations in HTL output"
This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e.

Revert "Add a field in HTL modules for instances"
This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502.

Revert "Generate (invalid) module instantiations for calls"
This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.

1 files changed, 6 insertions, 11 deletions

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 67b3648..541f9fa 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -167,12 +167,12 @@ Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st stk stk_len m start rst clk insts scldecls arrdecls wf,
+    forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf,
       m = (mkmodule f.(RTL.fn_params)
                         data
                         control
                         f.(RTL.fn_entrypoint)
-                        st stk stk_len fin rtrn start rst clk insts scldecls arrdecls wf) ->
+                        st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) ->
       (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
                tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) ->
       stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) ->
@@ -444,10 +444,10 @@ Proof.
   - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ.
     apply declare_reg_freshreg_trans in EQ1. congruence.
   - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence.
-  (* - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. *)
-  (*   congruence. *)
+  - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0.
+    congruence.
   (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*)
-Admitted.
+Qed.
 Hint Resolve transf_instr_freshreg_trans : htlspec.
 
 Lemma collect_trans_instr_freshreg_trans :
@@ -509,7 +509,6 @@ Lemma iter_expand_instr_spec :
                       c!pc = Some instr ->
                       tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack).
 Proof.
-(* FIXME Broken by mpardalos
   induction l; simpl; intros; try contradiction.
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   destruct (peq pc pc1).
@@ -578,8 +577,7 @@ Proof.
     destruct H2. inversion H2. subst. contradiction.
     intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
     destruct H2. inv H2. contradiction. assumption. assumption.
-*)
-Admitted.
+Qed.
 Hint Resolve iter_expand_instr_spec : htlspec.
 
 Lemma create_arr_inv : forall w x y z a b c d,
@@ -616,9 +614,7 @@ Proof.
     monadInv Heqr.
 
   repeat unfold_match EQ9. monadInv EQ9.
-Admitted.
 
-(* FIXME Broken by @mpardalos
   (* TODO: We should be able to fold this into the automation. *)
   pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5.
   pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL.
@@ -643,4 +639,3 @@ Admitted.
   eapply iter_expand_instr_spec; eauto with htlspec.
   apply PTree.elements_complete.
 Qed.
-*)