From cf22582354cc24016bf24917c98cbb76f3b29100 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 5 Feb 2019 16:37:56 +0100
Subject: [PATCH] [printer] more flexible builder API
---
.../ast_printing/printer_api.mli | 12 ++-
.../ast_printing/printer_builder.ml | 96 ++++++++++---------
.../ast_printing/printer_builder.mli | 7 ++
3 files changed, 68 insertions(+), 47 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 1233d42b735..78de7bf3606 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -366,7 +366,7 @@ type state =
(** {2 Functions for pretty printing} *)
(* ********************************************************************* *)
-module type S = sig
+module type S_pp = sig
val pp_varname: Format.formatter -> string -> unit
@@ -474,8 +474,14 @@ module type S = sig
Format.formatter ->
'a ->
unit
- (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
- but add some extra braces '\{' and '\}' which are hidden by default. *)
+ (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
+ but add some extra braces '\{' and '\}' which are hidden by default. *)
+
+end
+
+module type S = sig
+
+ include S_pp
(* ********************************************************************* *)
(** {3 Extensible printer} *)
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index 06450f9994a..bba10960ff4 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -20,54 +20,15 @@
(* *)
(**************************************************************************)
-module Make
- (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
+module Make_pp
+ (P: sig val printer : unit -> Printer_api.extensible_printer_type end) =
struct
- module type PrinterClass = sig
- class printer : Printer_api.extensible_printer_type
- end
-
- let printer_class_ref =
- ref (module struct class printer = P.printer () end: PrinterClass)
-
- let printer_ref = ref None
-
- module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
-
- let set_printer p =
- printer_class_ref := p;
- printer_ref := None
-
- let update_printer x =
- let module X = (val x: PrinterExtension) in
- let module Cur = (val !printer_class_ref: PrinterClass) in
- let module Updated = X(Cur) in
- set_printer (module Updated: PrinterClass)
-
- let printer () : Printer_api.extensible_printer_type =
- match !printer_ref with
- | None ->
- let module Printer = (val !printer_class_ref: PrinterClass) in
- let p = new Printer.printer in
- printer_ref := Some p;
- p#reset ();
- p
- | Some p ->
- p#reset ();
- p
-
- let current_printer () = !printer_class_ref
-
- class extensible_printer = P.printer
+ let printer = P.printer
let without_annot f fmt x = (printer ())#without_annot f fmt x
let force_brace f fmt x = (printer ())#force_brace f fmt x
-
- let pp_varname fmt x = (printer())#varname fmt x
-
- (* eta-expansion required for applying side-effect of [printer ()] at the
- right time *)
+ let pp_varname fmt x = (printer ())#varname fmt x
let pp_location fmt x = (printer ())#location fmt x
let pp_constant fmt x = (printer ())#constant fmt x
let pp_ikind fmt x = (printer ())#ikind fmt x
@@ -113,7 +74,7 @@ struct
let pp_variant fmt x = (printer ())#variant fmt x
let pp_from fmt x = (printer ())#from "assigns" fmt x
let pp_full_assigns fmt x = (printer ())#assigns fmt x
- let pp_assigns = pp_full_assigns "assigns"
+ let pp_assigns fmt x = pp_full_assigns "assigns" fmt x
let pp_allocation fmt x = (printer ())#allocation ~isloop:false fmt x
let pp_loop_from fmt x = (printer ())#from "loop assigns" fmt x
let pp_loop_assigns fmt x = (printer ())#assigns "loop assigns" fmt x
@@ -129,6 +90,53 @@ struct
let pp_logic_constant fmt x = (printer ())#logic_constant fmt x
let pp_term_lhost fmt x = (printer ())#term_lhost fmt x
let pp_fundec fmt x = (printer ())#fundec fmt x
+
+end
+
+
+module Make
+ (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
+struct
+
+ module type PrinterClass = sig
+ class printer : Printer_api.extensible_printer_type
+ end
+
+ let printer_class_ref =
+ ref (module struct class printer = P.printer () end: PrinterClass)
+
+ let printer_ref = ref None
+
+ module type PrinterExtension = functor (X: PrinterClass) -> PrinterClass
+
+ let set_printer p =
+ printer_class_ref := p;
+ printer_ref := None
+
+ let update_printer x =
+ let module X = (val x: PrinterExtension) in
+ let module Cur = (val !printer_class_ref: PrinterClass) in
+ let module Updated = X(Cur) in
+ set_printer (module Updated: PrinterClass)
+
+ let printer () : Printer_api.extensible_printer_type =
+ match !printer_ref with
+ | None ->
+ let module Printer = (val !printer_class_ref: PrinterClass) in
+ let p = new Printer.printer in
+ printer_ref := Some p;
+ p#reset ();
+ p
+ | Some p ->
+ p#reset ();
+ p
+
+ let current_printer () = !printer_class_ref
+
+ class extensible_printer = P.printer
+
+ include Make_pp(struct let printer = printer end)
+
end
(*
diff --git a/src/kernel_services/ast_printing/printer_builder.mli b/src/kernel_services/ast_printing/printer_builder.mli
index d9af78ade52..1816cc0ec42 100644
--- a/src/kernel_services/ast_printing/printer_builder.mli
+++ b/src/kernel_services/ast_printing/printer_builder.mli
@@ -20,6 +20,13 @@
(* *)
(**************************************************************************)
+(** Build a dynamic printer that bind all pretty-printers to the
+ object obtained by (P()) *)
+
+module Make_pp
+ (P: sig val printer: unit -> Printer_api.extensible_printer_type end):
+ Printer_api.S_pp
+
(** Build a full pretty-printer from a pretty-printing class.
@since Fluorine-20130401 *)
--
GitLab