From 7ab00f12fb2345321de00b5f87659c9df3523a2f Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 3 May 2021 20:34:07 +0100 Subject: Rewrite transf_instr, move complicated part up Mapping the externctrl for the parameters requires a traversal on a list. Moved it up to the top of the branch to make it stand out in the proof. --- src/hls/HTLgen.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 68080e2..f769be2 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -493,6 +493,12 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | 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 params <- traverselist + (fun (a: nat * reg) => let (idx, arg) := a in + do param_reg <- map_externctrl fn (ctrl_param idx); + ret (param_reg, arg)) + (enumerate 0 args); + do _ <- declare_reg None dst 32; do join_state <- create_state; @@ -500,12 +506,6 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni do reset_reg <- map_externctrl fn ctrl_reset; do return_reg <- map_externctrl fn ctrl_return; - do params <- traverselist - (fun (a: nat * reg) => let (idx, arg) := a in - do param_reg <- map_externctrl fn (ctrl_param idx); - ret (param_reg, arg)) - (enumerate 0 args); - let fork_instr := fork reset_reg params in let join_instr := join return_reg reset_reg dst in -- cgit