From b92fe5bd91e6041aa2dedf87eaa399d7bcb506a8 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 8 Oct 2024 13:33:20 +0200
Subject: [PATCH] Rename Cnf into Translate

---
 rsc/extra/subgraphs.dot                     |  5 +----
 src/bin/common/solving_loop.ml              | 10 +++++-----
 src/lib/dune                                |  2 +-
 src/lib/frontend/{cnf.ml => translate.ml}   |  0
 src/lib/frontend/{cnf.mli => translate.mli} |  0
 src/lib/index.mld                           |  8 +-------
 src/lib/structures/expr.ml                  |  2 +-
 7 files changed, 9 insertions(+), 18 deletions(-)
 rename src/lib/frontend/{cnf.ml => translate.ml} (100%)
 rename src/lib/frontend/{cnf.mli => translate.mli} (100%)

diff --git a/rsc/extra/subgraphs.dot b/rsc/extra/subgraphs.dot
index 8b73671db5..4a5669cbe4 100644
--- a/rsc/extra/subgraphs.dot
+++ b/rsc/extra/subgraphs.dot
@@ -202,10 +202,7 @@ subgraph cluster_lib {
                 style=filled;
                 color=lightblue;
                 "Frontend";
-                "Cnf";
-                "Typechecker";
-                "Parsed_interface";
-                "Input";
+                "Translate";
                 "Parse_command"
         }
 
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 58269277a7..52c465ab2d 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -349,7 +349,7 @@ let process_source ?selector_inst ~print_status src =
       ~size_limit ~response_file
     |> Parser.init
     |> Typer.init
-      ~additional_builtins:Cnf.builtins
+      ~additional_builtins:Translate.builtins
       ~extension_builtins:[Typer.Ext.bv2nat]
     |> Typer_Pipe.init ~type_check
   in
@@ -512,7 +512,7 @@ let process_source ?selector_inst ~print_status src =
         { Typer_Pipe.id; contents; loc; attrs = []; implicit = false }
       in
       let cnf =
-        Cnf.make (State.get State.logic_file st).loc
+        Translate.make (State.get State.logic_file st).loc
           (State.get solver_ctx_key st).ctx stmt
       in
       State.set solver_ctx_key (
@@ -628,7 +628,7 @@ let process_source ?selector_inst ~print_status src =
       Expr.mk_term
         (Sy.name name)
         []
-        (Cnf.dty_to_ty term.DStd.Expr.term_ty)
+        (Translate.dty_to_ty term.DStd.Expr.term_ty)
     in
     match get_value simple_form with
     | Some v -> Fmt.to_to_string Expr.print v
@@ -705,7 +705,7 @@ let process_source ?selector_inst ~print_status src =
         in
         let stmt = { Typer_Pipe.id; contents; loc ; attrs; implicit } in
         let cnf, is_thm =
-          match Cnf.make (State.get State.logic_file st).loc l stmt with
+          match Translate.make (State.get State.logic_file st).loc l stmt with
           | { Commands.st_decl = Query (_, _, kind); _ } as cnf :: hyps ->
             let is_thm =
               match kind with Ty.Thm | Sat -> true | _ -> false
@@ -827,7 +827,7 @@ let process_source ?selector_inst ~print_status src =
              unsupported statement is encountered.
         *)
         let cnf =
-          Cnf.make (State.get State.logic_file st).loc
+          Translate.make (State.get State.logic_file st).loc
             (State.get solver_ctx_key st).ctx td
         in
         State.set solver_ctx_key (
diff --git a/src/lib/dune b/src/lib/dune
index 961ed444a3..f91c8ecea5 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -46,7 +46,7 @@
   ; modules that make up the lib
   (modules
     ; frontend
-    Cnf D_loop D_state_option Frontend Parsed_interface Models
+    Translate D_loop D_state_option Frontend Parsed_interface Models
     ; reasoners
     Ac Arith Arrays_rel Bitv Ccx Shostak Relation
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/translate.ml
similarity index 100%
rename from src/lib/frontend/cnf.ml
rename to src/lib/frontend/translate.ml
diff --git a/src/lib/frontend/cnf.mli b/src/lib/frontend/translate.mli
similarity index 100%
rename from src/lib/frontend/cnf.mli
rename to src/lib/frontend/translate.mli
diff --git a/src/lib/index.mld b/src/lib/index.mld
index 12642cf8a7..fd456523f8 100644
--- a/src/lib/index.mld
+++ b/src/lib/index.mld
@@ -78,11 +78,8 @@ Finally, the native input method is defined in the {!module:AltErgoLib.Parsed_in
 and {!module:AltErgoLib.Typechecker} modules.
 
 {!modules:
-AltErgoLib.Cnf
+AltErgoLib.Translate
 AltErgoLib.Frontend
-AltErgoLib.Input
-AltErgoLib.Parsed_interface
-AltErgoLib.Typechecker
 }
 
 
@@ -117,10 +114,7 @@ AltErgoLib.Matching_types
 AltErgoLib.Shostak
 AltErgoLib.Ac
 AltErgoLib.Arith
-AltErgoLib.Arrays
 AltErgoLib.Bitv
-AltErgoLib.Enum
-AltErgoLib.Ite
 AltErgoLib.Polynome
 AltErgoLib.Records
 AltErgoLib.Sig
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 7c726bafc4..2cd2be58eb 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -2346,7 +2346,7 @@ module Triggers = struct
           let content = TMap.fold (fun t _ acc -> t :: acc) res [] in
           let content = List.stable_sort pat_weight content in
           if Options.get_verbose () then
-            Printer.print_dbg ~module_name:"Cnf"
+            Printer.print_dbg ~module_name:"Translate"
               ~function_name:"clean_trigger"
               "AXIOM: %s@ \
                from multi-trig of sz %d : %a@ \