From 6662e938b23a59fe238f6b0e6b8716928ec703a6 Mon Sep 17 00:00:00 2001 From: Oleh Marakhovskyi Date: Sat, 14 Jun 2025 11:49:28 +0300 Subject: [PATCH 1/2] Count successful and failed test clauses --- src/suite.ml | 109 ++++++++++++++++++++++++++++----------------------- 1 file changed, 60 insertions(+), 49 deletions(-) diff --git a/src/suite.ml b/src/suite.ml index 89bf491..54e03a6 100644 --- a/src/suite.ml +++ b/src/suite.ml @@ -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, @@ -106,28 +106,37 @@ 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 "Test %s : ERROR | expected: %s, got: %s\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 + Printf.printf "%i / %i tests passed\n\n" ok_count (List.length results) + +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 @@ -136,34 +145,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\nTesting foundations\n"; + let ctx = add_var ctx "f" (Forall ("x", Real, Real)) in ( + test_type env ctx sequence_a (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 From 7859efe1b920ff2f2d9ad22f12360e077b0d7f21 Mon Sep 17 00:00:00 2001 From: Oleh Marakhovskyi Date: Sat, 14 Jun 2025 12:27:27 +0300 Subject: [PATCH 2/2] Colorize --- src/suite.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/suite.ml b/src/suite.ml index 54e03a6..da99e31 100644 --- a/src/suite.ml +++ b/src/suite.ml @@ -128,12 +128,14 @@ let test_term env ctx (term : exp) (expected_type : exp) (name : string) : test_ 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 "Test %s : ERROR | expected: %s, got: %s\n" error.name (string_of_exp error.expected) (string_of_exp error.result) + | 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 - Printf.printf "%i / %i tests passed\n\n" ok_count (List.length results) + 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 = ( @@ -154,9 +156,9 @@ let test_z3 () : test_result list = ) let test_foundations () = - print_endline "\n\nTesting foundations\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 sequence_a (Universe 0) "integral_sig" :: + 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" ::