Simon Génier pushed to branch eq-cong-eq-trans at Stefan / Typer

Commits: 115d8b01 by Simon Génier at 2020-09-09T12:06:50-04:00 Make eval tests throw on a compilation failure.

- - - - - e8257259 by Simon Génier at 2020-09-09T12:06:59-04:00 Remove commented eval test.

- - - - - 940ade63 by Simon Génier at 2020-09-09T12:06:59-04:00 Do not print callstack of test handler.

This line always print the same callstack, that of the handler, which gives no information about why the test failed.

- - - - - 53c514f5 by Simon Génier at 2020-09-09T12:06:59-04:00 Actually record the backtrace of exceptions while testing.

- - - - - e0d4964e by Simon Génier at 2020-09-09T12:06:59-04:00 Print compiler log on a compilation error in tests.

- - - - - e290b701 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix implicit arguments test.

- - - - - 5f740bf1 by Simon Génier at 2020-09-09T12:06:59-04:00 Fix case test with generic types.

- - - - - b6466a2b by Simon Génier at 2020-09-09T12:07:23-04:00 Fix the rest of the eval tests.

- - - - - 2041b4dd by Simon Génier at 2020-09-09T12:07:34-04:00 Remove = at the end of the flags to the test driver.

I think the intention was to have GNU style flags like --verbose=3, but that does not even work.

- - - - - 56e4fbed by Simon Génier at 2020-09-09T13:24:41-04:00 Easier elaboration tests.

I extracted these changes from another branch since I will need them for yet another. Ther should make elaboration tests easier to write. * New assertions reduce the amount of code to check the results. * Correctly restore state to be able to compare metavariables in two different code fragments.

- - - - - 9d41029c by Simon Génier at 2020-09-09T13:24:48-04:00 Rework add_test to avoid warnings.

- - - - - 10c27014 by Simon Génier at 2020-09-09T13:24:48-04:00 Make success and failure values.

- - - - - 18f49df0 by Simon Génier at 2020-09-09T13:31:55-04:00 Make expected an optional argument in elaboration tests.

- - - - - b7eb8f08 by Simon Génier at 2020-09-09T14:08:48-04:00 Fix safe head test.

- - - - - a8e2af1a by Simon Génier at 2020-09-10T09:38:07-04:00 Oops: add back running tests in the order they were inserted.

- - - - - a4540d14 by Simon Génier at 2020-09-10T15:47:53-04:00 Merge changes to elaboration and evaluation tests.

- - - - - 9cd1b2ce by Simon Génier at 2020-09-10T15:50:23-04:00 Move Eq_comm to pervasives.

Eq_comm can be defined in builtins since it does not use any macro (yet), but it's best to put it in pervasives to group it with other logic functions.

- - - - - 88dac43d by Simon Génier at 2020-09-10T15:50:23-04:00 Add a few logic functions.

- - - - -

13 changed files:

- GNUmakefile - btl/builtins.typer - btl/pervasive.typer - src/elab.ml - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml - tests/inverse_test.ml - tests/macro_test.ml - tests/sexp_test.ml - tests/unify_test.ml - tests/utest_lib.ml - tests/utest_main.ml

Changes:

===================================== GNUmakefile ===================================== @@ -69,7 +69,7 @@ tests-build: $(BUILDDIR)/tests/utests

tests-run: - @./$(BUILDDIR)/tests/utests --verbose= 3 + @./$(BUILDDIR)/tests/utests --verbose 3

test-file: $(OCAMLBUILD) src/test.$(COMPILE_MODE) -I src $(OBFLAGS) @@ -105,7 +105,7 @@ run/typer: @./$(BUILDDIR)/typer

run/tests: - @./$(BUILDDIR)/tests/utests --verbose= 1 + @./$(BUILDDIR)/tests/utests --verbose 1

run/typer-file: @./$(BUILDDIR)/typer ./samples/test__.typer

===================================== btl/builtins.typer ===================================== @@ -58,18 +58,6 @@ Eq_cast : (x : ?) ≡> (y : ?) %% Eq_cast : Eq ?x ?y ≡> ?f ?x -> ?f ?y; Eq_cast = Built-in "Eq.cast";

-%% Commutativity of equality! -%% FIXME: I'd like to just say: -%% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; -Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; -Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: The code is incorrectly accepted even without - %% this `(p := p)` because we just get a metavar which - %% remains uninstantiated and undetected (and then gets - %% throw away by erasure)! - (p := p) - Eq_refl; - %% General recursion!! %% Whether this breaks consistency or not is a good question. %% The basic idea is the following:

===================================== btl/pervasive.typer ===================================== @@ -452,8 +452,38 @@ in List_map mf xs; False = Void; True = Unit;

+%% Prove anything from a contradiction. +unvoid : Void -> ?t; +unvoid v = case v; + Not prop = prop -> False;

+%% Commutativity of equality! +%% FIXME: I'd like to just say: +%% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; +Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; +Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) + %% FIXME: The code is incorrectly accepted even without + %% this `(p := p)` because we just get a metavar which + %% remains uninstantiated and undetected (and then gets + %% throw away by erasure)! + (p := p) + Eq_refl; + +%% Congruence of equality. You can "inject" a (pure) function on both sides of an +%% equality and it will remain true. +Eq_cong + : (x : ?t) + ≡> (y : ?t) + ≡> (p : Eq x y) + ≡> (f : ?t -> ?r) + -> Eq (f x) (f y); +Eq_cong f = Eq_cast (f := lambda xy -> Eq (f x) (f xy)) (p := p) Eq_refl; + +%% Transitivity of equality. +Eq_trans : (x : ?t) ≡> (y : ?t) ≡> (z : ?t) ≡> Eq x y -> Eq y z -> Eq x z; +Eq_trans p q = Eq_cast (f := lambda yz -> Eq x yz) (p := q) p; + %% Like Bool, except that it additionally carries the meaning of its value. %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't

===================================== src/elab.ml ===================================== @@ -1945,21 +1945,19 @@ let default_rctx = EV.from_ectx default_ectx * --------------------------------------------------------- *)

let lexp_expr_str str ctx = - try let tenv = default_stt in - let grm = ectx_get_grammar ctx in - let limit = Some ";" in - let pxps = sexp_parse_str str tenv grm limit in - let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) - lexps; - lexps - with Log.Stop_Compilation s -> [] + let tenv = default_stt in + let grm = ectx_get_grammar ctx in + let limit = Some ";" in + let pxps = sexp_parse_str str tenv grm limit in + let lexps = lexp_parse_all pxps ctx in + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + lexps; + lexps

let lexp_decl_str str ctx = - try let tenv = default_stt in - let tokens = lex_str str tenv in - lexp_p_decls [] tokens ctx - with Log.Stop_Compilation s -> ([],ctx) + let tenv = default_stt in + let tokens = lex_str str tenv in + lexp_p_decls [] tokens ctx

(* Eval String @@ -1967,15 +1965,11 @@ let lexp_decl_str str ctx = (* Because we cant include Elab in eval.ml *)

let eval_expr_str str lctx rctx = - try let lxps = lexp_expr_str str lctx in - let elxps = List.map OL.erase_type lxps in - EV.eval_all elxps rctx false - with Log.Stop_Compilation s -> [] + let lxps = lexp_expr_str str lctx in + let elxps = List.map OL.erase_type lxps in + EV.eval_all elxps rctx false

let eval_decl_str str lctx rctx = - let prev_lctx, prev_rctx = lctx, rctx in - try - let lxps, lctx = lexp_decl_str str lctx in - let elxps = (List.map OL.clean_decls lxps) in - (EV.eval_decls_toplevel elxps rctx), lctx - with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) + let lxps, lctx = lexp_decl_str str lctx in + let elxps = List.map OL.clean_decls lxps in + (EV.eval_decls_toplevel elxps rctx), lctx

===================================== tests/elab_test.ml ===================================== @@ -1,4 +1,4 @@ -(* elab_test.ml --- +(* elab_test.ml --- * * Copyright (C) 2016-2017 Free Software Foundation, Inc. * @@ -21,42 +21,45 @@ * * -------------------------------------------------------------------------- *)

- open Utest_lib

-open Pexp -open Lexp - -open Builtin - -let test - (input_gen: (unit -> 'a list)) - (fmt: 'b list -> string list) - (tester: 'a -> ('b * bool)): (string * bool) list = - let input = List.map tester (input_gen ()) - in let str = List.map (fun (s, _) -> s ) input - in let b = List.map (fun (_, b) -> b) input - in List.combine (fmt str) b - -let generate_tests (name: string) - (input_gen: (unit -> 'a list)) - (fmt: 'b list -> string list) - (tester: 'a -> ('b * bool)) = - let idx = (ref 0) - in List.map (fun (sub, res) -> - idx := !idx + 1; - add_test name - ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) - (fun () -> if res then success () else failure ())) - (test input_gen fmt tester) - -(* let input = "y = lambda x -> x + 1;" *) -let inputs = - [("identity", {| -id = lambda (α : Type) ≡> lambda (x : α) -> x; -res = id 3; - |}); - ("whnf of case", {| +let add_elab_test elab test name ?(setup="") ?(expected="") input = + let run_elab_test () = + let ectx = Elab.default_ectx in + let _, ectx = Elab.lexp_decl_str setup ectx in + let last_metavar = !Unification.global_last_metavar in + let actual, _ = elab input ectx in + if String.equal expected "" + then success + else + (Unification.global_last_metavar := last_metavar; + let expected, _ = elab expected ectx in + test actual expected) + in + add_test "ELAB" name run_elab_test + +(** Run setup, then elaborate [input]. Succeeds if there are no compilation + errors and [expected] elaborates to the same lexp, if provided. *) +let add_elab_test_expr = + add_elab_test (fun s ctx -> Elab.lexp_expr_str s ctx, ctx) expect_equal_lexps + +(** Like {!add_elab_test_expr}, but elaborates [input] and [expected] as top + level declarations instead of expressions. *) +let add_elab_test_decl = + add_elab_test Elab.lexp_decl_str expect_equal_decls + +let _ = add_elab_test_expr + "Instanciate implicit arguments" + ~setup:{| +f : (i : Int) -> Eq i i -> Int; +f = lambda i -> lambda eq -> i; + |} + ~expected:"f 4 (Eq_refl (x := 4));" + "f 4 Eq_refl;" + +let _ = add_elab_test_decl + "Whnf of case" + {| Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); box = (datacons Box box); unbox b = ##case_ (b | box inside => inside); @@ -67,103 +70,6 @@ example1 = true;

example2 : alwaysbool (box Int); example2 = true; - |}); - ] - -let generate_lexp_from_str str = - List.hd ((fun (lst, _) -> - (List.map - (fun (_, lxp, _) -> lxp)) - (List.flatten lst)) - (Elab.lexp_decl_str str Elab.default_ectx)) - -let _ = generate_tests - "TYPECHECK" - (fun () -> inputs) - (fun x -> x) - (fun (name, input) -> - let result = - try - let ectx = Elab.default_ectx in - let pres = Prelexer.prelex_string input in - let sxps = Lexer.lex Grammar.default_stt pres in - let _lxps, _ectx = Elab.lexp_p_decls [] sxps ectx in - Log.stop_on_error(); - true - with - | Log.Stop_Compilation _ -> (Log.print_and_clear_log (); false) - | Log.Internal_error _ -> (Log.print_and_clear_log (); false) in - (name, result) - ) - -let lctx = Elab.default_ectx -(* let _ = (add_test "TYPECHEK_LEXP" "lexp_print" (fun () -> - * - * let dcode = " - * sqr = lambda (x) -> x * x; - * cube = lambda (x) -> x * (sqr x); - * - * mult = lambda (x) -> lambda (y) -> x * y; - * - * twice = (mult 2); - * - * let_fun = lambda (x) -> - * let a = (twice x); b = (mult 2 x); in - * a + b;" in - * - * let ret1, _ = lexp_decl_str dcode lctx in - * - * let to_str decls = - * let str = _lexp_str_decls (!compact_ppctx) (List.flatten ret1) in - * List.fold_left (fun str lxp -> str ^ lxp) "" str in - * - * (* Cast to string *) - * let str1 = to_str ret1 in - * - * print_string str1; - * - * (* read code again *) - * let ret2, _ = lexp_decl_str str1 lctx in - * - * (* Cast to string *) - * let str2 = to_str ret2 in - * - * if str1 = str2 then success () else failure () - * )) *) - -(* -let set_to_list s = - StringSet.fold (fun g a -> g::a) s [] - -let _ = (add_test "LEXP" "Free Variable" (fun () -> - - let dcode = " - a = 2; - b = 3; - f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b are fv - " in - - let ret = pexp_decl_str dcode in - let g = match List.rev ret with - | (_, g, _)::_ -> g - | _ -> raise (Unexpected_result "Unexpected empty list") in - - let (bound, free) = free_variable g in - - let bound = set_to_list bound in - let (free, _) = free in - - match bound with - | ["x"] ->( - match free with - | ["_+_"; "f"; "b"; "a"] -> success () - | _ -> failure ()) - | _ -> failure () - -)) *) - -(* run all tests *) -let _ = run_all () + |}

let _ = run_all ()

===================================== tests/env_test.ml ===================================== @@ -67,14 +67,8 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> (ctx, idx - 1)) (rctx, n) var in

- print_rte_ctx rctx; - - success () - ) - else - success () - -)) + print_rte_ctx rctx); + success))

(* run all tests *)

===================================== tests/eval_test.ml ===================================== @@ -52,15 +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 ( - (* List.hd was throwing when run or res failed to compile *) - (match erun with x::_ -> value_print x - | _ -> print_string ("no run expression\n")); - (match eres with x::_ -> value_print x - | _ -> print_string ("no result expression\n")); - failure ())) + expect_equal_values erun eres)

let test_eval_eqv decl run res = test_eval_eqv_named run decl run res

@@ -276,21 +268,6 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv "w = 2" "decltype w" "Int" let _ = test_eval_eqv "w = 2" "declexpr w" "2"

-(* let attr_decl = " - * w = 2; - * greater-than = new-attribute (Int -> Int); - * greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" - * - * let _ = test_eval_eqv_named - * "has-attribute" - * - * attr_decl - * - * "has-attribute greater-than w; - * (get-attribute greater-than w) 3;" - * - * "true; 3" *) - let _ = (add_test "EVAL" "Monads" (fun () ->

let dcode = " @@ -304,10 +281,9 @@ let _ = (add_test "EVAL" "Monads" (fun () ->

(* Eval defined lambda *) let ret = Elab.eval_expr_str rcode ectx rctx in - match ret with - | [v] -> success () - | _ -> failure () -)) + match ret with + | [v] -> success + | _ -> failure))

let _ = test_eval_eqv_named "Argument Reordering" @@ -350,21 +326,20 @@ let _ = test_eval_eqv_named

""hello"; 5.0; "hello"; 5.0; "hello"; 7"

-(* let _ = test_eval_eqv_named - * "Implicit Arguments" - * - * "default = new-attribute Macro; - * default = add-attribute default Int (macro (lambda (lst : List Sexp) -> - * (IO_return (Sexp_integer (Int->Integer 1))))); - * - * fun = lambda (x : Int) => - * lambda (y : Int) -> - * lambda (z : Int) -> x * y + z;" - * - * "fun 2 1; - * fun 2 1" - * - * "3; 3" *) +let _ = test_eval_eqv_named + "Implicit Arguments" + + {| + fun = lambda (x : Int) => + lambda (p : Eq x x) -> + x; + |} + + {| + fun (Eq_refl (x := 2)) + |} + + "2"

let _ = test_eval_eqv_named "Equalities" @@ -382,8 +357,8 @@ let _ = test_eval_eqv_named "P = (a : Type) ≡> a -> Not (Not a); p : P; p = lambda a ≡> lambda x notx -> notx x; - tP : Decidable P; - tP = (datacons Decidable true) (prop := P) (p := p); + tP : Decidable (ℓ := ?ℓ₀) P; + tP = (datacons (Decidable (ℓ := ?ℓ₀)) true) (prop := P) (p := p);

PairTest = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));

@@ -404,40 +379,70 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Y"

- "length_y = lambda t ≡> - %% FIXME: The `a` argument should be inferred! - Y (a := List t) (witness := (lambda l -> 0)) - (lambda length l - -> case l - | nil => 0 - | cons _ l => 1 + length l);" + {| + length_y = + Y (witness := (lambda l -> 0)) + (lambda length l + -> case l + | nil => 0 + | cons _ l => 1 + length l); + |}

"length_y (cons 1 (cons 5 nil));"

"2;"

let _ = test_eval_eqv_named - "Block" + "Block"

- "a = 2" + "a = 2"

- "a + 1;" - "{a + 1};" + "a + 1;" + "{a + 1};"

let _ = test_eval_eqv_named - "define-operator" + "define-operator"

- "define-operator "IF" () 2; - define-operator "THEN" 2 1; - define-operator "ELSE" 1 66; - IF_THEN_ELSE_ = if_then_else_;" + {| + define-operator "IF" () 2; + define-operator "THEN" 2 1; + define-operator "ELSE" 1 66; + IF_THEN_ELSE_ = if_then_else_; + |}

- "IF true THEN 2 ELSE 3;" - "if true then 2 else 3;" + "IF true THEN 2 ELSE 3;" + "if true then 2 else 3;"

let _ = test_eval_eqv_named - "Type Alias" "ListInt = List Int;" "" (* == *) "" + "Type Alias" "ListInt = List Int;" "" ""

-(* run all tests *) -let _ = run_all () +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/inverse_test.ml ===================================== @@ -94,7 +94,7 @@ let inv_add_test name inputs = then b else not b) | None -> (not b)) true inputs - then success () else failure ()) + then success else failure)

let _ = inv_add_test "Manual" input

===================================== tests/macro_test.ml ===================================== @@ -60,11 +60,7 @@ let _ = (add_test "MACROS" "macros base" (fun () -> let ecode = "(lambda (x : Int) -> sqr 3) 5;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint(r)] -> expect_equal_int r (3 * 3) - | _ -> failure ()) -) + expect_equal_values ret [Vint(3 * 3)]))

let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " @@ -89,14 +85,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let ecode = "a; b;" in

let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint(a); Vint(b)] -> - if (a = 1 && b = 2) then success () else failure () - - | _ -> failure ()) -) - + expect_equal_values ret [Vint(1); Vint(2)]))

(* run all tests *) let _ = run_all ()

===================================== tests/sexp_test.ml ===================================== @@ -4,7 +4,7 @@ open Utest_lib

let sexp_parse_str dcode = sexp_parse_str dcode Grammar.default_stt Grammar.default_grammar (Some ";") - + let test_sexp_add dcode testfun = add_test "SEXP" dcode (fun () -> testfun (sexp_parse_str dcode)) @@ -14,8 +14,8 @@ let _ = test_sexp_add "lambda x -> x + x" (fun ret -> | [Node(Symbol(_, "lambda_->_"), [Symbol(_, "x"); Node(Symbol(_, "_+_"), [Symbol(_, "x"); Symbol(_, "x")])])] - -> success () - | _ -> failure () + -> success + | _ -> failure )

let _ = test_sexp_add "x * x * x" (fun ret -> @@ -23,8 +23,8 @@ let _ = test_sexp_add "x * x * x" (fun ret -> | [Node(Symbol(_, "_*_"), [Node(Symbol(_, "_*_"), [Symbol(_, "x"); Symbol(_, "x")]); Symbol(_, "x")])] - -> success () - | _ -> failure () + -> success + | _ -> failure )

let test_sexp_eqv dcode1 dcode2 = @@ -33,10 +33,10 @@ let test_sexp_eqv dcode1 dcode2 = let s1 = sexp_parse_str dcode1 in let s2 = sexp_parse_str dcode2 in if sexp_eq_list s1 s2 - then success () + then success else (sexp_print (List.hd s1); sexp_print (List.hd s2); - failure ())) + failure))

let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y"

===================================== tests/unify_test.ml ===================================== @@ -224,7 +224,7 @@ let _ = List.map idx := !idx + 1; add_test "UNIFICATION" ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str ) - (fun () -> if expected = res then success () else failure ())) + (fun () -> if expected = res then success else failure)) (List.combine (fmt unifications) unifications )

let _ = run_all ()

===================================== tests/utest_lib.ml ===================================== @@ -37,13 +37,11 @@ open Fmt module StringMap = Map.Make (struct type t = string let compare = String.compare end)

+type test_fun = unit -> int +type section = test_fun StringMap.t * string list

-type test_fun = (unit -> int) -type tests = (test_fun) StringMap.t -type sections = ((tests) StringMap.t) * string list - -let success () = 0 -let failure () = (-1) +let success = 0 +let failure = -1

(* * SECTION NAME - TEST NAME - FUNCTION (() -> int) @@ -79,15 +77,15 @@ let set_verbose lvl = Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing)

let arg_defs = [ - ("--verbose=", + ("--verbose", Arg.Int set_verbose, " Set verbose level"); - ("--samples=", + ("--samples", Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); (* Allow users to select which test to run *) - ("--fsection=", + ("--fsection", Arg.String (fun g -> global_fsection := U.string_uppercase g), " Set test filter"); - ("--ftitle=", + ("--ftitle", Arg.String (fun g -> global_ftitle := U.string_uppercase g), " Set test filter"); ] @@ -115,63 +113,104 @@ let ut_string2 = ut_string 2 let unexpected_throw sk tk e = ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); ut_string2 "[ ] UNEXPECTED THROW:\n"; - ut_string2 "[ ] ----------------------------- Callstack (20): -----------------------------------------\n"; - ut_string2 ("[ ] " ^ (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20))); - ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] ----------------------------- Backtrace: ----------------------------------------------\n"; ut_string2 ("[ ] " ^ (Printexc.get_backtrace ()) ^ "\n"); ut_string2 "[ ] ---------------------------------------------------------------------------------------\n"; ut_string2 "[ ] "; ut_string2 ((Printexc.to_string e) ^ "\n" ^ reset)

-let _expect_equal_t to_string value expect = - if value = expect then - success () - else( - ut_string2 (red ^ "[ ] EXPECTED: " ^ (to_string expect)^ "\n"); - ut_string2 ( "[ ] GOT: " ^ (to_string value) ^ "\n" ^ reset); - failure ()) - -let expect_equal_int = _expect_equal_t string_of_int -let expect_equal_float = _expect_equal_t string_of_float -let expect_equal_str = _expect_equal_t (fun g -> g) - - -let add_section sname = - try - StringMap.find sname (!global_sections) - with - Not_found -> - insertion_order := sname::(!insertion_order); - (StringMap.empty, ref []) - -(* USAGE *) -(* +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) ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n"); + failure) + +let print_value_list values = + List.fold_left (fun s v -> s ^ "\n" ^ Env.value_string v) "" values + +let expect_equal_int = _expect_equal_t Int.equal string_of_int +let expect_equal_float = _expect_equal_t Float.equal string_of_float +let expect_equal_str = _expect_equal_t String.equal (fun g -> g) +let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list + +let expect_equal_lexps = + let rec lexp_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when Lexp.eq l_head r_head + -> lexp_list_eq l_tail r_tail + | _ -> false + in + let string_of_lexp_list lexps = + List.fold_left (fun s lexp -> s ^ "\n" ^ Lexp.lexp_string lexp) "" lexps + in + _expect_equal_t lexp_list_eq string_of_lexp_list + +let expect_equal_decls = + let rec decl_eq l r = + let (_, l_vname), l_lexp, l_ltype = l in + let (_, r_vname), r_lexp, r_ltype = r in + Option.equal String.equal l_vname r_vname + && Lexp.eq l_lexp r_lexp + && Lexp.eq l_ltype r_ltype + in + let rec mutual_decl_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when decl_eq l_head r_head + -> mutual_decl_list_eq l_tail r_tail + | _ -> false + in + let rec decl_list_eq l r = + match l, r with + | [], [] -> true + | l_head :: l_tail, r_head :: r_tail when mutual_decl_list_eq l_head r_head + -> decl_list_eq l_tail r_tail + | _ -> false + in + let string_of_decl_list ds = + let buffer = Buffer.create 1024 in + let string_of_mutual_decl_list ds = + let source = Lexp.lexp_str_decls Lexp.pretty_ppctx ds in + let add_decl d = + Buffer.add_string buffer d; + Buffer.add_char buffer '\n' + in + List.iter add_decl source + in + List.iter string_of_mutual_decl_list ds; + Buffer.contents buffer + in + _expect_equal_t decl_list_eq string_of_decl_list + +(* USAGE + * * (add_test "LET" "Base Case" (fun () -> * let r = eval_string "let a = 2; b = 3; in a + b;" in * let v = (get_int r) in * if v = 5 then success () else failure ())) - * - * sname: Section Name - * tname: Test Name - * tfun : test function (unit -> int) *) -let add_test sname tname tfun = - - (* Does Section Exist ? *) - let (tmap, lst) = add_section sname in - - try let _ = StringMap.find tname tmap in - ut_string2 "TEST ALREADY EXISTS" - with - Not_found -> - - lst := tname::(!lst); - - (* add test *) - let ntmap = StringMap.add tname tfun tmap in - global_sections := StringMap.add sname (ntmap, lst) (!global_sections); - - number_test := (!number_test + 1) +let add_test section_name test_name test_fun = + let update_tests = function + | Some _ as entry + -> (ut_string2 (red ^ {|Test "|} ^ test_name ^ {|" alread exists.|} ^ reset); + entry) + | None + -> (number_test := !number_test + 1; + Some test_fun) + in + let update_sections section = + let updated_entry = match section with + | Some (tests, order) + -> StringMap.update test_name update_tests tests, test_name :: order + | None + -> (insertion_order := section_name :: !insertion_order; + StringMap.singleton test_name test_fun, [test_name]) + in + Some updated_entry + in + global_sections := StringMap.update section_name update_sections !global_sections

(* sk : Section Key * tmap: test_name -> tmap @@ -180,29 +219,36 @@ let for_all_tests sk tmap tk = if (must_run_title tk) then ( let tv = StringMap.find tk tmap in flush stdout; + Log.clear_log (); try let r = tv () in if r = 0 then( ut_string2 (green ^ "[ OK] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset)) else( ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n" ^ reset); - ret_code := failure ()) - with e -> - ret_code := failure (); - unexpected_throw sk tk e) else () + ret_code := failure) + with + | Log.Stop_Compilation message -> + ret_code := failure; + ut_string2 (red ^ "[ FAIL] " ^ sk ^ " - " ^ tk ^ "\n"); + ut_string2 ("[ ] " ^ message ^ "\n" ^ reset); + Log.print_log (); + | e -> + ret_code := failure; + unexpected_throw sk tk e) else ()

let for_all_sections sk = - let tmap, tst = StringMap.find sk (!global_sections) in - - if (must_run_section sk) then( - ut_string2 ("[RUN ] " ^ sk ^ " \n"); - tst := List.rev (!tst); - List.iter (for_all_tests sk tmap) (!tst)) - - else () + let tmap, tst = StringMap.find sk (!global_sections) in + let tst = List.rev tst in + if must_run_section sk + then ( + ut_string2 ("[RUN ] " ^ sk ^ " \n"); + List.iter (for_all_tests sk tmap) tst)

(* Run all *) let run_all () = + Printexc.record_backtrace true; + parse_args ();

insertion_order := List.rev (!insertion_order);

===================================== tests/utest_main.ml ===================================== @@ -43,17 +43,17 @@ let global_ftitle = ref "" let global_filter = ref false

let arg_defs = [ - ("--verbose=", + ("--verbose", Arg.Int (fun g -> global_verbose_lvl := g), " Set verbose level"); - ("--samples=", + ("--samples", Arg.String (fun g -> global_sample_dir := g), " Set sample directory"); - ("--tests=", + ("--tests", Arg.String (fun g -> global_tests_dir := g), " Set tests directory"); (* Allow users to select which test to run *) - ("--fsection=", + ("--fsection", Arg.String (fun g -> global_fsection := U.string_uppercase g; global_filter := true), " Set test filter"); - ("--ftitle=", + ("--ftitle", Arg.String (fun g -> global_ftitle := U.string_uppercase g; global_filter := true), " Set test filter"); ] @@ -130,10 +130,10 @@ let main () = let exit_code = ref 0 in let failed_test = ref 0 in let tests_n = ref 0 in - let test_args = " --samples= " ^ root_folder ^ - " --verbose= " ^ (string_of_int !global_verbose_lvl) ^ + let test_args = " --samples " ^ root_folder ^ + " --verbose " ^ (string_of_int !global_verbose_lvl) ^ (if not (!global_ftitle = "") then - (" --ftitle= " ^ !global_ftitle) else "") in + (" --ftitle " ^ !global_ftitle) else "") in

List.iter (fun file -> flush stdout;

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2a2018c3a45c0723060ab178cae7b958a...