Start using qcheck to test parser

dune-project

@@ -40,6 +40,9 @@
   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
+  qcheck
+  qcheck-alcotest
+  ppx_deriving_qcheck)) ; 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

src/haz3lmenhir/AST.re

@@ -1,13 +1,13 @@
 open Sexplib.Std;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type filter_action =
   | Pause
   | Debug
   | Hide
   | Eval;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_bin_float =
   | Plus
   | Minus
@@ -21,12 +21,12 @@ type op_bin_float =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_bin_bool =
   | And
   | Or;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_bin_int =
   | Plus
   | Minus
@@ -40,49 +40,49 @@ type op_bin_int =
   | Equals
   | NotEquals;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_bin_string =
   | Concat
   | Equals;
 
 // TODO Rename to match others
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type binOp =
   | IntOp(op_bin_int)
   | FloatOp(op_bin_float)
   | StringOp(op_bin_string)
   | BoolOp(op_bin_bool);
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_un_meta =
   | Unquote;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_un_int =
   | Minus;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_un_bool =
   | Not;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type op_un =
   | Meta(op_un_meta)
   | Int(op_un_int)
   | Bool(op_un_bool);
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type typ_provenance =
   | Internal
   | EmptyHole;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type tpat =
-  | InvalidTPat(string)
+  | InvalidTPat([@arb small_printable_gen] string)
   | EmptyHoleTPat
   | VarTPat(string);
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type typ =
   | IntType
   | StringType
@@ -100,7 +100,7 @@ type typ =
   | ForallType(tpat, typ)
   | RecType(tpat, typ);
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type pat =
   | CastPat(pat, typ, typ)
   | EmptyHolePat
@@ -117,12 +117,12 @@ type pat =
   | ApPat(pat, pat)
   | InvalidPat(string);
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type if_consistency =
   | Consistent
   | Inconsistent;
 
-[@deriving (show({with_path: false}), sexp)]
+[@deriving (show({with_path: false}), sexp, qcheck)]
 type deferral_pos =
   | InAp
   | OutsideAp;
@@ -161,3 +161,28 @@ type exp =
   | TypAp(exp, typ)
   | DynamicErrorHole(exp, string)
   | TyAlias(tpat, typ, exp);
+
+let arb_int = QCheck.(map(x => Int(x), small_int));
+
+let arb_str =
+  QCheck.(map(x => String(x), string_small_of(Gen.char_range('a', 'z')))); // Make strings anything other than `"`"
+
+// Floats are positive because we use UnOp minus
+let arb_float = QCheck.(map(x => Float(x), pos_float));
+
+// ['a'-'z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
+// Can't be t, e, tp, or p because of the lexer
+let arb_ident =
+  QCheck.(
+    let arb_alpha = Gen.char_range('a', 'd'); // TODO make this support full indent instead of just lower alpha
+    string_gen_of_size(Gen.int_range(1, 5), arb_alpha)
+  );
+
+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]);
+};

src/haz3lmenhir/dune

@@ -1,11 +1,16 @@
 (library
  (name haz3lmenhir)
- (libraries util re sexplib unionFind haz3lcore)
+ (libraries util re sexplib unionFind haz3lcore qcheck-alcotest)
  (modules AST Conversion Interface Lexer Parser)
  (instrumentation
   (backend bisect_ppx))
  (preprocess
-  (pps ppx_let ppx_sexp_conv ppx_deriving.show ppx_yojson_conv)))
+  (pps
+   ppx_let
+   ppx_sexp_conv
+   ppx_deriving.show
+   ppx_yojson_conv
+   ppx_deriving_qcheck)))
 
 (ocamllex Lexer)
 

test/Test_Menhir.re

@@ -241,6 +241,37 @@ let menhir_doesnt_crash_test = (name, src) =>
     },
   );
 
+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),
+    exp => {
+      let core_exp = Conversion.Exp.of_menhir_ast(exp);
+
+      let segment =
+        ExpToSegment.exp_to_segment(
+          ~settings=
+            ExpToSegment.Settings.of_core(
+              ~inline=true, // TODO What does inline do?
+              CoreSettings.off,
+            ),
+          core_exp,
+        );
+
+      let serialized = Printer.of_segment(~holes=Some("?"), segment);
+      let make_term_parsed = make_term_parse(serialized);
+      let menhir_parsed =
+        Haz3lmenhir.Conversion.Exp.of_menhir_ast(
+          Haz3lmenhir.Interface.parse_program(serialized),
+        );
+
+      Haz3lcore.DHExp.fast_equal(make_term_parsed, menhir_parsed);
+    },
+  );
+
 let tests = [
   parser_test("Integer Literal", Int(8) |> Exp.fresh, "8"),
   parser_test("Fun", fun_exp, "fun x -> x"),
@@ -850,4 +881,5 @@ let ex5 = list_of_mylist(x) in
 (ex1, ex2, ex3, ex4, ex5)
     |},
   ),
+  QCheck_alcotest.to_alcotest(qcheck_menhir_maketerm_equivalent_test),
 ];