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 ->
(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
[] ->
) 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
| _ ->
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
(known_ids @ dom', resolve_id'), metasenv',term
end
;;
+
+module EnvironmentP3 =
+ struct
+ type t = domain_and_interpretation
+
+ let empty = ""
+
+ let to_string (dom,resolve_id) =
+ 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)
+ in
+ String.concat "\n"
+ (List.map
+ (function v ->
+ let uri =
+ match resolve_id v with
+ None -> assert false
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
+ in
+ "alias " ^
+ (match v with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) ->
+ (* CSC: To be implemented *)
+ assert false
+ )^ " " ^ (string_of_cic_textual_parser_uri uri)
+ ) dom)
+
+ let of_string inputtext =
+ let regexpr =
+ let alfa = "[a-zA-Z_-]" in
+ let digit = "[0-9]" in
+ let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
+ let blanks = "\( \|\t\|\n\)+" in
+ let nonblanks = "[^ \t\n]+" in
+ let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
+ Str.regexp
+ ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
+ in
+ let rec aux n =
+ try
+ let n' = Str.search_forward regexpr inputtext n in
+ let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
+ let uri =
+ MQueryMisc.cic_textual_parser_uri_of_string
+ ("cic:" ^ (Str.matched_group 5 inputtext))
+ in
+ let dom,resolve_id = aux (n' + 1) in
+ if List.mem id dom then
+ dom,resolve_id
+ else
+ id::dom,
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
+ with
+ Not_found -> ([],function _ -> None)
+ in
+ aux 0
+ end