[WP] Document functions related to driver config

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.

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

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