Add SANY parser backend

deps/tla2tools.jar/Makefile

@@ -0,0 +1,11 @@
+TLA_TOOLS_JAR_URL=https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
+
+tla2tools.jar:
+	wget --progress=dot:giga $(TLA_TOOLS_JAR_URL)
+
+clean:
+	rm tla2sany.jar
+
+sany: tla2tools.jar
+
+.PHONY: sany clean

deps/tla2tools.jar/dune

@@ -0,0 +1,9 @@
+; Download SANY
+(rule
+ (deps "Makefile")
+ (targets tla2tools.jar)
+ (action (run "make" "-C" "." "sany")))
+
+(install
+ (section (site (tlapm backends)))
+ (files (tla2tools.jar as bin/tla2tools.jar)))

dune-project

@@ -51,6 +51,7 @@
   ppx_inline_test
   ppx_assert
   ppx_deriving
+  xmlm
   ounit2)
  (depopts
   lsp         ; https://github.com/ocaml/ocaml-lsp

src/dune

@@ -22,6 +22,7 @@
   dune-site
   dune-build-info
   camlzip ; main deps.
+  xmlm
   sexplib)
  ; for inline tests only (ppx_assert).
  (foreign_stubs

src/params.ml

@@ -56,6 +56,11 @@ let prefer_stdlib = ref false
 (* If set to true, the TLAPM will prefer the modules from the STDLIB
    instead of modules with the same names in the search path. *)
 
+type parser = | Tlapm | Sany
+let parser_backend = ref Tlapm
+
+let module_jar_paths = ref []
+
 let noproving = ref false (* Don't send any obligation to the back-ends. *)
 
 let printallobs = ref false

src/params.mli

@@ -7,6 +7,9 @@ val toolbox: bool ref
 val toolbox_vsn: int ref
 val use_stdin: bool ref
 val prefer_stdlib: bool ref
+type parser = | Tlapm | Sany
+val parser_backend: parser ref
+val module_jar_paths : string list ref
 
 (* expr/fmt.ml *)
 val debugging: string -> bool

src/paths.ml

@@ -15,15 +15,25 @@ let backend_paths =
 let stdlib_paths =
   site_paths Setup_paths.Sites.stdlib [ "lib"; "tlapm"; "stdlib" ]
 
+let backend_path_elems =
+  let site_bin bs = Filename.concat bs "bin" in
+  let site_isa bs = List.fold_left Filename.concat bs [ "Isabelle"; "bin" ] in
+  let site_paths bs = [ site_bin bs; site_isa bs ] in
+  List.concat (List.map site_paths backend_paths)
+
 (** If the backends site is not available ([]), then look for executables in the PATH,
       otherwise we are in the dune-based build and should look for the backends in the
       specified site locations. *)
 let backend_path_string =
-  let site_bin bs = Filename.concat bs "bin" in
-  let site_isa bs = List.fold_left Filename.concat bs [ "Isabelle"; "bin" ] in
-  let site_paths bs = [ site_bin bs; site_isa bs ] in
-  let path_elems = List.concat (List.map site_paths backend_paths) in
-  Printf.sprintf "%s:%s" (String.concat ":" path_elems) (Sys.getenv "PATH")
+  let paths = String.concat ":" backend_path_elems in
+  try Printf.sprintf "%s:%s" paths (Sys.getenv "PATH")
+  with Not_found -> paths
+
+
+let backend_classpath_string jar_file =
+  let classpath = List.map (fun path -> Filename.concat path jar_file) backend_path_elems |> String.concat ":" in
+  try Printf.sprintf "%s:%s" classpath (Sys.getenv "CLASSPATH")
+  with Not_found -> classpath
 
 let find_path_containing paths file =
   let find_actual path = Sys.file_exists (Filename.concat path file) in

src/paths.mli

@@ -1,4 +1,5 @@
 val backend_path_string : string
+val backend_classpath_string : string -> string
 val backend_paths : string list
 val stdlib_paths : string list
 val find_path_containing : string list -> string -> string option