From f9f775a550264a8dc9ce7ea9a48b79892a122c3c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 4 Nov 2010 22:32:02 +0000 Subject: [PATCH] - further simplifications (??) of the status dependencies --- .../grafite_engine/grafiteEngine.ml | 16 ++-- .../components/grafite_engine/grafiteTypes.ml | 1 + .../grafite_engine/grafiteTypes.mli | 1 + .../grafite_engine/nCicCoercDeclaration.ml | 8 +- matita/components/grafite_parser/.depend | 3 - matita/components/grafite_parser/Makefile | 3 +- .../grafite_parser/grafiteParser.ml | 1 - matita/components/lexicon/.depend | 16 ++-- matita/components/lexicon/Makefile | 3 +- .../grafiteDisambiguate.ml | 74 +++++++++++++++---- .../grafiteDisambiguate.mli | 37 ++++++++-- matita/components/lexicon/lexiconSync.ml | 2 +- matita/components/lexicon/lexiconSync.mli | 2 +- matita/components/lexicon/lexiconTypes.ml | 56 -------------- matita/components/lexicon/lexiconTypes.mli | 46 ------------ matita/components/ng_tactics/nTacStatus.ml | 8 +- matita/components/ng_tactics/nTacStatus.mli | 4 +- matita/components/statuses.txt | 18 +++-- matita/matita/applyTransformation.ml | 6 ++ matita/matita/applyTransformation.mli | 10 ++- matita/matita/matita.ml | 2 +- matita/matita/matitaEngine.ml | 6 +- matita/matita/matitaGuiTypes.mli | 8 +- matita/matita/matitaMathView.ml | 12 +-- matita/matita/matitaScript.ml | 8 +- matita/matita/matitacLib.ml | 8 +- 26 files changed, 172 insertions(+), 187 deletions(-) rename matita/components/{grafite_parser => lexicon}/grafiteDisambiguate.ml (72%) rename matita/components/{grafite_parser => lexicon}/grafiteDisambiguate.mli (59%) delete mode 100644 matita/components/lexicon/lexiconTypes.ml delete mode 100644 matita/components/lexicon/lexiconTypes.mli 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/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/grafite_parser/grafiteDisambiguate.ml b/matita/components/lexicon/grafiteDisambiguate.ml similarity index 72% rename from matita/components/grafite_parser/grafiteDisambiguate.ml rename to matita/components/lexicon/grafiteDisambiguate.ml index 7511e02aa..5b27aba1b 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/lexicon/grafiteDisambiguate.ml @@ -25,19 +25,67 @@ (* $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 LexiconTypes.g_status + inherit Interpretations.g_status + method disambiguate_db: db end class status = object (self) - inherit LexiconTypes.status - method set_grafite_disambiguate_status + 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_lexicon_engine_status o) + = 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 @@ -120,15 +168,15 @@ let fix_instance item l = ;; -let disambiguate_nterm expty estatus context metasenv subst thing +let disambiguate_nterm estatus expty context metasenv subst thing = let diff, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term ~rdb:estatus - ~aliases:estatus#lstatus.LexiconTypes.aliases + ~aliases:estatus#disambiguate_db.aliases ~expty - ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) + ~universe:(Some estatus#disambiguate_db.multi_aliases) ~lookup_in_library:nlookup_in_library ~mk_choice:(ncic_mk_choice estatus) ~mk_implicit ~fix_instance @@ -136,8 +184,8 @@ let disambiguate_nterm expty estatus context metasenv subst thing ~context ~metasenv ~subst thing) in let estatus = - LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true - GrafiteAst.WithPreferences diff + set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences + diff in metasenv, subst, estatus, cic ;; @@ -215,12 +263,12 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ~mk_implicit ~fix_instance ~uri ~rdb:estatus - ~aliases:estatus#lstatus.LexiconTypes.aliases - ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) + ~aliases:estatus#disambiguate_db.aliases + ~universe:(Some estatus#disambiguate_db.multi_aliases) (text,prefix_len,obj)) in let estatus = - LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true - GrafiteAst.WithPreferences diff + 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/lexicon/grafiteDisambiguate.mli similarity index 59% rename from matita/components/grafite_parser/grafiteDisambiguate.mli rename to matita/components/lexicon/grafiteDisambiguate.mli index 6caf5301f..6b203cab4 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/lexicon/grafiteDisambiguate.mli @@ -23,18 +23,45 @@ * 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 : - NCic.term option -> - (#LexiconTypes.status as 'status) -> - NCic.context -> NCic.metasenv -> NCic.substitution -> + #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 : - #LexiconTypes.status as 'status -> - ?baseuri:string -> + #status as 'status -> ?baseuri:string -> (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> 'status * NCic.obj 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 -- 2.39.2