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
exception NoWellTypedInterpretation of
int *
((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- (Stdpp.location * string) Lazy.t * bool) list
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t *
+ bool) list
exception PathNotWellFormed
val interpretate_path :
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 *
exception Choice_not_found of string Lazy.t
(** register a new number choice *)
-val add_num_choice: codomain_item -> unit
+val add_num_choice: Cic.term codomain_item -> unit
(** {2 Choices lookup}
* for user defined aliases *)
-val lookup_num_choices: unit -> codomain_item list
+val lookup_num_choices: unit -> Cic.term codomain_item list
(** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> codomain_item
+val lookup_num_by_dsc: string -> Cic.term codomain_item
(** @param symbol symbol as per AST
* @param dsc description (1st component of codomain_item)
*)
-val lookup_symbol_by_dsc: string -> string -> codomain_item
+val lookup_symbol_by_dsc: string -> string -> Cic.term codomain_item
val mk_choice:
string * CicNotationPt.argument_pattern list *
CicNotationPt.cic_appl_pattern ->
- codomain_item
+ Cic.term codomain_item
end
-type codomain_item =
+type 'term codomain_item =
string * (* description *)
- (environment -> string -> Cic.term list -> Cic.term)
+ ('term environment -> string -> 'term list -> 'term)
(* environment, literal number, arguments as needed *)
-and environment = codomain_item Environment.t
+and 'term environment = 'term codomain_item Environment.t
-type multiple_environment = codomain_item list Environment.t
+type 'term multiple_environment = 'term codomain_item list Environment.t
(** adds a (name,uri) list l to a disambiguation environment e **)
* wrong number of Cic.term arguments received) *)
exception Invalid_choice of (Stdpp.location * string) Lazy.t
-type codomain_item =
+type 'term codomain_item =
string * (* description *)
- (environment -> string -> Cic.term list -> Cic.term)
+ ('term environment -> string -> 'term list -> 'term)
(* environment, literal number, arguments as needed *)
-and environment = codomain_item Environment.t
+and 'term environment = 'term codomain_item Environment.t
-type multiple_environment = codomain_item list Environment.t
+type 'term multiple_environment = 'term codomain_item list Environment.t
(* a simple case of extension of a disambiguation environment *)
val env_of_list:
- (string * string * Cic.term) list -> environment -> environment
+ (string * string * 'term) list -> 'term environment -> 'term environment
val multiple_env_of_list:
- (string * string * Cic.term) list -> multiple_environment ->
- multiple_environment
+ (string * string * 'term) list -> 'term multiple_environment ->
+ 'term multiple_environment
module type Callbacks =
sig
val parse_environment:
include_paths:string list ->
string ->
- DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
+ Cic.term DisambiguateTypes.environment *
+ Cic.term DisambiguateTypes.multiple_environment
(** @param fname file from which load notation *)
val load_notation: include_paths:string list -> string -> LexiconEngine.status
in
HLog.debug debug; assert false
+
+let lookup_in_library interactive_user_uri_choice input_or_locate_uri item =
+ let dbd = LibraryDb.instance () in
+ let choices_of_id id =
+ let uris = Whelp.locate ~dbd id in
+ let uris =
+ match uris with
+ | [] ->
+ (match
+ (input_or_locate_uri
+ ~title:("URI matching \"" ^ id ^ "\" unknown.")
+ ?id:(Some id) ())
+ with
+ | None -> []
+ | Some uri -> [uri])
+ | [uri] -> [uri]
+ | _ ->
+ interactive_user_uri_choice ~selection_mode:`MULTIPLE
+ ?ok:(Some "Try selected.")
+ ?enable_button_for_non_vars:(Some true)
+ ~title:"Ambiguous input."
+ ~msg: ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one or more interpretations:")
+ ~id
+ uris
+ in
+ List.map
+ (fun uri ->
+ (UriManager.string_of_uri uri,
+ let term =
+ try
+ CicUtil.term_of_uri uri
+ with exn ->
+ assert false
+ in
+ fun _ _ _ -> term))
+ uris
+ in
+ match item with
+ | DisambiguateTypes.Id id -> choices_of_id id
+ | DisambiguateTypes.Symbol (symb, _) ->
+ (try
+ List.map DisambiguateChoices.mk_choice
+ (TermAcicContent.lookup_interpretations symb)
+ with
+ TermAcicContent.Interpretation_not_found -> [])
+ | DisambiguateTypes.Num instance ->
+ DisambiguateChoices.lookup_num_choices ()
+;;
+
(** @param term not meaningful when context is given *)
let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
term =
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, subst, cic, _) =
singleton "first"
- (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ (GrafiteDisambiguator.disambiguate_term
~aliases:lexicon_status.LexiconEngine.aliases
?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~lookup_in_library
~context ~metasenv ~subst:[] (text,prefix_len,term))
in
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, _, cic, ugraph) =
singleton "second"
- (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ (GrafiteDisambiguator.disambiguate_term ~lookup_in_library
~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
~context ~metasenv ~subst:[] ?goal
| CicNotationPt.Theorem _ -> None in
let (diff, metasenv, _, cic, _) =
singleton "third"
- (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+ (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
(text,prefix_len,obj)) in
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 *)
exception Unbound_identifier of string
let disambiguate_thing ~aliases ~universe
~(f:?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'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 ->
+ 'a 'b 'term.
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'term DisambiguateTypes.multiple_environment option ->
f:(?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:'term DisambiguateTypes.environment ->
+ universe:'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
(List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
user_asked
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
- ~aliases ~universe term
+let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
=
assert (fresh_instances = None);
let f =
- Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+ Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
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 ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj =
assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
~drop_aliases_and_clear_diff obj
-let disambiguate_thing ~dbd = assert false
+let disambiguate_thing ~context = assert false
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 *)
*)
val aliases_of_domain_and_codomain_items_list:
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+ (DisambiguateTypes.domain_item *
+ Cic.term DisambiguateTypes.codomain_item) list ->
LexiconAst.alias_spec list
-val pp_environment: DisambiguateTypes.environment -> string
+val pp_environment: Cic.term DisambiguateTypes.environment -> string
exception MetadataNotFound of string (* file name *)
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: DisambiguateTypes.multiple_environment;
+ aliases: Cic.term DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: Cic.term DisambiguateTypes.multiple_environment;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
exception IncludedFileNotCompiled of string * string
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: DisambiguateTypes.multiple_environment;
+ aliases: Cic.term DisambiguateTypes.environment;(** disambiguation aliases *)
+ multi_aliases: Cic.term DisambiguateTypes.multiple_environment;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
val set_proof_aliases:
status ->
- (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list ->
+ (DisambiguateTypes.Environment.key *
+ Cic.term DisambiguateTypes.codomain_item) list ->
status
(* this callback is called on every lexicon command *)
* order to be equal to aliases of the second argument *)
val alias_diff:
from:LexiconEngine.status -> LexiconEngine.status ->
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
+ (DisambiguateTypes.domain_item *
+ Cic.term DisambiguateTypes.codomain_item) list
val push: unit -> unit
val pop: unit -> unit
nDisambiguate.cmo: nDisambiguate.cmi
nDisambiguate.cmx: nDisambiguate.cmi
+nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi
+nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi
--- /dev/null
+nDisambiguate.cmo: nDisambiguate.cmi
+nDisambiguate.cmx: nDisambiguate.cmi
+nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi
+nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi
PREDICATES =
INTERFACE_FILES = \
- nDisambiguate.mli\
+ nDisambiguate.mli nGrafiteDisambiguator.mli\
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
-(* $Id: disambiguate.ml 9178 2008-11-12 12:09:52Z tassi $ *)
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
open Printf
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
module Make (C : DisambiguateTypes.Callbacks) : sig
val disambiguate_term :
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+exception Ambiguous_input
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) 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 = false;;
+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
+
+ let interactive_interpretation_choice interp =
+ !_choose_interp_callback interp
+
+ 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 *)
+ end
+
+module Disambiguator = NDisambiguate.Make (Callbacks)
+
+let only_one_pass = ref false;;
+
+let disambiguate_thing ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b)
+ ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
+ ~(drop_aliases_and_clear_diff: 'b -> 'b)
+ (thing: 'a)
+=
+ assert (universe <> None);
+ let library = false, DisambiguateTypes.Environment.empty, None in
+ let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+ let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+ let passes = (* <fresh_instances?, aliases, coercions?> *)
+ if !only_one_pass then
+ [ (true, mono_aliases, false) ]
+ else
+ [ (true, mono_aliases, false);
+ (true, multi_aliases, false);
+ (true, mono_aliases, true);
+ (true, multi_aliases, true);
+ (true, library, false);
+ (* for demo to reduce the number of interpretations *)
+ (true, library, true);
+ ]
+ in
+ let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
+ CicRefine.insert_coercions := insert_coercions;
+ f ~fresh_instances ~aliases ~universe thing
+ in
+ let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+ if use_mono_aliases then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else if user_asked then
+ drop_aliases ~minimize_instances:true res (* one shot aliases *)
+ else
+ drop_aliases_and_clear_diff res
+ in
+ let rec aux i errors passes =
+ debug_print (lazy ("Pass: " ^ string_of_int i));
+ match passes with
+ [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
+ | hd :: tl ->
+ (try
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
+ aux (i+1) (errors @ [newerrors]) tl)
+ | [] -> assert false
+ in
+ let saved_insert_coercions = !CicRefine.insert_coercions in
+ try
+ let res = aux 1 [] passes in
+ CicRefine.insert_coercions := saved_insert_coercions;
+ res
+ with exn ->
+ CicRefine.insert_coercions := saved_insert_coercions;
+ raise exn
+
+type disambiguator_thing =
+ { do_it :
+ 'a 'b.
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ f:(?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe: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
+ }
+
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+ { do_it =
+ fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+ -> profiler.HExtlib.profile
+ (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff) thing
+ }
+
+let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
+ let module D = DisambiguateTypes in
+ let minimize d =
+ if not minimize_instances then
+ d
+ else
+ let rec aux =
+ function
+ [] -> []
+ | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function
+ (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
+ | _ -> true
+ ) d
+ then
+ (D.Symbol (s,0),ci)::(aux tl)
+ else
+ he::(aux tl)
+ | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
+ if
+ List.for_all
+ (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
+ then
+ (D.Num 0,ci)::(aux tl)
+ else
+ he::(aux tl)
+ | he::tl -> he::(aux tl)
+ in
+ aux d
+ in
+ (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+ user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+ (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+ user_asked
+
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+ ~aliases ~universe term
+ =
+ assert (fresh_instances = None);
+ let f =
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+ 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 =
+ assert (fresh_instances = None);
+ let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff obj
+
+let disambiguate_thing ~dbd = assert false
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id$ *)
+
+exception Ambiguous_input
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ (Stdpp.location * string) Lazy.t * bool) list list
+ (** parameters are: option name, error message *)
+type choose_uris_callback =
+ id:string -> UriManager.uri list -> UriManager.uri list
+type choose_interp_callback =
+ string -> int -> (Stdpp.location list * string * string) list list ->
+ int list
+
+val set_choose_uris_callback: choose_uris_callback -> unit
+val set_choose_interp_callback: choose_interp_callback -> unit
+
+val disambiguate_term :
+ ?fresh_instances:bool ->
+ dbd:HSql.dbd ->
+ context:NCic.context ->
+ metasenv:NCic.metasenv ->
+ subst:NCic.substitution ->
+ aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:DisambiguateTypes.multiple_environment option ->
+ ?goal: int ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+ ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ NCic.metasenv * (* new metasenv *)
+ NCic.substitution *
+ NCic.term) list * (* disambiguated term *)
+ bool
+
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement) ->
((GrafiteTypes.status * LexiconEngine.status) *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
+ (DisambiguateTypes.domain_item *
+ Cic.term DisambiguateTypes.codomain_item) option
) list
CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string)
GrafiteAst.statement -> unit) ->
((GrafiteTypes.status * LexiconEngine.status) *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
+ (DisambiguateTypes.domain_item *
+ Cic.term DisambiguateTypes.codomain_item) option
) list
(* this callback is called on every grafite command *)
val compact_disambiguation_errors :
bool ->
(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 ->
(Stdpp.location *
(int list *
(int list * (Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list *
+ (DisambiguateTypes.domain_item * string) list) list *
string Lazy.t * bool) list) list
val to_string: exn -> Stdpp.location option * string
String.concat "\n"
("" ::
List.map
- (fun k,value ->
+ (fun k,value ->
DisambiguatePp.pp_environment
- (DisambiguateTypes.Environment.add k value
+ (DisambiguateTypes.Environment.add k
+ (value,(fun _ _ _ -> Cic.Implicit None))
DisambiguateTypes.Environment.empty))
diff) ^ "\n"
in
projects / helm.git / commitdiff