X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;fp=helm%2FgTopLevel%2Fregtest.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=c6b598151b2127babf3df6f449274fe41c857caa;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml deleted file mode 100644 index c6b598151..000000000 --- a/helm/gTopLevel/regtest.ml +++ /dev/null @@ -1,380 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -let argc = Array.length Sys.argv - -let rawsep = "###" -let sep = Pcre.regexp (sprintf "^%s" rawsep) -let sep2 = Pcre.regexp (sprintf "^%s%s" rawsep 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 | EEnv | EMetasenv | ETerm | EType | EReduced - -(* regtest file format - * < cic term in concrete syntax > - * separatorseparator INTERPRETATION NUMBER separatorseparator - * separator (* see sep above *) - * < expected disambiguating environment (EnvironmentP3.to_string) > - * separator (* see sep above *) - * < 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 (CicPp.ppterm) > - * separator (* see sep above *) - * < expected reduced cic term as (CicPp.ppterm) > - * ... (* repeat from ... INTERPRETATION NUMBER ... *) - *) - -type regtest = { - term: string; (* raw cic term *) - eenv : string; (* disambiguating parsing environment *) - emetasenv : string; (* expected metasenv *) - eterm: string; (* expected term *) - etype: string; (* expected type *) - ereduced: string; (* expected reduced term *) -} - -let print_test tests fname = - let oc = open_out fname in - output_string oc (List.hd tests).term; - let i = ref 0 in - List.iter - (function test -> - incr i ; - output_string oc - (String.concat "" - [ sprintf "%s%s INTERPRETATION NUMBER %d %s%s\n" rawsep rawsep !i rawsep rawsep ; - sprintf "%s (* disambiguation environment *)\n" rawsep; - test.eenv; - 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 ]) - ) tests; - close_out oc - -let parse_regtest = - let term = Buffer.create 1024 in (* raw term *) - let eenv = Buffer.create 1024 in (* disambiguating parser environment *) - 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 := EEnv - | EEnv -> state := EMetasenv - | EMetasenv -> state := ETerm - | ETerm -> state := EType - | EType -> state := EReduced - | EReduced -> assert false - in - let buffer_of_state = function - | Term -> term | EEnv -> eenv | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype - | EReduced -> ereduced - in - let clear_buffers () = - List.iter Buffer.clear [ eenv; emetasenv; eterm; etype; ereduced ] - in - fun fname -> - state := Term; - let first = ref true in - let res = ref [] in - let push_res () = - res := - {term = Buffer.contents term; - eenv = Buffer.contents eenv; - emetasenv = Buffer.contents emetasenv; - eterm = Buffer.contents eterm; - etype = Buffer.contents etype; - ereduced = Buffer.contents ereduced } :: !res ; - in - Buffer.clear term; - let ic = open_in fname in - (try - while true do - let line = input_line ic in - match line with - | l when Pcre.pmatch ~rex:sep2 l -> - if !first then first := false else push_res () ; - clear_buffers (); - state := Term - | l when Pcre.pmatch ~rex:sep l -> bump_state () - | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n") - done - with End_of_file -> ()); - 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; - in - let rec aux = - function - [],[] -> true - | ex::extl, fo::fotl -> - let outcome1 = as_expected_one och ex fo in - let outcome2 = aux (extl,fotl) in - outcome1 && outcome2 - | [],found -> - print_endline "### Too many interpretations found:" ; - List.iter print_interpretation found; - false - | expected,[] -> - print_endline "### Too few interpretations found:" ; - List.iter print_interpretation expected; - false - in - let outcome = aux (expected,found) in - (if Lazy.lazy_is_val och then close_out (Lazy.force och)) ; - outcome - -let test_this mqi_handle uri_pred raw_term = - let empty_context = [] in - List.map - (function (env, metasenv, cic_term) -> - 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 *) - eenv = DisambiguatingParser.EnvironmentP3.to_string env ^ "\n"; - emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; - eterm = CicPp.ppterm cic_term ^ "\n"; - etype = etype ^ "\n"; - ereduced = ereduced ^ "\n"; - } - ) (BatchParser.parse mqi_handle ~uri_pred raw_term) - -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 mqi_handle generate dump fnames tryvars prefix varsprefix = - let uri_pred = BatchParser.uri_pred_of_conf tryvars ~prefix ~varsprefix in - if generate then - begin - (* gen mode *) - print_endline "[ Gen mode ]"; - List.iter - (function fname -> - let test_fname = fname ^ ".test" in - let env_fname = fname ^ ".env" in - print_endline (sprintf "Generating regtest %s -> %s\n ..." - fname test_fname); - let raw_term = (List.hd (parse_regtest fname)).term in - let results = test_this mqi_handle uri_pred raw_term in - print_test results 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 - 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 mqi_handle uri_pred (List.hd 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 _ = - - Helm_registry.load_from "gTopLevel.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 mqi_debug_fun s = - HelmLogger.log ~append_NL:true (`Msg (`T s)) in - let mqi_handle = MQIConn.init ~log:mqi_debug_fun () in - - 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 prefix = ref "" 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)" ; - "-prefix", Arg.Set_string prefix, - "limit object choices to URIs beginning with prefix" ; - "--prefix", Arg.Set_string prefix, - "limit object choices to URIs beginning with prefix" ; - "-varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix; overrides -prefix" ; - "--varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix; overrides -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) ; - if !varsprefix = "###" then varsprefix := !prefix ; - main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix; - MQIConn.close mqi_handle