]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/boxPp.ml
new (box based) pretty printer
[helm.git] / helm / ocaml / cic_transformations / boxPp.ml
diff --git a/helm/ocaml/cic_transformations/boxPp.ml b/helm/ocaml/cic_transformations/boxPp.ml
new file mode 100644 (file)
index 0000000..922d5c6
--- /dev/null
@@ -0,0 +1,21 @@
+
+let to_string object_to_string b =
+  let layout = ref [] in
+  let rec aux_h current_s =
+    function
+       [] -> layout := current_s::!layout
+      | Box.Text (_,s)::tl -> aux_h (current_s ^ s) tl
+      | (Box.Space _)::_ -> assert false
+      | Box.H (_,bl)::tl -> aux_h current_s (bl@tl)
+      | Box.V (_,[])::tl -> aux_h current_s tl
+      | Box.V (_,[b])::tl -> aux_h current_s (b::tl)
+      | Box.V (_,b::bl')::tl ->
+         aux_h current_s [b] ; 
+         aux_h (String.make (String.length current_s) ' ') (Box.V([],bl')::tl)
+      | Box.Object (_,obj)::tl -> aux_h (current_s ^ (object_to_string obj)) tl
+      | (Box.Action _)::tl -> assert false
+  in
+    aux_h "" [b] ;
+    List.rev !layout
+
+let pp_term t = String.concat "\n" (to_string CicAstPp.pp_term (Ast2pres.ast2box t))