+(* 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 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(** Functions that should be moved in another module **)
+
+exception IllFormedUri of string;;
+
+let string_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ let uri' =
+ match uri with
+ CTP.ConUri uri -> UriManager.string_of_uri uri
+ | CTP.VarUri uri -> UriManager.string_of_uri uri
+ | CTP.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
+ | CTP.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
+ string_of_int consno
+ in
+ (* 4 = String.length "cic:" *)
+ String.sub uri' 4 (String.length uri' - 4)
+;;
+
+let cic_textual_parser_uri_of_string uri' =
+ prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
+ try
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+ CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+ else
+ if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+ CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+ CicTextualParser0.IndTyUri (uri'',typeno)
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
+ )
+ with
+ _ -> raise (IllFormedUri uri')
+;;
+let cic_textual_parser_uri_of_string uri' =
+ let res = cic_textual_parser_uri_of_string uri' in
+ prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
+ res
+
+(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
+let wrong_xpointer_format_from_wrong_xpointer_format' uri =
+ try
+ let index_sharp = String.index uri '#' in
+ let index_rest = index_sharp + 10 in
+ let baseuri = String.sub uri 0 index_sharp in
+ let rest =
+ String.sub uri index_rest (String.length uri - index_rest - 1)
+ in
+ baseuri ^ "#" ^ rest
+ with Not_found -> uri
+;;
+
+(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
+let get_last_query =
+ let query = ref "" in
+ MQueryGenerator.set_confirm_query
+ (function q -> query := MQueryUtil.text_of_query q ; true) ;
+ function result ->
+ !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+;;
+
+(** This module provides a functor to disambiguate the input **)
+(** given a set of user-interface call-backs **)
+
+module type Callbacks =
+ sig
+ 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 =
+ string list * (string -> CicTextualParser0.uri option)
+;;
+
+module Make(C:Callbacks) =
+ struct
+
+ let locate_one_id id =
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ ->
+ wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ let html=
+ " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
+ in
+ C.output_html html ;
+ 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 cic_textual_parser_uri_of_string uris'
+
+
+ exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+
+ type test_result =
+ Ok of Cic.term * Cic.metasenv
+ | Ko
+ | Uncertain
+
+ let disambiguate_input 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 locate_one_id dom' in
+ let tests_no =
+ List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+ in
+ if tests_no > 1 then
+ C.output_html
+ ("<h1>Disambiguation phase started: " ^
+ 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'' =
+ let resolve_id' =
+ function id ->
+ match resolve_id id with
+ None -> None
+ | Some uri -> Some (CicTextualParser0.Uri uri)
+ in
+ 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 = !CicTextualParser0.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 ;-(( *)
+ CicTextualParser0.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::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
+ filter uris
+ | _,_ -> 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 ->
+ id,
+ match resolve id with
+ None -> assert false
+ | Some 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 ^ ")"
+ ) 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
+;;