in
match ast with
| CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux (-1, -1) context term
+ | term -> aux CicAst.dummy_floc context term
let domain_of_term ~context ast =
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
rev_uniq
(match ast with
| CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux (-1, -1) context term)
-
+ | term -> aux CicAst.dummy_floc context term)
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
module Make (C: Callbacks) =
struct
- let choices_of_id mqi_handle id =
- let query = MQueryGenerator.locate id in
- let result = MQueryInterpreter.execute mqi_handle query in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let uris' =
+ let choices_of_id dbh id =
+ let uris = MetadataQuery.locate ~dbh id in
+ let uris =
match uris with
| [] ->
[UriManager.string_of_uri (C.input_or_locate_uri
(uri,
let term =
try
- HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
- with _ -> assert false
+ CicUtil.term_of_uri uri
+ with exn ->
+ prerr_endline uri;
+ prerr_endline (Printexc.to_string exn);
+ assert false
in
fun _ _ _ -> term))
- uris'
+ uris
- let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
+ let disambiguate_term ~(dbh:Dbi.connection) context metasenv term
+ ~aliases:current_env
=
debug_print "NEW DISAMBIGUATE INPUT";
let disambiguate_context = (* cic context -> disambiguate context *)
(try
Hashtbl.find id_choices id
with Not_found ->
- let choices = choices_of_id mqi_handle id in
+ let choices = choices_of_id dbh id in
Hashtbl.add id_choices id choices;
choices)
| Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb