From 53c9b78fc96266e4d76ba8961888211fb27644a0 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 15 Sep 2024 13:07:54 +0300 Subject: [PATCH 1/6] Expose dequeue from the tlapm_lib, use Module.T instead M_t. Signed-off-by: Karolis Petrauskas --- src/tlapm_lib.ml | 5 +++-- src/tlapm_lib.mli | 3 ++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index 3ad177c3..0321e8ef 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -13,6 +13,7 @@ module Property = Property module Proof = Proof module Expr = Expr module Util = Util +module Deque = Deque module Loc = Loc module Ctx = Ctx module Backend = Backend @@ -650,8 +651,8 @@ 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 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 diff --git a/src/tlapm_lib.mli b/src/tlapm_lib.mli index 41916da6..57de4b9b 100644 --- a/src/tlapm_lib.mli +++ b/src/tlapm_lib.mli @@ -7,6 +7,7 @@ module Property = Property module Proof = Proof module Expr = Expr module Util = Util +module Deque = Deque module Loc = Loc module Ctx = Ctx module Backend = Backend @@ -24,7 +25,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. *) From da6ad300755345896a5a5c29a545df087ea95adf Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Sun, 15 Sep 2024 13:12:48 +0300 Subject: [PATCH 2/6] Export tlapm_lib for for other projects. Signed-off-by: Karolis Petrauskas --- src/dune | 1 + src/tlapm_lib.mli | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/src/dune b/src/dune index 50199be2..5683565b 100644 --- a/src/dune +++ b/src/dune @@ -13,6 +13,7 @@ (library (name tlapm_lib) + (public_name tlapm) (modules (:standard \ tlapm test_schedule why3_interface abstractor)) (libraries diff --git a/src/tlapm_lib.mli b/src/tlapm_lib.mli index 57de4b9b..ec04b354 100644 --- a/src/tlapm_lib.mli +++ b/src/tlapm_lib.mli @@ -1,5 +1,9 @@ (* * 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 From caefe8181928b871a7ab8a3d40d61720dc3069a4 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Mon, 30 Sep 2024 10:37:29 +0300 Subject: [PATCH 3/6] Expose builtin module. Signed-off-by: Karolis Petrauskas --- src/tlapm_lib.ml | 1 + src/tlapm_lib.mli | 1 + 2 files changed, 2 insertions(+) diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index 0321e8ef..0febc1c3 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -17,6 +17,7 @@ module Deque = Deque module Loc = Loc module Ctx = Ctx module Backend = Backend +module Builtin = Builtin open Proof.T diff --git a/src/tlapm_lib.mli b/src/tlapm_lib.mli index ec04b354..4f9544b4 100644 --- a/src/tlapm_lib.mli +++ b/src/tlapm_lib.mli @@ -15,6 +15,7 @@ module Deque = Deque module Loc = Loc module Ctx = Ctx module Backend = Backend +module Builtin = Builtin val main : string list -> unit val init : unit -> unit From b8b2611db2d5def2985f84afee24c5261be86835 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Wed, 2 Oct 2024 23:32:00 +0300 Subject: [PATCH 4/6] Fix printing of the QED step. Signed-off-by: Karolis Petrauskas --- src/proof/p_fmt.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proof/p_fmt.ml b/src/proof/p_fmt.ml index b71e6c43..b6a5e98b 100644 --- a/src/proof/p_fmt.ml +++ b/src/proof/p_fmt.ml @@ -125,7 +125,7 @@ let rec pp_print_proof cx ff prf = cx) cx ff inits in - fprintf ff "@[%s%s QED%a@]" + fprintf ff "@[%s%s QED %a@]" (step_name prf) (step_dot prf) (pp_print_qed_step(*proof_nl*) cx) qed | Error msg -> From 38c2ea958249ccc81f7e90342bb975918144ea02 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Wed, 2 Oct 2024 23:56:30 +0300 Subject: [PATCH 5/6] Print EXTENDS for a parsed/final module. Signed-off-by: Karolis Petrauskas --- src/module/m_fmt.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/module/m_fmt.ml b/src/module/m_fmt.ml index b3432109..bf8397b3 100644 --- a/src/module/m_fmt.ml +++ b/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 "@[---- MODULE %s ----@," m.core.name.core ; begin match m.core.stage with + | Final _ | Parsed when m.core.extendees <> [] -> fprintf ff "EXTENDS @[%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 From 3e4f492bbee88632cea95426c7375c20148ce5aa Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Thu, 3 Oct 2024 00:35:01 +0300 Subject: [PATCH 6/6] Experiment: modctx_of_mule Signed-off-by: Karolis Petrauskas --- src/tlapm_lib.ml | 20 +++++++++++++++----- src/tlapm_lib.mli | 8 ++++++++ 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index 0febc1c3..69d7edd8 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -616,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 ; @@ -652,6 +649,19 @@ 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 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 diff --git a/src/tlapm_lib.mli b/src/tlapm_lib.mli index 4f9544b4..46afd00a 100644 --- a/src/tlapm_lib.mli +++ b/src/tlapm_lib.mli @@ -20,6 +20,14 @@ 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 ->