From 5a53b0fc0100bff10c9285bf1291b7cc2f41267b Mon Sep 17 00:00:00 2001 From: Benedikt Becker Date: Thu, 9 Apr 2020 15:30:40 +0200 Subject: [PATCH] Clean alias for utility_context in SymbolicUtility --- src/symbolic/symbolicUtility.ml | 13 ++++++------- src/symbolic/symbolicUtility.mli | 13 ++++++------- src/symbolic/utilities/mkdir.ml | 1 - src/symbolic/utilities/mkdir.mli | 2 +- 4 files changed, 13 insertions(+), 16 deletions(-) diff --git a/src/symbolic/symbolicUtility.ml b/src/symbolic/symbolicUtility.ml index a565cc38..1e9715bb 100644 --- a/src/symbolic/symbolicUtility.ml +++ b/src/symbolic/symbolicUtility.ml @@ -315,12 +315,6 @@ module MakeInterpreter (Filesystem: FILESYSTEM) = struct end end -module UtilityContext = struct - type context = utility_context = { - cwd: Path.normal; - env: string Env.SMap.t; - args: string list; - } end (* Constraints *) @@ -434,6 +428,12 @@ module Mixed = struct include MakeInterpreter (MixedImplementation) include MakeSpecifications (MixedImplementation) + type context = utility_context = { + cwd: Path.normal; + env: string Env.SMap.t; + args: string list; + } + let state_from_constraints (s : Constraints.state) : state = { filesystem=MixedImplementation.Constraints s.filesystem; stdin=s.stdin; @@ -486,7 +486,6 @@ end module ConstraintsCompatibility = struct include Mixed - include UtilityContext let success_case ~descr ?stdout constraints = success_case ~descr ?stdout (case_spec ~constraints ()) diff --git a/src/symbolic/symbolicUtility.mli b/src/symbolic/symbolicUtility.mli index e9ce7bc1..85065521 100644 --- a/src/symbolic/symbolicUtility.mli +++ b/src/symbolic/symbolicUtility.mli @@ -199,12 +199,6 @@ module MakeInterpreter (Filesystem: FILESYSTEM) : sig end end -module UtilityContext : sig - type context = utility_context = { - cwd: Path.normal; - env: string Env.SMap.t; - args: string list; - } end (** {1 Constraints backend} *) @@ -288,6 +282,12 @@ module Mixed : sig include module type of MakeInterpreter (MixedImplementation) include module type of MakeSpecifications (MixedImplementation) + type context = utility_context = { + cwd: Path.normal; + env: string Env.SMap.t; + args: string list; + } + (** Symbolically interprete a program using the constraints backend *) val interp_program_constraints : input -> Constraints.sym_state list -> program -> (Constraints.state list * Constraints.state list * Constraints.state list) @@ -299,7 +299,6 @@ end engine: Create mixed utilities with the interface of constraints-based utilities *) module ConstraintsCompatibility : sig include module type of Mixed - include module type of UtilityContext val success_case: descr:string -> ?stdout:Stdout.t -> Constraints.case_spec -> case val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> Constraints.case_spec -> case diff --git a/src/symbolic/utilities/mkdir.ml b/src/symbolic/utilities/mkdir.ml index 2213d14b..c8b80f08 100644 --- a/src/symbolic/utilities/mkdir.ml +++ b/src/symbolic/utilities/mkdir.ml @@ -1,7 +1,6 @@ open Format open Colis_constraints open Clause -open SymbolicUtility.UtilityContext open SymbolicUtility.Mixed let name = "mkdir" diff --git a/src/symbolic/utilities/mkdir.mli b/src/symbolic/utilities/mkdir.mli index 054dc19e..5a1f0642 100644 --- a/src/symbolic/utilities/mkdir.mli +++ b/src/symbolic/utilities/mkdir.mli @@ -1,5 +1,5 @@ (** Symbolic execution of mkdir *) -open SymbolicUtility.ConstraintsCompatibility +open SymbolicUtility.Mixed val name : string val interprete : context -> utility