X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=107cc3c549907ed1c6eb8b8473314d1043b6415b;hb=54a8531f102cada0ed596af02913c7b6d8acc086;hp=21173e9e5308221a81ddb53841c44a0ba2827e9e;hpb=9be7ec5bbacfafed8a3e37cfe0095f2aea1b9bf9;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 21173e9e5..107cc3c54 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,31 +1,35 @@ open Printf -let mqi_debug_fun = ignore +Helm_registry.load_from "gTopLevel.conf.xml";; + +let mqi_debug_fun s = + HelmLogger.log ~append_NL:true (`Msg (`T s)) 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 exception Failure of string -exception Multiple_interpretations let fail msg = raise (Failure msg) -let uri_predicate = ref BatchParser.constants_only +let uri_predicate = ref (BatchParser.constants_only ~prefix:"") module DisambiguateCallbacks = struct - let output_html ?(append_NL = true) msg = - if verbose then - (if append_NL then print_string else print_endline) - (Ui_logger.string_of_html_msg msg) - let interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices - let interactive_interpretation_choice _ = raise Multiple_interpretations - let input_or_locate_uri ~title = fail "Unknown identifier" + let interactive_interpretation_choice = + let rec aux n = + function + [] -> [] + | _::tl -> n::(aux (n+1) tl) + in + aux 0 + + let input_or_locate_uri ~title = fail ("Unknown identifier: " ^ title) end module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) @@ -33,7 +37,7 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) let debug_print s = prerr_endline ("^^^^^^ " ^ s) let test_uri uri = - let obj = CicCache.get_obj uri in + let obj = CicEnvironment.get_obj uri in let (annobj, _, _, ids_to_inner_sorts, _, _, _) = Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in @@ -43,12 +47,20 @@ 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); + let res = + Disambiguate'.disambiguate_term mqi_handle [] [] new_ast + DisambiguateTypes.Environment.empty in + List.iter + (fun (domain, _, term) -> + debug_print + ("domain: " ^ CicTextualParser2.EnvironmentP3.to_string domain) ; + debug_print ("term: " ^ CicPp.ppterm term) + ) res ; + List.length res in match annobj with | Cic.AConstant (_, _, _, None, ty, _) -> @@ -57,46 +69,44 @@ let test_uri uri = | Cic.AConstant (_, _, _, Some bo, ty, _) -> (* debug_print "Cic.AConstant (bo)"; - round_trip bo; + let n = round_trip bo in *) debug_print "Cic.AConstant (ty)"; - round_trip ty + round_trip ty (* + n *) | Cic.AVariable (_, _, None, ty, _) -> debug_print "Cic.AVariable (ty)"; round_trip ty | Cic.AVariable (_, _, Some bo, ty, _) -> +(* debug_print "Cic.AVariable (bo)"; - round_trip bo; + let n = round_trip bo in +*) debug_print "Cic.AVariable (ty)"; - round_trip ty - | Cic.ACurrentProof (_, _, _, _, proof, ty, _) -> - debug_print "Cic.ACurrentProof (proof)"; - round_trip proof; - debug_print "Cic.ACurrentProof (ty)"; - round_trip ty + round_trip ty (* + n *) + | Cic.ACurrentProof (_, _, _, _, _, _, _) -> + assert false | Cic.AInductiveDefinition _ -> - debug_print "AInductiveDefinition: boh ..." + debug_print "AInductiveDefinition: boh ..." ; + assert false let test_uri uri = try - test_uri uri; - `Ok + if test_uri uri = 1 then `Ok else `Maybe with - | Multiple_interpretations -> `Maybe | exn -> prerr_endline (sprintf "Top Level Uncaught Exception: %s" (Printexc.to_string exn)); `Nok -let report ok nok maybe = +let report (ok,nok,maybe) = print_newline (); print_endline "TestLibrary report"; print_endline "Succeeded URIs:"; - List.iter (fun s -> print_endline ("\t" ^ s)) ok; + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !ok); print_endline "Failed URIs:"; - List.iter (fun s -> print_endline ("\t" ^ s)) nok; + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok); print_endline "Multiple answers URIs:"; - List.iter (fun s -> print_endline ("\t" ^ s)) maybe; + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe); print_newline () let do_uri (ok, nok, maybe) uri = @@ -116,33 +126,45 @@ let do_uri (ok, nok, maybe) uri = let do_file status fname = try let ic = open_in fname in - while true do - let line = input_line ic in - try - let uri = UriManager.uri_of_string line in - do_uri status uri - with UriManager.IllFormedUri _ -> - printf "Error parsing URI '%s', ignoring it" line - done + (try + while true do + let line = input_line ic in + try + let uri = UriManager.uri_of_string line in + do_uri status uri + with UriManager.IllFormedUri _ -> + printf "Error parsing URI '%s', ignoring it" line + done + with End_of_file -> + close_in ic) with exn -> printf "Error trying to access '%s' (%s), skipping the file\n%!" fname (Printexc.to_string exn) let _ = + HelmLogger.register_log_callback + (fun ?(append_NL = true) msg -> + (if append_NL then prerr_endline else prerr_string) + (HelmLogger.string_of_html_msg msg)); let names = ref [] in let tryvars = ref false in - let varsprefix = ref "" in + let prefix = ref "" in + let varsprefix = ref "####" in let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in let spec = [ "-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" ; "-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 name -> names := name :: !names) usage; let names = List.rev !names in - uri_predicate := BatchParser.uri_pred_of_conf !tryvars !varsprefix; + if !varsprefix = "####" then varsprefix := !prefix ; + uri_predicate := + BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix; let status = (ref [], ref [], ref []) in (* URIs *) List.iter (fun name -> @@ -154,5 +176,5 @@ let _ = do_file status name else printf "Don't know what to do with '%s', ignoring it\n%!" name) - names - + names ; + report status