...

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

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
index 5abdec6e183935b77ca6a9925f8ec2de97ec3f0c..e40981861ff756fd3d75b8d12e9ae2d4b011581e 100644 (file)
--- a/helm/gTopLevel/testlibrary.ml
+++ b/helm/gTopLevel/testlibrary.ml
@@ -1,9 +1,11 @@
 
 open Printf
 
+Helm_registry.load_from "gTopLevel.conf.xml";;
+
 let mqi_debug_fun = ignore
 let mqi_flags = []
-let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
+let mqi_handle = MQIConn.init ~flags:mqi_flags ~log:mqi_debug_fun ()
 
 let verbose = false
 
@@ -20,7 +22,7 @@ module DisambiguateCallbacks =
      List.filter !uri_predicate choices
 
   let interactive_interpretation_choice _ = raise Multiple_interpretations
-  let input_or_locate_uri ~title = fail "Unknown identifier"
+  let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title)
  end
 
 module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
@@ -38,12 +40,15 @@ let test_uri uri =
     let (ast, _) =
       Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
     in
-    debug_print ("ast: " ^ CicAstPp.pp_term ast);
-    let (_, _, term) =
-      Disambiguate'.disambiguate_term mqi_handle [] [] ast
-        DisambiguateTypes.Environment.empty
-    in
-    debug_print ("term: " ^ CicPp.ppterm term)
+    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);
+    List.iter
+     (fun (_, _, term) ->
+       debug_print ("term: " ^ CicPp.ppterm term))
+     (Disambiguate'.disambiguate_term mqi_handle [] [] new_ast
+       DisambiguateTypes.Environment.empty)
   in
   match annobj with
   | Cic.AConstant (_, _, _, None, ty, _) ->
@@ -127,7 +132,6 @@ let do_file status fname =
       fname (Printexc.to_string exn)
 
 let _ =
-  Helm_registry.load_from "triciclo.conf.xml";
   HelmLogger.register_log_callback
    (fun ?(append_NL = true) msg ->
      (if append_NL then prerr_endline else prerr_string)