From 117c1abc464c995df2320554a5f3902cb4de5fcb Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 29 Jan 2021 13:33:20 +0100 Subject: [PATCH] [kernel] Allow iterating over Properties in a fixed order --- src/kernel_services/ast_data/property_status.ml | 3 ++- src/kernel_services/ast_data/property_status.mli | 15 ++++++++++++--- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml index 807c37dc474..82c81ac995e 100644 --- a/src/kernel_services/ast_data/property_status.ml +++ b/src/kernel_services/ast_data/property_status.ml @@ -182,9 +182,10 @@ let fold_on_statuses f ip acc = Emitter_with_properties.Hashtbl.fold f h acc with Not_found -> acc - let iter f = Status.iter (fun p _ -> f p) let fold f = Status.fold (fun p _ -> f p) +let iter_sorted ~cmp f = Status.iter_sorted ~cmp (fun p _ -> f p) +let fold_sorted ~cmp f = Status.fold_sorted ~cmp (fun p _ -> f p) (* ok to be computed once right now since there is no parameter dependency *) let usable_kernel_emitter = Emitter.get Emitter.kernel diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli index 5656c38152b..94f0418c371 100644 --- a/src/kernel_services/ast_data/property_status.mli +++ b/src/kernel_services/ast_data/property_status.mli @@ -124,6 +124,9 @@ val get: Property.t -> status Consider using {!Property_status.Consolidation.get} if you want to know the consolidated status of the property. *) +(** Iteration on all the individual statuses emitted for the given property. + @since Aluminium-20160501 *) + val iter_on_statuses: (emitter_with_properties -> emitted_status -> unit) -> Property.t -> unit @@ -131,8 +134,6 @@ val fold_on_statuses: (emitter_with_properties -> emitted_status -> 'a -> 'a) -> Property.t -> 'a -> 'a -(** Iteration on all the individual statuses emitted for the given property. - @since Aluminium-20160501 *) (* ************************************************************************ *) (** {2 Consolidated status} *) @@ -232,12 +233,20 @@ module Consolidation_graph: sig end (* ************************************************************************* *) -(** {2 Access to the registered properties} *) +(** {2 Iteration over the registered properties} *) (* ************************************************************************* *) val iter: (Property.t -> unit) -> unit val fold: (Property.t -> 'a -> 'a) -> 'a -> 'a +(** @since Frama-C+dev *) +val iter_sorted: + cmp:(Property.t -> Property.t -> int) -> (Property.t -> unit) -> unit + +val fold_sorted: + cmp:(Property.t -> Property.t -> int) -> + (Property.t -> 'a -> 'a) -> 'a -> 'a + (* ************************************************************************* *) (** {2 API not for casual users} *) (* ************************************************************************* *) -- GitLab