Expose Misc.is_registered rather than Constraints.is_registered i…

…n SymbolicConstraints
colis-anr · Feb 26, 2020 · acb30bf · acb30bf
1 parent f335dc0
commit acb30bf
Show file tree

Hide file tree

Showing 2 changed files with 70 additions and 28 deletions.
diff --git a/src/colis.ml b/src/colis.ml
@@ -117,34 +117,55 @@ module FilesystemSpec = FilesystemSpec
 
 module Constraints = Colis_constraints
 
+let () =
+  (* Register the utilities to the mixed backend, which is used in interpreting the
+     interfaces for constraints and transducers equally *)
+  List.iter SymbolicUtility.Mixed.register [
+    (module Basics.True) ;
+    (module Basics.Colon) ;
+    (module Basics.False) ;
+    (module Basics.Echo) ;
+    (module Cp);
+    (module Dpkg) ;
+    (module DpkgMaintscriptHelper) ;
+    (module EmacsPackage.Install) ;
+    (module EmacsPackage.Remove) ;
+    (module Mkdir);
+    (module Mv);
+    (module Rm) ;
+    (module Test) ;
+    (module Test.Bracket) ;
+    (module Touch) ;
+    (module UpdateAlternatives) ;
+    (module UpdateMenus) ;
+    (module Which) ;
+    (module Which.Silent) ;
+    (* The Dark World *)
+    (module ColisInternalUnsafeTouch) ;
+  ]
+
 module SymbolicConstraints = struct
-  include SymbolicUtility.Constraints
+  open Constraints
 
-  let () =
-    let open SymbolicUtility in
-    List.iter Mixed.register [
-      (module Basics.True) ;
-      (module Basics.Colon) ;
-      (module Basics.False) ;
-      (module Basics.Echo) ;
-      (module Cp);
-      (module Dpkg) ;
-      (module DpkgMaintscriptHelper) ;
-      (module EmacsPackage.Install) ;
-      (module EmacsPackage.Remove) ;
-      (module Mkdir);
-      (module Mv);
-      (module Rm) ;
-      (module Test) ;
-      (module Test.Bracket) ;
-      (module Touch) ;
-      (module UpdateAlternatives) ;
-      (module UpdateMenus) ;
-      (module Which) ;
-      (module Which.Silent) ;
-      (* The Dark World *)
-      (module ColisInternalUnsafeTouch) ;
-    ]
+  type filesystem = SymbolicUtility.Constraints.filesystem = {
+    root: Var.t;
+    clause: Clause.sat_conj;
+    root0: Var.t option;
+  }
+
+  type state = SymbolicUtility.Constraints.state ={
+    filesystem: filesystem;
+    stdin: string list;
+    stdout: Common.Stdout.t;
+    log: Common.Stdout.t;
+  }
+
+  type sym_state = SymbolicUtility.Constraints.sym_state = {
+    context : Common.Context.context;
+    state : state;
+  }
+
+  let is_registered = SymbolicUtility.Mixed.is_registered
 
   let add_fs_spec_to_clause root clause fs_spec =
     let fs_clause = FilesystemSpec.compile root fs_spec in

diff --git a/src/colis.mli b/src/colis.mli
@@ -98,11 +98,32 @@ module FilesystemSpec = FilesystemSpec
 
 module Constraints = Colis_constraints
 
-(** The symbolic interpreter using constraints *)
+(** The symbolic interpreter using constraints on the mixed backend of SymbolicUtility *)
 module SymbolicConstraints : sig
   open Constraints
+  open Common
 
-  include module type of SymbolicUtility.Constraints
+  type filesystem = SymbolicUtility.Constraints.filesystem = {
+    root: Var.t;
+    clause: Clause.sat_conj;
+    root0: Var.t option;
+  }
+
+  type state = SymbolicUtility.Constraints.state = {
+      filesystem: filesystem;
+      stdin: string list;
+      stdout: Stdout.t;
+      log: Stdout.t;
+    }
+
+  type sym_state = SymbolicUtility.Constraints.sym_state = {
+    context : Context.context;
+    state : state;
+  }
+
+  (** Test if an utility is registerered in the mixed backend (the actual backend for this
+      module) *)
+  val is_registered : string -> bool
 
   (** [compile_fs_spec root conj fs_spec] creates a disjunction that represents the conjunction [conj] with constraints representing the filesystem specified by [fs_spec] *)
   val add_fs_spec_to_clause : Var.t -> Clause.sat_conj -> FilesystemSpec.t -> Clause.sat_conj list