From c1f74c5fe5c69d3d830f6a58bc0e20c99d1fa8f7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 24 Nov 2005 18:26:49 +0000 Subject: [PATCH] Reshaped structure of ocaml/ libraries, matita changed accordingly. Verbose list of the changes: Modified Files: Makefile.in METAS/meta.helm-cic_disambiguation.src cic_disambiguation/.depend cic_disambiguation/Makefile cic_disambiguation/disambiguate.ml cic_disambiguation/disambiguate.mli cic_disambiguation/disambiguateChoices.ml cic_disambiguation/disambiguateTypes.ml cic_disambiguation/disambiguateTypes.mli extlib/.depend extlib/Makefile xml/xml.ml xml/xml.mli Added Files: METAS/meta.helm-acic_content.src METAS/meta.helm-cic_acic.src METAS/meta.helm-content_pres.src METAS/meta.helm-grafite.src METAS/meta.helm-hgdome.src acic_content/.cvsignore acic_content/.depend acic_content/Makefile acic_content/acic2astMatcher.ml acic_content/acic2astMatcher.mli acic_content/acic2content.ml acic_content/acic2content.mli acic_content/cicNotationEnv.ml acic_content/cicNotationEnv.mli acic_content/cicNotationPp.ml acic_content/cicNotationPp.mli acic_content/cicNotationPt.ml acic_content/cicNotationUtil.ml acic_content/cicNotationUtil.mli acic_content/content.ml acic_content/content.mli acic_content/content2cic.ml acic_content/content2cic.mli acic_content/contentPp.ml acic_content/contentPp.mli acic_content/termAcicContent.ml acic_content/termAcicContent.mli cic_acic/.cvsignore cic_acic/.depend cic_acic/Makefile cic_acic/cic2Xml.ml cic_acic/cic2Xml.mli cic_acic/cic2acic.ml cic_acic/cic2acic.mli cic_acic/doubleTypeInference.ml cic_acic/doubleTypeInference.mli cic_acic/eta_fixing.ml cic_acic/eta_fixing.mli content_pres/.cvsignore content_pres/.depend content_pres/Makefile content_pres/box.ml content_pres/box.mli content_pres/boxPp.ml content_pres/boxPp.mli content_pres/cicNotationLexer.ml content_pres/cicNotationLexer.mli content_pres/cicNotationParser.ml content_pres/cicNotationParser.mli content_pres/cicNotationPres.ml content_pres/cicNotationPres.mli content_pres/content2pres.ml content_pres/content2pres.mli content_pres/content2presMatcher.ml content_pres/content2presMatcher.mli content_pres/mpresentation.ml content_pres/mpresentation.mli content_pres/renderingAttrs.ml content_pres/renderingAttrs.mli content_pres/sequent2pres.ml content_pres/sequent2pres.mli content_pres/termContentPres.ml content_pres/termContentPres.mli content_pres/test_lexer.ml extlib/patternMatcher.ml extlib/patternMatcher.mli grafite/.cvsignore grafite/.depend grafite/Makefile grafite/cicNotation.ml grafite/cicNotation.mli grafite/grafiteAst.ml grafite/grafiteAstPp.ml grafite/grafiteAstPp.mli grafite/grafiteParser.ml grafite/grafiteParser.mli grafite/print_grammar.ml grafite/test_dep.ml grafite/test_parser.ml hgdome/.cvsignore hgdome/.depend hgdome/Makefile hgdome/domMisc.ml hgdome/domMisc.mli hgdome/xml2Gdome.ml hgdome/xml2Gdome.mli Removed Files: METAS/meta.helm-cic_notation.src METAS/meta.helm-cic_omdoc.src METAS/meta.helm-cic_transformations.src cic_disambiguation/disambiguatePp.ml cic_disambiguation/disambiguatePp.mli cic_notation/.cvsignore cic_notation/.depend cic_notation/Makefile cic_notation/TODO cic_notation/box.ml cic_notation/box.mli cic_notation/boxPp.ml cic_notation/boxPp.mli cic_notation/cicNotation.ml cic_notation/cicNotation.mli cic_notation/cicNotationEnv.ml cic_notation/cicNotationEnv.mli cic_notation/cicNotationFwd.ml cic_notation/cicNotationFwd.mli cic_notation/cicNotationLexer.ml cic_notation/cicNotationLexer.mli cic_notation/cicNotationMatcher.ml cic_notation/cicNotationMatcher.mli cic_notation/cicNotationParser.expanded.ml cic_notation/cicNotationParser.ml cic_notation/cicNotationParser.mli cic_notation/cicNotationPp.ml cic_notation/cicNotationPp.mli cic_notation/cicNotationPres.ml cic_notation/cicNotationPres.mli cic_notation/cicNotationPt.ml cic_notation/cicNotationRew.ml cic_notation/cicNotationRew.mli cic_notation/cicNotationTag.ml cic_notation/cicNotationTag.mli cic_notation/cicNotationUtil.ml cic_notation/cicNotationUtil.mli cic_notation/grafiteAst.ml cic_notation/grafiteAstPp.ml cic_notation/grafiteAstPp.mli cic_notation/grafiteParser.ml cic_notation/grafiteParser.mli cic_notation/mpresentation.ml cic_notation/mpresentation.mli cic_notation/print_grammar.ml cic_notation/renderingAttrs.ml cic_notation/renderingAttrs.mli cic_notation/test_dep.ml cic_notation/test_lexer.ml cic_notation/test_parser.conf.xml cic_notation/test_parser.ml cic_notation/doc/.cvsignore cic_notation/doc/Makefile cic_notation/doc/body.tex cic_notation/doc/infernce.sty cic_notation/doc/ligature.sty cic_notation/doc/main.tex cic_notation/doc/manfnt.sty cic_notation/doc/reserved.sty cic_notation/doc/samples.ma cic_notation/doc/semantic.sty cic_notation/doc/shrthand.sty cic_notation/doc/tdiagram.sty cic_omdoc/.cvsignore cic_omdoc/.depend cic_omdoc/Makefile cic_omdoc/cic2acic.ml cic_omdoc/cic2acic.mli cic_omdoc/cic2content.ml cic_omdoc/cic2content.mli cic_omdoc/content.ml cic_omdoc/content.mli cic_omdoc/content2cic.ml cic_omdoc/content2cic.mli cic_omdoc/contentPp.ml cic_omdoc/contentPp.mli cic_omdoc/doubleTypeInference.ml cic_omdoc/doubleTypeInference.mli cic_omdoc/eta_fixing.ml cic_omdoc/eta_fixing.mli cic_transformations/.cvsignore cic_transformations/.depend cic_transformations/Makefile cic_transformations/applyTransformation.ml cic_transformations/applyTransformation.mli cic_transformations/cic2Xml.ml cic_transformations/cic2Xml.mli cic_transformations/content2pres.ml cic_transformations/content2pres.mli cic_transformations/domMisc.ml cic_transformations/domMisc.mli cic_transformations/sequent2pres.ml cic_transformations/sequent2pres.mli cic_transformations/xml2Gdome.ml cic_transformations/xml2Gdome.mli --- helm/matita/.depend | 18 ++++--- helm/matita/Makefile.in | 7 ++- helm/matita/applyTransformation.ml | 70 ++++++++++++++++++++++++ helm/matita/applyTransformation.mli | 57 ++++++++++++++++++++ helm/matita/configure.ac | 14 ++--- helm/matita/disambiguatePp.ml | 83 +++++++++++++++++++++++++++++ helm/matita/disambiguatePp.mli | 34 ++++++++++++ helm/matita/matitaEngine.ml | 10 ++-- helm/matita/matitaMathView.ml | 6 +-- helm/matita/matitaScript.ml | 8 +-- helm/matita/matitaTypes.ml | 2 +- helm/matita/matitaTypes.mli | 2 +- 12 files changed, 278 insertions(+), 33 deletions(-) create mode 100644 helm/matita/applyTransformation.ml create mode 100644 helm/matita/applyTransformation.mli create mode 100644 helm/matita/disambiguatePp.ml create mode 100644 helm/matita/disambiguatePp.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index ff2e6c935..e10acb2be 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,3 +1,7 @@ +applyTransformation.cmo: applyTransformation.cmi +applyTransformation.cmx: applyTransformation.cmi +disambiguatePp.cmo: disambiguatePp.cmi +disambiguatePp.cmx: disambiguatePp.cmi dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \ @@ -58,10 +62,10 @@ matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - buildTimeConf.cmo matitaMathView.cmi + buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - buildTimeConf.cmx matitaMathView.cmi + buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \ @@ -74,14 +78,16 @@ matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ - matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi + matitaDisambiguator.cmi matitaDb.cmi disambiguatePp.cmi buildTimeConf.cmo \ + matitaScript.cmi matitaScript.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \ matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaEngine.cmx \ - matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx matitaScript.cmi + matitaDisambiguator.cmx matitaDb.cmx disambiguatePp.cmx buildTimeConf.cmx \ + matitaScript.cmi matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - matitaSync.cmi + disambiguatePp.cmi matitaSync.cmi matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - matitaSync.cmi + disambiguatePp.cmx matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi matitaDisambiguator.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 127f8a407..6d32e6eb7 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -42,7 +42,8 @@ CMOS = \ matitaMisc.cmo \ matitaDb.cmo \ matitamakeLib.cmo \ - matitaInit.cmo \ + matitaInit.cmo \ + disambiguatePp.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitaExcPp.cmo \ @@ -52,6 +53,7 @@ CMOS = \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ + applyTransformation.cmo \ matitaMathView.cmo \ matitaGui.cmo \ $(NULL) @@ -64,7 +66,8 @@ CCMOS = \ matitaMisc.cmo \ matitaDb.cmo \ matitamakeLib.cmo \ - matitaInit.cmo \ + matitaInit.cmo \ + disambiguatePp.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitaExcPp.cmo \ diff --git a/helm/matita/applyTransformation.ml b/helm/matita/applyTransformation.ml new file mode 100644 index 000000000..861fe922d --- /dev/null +++ b/helm/matita/applyTransformation.ml @@ -0,0 +1,70 @@ +(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 21/11/2003 *) +(* *) +(* *) +(***************************************************************************) + +let mpres_document pres_box = + Xml.add_xml_declaration (CicNotationPres.print_box pres_box) + +let mml_of_cic_sequent metasenv sequent = + let unsh_sequent,(asequent,ids_to_terms, + ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) + = + Cic2acic.asequent_of_sequent metasenv sequent + in + let content_sequent = Acic2content.map_sequent asequent in + let pres_sequent = + (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) + in + let xmlpres = mpres_document pres_sequent in + (Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres, + unsh_sequent, + (asequent, + (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) + +let mml_of_cic_object obj = + let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, + ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object obj + in + let content = + Acic2content.annobj2content ~ids_to_inner_sorts ~ids_to_inner_types annobj + in + let pres = Content2pres.content2pres ~ids_to_inner_sorts content in + let xmlpres = mpres_document pres in + let mathml = Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres in + (mathml,(annobj, + (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, + ids_to_inner_sorts,ids_to_inner_types))) + diff --git a/helm/matita/applyTransformation.mli b/helm/matita/applyTransformation.mli new file mode 100644 index 000000000..8e023aea6 --- /dev/null +++ b/helm/matita/applyTransformation.mli @@ -0,0 +1,57 @@ +(* Copyright (C) 2000-2002, 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://cs.unibo.it/helm/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 21/11/2003 *) +(* *) +(* *) +(***************************************************************************) + +val mml_of_cic_sequent: + Cic.metasenv -> (* metasenv *) + Cic.conjecture -> (* sequent *) + Gdome.document * (* Math ML *) + Cic.conjecture * (* unshared sequent *) + (Cic.annconjecture * (* annsequent *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *) + +val mml_of_cic_object: + Cic.obj -> (* object *) + Gdome.document * (* Math ML *) + (Cic.annobj * (* annobj *) + ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *) + (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *) + (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *) + (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *) + (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) + (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) + diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 3ed0cef34..21a02fbc4 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -33,15 +33,10 @@ else AC_MSG_ERROR(could not find camlp4o) fi FINDLIB_COMREQUIRES="\ -pcre \ -mysql \ -helm-registry \ -helm-extlib \ -helm-hmysql \ -helm-cic_notation \ -helm-tactics \ helm-cic_disambiguation \ -helm-cic_transformations \ +helm-grafite \ +helm-hgdome \ +helm-tactics \ " FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES" FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES" @@ -59,9 +54,6 @@ lablgtk2.glade \ lablgtkmathview \ lablgtksourceview \ helm-xmldiff \ -helm-cic_transformations \ -helm-tactics \ -helm-cic_disambiguation \ helm-paramodulation \ " for r in $FINDLIB_REQUIRES diff --git a/helm/matita/disambiguatePp.ml b/helm/matita/disambiguatePp.ml new file mode 100644 index 000000000..c3a48e409 --- /dev/null +++ b/helm/matita/disambiguatePp.ml @@ -0,0 +1,83 @@ +(* Copyright (C) 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/ + *) + +open DisambiguateTypes + +let parse_environment str = + let stream = Ulexing.from_utf8_string str in + let environment = ref Environment.empty in + let multiple_environment = ref Environment.empty in + try + while true do + let alias = + match GrafiteParser.parse_statement stream with + GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias))) + -> alias + | _ -> assert false in + let key,value = + (*CSC: Warning: this code should be factorized with the corresponding + code in MatitaEngine *) + match alias with + GrafiteAst.Ident_alias (id,uri) -> + Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) + | GrafiteAst.Symbol_alias (symb,instance,desc) -> + Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc + | GrafiteAst.Number_alias (instance,desc) -> + Num instance, + DisambiguateChoices.lookup_num_by_dsc desc + in + environment := Environment.add key value !environment; + multiple_environment := Environment.cons key value !multiple_environment; + done; + assert false + with End_of_file -> + !environment, !multiple_environment + +let alias_of_domain_and_codomain_items domain_item (dsc,_) = + match domain_item with + Id id -> GrafiteAst.Ident_alias (id, dsc) + | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc) + | Num i -> GrafiteAst.Number_alias (i, dsc) + +let aliases_of_environment env = + Environment.fold + (fun domain_item codomain_item acc -> + alias_of_domain_and_codomain_items domain_item codomain_item::acc + ) env [] + +let aliases_of_domain_and_codomain_items_list l = + List.fold_left + (fun acc (domain_item,codomain_item) -> + alias_of_domain_and_codomain_items domain_item codomain_item::acc + ) [] l + +let pp_environment env = + let aliases = aliases_of_environment env in + let strings = + List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases + in + String.concat "\n" (List.sort compare strings) diff --git a/helm/matita/disambiguatePp.mli b/helm/matita/disambiguatePp.mli new file mode 100644 index 000000000..69b6e8451 --- /dev/null +++ b/helm/matita/disambiguatePp.mli @@ -0,0 +1,34 @@ +(* Copyright (C) 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/ + *) + +val parse_environment: + string -> + DisambiguateTypes.environment * DisambiguateTypes.multiple_environment + +val aliases_of_domain_and_codomain_items_list: + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> + GrafiteAst.alias_spec list + +val pp_environment: DisambiguateTypes.environment -> string diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index bf39a1cac..b62dd23de 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -676,11 +676,11 @@ let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; let disambiguate_obj status obj = let uri = match obj with - GrafiteAst.Inductive (_,(name,_,_,_)::_) - | GrafiteAst.Record (_,name,_,_) -> + | CicNotationPt.Inductive (_,(name,_,_,_)::_) + | CicNotationPt.Record (_,name,_,_) -> Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind")) - | GrafiteAst.Inductive _ -> assert false - | GrafiteAst.Theorem _ -> None in + | CicNotationPt.Inductive _ -> assert false + | CicNotationPt.Theorem _ -> None in let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) @@ -850,7 +850,7 @@ let eval_command opts status cmd = if opts.do_heavy_checks then begin let dbd = MatitaDb.instance () in - let similar = MetadataQuery.match_term ~dbd ty in + let similar = Whelp.match_term ~dbd ty in let similar_len = List.length similar in if similar_len> 30 then (MatitaLog.message diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 507837c15..7a54049a8 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -328,9 +328,9 @@ object (self) in let _, _, _, annterm = acic_sequent in let ast, ids_to_uris = - CicNotationRew.ast_of_acic ids_to_inner_sorts annterm + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in - let pped_ast = CicNotationRew.pp_ast ast in + let pped_ast = TermContentPres.pp_ast ast in let markup = CicNotationPres.render ids_to_uris pped_ast in BoxPp.render_to_string text_width markup in @@ -613,7 +613,7 @@ let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = - [ `Ast of DisambiguateTypes.term + [ `Ast of CicNotationPt.term | `Cic of Cic.term * Cic.metasenv | `String of string ] diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 4413f9b8a..3fa4e93e7 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -237,7 +237,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = (* WHELP's stuff *) | TA.WMatch (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.match_term ~dbd term in + let l = Whelp.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." (HExtlib.trim_blanks unparsed_text) @@ -247,12 +247,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate_macro_term term status user_goal in - let l = MQ.instance ~dbd term in + let l = Whelp.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length | TA.WLocate (loc, s) -> - let l = MQ.locate ~dbd s in + let l = Whelp.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length @@ -263,7 +263,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None | _ -> failwith "Not a MutInd" in - let l = MQ.elim ~dbd uri in + let l = Whelp.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], parsed_text_length diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 8bd32bb23..8ee007d47 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -62,7 +62,7 @@ type option_value = type options = option_value StringMap.t let no_options = StringMap.empty -type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command +type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command type moo = ast_command list * GrafiteAst.metadata list type status = { diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index e54fe5c7e..a558d10e3 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -52,7 +52,7 @@ type option_value = type options = option_value StringMap.t val no_options : 'a StringMap.t -type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command +type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command type moo = ast_command list * GrafiteAst.metadata list (** *) type status = { -- 2.39.2