Merge pull request #215 from jmid/rename-base-modules

Rename base modules

Author: jmid

doc/example/lin_tests_dsl.ml

@@ -7,7 +7,7 @@ struct
   let init () = Hashtbl.create ~random:false 42
   let cleanup _ = ()
 
-  open Lin_base
+  open Lin
   let a,b = char_printable,nat_small
   let api =
     [ val_ "Hashtbl.add"    Hashtbl.add    (t @-> a @-> b @-> returning unit);

doc/example/stm_tests.ml

@@ -1,5 +1,5 @@
 open QCheck
-open STM_base
+open STM
 
 (** parallel STM tests of Hashtbl *)
 

doc/paper-examples/lin_tests_dsl.ml

@@ -8,7 +8,7 @@ struct
   let init () = Hashtbl.create ~random:false 42
   let cleanup _ = ()
 
-  open Lin_base
+  open Lin
   let a,b = char_printable,nat_small
   let api =
     [ val_ "Hashtbl.clear"    Hashtbl.clear    (t @-> returning unit);

doc/paper-examples/stm_tests.ml

@@ -1,5 +1,5 @@
 open QCheck
-open STM_base
+open STM
 
 (** parallel STM tests of Hashtbl *)
 

lib/STM_base.ml renamed to lib/STM.ml

@@ -63,7 +63,7 @@ type res =
 let show_res (Res ((_,show), v)) = show v
 
 (** The specification of a state machine. *)
-module type STM_spec =
+module type Spec =
 sig
   type cmd
   (** The type of commands *)
@@ -109,9 +109,9 @@ sig
 end
 
 
-module STM_internal =
+module Internal =
 struct
-  module Make(Spec : STM_spec) = struct
+  module Make(Spec : Spec) = struct
 
     let rec gen_cmds arb s fuel =
       Gen.(if fuel = 0

lib/STM_base.mli renamed to lib/STM.mli

@@ -76,7 +76,7 @@ val show_res : res -> string
 
 
 (** The specification of a state machine. *)
-module type STM_spec =
+module type Spec =
 sig
   type cmd
   (** The type of commands *)
@@ -127,13 +127,13 @@ sig
 end
 
 
-module STM_internal : sig
+module Internal : sig
 open QCheck
 (** Internal helper module to build STM tests. *)
 
 
 (** Derives a test framework from a state machine specification. *)
-module Make (Spec : STM_spec) :
+module Make (Spec : Spec) :
 sig
   (** {3 The resulting test framework derived from a state machine specification} *)
 

lib/STM_domain.ml

@@ -1,10 +1,10 @@
-open STM_base
+open STM
 
-module Make (Spec: STM_spec) = struct
+module Make (Spec: Spec) = struct
 
   open Util
   open QCheck
-  open STM_internal.Make(Spec)
+  open Internal.Make(Spec)
 
   let check_obs = check_obs
   let arb_cmds_par = arb_cmds_par

lib/STM_domain.mli

@@ -1,8 +1,8 @@
 (** Module for building parallel STM tests over [Domain]s *)
 
-module Make : functor (Spec : STM_base.STM_spec) ->
+module Make : functor (Spec : STM.Spec) ->
   sig
-    val check_obs : (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> (Spec.cmd * STM_base.res) list -> Spec.state -> bool
+    val check_obs : (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> Spec.state -> bool
     (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref]
         and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
 
@@ -15,7 +15,7 @@ module Make : functor (Spec : STM_base.STM_spec) ->
     val shrink_triple : (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.Shrink.t
     (** [shrink_triple arb0 arb1 arb2] is a [Shrinker.t] for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
 
-    val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM_base.res) list
+    val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut]
         and returns the list of corresponding [cmd] and result pairs. *)
 

lib/STM_sequential.ml

@@ -1,9 +1,9 @@
-open STM_base
+open STM
 
-module Make (Spec: STM_spec) = struct
+module Make (Spec: Spec) = struct
 
   open QCheck
-  open STM_internal.Make(Spec)
+  open Internal.Make(Spec)
 
   (* re-export some functions *)
   let cmds_ok        = cmds_ok

lib/STM_sequential.mli

@@ -1,6 +1,6 @@
 (** Module for building sequential STM tests *)
 
-module Make : functor (Spec : STM_base.STM_spec) ->
+module Make : functor (Spec : STM.Spec) ->
   sig
     val cmds_ok : Spec.state -> Spec.cmd list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).