From 1d212933a86f2820a151555516f7a53ab1c9f8e7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 26 Nov 2008 16:11:47 +0000 Subject: [PATCH] disambiguation even more abstracted --- .../cic_disambiguation/disambiguate.ml | 156 +++++++------- .../cic_disambiguation/disambiguate.mli | 64 ++++-- .../disambiguateChoices.mli | 10 +- .../cic_disambiguation/disambiguateTypes.ml | 8 +- .../cic_disambiguation/disambiguateTypes.mli | 14 +- .../grafite_parser/cicNotation2.mli | 3 +- .../grafite_parser/grafiteDisambiguate.ml | 57 ++++- .../grafite_parser/grafiteDisambiguator.ml | 27 ++- .../grafite_parser/grafiteDisambiguator.mli | 2 +- .../components/lexicon/disambiguatePp.mli | 5 +- .../components/lexicon/lexiconEngine.ml | 4 +- .../components/lexicon/lexiconEngine.mli | 7 +- .../components/lexicon/lexiconSync.mli | 3 +- .../components/ng_disambiguation/.depend | 2 + .../components/ng_disambiguation/.depend.opt | 4 + .../components/ng_disambiguation/Makefile | 2 +- .../ng_disambiguation/nDisambiguate.ml | 36 +--- .../ng_disambiguation/nDisambiguate.mli | 11 + .../nGrafiteDisambiguator.ml | 203 ++++++++++++++++++ .../nGrafiteDisambiguator.mli | 45 ++++ helm/software/matita/matitaEngine.mli | 6 +- helm/software/matita/matitaExcPp.mli | 4 +- helm/software/matita/matitaGui.ml | 5 +- 23 files changed, 507 insertions(+), 171 deletions(-) create mode 100644 helm/software/components/ng_disambiguation/.depend.opt create mode 100644 helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml create mode 100644 helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 47e9c1821..655747365 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -36,14 +36,14 @@ module Ast = CicNotationPt 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 @@ -159,7 +159,7 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = 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 -> @@ -932,22 +932,32 @@ let domain_diff dom1 dom2 = 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) -> @@ -960,22 +970,32 @@ sig ('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* @@ -984,12 +1004,21 @@ sig 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 * @@ -999,45 +1028,12 @@ end 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) @@ -1062,20 +1058,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_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 = @@ -1084,7 +1071,10 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | 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 @@ -1124,8 +1114,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" ("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 @@ -1302,6 +1292,7 @@ in refine_profiler.HExtlib.profile foo () 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 @@ -1337,14 +1328,16 @@ in refine_profiler.HExtlib.profile foo () 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 -> @@ -1360,18 +1353,21 @@ in refine_profiler.HExtlib.profile foo () | 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 @@ -1380,9 +1376,11 @@ in refine_profiler.HExtlib.profile foo () 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 diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index bb4c72640..201bdb3b7 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -36,8 +36,9 @@ 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 : @@ -61,22 +62,32 @@ val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain 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) -> @@ -89,22 +100,32 @@ sig ('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* @@ -113,12 +134,21 @@ sig 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 * diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.mli b/helm/software/components/cic_disambiguation/disambiguateChoices.mli index 0ad498106..a229a772f 100644 --- a/helm/software/components/cic_disambiguation/disambiguateChoices.mli +++ b/helm/software/components/cic_disambiguation/disambiguateChoices.mli @@ -31,23 +31,23 @@ open DisambiguateTypes 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 diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml index e9927c7b6..dae0542b9 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml @@ -85,14 +85,14 @@ struct 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 **) diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli index d9cedf5f0..c33013ee6 100644 --- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli +++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli @@ -43,22 +43,22 @@ end * 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 diff --git a/helm/software/components/grafite_parser/cicNotation2.mli b/helm/software/components/grafite_parser/cicNotation2.mli index 00f184b3b..972c55b51 100644 --- a/helm/software/components/grafite_parser/cicNotation2.mli +++ b/helm/software/components/grafite_parser/cicNotation2.mli @@ -29,7 +29,8 @@ 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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index ad7f70ef1..4d7655f6d 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -45,15 +45,66 @@ let singleton msg = function 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 @@ -71,7 +122,7 @@ let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term = 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 @@ -458,7 +509,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = | 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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index 5d803e979..4b647c780 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -36,7 +36,7 @@ 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 *) exception Unbound_identifier of string @@ -86,8 +86,8 @@ let only_one_pass = ref false;; 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) @@ -148,12 +148,12 @@ let disambiguate_thing ~aliases ~universe 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 @@ -207,20 +207,19 @@ 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 +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 diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli index d6ff0be4c..1d97b1b6b 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli @@ -30,7 +30,7 @@ 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 *) diff --git a/helm/software/components/lexicon/disambiguatePp.mli b/helm/software/components/lexicon/disambiguatePp.mli index e8d9b94a4..e85a28443 100644 --- a/helm/software/components/lexicon/disambiguatePp.mli +++ b/helm/software/components/lexicon/disambiguatePp.mli @@ -24,7 +24,8 @@ *) 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 diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 8a51e9523..f48ffe400 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -34,8 +34,8 @@ exception IncludedFileNotCompiled of string * 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 *) } diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index b69495f4e..8447eb035 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -26,8 +26,8 @@ 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 *) } @@ -38,7 +38,8 @@ val eval_command : status -> LexiconAst.command -> status 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 *) diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli index a291b3a9b..03875690a 100644 --- a/helm/software/components/lexicon/lexiconSync.mli +++ b/helm/software/components/lexicon/lexiconSync.mli @@ -35,7 +35,8 @@ val time_travel: * 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 diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 0d758d77c..833273319 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,2 +1,4 @@ nDisambiguate.cmo: nDisambiguate.cmi nDisambiguate.cmx: nDisambiguate.cmi +nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi +nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt new file mode 100644 index 000000000..833273319 --- /dev/null +++ b/helm/software/components/ng_disambiguation/.depend.opt @@ -0,0 +1,4 @@ +nDisambiguate.cmo: nDisambiguate.cmi +nDisambiguate.cmx: nDisambiguate.cmi +nGrafiteDisambiguator.cmo: nDisambiguate.cmi nGrafiteDisambiguator.cmi +nGrafiteDisambiguator.cmx: nDisambiguate.cmx nGrafiteDisambiguator.cmi diff --git a/helm/software/components/ng_disambiguation/Makefile b/helm/software/components/ng_disambiguation/Makefile index f753387f4..3bac09451 100644 --- a/helm/software/components/ng_disambiguation/Makefile +++ b/helm/software/components/ng_disambiguation/Makefile @@ -2,7 +2,7 @@ PACKAGE = ng_disambiguation PREDICATES = INTERFACE_FILES = \ - nDisambiguate.mli\ + nDisambiguate.mli nGrafiteDisambiguator.mli\ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index 514e2f781..5313ee20f 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -1,29 +1,15 @@ -(* 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 diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.mli b/helm/software/components/ng_disambiguation/nDisambiguate.mli index 279e54b78..a61d37653 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nDisambiguate.mli @@ -1,4 +1,15 @@ +(* + ||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 : diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml new file mode 100644 index 000000000..328856a0f --- /dev/null +++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml @@ -0,0 +1,203 @@ +(* + ||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 = (* *) + 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 diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli new file mode 100644 index 000000000..2e47b4ffb --- /dev/null +++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli @@ -0,0 +1,45 @@ +(* + ||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 + diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index bb4537d8d..bdde2dd39 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -32,7 +32,8 @@ val eval_ast : 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 @@ -57,7 +58,8 @@ val eval_from_stream : 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 *) diff --git a/helm/software/matita/matitaExcPp.mli b/helm/software/matita/matitaExcPp.mli index 77a5a3ce9..4a40f6c24 100644 --- a/helm/software/matita/matitaExcPp.mli +++ b/helm/software/matita/matitaExcPp.mli @@ -26,12 +26,12 @@ 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 diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 0cbf2d89a..234d44be9 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -327,9 +327,10 @@ let rec interactive_error_interp ~all_passes 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 -- 2.39.2