(* *)
(******************************************************************************)
-(** Functions that should be moved in another module **)
-
-exception IllFormedUri of string;;
-
-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)
-;;
-
-let cic_textual_parser_uri_of_string uri' =
- prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
- try
- (* 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)
- )
- with
- _ -> raise (IllFormedUri uri')
-;;
-let cic_textual_parser_uri_of_string uri' =
- let res = cic_textual_parser_uri_of_string uri' in
- prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
- res
-
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
- let index_sharp = String.index uri '#' in
- let index_rest = index_sharp + 10 in
- let baseuri = String.sub uri 0 index_sharp in
- let rest =
- String.sub uri index_rest (String.length uri - index_rest - 1)
- in
- baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
-(* 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>"
-;;
-
(** This module provides a functor to disambiguate the input **)
(** given a set of user-interface call-backs **)
module type Callbacks =
sig
+ (* The following two functions are used to save/restore the metasenv *)
+ (* before/after the parsing. *)
+ (*CSC: This should be made functional sooner or later! *)
+ val get_metasenv : unit -> Cic.metasenv
+ val set_metasenv : Cic.metasenv -> unit
+
val output_html : string -> unit
val interactive_user_uri_choice :
selection_mode:[`SINGLE | `EXTENDED] ->
;;
type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+ CicTextualParser0.interpretation
;;
module Make(C:Callbacks) =
struct
- let locate_one_id id =
- let result = MQueryGenerator.locate id in
+ let locate_one_id mqi_handle id =
+ let query = MQueryGenerator.locate id in
+ let result = MQueryInterpreter.execute mqi_handle query in
let uris =
List.map
(function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
+ MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
- let html=
- " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
- in
- C.output_html html ;
+ C.output_html "<h1>Locate Query: </h1><pre>";
+ MQueryUtil.text_of_query C.output_html query "";
+ C.output_html "<h1>Result:</h1>";
+ MQueryUtil.text_of_result C.output_html result "<br>";
let uris' =
match uris with
[] ->
~id
uris
in
- List.map cic_textual_parser_uri_of_string uris'
+ List.map MQueryMisc.cic_textual_parser_uri_of_string uris'
exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
| Ko
| Uncertain
- let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris=
+ type ambiguous_choices =
+ Uris of CicTextualParser0.uri list
+ | Symbols of (CicTextualParser0.interpretation -> Cic.term) list
+
+ let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris=
let known_ids,resolve_id = id_to_uris in
let dom' =
let rec filter =
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
+ let list_of_uris =
+ List.map
+ (function
+ CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id)
+ | CicTextualParser0.Symbol (descr,choices) ->
+ (* CSC: Implementare la funzione di filtraggio manuale *)
+ (* CSC: corrispondente alla locate_one_id *)
+ Symbols (List.map snd choices)
+ ) dom' in
let tests_no =
- List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
+ List.fold_left
+ (fun i uris ->
+ let len =
+ match uris with
+ Uris l -> List.length l
+ | Symbols l -> List.length l
+ in
+ i * len
+ ) 1 list_of_uris
in
if tests_no > 1 then
C.output_html
- ("<h1>Disambiguation phase started: " ^
+ ("<h1>Disambiguation phase started: up to " ^
string_of_int tests_no ^ " cases will be tried.") ;
(* and now we compute the list of all possible assignments from *)
(* id to uris that generate well-typed terms *)
let test resolve_id residual_dom =
(* We put implicits in place of every identifier that is not *)
(* resolved by resolve_id *)
- let resolve_id'' =
- let resolve_id' =
- function id ->
- match resolve_id id with
- None -> None
- | Some uri -> Some (CicTextualParser0.Uri uri)
- in
- List.fold_left
- (fun f id ->
- function id' ->
- if id = id' then Some (CicTextualParser0.Implicit) else f id'
- ) resolve_id' residual_dom
+ let resolve_id' =
+ List.fold_left
+ (fun f id ->
+ function id' ->
+ if id = id' then Some (CicTextualParser0.Implicit) else f id'
+ ) resolve_id residual_dom
in
(* and we try to refine the term *)
- let saved_status = !CicTextualParser0.metasenv in
- let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
+ let saved_status = C.get_metasenv () in
+ let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
(* The parser is imperative ==> we must restore the old status ;-(( *)
- CicTextualParser0.metasenv := saved_status ;
+ C.set_metasenv saved_status ;
try
let term,_,_,metasenv'' =
CicRefine.type_of_aux' metasenv' context expr
let rec filter =
function
[] -> []
- | uri::uritl ->
+ | (uri : CicTextualParser0.interpretation_codomain_item)::uritl ->
let resolve_id' =
function id' -> if id = id' then Some uri else resolve_id id'
in
filter uritl
)
in
- filter uris
+ (match uris with
+ Uris uris ->
+ filter
+ (List.map (function uri -> CicTextualParser0.Uri uri) uris)
+ | Symbols symbols ->
+ filter
+ (List.map
+ (function sym -> CicTextualParser0.Term sym) symbols))
| _,_ -> assert false
in
aux resolve_id dom' list_of_uris
(function (resolve,_,_) ->
List.map
(function id ->
- id,
+ (match id with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) -> descr
+ ),
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 ^ ")"
+ | Some (CicTextualParser0.Uri 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 ^ ")")
+ | Some (CicTextualParser0.Term term) ->
+ (* CSC: Implementare resa delle scelte *)
+ "To be implemented XXX01"
+ | Some CicTextualParser0.Implicit -> assert false
) dom
) resolve_ids
in
projects / helm.git / blobdiff