+(* 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'
+;;
+