Merge pull request #147 from ahelwer/expose-parser

Exposed parse method in TLAPM API

lsp/lib/parser/parser.ml

@@ -1,3 +1,7 @@
 let module_of_string ~content ~filename ~loader_paths =
-  Tlapm_lib.module_of_string ~content ~filename ~loader_paths
-    ~prefer_stdlib:true
+  match
+    Tlapm_lib.modctx_of_string ~content ~filename ~loader_paths
+      ~prefer_stdlib:true
+  with
+  | Ok (_mcx, mule) -> Ok mule
+  | Error err -> Error err

src/tlapm_lib.ml

@@ -615,7 +615,7 @@ let init () =
        exit 3
 
 (* Access to this function has to be synchronized. *)
-let module_of_string ~(content : string) ~(filename : string) ~loader_paths ~prefer_stdlib : (Module.T.mule, (string option* string)) result =
+let modctx_of_string ~(content : string) ~(filename : string) ~loader_paths ~prefer_stdlib : (modctx * Module.T.mule, string option * string) result =
     let parse_it () =
         Errors.reset ();
         Params.prefer_stdlib := prefer_stdlib;
@@ -637,11 +637,11 @@ let module_of_string ~(content : string) ~(filename : string) ~loader_paths ~pre
             | false -> (mcx, found)
         ) (mcx, None) mods in
         match mule with
-        | Some mule -> Ok mule
-        | None -> failwith "module_of_string, found no module we tried to parse."
+        | Some mule -> Ok (mcx, mule)
+        | None -> failwith "modctx_of_string, found no module we tried to parse."
     in
     match parse_it () with
-    | Ok mule -> Ok mule
+    | Ok (mcx, mule) -> Ok (mcx, mule)
     | Error e -> Error e
     | exception e ->
         (match !Errors.loc, !Errors.msg with
@@ -650,4 +650,9 @@ let module_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 (flex, _) = Alexer.lex_string module_str in
+    Tla_parser.P.run hparse ~init:Tla_parser.init ~source:flex
+
 let stdlib_search_paths = Params.stdlib_search_paths

src/tlapm_lib.mli

@@ -14,13 +14,19 @@ module Backend = Backend
 val main : string list -> unit
 val init : unit -> unit
 
-val module_of_string :
+val modctx_of_string :
   content:string ->
   filename:string ->
   loader_paths:string list ->
   prefer_stdlib:bool ->
-  (Module.T.mule, string option * string) result
-(** Parse module from a specified string, assume it is located in the specified path. *)
+  (Module.T.modctx * Module.T.mule, string option * string) result
+(** Parse and elaborate the specified module and its context
+    from a specified string, assume it is located in the
+    specified path. *)
+
+val module_of_string : string -> M_t.mule option
+(** Parse the specified string as a module. No dependencies
+    are considered, nor proof obligations are elaborated. *)
 
 val stdlib_search_paths : string list
 (** A list of paths to look for stdlib modules. *)