Skip to content

Commit

Permalink
Fix constructor ident
Browse files Browse the repository at this point in the history
- Add stubbed test for menhir/exptosegment invertibility
  • Loading branch information
7h3kk1d committed Dec 16, 2024
1 parent 3d11a0d commit 428faaa
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 6 deletions.
7 changes: 2 additions & 5 deletions src/haz3lmenhir/AST.re
Original file line number Diff line number Diff line change
Expand Up @@ -270,11 +270,8 @@ let rec gen_exp_sized = (n: int): QCheck.Gen.t(exp) =>
),
Gen.map(exp => Test(exp), self(n - 1)),
Gen.map2(
(name, typ) => {
print_endline("Generating constructor");
Constructor(name, typ);
},
arb_ident.gen, // Replace with constructor type
(name, typ) => {Constructor(name, typ)},
arb_constructor_ident.gen,
gen_typ_sized(n - 1),
),
]);
Expand Down
47 changes: 46 additions & 1 deletion test/Test_Menhir.re
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,51 @@ let qcheck_menhir_maketerm_equivalent_test =
Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed);

Haz3lcore.DHExp.fast_equal(make_term_parsed, menhir_parsed_converted);
// && menhir_parsed == exp; // TODO Add this as separate property
},
);

// TODO This fails due to types not being serialized on constructors
// We should do a pass before the equality check that removes the types on the constructors and check equality after
let qcheck_menhir_serialized_equivalent_test =
QCheck.Test.make(
~name="Menhir through ExpToSegment and back",
~count=100,
QCheck.make(~print=AST.show_exp, AST.gen_exp_sized(3)),
exp => {
let core_exp = Conversion.Exp.of_menhir_ast(exp);

// TODO Maybe only do this when necessary.
// TODO Check with Matthew if I'm using this correctly
// Add parens around tuples
let core_exp =
Exp.map_term(
~f_exp=
(cont, e) =>
switch (e.term) {
| Tuple(es) =>
Parens(Tuple(es |> List.map(cont)) |> Exp.fresh)
|> Exp.fresh
| _ => cont(e)
},
core_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 menhir_parsed = Haz3lmenhir.Interface.parse_program(serialized);
print_endline("Serialized: " ++ serialized);
print_endline("Menhir parsed: " ++ AST.show_exp(menhir_parsed));
print_endline("Original" ++ AST.show_exp(exp));
menhir_parsed == exp;
},
);

Expand Down Expand Up @@ -905,4 +949,5 @@ let ex5 = list_of_mylist(x) in
|},
),
QCheck_alcotest.to_alcotest(qcheck_menhir_maketerm_equivalent_test),
// QCheck_alcotest.to_alcotest(qcheck_menhir_serialized_equivalent_test),
];

0 comments on commit 428faaa

Please sign in to comment.