X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=34f71d41201601264975689ad6dd4249b6923aaa;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f35ee096a23f5fa63b0abf1efc06ff33ba1d7d60;hpb=cf8abaf99bf9065c82d8f668d441bc4c0a2a13df;p=helm.git

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index f35ee096a..34f71d412 100644
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -8,7 +8,15 @@ Helm_registry.load_from "gTopLevel.conf.xml";;
 let mqi_debug_fun s =
  HelmLogger.log ~append_NL:true (`Msg (`T s))
 let mqi_flags = []
+
+let dbd = Mysql.quick_connect
+    ~host:(Helm_registry.get "db.host")
+    ~user:(Helm_registry.get "db.user")
+    ~database:(Helm_registry.get "db.database")
+    ()
+(*
 let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
+*)
 
 let verbose = false
 
@@ -40,11 +48,11 @@ let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
 let test_uri typecheck uri =
   if typecheck then
-    try ignore(CicTypeChecker.typecheck uri);1
+    try ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);1
     with CicTypeChecker.TypeCheckerFailure s | 
          CicTypeChecker.AssertFailure s -> 0
   else
-  let obj = CicEnvironment.get_obj uri in
+  let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
     Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
   in
@@ -52,17 +60,19 @@ let test_uri typecheck uri =
   let round_trip annterm =
     debug_print "(1) acic -> ast";
     let (ast, _) =
-      Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
+      Acic2Ast.ast_of_acic ids_to_inner_sorts (*ids_to_uris*) annterm
     in
     let new_pp = BoxPp.pp_term ast in
     debug_print ("ast:\n" ^ new_pp);
     let new_ast = CicTextualParser2.parse_term (Stream.of_string new_pp) in
     debug_print ("new_ast:\n" ^ CicAstPp.pp_term ast);
     let res =
-     Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
-      DisambiguateTypes.Environment.empty in
+     Disambiguate'.disambiguate_term ~dbd [] [] new_ast
+      ~aliases:DisambiguateTypes.Environment.empty 
+      ~initial_ugraph:CicUniv.empty_ugraph 
+    in
     List.iter
-     (fun (domain, _, term) ->
+     (fun (domain, _, term, _) ->
        debug_print
         ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ;
        debug_print ("term: " ^ CicPp.ppterm term)
@@ -153,10 +163,7 @@ let do_uri typecheck (ok, nok, maybe, timeout) uri =
       maybe := uri_str :: !maybe
   | `TimeOut ->
       print_endline "[TIMEOUT!]";
-      timeout := uri_str :: !timeout);
-  print_endline "--";
-  print_endline (CicUniv.print_stats ());
-  print_endline "--"
+      timeout := uri_str :: !timeout)
 
 let do_file typecheck status fname =
   try