--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** 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 : string -> unit
+ val interactive_user_uri_choice :
+ selection_mode:[`SINGLE | `EXTENDED] ->
+ ?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 "<h1>Locate Query: </h1><pre>";
+ MQueryUtil.text_of_query C.output_html query "";
+ C.output_html "<h1>Result:</h1>";
+ MQueryUtil.text_of_result C.output_html result "<br>";
+ 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:`EXTENDED
+ ~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
+ ("<h1>Disambiguation phase started: up to " ^
+ string_of_int tests_no ^ " cases will be tried.") ;
+ (* 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
+;;
projects / helm.git / blobdiff