diff options
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..df5dc37 --- /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 (cond, elist, e) -> + fprintf pp "%a; " (PrintOp.print_condition print_expression) (cond, to_expr_list elist); + print_expression pp e +*) |