|
open OUnit
open Utest
open Pp_diff
open Proof_diffs
let tokenize_string = Proof_diffs.tokenize_string
let diff_pp = diff_pp ~tokenize_string
let diff_str = diff_str ~tokenize_string
let tests = ref []
let add_test name test = tests := (mk_test name (TestCase test)) :: !tests
let log_out_ch = open_log_out_ch __FILE__
let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
let cprintf s = cfprintf log_out_ch s
let _ = Proof_diffs.log_out_ch := log_out_ch
let string_of_string s : string = "\"" ^ s ^ "\""
(* todo: OCaml: why can't the body of the test function be given in the add_test line? *)
let t () =
let expected : diff_list = [] in
let diffs = diff_str "" " " in
assert_equal ~msg:"empty" ~printer:string_of_diffs expected diffs;
let (has_added, has_removed) = has_changes diffs in
assert_equal ~msg:"has `Added" ~printer:string_of_bool false has_added;
assert_equal ~msg:"has `Removed" ~printer:string_of_bool false has_removed
let _ = add_test "diff_str empty" t
let t () =
let expected : diff_list =
[ `Common (0, 0, "a"); `Common (1, 1, "b"); `Common (2, 2, "c")] in
let diffs = diff_str "a b c" " a b\t c\n" in
assert_equal ~msg:"white space" ~printer:string_of_diffs expected diffs;
let (has_added, has_removed) = has_changes diffs in
assert_equal ~msg:"no `Added" ~printer:string_of_bool false has_added;
assert_equal ~msg:"no `Removed" ~printer:string_of_bool false has_removed
let _ = add_test "diff_str white space" t
let t () =
let expected : diff_list = [ `Removed (0, "a"); `Added (0, "b")] in
let diffs = diff_str "a" "b" in
assert_equal ~msg:"add/remove" ~printer:string_of_diffs expected diffs;
let (has_added, has_removed) = has_changes diffs in
assert_equal ~msg:"has `Added" ~printer:string_of_bool true has_added;
assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
let _ = add_test "diff_str add/remove" t
(* lexer tweaks:
comments are lexed as multiple tokens
strings tokens include begin/end quotes and embedded ""
single multibyte characters returned even if they're not keywords
inputs that give a lexer failure (but no use case needs them yet):
".12"
unterminated string
invalid UTF-8 sequences
*)
let t () =
let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in
let toks = tokenize_string str in
(*List.iter (fun x -> cprintf "'%s' " x) toks;*)
(*cprintf "\n";*)
let str_no_white = String.concat "" (String.split_on_char ' ' str) in
assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks);
List.iter (fun s ->
assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks))
[ "(*"; "()"; ":="]
let _ = add_test "tokenize_string/diff_mode in lexer" t
open Pp
(* example that was failing from #8922 *)
let t () =
Proof_diffs.write_diffs_option "removed";
ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
Proof_diffs.write_diffs_option "on"
let _ = add_test "shorten_diff_span failure from #8922" t
(* note pp_to_string concatenates adjacent strings, could become one token,
e.g. str " a" ++ str "b " will give a token "ab" *)
(* checks background is present and correct *)
let t () =
let o_pp = str "a" ++ str "!" ++ str "c" in
let n_pp = str "a" ++ str "?" ++ str "c" in
let (o_exp, n_exp) = (wrap_in_bg "diff.removed" (str "a" ++ (tag "diff.removed" (str "!")) ++ str "c"),
wrap_in_bg "diff.added" (str "a" ++ (tag "diff.added" (str "?")) ++ str "c")) in
let (o_diff, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"removed" ~printer:db_string_of_pp o_exp o_diff;
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp n_diff
let _ = add_test "diff_pp/add_diff_tags add/remove" t
let t () =
(*Printf.printf "%s\n" (string_of_diffs (diff_str "a d" "a b c d"));*)
let o_pp = str "a" ++ str " d" in
let n_pp = str "a" ++ str " b " ++ str " c " ++ str "d" ++ str " e " in
let n_exp = flatten (wrap_in_bg "diff.added" (seq [
str "a";
str " "; (tag "start.diff.added" (str "b "));
(tag "end.diff.added" (str " c")); str " ";
(str "d");
str " "; (tag "diff.added" (str "e")); str " "
])) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff);;
let _ = add_test "diff_pp/add_diff_tags a span with spaces" t
let t () =
let o_pp = str " " in
let n_pp = tag "sometag" (str "a") in
let n_exp = flatten (wrap_in_bg "diff.added" (tag "diff.added" (tag "sometag" (str "a")))) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = add_test "diff_pp/add_diff_tags diff tags outside existing tags" t
let t () =
let o_pp = str " " in
let n_pp = seq [(tag "sometag" (str " a ")); str "b"] in
let n_exp = flatten (wrap_in_bg "diff.added"
(seq [tag "sometag" (str " "); (tag "start.diff.added" (tag "sometag" (str "a ")));
(tag "end.diff.added" (str "b"))]) ) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = add_test "diff_pp/add_diff_tags existing tagged values with spaces" t
let t () =
let o_pp = str " " in
let n_pp = str " a b " in
let n_exp = flatten (wrap_in_bg "diff.added"
(seq [str " "; tag "diff.added" (str "a b"); str " "])) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = add_test "diff_pp/add_diff_tags multiple tokens in pp" t
let t () =
let o_pp = str "a d" in
let n_pp = seq [str "a b"; str "c d"] in
let n_exp = flatten (wrap_in_bg "diff.added"
(seq [str "a "; tag "start.diff.added" (str "b");
tag "end.diff.added" (str "c"); str " d"])) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = add_test "diff_pp/add_diff_tags token spanning multiple Ppcmd_strs" t
let t () =
let o_pp = seq [str ""; str "a"] in
let n_pp = seq [str ""; str "a b"] in
let n_exp = flatten (wrap_in_bg "diff.added"
(seq [str ""; str "a "; tag "diff.added" (str "b")])) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = add_test "diff_pp/add_diff_tags empty string preserved" t
(* todo: awaiting a change in the lexer to return the quotes of the string token *)
let t () =
let s = "\"a b\"" in
let o_pp = seq [str s] in
let n_pp = seq [str "\"a b\" "] in
cprintf "ppcmds: %s\n" (string_of_ppcmds n_pp);
let n_exp = flatten (wrap_in_bg "diff.added"
(seq [str ""; str "a "; tag "diff.added" (str "b")])) in
let (_, n_diff) = diff_pp o_pp n_pp in
assert_equal ~msg:"string" ~printer:string_of_string "a b" (List.hd (tokenize_string s));
assert_equal ~msg:"added" ~printer:db_string_of_pp n_exp (flatten n_diff)
let _ = if false then add_test "diff_pp/add_diff_tags token containing white space" t
let add_entries map idents rhs_pp =
let make_entry() = { idents; rhs_pp; done_ = false } in
List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;;
let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps
let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps
(* a : foo
b : bar car ->
b : car
a : foo bar *)
let t () =
write_diffs_option "removed"; (* turn on "removed" option *)
let o_line_idents = [ ["a"]; ["b"]] in
let o_hyp_map = ref StringMap.empty in
add_entries o_hyp_map ["a"] (str " : foo");
add_entries o_hyp_map ["b"] (str " : bar car");
let n_line_idents = [ ["b"]; ["a"]] in
let n_hyp_map = ref StringMap.empty in
add_entries n_hyp_map ["b"] (str " : car");
add_entries n_hyp_map ["a"] (str " : foo bar");
let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ]));
flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : car" ]));
flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : foo "; (tag "diff.added" (str "bar")) ]))
] in
let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
(*print_list hyps_diff_list;*)
(*db_print_list hyps_diff_list;*)
List.iter2 (fun exp act ->
assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act))
expected hyps_diff_list
let _ = add_test "diff_hyps simple diffs" t
(* a : nat
c, d : int ->
a, b : nat
d : int
and keeps old order *)
let t () =
write_diffs_option "removed"; (* turn on "removed" option *)
let o_line_idents = [ ["a"]; ["c"; "d"]] in
let o_hyp_map = ref StringMap.empty in
add_entries o_hyp_map ["a"] (str " : nat");
add_entries o_hyp_map ["c"; "d"] (str " : int");
let n_line_idents = [ ["a"; "b"]; ["d"]] in
let n_hyp_map = ref StringMap.empty in
add_entries n_hyp_map ["a"; "b"] (str " : nat");
add_entries n_hyp_map ["d"] (str " : int");
let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ]));
flatten (wrap_in_bg "diff.removed" (seq [(tag "start.diff.removed" (str "c")); (tag "end.diff.removed" (str ",")); str " "; str "d"; str " : int" ]));
flatten (wrap_in_bg "diff.added" (seq [str "d"; str " : int" ]))
] in
let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
(*print_list hyps_diff_list;*)
(*print_list expected;*)
(*db_print_list hyps_diff_list;*)
(*db_print_list expected;*)
List.iter2 (fun exp act ->
assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act))
expected hyps_diff_list
let _ = add_test "diff_hyps compacted" t
(* a : foo
b : bar
c : nat ->
b, a, c : nat
DIFFS
b : bar (remove bar)
b : nat (add nat)
a : foo (remove foo)
a : nat (add nat)
c : nat
is this a realistic use case?
*)
let t () =
write_diffs_option "removed"; (* turn on "removed" option *)
let o_line_idents = [ ["a"]; ["b"]; ["c"]] in
let o_hyp_map = ref StringMap.empty in
add_entries o_hyp_map ["a"] (str " : foo");
add_entries o_hyp_map ["b"] (str " : bar");
add_entries o_hyp_map ["c"] (str " : nat");
let n_line_idents = [ ["b"; "a"; "c"] ] in
let n_hyp_map = ref StringMap.empty in
add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat");
let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))]));
flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))]));
flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "foo"))]));
flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "nat"))]));
flatten (seq [str "c"; str " : nat"])
] in
let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
(*print_list hyps_diff_list;*)
(*db_print_list hyps_diff_list;*)
List.iter2 (fun exp act ->
assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act))
expected hyps_diff_list
let _ = add_test "diff_hyps compacted with join" t
(* b, a, c : nat ->
a : foo
b : bar
c : nat
DIFFS
a : nat (remove nat)
a : foo (add foo)
b : nat (remove nat)
b : bar (add bar)
c : nat
is this a realistic use case? *)
let t () =
write_diffs_option "removed"; (* turn on "removed" option *)
let o_line_idents = [ ["b"; "a"; "c"] ] in
let o_hyp_map = ref StringMap.empty in
add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat");
let n_line_idents = [ ["a"]; ["b"]; ["c"]] in
let n_hyp_map = ref StringMap.empty in
add_entries n_hyp_map ["a"] (str " : foo");
add_entries n_hyp_map ["b"] (str " : bar");
add_entries n_hyp_map ["c"] (str " : nat");
let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "nat"))]));
flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "foo"))]));
flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "nat"))]));
flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "bar"))]));
flatten (seq [str "c"; str " : nat"])
] in
let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
(*print_list hyps_diff_list;*)
(*db_print_list hyps_diff_list;*)
List.iter2 (fun exp act ->
assert_equal ~msg:"added" ~printer:db_string_of_pp exp (flatten act))
expected hyps_diff_list
let _ = add_test "diff_hyps compacted with split" t
(* other potential tests
coqtop/terminal formatting BLOCKED: CAN'T GET TAGS IN FORMATTER
white space at end of line
spanning diffs
shorten_diff_span
MAYBE NOT WORTH IT
diff_pp/add_diff_tags
add/remove - show it preserves, recurs and processes:
nested in boxes
breaks, etc. preserved
diff_pp_combined with/without removed
*)
let _ = run_tests __FILE__ log_out_ch (List.rev !tests)
[ Original von:0.40Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
Datei übertragen
]
|
