From 22322017770c9045657f0d3a43f186ab46b0e127 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 13 Nov 2021 23:02:21 +0000
Subject: Add commented out pretty printing for Abstr

---
 src/hls/PrintAbstr.ml | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 src/hls/PrintAbstr.ml

diff --git a/src/hls/PrintAbstr.ml b/src/hls/PrintAbstr.ml
new file mode 100644
index 0000000..c63fa02
--- /dev/null
+++ b/src/hls/PrintAbstr.ml
@@ -0,0 +1,39 @@
+(**open Camlcoq
+open Datatypes
+open Maps
+open AST
+open Abstr
+open PrintAST
+open Printf
+
+let rec expr_to_list = function
+  | Enil -> []
+  | Econs (e, el) -> e :: expr_to_list el
+
+let res pp = function
+  | Reg r -> fprintf pp "r%d" (P.to_int r)
+  | Pred r -> fprintf pp "p%d" (P.to_int r)
+  | Mem -> fprintf pp "M"
+
+let rec print_expression pp = function
+  | Ebase r -> fprintf pp "%a'" res r
+  | Eop (op, el) -> fprintf pp "(%a)" (PrintOp.print_operation print_expression) (op, expr_to_list el)
+  | Eload (chunk, addr, el, e) ->
+    fprintf pp "(%s[%a][%a])"
+       (name_of_chunk chunk) print_expression e
+       (PrintOp.print_addressing print_expression) (addr, expr_to_list el)
+  | Estore (e, chunk, addr, el, m) ->
+    fprintf pp "(%s[%a][%a] = %a)"
+      (name_of_chunk chunk) print_expression m
+      (PrintOp.print_addressing print_expression) (addr, expr_to_list el)
+      print_expression e
+  | Esetpred (c, el) ->
+    fprintf pp "(%a)" (PrintOp.print_condition print_expression) (c, expr_to_list el)
+
+let rec print_predicated pp = function
+  | NE.Coq_singleton (p, e) ->
+    fprintf pp "%a %a" PrintRTLBlockInstr.print_pred_option p print_expression e
+  | NE.Coq_cons ((p, e), pr) ->
+    fprintf pp "%a %a\n%a" PrintRTLBlockInstr.print_pred_option p print_expression e
+      print_predicated pr
+*)
-- 
cgit