[wp] Top level module importer registration

src/plugins/wp/Why3Import.ml

@@ -32,6 +32,24 @@ module WConf = Why3.Whyconf
 
 let dkey = L.register_category "why3.import"
 
+(* -------------------------------------------------------------------------- *)
+(* ---    Module registration                                             --- *)
+(* -------------------------------------------------------------------------- *)
+
+let loader (ctxt: Logic_typing.module_builder) (loc: C.location) (m: string list) =
+  begin
+    L.result "[test-import:%d] Loading %s.@." (fst loc).pos_lnum (String.concat "::" m) ;
+    let t = Cil_const.make_logic_type "t" in
+    let check = Cil_const.make_logic_info "check" in
+    let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
+    let k = Cil_const.make_logic_var_formal "k" Linteger in
+    check.l_profile <- [x;k] ;
+    ctxt.add_logic_type loc t ;
+    ctxt.add_logic_function loc check ;
+  end
+
+let () = Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader
+
 (* -------------------------------------------------------------------------- *)
 (* ---    Why3 Environment                                                --- *)
 (* -------------------------------------------------------------------------- *)
@@ -320,24 +338,6 @@ let import_theory (env : env) thname =
 (* ---    Module registration                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let loader (ctxt: Logic_typing.module_builder) (loc: C.location) (m: string list) =
-  begin
-    L.result "[test-import:%d] Loading %s.@." (fst loc).pos_lnum (String.concat "::" m) ;
-    let t = Cil_const.make_logic_type "t" in
-    let check = Cil_const.make_logic_info "check" in
-    let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
-    let k = Cil_const.make_logic_var_formal "k" Linteger in
-    check.l_profile <- [x;k] ;
-    ctxt.add_logic_type loc t ;
-    ctxt.add_logic_function loc check ;
-  end
-
-let register () =
-  begin
-    Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader
-  end
-
-
 (* -------------------------------------------------------------------------- *)
 (* ---    Main                                                            --- *)
 (* -------------------------------------------------------------------------- *)
@@ -345,7 +345,6 @@ let register () =
 let () =
   Boot.Main.extend
     begin fun () ->
-      register ();
       let libs = L.Library.get() in
       let imports = L.Import.get() in
       if libs <> [] || imports <> [] then