diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-30 22:15:02 +0100 |
commit | 8bc6214e053aa4487abfbd895c00e2da9f21bd8a (patch) | |
tree | 2301479ca921c014a57ca419fbeb32f17624e7e7 /src/hls/Renaming.v | |
parent | b067e5c7b0ecce9ffbf21e9c4a7ff96328dec2ba (diff) | |
download | vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.tar.gz vericert-8bc6214e053aa4487abfbd895c00e2da9f21bd8a.zip |
WIP
Diffstat (limited to 'src/hls/Renaming.v')
-rw-r--r-- | src/hls/Renaming.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index b9fbcaa..6c816c2 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -102,12 +102,12 @@ Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := ret (Vcond e' s1' s2') | Vcase e cs def => do e' <- renumber_expr e; - do cs' <- sequence (map - (fun (c : (Verilog.expr * Verilog.stmnt)) => - let (c_expr, c_stmnt) := c in + do cs_list' <- sequence (map + (fun '(c_expr, c_stmnt) => do expr' <- renumber_expr c_expr; do stmnt' <- renumber_stmnt c_stmnt; - ret (expr', stmnt')) cs); + ret (expr', stmnt')) (stmnt_to_list cs)); + let cs' := list_to_stmnt cs_list' in do def' <- match def with | None => ret None | Some d => do def' <- renumber_stmnt d; ret (Some def') |