From 8c3b7536ea13c4bec1bc8952fcb7823d90c2bc22 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 15 Dec 2024 12:18:00 -0500 Subject: [PATCH] Start using qcheck to test parser --- dune-project | 5 +++- hazel.opam | 4 +++ hazel.opam.locked | 10 +++++-- src/haz3lmenhir/AST.re | 59 ++++++++++++++++++++++++++++++------------ src/haz3lmenhir/dune | 9 +++++-- test/Test_Menhir.re | 32 +++++++++++++++++++++++ 6 files changed, 97 insertions(+), 22 deletions(-) diff --git a/dune-project b/dune-project index 4dd3442bc4..a8e9d11527 100644 --- a/dune-project +++ b/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 diff --git a/hazel.opam b/hazel.opam index 09ee887ab3..16ed5457ba 100644 --- a/hazel.opam +++ b/hazel.opam @@ -14,6 +14,7 @@ depends: [ "reason" {>= "3.12.0"} "ppx_yojson_conv_lib" "ppx_yojson_conv" + "incr_dom" "bisect_ppx" "omd" {>= "2.0.0~alpha4"} "ezjs_idb" @@ -25,6 +26,9 @@ depends: [ "ocamlformat" "junit_alcotest" {with-test} "ocaml-lsp-server" + "qcheck" + "qcheck-alcotest" + "ppx_deriving_qcheck" "odoc" {with-doc} ] build: [ diff --git a/hazel.opam.locked b/hazel.opam.locked index 856b83ad33..399042a839 100644 --- a/hazel.opam.locked +++ b/hazel.opam.locked @@ -10,7 +10,7 @@ homepage: "https://github.com/hazelgrove/hazel" bug-reports: "https://github.com/hazelgrove/hazel/issues" depends: [ "abstract_algebra" {= "v0.16.0"} - "alcotest" {= "1.8.0" & with-test} + "alcotest" {= "1.8.0"} "angstrom" {= "0.16.1"} "astring" {= "0.8.5"} "async" {= "v0.16.0"} @@ -38,8 +38,8 @@ depends: [ "bignum" {= "v0.16.0"} "bigstringaf" {= "0.10.0"} "bin_prot" {= "v0.16.0"} - "bonsai" {= "v0.16.0"} "bisect_ppx" {= "2.8.3"} + "bonsai" {= "v0.16.0"} "camlp-streams" {= "5.0.1"} "chrome-trace" {= "3.16.0"} "cmdliner" {= "1.3.0"} @@ -142,6 +142,7 @@ depends: [ "omd" {= "2.0.0~alpha4"} "ordering" {= "3.16.0"} "ordinal_abbreviation" {= "v0.16.0"} + "ounit2" {= "2.2.7"} "parsexp" {= "v0.16.0"} "patdiff" {= "v0.16.1"} "patience_diff" {= "v0.16.0"} @@ -157,6 +158,7 @@ depends: [ "ppx_custom_printf" {= "v0.16.0"} "ppx_derivers" {= "1.2.1"} "ppx_deriving" {= "6.0.2"} + "ppx_deriving_qcheck" {= "0.5"} "ppx_disable_unused_warnings" {= "v0.16.0"} "ppx_enumerate" {= "v0.16.0"} "ppx_expect" {= "v0.16.0"} @@ -193,6 +195,10 @@ depends: [ "protocol_version_header" {= "v0.16.0"} "ptime" {= "1.2.0" & with-test} "ptmap" {= "2.0.5"} + "qcheck" {= "0.23"} + "qcheck-alcotest" {= "0.23"} + "qcheck-core" {= "0.23"} + "qcheck-ounit" {= "0.23"} "re" {= "1.12.0"} "reason" {= "3.12.0"} "record_builder" {= "v0.16.0"} diff --git a/src/haz3lmenhir/AST.re b/src/haz3lmenhir/AST.re index d8798ded94..625e027659 100644 --- a/src/haz3lmenhir/AST.re +++ b/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]); +}; diff --git a/src/haz3lmenhir/dune b/src/haz3lmenhir/dune index d9a9683a19..1169266987 100644 --- a/src/haz3lmenhir/dune +++ b/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) diff --git a/test/Test_Menhir.re b/test/Test_Menhir.re index 359d8ee281..2f57753d86 100644 --- a/test/Test_Menhir.re +++ b/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), ];