+let cic_textual_parser_uri_of_uri uri' =
+ (* 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)
+ )
+;;
+
+
+let term_of_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ match (cic_textual_parser_uri_of_uri uri) with
+ CTP.ConUri uri -> C.Const (uri,[])
+ | CTP.VarUri uri -> C.Var (uri,[])
+ | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
+ | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
+;;
+
+(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
+
+exception NoChoice;;
+
+let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris =
+ let choice = ref None in
+ let window = GWindow.dialog ~modal:true ~title () in
+ let lMessage =
+ GMisc.label ~text:msg ~packing:window#vbox#add () in
+ let vbox = GPack.vbox ~border_width:10
+ ~packing:(window#action_area#pack ~expand:true ~padding:4) () in
+ let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in
+ let combo =
+ GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in
+ let checkb =
+ GButton.button ~label:"Check"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let cancelb =
+ GButton.button ~label:cancel
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ let ok_callback () =
+ choice := Some combo#entry#text ;
+ window#destroy ()
+ in
+ let check_callback () = !check_term [] [] (term_of_uri combo#entry#text) in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore (okb#connect#clicked ok_callback) ;
+ ignore (checkb#connect#clicked check_callback) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GMain.Main.main () ;
+ match !choice with
+ None -> raise NoChoice
+ | Some uri -> uri
+;;
+
+(* MISC FUNCTIONS *)
+
+(* 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>"
+;;
+
+let register_alias (id,uri) =
+ let dom,resolve_id = !id_to_uris in
+ id_to_uris :=
+ (if List.mem id dom then dom else id::dom),
+ function id' -> if id' = id then Some uri else resolve_id id'
+;;
+
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
+ outputhtml#set_topline (-1)
+;;
+
+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
+ begin
+ match !rendering_window with
+ None -> assert false
+ | Some rw -> output_html rw#outputhtml html ;
+ end ;
+ let uris' =
+ match uris with
+ [] ->
+ (match
+ (GToolbox.input_string ~title:"Unknown input"
+ ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+ with
+ None -> raise NoChoice
+ | Some uri -> ["cic:" ^ uri]
+ )
+ | [uri] -> [uri]
+ | _ ->
+ try
+ [interactive_user_uri_choice
+ ~cancel:"Try every possibility."
+ ~title:"Ambiguous input."
+ ~msg:
+ ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one interpretation:")
+ uris
+ ]
+ with
+ NoChoice -> uris
+ in
+ List.map cic_textual_parser_uri_of_uri uris'
+;;
+
+exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
+exception AmbiguousInput;;
+
+let disambiguate_input context metasenv dom mk_metasenv_and_expr =
+ 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
+ (* and now we compute the list of all possible assignments from id to uris *)
+ let resolve_ids =
+ let rec aux ids list_of_uris =
+ match ids,list_of_uris with
+ [],[] -> [resolve_id]
+ | id::idtl,uris::uristl ->
+ let resolves = aux idtl uristl in
+ List.concat
+ (List.map
+ (function uri ->
+ List.map
+ (function f ->
+ function id' -> if id = id' then Some uri else f id'
+ ) resolves
+ ) uris
+ )
+ | _,_ -> assert false
+ in
+ aux dom' list_of_uris
+ in
+prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ;
+ (* now we select only the ones that generates well-typed terms *)
+ let resolve_ids' =
+ let rec filter =
+ function
+ [] -> []
+ | resolve::tl ->
+ let metasenv',expr = mk_metasenv_and_expr resolve in
+ try
+(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context expr) ;
+ resolve::(filter tl)
+ with
+ _ -> filter tl
+ in
+ filter resolve_ids
+ in
+ let resolve_id' =
+ match resolve_ids' with
+ [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ | [resolve_id] -> resolve_id
+ | _ ->
+ let choices =
+ List.map
+ (function resolve ->
+ String.concat " ; "
+ (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 choice =
+ GToolbox.question_box ~title:"Ambiguous input."
+ ~buttons:choices
+ ~default:1 "Ambiguous input. Please, choose one interpretation."
+ in
+ if choice > 0 then
+ List.nth resolve_ids' (choice - 1)
+ else
+ (* No choice from the user *)
+ raise NoChoice
+ in
+ id_to_uris := known_ids @ dom', resolve_id' ;
+ mk_metasenv_and_expr resolve_id'
+;;
+