ocaml 3.09 transition

[helm.git] / helm / gTopLevel / testlibrary.ml

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index fccdc19c619530b67093437c77a00254b2534869..34f71d41201601264975689ad6dd4249b6923aaa 100644 (file)
--- 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
 
@@ -38,8 +46,13 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
 
 let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 
-let test_uri uri =
-  let obj = CicEnvironment.get_obj uri in
+let test_uri typecheck uri =
+  if typecheck then
+    try ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);1
+    with CicTypeChecker.TypeCheckerFailure s | 
+         CicTypeChecker.AssertFailure s -> 0
+  else
+  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
@@ -47,17 +60,19 @@ let test_uri 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)
@@ -103,10 +118,10 @@ ignore
 ;;
 
 
-let test_uri uri =
+let test_uri typecheck uri =
   try
    ignore (Unix.alarm !time_out) ;
-   if test_uri uri = 1 then `Ok else `Maybe
+   if test_uri typecheck uri = 1 then `Ok else `Maybe
   with
   | TimeOut ->
      (* We do this to clear the alarm set by the signal handler *)
@@ -133,10 +148,10 @@ let report (ok,nok,maybe,timeout) =
   List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
   print_newline ()
 
-let do_uri (ok, nok, maybe, timeout) uri =
+let do_uri typecheck (ok, nok, maybe, timeout) uri =
   let uri_str = UriManager.string_of_uri uri in
   printf "Testing URI: %-55s %!" (uri_str ^ " ...");
-  match test_uri uri with
+  (match test_uri typecheck uri with
   | `Ok ->
       print_endline "\e[01;32m[   OK   ]\e[00m";
       ok := uri_str :: !ok
@@ -148,9 +163,9 @@ let do_uri (ok, nok, maybe, timeout) uri =
       maybe := uri_str :: !maybe
   | `TimeOut ->
       print_endline "\e[01;34m[TIMEOUT!]\e[00m";
-      timeout := uri_str :: !timeout
+      timeout := uri_str :: !timeout)
 
-let do_file status fname =
+let do_file typecheck status fname =
   try
     let ic = open_in fname in
     (try
@@ -158,7 +173,7 @@ let do_file status fname =
         let line = input_line ic in
         try
           let uri = UriManager.uri_of_string line in
-          do_uri status uri
+          do_uri typecheck status uri
         with UriManager.IllFormedUri _ ->
           printf "Error parsing URI '%s', ignoring it" line
       done
@@ -175,6 +190,7 @@ let _ =
        (HelmLogger.string_of_html_msg msg));
   let names = ref [] in
   let tryvars = ref false in
+  let typecheck = ref false in
   let prefix = ref "" in
   let varsprefix = ref "####" in
   let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
@@ -186,7 +202,8 @@ let _ =
       "-varsprefix", Arg.Set_string varsprefix,
         "limit variable choices to URIs beginning with prefix; overrides -prefix" ;
       "-timeout", Arg.Set_int time_out,
-       "number of seconds before a timeout; 0 means no timeout"
+       "number of seconds before a timeout; 0 means no timeout";
+       "-typecheck", Arg.Set typecheck, "simply typechek the uri"
     ]
   in
   Arg.parse spec (fun name -> names := name :: !names) usage;
@@ -199,10 +216,10 @@ let _ =
     (fun name ->
       try
         let uri = UriManager.uri_of_string name in
-        do_uri status uri
+        do_uri !typecheck status uri
       with UriManager.IllFormedUri _ ->
         if Sys.file_exists name then
-          do_file status name
+          do_file !typecheck status name
         else
           printf "Don't know what to do with '%s', ignoring it\n%!" name)
     names ;