Skip to content

Improvements to test suite #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
5HT merged 2 commits into from
Jun 14, 2025
Merged

Improvements to test suite #3

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6662e93
Count successful and failed test clauses
Jealrock Jun 14, 2025
7859efe
Colorize
Jealrock Jun 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 62 additions & 49 deletions src/suite.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ let sup_a : exp = Sup set_a
let inf_a : exp = Inf set_a

let interval_a_b (a : exp) (b : exp) : exp =
Set (Lam ("x", Real, And (RealIneq (Lte, a, Var "x"), RealIneq (Lte, Var "x", b))))
Set (Lam ("x", Real, And (RealIneq (Lte, a, Var "x"), RealIneq (Lte, Var "x", b))))

let lebesgue_measure (a : exp) (b : exp) : exp =
Mu (Real,
Expand Down Expand Up @@ -106,28 +106,39 @@ let test_set_eq_incorrect : exp =

(* suite *)

let test_type env ctx (term : exp) (expected_type : exp) (name : string) : unit =
Printf.printf "TEST ";
try let inferred_type = infer env ctx term in
if equal env ctx inferred_type expected_type then
Printf.printf "OK> %s : %s\n" name (string_of_exp inferred_type)
else (
Printf.printf "ERROR>\nTerm: %s\nInferred: %s\nExpected: %s\n" (string_of_exp term) (string_of_exp inferred_type) (string_of_exp expected_type);
raise (TypeError "Type mismatch")
)
with TypeError msg -> Printf.printf "Error in %s: %s\n" name msg

let test_term env ctx (term : exp) (expected_type : exp) (name : string) : unit =
Printf.printf "TEST ";
try if equal env ctx term expected_type then
Printf.printf "OK> %s = %s\n" name (string_of_exp term)
else (
Printf.printf "ERROR>\nTerm: %s\nExpected: %s\n" (string_of_exp term) (string_of_exp expected_type);
raise (TypeError "Term mismatch")
)
with TypeError msg -> Printf.printf "Error in %s: %s\n" name msg

let test_z3 () =
type test_error = { name : string; result : exp; expected : exp }
type test_result = (string, test_error) Result.t

let test_type env ctx (term : exp) (expected_type : exp) (name : string) : test_result =
let inferred_type = infer env ctx term in
if equal env ctx inferred_type expected_type then
Result.ok name
else (
Result.error { name; result = inferred_type; expected = expected_type }
)

let test_term env ctx (term : exp) (expected_type : exp) (name : string) : test_result =
let normalized_term = normalize env ctx term in
if equal env ctx normalized_term expected_type then
Result.ok name
else (
Result.error { name; result = normalized_term; expected = expected_type }
)

let test_print_result (result : test_result) : unit =
match result with
| Result.Ok name -> Printf.printf "Test %s : OK\n" name
| Result.Error error -> Printf.printf "\x1b[31mTest %s : ERROR | expected: %s, got: %s\x1b[0m\n" error.name (string_of_exp error.expected) (string_of_exp error.result)

let test_print_results (results : test_result list) : unit =
List.iter test_print_result results;
let ok_count = List.length (List.filter Result.is_ok results) in
let all_count = List.length results in
let color = if ok_count == all_count then "\x1b[32m" else "\x1b[31m" in
Printf.printf "%s%i / %i tests passed\x1b[0m\n\n\n" color ok_count all_count

let test_z3 () : test_result list =
(
let ctx = (add_var ctx "x" Real) in
let a = (interval_a_b Zero One) in
let b = (interval_a_b One (RealOps (Plus, One, One))) in
Expand All @@ -136,34 +147,36 @@ let test_z3 () =
let one_point = interval_a_b One One in
(* Property 1: C = [1, 1] *)
let prop1 = SetEq (c, one_point) in
test_term env ctx (normalize env ctx prop1) True "C = [1, 1]";
test_term env ctx (normalize env ctx prop1) True "C = [1, 1]" ::
(* Property 2: D ⇔ (x = 1) *)
let x_eq_one = RealIneq (Eq, Var "x", One) in
let prop2 = smt_verify_iff ctx_z3 d x_eq_one in
test_term env ctx prop2 True "D ⇔ x = 1";
Printf.printf "Z3 tests passed!\n"
test_term env ctx prop2 True "D ⇔ x = 1" ::
[]
)

let test_foundations () =
let ctx = add_var ctx "f" (Forall ("x", Real, Real)) in
test_type env ctx integral_sig (Universe 0) "integral_sig";
test_type env ctx sequence_a (Forall ("n", Nat, Real)) "sequence_a";
test_type env ctx limit_a Prop "limit_a";
test_type env ctx inf_a (Real) "inf_a";
test_type env ctx sup_a (Real) "sup_a";
test_type env ctx set_a (Set Real) "set_a";
test_type env ctx universal (Set Prop) "universal set";
test_type env ctx e Real "e";
test_type env ctx l2_space (Forall ("f", Forall ("x", Real, Real), Prop)) "l_2 space";
test_type env ctx sigma_algebra Prop "sigma_algebra";
test_type env (add_var ctx "f" (Forall ("x", Real, Real))) measurable (Prop) "measurable";
test_type env ctx (interval_a_b Zero One) (Set Real) "interval_[a,b]";
test_type env ctx integral_term integral_sig "integral_term";
test_type env ctx (lebesgue_measure Zero One) (Measure (Real, Set (Set Real))) "lebesgue_measure";
test_type env ctx test_set_eq Prop "set_eq_s1_s2";
test_type env ctx test_set_eq_incorrect Prop "set_eq_s1_s2_incorrect";
test_term env ctx (normalize env ctx test_set_eq_incorrect) False "set_eq_s1_s2_incorrect";
test_type env ctx test_set_eq_correct Prop "set_eq_s1_s2_correct";
test_term env ctx (normalize env ctx test_set_eq_correct) True "set_eq_s1_s2_correct";
test_z3();
Printf.printf "All tests passed!\n"

print_endline "\n\n\x1b[1mTesting foundations\x1b[0m\n";
let ctx = add_var ctx "f" (Forall ("x", Real, Real)) in (
test_type env ctx integral_sig (Universe 0) "integral_sig" ::
test_type env ctx sequence_a (Forall ("n", Nat, Real)) "sequence_a" ::
test_type env ctx limit_a Prop "limit_a" ::
test_type env ctx inf_a (Real) "inf_a" ::
test_type env ctx sup_a (Real) "sup_a" ::
test_type env ctx set_a (Set Real) "set_a" ::
test_type env ctx universal (Set Prop) "universal set" ::
test_type env ctx e Real "e" ::
test_type env ctx l2_space (Forall ("f", Forall ("x", Real, Real), Prop)) "l_2 space" ::
test_type env ctx sigma_algebra Prop "sigma_algebra" ::
test_type env (add_var ctx "f" (Forall ("x", Real, Real))) measurable (Prop) "measurable" ::
test_type env ctx (interval_a_b Zero One) (Set Real) "interval_[a,b]" ::
test_type env ctx integral_term integral_sig "integral_term" ::
test_type env ctx (lebesgue_measure Zero One) (Measure (Real, Set (Set Real))) "lebesgue_measure" ::
test_type env ctx test_set_eq Prop "set_eq_s1_s2" ::
test_type env ctx test_set_eq_incorrect Prop "set_eq_s1_s2_incorrect" ::
test_term env ctx (normalize env ctx test_set_eq_incorrect) False "set_eq_s1_s2_incorrect" ::
test_type env ctx test_set_eq_correct Prop "set_eq_s1_s2_correct" ::
test_term env ctx (normalize env ctx test_set_eq_correct) True "set_eq_s1_s2_correct" ::
[]
) |> fun l -> l @ (test_z3 ())
|> test_print_results