X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=f82759195dae6bf5e50fbba9add0ed7fe09c09bc;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=143ac5e11f83949682d513dfd51bb0f39328f4c1;hpb=a5709dff43233c041f77a4ee4b7f2df1a3c51ab6;p=helm.git diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index 143ac5e11..f82759195 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -27,13 +27,13 @@ class type g_status = object - inherit LexiconEngine.g_status + inherit LexiconTypes.g_status inherit NCicCoercion.g_status end class status = object (self) - inherit LexiconEngine.status + inherit LexiconTypes.status inherit NCicCoercion.status method set_grafite_disambiguate_status : 'status. #g_status as 'status -> 'self @@ -55,7 +55,7 @@ let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" let ncic_mk_choice status = function - | LexiconAst.Symbol_alias (name, _, dsc) -> + | GrafiteAst.Symbol_alias (name, _, dsc) -> if name = __Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) else if name = __Closed_Implicit then @@ -69,11 +69,11 @@ let ncic_mk_choice status = function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) ~term_of_nref:(fun nref -> NCic.Const nref) name dsc - | LexiconAst.Number_alias (_, dsc) -> + | GrafiteAst.Number_alias (_, dsc) -> let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in desc, `Num_interp (fun num -> match f with `Num_interp f -> f num | _ -> assert false) - | LexiconAst.Ident_alias (name, uri) -> + | GrafiteAst.Ident_alias (name, uri) -> uri, `Sym_interp (fun l->assert(l = []); let nref = NReference.reference_of_string uri in @@ -84,9 +84,9 @@ let ncic_mk_choice status = function let mk_implicit b = match b with | false -> - LexiconAst.Symbol_alias (__Implicit,-1,"Fake Implicit") + GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") | true -> - LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") + GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") ;; let nlookup_in_library @@ -97,7 +97,7 @@ let nlookup_in_library (try let references = NCicLibrary.resolve id in List.map - (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u) + (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) ) references with NCicEnvironment.ObjectNotFound _ -> []) @@ -109,13 +109,13 @@ let fix_instance item l = DisambiguateTypes.Symbol (_,n) -> List.map (function - LexiconAst.Symbol_alias (s,_,d) -> LexiconAst.Symbol_alias (s,n,d) + GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) | _ -> assert false ) l | DisambiguateTypes.Num n -> List.map (function - LexiconAst.Number_alias (_,d) -> LexiconAst.Number_alias (n,d) + GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d) | _ -> assert false ) l | DisambiguateTypes.Id _ -> l @@ -128,16 +128,18 @@ let disambiguate_nterm expty estatus context metasenv subst thing singleton "first" (NCicDisambiguate.disambiguate_term ~rdb:estatus - ~aliases:estatus#lstatus.LexiconEngine.aliases + ~aliases:estatus#lstatus.LexiconTypes.aliases ~expty - ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) + ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) ~lookup_in_library:nlookup_in_library ~mk_choice:(ncic_mk_choice estatus) ~mk_implicit ~fix_instance - ~description_of_alias:LexiconAst.description_of_alias + ~description_of_alias:GrafiteAst.description_of_alias ~context ~metasenv ~subst thing) in - let estatus = LexiconEngine.set_proof_aliases estatus diff in + let estatus = + LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff + in metasenv, subst, estatus, cic ;; @@ -209,14 +211,15 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = singleton "third" (NCicDisambiguate.disambiguate_obj ~lookup_in_library:nlookup_in_library - ~description_of_alias:LexiconAst.description_of_alias + ~description_of_alias:GrafiteAst.description_of_alias ~mk_choice:(ncic_mk_choice estatus) ~mk_implicit ~fix_instance ~uri ~rdb:estatus - ~aliases:estatus#lstatus.LexiconEngine.aliases - ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) + ~aliases:estatus#lstatus.LexiconTypes.aliases + ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) (text,prefix_len,obj)) in - let estatus = LexiconEngine.set_proof_aliases estatus diff in + let estatus = LexiconEngine.set_proof_aliases estatus + GrafiteAst.WithPreferences diff in estatus, cic ;;