X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fregtest.ml;h=bee1c28166a54f555ee0448253b4f32b08a6b774;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c146683ad4335c1d563311587e0f743662c960a5;hpb=edb6ab182b915ebc8b2810574b0a87bdab39d051;p=helm.git diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index c146683ad..bee1c2816 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -29,14 +29,18 @@ 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 | EMetasenv | ETerm | EType | EReduced +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 *) @@ -45,33 +49,44 @@ type state = Term | EMetasenv | ETerm | EType | EReduced * < 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 test fname = +let print_test tests fname = let oc = open_out fname in - output_string oc - (String.concat "" - [ 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 ]); + 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 *) @@ -79,49 +94,61 @@ let parse_regtest = let state = ref Term in let bump_state () = match !state with - | Term -> state := EMetasenv + | 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 | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype + | Term -> term | EEnv -> eenv | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced in let clear_buffers () = - List.iter Buffer.clear [ term; emetasenv; eterm; etype; ereduced ] + List.iter Buffer.clear [ eenv; emetasenv; eterm; etype; ereduced ] in fun fname -> state := Term; - clear_buffers (); + 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 -> ()); - { term = Buffer.contents term; - emetasenv = Buffer.contents emetasenv; - eterm = Buffer.contents eterm; - etype = Buffer.contents etype; - ereduced = Buffer.contents ereduced } + push_res () ; + List.rev !res -let as_expected report_fname expected found = (* ignores "term" field *) +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 && emetasenv_ok && etype_ok && ereduced_ok in - if outcome then - (if Sys.file_exists report_fname then Sys.remove report_fname) - else + let outcome = + eterm_ok && eenv_ok && emetasenv_ok && etype_ok && ereduced_ok + in begin - let och = open_out report_fname in - let print_endline = print_endline_to_channel och in + 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:"; @@ -129,6 +156,13 @@ let as_expected report_fname expected found = (* ignores "term" field *) 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:"; @@ -150,30 +184,71 @@ let as_expected report_fname expected found = (* ignores "term" field *) print_endline "# found:"; print_endline (" " ^ found.ereduced); end; - close_out och ; end; outcome -let test_this uri_pred raw_term = - let empty_context = [] 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" +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 ereduced = - try - CicPp.ppterm (CicReduction.whd empty_context cic_term) - with _ -> "MALFORMED" + 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 - { - term = raw_term; (* useless *) - emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; - eterm = CicPp.ppterm cic_term ^ "\n"; - etype = etype ^ "\n"; - ereduced = ereduced ^ "\n"; - } + 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,ugraph ) -> + let etype = + try + let ty, _ = + (CicTypeChecker.type_of_aux' metasenv empty_context cic_term ugraph) + in + CicPp.ppterm ty + 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 CicUniv.empty_ugraph) let dump_environment filename = try @@ -202,8 +277,8 @@ let restore_environment filename = else CicEnvironment.empty () -let main generate dump fnames tryvars varsprefix = - let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in +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 *) @@ -214,9 +289,9 @@ let main generate dump fnames tryvars varsprefix = 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 uri_pred raw_term in - print_test result 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 @@ -235,7 +310,7 @@ let main generate dump fnames tryvars varsprefix = let is_ok = try let expected = parse_regtest test_fname in - let actual = test_this uri_pred expected.term 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) @@ -259,12 +334,27 @@ let main generate dump fnames tryvars varsprefix = 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)); + Helm_registry.load_from "gTopLevel.conf.xml"; + let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () + 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 varsprefix = ref "" in + let prefix = ref "" in + let varsprefix = ref "###" in let usage = "regtest [OPTION] ... test1 ..." in let spec = ["-gen", Arg.Set gen, @@ -277,14 +367,19 @@ let _ = "--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" ; + "limit variable choices to URIs beginning with prefix; overrides -prefix" ; "--varsprefix", Arg.Set_string varsprefix, - "limit variable choices to URIs beginning with prefix" ; + "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) ; - main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix - + if !varsprefix = "###" then varsprefix := !prefix ; + main dbd !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix; + Mysql.disconnect dbd