From 12809955a4a6c693072f5b924603165f83cc382e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 23 Jan 2004 15:30:33 +0000 Subject: [PATCH] - Added DisambiguatingParser (that abstracts both the parser and the disambiguator used) - Added ChosenTermEditor (used to swap quickly the editor used). - moved disambiguate.ml* to oldDisambiguate.ml* --- helm/gTopLevel/.depend | 18 +- helm/gTopLevel/Makefile | 14 +- helm/gTopLevel/chosenTermEditor.ml | 7 + helm/gTopLevel/chosenTermEditor.mli | 23 ++ helm/gTopLevel/disambiguatingParser.ml | 81 +++++++ helm/gTopLevel/disambiguatingParser.mli | 48 ++++ helm/gTopLevel/gTopLevel.ml | 82 +------ helm/gTopLevel/oldDisambiguate.ml | 281 ++++++++++++++++++++++++ helm/gTopLevel/oldDisambiguate.mli | 67 ++++++ helm/gTopLevel/termEditor.ml | 33 ++- helm/gTopLevel/termEditor.mli | 8 +- 11 files changed, 552 insertions(+), 110 deletions(-) create mode 100644 helm/gTopLevel/chosenTermEditor.ml create mode 100644 helm/gTopLevel/chosenTermEditor.mli create mode 100644 helm/gTopLevel/disambiguatingParser.ml create mode 100644 helm/gTopLevel/disambiguatingParser.mli create mode 100644 helm/gTopLevel/oldDisambiguate.ml create mode 100644 helm/gTopLevel/oldDisambiguate.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index b8aab90b4..9ff1f45de 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,11 +1,17 @@ +termEditor.cmi: disambiguatingParser.cmi invokeTactics.cmi: termEditor.cmi termViewer.cmi hbugs.cmi: invokeTactics.cmi +chosenTermEditor.cmi: disambiguatingParser.cmi proofEngine.cmo: proofEngine.cmi proofEngine.cmx: proofEngine.cmi logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi -termEditor.cmo: termEditor.cmi -termEditor.cmx: termEditor.cmi +oldDisambiguate.cmo: oldDisambiguate.cmi +oldDisambiguate.cmx: oldDisambiguate.cmi +disambiguatingParser.cmo: disambiguatingParser.cmi +disambiguatingParser.cmx: disambiguatingParser.cmi +termEditor.cmo: disambiguatingParser.cmi termEditor.cmi +termEditor.cmx: disambiguatingParser.cmx termEditor.cmi xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi chosenTransformer.cmo: chosenTransformer.cmi @@ -20,7 +26,11 @@ invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ termViewer.cmx invokeTactics.cmi hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi -gTopLevel.cmo: chosenTransformer.cmi hbugs.cmi invokeTactics.cmi \ +chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi +chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi +gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \ + disambiguatingParser.cmi hbugs.cmi invokeTactics.cmi \ logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi -gTopLevel.cmx: chosenTransformer.cmx hbugs.cmx invokeTactics.cmx \ +gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \ + disambiguatingParser.cmx hbugs.cmx invokeTactics.cmx \ logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index fe1ccddd7..bcf0b74ff 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,9 +1,8 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ - helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ - helm-mathql helm-mathql_interpreter helm-mathql_generator \ - helm-tactics threads hbugs-client mathml-editor \ - helm-cic_transformations helm-logger helm-cic_textual_parser2 + gdome2-xslt helm-mathql_interpreter helm-mathql_generator \ + helm-tactics hbugs-client mathml-editor helm-cic_transformations \ + helm-cic_textual_parser2 PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLFIND = ocamlfind @@ -23,9 +22,10 @@ stop: $(MAKE) -C ../hbugs/ stop INTERFACE_FILES = \ - proofEngine.mli logicalOperations.mli \ - termEditor.mli xmlDiff.mli chosenTransformer.mli termViewer.mli \ - invokeTactics.mli hbugs.mli + proofEngine.mli logicalOperations.mli oldDisambiguate.mli \ + disambiguatingParser.mli termEditor.mli xmlDiff.mli chosenTransformer.mli \ + termViewer.mli invokeTactics.mli hbugs.mli chosenTermEditor.mli +# texTermEditor.mli DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml diff --git a/helm/gTopLevel/chosenTermEditor.ml b/helm/gTopLevel/chosenTermEditor.ml new file mode 100644 index 000000000..f6a7b0380 --- /dev/null +++ b/helm/gTopLevel/chosenTermEditor.ml @@ -0,0 +1,7 @@ +(* +module ChosenTermEditor = TexTermEditor;; +*) +module ChosenTermEditor = TermEditor;; + +module Make = ChosenTermEditor.Make;; +class type term_editor = ChosenTermEditor.term_editor;; diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli new file mode 100644 index 000000000..962aa0532 --- /dev/null +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -0,0 +1,23 @@ +class type term_editor = + object + method coerce : GObj.widget + method get_as_string : string + method get_metasenv_and_term : + context:Cic.context -> + metasenv:Cic.metasenv -> Cic.metasenv * Cic.term + method environment : DisambiguatingParser.Environment.t ref + method reset : unit + method set_term : string -> unit + end + +module Make : + functor (C : Disambiguate_types.Callbacks) -> + sig + val term_editor : + MQIConn.handle -> + ?packing:(GObj.widget -> unit) -> + ?width:int -> + ?height:int -> + ?isnotempty_callback:(bool -> unit) -> + ?share_environment_with:term_editor -> unit -> term_editor + end diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml new file mode 100644 index 000000000..057cacb42 --- /dev/null +++ b/helm/gTopLevel/disambiguatingParser.ml @@ -0,0 +1,81 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception NoWellTypedInterpretation + +module Environment = + struct + type t = Disambiguate_types.environment + + let empty = Disambiguate_types.Environment.empty + + let to_string env = +prerr_endline "TODO: implement and move away" ; + Disambiguate_types.Environment.fold + (fun i v s -> + match i with + | Disambiguate_types.Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v) + | _ -> "") + env "" + + let of_string inputtext = + let regexpr = + let alfa = "[a-zA-Z_-]" in + let digit = "[0-9]" in + let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in + let blanks = "\( \|\t\|\n\)+" in + let nonblanks = "[^ \t\n]+" in + let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) + Str.regexp + ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") + in + let rec aux n = + try + let n' = Str.search_forward regexpr inputtext n in + let id = Disambiguate_types.Id (Str.matched_group 2 inputtext) in + let uri = "cic:" ^ (Str.matched_group 5 inputtext) in + let resolve_id = aux (n' + 1) in + if Disambiguate_types.Environment.mem id resolve_id then + resolve_id + else + let term = Disambiguate.term_of_uri uri in + (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term)) + resolve_id) + with + Not_found -> Disambiguate_types.Environment.empty + in + aux 0 + end +;; + +module Make (C : Disambiguate_types.Callbacks) = + struct + let disambiguate_term mqi_handle context metasenv term_as_string environment = + let module Disambiguate' = Disambiguate.Make (C) in + let term = Parser.parse_term (Stream.of_string term_as_string) in + Disambiguate'.disambiguate_term + mqi_handle context metasenv term environment + end +;; diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli new file mode 100644 index 000000000..6edb84239 --- /dev/null +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception NoWellTypedInterpretation + +module Environment : + sig + type t + val empty : t + val to_string : t -> string + val of_string : string -> t + end + +module Make (C : Disambiguate_types.Callbacks) : + sig + val disambiguate_term : + MQIConn.handle -> + Cic.context -> + Cic.metasenv -> + string -> + Environment.t -> (* previous interpretation status *) + Environment.t * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.term (* disambiguated term *) + end + diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d54236fd8..76ebe6cc6 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -719,7 +719,7 @@ let load_unfinished_proof () = let edit_aliases () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let id_to_uris = inputt#id_to_uris in + let id_to_uris = inputt#environment in let chosen = ref false in let window = GWindow.window @@ -744,66 +744,14 @@ let edit_aliases () = ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - let resolve_id = !id_to_uris in ignore (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) - (Disambiguate_types.Environment.fold - (fun i v s -> - match i with - | Disambiguate_types.Id id -> s ^ sprintf "alias %s %s\n" id (fst v) - | _ -> "") - resolve_id "")) ; -(* - (function v -> - let uri = - match resolve_id v with - None -> assert false - | Some (CicTextualParser0.Uri uri) -> uri - | Some (CicTextualParser0.Term _) - | Some CicTextualParser0.Implicit -> assert false - in - "alias " ^ - (match v with - CicTextualParser0.Id id -> id - | CicTextualParser0.Symbol (descr,_) -> - (* CSC: To be implemented *) - assert false - )^ " " ^ (string_of_cic_textual_parser_uri uri) - ) -*) + (DisambiguatingParser.Environment.to_string !id_to_uris)) ; window#show () ; GtkThread.main (); if !chosen then - let resolve_id = - let inputtext = input#buffer#get_text () in - let regexpr = - let alfa = "[a-zA-Z_-]" in - let digit = "[0-9]" in - let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in - let blanks = "\( \|\t\|\n\)+" in - let nonblanks = "[^ \t\n]+" in - let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) - Str.regexp - ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") - in - let rec aux n = - try - let n' = Str.search_forward regexpr inputtext n in - let id = Disambiguate_types.Id (Str.matched_group 2 inputtext) in - let uri = "cic:" ^ (Str.matched_group 5 inputtext) in - let resolve_id = aux (n' + 1) in - if Disambiguate_types.Environment.mem id resolve_id then - resolve_id - else - let term = Disambiguate.term_of_uri uri in - (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term)) - resolve_id) - with - Not_found -> TermEditor.empty_id_to_uris - in - aux 0 - in - id_to_uris := resolve_id + id_to_uris := + DisambiguatingParser.Environment.of_string (input#buffer#get_text ()) ;; let proveit () = @@ -1083,18 +1031,8 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) -(* -module ChosenTermEditor = TexTermEditor;; -module ChosenTextualParser0 = TexCicTextualParser0;; -*) -module ChosenTermEditor = TermEditor;; -module ChosenTextualParser0 = CicTextualParser0;; - module Callbacks = struct - let get_metasenv () = !ChosenTextualParser0.metasenv - let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv - let output_html ?append_NL = output_html ?append_NL (outputhtml ()) let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> @@ -1254,7 +1192,7 @@ let new_inductive () = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (*non_empty_type := b ;*) @@ -1366,7 +1304,7 @@ let new_inductive () = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (* (*non_empty_type := b ;*) @@ -1513,18 +1451,14 @@ let new_proof () = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> non_empty_type := b ; okb#misc#set_sensitive (b && uri_entry#text <> "")) in let _ = -let xxx = inputt#get_as_string in - newinputt#set_term xxx ; -(* - newinputt#set_term inputt#get_as_string ; -*) + newinputt#set_term inputt#get_as_string ; inputt#reset in let _ = uri_entry#connect#changed diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml new file mode 100644 index 000000000..6338690bc --- /dev/null +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -0,0 +1,281 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(******************************************************************************) + +open Printf + +(** This module provides a functor to disambiguate the input **) +(** given a set of user-interface call-backs **) + +module type Callbacks = + sig + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit + val interactive_user_uri_choice : + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?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 + val input_or_locate_uri : title:string -> UriManager.uri + end +;; + +type domain_and_interpretation = + CicTextualParser0.interpretation_domain_item list * + CicTextualParser0.interpretation +;; + +module Make(C:Callbacks) = + struct + + let locate_one_id mqi_handle id = + let query = MQueryGenerator.locate id in + let result = MQueryInterpreter.execute mqi_handle query in + let uris = + List.map + (function uri,_ -> + MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + C.output_html (`Msg (`T "Locate query:")); + MQueryUtil.text_of_query + (fun s -> C.output_html ~append_NL:false (`Msg (`T s))) + "" query; + C.output_html (`Msg (`T "Result:")); + MQueryUtil.text_of_result (fun s -> C.output_html (`Msg (`T s))) "" result; + let uris' = + match uris with + [] -> + [UriManager.string_of_uri + (C.input_or_locate_uri + ~title:("URI matching \"" ^ id ^ "\" unknown."))] + | [uri] -> [uri] + | _ -> + C.interactive_user_uri_choice + ~selection_mode:`MULTIPLE + ~ok:"Try every selection." + ~enable_button_for_non_vars:true + ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + ~id + uris + in + List.map MQueryMisc.cic_textual_parser_uri_of_string uris' + + + exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput + + type test_result = + Ok of Cic.term * Cic.metasenv + | Ko + | Uncertain + + type ambiguous_choices = + Uris of CicTextualParser0.uri list + | Symbols of (CicTextualParser0.interpretation -> Cic.term) list + + let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris= + let known_ids,resolve_id = id_to_uris in + let dom' = + let rec filter = + function + [] -> [] + | he::tl -> + if List.mem he known_ids then filter tl else he::(filter tl) + in + filter dom + in + (* for each id in dom' we get the list of uris associated to it *) + let list_of_uris = + List.map + (function + CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id) + | CicTextualParser0.Symbol (descr,choices) -> + (* CSC: Implementare la funzione di filtraggio manuale *) + (* CSC: corrispondente alla locate_one_id *) + Symbols (List.map snd choices) + ) dom' in + let tests_no = + List.fold_left + (fun i uris -> + let len = + match uris with + Uris l -> List.length l + | Symbols l -> List.length l + in + i * len + ) 1 list_of_uris + in + if tests_no > 1 then + C.output_html (`Msg (`T (sprintf + "Disambiguation phase started: up to %d cases will be tried" + tests_no))); + (* and now we compute the list of all possible assignments from *) + (* id to uris that generate well-typed terms *) + let resolve_ids = + (* function to test if a partial interpretation is so far correct *) + let test resolve_id residual_dom = + (* We put implicits in place of every identifier that is not *) + (* resolved by resolve_id *) + let resolve_id' = + List.fold_left + (fun f id -> + function id' -> + if id = id' then Some (CicTextualParser0.Implicit) else f id' + ) resolve_id residual_dom + in + (* and we try to refine the term *) + let metasenv',expr = mk_metasenv_and_expr resolve_id' in +(*CSC: Bug here: we do not try to typecheck also the metasenv' *) + try + let term,_,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context expr + in + Ok (term,metasenv'') + with + CicRefine.MutCaseFixAndCofixRefineNotImplemented -> + (try + let term = CicTypeChecker.type_of_aux' metasenv' context expr in + Ok (term,metasenv') + with _ -> Ko + ) + | CicRefine.Uncertain _ -> +prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ; + Uncertain + | _ -> +prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; + Ko + in + let rec aux resolve_id ids list_of_uris = + match ids,list_of_uris with + [],[] -> + (match test resolve_id [] with + Ok (term,metasenv) -> [resolve_id,term,metasenv] + | Ko | Uncertain -> []) + | id::idtl,uris::uristl -> + let rec filter = + function + [] -> [] + | (uri : CicTextualParser0.interpretation_codomain_item)::uritl -> + let resolve_id' = + function id' -> if id = id' then Some uri else resolve_id id' + in + (match test resolve_id' idtl with + Ok (term,metasenv) -> + (* the next three ``if''s are used to avoid the base *) + (* case where the term would be refined a second time. *) + (if uristl = [] then + [resolve_id',term,metasenv] + else + (aux resolve_id' idtl uristl) + ) @ (filter uritl) + | Uncertain -> + (if uristl = [] then [] + else + (aux resolve_id' idtl uristl) + ) @ (filter uritl) + | Ko -> + filter uritl + ) + in + (match uris with + Uris uris -> + filter + (List.map (function uri -> CicTextualParser0.Uri uri) uris) + | Symbols symbols -> + filter + (List.map + (function sym -> CicTextualParser0.Term sym) symbols)) + | _,_ -> assert false + in + aux resolve_id dom' list_of_uris + in + List.iter + (function (resolve,term,newmetasenv) -> + (* If metasen <> newmetasenv is a normal condition, we should *) + (* be prepared to apply the returned substitution to the *) + (* whole current proof. *) + if metasenv <> newmetasenv then + begin + prerr_endline + (Printf.sprintf + "+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n" + (CicMetaSubst.ppmetasenv [] metasenv) + (CicMetaSubst.ppmetasenv [] newmetasenv)) ; + (* an assert would raise an exception that could be caught *) + exit 1 + end + ) resolve_ids ; + let resolve_id',term,metasenv' = + match resolve_ids with + [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput + | [resolve_id] -> resolve_id + | _ -> + let choices = + List.map + (function (resolve,_,_) -> + List.map + (function id -> + (match id with + CicTextualParser0.Id id -> id + | CicTextualParser0.Symbol (descr,_) -> descr + ), + match resolve id with + None -> assert false + | Some (CicTextualParser0.Uri uri) -> + (match uri with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri -> + UriManager.string_of_uri uri + | CicTextualParser0.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ ")" + | CicTextualParser0.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")") + | Some (CicTextualParser0.Term term) -> + (* CSC: Implementare resa delle scelte *) + "To be implemented XXX01" + | Some CicTextualParser0.Implicit -> assert false + ) dom + ) resolve_ids + in + let index = C.interactive_interpretation_choice choices in + List.nth resolve_ids index + in + (known_ids @ dom', resolve_id'), metasenv',term +end +;; diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli new file mode 100644 index 000000000..242b3102a --- /dev/null +++ b/helm/gTopLevel/oldDisambiguate.mli @@ -0,0 +1,67 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 15/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +(** This module provides a functor to disambiguate the input **) +(** given a set of user-interface call-backs **) + +module type Callbacks = + sig + val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit + val interactive_user_uri_choice : + selection_mode:[`SINGLE | `MULTIPLE] -> + ?ok:string -> + ?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 + val input_or_locate_uri : title:string -> UriManager.uri + end + +type domain_and_interpretation = + CicTextualParser0.interpretation_domain_item list * + CicTextualParser0.interpretation + +module Make (C : Callbacks) : + sig + exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput + val disambiguate_input : + MQIConn.handle -> + Cic.context -> + Cic.metasenv -> + CicTextualParser0.interpretation_domain_item list -> + (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) -> + id_to_uris:domain_and_interpretation -> + domain_and_interpretation * Cic.metasenv * Cic.term + end diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index f034c45b1..ca5cca601 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -35,8 +35,6 @@ open Printf -open Disambiguate_types - (* A WIDGET TO ENTER CIC TERMS *) class type term_editor = @@ -50,23 +48,21 @@ class type term_editor = method reset : unit (* The input of set_term is unquoted *) method set_term : string -> unit - method id_to_uris : environment ref + method environment : DisambiguatingParser.Environment.t ref end -let empty_id_to_uris = Environment.empty - -module Make(C: Callbacks) = +module Make(C:Disambiguate_types.Callbacks) = struct - module Disambiguate' = Disambiguate.Make(C);; + module Disambiguate' = DisambiguatingParser.Make(C);; class term_editor_impl mqi_handle ?packing ?width ?height - ?isnotempty_callback ?share_id_to_uris_with () : term_editor + ?isnotempty_callback ?share_environment_with () : term_editor = - let id_to_uris = - match share_id_to_uris_with with - None -> ref empty_id_to_uris - | Some obj -> obj#id_to_uris + let environment = + match share_environment_with with + None -> ref DisambiguatingParser.Environment.empty + | Some obj -> obj#environment in let input = GText.view ~editable:true ?width ?height ?packing () in let _ = @@ -100,17 +96,14 @@ module Make(C: Callbacks) = | None -> None ) context in - let term = - Parser.parse_term (Stream.of_string (input#buffer#get_text ())) - in - let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_term mqi_handle context metasenv term - ~aliases:!id_to_uris + let environment',metasenv,expr = + Disambiguate'.disambiguate_term mqi_handle context metasenv + (input#buffer#get_text ()) !environment in - id_to_uris := id_to_uris'; + environment := environment'; (metasenv, expr) - method id_to_uris = id_to_uris + method environment = environment end let term_editor = new term_editor_impl diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index e9c85f88c..e9e725ed2 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -33,12 +33,10 @@ class type term_editor = metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit method set_term : string -> unit - method id_to_uris : Disambiguate_types.environment ref + method environment : DisambiguatingParser.Environment.t ref end -val empty_id_to_uris : Disambiguate_types.environment - -module Make (C : Callbacks) : +module Make (C : Disambiguate_types.Callbacks) : sig val term_editor : MQIConn.handle -> @@ -46,6 +44,6 @@ module Make (C : Callbacks) : ?width:int -> ?height:int -> ?isnotempty_callback:(bool -> unit) -> - ?share_id_to_uris_with:term_editor -> + ?share_environment_with:term_editor -> unit -> term_editor end -- 2.39.2