From e9c6de34f4a1e784050a78db81787502cd112976 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 28 Oct 2009 15:26:49 +0000 Subject: [PATCH] One-shot aliases were no longer generated because of a bug (i.e. all aliases retrieved from the universe used to have instance=0). Fixed by parameterizing once again all the functions with a ~fix_instance function to fix the instance. --- .../cic_disambiguation/cicDisambiguate.ml | 7 ++-- .../cic_disambiguation/cicDisambiguate.mli | 2 ++ .../components/disambiguation/disambiguate.ml | 14 ++++---- .../disambiguation/disambiguate.mli | 1 + .../disambiguation/multiPassDisambiguator.ml | 11 ++++--- .../disambiguation/multiPassDisambiguator.mli | 1 + .../grafite_parser/grafiteDisambiguate.ml | 28 +++++++++++++--- .../ng_disambiguation/nCicDisambiguate.ml | 8 ++--- .../ng_disambiguation/nCicDisambiguate.mli | 32 +++++++++++-------- 9 files changed, 67 insertions(+), 37 deletions(-) diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 853c38e4b..8f8bba7d8 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml @@ -649,13 +649,14 @@ let string_context_of_context = let disambiguate_term ~context ~metasenv ~subst ~expty ?(initial_ugraph = CicUniv.oblivion_ugraph) - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~lookup_in_library (text,prefix_len,term) = let mk_localization_tbl x = Cic.CicHash.create x in MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst ~initial_ugraph ~aliases ~string_context_of_context ~universe ~lookup_in_library ~mk_implicit ~description_of_alias + ~fix_instance ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) @@ -665,7 +666,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty ~freshen_thing:CicNotationUtil.freshen_term ~passes:(MultiPassDisambiguator.passes ()) -let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice +let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) = let mk_localization_tbl x = Cic.CicHash.create x in @@ -673,7 +674,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice ~aliases ~universe ~uri ~string_context_of_context ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library ~mk_implicit ~description_of_alias + ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance ~initial_ugraph:CicUniv.empty_ugraph ~interpretate_thing:(interpretate_obj ~mk_choice) ~refine_thing:refine_obj diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.mli b/helm/software/components/cic_disambiguation/cicDisambiguate.mli index ecb592682..52919dfa1 100644 --- a/helm/software/components/cic_disambiguation/cicDisambiguate.mli +++ b/helm/software/components/cic_disambiguation/cicDisambiguate.mli @@ -35,6 +35,7 @@ val disambiguate_term : ?initial_ugraph:CicUniv.universe_graph -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> @@ -54,6 +55,7 @@ val disambiguate_term : val disambiguate_obj : mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index f3ba95765..5ac709f9b 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -408,11 +408,16 @@ let domain_diff dom1 dom2 = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" +type alias_spec = + | Ident_alias of string * string (* identifier, uri *) + | Symbol_alias of string * int * string (* name, instance no, description *) + | Number_alias of int * string (* instance no, description *) + let disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context ~initial_ugraph:base_univ ~expty - ~mk_implicit ~description_of_alias + ~mk_implicit ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl @@ -439,12 +444,7 @@ let disambiguate_thing input_or_locate_uri item | Some e -> (try - let item = - match item with - | Symbol (symb, _) -> Symbol (symb, 0) - | item -> item - in - Environment.find item e + fix_instance item (Environment.find item e) with Not_found -> []) in (* diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index ffbdf884d..cffb1df0a 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -96,6 +96,7 @@ val disambiguate_thing: expty: 'refined_thing option -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> lookup_in_library:( diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index 5767aa3e3..d3250c2fe 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -141,19 +141,22 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing | [] -> assert false in aux 1 [] passes +;; let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit - ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing - ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing + ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~mk_localization_tbl thing = let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = let thing = if fresh_instances then freshen_thing thing else thing in Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context - ~initial_ugraph ~expty ~mk_implicit ~description_of_alias + ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl (txt,len,thing) in - disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing + disambiguate_thing ~description_of_alias ~passes ~aliases + ~universe ~f thing diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli index a5b5def32..41b79c9b0 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -50,6 +50,7 @@ val disambiguate_thing: expty: 'refined_thing option -> mk_implicit:(bool -> 'alias) -> description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index b53d6ea3f..6aee803f4 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -175,6 +175,24 @@ let nlookup_in_library | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item ;; +let fix_instance item l = + match item with + DisambiguateTypes.Symbol (_,n) -> + List.map + (function + LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Num n -> + List.map + (function + LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Id _ -> l +;; + + (** @param term not meaningful when context is given *) let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv term = @@ -186,7 +204,7 @@ term = ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit + ~mk_implicit ~fix_instance ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst:[] (text,prefix_len,term)) in @@ -206,7 +224,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) ~lookup_in_library:nlookup_in_library ~mk_choice:ncic_mk_choice - ~mk_implicit + ~mk_implicit ~fix_instance ~description_of_alias:LexiconAst.description_of_alias ~context ~metasenv ~subst thing) in @@ -228,7 +246,7 @@ let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term = (CicDisambiguate.disambiguate_term ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit + ~mk_implicit ~fix_instance ~description_of_alias:LexiconAst.description_of_alias ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) @@ -734,7 +752,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = (CicDisambiguate.disambiguate_obj ~lookup_in_library ~mk_choice:cic_mk_choice - ~mk_implicit + ~mk_implicit ~fix_instance ~description_of_alias:LexiconAst.description_of_alias ~aliases:estatus#lstatus.LexiconEngine.aliases ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) @@ -781,7 +799,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ~lookup_in_library:nlookup_in_library ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice - ~mk_implicit + ~mk_implicit ~fix_instance ~uri:(OCic2NCic.nuri_of_ouri uri) ~rdb:estatus ~aliases:estatus#lstatus.LexiconEngine.aliases diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index f221a2b05..7ebca20d7 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -614,7 +614,7 @@ let interpretate_obj ;; let disambiguate_term ~context ~metasenv ~subst ~expty - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~rdb ~lookup_in_library (text,prefix_len,term) = @@ -623,7 +623,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_term ~context ~metasenv ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias + ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~passes:(MultiPassDisambiguator.passes ()) @@ -636,7 +636,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty ;; let disambiguate_obj - ~mk_implicit ~description_of_alias ~mk_choice + ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice ~aliases ~universe ~rdb ~lookup_in_library ~uri (text,prefix_len,obj) = @@ -645,7 +645,7 @@ let disambiguate_obj MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_obj ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases - ~mk_implicit ~description_of_alias + ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:(Some uri) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index a9f15244c..d28708e3a 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -20,6 +20,7 @@ val disambiguate_term : expty:NCic.term option -> mk_implicit: (bool -> 'alias) -> description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> @@ -37,20 +38,23 @@ val disambiguate_term : bool val disambiguate_obj : - mk_implicit:(bool -> 'a) -> - description_of_alias:('a -> string) -> - mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) -> - aliases:'a DisambiguateTypes.Environment.t -> - universe:'a list DisambiguateTypes.Environment.t option -> - rdb:#NRstatus.status -> - lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> 'a list) -> - uri:NUri.uri -> - string * int * CicNotationPt.term CicNotationPt.obj -> - ((DisambiguateTypes.Environment.key * 'a) list * NCic.metasenv * - NCic.substitution * NCic.obj) - list * bool + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> + mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> + rdb:#NRstatus.status -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + 'alias list) -> + uri:NUri.uri -> + string * int * CicNotationPt.term CicNotationPt.obj -> + ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv * + NCic.substitution * NCic.obj) + list * bool val disambiguate_path: CicNotationPt.term -> NCic.term -- 2.39.2