From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 16:19:22 +0000 (+0000) Subject: moved disambiguate module away X-Git-Tag: V_0_5_1_4~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d9de12a536ee4b9e369849ff7e9aa4ca464de9d;p=helm.git moved disambiguate module away --- diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml deleted file mode 100644 index 07a036839..000000000 --- a/helm/gTopLevel/disambiguate.ml +++ /dev/null @@ -1,288 +0,0 @@ -(* 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 - (* The following two functions are used to save/restore the metasenv *) - (* before/after the parsing. *) - (*CSC: This should be made functional sooner or later! *) - val get_metasenv : unit -> Cic.metasenv - val set_metasenv : Cic.metasenv -> unit - - 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 saved_status = C.get_metasenv () in - let metasenv',expr = mk_metasenv_and_expr resolve_id' in -(*CSC: Bug here: we do not try to typecheck also the metasenv' *) - (* The parser is imperative ==> we must restore the old status ;-(( *) - C.set_metasenv saved_status ; - 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 - ("+++++ ASSERTION FAILED: " ^ - "a refine operation should not modify the metasenv") ; - (* 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/disambiguate.mli b/helm/gTopLevel/disambiguate.mli deleted file mode 100644 index 79e77df48..000000000 --- a/helm/gTopLevel/disambiguate.mli +++ /dev/null @@ -1,73 +0,0 @@ -(* 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 - (* The following two functions are used to save/restore the metasenv *) - (* before/after the parsing. *) - (*CSC: This should be made functional sooner or later! *) - val get_metasenv : unit -> Cic.metasenv - val set_metasenv : Cic.metasenv -> unit - - 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