Merge pull request #189 from jmid/rm-addgc

Remove STM_spec.AddGC functor

Author: jmid

lib/STM_spec.ml

@@ -105,51 +105,3 @@ sig
       model's result.
       Note: [s] is in this case the model's state prior to command execution. *)
 end
-
-module AddGC(Spec : Spec) : Spec = struct
-  type cmd =
-    | GC_minor
-    | UserCmd of Spec.cmd
-
-  type state = Spec.state
-  type sut   = Spec.sut
-
-  let init_state  = Spec.init_state
-  let init_sut () = Spec.init_sut ()
-  let cleanup sut = Spec.cleanup sut
-
-  let show_cmd c = match c with
-    | GC_minor -> "<GC.minor>"
-    | UserCmd c -> Spec.show_cmd c
-
-  let gen_cmd s =
-    (Gen.frequency
-       [(1,Gen.return GC_minor);
-        (5,Gen.map (fun c -> UserCmd c) (Spec.arb_cmd s).gen)])
-
-  let shrink_cmd s c = match c with
-    | GC_minor  -> Iter.empty
-    | UserCmd c ->
-       match (Spec.arb_cmd s).shrink with
-       | None     -> Iter.empty (* no shrinker provided *)
-       | Some shk -> Iter.map (fun c' -> UserCmd c') (shk c)
-
-  let arb_cmd s = make ~print:show_cmd ~shrink:(shrink_cmd s) (gen_cmd s)
-
-  let next_state c s = match c with
-    | GC_minor  -> s
-    | UserCmd c -> Spec.next_state c s
-
-  let precond c s = match c with
-    | GC_minor  -> true
-    | UserCmd c -> Spec.precond c s
-
-  let run c s = match c with
-    | GC_minor  -> (Gc.minor (); Res (unit, ()))
-    | UserCmd c -> Spec.run c s
-
-  let postcond c s r = match c,r with
-    | GC_minor,  Res ((Unit,_),_) -> true
-    | UserCmd c, r -> Spec.postcond c s r
-    | _,_ -> false
-end

lib/STM_spec.mli

@@ -122,5 +122,3 @@ sig
       model's result. A [postcond] function should be a pure.
       Note: [s] is in this case the model's state prior to command execution. *)
 end
-
-module AddGC : functor (Spec : Spec) -> Spec

src/neg_tests/ref_stm_dom_tests.ml

@@ -2,17 +2,9 @@ open Ref_stm_spec
 
 module RT_int   = STM_domain.Make(RConf_int)
 module RT_int64 = STM_domain.Make(RConf_int64)
-
-(*module RConf_int_GC = STM_base.AddGC(RConf_int)*)
-(*module RConf_int64_GC = STM_base.AddGC(RConf_int64)*)
-
-(*module RT_int_GC = STM_domain.Make(RConf_int_GC)*)
-(*module RT_int64_GC = STM_domain.Make(RConf_int64_GC)*)
 ;;
 QCheck_runner.run_tests_main
   (let count = 1000 in
    [RT_int.neg_agree_test_par      ~count ~name:"STM int ref test parallel";
-  (*RT_int_GC.neg_agree_test_par   ~count ~name:"STM int ref test parallel (w/AddGC functor)";*)
     RT_int64.neg_agree_test_par    ~count ~name:"STM int64 ref test parallel";
-  (*RT_int64_GC.neg_agree_test_par ~count ~name:"STM int64 ref test parallel (w/AddGC functor)";*)
    ])

src/neg_tests/ref_stm_thread_tests.ml

@@ -2,17 +2,9 @@ open Ref_stm_spec
 
 module RT_int   = STM_thread.Make(RConf_int)
 module RT_int64 = STM_thread.Make(RConf_int64)
-
-(*module RConf_int_GC   = STM_base.AddGC(RConf_int)*)
-(*module RConf_int64_GC = STM_base.AddGC(RConf_int64)*)
-
-(*module RT_int_GC   = STM_thread.Make(RConf_int_GC)*)
-(*module RT_int64_GC = STM_thread.Make(RConf_int64_GC)*)
 ;;
 QCheck_runner.run_tests_main
   (let count = 1000 in
    [RT_int.agree_test_conc       ~count ~name:"STM int ref test with Thread";
-  (*RT_int_GC.agree_test_conc    ~count ~name:"STM int ref test with Thread (w/AddGC functor)";*)
     RT_int64.neg_agree_test_conc ~count ~name:"STM int64 ref test with Thread";
-  (*RT_int64_GC.agree_test_conc  ~count ~name:"STM int64 ref test with Thread (w/AddGC functor)";*)
    ])