Simon Génier pushed to branch elab-tests at Stefan / Typer
Commits: 38d67961 by Simon Génier at 2020-09-08T11:31:28-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.
- - - - -
2 changed files:
- tests/elab_test.ml - tests/utest_lib.ml
Changes:
===================================== tests/elab_test.ml ===================================== @@ -21,149 +21,43 @@ * * -------------------------------------------------------------------------- *)
- 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", {| -Box = (typecons (Box (l : TypeLevel) (t : Type_ l)) (box t)); -box = (datacons Box box); -unbox b = ##case_ (b | box inside => inside); -alwaysbool b = ##case_ (b | box _ => Bool); - -example1 : unbox (box (lambda x -> Bool)) 1; -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 add_elab_test elab test name setup input expected = + 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 + 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 both [input] and [expected] and fail the test if + the results are different. *) +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" + {| + id : (t : Type) -> t; + id = lambda x -> x; + |} + "id 2;" + "2;" + +let _ = add_elab_test_decl + "Desugar let binding with 1 argument" + "" + "f x = x;" + "f = lambda x -> x;"
let _ = run_all ()
===================================== tests/utest_lib.ml ===================================== @@ -123,18 +123,71 @@ let unexpected_throw sk tk e = 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 _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)); + 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
let add_section sname = try
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/38d67961f7cea6e3df78d02711f83a7336...
Afficher les réponses par date