(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 ->
- as_expected_one och ex fo &&
- aux (extl,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" ;
+ print_endline "### Too many interpretations found:" ;
+ List.iter print_interpretation found;
false
| expected,[] ->
- print_endline "### Too few interpretations found" ;
+ print_endline "### Too few interpretations found:" ;
+ List.iter print_interpretation expected;
false
in
let outcome = aux (expected,found) in
let test_this mqi_handle uri_pred raw_term =
let empty_context = [] in
List.map
- (function (env, metasenv, cic_term) ->
+ (function (env, metasenv, cic_term,ugraph ) ->
let etype =
try
- CicPp.ppterm
- (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
+ let ty, _ =
+ (CicTypeChecker.type_of_aux' metasenv empty_context cic_term ugraph)
+ in
+ CicPp.ppterm ty
with _ -> "MALFORMED"
in
let ereduced =
etype = etype ^ "\n";
ereduced = ereduced ^ "\n";
}
- ) (BatchParser.parse mqi_handle ~uri_pred raw_term)
+ ) (BatchParser.parse mqi_handle ~uri_pred raw_term CicUniv.empty_ugraph)
let dump_environment filename =
try
else
CicEnvironment.empty ()
-let main mqi_handle 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 *)
(fun ?(append_NL = true) msg ->
(if append_NL then prerr_endline else prerr_string)
(HelmLogger.string_of_html_msg msg));
-
- let mqi_debug_fun = ignore in
- let mqi_handle = MQIConn.init ~log:mqi_debug_fun () in
-
+ 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,
"--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 mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix;
- MQIConn.close mqi_handle
+ if !varsprefix = "###" then varsprefix := !prefix ;
+ main dbd !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix;
+ Mysql.disconnect dbd