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'' =
- CicRefine.type_of_aux' metasenv' context expr
+ let term,_,metasenv'',_ = (* TASSI: FIXME what are we doning here?*)
+ CicRefine.type_of_aux' metasenv' context expr CicUniv.empty_ugraph
in
- Ok (term,metasenv'')
+ Ok (term,metasenv'') (* TASSI: whould we pass back the ugraph? *)
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
;;
+
+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
projects / helm.git / blobdiff