exception NoWellTypedInterpretation of
int *
((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ (DisambiguateTypes.domain_item * string) list *
(Stdpp.location * string) Lazy.t * bool) list
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
exception Try_again of string Lazy.t
-type aliases = bool * DisambiguateTypes.environment
+type 'term aliases = bool * 'term DisambiguateTypes.environment
type 'a disambiguator_input = string * int * 'a
type domain = domain_tree list
in
process_exn Stdpp.dummy_loc exn
-let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
+let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
snd (Environment.find item env) env num args
with Not_found ->
module type Disambiguator =
sig
val disambiguate_thing:
- dbd:HSql.dbd ->
context:'context ->
metasenv:'metasenv ->
subst:'subst ->
+ mk_implicit:([ `Closed ] option -> 'refined_thing) ->
initial_ugraph:'ugraph ->
hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
(('refined_thing,'metasenv,'subst,'ugraph) test_result ->
('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
- universe:DisambiguateTypes.codomain_item list
+ aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+ universe:'refined_thing DisambiguateTypes.codomain_item list
DisambiguateTypes.Environment.t option ->
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ 'refined_thing DisambiguateTypes.codomain_item list) ->
uri:'uri ->
pp_thing:('ast_thing -> string) ->
domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
interpretate_thing:(context:'context ->
- env:DisambiguateTypes.codomain_item
+ env:'refined_thing DisambiguateTypes.codomain_item
DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
localization_tbl:'cichash ->
string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
- list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
+ ((DisambiguateTypes.Environment.key *
+ 'refined_thing DisambiguateTypes.codomain_item) list *
+ 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HSql.dbd ->
context:Cic.context ->
metasenv:Cic.metasenv ->
subst:Cic.substitution ->
?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.term DisambiguateTypes.multiple_environment option ->
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
CicNotationPt.term disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.substitution *
Cic.term*
val disambiguate_obj :
?fresh_instances:bool ->
- dbd:HSql.dbd ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.term DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
CicNotationPt.term CicNotationPt.obj disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.substitution *
Cic.obj *
module Make (C: Callbacks) =
struct
- let choices_of_id dbd id =
- let uris = Whelp.locate ~dbd id in
- let uris =
- match uris with
- | [] ->
- (match
- (C.input_or_locate_uri
- ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
- with
- | None -> []
- | Some uri -> [uri])
- | [uri] -> [uri]
- | _ ->
- C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
- ~ok:"Try selected." ~enable_button_for_non_vars:true
- ~title:"Ambiguous input." ~id
- ~msg: ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- uris
- in
- List.map
- (fun uri ->
- (UriManager.string_of_uri uri,
- let term =
- try
- CicUtil.term_of_uri uri
- with exn ->
- debug_print (lazy (UriManager.string_of_uri uri));
- debug_print (lazy (Printexc.to_string exn));
- assert false
- in
- fun _ _ _ -> term))
- uris
-
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
- let disambiguate_thing ~dbd ~context ~metasenv ~subst
+ let disambiguate_thing
+ ~context ~metasenv ~subst ~mk_implicit
~initial_ugraph:base_univ ~hint
- ~aliases ~universe
+ ~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~localization_tbl
(thing_txt,thing_txt_prefix_len,thing)
let lookup_choices =
fun item ->
let choices =
- let lookup_in_library () =
- match item with
- | Id id -> choices_of_id dbd id
- | Symbol (symb, _) ->
- (try
- List.map DisambiguateChoices.mk_choice
- (TermAcicContent.lookup_interpretations symb)
- with
- TermAcicContent.Interpretation_not_found -> [])
- | Num instance ->
- DisambiguateChoices.lookup_num_choices ()
- in
match universe with
- | None -> lookup_in_library ()
+ | None ->
+ lookup_in_library
+ C.interactive_user_uri_choice
+ C.input_or_locate_uri item
| Some e ->
(try
let item =
| item -> item
in
Environment.find item e
- with Not_found -> lookup_in_library ())
+ with Not_found ->
+ lookup_in_library
+ C.interactive_user_uri_choice
+ C.input_or_locate_uri item)
in
choices
in
("Implicit",
(match item with
| Id _ | Num _ ->
- (fun _ _ _ -> Cic.Implicit (Some `Closed))
- | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
+ (fun _ _ _ -> mk_implicit (Some `Closed))
+ | Symbol _ -> (fun _ _ _ -> mk_implicit None)))
env in
aux (aux env l) tl in
let filled_env = aux aliases todo_dom in
Not_found -> None)
thing_dom
in
+ let diff= List.map (fun a,b -> a,fst b) diff in
env',diff,loc_msg,significant
) errors
in
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"
- let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
+ let disambiguate_term ?(fresh_instances=false) ~context ~metasenv
~subst ?goal
?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
+ ~lookup_in_library
(text,prefix_len,term)
=
let term =
if fresh_instances then CicNotationUtil.freshen_term term else term
in
+ let mk_implicit x = Cic.Implicit x in
let hint = match goal with
| None -> (fun _ x -> x), fun k -> k
| Some i ->
| k -> k
in
let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~dbd ~context ~metasenv ~subst
- ~initial_ugraph ~aliases
- ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
+ disambiguate_thing ~context ~metasenv ~subst
+ ~initial_ugraph ~aliases ~mk_implicit
+ ~universe ~lookup_in_library
+ ~uri:None ~pp_thing:CicNotationPp.pp_term
~domain_of_thing:domain_of_term
~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
~refine_thing:refine_term (text,prefix_len,term)
~localization_tbl
~hint
- let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
- (text,prefix_len,obj)
+ let disambiguate_obj
+ ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library
+ (text,prefix_len,obj)
=
+ let mk_implicit x = Cic.Implicit x in
let obj =
if fresh_instances then CicNotationUtil.freshen_obj obj else obj
in
fun k -> k
in
let localization_tbl = Cic.CicHash.create 503 in
- disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[]
- ~aliases ~universe ~uri
- ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
+ disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
+ ~aliases ~universe ~uri ~mk_implicit
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~domain_of_thing:domain_of_obj
+ ~lookup_in_library
~initial_ugraph:CicUniv.empty_ugraph
~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
~localization_tbl
projects / helm.git / blobdiff