(* $Id$ *)
-exception Ambiguous_input
exception DisambiguationError 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 list
- (** parameters are: option name, error message *)
-type choose_uris_callback = id:string -> NUri.uri list -> NUri.uri list
-type choose_interp_callback =
- string -> int -> (Stdpp.location list * string * string) list list ->
- int list
open Printf
let debug_print s =
if debug then prerr_endline (Lazy.force s);;
-let mono_uris_callback ~id =
- if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
- "matita.auto_disambiguation"
- then function l -> l
- else raise Ambiguous_input
-
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
module Callbacks =
struct
let interactive_user_uri_choice ~selection_mode ?ok
?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- !_choose_uris_callback ~id uris
+ assert false
let interactive_interpretation_choice interp =
- !_choose_interp_callback interp
+ assert false
- let input_or_locate_uri ~(title:string) ?id () = None
- (* Zack: I try to avoid using this callback. I therefore assume that
- * the presence of an identifier that can't be resolved via "locate"
- * query is a syntax error *)
+ let input_or_locate_uri ~(title:string) ?id () =
+ assert false
end
module Disambiguator = NDisambiguate.Make (Callbacks)
let disambiguate_thing ~aliases ~universe
~(f:?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:NCic.term DisambiguateTypes.environment ->
+ universe:NCic.term DisambiguateTypes.multiple_environment option ->
'a -> 'b)
~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
~(drop_aliases_and_clear_diff: 'b -> 'b)
type disambiguator_thing =
{ do_it :
'a 'b.
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:NCic.term DisambiguateTypes.environment ->
+ universe:NCic.term DisambiguateTypes.multiple_environment option ->
f:(?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:NCic.term DisambiguateTypes.environment ->
+ universe:NCic.term DisambiguateTypes.multiple_environment option ->
'a -> 'b * bool) ->
drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
in
aux d
in
- (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+ (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
user_asked
let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+ (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
user_asked
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+let disambiguate_term ~context ~metasenv ~subst ?goal
~aliases ~universe term
=
- assert (fresh_instances = None);
let f =
- Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+ Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal
+ ~lookup_in_library:(fun _ _ -> assert false)
in
disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff term
-let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+let disambiguate_obj ~aliases ~universe ~uri obj =
+ assert false (*
assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in
disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff obj
-
-let disambiguate_thing ~dbd = assert false
+ *)