From 5e1c4e50b88cd1b75a14a34b93297a3aba6af890 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 18:30:25 +0000 Subject: [PATCH] Improved output when [ MANY ] occurs. --- helm/gTopLevel/testlibrary.ml | 47 +++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 19 deletions(-) diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index e40981861..ea6e4c6c0 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -10,7 +10,6 @@ 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 @@ -21,7 +20,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 @@ -44,11 +50,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 res = + Disambiguate'.disambiguate_term mqi_handle [] [] new_ast + DisambiguateTypes.Environment.empty in List.iter - (fun (_, _, term) -> - debug_print ("term: " ^ CicPp.ppterm term)) - (Disambiguate'.disambiguate_term mqi_handle [] [] new_ast - DisambiguateTypes.Environment.empty) + (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,32 +68,30 @@ 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)); -- 2.39.2