From 7304fb5943dae602ea5bb9113a5533aa46a80d1c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 11 Dec 2019 16:08:43 +0100
Subject: [PATCH] [WP] Document functions related to driver config
---
src/plugins/wp/Sigs.ml | 4 ++--
src/plugins/wp/wpContext.ml | 6 +++---
src/plugins/wp/wpContext.mli | 12 ++++++++++--
3 files changed, 15 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 43db54a110a..a4a3bf6cd92 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -277,9 +277,9 @@ sig
(** {2 Model Definition} *)
- val configure : WpContext.tuning
+ val configure : unit -> WpContext.rollback
(** Initializers to be run before using the model.
- Typically sets {!Context} values. *)
+ Typically push {!Context} values and returns a function to rollback. *)
val configure_ia: automaton -> vertex binder
(** Given an automaton, return a vertex's binder.
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index 7a3fd5eef54..eb24e7e305f 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -33,7 +33,6 @@ type model = {
}
and rollback = (unit -> unit)
-and tuning = unit -> rollback
and scope = Global | Kf of Kernel_function.t
and hypotheses = unit -> MemoryContext.clause list
and context = model * scope
@@ -70,7 +69,7 @@ struct
end
-let register ~id ?(descr=id) ?(configure=fun _ -> (fun () -> ()))
+let register ~id ?(descr=id) ~configure
?(hypotheses=nohyp) () =
if MODELS.mem id then
Wp_parameters.fatal "Duplicate model '%s'" id ;
@@ -133,7 +132,8 @@ let on_context gamma f x =
let current = Context.push context (id,gamma) in
let rollback = try
configure gamma Context.configure
- with _err -> Kernel.fatal "Model configuration failed"
+ with _ ->
+ Kernel.fatal "Model configuration failed"
in
try
let result = f x in
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index e84f12819af..a8a18e2d80a 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -25,15 +25,23 @@
type model
type scope = Global | Kf of Kernel_function.t
type rollback = unit -> unit
-type tuning = unit -> rollback
type hypotheses = unit -> MemoryContext.clause list
val register :
id:string ->
?descr:string ->
- ?configure:((unit -> unit) -> rollback) ->
+ configure:((unit -> unit) -> rollback) ->
?hypotheses:hypotheses ->
unit -> model
+(** Model registration. The model is identified by [id] and described by
+ [descr] (that defaults to [id]). The [configure] function is called on
+ [WpContext.on_context] call, it must prepare and set the different
+ [Context.values] related to the model. For this, it receives in input
+ the function used to extend the driver (and that should be transmitted
+ to the [LogicBuiltins.new_driver] function if needed. In exchange, it
+ must return the function that allows to rollback on the original state.
+ The [hypotheses] function must return the hypotheses made by the model.
+*)
val get_descr : model -> string
val get_emitter : model -> Emitter.t
--
GitLab