From 901fd479e6b9e356bfa683ad0bb056390aaee3d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 11:43:09 +0200
Subject: [PATCH] [modules] document logic_name api
---
src/kernel_services/ast_printing/cil_printer.ml | 4 ++--
src/kernel_services/ast_printing/printer_api.ml | 7 ++++++-
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 611431bf02..fa0a5d3969 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1263,9 +1263,9 @@ class cil_printer () = object (self)
method builtin_logic_info fmt bli =
fprintf fmt "%a" self#varname bli.bl_name
- method logic_type_info fmt s = fprintf fmt "%a" self#logic_name s.lt_name
+ method logic_type_info fmt s = self#logic_name fmt s.lt_name
- method logic_ctor_info fmt ci = fprintf fmt "%a" self#logic_name ci.ctor_name
+ method logic_ctor_info fmt ci = self#logic_name fmt ci.ctor_name
method initinfo fmt io =
match io.init with
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index 14c22c78d8..1066405ee1 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -274,8 +274,13 @@ class type extensible_printer_type = object
method builtin_logic_info: Format.formatter -> builtin_logic_info -> unit
method logic_type_info: Format.formatter -> logic_type_info -> unit
method logic_ctor_info: Format.formatter -> logic_ctor_info -> unit
- method logic_name: Format.formatter -> string -> unit
method logic_var: Format.formatter -> logic_var -> unit
+
+ (** logic names, with full module path if needed (eg. "foo::bar::jazz")
+ Defaults to [self#varname], with the full name truncated to the currently
+ opened module, if any. *)
+ method logic_name: Format.formatter -> string -> unit
+
method quantifiers: Format.formatter -> quantifiers -> unit
method predicate_node: Format.formatter -> predicate_node -> unit
method predicate: Format.formatter -> predicate -> unit
--
GitLab