From 29442b4d21cf07992ad4e5c981085dada1f90fe4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 13:20:11 +0000 Subject: [PATCH] The disambiguation now returns a list of interpretations. Note: the regtest is broken by this commit. --- helm/gTopLevel/batchParser.ml | 20 +++-- helm/gTopLevel/batchParser.mli | 4 +- helm/gTopLevel/disambiguatingParser.mli | 6 +- helm/gTopLevel/gTopLevel.ml | 2 +- helm/gTopLevel/oldDisambiguate.ml | 15 ++-- helm/gTopLevel/oldDisambiguate.mli | 4 +- helm/gTopLevel/regtest.ml | 112 +++++++++++++++--------- helm/gTopLevel/termEditor.ml | 4 + helm/gTopLevel/testlibrary.ml | 10 +-- helm/gTopLevel/texTermEditor.ml | 8 +- 10 files changed, 114 insertions(+), 71 deletions(-) diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index 7cbc31201..515c417cb 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -44,7 +44,14 @@ module DisambiguateCallbacks = ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id choices = List.filter !uri_predicate choices - let interactive_interpretation_choice _ = fail "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" end @@ -59,12 +66,11 @@ let parse mqi_handle ?(uri_pred = constants_only) = let empty_context = [] in let empty_metasenv = [] in fun input -> - let (_, metasenv, term) = - Disambiguate'.disambiguate_term - mqi_handle empty_context empty_metasenv input empty_environment - in - (metasenv, term) + List.map (fun (_,metasenv,term) -> metasenv,term) + (Disambiguate'.disambiguate_term + mqi_handle empty_context empty_metasenv input empty_environment) let parse_pp mqi_handle ?uri_pred input = - CicPp.ppterm (snd (parse mqi_handle ?uri_pred input)) + List.map (fun (_,t) -> CicPp.ppterm t) + (parse mqi_handle ?uri_pred input) diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index ba5d5ab58..ff82e6fa0 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -37,10 +37,10 @@ val uri_pred_of_conf: bool -> string -> (string -> bool) * batch mode if possible, otherwise raises Failure above. * uri_pred is the predicate used to select which uris are tried. Per default * only constant URIs are accepted *) -val parse: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> Cic.metasenv * Cic.term +val parse: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> (Cic.metasenv * Cic.term) list (** as above, but instead of returning the parsed cic term, pretty prints it * (ignoring returned metasenv) *) -val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string +val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string list diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 5ddf68377..620198a52 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -41,8 +41,8 @@ module Make (C : DisambiguateTypes.Callbacks) : Cic.metasenv -> string -> EnvironmentP3.t -> (* previous interpretation status *) - EnvironmentP3.t * (* new interpretation status *) - Cic.metasenv * (* new metasenv *) - Cic.term (* disambiguated term *) + (EnvironmentP3.t * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term) list (* disambiguated term *) end diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 9ff7e8fc6..5df73dc1c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -379,7 +379,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index 39be585e5..9b1d4937c 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -46,7 +46,7 @@ module type Callbacks = ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list val interactive_interpretation_choice : - (string * string) list list -> int + (string * string) list list -> int list val input_or_locate_uri : title:string -> UriManager.uri end ;; @@ -232,10 +232,10 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; exit 1 end ) resolve_ids ; - let resolve_id',term,metasenv' = + let res = match resolve_ids with [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput - | [resolve_id] -> resolve_id + | [_] -> resolve_ids | _ -> let choices = List.map @@ -266,10 +266,13 @@ prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; ) dom ) resolve_ids in - let index = C.interactive_interpretation_choice choices in - List.nth resolve_ids index + let indexes = C.interactive_interpretation_choice choices in + List.map (List.nth resolve_ids) indexes in - (known_ids @ dom', resolve_id'), metasenv',term + List.map + (fun (resolve_id',term,metasenv') -> + (known_ids @ dom', resolve_id'), metasenv',term + ) res end ;; diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli index 8fcc1c934..d9cc5840d 100644 --- a/helm/gTopLevel/oldDisambiguate.mli +++ b/helm/gTopLevel/oldDisambiguate.mli @@ -44,7 +44,7 @@ module type Callbacks = ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list val interactive_interpretation_choice : - (string * string) list list -> int + (string * string) list list -> int list val input_or_locate_uri : title:string -> UriManager.uri end @@ -62,7 +62,7 @@ module Make (C : Callbacks) : CicTextualParser0.interpretation_domain_item list -> (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) -> id_to_uris:domain_and_interpretation -> - domain_and_interpretation * Cic.metasenv * Cic.term + (domain_and_interpretation * Cic.metasenv * Cic.term) list end module EnvironmentP3 : diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 76621b5ec..4142afa1a 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -55,19 +55,26 @@ type regtest = { ereduced: string; (* expected reduced term *) } -let print_test test fname = +let print_test tests fname = let oc = open_out fname in - output_string oc - (String.concat "" - [ test.term; - sprintf "%s (* METASENV after disambiguation *)\n" rawsep; - test.emetasenv; - sprintf "%s (* TERM after disambiguation *)\n" rawsep; - test.eterm; - sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep; - test.etype; - sprintf "%s (* REDUCED disambiguated term *)\n" rawsep; - test.ereduced ]); + output_string oc (List.hd tests).term; + let i = ref 0 in + List.iter + (function test -> + incr i ; + output_string oc + (String.concat "" + [ sprintf "INTERPRETATION NUMBER %d\n" !i; + sprintf "%s (* METASENV after disambiguation *)\n" rawsep; + test.emetasenv; + sprintf "%s (* TERM after disambiguation *)\n" rawsep; + test.eterm; + sprintf "%s (* TYPE_OF the disambiguated term *)\n" rawsep; + test.etype; + sprintf "%s (* REDUCED disambiguated term *)\n" rawsep; + test.ereduced; + "\n" ]) + ) tests; close_out oc let parse_regtest = @@ -104,24 +111,20 @@ let parse_regtest = | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n") done with End_of_file -> ()); - { term = Buffer.contents term; + [{ term = Buffer.contents term; emetasenv = Buffer.contents emetasenv; eterm = Buffer.contents eterm; etype = Buffer.contents etype; - ereduced = Buffer.contents ereduced } + ereduced = Buffer.contents ereduced }] -let as_expected report_fname expected found = (* ignores "term" field *) +let as_expected_one och expected found = (* ignores "term" field *) let eterm_ok = expected.eterm = found.eterm in let emetasenv_ok = expected.emetasenv = found.emetasenv in let etype_ok = expected.etype = found.etype in let ereduced_ok = expected.ereduced = found.ereduced in let outcome = eterm_ok && emetasenv_ok && etype_ok && ereduced_ok in - if outcome then - (if Sys.file_exists report_fname then Sys.remove report_fname) - else begin - let och = open_out report_fname in - let print_endline = print_endline_to_channel och in + let print_endline = print_endline_to_channel (Lazy.force och) in if not eterm_ok then begin print_endline "### Term mismatch ###"; print_endline "# expected:"; @@ -150,30 +153,53 @@ let as_expected report_fname expected found = (* ignores "term" field *) print_endline "# found:"; print_endline (" " ^ found.ereduced); end; - close_out och ; end; outcome +let as_expected report_fname expected found = + (if Sys.file_exists report_fname then Sys.remove report_fname) ; + let och = lazy (open_out report_fname) in + let print_endline = print_endline_to_channel (Lazy.force och) in + let rec aux = + function + [],[] -> true + | ex::extl, fo::fotl -> + as_expected_one och ex fo && + aux (extl,fotl) + | [],found -> + print_endline "### Too many interpretations found" ; + false + | expected,[] -> + print_endline "### Too few interpretations found" ; + false + in + let outcome = aux (expected,found) in + (if Lazy.lazy_is_val och then close_out (Lazy.force och)) ; + outcome + let test_this mqi_handle uri_pred raw_term = let empty_context = [] in - let (metasenv, cic_term) = BatchParser.parse mqi_handle ~uri_pred raw_term in - let etype = - try - CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) - with _ -> "MALFORMED" - in - let ereduced = - try - CicPp.ppterm (CicReduction.whd empty_context cic_term) - with _ -> "MALFORMED" - in - { - term = raw_term; (* useless *) - emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; - eterm = CicPp.ppterm cic_term ^ "\n"; - etype = etype ^ "\n"; - ereduced = ereduced ^ "\n"; - } + List.map + (function (metasenv, cic_term) -> + let etype = + try + CicPp.ppterm + (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) + with _ -> "MALFORMED" + in + let ereduced = + try + CicPp.ppterm (CicReduction.whd empty_context cic_term) + with _ -> "MALFORMED" + in + { + term = raw_term; (* useless *) + emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n"; + eterm = CicPp.ppterm cic_term ^ "\n"; + etype = etype ^ "\n"; + ereduced = ereduced ^ "\n"; + } + ) (BatchParser.parse mqi_handle ~uri_pred raw_term) let dump_environment filename = try @@ -214,9 +240,9 @@ let main mqi_handle generate dump fnames tryvars varsprefix = let env_fname = fname ^ ".env" in print_endline (sprintf "Generating regtest %s -> %s\n ..." fname test_fname); - let raw_term = (parse_regtest fname).term in - let result = test_this mqi_handle uri_pred raw_term in - print_test result test_fname ; + let raw_term = (List.hd (parse_regtest fname)).term in + let results = test_this mqi_handle uri_pred raw_term in + print_test results test_fname ; if dump then dump_environment env_fname ; ) fnames end else @@ -235,7 +261,7 @@ let main mqi_handle generate dump fnames tryvars varsprefix = let is_ok = try let expected = parse_regtest test_fname in - let actual = test_this mqi_handle uri_pred expected.term in + let actual = test_this mqi_handle uri_pred (List.hd expected).term in if dump then dump_environment env_fname ; if as_expected report_fname expected actual then (incr ok ; true) diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index db637554f..3a74ef051 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -99,8 +99,12 @@ module Make(C:DisambiguateTypes.Callbacks) = ) context in let environment',metasenv,expr = + match Disambiguate'.disambiguate_term mqi_handle context metasenv (input#buffer#get_text ()) !environment + with + [environment',metasenv,expr] -> environment',metasenv,expr + | _ -> assert false in environment := environment'; (metasenv, expr) diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index 6c76a6b2d..e40981861 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -44,11 +44,11 @@ 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) + 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, _) -> diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index b5dea9816..e06950508 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -211,8 +211,12 @@ module Make(C:DisambiguateTypes.Callbacks) = in debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ; let environment',metasenv,expr = - Disambiguate'.disambiguate_term mqi_handle - context metasenv (Mathml_editor.get_tex tex_editor) !environment + match + Disambiguate'.disambiguate_term mqi_handle + context metasenv (Mathml_editor.get_tex tex_editor) !environment + with + [environment',metasenv,expr] -> environment',metasenv,expr + | _ -> assert false in environment := environment' ; metasenv,expr -- 2.39.2