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/Compiler.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/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index 1dc9826..5ff291e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -139,6 +139,21 @@ Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop) : A -> A -> Prop := if flag tt then R else eq. +Definition match_rep {A: Type} (R: A -> A -> Prop): A -> A -> Prop := + Relation_Operators.clos_refl_trans A R. + +Global Instance TransfIfLink {A: Type} {LA: Linker A} + (transf: A -> A -> Prop) (TL: TransfLink transf) + : TransfLink (match_rep transf). +Admitted. + +Lemma total_rep_match: + forall (A B: Type) (n: list B) (f: A -> B -> A) + (rel: A -> A -> Prop) (prog: A), + (forall b p, rel p (f p b)) -> + match_rep rel prog (fold_left f n prog). +Proof. Admitted. + Lemma total_if_match: forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A), @@ -264,7 +279,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program @@ print (print_GibleSeq 1) - @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program + @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil)) @@ print (print_GibleSeq 2) @@@ DeadBlocks.transf_program @@ print (print_GibleSeq 3) |