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.

3 files changed, 41 insertions, 155 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 8e060e4..68e0293 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -16,9 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import List.
-Import ListNotations.
-
 From compcert Require Import Maps.
 From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
@@ -34,9 +31,8 @@ Record state: Type := mkstate {
   st_st : reg;
   st_freshreg: reg;
   st_freshstate: node;
-  st_scldecls: AssocMap.t scl_decl;
+  st_scldecls: AssocMap.t (option io * scl_decl);
   st_arrdecls: AssocMap.t (option io * arr_decl);
-  st_insts: AssocMap.t instantiation;
   st_datapath: datapath;
   st_controllogic: controllogic;
 }.
@@ -45,9 +41,8 @@ Definition init_state (st : reg) : state :=
   mkstate st
           1%positive
           1%positive
-          (AssocMap.empty scl_decl)
+          (AssocMap.empty (option io * scl_decl))
           (AssocMap.empty (option io * arr_decl))
-          (AssocMap.empty instantiation)
           (AssocMap.empty stmnt)
           (AssocMap.empty stmnt).
 
@@ -64,8 +59,6 @@ Module HTLState <: State.
         (forall n,
             s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
         (forall n,
-            s1.(st_insts)!n = None \/ s2.(st_insts)!n = s1.(st_insts)!n) ->
-        (forall n,
             s1.(st_controllogic)!n = None
             \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
         st_incr s1 s2.
@@ -80,9 +73,8 @@ Module HTLState <: State.
     forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
   Proof.
     intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.
-    - destruct H4 with n; destruct H9 with n; intuition congruence.
-    - destruct H5 with n; destruct H10 with n; intuition congruence.
-    - destruct H6 with n; destruct H11 with n; intuition congruence.
+    - destruct H4 with n; destruct H8 with n; intuition congruence.
+    - destruct H5 with n; destruct H9 with n; intuition congruence.
   Qed.
 
 End HTLState.
@@ -124,7 +116,6 @@ Lemma add_instr_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       s.(st_insts)
        (AssocMap.set n st s.(st_datapath))
        (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
 Proof.
@@ -140,9 +131,8 @@ Lemma declare_reg_state_incr :
        s.(st_st)
        s.(st_freshreg)
        s.(st_freshstate)
-       (AssocMap.set r (VScalar i sz) s.(st_scldecls))
+       (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
        s.(st_arrdecls)
-       s.(st_insts)
        s.(st_datapath)
        s.(st_controllogic)).
 Proof. auto with htlh. Qed.
@@ -152,9 +142,8 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
                 s.(st_st)
                 s.(st_freshreg)
                 s.(st_freshstate)
-                (AssocMap.set r (VScalar i sz) s.(st_scldecls))
+                (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
                 s.(st_arrdecls)
-                s.(st_insts)
                 s.(st_datapath)
                 s.(st_controllogic))
               (declare_reg_state_incr i s r sz).
@@ -169,7 +158,6 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
                (st_freshstate s)
                s.(st_scldecls)
                s.(st_arrdecls)
-               s.(st_insts)
                (AssocMap.set n st s.(st_datapath))
                (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
          (add_instr_state_incr s n n' st STM TRANS)
@@ -187,7 +175,6 @@ Lemma add_instr_skip_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       s.(st_insts)
        (AssocMap.set n st s.(st_datapath))
        (AssocMap.set n Vskip s.(st_controllogic))).
 Proof.
@@ -206,7 +193,6 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
                (st_freshstate s)
                s.(st_scldecls)
                s.(st_arrdecls)
-               s.(st_insts)
                (AssocMap.set n st s.(st_datapath))
                (AssocMap.set n Vskip s.(st_controllogic)))
          (add_instr_skip_state_incr s n st STM TRANS)
@@ -224,7 +210,6 @@ Lemma add_node_skip_state_incr :
        (st_freshstate s)
        s.(st_scldecls)
        s.(st_arrdecls)
-       s.(st_insts)
        (AssocMap.set n Vskip s.(st_datapath))
        (AssocMap.set n st s.(st_controllogic))).
 Proof.
@@ -243,52 +228,12 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit :=
                (st_freshstate s)
                s.(st_scldecls)
                s.(st_arrdecls)
-               s.(st_insts)
                (AssocMap.set n Vskip s.(st_datapath))
                (AssocMap.set n st s.(st_controllogic)))
          (add_node_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
 
-Fixpoint assocmap_nextavailable {A: Type} (m: AssocMap.t A) : positive :=
-  match m with
-  | AssocMap.Leaf => 1
-  | AssocMap.Node _ _ r => (assocmap_nextavailable r)~1
-  end.
-
-Theorem assocmap_nextavailable_correct : forall (A: Type) m, m!(@assocmap_nextavailable A m) = None.
-Proof. induction m; tauto. Qed.
-
-Lemma add_instance_state_incr :
-  forall s inst,
-    st_incr s
-      (mkstate
-        s.(st_st)
-        s.(st_freshreg)
-        s.(st_freshstate)
-        s.(st_scldecls)
-        s.(st_arrdecls)
-        (AssocMap.set (assocmap_nextavailable s.(st_insts)) inst s.(st_insts))
-        s.(st_datapath)
-        s.(st_controllogic)).
-Proof.
-Admitted.
-
-Definition add_instance (mod_name: ident) (args: list reg) (finished: reg) (dst: reg) : mon unit :=
-  fun s =>
-        let instname := assocmap_nextavailable s.(st_insts) in
-        let inst := HTL.HTLinstantiation mod_name instname args dst finished in
-        OK tt (mkstate
-              s.(st_st)
-              s.(st_freshreg)
-              s.(st_freshstate)
-              s.(st_scldecls)
-              s.(st_arrdecls)
-              (AssocMap.set instname inst s.(st_insts))
-              s.(st_datapath)
-              s.(st_controllogic))
-       (add_instance_state_incr s inst).
-
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -441,7 +386,6 @@ Lemma add_branch_instr_state_incr:
                 (st_freshstate s)
                 s.(st_scldecls)
                 s.(st_arrdecls)
-                s.(st_insts)
                 (AssocMap.set n Vskip (st_datapath s))
                 (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
 Proof.
@@ -460,7 +404,6 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                 (st_freshstate s)
                 s.(st_scldecls)
                 s.(st_arrdecls)
-                s.(st_insts)
                 (AssocMap.set n Vskip (st_datapath s))
                 (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
          (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
@@ -501,58 +444,6 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
-Lemma create_reg_state_incr:
-  forall s sz i,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         s.(st_insts)
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_reg (i : option io) (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_insts s)
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_reg_state_incr s sz i).
-
-Lemma create_wire_state_incr:
-  forall s sz,
-    st_incr s (mkstate
-         s.(st_st)
-         (Pos.succ (st_freshreg s))
-         (st_freshstate s)
-         (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls))
-         s.(st_arrdecls)
-         s.(st_insts)
-         (st_datapath s)
-         (st_controllogic s)).
-Proof. constructor; simpl; auto with htlh. Qed.
-
-Definition create_wire (sz : nat) : mon reg :=
-  fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
-                   s.(st_st)
-                   (Pos.succ r)
-                   (st_freshstate s)
-                   (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls))
-                   (st_arrdecls s)
-                   (st_insts s)
-                   (st_datapath s)
-                   (st_controllogic s))
-              (create_wire_state_incr s sz).
-
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
@@ -578,14 +469,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
         do dst <- translate_arr_access mem addr args stack;
         add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)
       else error (Errors.msg "State is larger than 2^32.")
-    | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
-    | Icall sig (inr fn) args dst n' =>
-      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        do finished <- create_wire 1;
-        do res <- create_wire 32;
-        (* TODO implement control and datapaths for instantiated module *)
-        add_instance fn args finished res
-      else error (Errors.msg "State is larger than 2^32.")
+    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
     | Icond cond args n1 n2 =>
@@ -607,6 +491,30 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     end
   end.
 
+Lemma create_reg_state_incr:
+  forall s sz i,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+         s.(st_arrdecls)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg (i : option io) (sz : nat) : mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))
+                   (st_arrdecls s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_reg_state_incr s sz i).
+
 Lemma create_arr_state_incr:
   forall s sz ln i,
     st_incr s (mkstate
@@ -615,7 +523,6 @@ Lemma create_arr_state_incr:
          (st_freshstate s)
          s.(st_scldecls)
          (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-         (st_insts s)
          (st_datapath s)
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
@@ -628,7 +535,6 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=
                    (st_freshstate s)
                    s.(st_scldecls)
                    (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))
-                   (st_insts s)
                    (st_datapath s)
                    (st_controllogic s))
               (create_arr_state_incr s sz ln i).
@@ -692,7 +598,6 @@ Definition transf_module (f: function) : mon module :=
            start
            rst
            clk
-           current_state.(st_insts)
            current_state.(st_scldecls)
            current_state.(st_arrdecls)
            (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))
@@ -705,9 +610,8 @@ Definition max_state (f: function) : state :=
   mkstate st
           (Pos.succ st)
           (Pos.succ (max_pc_function f))
-          (AssocMap.set st (VScalar None 32) (st_scldecls (init_state st)))
+          (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))
           (st_arrdecls (init_state st))
-          (st_insts (init_state st))
           (st_datapath (init_state st))
           (st_controllogic (init_state st)).
 
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.
-*)
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 07034cc..a0be0fa 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -16,9 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import List.
-Import ListNotations.
-
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST.
@@ -30,11 +27,8 @@ Definition transl_list_fun (a : node * Verilog.stmnt) :=
 
 Definition transl_list st := map transl_list_fun st.
 
-Definition scl_to_Vdecl_fun (a : reg * scl_decl) :=
-  match a with
-  | (r, (VScalar io sz)) => (Vdecl io r sz)
-  | (r, VWire sz) => (Vdeclwire r sz)
-  end.
+Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) :=
+  match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end.
 
 Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl.
 
@@ -43,12 +37,6 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) :=
 
 Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl.
 
-Definition inst_to_Vdecl_fun (m: HTL.module) (a: positive * HTL.instantiation) :=
-  match a with (_, HTLinstantiation mod_name inst_name args fin dst) =>
-               (Vinstancedecl mod_name inst_name ([mod_start m; mod_reset m; mod_clk m] ++ args ++ [dst;fin])) end.
-
-Definition inst_to_Vdecl (m: HTL.module) := map (inst_to_Vdecl_fun m).
-
 Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
@@ -58,8 +46,7 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
                                                (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
       :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
       :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
-                                               ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))
-                                               ++ inst_to_Vdecl m (AssocMap.elements m.(mod_insts))) in
+                          ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
   Verilog.mkmodule m.(mod_start)
                    m.(mod_reset)
                    m.(mod_clk)