Skip to content

Commit

Permalink
progress on testing
Browse files Browse the repository at this point in the history
  • Loading branch information
@cyrus-
cyrus- committed Feb 13, 2025
1 parent c04e5a2 commit d30ff79
Show file tree
Hide file tree
Showing 4 changed files with 125 additions and 85 deletions.
107 changes: 70 additions & 37 deletions test/Test_Coverage.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,13 +4,42 @@ open Haz3lcore;
let testable_typ = testable(Fmt.using(Typ.show, Fmt.string), Typ.fast_equal);
let testable_info_error_pat =
testable(Fmt.using(Info.show_error_pat, Fmt.string), Info.equal_error_pat);
let testable_list_uuidm = testable(Fmt.list(Uuidm.pp), (==));

let statics = Statics.mk(CoreSettings.on, Builtins.ctx_init);
let info_error_of_pat_id = (f: Exp.t, id: Id.t): option(Info.error_pat) => {
Statics.get_pat_error_at(statics(f), id);
};

let alco_check = Alcotest.option(testable_typ) |> Alcotest.check;
let no_errors = (name, exp) => {
test_case(
name,
`Quick,
() => {
let s = statics(exp);
let errors = Statics.Map.error_ids(s);
Alcotest.check(testable_list_uuidm, "Static Errors", [], errors);
},
);
};

let parse_exp = (s: string) => {
switch (MakeTerm.parse_exp(s)) {
| Some(e) => e
| None => Alcotest.fail("Failed to parse expression: " ++ s)
};
};

let parse_menhir = (s: string) => {
let (e, _) =
Haz3lmenhir.Conversion.Exp.of_menhir_ast(
Haz3lmenhir.Interface.parse_program(s),
);
// print_endline("Parsed: " ++ Exp.show(e));
// print_endline("Original: " ++ (parse_exp(s) |> Exp.show));
// failwith("X");
e;
};

let reusable_id = Id.mk();
let reusable_pat: TermBase.pat_term => TermBase.pat_t =
Expand All @@ -25,7 +54,7 @@ let bare_let =
"let x = 1 in x",
None,
info_error_of_pat_id(
Exp.Fresh.(let_(reusable_pat(Var("x")), int(1), var("x"))),
Term.Fresh.(let_(reusable_pat(Var("x")), int(1), var("x"))),
reusable_id,
),
)
Expand All @@ -38,7 +67,7 @@ let bare_fun =
"fun x -> x",
None,
info_error_of_pat_id(
Exp.Fresh.(fun_(reusable_pat(Var("x")), var("x"), None, None)),
Term.Fresh.(fun_(reusable_pat(Var("x")), var("x"), None, None)),
reusable_id,
),
)
Expand All @@ -51,13 +80,9 @@ let annotated_let =
"let x : Int = 1 in x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
let_(
reusable_pat(
Pat.Fresh.(
Cast(var("x"), Typ.Fresh.int(), Typ.Fresh.unknown(Internal))
),
),
reusable_pat(Cast(pvar("x"), tint(), tunknown(Internal))),
int(1),
var("x"),
)
Expand All @@ -74,13 +99,9 @@ let annotated_fun =
"fun x : Int -> x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
fun_(
reusable_pat(
Pat.Fresh.(
Cast(var("x"), Typ.Fresh.int(), Typ.Fresh.unknown(Internal))
),
),
reusable_pat(Cast(pvar("x"), tint(), tunknown(Internal))),
var("x"),
None,
None,
Expand All @@ -98,11 +119,9 @@ let let_tuple =
"let (x, y, z) = 1 in x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
let_(
reusable_pat(
Pat.Fresh.(Tuple([var("x"), var("y"), var("z")])),
),
reusable_pat(Tuple([pvar("x"), pvar("y"), pvar("z")])),
tuple([int(1), int(2), int(3)]),
var("x"),
)
Expand All @@ -119,11 +138,9 @@ let fun_tuple =
"fun (x, y, z) => x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
fun_(
reusable_pat(
Pat.Fresh.(Tuple([var("x"), var("y"), var("z")])),
),
reusable_pat(Tuple([pvar("x"), pvar("y"), pvar("z")])),
var("x"),
None,
None,
Expand All @@ -142,15 +159,13 @@ let annotated_let_tuple =
"let (x, y, z): (Int, Int, Int) = 1 in x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
let_(
reusable_pat(
Pat.Fresh.(
Cast(
tuple([var("x"), var("y"), var("z")]),
Typ.Fresh.(prod([int(), int(), int()])),
Typ.Fresh.unknown(Internal),
)
Cast(
ptuple([pvar("x"), pvar("y"), pvar("z")]),
tprod([tint(), tint(), tint()]),
tunknown(Internal),
),
),
tuple([int(1), int(2), int(3)]),
Expand All @@ -170,15 +185,13 @@ let annotated_fun_tuple =
"fun (x, y, z) : (Int, Int, Int) -> x",
None,
info_error_of_pat_id(
Exp.Fresh.(
Term.Fresh.(
fun_(
reusable_pat(
Pat.Fresh.(
Cast(
tuple([var("x"), var("y"), var("z")]),
Typ.Fresh.(prod([int(), int(), int()])),
Typ.Fresh.unknown(Internal),
)
Cast(
ptuple([pvar("x"), pvar("y"), pvar("z")]),
tprod([tint(), tint(), tint()]),
tunknown(Internal),
),
),
var("x"),
Expand All @@ -191,6 +204,25 @@ let annotated_fun_tuple =
)
);

let peanut_tree =
no_errors(
"Peanut Figure 1: Exhaustive + Irredundant Tree",
parse_menhir(
{|
type Tree = +Empty + Leaf(Int) + Node([Tree]) in
let f = fun (x : Tree) ->
{{{case x
| Node([]) => Empty
| Node([x]) => Node([f(x), Empty])
| Node([x, y]) => Node([f(x), f(y)])
| Node(x::y::tl) => Node(f(x)::[f(Node(y::tl))])
| Leaf(x) => Leaf(x)
| Empty => Empty
end}}}
in ?
|},
),
);
// TODO: list examples from paper
// TODO: first example from paper
// TODO: recursive type
Expand All @@ -213,5 +245,6 @@ let tests = (
fun_tuple,
annotated_let_tuple,
annotated_fun_tuple,
peanut_tree,
],
);
11 changes: 5 additions & 6 deletions test/Test_Elaboration.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -858,14 +858,13 @@ in 1|},
module MenhirElaborationTests = {
//dhexp = expected
//uexp = tested
let alco_check_menhir = (name: string, dhexp: string, uexp: Term.Exp.t) =>
alco_check(
name,
let alco_check_menhir = (name: string, dhexp: string, uexp: Term.Exp.t) => {
let (e, _) =
Haz3lmenhir.Conversion.Exp.of_menhir_ast(
Haz3lmenhir.Interface.parse_program(dhexp),
),
dhexp_of_uexp(uexp),
);
);
alco_check(name, e, dhexp_of_uexp(uexp));
};

//Test for an empty hole
let empty_hole_str = "?";
Expand Down
37 changes: 23 additions & 14 deletions test/Test_Menhir.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,14 +48,17 @@ let make_term_parse = (s: string) =>
MakeTerm.from_zip_for_sem(Option.get(Printer.zipper_of_string(s))).term,
);

let menhir_matches = (exp: Term.Exp.t, actual: string) =>
alco_check(
"menhir matches expected parse",
exp,
let menhir_parse = (s: string) => {
let (e, _) =
Haz3lmenhir.Conversion.Exp.of_menhir_ast(
Haz3lmenhir.Interface.parse_program(actual),
),
);
Haz3lmenhir.Interface.parse_program(s),
);
e;
};

let menhir_matches = (exp: Term.Exp.t, actual: string) => {
alco_check("menhir matches expected parse", exp, menhir_parse(actual));
};

let menhir_only_test = (name: string, exp: Term.Exp.t, actual: string) =>
test_case(name, `Quick, () => {menhir_matches(exp, actual)});
Expand Down Expand Up @@ -84,9 +87,7 @@ let menhir_maketerm_equivalent_test =
alco_check(
"Menhir parse matches MakeTerm parse",
make_term_parse(actual),
Haz3lmenhir.Conversion.Exp.of_menhir_ast(
Haz3lmenhir.Interface.parse_program(actual),
),
menhir_parse(actual),
)
});

Expand All @@ -101,7 +102,10 @@ let qcheck_menhir_maketerm_equivalent_test =
~count=100,
QCheck.make(~print=AST.show_exp, AST.gen_exp_sized(7)),
exp => {
let core_exp = Conversion.Exp.of_menhir_ast(exp);
let core_exp = {
let (e, _) = Conversion.Exp.of_menhir_ast(exp);
e;
};

let segment =
ExpToSegment.exp_to_segment(
Expand All @@ -113,8 +117,10 @@ let qcheck_menhir_maketerm_equivalent_test =
let serialized = Printer.of_segment(~holes=Some("?"), segment);
let make_term_parsed = make_term_parse(serialized);
let menhir_parsed = Haz3lmenhir.Interface.parse_program(serialized);
let menhir_parsed_converted =
Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed);
let menhir_parsed_converted = {
let (e, _) = Haz3lmenhir.Conversion.Exp.of_menhir_ast(menhir_parsed);
e;
};

switch (
Haz3lcore.DHExp.fast_equal(make_term_parsed, menhir_parsed_converted)
Expand Down Expand Up @@ -147,7 +153,10 @@ let qcheck_menhir_serialized_equivalent_test =
~count=1000,
QCheck.make(~print=AST.show_exp, AST.gen_exp_sized(7)),
exp => {
let core_exp = Conversion.Exp.of_menhir_ast(exp);
let core_exp = {
let (e, _) = Conversion.Exp.of_menhir_ast(exp);
e;
};

let segment =
ExpToSegment.exp_to_segment(
Expand Down
Loading

0 comments on commit d30ff79

Please sign in to comment.