X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Fregtest.ml;h=aebc746889cf98e18615271c3a9d58b45cd3b81b;hb=98295941bee765a0cb4070eb3f2df553228c11c8;hp=a38d5a02be8c4d85817d900f038b7d33d0de489b;hpb=ded0396c81ec49a45d9406becb602e1071e6820b;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index a38d5a02b..aebc74688 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -27,66 +27,74 @@ open Printf let argc = Array.length Sys.argv -let usage () = - prerr_endline "Usage: regtest ..."; - prerr_endline " regtest (-gen|--gen) ..."; - exit 2 - let rawsep = "###" -let sep = Pcre.regexp rawsep -let msg_prefix = "*** REGTEST *** " -let print_msg s = prerr_endline (msg_prefix ^ s) +let sep = Pcre.regexp (sprintf "^%s" rawsep) +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 | ETerm | EType | EReduced +type state = Term | EMetasenv | ETerm | EType | EReduced (* regtest file format * < cic term in concrete syntax > * separator (* see sep above *) - * < expected cic term after disambiguation as PPed by CicPp.ppterm > + * < expected metasenv after disambiguation (CicMetaSubst.ppmetasenv) > + * separator (* see sep above *) + * < expected cic term after disambiguation (CicPp.ppterm) > * separator (* see sep above *) - * < expected cic type as per type_of as PPed by CicPp.ppterm > + * < expected cic type as per type_of (CicPp.ppterm) > * separator (* see sep above *) - * < expected reduced cic term as PPed by CicPp.ppterm > + * < expected reduced cic term as (CicPp.ppterm) > *) type regtest = { term: string; (* raw cic term *) + emetasenv : string; (* expected metasenv *) eterm: string; (* expected term *) etype: string; (* expected type *) ereduced: string; (* expected reduced term *) } - (* this should be the only function here printing on stdout *) let print_test test fname = let oc = open_out fname in output_string oc (String.concat "" - [ test.term; rawsep ^ "\n"; - test.eterm; rawsep ^ "\n"; - test.etype; rawsep ^ "\n"; + [ test.term; + sprintf "%s (* METASENV after disambiguation *)\n" rawsep; + test.emetasenv; + sprintf "%s (* TERM after disambiguation *)\n" rawsep; + test.eterm; + sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep; + test.etype; + sprintf "%s (* REDUCED disambiguated term *)\n" rawsep; test.ereduced ]); close_out oc let parse_regtest = let term = Buffer.create 1024 in (* raw term *) + let emetasenv = Buffer.create 1024 in (* expected metasenv *) let eterm = Buffer.create 1024 in (* raw expected term *) let etype = Buffer.create 1024 in (* raw expected type *) let ereduced = Buffer.create 1024 in (* raw expected reducted term *) let state = ref Term in let bump_state () = match !state with - | Term -> state := ETerm + | Term -> state := EMetasenv + | EMetasenv -> state := ETerm | ETerm -> state := EType | EType -> state := EReduced | EReduced -> assert false in let buffer_of_state = function - | Term -> term | ETerm -> eterm | EType -> etype | EReduced -> ereduced + | Term -> term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype + | EReduced -> ereduced + in + let clear_buffers () = + List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ] in fun fname -> state := Term; - Buffer.clear term; Buffer.clear eterm; Buffer.clear etype; - Buffer.clear ereduced; + clear_buffers (); let ic = open_in fname in (try while true do @@ -97,81 +105,191 @@ let parse_regtest = done with End_of_file -> ()); { 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 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 cic_type = CicTypeChecker.type_of_aux' metasenv empty_context cic_term in - let cic_reduced = CicReduction.whd empty_context cic_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" + in + let ereduced = + try + CicPp.ppterm (CicReduction.whd empty_context cic_term) + with _ -> "MALFORMED" + in { term = raw_term; (* useless *) + emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; eterm = CicPp.ppterm cic_term ^ "\n"; - etype = CicPp.ppterm cic_type ^ "\n"; - ereduced = CicPp.ppterm cic_reduced ^ "\n"; + etype = etype ^ "\n"; + ereduced = ereduced ^ "\n"; } -let main () = - if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *) - print_msg "[ Gen mode ]"; - for i = 2 to argc - 1 do - let fname = Sys.argv.(i) in +let dump_environment filename = + try + let oc = open_out filename in + CicEnvironment.dump_to_channel oc; + close_out oc + with exc -> + prerr_endline + ("DUMP_ENVIRONMENT FAILURE, uncaught excecption " ^ + Printexc.to_string exc) ; + raise exc + +let restore_environment filename = + if Sys.file_exists filename then + begin + try + let ic = open_in filename in + CicEnvironment.restore_from_channel ic; + close_in ic + with exc -> + prerr_endline + ("RESTORE_ENVIRONMENT FAILURE, uncaught excecption " ^ + Printexc.to_string exc) ; + raise exc + end + else + CicEnvironment.empty () + +let main generate dump fnames tryvars varsprefix = + let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in + if generate then + begin + (* gen mode *) + print_endline "[ Gen mode ]"; + List.iter + (function fname -> let test_fname = fname ^ ".test" in - print_msg (sprintf "Generating regtest %s -> %s\n ..." + let env_fname = fname ^ ".env" in + 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 - print_test result test_fname - done - end else begin (* regtest mode *) - prerr_endline "[ Regtest mode ]"; + let result = test_this uri_pred raw_term in + print_test result test_fname ; + if dump then dump_environment env_fname ; + ) fnames + end else + begin + (* regtest mode *) + print_endline "[ Regtest mode ]"; let (ok, nok) = (ref 0, ref []) in - for i = 1 to argc - 1 do - let fname = Sys.argv.(i) in - prerr_endline ("# " ^ fname); - let expected = parse_regtest fname in - let actual = test_this expected.term in - if as_expected expected actual then - incr ok - else - nok := fname :: !nok; - done; - print_msg "Regtest completed:"; - print_msg (sprintf "Succeeded: %d" !ok); - print_msg (sprintf "Failed: %d" (List.length !nok)); - List.iter (fun fname -> print_msg (sprintf " %s failed :-(" fname)) + List.iter + (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 uri_pred expected.term in + if dump then dump_environment env_fname ; + if as_expected report_fname expected actual then + (incr ok ; true) + else + (nok := fname :: !nok ; false) + with e -> (nok := fname :: !nok ; false) + in + let timediff = Unix.gettimeofday () -. time in + print (sprintf "done in %f seconds\t" timediff) ; + print_endline + (if is_ok then + "[ OK ]" + else + "[ FAILED ]") + ) fnames ; + print_endline "*** Summary ***"; + print_endline (sprintf "Succeeded: %d" !ok); + print_endline (sprintf "Failed: %d" (List.length !nok)); + List.iter (fun fname -> print_endline (sprintf " %s failed :-(" fname)) (List.rev !nok) end -let _ = try main () with Invalid_argument _ -> usage () +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, "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 (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 !tryvars !varsprefix