diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-09-29 20:48:35 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-09-29 20:48:35 +0100 |
commit | a1657466c7d8af0ed405723bf3aa83bafedf9816 (patch) | |
tree | 752b72608d621cec57de920e86d7a70f9de36662 /src/hls/IfConversion.v | |
parent | 4ba9568762cecd2bda449d19fed45cfd002fcdbe (diff) | |
download | vericert-a1657466c7d8af0ed405723bf3aa83bafedf9816.tar.gz vericert-a1657466c7d8af0ed405723bf3aa83bafedf9816.zip |
Add new if-conversion pass with top-level fold
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r-- | src/hls/IfConversion.v | 28 |
1 files changed, 12 insertions, 16 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 9719ae6..6693b82 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -35,10 +35,9 @@ Require Import vericert.hls.GibleSeq. Require Import vericert.hls.Predicate. Require Import vericert.bourdoncle.Bourdoncle. -Definition if_conv_t : Type := PTree.t (list (node * node)). +Definition if_conv_t : Type := list (node * node). Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N). -Parameter get_if_conv_t : program -> list if_conv_t. #[local] Open Scope positive. @@ -225,7 +224,7 @@ Definition ifconv_list (headers: list node) (c: code) := Definition if_convert_code (c: code) iflist := fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c. -Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function := +Definition transf_function (l: option if_conv_t) (f: function) : function := let (b, _) := build_bourdoncle f in let b' := get_loops b in let iflist := ifconv_list b' f.(fn_code) in @@ -235,28 +234,25 @@ Definition transf_function (l: if_conv_t) (i: ident) (f: function) : function := Section TRANSF_PROGRAM. - Context {A B V: Type}. - Variable transf: ident -> A -> B. + Context {A B V DATA: Type}. + Variable transf: option DATA -> A -> B. - Definition transform_program_globdef' (idg: ident * globdef A V) : ident * globdef B V := + Definition transform_program_globdef' (data: PTree.t DATA) (idg: ident * globdef A V) : ident * globdef B V := match idg with - | (id, Gfun f) => (id, Gfun (transf id f)) + | (id, Gfun f) => (id, Gfun (transf (data!id) f)) | (id, Gvar v) => (id, Gvar v) end. - Definition transform_program' (p: AST.program A V) : AST.program B V := + Definition transform_program_data (data: PTree.t DATA) (p: AST.program A V) : AST.program B V := mkprogram - (List.map transform_program_globdef' p.(prog_defs)) + (List.map (transform_program_globdef' data) p.(prog_defs)) p.(prog_public) p.(prog_main). End TRANSF_PROGRAM. -Definition transf_fundef (l: if_conv_t) (i: ident) (fd: fundef) : fundef := - transf_fundef (transf_function l i) fd. +Definition transf_fundef (l: option if_conv_t) (fd: fundef) : fundef := + transf_fundef (transf_function l) fd. -Definition transf_program_rec (p: program) (l: if_conv_t) : program := - transform_program' (transf_fundef l) p. - -Definition transf_program (p: program) : program := - fold_left transf_program_rec (get_if_conv_t p) p. +Definition transf_program (l: PTree.t if_conv_t) (p: program) : program := + transform_program_data transf_fundef l p. |