From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 22:32:02 +0000 (+0000) Subject: - further simplifications (??) of the status dependencies X-Git-Tag: make_still_working~2727 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9f775a550264a8dc9ce7ea9a48b79892a122c3c;p=helm.git - further simplifications (??) of the status dependencies --- diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 50095cf13..7fa62ff74 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -51,7 +51,7 @@ let inject_unification_hint = let eval_unification_hint status t n = let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in let status = basic_eval_unification_hint (t,n) status in @@ -78,7 +78,7 @@ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status = let diff = [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)] in - LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff ;; let inject_interpretation = @@ -479,7 +479,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (fun status (name,cpos,arity) -> try let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,NotationPt.Ident (name,None)) in assert (metasenv = [] && subst = []); let status, nuris = @@ -571,7 +571,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let metasenv,subst,status,sort = match sort with | None -> [],[],status,NCic.Sort NCic.Prop | Some s -> - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,s) in assert (metasenv = []); @@ -585,7 +585,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (NCicPp.ppterm ~metasenv ~subst ~context:[] sort))) in let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm None status [] [] subst + GrafiteDisambiguate.disambiguate_nterm status None [] [] subst (text,prefix_len,indty) in let indtyno,(_,leftno,tys,_,_) = match indty with @@ -623,7 +623,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = try match DisambiguateTypes.Environment.find item - status#lstatus.LexiconTypes.aliases + status#disambiguate_db.GrafiteDisambiguate.aliases with GrafiteAst.Ident_alias (_, uri) -> NotationPt.NRefPattern (NReference.reference_of_string uri) @@ -632,7 +632,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)); - LexiconEngine.dump_aliases prerr_endline "" status; + GrafiteDisambiguate.dump_aliases prerr_endline "" status; raise (Failure ((DisambiguateTypes.string_of_domain_item item) ^ " not found")) @@ -670,7 +670,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = [DisambiguateTypes.Num instance,spec] in let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*) - LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff (* assert false (* MANCA SALVATAGGIO SU DISCO *) *) ;; diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 573fa28c9..0e1b87fa1 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -42,6 +42,7 @@ class status = fun (b : string) -> inherit NCicLibrary.dumpable_status inherit NCicLibrary.status inherit GrafiteParser.status + inherit TermContentPres.status val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) method baseuri = baseuri diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index fd89f4648..4e226f703 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -39,6 +39,7 @@ class status : inherit NCicLibrary.dumpable_status inherit NCicLibrary.status inherit GrafiteParser.status + inherit TermContentPres.status method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml index ca56a3aee..7cc5644d9 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.ml +++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml @@ -133,7 +133,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = (try let metasenv,subst,status,src = GrafiteDisambiguate.disambiguate_nterm - None status ctx [] [] ("",0,src) in + status None ctx [] [] ("",0,src) in let src = NCicUntrusted.apply_subst subst [] src in (* CHECK that the declared pattern matches the abstraction *) let _ = NCicUnification.unify status metasenv subst ctx ty src in @@ -151,7 +151,7 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = let status, tgt, arity = let metasenv,subst,status,tgt = GrafiteDisambiguate.disambiguate_nterm - None status [] [] [] ("",0,tgt) in + status None [] [] [] ("",0,tgt) in let tgt = NCicUntrusted.apply_subst subst [] tgt in (* CHECK che sia unificabile mancante *) let rec count_prod = function @@ -313,11 +313,11 @@ let basic_eval_and_record_ncoercion_from_t_cpos_arity let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt = let metasenv,subst,status,ty = - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in assert (metasenv=[]); let ty = NCicUntrusted.apply_subst subst [] ty in let metasenv,subst,status,t = - GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in + GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in let status, src, tgt, cpos, arity = diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend index e45f9bef8..b8b65a8c0 100644 --- a/matita/components/grafite_parser/.depend +++ b/matita/components/grafite_parser/.depend @@ -1,12 +1,9 @@ dependenciesParser.cmi: grafiteParser.cmi: -grafiteDisambiguate.cmi: print_grammar.cmi: grafiteParser.cmi dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi grafiteParser.cmx: grafiteParser.cmi -grafiteDisambiguate.cmo: grafiteDisambiguate.cmi -grafiteDisambiguate.cmx: grafiteDisambiguate.cmi print_grammar.cmo: print_grammar.cmi print_grammar.cmx: print_grammar.cmi diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 631e40eb4..1005a0019 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -4,8 +4,7 @@ PREDICATES = INTERFACE_FILES = \ dependenciesParser.mli \ grafiteParser.mli \ - grafiteDisambiguate.mli \ - print_grammar.mli \ + print_grammar.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml deleted file mode 100644 index 7511e02aa..000000000 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ /dev/null @@ -1,226 +0,0 @@ -(* - * - * 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/ - *) - -(* $Id$ *) - -class type g_status = - object - inherit LexiconTypes.g_status - end - -class status = - object (self) - inherit LexiconTypes.status - method set_grafite_disambiguate_status - : 'status. #g_status as 'status -> 'self - = fun o -> (self#set_lexicon_engine_status o) - end - -exception BaseUriNotSetYet - -let singleton msg = function - | [x], _ -> x - | l, _ -> - let debug = - Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" - msg (List.length l) - in - prerr_endline debug; assert false - -let __Implicit = "__Implicit__" -let __Closed_Implicit = "__Closed_Implicit__" - -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 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_nref:(fun nref -> NCic.Const nref) - name 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) - | GrafiteAst.Ident_alias (name, uri) -> - uri, `Sym_interp - (fun l->assert(l = []); - let nref = NReference.reference_of_string uri in - NCic.Const nref) -;; - - -let mk_implicit b = - match b with - | false -> - GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") - | true -> - GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") -;; - -let nlookup_in_library - interactive_user_uri_choice input_or_locate_uri item -= - match item with - | DisambiguateTypes.Id id -> - (try - let references = NCicLibrary.resolve id in - List.map - (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) - ) references - with - NCicEnvironment.ObjectNotFound _ -> []) - | _ -> [] -;; - -let fix_instance item l = - match item with - DisambiguateTypes.Symbol (_,n) -> - List.map - (function - GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) - | _ -> assert false - ) l - | DisambiguateTypes.Num n -> - List.map - (function - GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d) - | _ -> assert false - ) l - | DisambiguateTypes.Id _ -> l -;; - - -let disambiguate_nterm expty estatus context metasenv subst thing -= - let diff, metasenv, subst, cic = - singleton "first" - (NCicDisambiguate.disambiguate_term - ~rdb:estatus - ~aliases:estatus#lstatus.LexiconTypes.aliases - ~expty - ~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:GrafiteAst.description_of_alias - ~context ~metasenv ~subst thing) - in - let estatus = - LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true - GrafiteAst.WithPreferences diff - in - metasenv, subst, estatus, cic -;; - - -type pattern = - NotationPt.term Disambiguate.disambiguator_input option * - (string * NCic.term) list * NCic.term option - -let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = - let interp path = NCicDisambiguate.disambiguate_path path in - let goal_path = HExtlib.map_option interp goal_path in - let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - let wanted = - match wanted with None -> None | Some x -> Some (text,prefix_len,x) - in - (wanted, hyp_paths, goal_path) -;; - -let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function - | `Unfold (Some t) -> assert false (* MATITA 1.0 *) - | `Normalize - | `Simpl - | `Unfold None - | `Whd as kind -> kind -;; - -let disambiguate_auto_params - disambiguate_term metasenv context (oterms, params) -= - match oterms with - | None -> metasenv, (None, params) - | Some terms -> - let metasenv, terms = - List.fold_right - (fun t (metasenv, terms) -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,t::terms) terms (metasenv, []) - in - metasenv, (Some terms, params) -;; - -let disambiguate_just disambiguate_term context metasenv = - function - `Term t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv, `Term t - | `Auto params -> - let metasenv,params = disambiguate_auto_params disambiguate_term metasenv - context params - in - metasenv, `Auto params -;; - -let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = - let uri = - let baseuri = - match baseuri with Some x -> x | None -> raise BaseUriNotSetYet - in - let name = - match obj with - | NotationPt.Inductive (_,(name,_,_,_)::_) - | NotationPt.Record (_,name,_,_) -> name ^ ".ind" - | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" - | NotationPt.Inductive _ -> assert false - in - NUri.uri_of_string (baseuri ^ "/" ^ name) - in - let diff, _, _, cic = - singleton "third" - (NCicDisambiguate.disambiguate_obj - ~lookup_in_library:nlookup_in_library - ~description_of_alias:GrafiteAst.description_of_alias - ~mk_choice:(ncic_mk_choice estatus) - ~mk_implicit ~fix_instance - ~uri - ~rdb:estatus - ~aliases:estatus#lstatus.LexiconTypes.aliases - ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) - (text,prefix_len,obj)) in - let estatus = - LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true - GrafiteAst.WithPreferences diff - in - estatus, cic -;; diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli deleted file mode 100644 index 6caf5301f..000000000 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* Copyright (C) 2004-2005, 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/ - *) - -exception BaseUriNotSetYet - -val disambiguate_nterm : - NCic.term option -> - (#LexiconTypes.status as 'status) -> - NCic.context -> NCic.metasenv -> NCic.substitution -> - NotationPt.term Disambiguate.disambiguator_input -> - NCic.metasenv * NCic.substitution * 'status * NCic.term - -val disambiguate_nobj : - #LexiconTypes.status as 'status -> - ?baseuri:string -> - (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> - 'status * NCic.obj - -type pattern = - NotationPt.term Disambiguate.disambiguator_input option * - (string * NCic.term) list * NCic.term option - -val disambiguate_npattern: - GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 5b092a6d3..fb042585a 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -27,7 +27,6 @@ module N = NotationPt module G = GrafiteAst -module LE = LexiconEngine type 'a localized_option = LSome of 'a diff --git a/matita/components/lexicon/.depend b/matita/components/lexicon/.depend index 43aa8b202..ae6436114 100644 --- a/matita/components/lexicon/.depend +++ b/matita/components/lexicon/.depend @@ -1,9 +1,9 @@ -lexiconTypes.cmi: -lexiconEngine.cmi: lexiconTypes.cmi +grafiteDisambiguate.cmi: +lexiconTypes.cmi: grafiteDisambiguate.cmi lexiconSync.cmi: lexiconTypes.cmi -lexiconTypes.cmo: lexiconTypes.cmi -lexiconTypes.cmx: lexiconTypes.cmi -lexiconEngine.cmo: lexiconTypes.cmi lexiconEngine.cmi -lexiconEngine.cmx: lexiconTypes.cmx lexiconEngine.cmi -lexiconSync.cmo: lexiconTypes.cmi lexiconEngine.cmi lexiconSync.cmi -lexiconSync.cmx: lexiconTypes.cmx lexiconEngine.cmx lexiconSync.cmi +grafiteDisambiguate.cmo: grafiteDisambiguate.cmi +grafiteDisambiguate.cmx: grafiteDisambiguate.cmi +lexiconTypes.cmo: grafiteDisambiguate.cmi lexiconTypes.cmi +lexiconTypes.cmx: grafiteDisambiguate.cmx lexiconTypes.cmi +lexiconSync.cmo: lexiconSync.cmi +lexiconSync.cmx: lexiconSync.cmi diff --git a/matita/components/lexicon/Makefile b/matita/components/lexicon/Makefile index 1213f0b52..b7aba0ebd 100644 --- a/matita/components/lexicon/Makefile +++ b/matita/components/lexicon/Makefile @@ -2,8 +2,7 @@ PACKAGE = lexicon PREDICATES = INTERFACE_FILES = \ - lexiconTypes.mli \ - lexiconEngine.mli \ + grafiteDisambiguate.mli \ lexiconSync.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/matita/components/lexicon/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml new file mode 100644 index 000000000..5b27aba1b --- /dev/null +++ b/matita/components/lexicon/grafiteDisambiguate.ml @@ -0,0 +1,274 @@ +(* + * + * 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/ + *) + +(* $Id$ *) + +type db = { + aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; + new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list +} + +let initial_status = { + aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; + new_aliases = [] +} + +class type g_status = + object + inherit Interpretations.g_status + method disambiguate_db: db + end + +class status = + object (self) + inherit Interpretations.status + val disambiguate_db = initial_status + method disambiguate_db = disambiguate_db + method set_disambiguate_db v = {< disambiguate_db = v >} + method set_disambiguate_status + : 'status. #g_status as 'status -> 'self + = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) + end + +let dump_aliases out msg status = + out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:"); + DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x)) + status#disambiguate_db.aliases + +let set_proof_aliases status ~implicit_aliases mode new_aliases = + if mode = GrafiteAst.WithoutPreferences then + status + else + (* MATITA 1.0 + let new_commands = + List.map + (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases + in *) + let aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) + status#disambiguate_db.aliases new_aliases in + let multi_aliases = + List.fold_left (fun acc (d,c) -> + DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias + d c acc) + status#disambiguate_db.multi_aliases new_aliases + in + let new_status = + {multi_aliases = multi_aliases ; + aliases = aliases; + new_aliases = + (if implicit_aliases then new_aliases else []) @ + status#disambiguate_db.new_aliases} + in + status#set_disambiguate_db new_status + +exception BaseUriNotSetYet + +let singleton msg = function + | [x], _ -> x + | l, _ -> + let debug = + Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations" + msg (List.length l) + in + prerr_endline debug; assert false + +let __Implicit = "__Implicit__" +let __Closed_Implicit = "__Closed_Implicit__" + +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 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_nref:(fun nref -> NCic.Const nref) + name 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) + | GrafiteAst.Ident_alias (name, uri) -> + uri, `Sym_interp + (fun l->assert(l = []); + let nref = NReference.reference_of_string uri in + NCic.Const nref) +;; + + +let mk_implicit b = + match b with + | false -> + GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit") + | true -> + GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") +;; + +let nlookup_in_library + interactive_user_uri_choice input_or_locate_uri item += + match item with + | DisambiguateTypes.Id id -> + (try + let references = NCicLibrary.resolve id in + List.map + (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u) + ) references + with + NCicEnvironment.ObjectNotFound _ -> []) + | _ -> [] +;; + +let fix_instance item l = + match item with + DisambiguateTypes.Symbol (_,n) -> + List.map + (function + GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Num n -> + List.map + (function + GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d) + | _ -> assert false + ) l + | DisambiguateTypes.Id _ -> l +;; + + +let disambiguate_nterm estatus expty context metasenv subst thing += + let diff, metasenv, subst, cic = + singleton "first" + (NCicDisambiguate.disambiguate_term + ~rdb:estatus + ~aliases:estatus#disambiguate_db.aliases + ~expty + ~universe:(Some estatus#disambiguate_db.multi_aliases) + ~lookup_in_library:nlookup_in_library + ~mk_choice:(ncic_mk_choice estatus) + ~mk_implicit ~fix_instance + ~description_of_alias:GrafiteAst.description_of_alias + ~context ~metasenv ~subst thing) + in + let estatus = + set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences + diff + in + metasenv, subst, estatus, cic +;; + + +type pattern = + NotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = + let interp path = NCicDisambiguate.disambiguate_path path in + let goal_path = HExtlib.map_option interp goal_path in + let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in + let wanted = + match wanted with None -> None | Some x -> Some (text,prefix_len,x) + in + (wanted, hyp_paths, goal_path) +;; + +let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function + | `Unfold (Some t) -> assert false (* MATITA 1.0 *) + | `Normalize + | `Simpl + | `Unfold None + | `Whd as kind -> kind +;; + +let disambiguate_auto_params + disambiguate_term metasenv context (oterms, params) += + match oterms with + | None -> metasenv, (None, params) + | Some terms -> + let metasenv, terms = + List.fold_right + (fun t (metasenv, terms) -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,t::terms) terms (metasenv, []) + in + metasenv, (Some terms, params) +;; + +let disambiguate_just disambiguate_term context metasenv = + function + `Term t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv, `Term t + | `Auto params -> + let metasenv,params = disambiguate_auto_params disambiguate_term metasenv + context params + in + metasenv, `Auto params +;; + +let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = + let uri = + let baseuri = + match baseuri with Some x -> x | None -> raise BaseUriNotSetYet + in + let name = + match obj with + | NotationPt.Inductive (_,(name,_,_,_)::_) + | NotationPt.Record (_,name,_,_) -> name ^ ".ind" + | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" + | NotationPt.Inductive _ -> assert false + in + NUri.uri_of_string (baseuri ^ "/" ^ name) + in + let diff, _, _, cic = + singleton "third" + (NCicDisambiguate.disambiguate_obj + ~lookup_in_library:nlookup_in_library + ~description_of_alias:GrafiteAst.description_of_alias + ~mk_choice:(ncic_mk_choice estatus) + ~mk_implicit ~fix_instance + ~uri + ~rdb:estatus + ~aliases:estatus#disambiguate_db.aliases + ~universe:(Some estatus#disambiguate_db.multi_aliases) + (text,prefix_len,obj)) in + let estatus = + set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences + diff + in + estatus, cic +;; diff --git a/matita/components/lexicon/grafiteDisambiguate.mli b/matita/components/lexicon/grafiteDisambiguate.mli new file mode 100644 index 000000000..6b203cab4 --- /dev/null +++ b/matita/components/lexicon/grafiteDisambiguate.mli @@ -0,0 +1,73 @@ +(* Copyright (C) 2004-2005, 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/ + *) + +type db = { + aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; + multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; + new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list +} + +class type g_status = + object + inherit Interpretations.g_status + method disambiguate_db: db + end + +class status : + object ('self) + inherit g_status + inherit Interpretations.status + method set_disambiguate_db: db -> 'self + method set_disambiguate_status: #g_status -> 'self + end + +val set_proof_aliases: + #status as 'status -> + implicit_aliases:bool -> (* implicit ones are made explicit *) + GrafiteAst.inclusion_mode -> + (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status + +(* args: print function, message (may be empty), status *) +val dump_aliases: (string -> unit) -> string -> #status -> unit + +exception BaseUriNotSetYet + +val disambiguate_nterm : + #status as 'status -> + NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution -> + NotationPt.term Disambiguate.disambiguator_input -> + NCic.metasenv * NCic.substitution * 'status * NCic.term + +val disambiguate_nobj : + #status as 'status -> ?baseuri:string -> + (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> + 'status * NCic.obj + +type pattern = + NotationPt.term Disambiguate.disambiguator_input option * + (string * NCic.term) list * NCic.term option + +val disambiguate_npattern: + GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml index 9a5ff7633..e06c04372 100644 --- a/matita/components/lexicon/lexiconSync.ml +++ b/matita/components/lexicon/lexiconSync.ml @@ -37,6 +37,6 @@ let add_aliases_for_objs status = GrafiteAst.Ident_alias (name,NReference.string_of_reference u) ) references in - LexiconEngine.set_proof_aliases status ~implicit_aliases:false + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false GrafiteAst.WithPreferences new_env ) status diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli index f9ed52406..b46af6fbb 100644 --- a/matita/components/lexicon/lexiconSync.mli +++ b/matita/components/lexicon/lexiconSync.mli @@ -24,4 +24,4 @@ *) val add_aliases_for_objs: - #LexiconTypes.status as 'status -> NUri.uri list -> 'status + #GrafiteDisambiguate.status as 'status -> NUri.uri list -> 'status diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml deleted file mode 100644 index 4f57cbfc3..000000000 --- a/matita/components/lexicon/lexiconTypes.ml +++ /dev/null @@ -1,56 +0,0 @@ -(* Copyright (C) 2004-2005, 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/ - *) - -(* $Id$ *) - -type lexicon_status = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -} - -let initial_status = { - aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty; - new_aliases = [] -} - -class type g_status = - object - inherit Interpretations.g_status - inherit TermContentPres.g_status - method lstatus: lexicon_status - end - -class status = - object(self) - inherit Interpretations.status - inherit TermContentPres.status - val lstatus = initial_status - method lstatus = lstatus - method set_lstatus v = {< lstatus = v >} - method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self - = fun o -> ((self#set_lstatus o#lstatus)#set_interp_status o)#set_content_pres_status o - end diff --git a/matita/components/lexicon/lexiconTypes.mli b/matita/components/lexicon/lexiconTypes.mli deleted file mode 100644 index 0ffd78bac..000000000 --- a/matita/components/lexicon/lexiconTypes.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* Copyright (C) 2004-2005, 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/ - *) - -type lexicon_status = { - aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; - new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -} - -class type g_status = - object - inherit Interpretations.g_status - inherit TermContentPres.g_status - method lstatus: lexicon_status - end - -class status : - object ('self) - inherit g_status - inherit Interpretations.status - inherit TermContentPres.status - method set_lstatus: lexicon_status -> 'self - method set_lexicon_engine_status: #g_status -> 'self - end diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index fbcdccb31..26e92add4 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -66,7 +66,7 @@ class auto_status = class type g_pstatus = object - inherit LexiconTypes.g_status + inherit GrafiteDisambiguate.g_status inherit g_auto_status inherit g_eq_status method obj: NCic.obj @@ -75,7 +75,7 @@ class type g_pstatus = class pstatus = fun (o: NCic.obj) -> object (self) - inherit LexiconTypes.status + inherit GrafiteDisambiguate.status inherit auto_status inherit eq_status val obj = o @@ -83,7 +83,7 @@ class pstatus = method set_obj o = {< obj = o >} method set_pstatus : 'status. #g_pstatus as 'status -> 'self = fun o -> - (((self#set_lexicon_engine_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o + (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o end type tactic_term = NotationPt.term Disambiguate.disambiguator_input @@ -195,7 +195,7 @@ let disambiguate status context t ty = in let uri,height,metasenv,subst,obj = status#obj in let metasenv, subst, status, t = - GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t + GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t in let new_pstatus = uri,height,metasenv,subst,obj in status#set_obj new_pstatus, (context, t) diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index ddaf9da80..cfb7123bb 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -43,7 +43,7 @@ class auto_status : class type g_pstatus = object - inherit LexiconTypes.g_status + inherit GrafiteDisambiguate.g_status inherit g_auto_status inherit g_eq_status method obj: NCic.obj @@ -52,7 +52,7 @@ class type g_pstatus = class pstatus : NCic.obj -> object ('self) - inherit LexiconTypes.status + inherit GrafiteDisambiguate.status inherit auto_status inherit eq_status method obj: NCic.obj diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index 731cffeaa..38800d6c0 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -4,14 +4,18 @@ grafitetypes(baseuri,ng_mode) |--> grafiteparser(db=ast_statement grammarentry) | |--> cicnotationparser(db=grammars+keywords+items) | + |--> termcontentpres(db=level1_patterns21,compiled21, + | pattern21_matrix,counter) + | |--> tac(obj,stack) |--> auto(automation_cache) |--> eq(eq_cache) - |--> lexicon(lstatus=aliases+multi_aliases+new_aliases) + |--> grafitedisambiguate(db=aliases+multi_aliases+new_aliases) |--> interpretation(db=level2_patterns32,compiled32, - | | pattern32_matrix,counter) - | |--> nciccoercion(db=...) - | |--> unif_hint(db=...) - | - |--> termcontentpres(db=level1_patterns21,compiled21, - pattern21_matrix,counter) + | pattern32_matrix,counter) + |--> nciccoercion(db=...) + |--> unif_hint(db=...) + +applytransformation() + |--> termcontentpres(...) + |--> interpretation(...) diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index da250c912..236e59def 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -35,6 +35,12 @@ (* $Id$ *) +class status = + object + inherit Interpretations.status + inherit TermContentPres.status + end + let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index d5c99447d..bcf3690d2 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -33,11 +33,17 @@ (* *) (***************************************************************************) +class status : + object + inherit Interpretations.status + inherit TermContentPres.status + end + val ntxt_of_cic_sequent: - map_unicode_to_tex:bool -> int -> #LexiconTypes.status -> + map_unicode_to_tex:bool -> int -> #status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) val ntxt_of_cic_object: - map_unicode_to_tex:bool -> int -> #LexiconTypes.status -> NCic.obj -> string + map_unicode_to_tex:bool -> int -> #status -> NCic.obj -> string diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index cefb46e29..d84203aa4 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -128,7 +128,7 @@ let _ = in addDebugItem "dump aliases" (fun _ -> let status = script#grafite_status in - LexiconEngine.dump_aliases prerr_endline "" status); + GrafiteDisambiguate.dump_aliases prerr_endline "" status); (* FG: DEBUGGING addDebugItem "dump interpretations" (fun _ -> let status = script#lexicon_status in diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index b87c8523b..a95936c97 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -54,11 +54,11 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name = let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = let baseuri = status#baseuri in let status = - status#set_lstatus { status#lstatus with LexiconTypes.new_aliases = [] } in + status#set_disambiguate_db { status#disambiguate_db with GrafiteDisambiguate.new_aliases = [] } in let status = GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) in - let new_aliases = status#lstatus.LexiconTypes.new_aliases in + let new_aliases = status#disambiguate_db.GrafiteDisambiguate.new_aliases in let _,intermediate_states = List.fold_left (fun (status,acc) (k,value) -> @@ -75,7 +75,7 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = status,acc else let status = - LexiconEngine.set_proof_aliases status ~implicit_aliases:false + GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false GrafiteAst.WithPreferences [k,value] in status, (status ,Some (k,value))::acc diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index f7c9a7b9f..03dab4c4c 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -131,9 +131,9 @@ object (** load a sequent and render it into parent widget *) method nload_sequent: - #LexiconTypes.status -> NCic.metasenv -> NCic.substitution -> int -> unit + #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit - method load_nobject: #LexiconTypes.status -> NCic.obj -> unit + method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit end class type sequentsViewer = @@ -141,9 +141,9 @@ object method reset: unit method load_logo: unit method load_logo_with_qed: unit - method nload_sequents: #NTacStatus.tac_status -> unit + method nload_sequents: #GrafiteTypes.status -> unit method goto_sequent: - #LexiconTypes.status -> int -> unit (* to be called _after_ load_sequents *) + #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 280ade3ee..9990805ad 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -620,7 +620,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #LexiconTypes.status as 'status -> NCic.metasenv -> + 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -637,7 +637,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #LexiconTypes.status as 'status -> NCic.obj -> unit + 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -727,8 +727,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit - = fun (status : #NTacStatus.tac_status) -> + method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit + = fun (status : #GrafiteTypes.status) -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #LexiconTypes.status as 'status -> page:int -> + 'status. #ApplyTransformation.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with @@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #LexiconTypes.status as 'status -> int -> unit + method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b8a72a4d2..c1bf944c7 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -144,7 +144,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us in let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm - None status ctx menv subst (parsed_text,parsed_text_length, + status None ctx menv subst (parsed_text,parsed_text_length, NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in @@ -276,16 +276,16 @@ class script ~(source_view: GSourceView2.source_view) let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses current baseuri = - let empty_lstatus = new LexiconTypes.status in + let empty_lstatus = new GrafiteDisambiguate.status in (match current with Some current -> NCicLibrary.time_travel - ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus); + ((new GrafiteTypes.status current#baseuri)#set_disambiguate_db current#disambiguate_db); (* CSC: there is a known bug in invalidation; temporary fix here *) NCicEnvironment.invalidate () | None -> ()); let lexicon_status = empty_lstatus in - let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in + let grafite_status = (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in grafite_status in let read_include_paths file = diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index cf037531f..d1962c99d 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -29,7 +29,7 @@ open Printf open GrafiteTypes -exception AttemptToInsertAnAlias of LexiconTypes.status +exception AttemptToInsertAnAlias of GrafiteDisambiguate.status let slash_n_RE = Pcre.regexp "\\n" ;; @@ -122,10 +122,10 @@ let compile atstart options fname = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; activate_extraction baseuri fname ; - let lexicon_status = new LexiconTypes.status in + let lexicon_status = new GrafiteDisambiguate.status in atstart (); (* FG: do not invoke before loading the core notation script *) let grafite_status = - (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in + (new GrafiteTypes.status baseuri)#set_disambiguate_db lexicon_status#disambiguate_db in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = Unix.times () @@ -172,7 +172,7 @@ let compile atstart options fname = | [] -> grafite_status | (g,None)::_ -> g | (g,Some _)::_ -> - raise (AttemptToInsertAnAlias (g :> LexiconTypes.status)) + raise (AttemptToInsertAnAlias (g :> GrafiteDisambiguate.status)) in aux_for_dump print_cb grafite_status in