X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=f82759195dae6bf5e50fbba9add0ed7fe09c09bc;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=bd633d5d2edb26057068c8ee0f8c3dc7146971a3;hpb=d284dd23d0e12a62a001d3473eadf4942d12ffaa;p=helm.git diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index bd633d5d2..f82759195 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -25,13 +25,23 @@ (* $Id$ *) +class type g_status = + object + inherit LexiconTypes.g_status + inherit NCicCoercion.g_status + end + +class status = + object (self) + inherit LexiconTypes.status + inherit NCicCoercion.status + method set_grafite_disambiguate_status + : 'status. #g_status as 'status -> 'self + = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o + end + exception BaseUriNotSetYet -type tactic = - (NotationPt.term, NotationPt.term, - NotationPt.term GrafiteAst.reduction, string) - GrafiteAst.tactic - let singleton msg = function | [x], _ -> x | l, _ -> @@ -44,27 +54,26 @@ let singleton msg = function let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let ncic_mk_choice = function - | LexiconAst.Symbol_alias (name, _, dsc) -> +let ncic_mk_choice status = function + | GrafiteAst.Symbol_alias (name, _, dsc) -> if name = __Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Term) else if name = __Closed_Implicit then dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed) else - DisambiguateChoices.lookup_symbol_by_dsc + DisambiguateChoices.lookup_symbol_by_dsc status ~mk_implicit:(function | true -> NCic.Implicit `Closed | false -> NCic.Implicit `Term) ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) - ~term_of_uri:(fun _ -> assert false) ~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 @@ -75,9 +84,9 @@ let ncic_mk_choice = 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 @@ -88,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 _ -> []) @@ -100,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 @@ -119,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 + ~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 ;; @@ -200,31 +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 - ~mk_choice:ncic_mk_choice + ~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 ;; -let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)= - match cmd with - | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Select (loc,uri) -> - estatus, GrafiteAst.Select(loc,uri) - | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Default _ - | GrafiteAst.Drop _ - | GrafiteAst.Include _ - | GrafiteAst.Print _ - | GrafiteAst.Qed _ - | GrafiteAst.Set _ as cmd -> - estatus,cmd - | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false