[WP] No more project driver

src/plugins/wp/Factory.ml

@@ -283,30 +283,11 @@ let configure_mheap = function
       in
       rollback
 
-module PROJECT = WpContext.Static
-    (struct
-      type key = unit
-      type data = LogicBuiltins.driver
-      let name = "Wp.Factory.PROJECT"
-      let pretty fmt _ = Format.fprintf fmt "%s" name
-      let compare _ _ = 0
-    end)
-
-let configure_driver setup base project_configure =
+let configure_driver setup driver () =
   let rollback_mheap = configure_mheap setup.mheap in
   let rollback_cint = Cint.configure setup.cint in
   let rollback_cfloat = Cfloat.configure setup.cfloat in
-  let project_driver = try PROJECT.find ()
-    with Not_found ->
-      let (setup_id, _) = describe setup in
-      let id = LogicBuiltins.id base ^ "_" ^ setup_id in
-      let project_driver =
-        LogicBuiltins.new_driver ~base ~id ~configure:project_configure ()
-      in
-      PROJECT.update () project_driver ;
-      project_driver
-  in
-  let old_driver = Context.push LogicBuiltins.driver project_driver in
+  let old_driver = Context.push LogicBuiltins.driver driver in
   let rollback () =
     Context.pop LogicBuiltins.driver old_driver ;
     rollback_cfloat () ;

src/plugins/wp/Factory.mli

@@ -39,7 +39,7 @@ type driver = LogicBuiltins.driver
 val ident : setup -> string
 val descr : setup -> string
 val compiler : mheap -> mvar -> (module Sigs.Compiler)
-val configure_driver : setup -> driver -> (unit -> unit) -> WpContext.rollback
+val configure_driver : setup -> driver -> unit -> WpContext.rollback
 val instance : setup -> driver -> WpContext.model
 val default : setup (** ["Var,Typed,Nat,Real"] memory model. *)
 val parse :

src/plugins/wp/wpContext.ml

@@ -29,7 +29,7 @@ type model = {
   descr : string ; (* Title of the Model (for pretty) *)
   emitter : Emitter.t ;
   hypotheses : hypotheses ;
-  configure : ((unit -> unit) -> rollback) ;
+  configure : (unit -> rollback) ;
 }
 
 and rollback = (unit -> unit)
@@ -51,7 +51,7 @@ struct
   let repr = {
     id = "?model" ; descr = "?model" ;
     emitter = Emitter.kernel ;
-    configure = (fun f -> f () ; (fun () -> ())) ;
+    configure = (fun () -> (fun () -> ())) ;
     hypotheses = nohyp ;
   }
 end
@@ -125,16 +125,14 @@ end
 
 let context : (string * context) Context.value = Context.create "WpContext"
 
-let configure (model,_) f = model.configure f
+let configure (model,_) = model.configure ()
 
 let on_context gamma f x =
   let id = S.id gamma in
   let current = Context.push context (id,gamma) in
-  let rollback = try
-      configure gamma Context.configure
-    with _ ->
-      Kernel.fatal "Model configuration failed"
-  in
+  let rollback = try configure gamma
+    with _ -> Kernel.fatal "Model configuration failed" in
+  Context.configure () ;
   try
     let result = f x in
     Context.pop context current ;

src/plugins/wp/wpContext.mli

@@ -30,17 +30,15 @@ type hypotheses = unit -> MemoryContext.clause list
 val register :
   id:string ->
   ?descr:string ->
-  configure:((unit -> unit) -> rollback) ->
+  configure:(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.
+    [Context.values] related to the model. 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