Add lists to pbt for menhir

hazelgrove · Dec 15, 2024 · 542f10f · 542f10f
1 parent 8c3b753
commit 542f10f
Show file tree

Hide file tree

Showing 2 changed files with 53 additions and 10 deletions.
diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re
@@ -180,9 +180,46 @@ let arb_ident =
 
 let arb_var = QCheck.(map(x => Var(x), arb_ident));
 
-let arb_exp_sized = (size: int): QCheck.arbitrary(exp) => {
-  open QCheck;
-  let i = QCheck.small_int;
-  let foo = arb_typ_sized;
-  oneof([arb_int, arb_str, arb_float, arb_var]);
-};
+let arb_exp_sized: QCheck.arbitrary(exp) =
+  QCheck.(
+    let leaf = oneof([arb_int, arb_str, arb_float, arb_var]);
+
+    let gen: Gen.t(exp) =
+      QCheck.Gen.sized_size(
+        QCheck.Gen.int_range(0, 10), // Currently only size 10
+        QCheck.Gen.fix((self, n) => {
+          switch (n) {
+          | 0 => leaf.gen
+          | _ =>
+            print_endline("Size: " ++ string_of_int(n));
+            let list_sizes =
+              if (n <= 1) {
+                // Bug in nat_split for size=0
+                Gen.pure([|0, 0, 0, 0, 0|]);
+              } else {
+                QCheck.Gen.nat_split(
+                  ~size=n - 1,
+                  5 // Make different size lists
+                );
+              };
+            let lists_gen =
+              Gen.map(
+                (sizes: array(int)) => {
+                  let sizes = Array.to_list(sizes);
+                  let exps = List.map((size: int) => self(size), sizes);
+                  let flattened = Gen.flatten_l(exps);
+                  let foo =
+                    Gen.map((exps: list(exp)) => ListExp(exps), flattened);
+                  foo;
+                },
+                list_sizes,
+              );
+            let foo = Gen.join(lists_gen);
+
+            Gen.oneof([leaf.gen, foo]);
+          }
+        }),
+      );
+
+    QCheck.make(gen)
+  ); // TODO Printers, shrinkers stuff
diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re
@@ -88,8 +88,9 @@ let parser_test = (name: string, exp: Term.Exp.t, actual: string) =>
     },
   );
 
-let menhir_maketerm_equivalent_test = (name: string, actual: string) =>
-  test_case(name, `Quick, () => {
+let menhir_maketerm_equivalent_test =
+    (~speed_level=`Quick, name: string, actual: string) =>
+  test_case(name, speed_level, () => {
     alco_check(
       "Menhir parse matches MakeTerm parse",
       make_term_parse(actual),
@@ -246,8 +247,8 @@ let i = ref(0);
 let qcheck_menhir_maketerm_equivalent_test =
   QCheck.Test.make(
     ~name="Menhir and maketerm are equivalent",
-    ~count=1000,
-    AST.arb_exp_sized(1),
+    ~count=100,
+    AST.arb_exp_sized,
     exp => {
       let core_exp = Conversion.Exp.of_menhir_ast(exp);
 
@@ -610,6 +611,7 @@ let tests = [
     "true && 23 < int_of_float(51.00)" // TODO This looks like a bug in MakeTerm
   ),
   menhir_maketerm_equivalent_test(
+    ~speed_level=`Slow,
     "Altered Documentation Buffer: Basic Reference",
     {|
 let empty_hole = ? in
@@ -715,6 +717,7 @@ test 2 + 2 == 5 end;
   // TODO This is an issue with `int_of_float` being parsed
   // as a builtin function in menhir and a Var in MakeTerm
   menhir_maketerm_equivalent_test(
+    ~speed_level=`Slow,
     "Altered Documentation Buffer: Projectors",
     {|
 let fold = (((((((((((()))))))))))) in
@@ -734,6 +737,7 @@ if true && (23 < int_of_float(51.00))
 then ______ else "its: " ++ box    |},
   ),
   menhir_maketerm_equivalent_test(
+    ~speed_level=`Slow,
     "Altered Documentation Buffer: Types & Static Errors",
     {|
 let _ = unbound in
@@ -782,6 +786,7 @@ let _: [Int] = 1::[2.0] in
 |},
   ),
   menhir_maketerm_equivalent_test(
+    ~speed_level=`Slow,
     "Altered Documentation Buffer: adt dynamics",
     {|
 type Exp =
@@ -851,6 +856,7 @@ Ok(Lam("bro", Var("bro")))) end
   ),
   menhir_maketerm_equivalent_test(
     // Variable names are renamed due to lexing overtaking e, t, p, and tp
+    ~speed_level=`Slow,
     "Altered Documentation Buffer: Polymorphism",
     {|let id = typfun A -> (fun (x : A) -> x) in
 let ex1 = id@<Int>(1) in