diff options
| -rw-r--r-- | src/translation/HTLgen.v | 7 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 8 |
2 files changed, 5 insertions, 10 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 9c2e168..d7f88c1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,8 +17,8 @@ *) From coqup Require Import HTL Coquplib. -From compcert Require Import Maps. +From compcert Require Import Maps. From compcert Require Errors. From compcert Require Import AST RTL. @@ -179,11 +179,6 @@ Definition transf_function (f: function) : Errors.res module := | Error err => Errors.Error err end. -Definition example : mon HTL.code := PTree.traverse transf_instr - (PTree.set 2%positive (RTL.Icall sig ros args res n) (PTree.set 1%positive (RTL.Iop (Op.Omove) nil 1%positive 2%positive) (PTree.empty RTL.instruction))). - -Compute example. - Definition transf_fundef (fd: fundef) : Errors.res moddecl := transf_partial_fundef transf_function fd. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 202a8b7..f2620a7 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -60,19 +60,19 @@ Definition modsig (md : moddecl) := | AST.External ef => AST.ef_sig ef end. -(** Describes the transformation of VTL instruction by instruction. This applies +(** Describes various transformations that can be applied to HTL. This applies the transformation to each instruction in the function and returns the new function with the modified instructions. *) Section TRANSF. - Variable transf : node -> instruction -> instruction. + Variable transf_instr : node -> instruction -> instruction. - Definition transf_function (m : module) : module := + Definition transf_module (m : module) : module := mkmodule m.(mod_sig) m.(mod_params) m.(mod_stacksize) - (PTree.map transf m.(mod_code)) + (PTree.map transf_instr m.(mod_code)) m.(mod_insts) m.(mod_entrypoint). |