Try base_quickcheck deriving

dune-project

@@ -38,6 +38,7 @@
   unionFind
   ocamlformat
   (junit_alcotest :with-test)
-  ocaml-lsp-server)) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
+  ocaml-lsp-server
+  (base_quickcheck (>= 0.17.0)))) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html

dune-workspace

@@ -3,7 +3,7 @@
 (env
  (dev
   (flags
-   (:standard -warn-error -A)))
+   (:standard -w +30 -warn-error -A)))
  (release
   (flags
    (:standard -warn-error +A-58))))

src/haz3lcore/dune

@@ -10,7 +10,8 @@
    js_of_ocaml-ppx
    ppx_let
    ppx_sexp_conv
-   ppx_deriving.show)))
+   ppx_deriving.show
+   base_quickcheck.ppx_quickcheck)))
 
 (env
  (dev

src/haz3lcore/dynamics/FilterAction.re

@@ -1,14 +1,14 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type action =
   | Step
   | Eval;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type count =
   | One
   | All;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t = (action, count);
 
 let string_of_t = v => {

src/haz3lcore/dynamics/InvalidOperationError.re

@@ -1,4 +1,4 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t =
   | InvalidOfString
   | IndexOutOfBounds

src/haz3lcore/dynamics/VarBstMap.re

@@ -1,5 +1,6 @@
 open Util;
 open Ppx_yojson_conv_lib.Yojson_conv;
+open Base_quickcheck;
 module Sexp = Sexplib.Sexp;
 
 module Inner = {
@@ -206,6 +207,9 @@ module Ordered = {
   let without_keys = (keys, m) => {
     filterk(((s, _)) => !List.exists(x => x == s, keys), m);
   };
+
+  let quickcheck_observer_t_ = __ => Observer.opaque;
+  let quickcheck_shrinker_t_ = __ => Shrinker.atomic;
 };
 
 include VarBstMap0;

src/haz3lcore/dynamics/VarBstMap.rei

@@ -174,4 +174,9 @@ module Ordered: {
     [without_keys] removes all entires with the given keys from the map
    */
   let without_keys: (list(Var.t), t_('a)) => t_('a);
+
+  let quickcheck_observer_t_:
+    Base_quickcheck.Observer.t('a) => Base_quickcheck.Observer.t(t_('a));
+  let quickcheck_shrinker_t_:
+    Base_quickcheck.Shrinker.t('a) => Base_quickcheck.Shrinker.t(t_('a));
 };

src/haz3lcore/lang/Operators.re

@@ -1,21 +1,21 @@
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_bool =
   | Not;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_meta =
   | Unquote;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un_int =
   | Minus;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_bool =
   | And
   | Or;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_int =
   | Plus
   | Minus
@@ -29,7 +29,7 @@ type op_bin_int =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_float =
   | Plus
   | Minus
@@ -43,25 +43,25 @@ type op_bin_float =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin_string =
   | Concat
   | Equals;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_un =
   | Meta(op_un_meta)
   | Int(op_un_int)
   | Bool(op_un_bool);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type op_bin =
   | Int(op_bin_int)
   | Float(op_bin_float)
   | Bool(op_bin_bool)
   | String(op_bin_string);
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type ap_direction =
   | Forward
   | Reverse;

src/haz3lcore/lang/term/IdTagged.re

@@ -1,6 +1,7 @@
 open Util;
+open Base_quickcheck;
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t('a) = {
   [@show.opaque]
   ids: list(Id.t),

src/haz3lcore/statics/Constructor.re

@@ -1,6 +1,7 @@
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = string;
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
+type t =
+  [@quickcheck.generator Generator.string_of(Generator.char_alpha)] string;
 
 let equal = String.equal;

src/haz3lcore/statics/ConstructorMap.re

@@ -1,13 +1,13 @@
 open Util.OptUtil.Syntax;
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type variant('a) =
   | Variant(Constructor.t, list(Id.t), option('a))
   | BadEntry('a);
 
 // Invariant: Must not have duplicate constructors
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type t('a) = list(variant('a));
 
 let mk =

src/haz3lcore/statics/TermBase.re

@@ -1,8 +1,9 @@
 open Util;
+open Base_quickcheck;
 
 let continue = x => x;
 let stop = (_, x) => x;
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type deferral_position_t =
   | InAp
   | OutsideAp;
@@ -45,8 +46,7 @@ type deferral_position_t =
      structural equality except for the case of closures, where it just compares
      the id of the closure.
  */
-
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 type any_t =
   | Exp(exp_t)
   | Pat(pat_t)
@@ -146,7 +146,9 @@ and rul_term =
   | Hole(list(any_t))
   | Rules(exp_t, list((pat_t, exp_t)))
 and rul_t = IdTagged.t(rul_term)
-and environment_t = VarBstMap.Ordered.t_(exp_t)
+and environment_t =
+  [@quickcheck.generator Generator.return(VarBstMap.Ordered.empty)]
+  VarBstMap.Ordered.t_(exp_t)
 and closure_environment_t = (Id.t, environment_t)
 and stepper_filter_kind_t =
   | FilterStepper(filter)

src/haz3lcore/statics/Var.re

@@ -1,7 +1,8 @@
 open Util;
-
-[@deriving (show({with_path: false}), sexp, yojson)]
-type t = string;
+open Base_quickcheck;
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
+type t =
+  [@quickcheck.generator Generator.string_of(Generator.char_alpha)] string;
 
 let eq = String.equal;
 

src/haz3lcore/tiles/Id.re

@@ -1,5 +1,5 @@
 open Util;
-
+open Base_quickcheck;
 /* ID FAQ
 
    WHATS AN ID?
@@ -34,7 +34,7 @@ open Util;
 
    */
 
-[@deriving (show({with_path: false}), sexp, yojson)]
+[@deriving (show({with_path: false}), sexp, yojson, quickcheck)]
 let sexp_of_t: Uuidm.t => Sexplib.Sexp.t =
   t => Sexplib.Sexp.Atom(Uuidm.to_string(t));
 
@@ -59,6 +59,9 @@ let t_of_yojson: Yojson.Safe.t => Uuidm.t =
 type t = Uuidm.t;
 
 let mk: unit => t = Uuidm.v4_gen(Random.State.make_self_init());
+let quickcheck_generator = Generator.return(mk()); // TODO
+let quickcheck_observer = Observer.opaque;
+let quickcheck_shrinker = Shrinker.atomic;
 
 let compare: (t, t) => int = Uuidm.compare;
 let to_string: (~upper: bool=?, t) => string = Uuidm.to_string;