- { term = Buffer.contents term;
- emetasenv = Buffer.contents emetasenv;
- eterm = Buffer.contents eterm;
- etype = Buffer.contents etype;
- ereduced = Buffer.contents ereduced }
-
-let as_expected expected found = (* ignores "term" field *)
- let outcome = ref true in
- if expected.eterm <> found.eterm then begin
- print_msg "Term mismatch";
- print_msg " expected:";
- print_msg (" " ^ expected.eterm);
- print_msg " found:";
- print_msg (" " ^ found.eterm);
- outcome := false;
- end;
- if expected.etype <> found.etype then begin
- print_msg "Type mismatch";
- print_msg " expected:";
- print_msg (" " ^ expected.etype);
- print_msg " found:";
- print_msg (" " ^ found.etype);
- outcome := false;
- end;
- if expected.ereduced <> found.ereduced then begin
- print_msg "Reduced term mismatch";
- print_msg " expected:";
- print_msg (" " ^ expected.ereduced);
- print_msg " found:";
- print_msg (" " ^ found.ereduced);
- outcome := false;
- end;
- !outcome
-
-let test_this raw_term =
- let empty_context = [] in
- let (metasenv, cic_term) = BatchParser.parse raw_term in
- let etype =
- try
- CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
- with
- _ -> "MALFORMED"
+ push_res () ;
+ List.rev !res
+
+let as_expected_one och expected found = (* ignores "term" field *)
+ let eterm_ok = expected.eterm = found.eterm in
+ let eenv_ok = expected.eenv = found.eenv in
+ let emetasenv_ok = expected.emetasenv = found.emetasenv in
+ let etype_ok = expected.etype = found.etype in
+ let ereduced_ok = expected.ereduced = found.ereduced in
+ let outcome =
+ eterm_ok && eenv_ok && emetasenv_ok && etype_ok && ereduced_ok
+ in
+ begin
+ let print_endline s = print_endline_to_channel (Lazy.force och) s in
+ if not eterm_ok then begin
+ print_endline "### Term mismatch ###";
+ print_endline "# expected:";
+ print_endline (" " ^ expected.eterm);
+ print_endline "# found:";
+ print_endline (" " ^ found.eterm);
+ end;
+ if not eenv_ok then begin
+ print_endline "### Disambiguation environment mismatch ###";
+ print_endline "# expected:";
+ print_endline (" " ^ expected.eenv);
+ print_endline "# found:";
+ print_endline (" " ^ found.eenv);
+ end;
+ if not emetasenv_ok then begin
+ print_endline "### Metasenv mismatch ###";
+ print_endline "# expected:";
+ print_endline (" " ^ expected.emetasenv);
+ print_endline "# found:";
+ print_endline (" " ^ found.emetasenv);
+ end;
+ if not etype_ok then begin
+ print_endline "### Type mismatch ###";
+ print_endline "# expected:";
+ print_endline (" " ^ expected.etype);
+ print_endline "# found:";
+ print_endline (" " ^ found.etype);
+ end;
+ if expected.ereduced <> found.ereduced then begin
+ print_endline "### Reduced term mismatch ###";
+ print_endline "# expected:";
+ print_endline (" " ^ expected.ereduced);
+ print_endline "# found:";
+ print_endline (" " ^ found.ereduced);
+ end;
+ end;
+ outcome
+
+let as_expected report_fname expected found =
+ (if Sys.file_exists report_fname then Sys.remove report_fname) ;
+ let och = lazy (open_out report_fname) in
+ let print_endline s = print_endline_to_channel (Lazy.force och) s in
+ let print_interpretation test =
+ print_endline "## Interpretation dump ##";
+ print_endline "# Disambiguation environment:";
+ print_endline test.eenv;
+ print_endline "# Metasenv:";
+ print_endline test.emetasenv;
+ print_endline "# Term:";
+ print_endline test.eterm;
+ print_endline "# Type:";
+ print_endline test.etype;
+ print_endline "# Reduced term:";
+ print_endline test.ereduced;