module type Callbacks =
sig
- 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
+ (string * string) list list -> int list
+ val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri
end
;;
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
- C.output_html (`Msg (`T "Locate query:"));
+ HelmLogger.log (`Msg (`T "Locate query:"));
MQueryUtil.text_of_query
- (fun s -> C.output_html ~append_NL:false (`Msg (`T s)))
+ (fun s -> HelmLogger.log ~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;
+ HelmLogger.log (`Msg (`T "Result:"));
+ MQueryUtil.text_of_result (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
let uris' =
match uris with
[] ->
[UriManager.string_of_uri
(C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
| [uri] -> [uri]
| _ ->
C.interactive_user_uri_choice
) 1 list_of_uris
in
if tests_no > 1 then
- C.output_html (`Msg (`T (sprintf
+ HelmLogger.log (`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 *)
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,_,metasenv'' =
+ 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 _ ->
+ CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
Uncertain
- | _ ->
+ | CicRefine.RefineFailure _ ->
prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
Ko
in
prerr_endline
(Printf.sprintf
"+++++ ASSERTION FAILED: a refine operation should not modify the metasenv. Old metasenv:\n %s\n New metasenv:\n %s\n"
- (CicMetaSubst.ppmetasenv [] metasenv)
- (CicMetaSubst.ppmetasenv [] newmetasenv)) ;
+ (CicMetaSubst.ppmetasenv metasenv [])
+ (CicMetaSubst.ppmetasenv newmetasenv [])) ;
(* an assert would raise an exception that could be caught *)
exit 1
end
) resolve_ids ;
- let resolve_id',term,metasenv' =
+ let res =
match resolve_ids with
[] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
- | [resolve_id] -> resolve_id
+ | [_] -> resolve_ids
| _ ->
let choices =
List.map
) dom
) resolve_ids
in
- let index = C.interactive_interpretation_choice choices in
- List.nth resolve_ids index
+ let indexes = C.interactive_interpretation_choice choices in
+ List.map (List.nth resolve_ids) indexes
in
- (known_ids @ dom', resolve_id'), metasenv',term
+ List.map
+ (fun (resolve_id',term,metasenv') ->
+ (known_ids @ dom', resolve_id'), metasenv',term
+ ) res
end
;;