Make externctrl application its own HTL pass

4 files changed, 229 insertions, 185 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 38a9d0e..ea3720a 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -61,6 +61,7 @@ Require Import compcert.lib.Coqlib.
 Require vericert.hls.Verilog.
 Require vericert.hls.Veriloggen.
 Require vericert.hls.Veriloggenproof.
+Require vericert.hls.ApplyExternctrl.
 Require vericert.hls.Renaming.
 Require vericert.hls.HTLgen.
 Require vericert.hls.RTLBlock.
@@ -194,6 +195,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
    @@ print (print_HTL 1)
   @@@ Renaming.transf_program
    @@ print (print_HTL 2)
+  @@@ ApplyExternctrl.transf_program
+   @@ print (print_HTL 3)
   @@@ Veriloggen.transl_program.
 
 Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
@@ -297,7 +300,7 @@ Proof.
   destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
   rewrite ! compose_print_identity in T.
   destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
-  unfold transf_backend, time in T. simpl in T. rewrite ! compose_print_identity in T.
+  unfold transf_backend, time in T. rewrite ! compose_print_identity in T.
   destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.
   set (p8 := Renumber.transf_program p7) in *.
   set (p9 := total_if Compopts.optim_constprop Constprop.transf_program p8) in *.
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
new file mode 100644
index 0000000..44c6b83
--- /dev/null
+++ b/src/hls/ApplyExternctrl.v
@@ -0,0 +1,180 @@
+Require Import compcert.common.Errors.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.Maps.
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.Verilog.
+
+Import ListNotations.
+
+Section APPLY_EXTERNCTRL.
+  Local Open Scope assocmap.
+  Local Open Scope error_monad_scope.
+
+  Variable prog : HTL.program.
+  Variable m : HTL.module.
+
+  Let modmap := prog_modmap prog.
+
+  Definition get_mod_signal (othermod : HTL.module) (signal : HTL.controlsignal) :=
+    match signal with
+    | ctrl_finish => OK (HTL.mod_finish othermod)
+    | ctrl_return => OK (HTL.mod_return othermod)
+    | ctrl_start => OK (HTL.mod_start othermod)
+    | ctrl_reset => OK (HTL.mod_reset othermod)
+    | ctrl_clk => OK (HTL.mod_clk othermod)
+    | ctrl_param idx =>
+      match List.nth_error (HTL.mod_params othermod) idx with
+      | Some r => OK r
+      | None => Error (msg "Module does not have nth parameter")
+      end
+    end.
+
+  Definition reg_apply_externctrl (r : Verilog.reg) : res reg :=
+    match (HTL.mod_externctrl m) ! r with
+    | None => OK r
+    | Some (m, signal) =>
+      match modmap ! m with
+      | None => Error (msg "Veriloggen: Could not find definition for called module")
+      | Some othermod => get_mod_signal othermod signal
+      end
+    end.
+
+  Fixpoint expr_apply_externctrl (expr : Verilog.expr) {struct expr} : res Verilog.expr :=
+    match expr with
+    | Vlit n =>
+      OK (Vlit n)
+    | Vvar r =>
+      do r' <- reg_apply_externctrl r;
+      OK (Vvar r')
+    | Vvari r e =>
+      do r' <- reg_apply_externctrl r;
+      do e' <- expr_apply_externctrl e;
+      OK (Vvari r e)
+    | Vrange r e1 e2 =>
+      do r' <- reg_apply_externctrl r;
+      do e1' <- expr_apply_externctrl e1;
+      do e2' <- expr_apply_externctrl e2;
+      OK (Vrange r' e1' e2')
+    | Vinputvar r =>
+      do r' <- reg_apply_externctrl r;
+      OK (Vinputvar r')
+    | Vbinop op e1 e2 =>
+      do e1' <- expr_apply_externctrl e1;
+      do e2' <- expr_apply_externctrl e2;
+      OK (Vbinop op e1' e2')
+    | Vunop op e =>
+      do e' <- expr_apply_externctrl e;
+      OK (Vunop op e')
+    | Vternary e1 e2 e3 =>
+      do e1' <- expr_apply_externctrl e1;
+      do e2' <- expr_apply_externctrl e2;
+      do e3' <- expr_apply_externctrl e3;
+      OK (Vternary e1' e2' e3')
+    end.
+
+  Definition mmap_option {A B} (f : A -> res B) (opt : option A) : res (option B) :=
+    match opt with
+    | None => OK None
+    | Some a => do a' <- f a; OK (Some a')
+    end.
+
+  Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) :=
+    fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) :=
+      match cs with
+      | nil => OK nil
+      | (c_e, c_s) :: tl =>
+        do c_e' <- expr_apply_externctrl c_e;
+        do c_s' <- stmnt_apply_externctrl_ c_s;
+        do tl' <- cases_apply_externctrl tl;
+        OK ((c_e', c_s') :: tl')
+      end.
+
+  Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt :=
+    match stmnt with
+    | Vskip => OK Vskip
+    | Vseq s1 s2 =>
+      do s1' <- stmnt_apply_externctrl s1;
+      do s2' <- stmnt_apply_externctrl s2;
+      OK (Vseq s1' s2')
+    | Vcond e s1 s2 =>
+      do e' <- expr_apply_externctrl e;
+      do s1' <- stmnt_apply_externctrl s1;
+      do s2' <- stmnt_apply_externctrl s2;
+      OK (Vcond e' s1' s2')
+    | Vcase e cases def =>
+      do e' <- expr_apply_externctrl e;
+      do cases' <- cases_apply_externctrl_ stmnt_apply_externctrl cases;
+      do def' <- mmap_option (fun x => stmnt_apply_externctrl x) def;
+      OK (Vcase e' cases' def')
+    | Vblock e1 e2 =>
+      do e1' <- expr_apply_externctrl e1;
+      do e2' <- expr_apply_externctrl e2;
+      OK (Vblock e1' e2')
+    | Vnonblock e1 e2 =>
+      do e1' <- expr_apply_externctrl e1;
+      do e2' <- expr_apply_externctrl e2;
+      OK (Vnonblock e1' e2')
+    end.
+
+  (* Unused. Defined for completeness *)
+  Definition cases_apply_externctrl := cases_apply_externctrl_ stmnt_apply_externctrl.
+
+  Fixpoint xassocmap_apply_externctrl {A} (regmap : list (reg * A)) : res (list (reg * A)) :=
+    match regmap with
+    | nil => OK nil
+    | (r, v) :: l =>
+      do r' <- reg_apply_externctrl r;
+      do l' <- xassocmap_apply_externctrl l;
+      OK ((r', v) :: l')
+    end.
+
+  Definition assocmap_apply_externctrl {A} (regmap : AssocMap.t A) : res (AssocMap.t A) :=
+    do l <- xassocmap_apply_externctrl (AssocMap.elements regmap);
+    OK (AssocMap_Properties.of_list l).
+
+  Definition module_apply_externctrl : res HTL.module :=
+    do mod_start' <- reg_apply_externctrl (HTL.mod_start m);
+    do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m);
+    do mod_clk' <- reg_apply_externctrl (HTL.mod_clk m);
+    do mod_finish' <- reg_apply_externctrl (HTL.mod_finish m);
+    do mod_return' <- reg_apply_externctrl (HTL.mod_return m);
+    do mod_st' <- reg_apply_externctrl (HTL.mod_st m);
+    do mod_stk' <- reg_apply_externctrl (HTL.mod_stk m);
+    do mod_params' <- mmap reg_apply_externctrl (HTL.mod_params m);
+    do mod_controllogic' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_controllogic m);
+    do mod_datapath' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_datapath m);
+
+    do mod_scldecls' <- assocmap_apply_externctrl (HTL.mod_scldecls m);
+    do mod_arrdecls' <- assocmap_apply_externctrl (HTL.mod_arrdecls m);
+    do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m);
+
+    match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned,
+          zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with
+    | left LEDATA, left LECTRL =>
+      OK (HTL.mkmodule
+             mod_params'
+             mod_datapath'
+             mod_controllogic'
+             (HTL.mod_entrypoint m)
+             mod_st'
+             mod_stk'
+             (HTL.mod_stk_len m)
+             mod_finish'
+             mod_return'
+             mod_start'
+             mod_reset'
+             mod_clk'
+             mod_scldecls'
+             mod_arrdecls'
+             mod_externctrl'
+             (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA)))
+    | _, _ => Error (Errors.msg "More than 2^32 states.")
+    end.
+End APPLY_EXTERNCTRL.
+
+Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog).
+Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog.
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 1eb86e1..8d51750 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -105,6 +105,26 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
 Definition empty_stack (m : module) : Verilog.assocmap_arr :=
   (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)).
 
+
+Definition prog_modmap (p : HTL.program) :=
+  PTree_Properties.of_list (Option.map_option
+                               (fun a => match a with
+                                      | (ident, (AST.Gfun (AST.Internal f))) => Some (ident, f)
+                                      | _ => None
+                                      end)
+                               (AST.prog_defs p)).
+
+Lemma max_pc_wf :
+  forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
+            @map_well_formed T m.
+Proof.
+  unfold map_well_formed. intros.
+  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
+  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
+  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
+  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
+Qed.
+
 (** * Operational Semantics *)
 
 Definition genv := Globalenvs.Genv.t fundef unit.
@@ -247,14 +267,3 @@ Inductive final_state : state -> Integers.int -> Prop :=
 Definition semantics (m : program) :=
   Smallstep.Semantics step (initial_state m) final_state
                       (Globalenvs.Genv.globalenv m).
-
-Lemma max_pc_wf :
-  forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned ->
-            @map_well_formed T m.
-Proof.
-  unfold map_well_formed. intros.
-  exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.
-  apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.
-  unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.
-  simplify. transitivity (Z.pos (max_pc_map m)); eauto.
-Qed.
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index 1438e95..1f0938b 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -29,152 +29,17 @@ Require Import vericert.hls.ValueInt.
 Require Import vericert.hls.Verilog.
 Import ListNotations.
 
-Section APPLY_MAPPING.
-  Local Open Scope assocmap.
-  Local Open Scope error_monad_scope.
-
-  Variable externctrl : AssocMap.t (ident * controlsignal).
-  Variable modmap : PTree.t HTL.module.
-
-  Definition get_mod_signal (m : HTL.module) (signal : HTL.controlsignal) :=
-    match signal with
-    | ctrl_finish => OK (HTL.mod_finish m)
-    | ctrl_return => OK (HTL.mod_return m)
-    | ctrl_start => OK (HTL.mod_start m)
-    | ctrl_reset => OK (HTL.mod_reset m)
-    | ctrl_clk => OK (HTL.mod_clk m)
-    | ctrl_param idx =>
-      match List.nth_error (HTL.mod_params m) idx with
-      | Some r => OK r
-      | None => Error (msg "Module does not have nth parameter")
-      end
-    end.
-
-  Definition reg_apply_map (r : Verilog.reg) : res reg :=
-    match externctrl ! r with
-    | None => OK r
-    | Some (m, signal) =>
-      match modmap ! m with
-      | None => Error (msg "Veriloggen: Could not find definition for called module")
-      | Some othermod => get_mod_signal othermod signal
-      end
-    end.
-
-  Fixpoint expr_apply_map (expr : Verilog.expr) {struct expr} : res Verilog.expr :=
-    match expr with
-    | Vlit n =>
-      OK (Vlit n)
-    | Vvar r =>
-      do r' <- reg_apply_map r;
-      OK (Vvar r')
-    | Vvari r e =>
-      do r' <- reg_apply_map r;
-      do e' <- expr_apply_map e;
-      OK (Vvari r e)
-    | Vrange r e1 e2 =>
-      do r' <- reg_apply_map r;
-      do e1' <- expr_apply_map e1;
-      do e2' <- expr_apply_map e2;
-      OK (Vrange r' e1' e2')
-    | Vinputvar r =>
-      do r' <- reg_apply_map r;
-      OK (Vinputvar r')
-    | Vbinop op e1 e2 =>
-      do e1' <- expr_apply_map e1;
-      do e2' <- expr_apply_map e2;
-      OK (Vbinop op e1' e2')
-    | Vunop op e =>
-      do e' <- expr_apply_map e;
-      OK (Vunop op e')
-    | Vternary e1 e2 e3 =>
-      do e1' <- expr_apply_map e1;
-      do e2' <- expr_apply_map e2;
-      do e3' <- expr_apply_map e3;
-      OK (Vternary e1' e2' e3')
-    end.
-
-  Definition mmap_option {A B} (f : A -> res B) (opt : option A) : res (option B) :=
-    match opt with
-    | None => OK None
-    | Some a => do a' <- f a; OK (Some a')
-    end.
-
-  Definition cases_apply_map_ (stmnt_apply_map_ : Verilog.stmnt -> res Verilog.stmnt) :=
-    fix cases_apply_map (cs : list (Verilog.expr * Verilog.stmnt)) :=
-      match cs with
-      | nil => OK nil
-      | (c_e, c_s) :: tl =>
-        do c_e' <- expr_apply_map c_e;
-        do c_s' <- stmnt_apply_map_ c_s;
-        do tl' <- cases_apply_map tl;
-        OK ((c_e', c_s') :: tl')
-      end.
-
-  Fixpoint stmnt_apply_map (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt :=
-    match stmnt with
-    | Vskip => OK Vskip
-    | Vseq s1 s2 =>
-      do s1' <- stmnt_apply_map s1;
-      do s2' <- stmnt_apply_map s2;
-      OK (Vseq s1' s2')
-    | Vcond e s1 s2 =>
-      do e' <- expr_apply_map e;
-      do s1' <- stmnt_apply_map s1;
-      do s2' <- stmnt_apply_map s2;
-      OK (Vcond e' s1' s2')
-    | Vcase e cases def =>
-      do e' <- expr_apply_map e;
-      do cases' <- cases_apply_map_ stmnt_apply_map cases;
-      do def' <- mmap_option (fun x => stmnt_apply_map x) def;
-      OK (Vcase e' cases' def')
-    | Vblock e1 e2 =>
-      do e1' <- expr_apply_map e1;
-      do e2' <- expr_apply_map e2;
-      OK (Vblock e1' e2')
-    | Vnonblock e1 e2 =>
-      do e1' <- expr_apply_map e1;
-      do e2' <- expr_apply_map e2;
-      OK (Vnonblock e1' e2')
-    end.
-
-  (* Unused. Defined for completeness *)
-  Definition cases_apply_map := cases_apply_map_ stmnt_apply_map.
-End APPLY_MAPPING.
-
 Section TRANSLATE.
   Local Open Scope error_monad_scope.
 
-  Definition transl_datapath_fun externctrl modmap (a : Verilog.node * HTL.datapath_stmnt) :=
-    let (n, s) := a in
-    let node := Verilog.Vlit (posToValue n) in
-    do stmnt <- stmnt_apply_map externctrl modmap s;
-    OK (node, stmnt).
+  Definition transl_states : list (HTL.node * HTL.datapath_stmnt) -> list (Verilog.expr * Verilog.stmnt) :=
+    map (fun '(n, s) => (Verilog.Vlit (posToValue n), s)).
 
-  Definition transl_datapath externctrl modmap st := Errors.mmap (transl_datapath_fun externctrl modmap) st.
+  Definition scl_to_Vdecls :=
+    map (fun '(r, (io, Verilog.VScalar sz)) => Vdeclaration (Vdecl io r sz)).
 
-  Definition transl_ctrl_fun externctrl modmap (a : Verilog.node * HTL.control_stmnt) : Errors.res (Verilog.expr * Verilog.stmnt):=
-    let (n, s) := a in
-    let node := Verilog.Vlit (posToValue n) in
-    do stmnt <- stmnt_apply_map externctrl modmap s;
-    OK (node, stmnt).
-
-  Definition transl_ctrl externctrl modmap st := Errors.mmap (transl_ctrl_fun externctrl modmap) st.
-
-  Definition scl_to_Vdecl_fun externctrl modmap (a : reg * (option Verilog.io * Verilog.scl_decl)) :=
-    match a with (r, (io, Verilog.VScalar sz)) =>
-                 do r' <- reg_apply_map externctrl modmap r;
-                 OK (Verilog.Vdecl io r' sz)
-    end.
-
-  Definition scl_to_Vdecl externctrl modmap scldecl := mmap (scl_to_Vdecl_fun externctrl modmap) scldecl.
-
-  Definition arr_to_Vdeclarr_fun externctrl modmap (a : reg * (option Verilog.io * Verilog.arr_decl)) :=
-    match a with (r, (io, Verilog.VArray sz l)) =>
-                 do r' <- reg_apply_map externctrl modmap r;
-                 OK (Verilog.Vdeclarr io r' sz l)
-    end.
-
-  Definition arr_to_Vdeclarr externctrl modmap arrdecl := mmap (arr_to_Vdeclarr_fun externctrl modmap) arrdecl.
+  Definition arr_to_Vdeclarrs :=
+    map (fun '(r, (io, Verilog.VArray sz l)) => Vdeclaration (Vdeclarr io r sz l)).
 
   Definition called_functions (main_name : ident) (m : HTL.module) : list ident :=
     (* remove duplicates *)
@@ -185,14 +50,6 @@ Section TRANSLATE.
                          (List.filter (fun it => negb (Pos.eqb (fst (snd it)) main_name))
                                       (PTree.elements (HTL.mod_externctrl m)))).
 
-  Definition prog_modmap (p : HTL.program) :=
-    PTree_Properties.of_list (Option.map_option
-                            (fun a => match a with
-                                   | (ident, (Gfun (Internal f))) => Some (ident, f)
-                                   | _ => None
-                                   end)
-                            p.(prog_defs)).
-
   (** Clean up declarations for an inlined module. Make IO decls into reg, and remove the clk declaration *)
   Definition clean_up_decl (clk : reg) (it : Verilog.module_item) :=
     match it with
@@ -225,50 +82,45 @@ Section TRANSLATE.
                                         translated_modules in
 
 
-      do case_el_ctrl <- transl_ctrl (HTL.mod_externctrl m) modmap (PTree.elements (HTL.mod_controllogic m));
-      do case_el_data <- transl_datapath (HTL.mod_externctrl m) modmap (PTree.elements (HTL.mod_datapath m));
+      let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in
+      let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in
 
       let externctrl := HTL.mod_externctrl m in
-      do rst <- reg_apply_map externctrl modmap (HTL.mod_reset m);
-      do st <- reg_apply_map externctrl modmap (HTL.mod_st m);
-      do finish <- reg_apply_map externctrl modmap (HTL.mod_finish m);
-      do params <- mmap (reg_apply_map externctrl modmap) (HTL.mod_params m);
 
       (* Only declare the clock if this is the top-level module, i.e. there is no inherited clock *)
-      do maybe_clk_decl <- match externclk with
-                          | None =>
-                            do decl <- scl_to_Vdecl_fun externctrl modmap (clk, (Some Vinput, VScalar 1));
-                            OK [Vdeclaration decl]
-                          | Some _ => OK []
-                          end;
+      let maybe_clk_decl := match externclk with
+                            | None => scl_to_Vdecls [(clk, (Some Vinput, VScalar 1))]
+                            | Some _ => []
+                            end in
 
       let local_arrdecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_arrdecls m) in
-      do arr_decls <- arr_to_Vdeclarr externctrl modmap (AssocMap.elements local_arrdecls);
+      let arr_decls := arr_to_Vdeclarrs (AssocMap.elements local_arrdecls) in
 
       let local_scldecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_scldecls m) in
-      do scl_decls <- scl_to_Vdecl externctrl modmap (AssocMap.elements local_scldecls);
+      let scl_decls := scl_to_Vdecls (AssocMap.elements local_scldecls) in
 
       let body : list Verilog.module_item:=
-          Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar rst) (Vlit (ZToValue 1)))
+          Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1)))
                                                     (Vseq
-                                                      (Vnonblock (Vvar st) (Vlit (posToValue (HTL.mod_entrypoint m))))
-                                                      (Vnonblock (Vvar finish) (Vlit (ZToValue 0))))
-                                                    (Vcase (Vvar st) case_el_ctrl (Some Vskip)))
+                                                      (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m))))
+                                                      (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0))))
+                                                    (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip)))
                   :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip))
-                  :: List.map Vdeclaration (arr_decls ++ scl_decls)
+                  :: arr_decls
+                  ++ scl_decls
                   ++ maybe_clk_decl
                   ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) in
 
       OK (Verilog.mkmodule
                (HTL.mod_start m)
-               rst
-               clk
-               finish
+               (HTL.mod_reset m)
+               (HTL.mod_clk m)
+               (HTL.mod_finish m)
                (HTL.mod_return m)
-               st
+               (HTL.mod_st m)
                (HTL.mod_stk m)
                (HTL.mod_stk_len m)
-               params
+               (HTL.mod_params m)
                body
                (HTL.mod_entrypoint m))
     end.