X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Ftestlibrary.ml;h=ee1b982c41547aa6526628997d646226e316f52f;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=fc5fa2e79e022608fb78712e2706445732318df7;hpb=7938c0aa7ee2f7667dbdb74139043b095d646026;p=helm.git diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index fc5fa2e79..ee1b982c4 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -1,17 +1,21 @@ open Printf -let mqi_debug_fun = ignore +let time_out = ref 5;; + +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 ~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 @@ -19,7 +23,14 @@ module DisambiguateCallbacks = ~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 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 @@ -42,11 +53,16 @@ let test_uri uri = 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 (_, _, term) = - Disambiguate'.disambiguate_term mqi_handle [] [] new_ast - DisambiguateTypes.Environment.empty - in - debug_print ("term: " ^ CicPp.ppterm term) + 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, _) -> @@ -55,38 +71,53 @@ 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 + +exception TimeOut;; + +ignore + (Sys.signal Sys.sigalrm + (Sys.Signal_handle + (fun _ -> + (* We do this in case that some "with _" intercepts the first exception *) + ignore (Unix.alarm 1) ; + raise TimeOut))) +;; + let test_uri uri = try - test_uri uri; - `Ok + ignore (Unix.alarm !time_out) ; + if test_uri uri = 1 then `Ok else `Maybe with - | Multiple_interpretations -> `Maybe + | TimeOut -> + (* We do this to clear the alarm set by the signal handler *) + ignore (Unix.alarm 0) ; + `TimeOut | exn -> prerr_endline (sprintf "Top Level Uncaught Exception: %s" (Printexc.to_string exn)); `Nok -let report (ok,nok,maybe) = +let report (ok,nok,maybe,timeout) = print_newline (); print_endline "TestLibrary report"; print_endline "Succeeded URIs:"; @@ -95,9 +126,12 @@ let report (ok,nok,maybe) = List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !nok); print_endline "Multiple answers URIs:"; List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !maybe); + print_newline (); + print_endline ("URIs that timeout (" ^ string_of_int !time_out ^ "s):"); + List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout); print_newline () -let do_uri (ok, nok, maybe) uri = +let do_uri (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 @@ -110,6 +144,9 @@ let do_uri (ok, nok, maybe) uri = | `Maybe -> print_endline "[ MANY ]"; maybe := uri_str :: !maybe + | `TimeOut -> + print_endline "[TIMEOUT!]"; + timeout := uri_str :: !timeout let do_file status fname = try @@ -130,26 +167,32 @@ let do_file status fname = fname (Printexc.to_string exn) let _ = - Helm_registry.load_from "gTopLevel.conf.xml"; 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" ; + "-timeout", Arg.Set_int time_out, + "number of seconds before a timeout; 0 means no timeout" ] 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; - let status = (ref [], ref [], ref []) in (* URIs *) + if !varsprefix = "####" then varsprefix := !prefix ; + uri_predicate := + BatchParser.uri_pred_of_conf !tryvars ~prefix:!prefix ~varsprefix:!varsprefix; + let status = (ref [], ref [], ref [], ref []) in (* URIs *) List.iter (fun name -> try