Expose tlapm_lib for other projects.

src/dune

@@ -13,6 +13,7 @@
 
 (library
  (name tlapm_lib)
+ (public_name tlapm)
  (modules
   (:standard \ tlapm test_schedule why3_interface abstractor))
  (libraries

src/module/m_fmt.ml

@@ -104,13 +104,14 @@ let rec pp_print_modunit ?(force=false) cx ff mu = match mu.core with
 and pp_print_module ?(force=false) cx ff m =
   fprintf ff "@[<v0>---- MODULE %s ----@," m.core.name.core ;
   begin match m.core.stage with
+    | Final _
     | Parsed when m.core.extendees <> [] ->
         fprintf ff "EXTENDS @[<b0>%a@]@,"
           (pp_print_delimited Util.pp_print_hint) m.core.extendees
-    | Flat -> fprintf ff "@[Flat@]@,"
-    | Special -> fprintf ff "@[Special@]@,"
-    | Parsed -> fprintf ff "@[Parsed with no extendees@]@,"
-    | _ -> ()
+    | Flat -> fprintf ff "@[\\* EXTENDS: Flat@]@,"
+    | Special -> fprintf ff "@[\\* EXTENDS: Special@]@,"
+    | Parsed -> fprintf ff "@[\\* EXTENDS: Parsed with no extendees@]@,"
+    | Final _ -> ()
   end ;
   ignore begin
     List.fold_left begin

src/proof/p_fmt.ml

@@ -125,7 +125,7 @@ let rec pp_print_proof cx ff prf =
                    cx)
                 cx ff inits
             in
-            fprintf ff "@[<hv2>%s%s QED%a@]"
+            fprintf ff "@[<hv2>%s%s QED %a@]"
               (step_name prf) (step_dot prf)
               (pp_print_qed_step(*proof_nl*) cx) qed
         | Error msg ->

src/tlapm_lib.ml

@@ -13,9 +13,11 @@ module Property = Property
 module Proof = Proof
 module Expr = Expr
 module Util = Util
+module Deque = Deque
 module Loc = Loc
 module Ctx = Ctx
 module Backend = Backend
+module Builtin = Builtin
 
 open Proof.T
 
@@ -614,15 +616,12 @@ let init () =
        end;
        exit 3
 
-(* Access to this function has to be synchronized. *)
-let modctx_of_string ~(content : string) ~(filename : string) ~loader_paths ~prefer_stdlib : (modctx * Module.T.mule, string option * string) result =
+let modctx_of_mule' ~(mule : mule Lazy.t) ~(filename : string) ~loader_paths ~prefer_stdlib : (modctx * Module.T.mule, string option * string) result =
     let parse_it () =
         Errors.reset ();
         Params.prefer_stdlib := prefer_stdlib;
         setup_loader [filename] loader_paths;
-        let hint = Util.locate filename Loc.unknown in
-        let hint = Property.assign hint Module.Save.module_content_prop (Module.Save.String content) in
-        let mule = Module.Save.parse_file ~clock:Clocks.parsing hint in
+        let mule = Lazy.force mule in
         Params.input_files := [Filename.basename filename]; (* Needed, because p_gen.ml decides if obs should be generated by this. *)
         Params.set_search_path [Filename.dirname filename]; (* Were to look for referenced files. TODO: Take additional. *)
         mule.core.important <- true ;
@@ -650,8 +649,21 @@ let modctx_of_string ~(content : string) ~(filename : string) ~loader_paths ~pre
          | Some l, None -> Error (Some l, Printexc.to_string e)
          | None, None -> Error (None, Printexc.to_string e))
 
-let module_of_string module_str =
-    let hparse = Tla_parser.P.use M_parser.parse in
+let modctx_of_mule ~(mule : mule) ~(filename : string) ~loader_paths ~prefer_stdlib : (modctx * Module.T.mule, string option * string) result =
+    let mule = Lazy.from_val mule in
+    modctx_of_mule' ~mule ~filename ~loader_paths ~prefer_stdlib
+
+(* Access to this function has to be synchronized, if accessed from a multithreaded environment. *)
+let modctx_of_string ~(content : string) ~(filename : string) ~loader_paths ~prefer_stdlib : (modctx * Module.T.mule, string option * string) result =
+    let mule = lazy (
+        let hint = Util.locate filename Loc.unknown in
+        let hint = Property.assign hint Module.Save.module_content_prop (Module.Save.String content) in
+        Module.Save.parse_file ~clock:Clocks.parsing hint
+    ) in
+    modctx_of_mule' ~mule ~filename ~loader_paths ~prefer_stdlib
+
+let module_of_string (module_str : string) : Module.T.mule option =
+    let hparse = Tla_parser.P.use Module.Parser.parse in
     let (flex, _) = Alexer.lex_string module_str in
     Tla_parser.P.run hparse ~init:Tla_parser.init ~source:flex
 

src/tlapm_lib.mli

@@ -1,19 +1,33 @@
 (*
  * Copyright (C) 2008-2010  INRIA and Microsoft Corporation
+ *
+ * WARNING: While this library is exposed for other projects, its interface
+ * is considered experimentai and not stable. It can change in uncompatible
+ * ways in the future.
  *)
 
 module Module = Module
 module Property = Property
 module Proof = Proof
 module Expr = Expr
 module Util = Util
+module Deque = Deque
 module Loc = Loc
 module Ctx = Ctx
 module Backend = Backend
+module Builtin = Builtin
 
 val main : string list -> unit
 val init : unit -> unit
 
+val modctx_of_mule :
+  mule:Module.T.mule ->
+  filename:string ->
+  loader_paths:string list ->
+  prefer_stdlib:bool ->
+  (Module.T.modctx * Module.T.mule, string option * string) result
+(** Elaborate a module and its context from a module AST. *)
+
 val modctx_of_string :
   content:string ->
   filename:string ->
@@ -24,7 +38,7 @@ val modctx_of_string :
     from a specified string, assume it is located in the
     specified path. *)
 
-val module_of_string : string -> M_t.mule option
+val module_of_string : string -> Module.T.mule option
 (** Parse the specified string as a module. No dependencies
     are considered, nor proof obligations are elaborated. *)