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
(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
-
+ 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
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
+ main dbd !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !prefix !varsprefix;
+ Mysql.disconnect dbd