From 298c48e2193fce2b558308bfd28dfba87ebcae45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 18 Jun 2024 19:00:51 +0200
Subject: [PATCH] [kernel] renamed unfold-loop module
---
.../typing/{unroll_loops.ml => unfold_loops.ml} | 12 ++++++------
.../typing/{unroll_loops.mli => unfold_loops.mli} | 6 +++---
src/kernel_services/ast_data/ast.ml | 2 +-
src/kernel_services/plugin_entry_points/kernel.ml | 14 +++++++-------
src/kernel_services/plugin_entry_points/kernel.mli | 4 ++--
5 files changed, 19 insertions(+), 19 deletions(-)
rename src/kernel_internals/typing/{unroll_loops.ml => unfold_loops.ml} (99%)
rename src/kernel_internals/typing/{unroll_loops.mli => unfold_loops.mli} (92%)
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
similarity index 99%
rename from src/kernel_internals/typing/unroll_loops.ml
rename to src/kernel_internals/typing/unfold_loops.ml
index 6357d6e25cd..60d3ede0535 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -738,18 +738,18 @@ let apply_transformation ?(force=true) nb file =
(* Performs and closes all syntactic transformations *)
let compute file =
- let nb = Kernel.UnrollingLevel.get () in
- let force = Kernel.UnrollingForce.get () in
+ let nb = Kernel.UnfoldingLevel.get () in
+ let force = Kernel.UnfoldingForce.get () in
apply_transformation ~force nb file
-let unroll_transform =
+let transform =
File.register_code_transformation_category "loop unfolding"
let () =
File.add_code_transformation_after_cleanup
- ~deps:[(module Kernel.UnrollingLevel:Parameter_sig.S);
- (module Kernel.UnrollingForce:Parameter_sig.S)]
- unroll_transform compute
+ ~deps:[(module Kernel.UnfoldingLevel:Parameter_sig.S);
+ (module Kernel.UnfoldingForce:Parameter_sig.S)]
+ transform compute
let unroll_typer (ctxt: Logic_typing.typing_context) (_loc:location) args =
let open Logic_typing in
diff --git a/src/kernel_internals/typing/unroll_loops.mli b/src/kernel_internals/typing/unfold_loops.mli
similarity index 92%
rename from src/kernel_internals/typing/unroll_loops.mli
rename to src/kernel_internals/typing/unfold_loops.mli
index 2f2c4a12fe6..a078e243006 100644
--- a/src/kernel_internals/typing/unroll_loops.mli
+++ b/src/kernel_internals/typing/unfold_loops.mli
@@ -20,14 +20,14 @@
(* *)
(**************************************************************************)
-(** Syntactic loop unrolling.
+(** Syntactic loop unfolding.
Uses code transformation hook mechanism (after-cleanup phase)
of {!File} and exports nothing.
- Name of the transformation is "loop unrolling"
+ Name of the transformation is "loop unfolding"
*)
-val unroll_transform: File.code_transformation_category
+val transform: File.code_transformation_category
(*
Local Variables:
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index 0efd2a91414..5dbe5309e22 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -38,7 +38,7 @@ include
Kernel.ReadAnnot.self;
Kernel.PreprocessAnnot.self;
Kernel.Files.self;
- Kernel.UnrollingLevel.self;
+ Kernel.UnfoldingLevel.self;
Kernel.Keep_unused_specified_functions.self;
Kernel.Keep_unused_types.self;
Cil.selfFormalsDecl ]
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 3ff75f40f3f..73cf18ce7ce 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1268,26 +1268,26 @@ module JsonCompilationDatabase =
let normalisation = add_group "Customizing Normalization"
let () = Parameter_customize.set_group normalisation
-module UnrollingLevel =
+module UnfoldingLevel =
Zero
(struct
- let module_name = "UnrollingLevel"
+ let module_name = "UnfoldingLevel"
let option_name = "-ulevel"
let arg_name = "l"
let help =
- "unroll loops n times (defaults to 0) before analyzes. \
- A negative value hides UNROLL loop pragmas."
+ "unfold loops n times (defaults to 0) before analyzes. \
+ A negative value hides loop unfold annotations."
end)
let () = Parameter_customize.set_group normalisation
-module UnrollingForce =
+module UnfoldingForce =
Bool
(struct
- let module_name = "UnrollingForce"
+ let module_name = "UnfoldingForce"
let default = false
let option_name = "-ulevel-force"
let help =
- "ignore loop unfold \"done\" specifications (force unrolling)."
+ "ignore loop unfold \"done\" specifications (force unfolding)."
end)
let () = Parameter_customize.set_group normalisation
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 8d4f1b47e79..2e8856d2e52 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -438,10 +438,10 @@ module Set_project_as_default: Parameter_sig.Bool
(** {2 Customizing Normalization and parsing} *)
(* ************************************************************************* *)
-module UnrollingLevel: Parameter_sig.Int
+module UnfoldingLevel: Parameter_sig.Int
(** Behavior of option "-ulevel" *)
-module UnrollingForce: Parameter_sig.Bool
+module UnfoldingForce: Parameter_sig.Bool
(** Behavior of option "-ulevel-force"
@since Neon-20140301 *)
--
GitLab