X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;h=aebc746889cf98e18615271c3a9d58b45cd3b81b;hb=98295941bee765a0cb4070eb3f2df553228c11c8;hp=ecccf45791e0995e7df9baf6ffdd6a8453df45c8;hpb=e02c6e8e53e94e0bc7e2556fcd67645f46b039fc;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index ecccf4579..aebc74688 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -29,8 +29,9 @@ let argc = Array.length Sys.argv let rawsep = "###" let sep = Pcre.regexp (sprintf "^%s" rawsep) -let print s = print_string s +let print s = print_string s; flush stdout let print_endline s = print_endline s +let print_endline_to_channel ch s = output_string ch (s ^ "\n") type state = Term | EMetasenv | ETerm | EType | EReduced @@ -109,56 +110,62 @@ let parse_regtest = 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_endline "Term mismatch"; - print_endline " expected:"; - print_endline (" " ^ expected.eterm); - print_endline " found:"; - print_endline (" " ^ found.eterm); - outcome := false; - end; - if expected.emetasenv <> found.emetasenv then begin - print_endline "Metasenv mismatch"; - print_endline " expected:"; - print_endline (" " ^ expected.emetasenv); - print_endline " found:"; - print_endline (" " ^ found.emetasenv); - outcome := false; - end; - if expected.etype <> found.etype then begin - print_endline "Type mismatch"; - print_endline " expected:"; - print_endline (" " ^ expected.etype); - print_endline " found:"; - print_endline (" " ^ found.etype); - outcome := false; - 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); - outcome := false; - end; - !outcome +let as_expected report_fname expected found = (* ignores "term" field *) + let eterm_ok = expected.eterm = found.eterm 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 && emetasenv_ok && etype_ok && ereduced_ok in + if outcome then + (if Sys.file_exists report_fname then Sys.remove report_fname) + else + begin + let och = open_out report_fname in + let print_endline = print_endline_to_channel och 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 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; + close_out och ; + end; + outcome -let test_this raw_term = +let test_this uri_pred raw_term = let empty_context = [] in - let (metasenv, cic_term) = BatchParser.parse raw_term in + let (metasenv, cic_term) = BatchParser.parse ~uri_pred raw_term in let etype = try CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) - with - _ -> "MALFORMED" + with _ -> "MALFORMED" in let ereduced = try CicPp.ppterm (CicReduction.whd empty_context cic_term) - with - _ -> "MALFORMED" + with _ -> "MALFORMED" in { term = raw_term; (* useless *) @@ -178,7 +185,6 @@ let dump_environment filename = ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^ Printexc.to_string exc) ; raise exc -;; let restore_environment filename = if Sys.file_exists filename then @@ -195,9 +201,9 @@ let restore_environment filename = end else CicEnvironment.empty () -;; -let main generate dump fnames = +let main generate dump fnames tryvars varsprefix = + let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in if generate then begin (* gen mode *) @@ -209,7 +215,7 @@ let main generate dump fnames = print_endline (sprintf "Generating regtest %s -> %s\n ..." fname test_fname); let raw_term = (parse_regtest fname).term in - let result = test_this raw_term in + let result = test_this uri_pred raw_term in print_test result test_fname ; if dump then dump_environment env_fname ; ) fnames @@ -222,15 +228,16 @@ let main generate dump fnames = (function fname -> let env_fname = fname ^ ".env" in let test_fname = fname ^ ".test" in + let report_fname = fname ^ ".report" in restore_environment env_fname ; let time = Unix.gettimeofday () in print ("Processing " ^ fname ^":\t") ; let is_ok = try let expected = parse_regtest test_fname in - let actual = test_this expected.term in + let actual = test_this uri_pred expected.term in if dump then dump_environment env_fname ; - if as_expected expected actual then + if as_expected report_fname expected actual then (incr ok ; true) else (nok := fname :: !nok ; false) @@ -238,7 +245,11 @@ let main generate dump fnames = in let timediff = Unix.gettimeofday () -. time in print (sprintf "done in %f seconds\t" timediff) ; - print_endline (if is_ok then "[ OK ]" else "[ FAILED ]") + print_endline + (if is_ok then + "[ OK ]" + else + "[ FAILED ]") ) fnames ; print_endline "*** Summary ***"; print_endline (sprintf "Succeeded: %d" !ok); @@ -246,24 +257,39 @@ let main generate dump fnames = List.iter (fun fname -> print_endline (sprintf " %s failed :-(" fname)) (List.rev !nok) end -;; let _ = + Helm_registry.load_from "triciclo.conf.xml"; + HelmLogger.register_log_callback + (fun ?(append_NL = true) msg -> + (if append_NL then prerr_endline else prerr_string) + (HelmLogger.string_of_html_msg msg)); let fnames = ref [] in let gen = ref false in + let tryvars = ref false in let dump = ref false in let nodump = ref false in + let varsprefix = ref "" in let usage = "regtest [OPTION] ... test1 ..." in let spec = - ["-gen", Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ; - "--gen", Arg.Set gen, "generate the tests; implies -dump (unless -nodump is specified)" ; - "-dump", Arg.Set dump, "dumps the final environment" ; - "--dump", Arg.Set dump, "dumps the final environment" ; - "-nodump", Arg.Set dump, "do not dump the final environment" ; - "--nodump", Arg.Set dump, "do not dump the final environment" ] + ["-gen", Arg.Set gen, + "generate the tests; implies -dump (unless -nodump is specified)" ; + "--gen", Arg.Set gen, + "generate the tests; implies -dump (unless -nodump is specified)" ; + "-dump", Arg.Set dump, "dump the final environment" ; + "--dump", Arg.Set dump, "dump the final environment" ; + "-nodump", Arg.Set nodump, "do not dump the final environment" ; + "--nodump", Arg.Set nodump, "do not dump the final environment" ; + "-vars", Arg.Set tryvars, "try also variables" ; + "-novars", Arg.Clear tryvars, "do not try variables (default)" ; + "-varsprefix", Arg.Set_string varsprefix, + "limit variable choices to URIs beginning with prefix" ; + "--varsprefix", Arg.Set_string varsprefix, + "limit variable choices to URIs beginning with prefix" ; + ] in - Arg.parse spec (function filename -> fnames := filename::!fnames ) usage ; + Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ; if !fnames = [] then Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ; - main !gen ((!gen || !dump) && (not !nodump)) !fnames -;; + main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix +