diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-01 14:16:52 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-01 14:17:05 +0100 |
commit | c689bcc4eaaaf052ecb35539dff653185192b5e9 (patch) | |
tree | a20a766a9411429368748a57a171ba00d064f7fb /src/hls/PrintExpression.ml | |
parent | 23c700b5fb35fb00d994cb66e4597fe8ea0b28e1 (diff) | |
download | vericert-c689bcc4eaaaf052ecb35539dff653185192b5e9.tar.gz vericert-c689bcc4eaaaf052ecb35539dff653185192b5e9.zip |
Add printers for expressions and RTLPar
Diffstat (limited to 'src/hls/PrintExpression.ml')
-rw-r--r-- | src/hls/PrintExpression.ml | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/src/hls/PrintExpression.ml b/src/hls/PrintExpression.ml new file mode 100644 index 0000000..cfe6750 --- /dev/null +++ b/src/hls/PrintExpression.ml @@ -0,0 +1,40 @@ +(*open Printf +open Camlcoq +open Datatypes +open Maps +open PrintAST +open RTLPargen + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let pred pp r = + fprintf pp "p%d" (P.to_int r) + +let print_resource pp = function + | Reg r -> reg pp r + | Pred r -> pred pp r + | Mem -> fprintf pp "M" + +let rec to_expr_list = function + | Enil -> [] + | Econs (e, elist) -> e :: to_expr_list elist + +let rec print_expression pp = function + | Ebase r -> print_resource pp r + | Eop (op, elist, e) -> + PrintOp.print_operation print_expression pp (op, to_expr_list elist); + Printf.printf "; "; + print_expression pp e + | Eload (chunk, addr, elist, e) -> + fprintf pp "%s[%a]; " (name_of_chunk chunk) (PrintOp.print_addressing print_expression) (addr, to_expr_list elist); + print_expression pp e + | Estore (e, chunk, addr, elist, e') -> + fprintf pp "%s[%a] = %a; " (name_of_chunk chunk) + (PrintOp.print_addressing print_expression) (addr, to_expr_list elist) + print_expression e; + print_expression pp e + | Esetpred (p, cond, elist, e) -> + fprintf pp "%a = %a; " pred p (PrintOp.print_condition print_expression) (cond, to_expr_list elist); + print_expression pp e +*) |