Simon Génier pushed to branch elab-tests at Stefan / Typer Commits: b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test. - - - - - 2 changed files: - tests/eval_test.ml - tests/utest_lib.ml Changes: ===================================== tests/eval_test.ml ===================================== @@ -52,9 +52,7 @@ let test_eval_eqv_named name decl run res = let erun = Elab.eval_expr_str run ectx rctx in (* evaluated run expr *) let eres = Elab.eval_expr_str res ectx rctx in (* evaluated res expr *) - if value_eq_list erun eres - then success - else expect_equal_values eres erun) + expect_equal_values erun eres) let test_eval_eqv decl run res = test_eval_eqv_named run decl run res @@ -418,33 +416,33 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Type Alias" "ListInt = List Int;" "" "" -(* let _ = test_eval_eqv_named - * "Equality in case : safe head" - * - * {| - * unvoid (void : Void) = ##case_ void; - * - * Not prop = (contra : prop) ≡> False; - * - * head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; - * head ls p = - * ##case_ (ls - * | nil => unvoid (p (contra := (##DeBruijn 0))) - * | cons x xs => x); - * - * l = (cons 0 nil); - * - * nil≠l : Not (Eq nil l); - * nil≠l = - * lambda (if_it_were : Eq nil l) ≡> - * Eq_cast (x := nil) (y := l) - * (p := if_it_were) - * (f := lambda nill -> - * case nill - * | nil => True - * | cons _ _ => False) - * (); - * |} - * "head l nil≠l" "0" *) +let _ = test_eval_eqv_named + "Equality in case : safe head" + + {| +unvoid (void : Void) = ##case_ void; + +Not prop = (contra : prop) ≡> False; + +head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; +head ls p = + ##case_ (ls + | nil => unvoid (##DeBruijn 0) + | cons x xs => x); + +l = (cons 0 nil); + +nil≠l : Not (Eq nil l); +nil≠l = + lambda (if_it_were : Eq nil l) ≡> + Eq_cast (x := nil) (y := l) + (p := if_it_were) + (f := lambda nill -> + case nill + | nil => True + | cons _ _ => False) + (); + |} + "head l nil≠l" "0" let _ = run_all () ===================================== tests/utest_lib.ml ===================================== @@ -122,8 +122,8 @@ let _expect_equal_t equality_test to_string value expect = if equality_test value expect then success else ( - ut_string2 (red ^ "EXPECTED: " ^ reset ^ "\n" ^ (to_string expect)); - ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value)); + ut_string2 (red ^ "EXPECTED: " ^ reset ^ "\n" ^ (to_string expect) ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n"); failure) let print_value_list values = View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b7eb8f082e16cf284e756982dd081d9c7d... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b7eb8f082e16cf284e756982dd081d9c7d... You're receiving this email because of your account on gitlab.com.