From 4db221ee87ba30f63db0ea32c98858041e8e6213 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Feb 2007 19:36:05 +0000 Subject: [PATCH] - Procedural: moved in a directory on its own - ApplyTransofrmation: now handles inline macro expansion - GrafiteParser MatitaEngine MatitacLib: added a callback in each - tests/letrecand.ma: changed baseuri --- .../METAS/meta.helm-acic_procedural.src | 4 ++ helm/software/components/Makefile | 1 + .../components/acic_procedural/.depend | 10 +++ .../components/acic_procedural/.depend.opt | 10 +++ .../components/acic_procedural/Makefile | 14 ++++ .../acic2Procedural.ml | 0 .../acic2Procedural.mli | 0 .../cicClassify.ml | 0 .../cicClassify.mli | 0 .../proceduralConversion.ml | 0 .../proceduralConversion.mli | 0 .../proceduralTypes.ml | 0 .../proceduralTypes.mli | 0 helm/software/components/content_pres/.depend | 12 ---- .../components/content_pres/.depend.opt | 12 ---- .../software/components/content_pres/Makefile | 5 -- .../software/components/content_pres/objPp.ml | 65 ------------------- .../components/content_pres/objPp.mli | 28 -------- .../grafite_parser/grafiteParser.ml | 7 +- .../grafite_parser/grafiteParser.mli | 3 + .../components/metadata/metadataDeps.ml | 28 ++++++++ .../components/metadata/metadataDeps.mli | 3 + helm/software/matita/.depend | 20 ++++-- helm/software/matita/.depend.opt | 20 ++++-- helm/software/matita/Makefile | 4 +- helm/software/matita/applyTransformation.ml | 57 ++++++++++++++++ helm/software/matita/applyTransformation.mli | 7 ++ helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaEngine.ml | 5 ++ helm/software/matita/matitaEngine.mli | 2 + helm/software/matita/matitaScript.ml | 50 +------------- helm/software/matita/matitacLib.ml | 14 +++- helm/software/matita/matitacLib.mli | 3 + helm/software/matita/tests/letrecand.ma | 4 +- 34 files changed, 200 insertions(+), 190 deletions(-) create mode 100644 helm/software/components/METAS/meta.helm-acic_procedural.src create mode 100644 helm/software/components/acic_procedural/.depend create mode 100644 helm/software/components/acic_procedural/.depend.opt create mode 100644 helm/software/components/acic_procedural/Makefile rename helm/software/components/{content_pres => acic_procedural}/acic2Procedural.ml (100%) rename helm/software/components/{content_pres => acic_procedural}/acic2Procedural.mli (100%) rename helm/software/components/{content_pres => acic_procedural}/cicClassify.ml (100%) rename helm/software/components/{content_pres => acic_procedural}/cicClassify.mli (100%) rename helm/software/components/{content_pres => acic_procedural}/proceduralConversion.ml (100%) rename helm/software/components/{content_pres => acic_procedural}/proceduralConversion.mli (100%) rename helm/software/components/{content_pres => acic_procedural}/proceduralTypes.ml (100%) rename helm/software/components/{content_pres => acic_procedural}/proceduralTypes.mli (100%) delete mode 100644 helm/software/components/content_pres/objPp.ml delete mode 100644 helm/software/components/content_pres/objPp.mli diff --git a/helm/software/components/METAS/meta.helm-acic_procedural.src b/helm/software/components/METAS/meta.helm-acic_procedural.src new file mode 100644 index 000000000..e91f1f7d8 --- /dev/null +++ b/helm/software/components/METAS/meta.helm-acic_procedural.src @@ -0,0 +1,4 @@ +requires="helm-cic_proof_checking helm-acic_content helm-grafite" +version="0.0.1" +archive(byte)="acic_procedural.cma" +archive(native)="acic_procedural.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index a700970af..9f42d0dad 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -24,6 +24,7 @@ MODULES = \ library \ acic_content \ grafite \ + acic_procedural \ content_pres \ cic_unification \ whelp \ diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend new file mode 100644 index 000000000..5f1cd6590 --- /dev/null +++ b/helm/software/components/acic_procedural/.depend @@ -0,0 +1,10 @@ +cicClassify.cmo: cicClassify.cmi +cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + cicClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + cicClassify.cmx acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt new file mode 100644 index 000000000..5f1cd6590 --- /dev/null +++ b/helm/software/components/acic_procedural/.depend.opt @@ -0,0 +1,10 @@ +cicClassify.cmo: cicClassify.cmi +cicClassify.cmx: cicClassify.cmi +proceduralConversion.cmo: proceduralConversion.cmi +proceduralConversion.cmx: proceduralConversion.cmi +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ + cicClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ + cicClassify.cmx acic2Procedural.cmi diff --git a/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile new file mode 100644 index 000000000..3435f01d0 --- /dev/null +++ b/helm/software/components/acic_procedural/Makefile @@ -0,0 +1,14 @@ +PACKAGE = acic_procedural +PREDICATES = + +INTERFACE_FILES = \ + cicClassify.mli \ + proceduralConversion.mli \ + proceduralTypes.mli \ + acic2Procedural.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) + +include ../../Makefile.defs +include ../Makefile.common diff --git a/helm/software/components/content_pres/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml similarity index 100% rename from helm/software/components/content_pres/acic2Procedural.ml rename to helm/software/components/acic_procedural/acic2Procedural.ml diff --git a/helm/software/components/content_pres/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli similarity index 100% rename from helm/software/components/content_pres/acic2Procedural.mli rename to helm/software/components/acic_procedural/acic2Procedural.mli diff --git a/helm/software/components/content_pres/cicClassify.ml b/helm/software/components/acic_procedural/cicClassify.ml similarity index 100% rename from helm/software/components/content_pres/cicClassify.ml rename to helm/software/components/acic_procedural/cicClassify.ml diff --git a/helm/software/components/content_pres/cicClassify.mli b/helm/software/components/acic_procedural/cicClassify.mli similarity index 100% rename from helm/software/components/content_pres/cicClassify.mli rename to helm/software/components/acic_procedural/cicClassify.mli diff --git a/helm/software/components/content_pres/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml similarity index 100% rename from helm/software/components/content_pres/proceduralConversion.ml rename to helm/software/components/acic_procedural/proceduralConversion.ml diff --git a/helm/software/components/content_pres/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli similarity index 100% rename from helm/software/components/content_pres/proceduralConversion.mli rename to helm/software/components/acic_procedural/proceduralConversion.mli diff --git a/helm/software/components/content_pres/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml similarity index 100% rename from helm/software/components/content_pres/proceduralTypes.ml rename to helm/software/components/acic_procedural/proceduralTypes.ml diff --git a/helm/software/components/content_pres/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli similarity index 100% rename from helm/software/components/content_pres/proceduralTypes.mli rename to helm/software/components/acic_procedural/proceduralTypes.mli diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 78cde4140..2c5d65140 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -30,18 +30,6 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi -objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \ - acic2Procedural.cmi objPp.cmi -objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \ - acic2Procedural.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt index 78cde4140..2c5d65140 100644 --- a/helm/software/components/content_pres/.depend.opt +++ b/helm/software/components/content_pres/.depend.opt @@ -30,18 +30,6 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi -proceduralConversion.cmo: proceduralConversion.cmi -proceduralConversion.cmx: proceduralConversion.cmi -proceduralTypes.cmo: proceduralTypes.cmi -proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi -objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \ - acic2Procedural.cmi objPp.cmi -objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \ - acic2Procedural.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/helm/software/components/content_pres/Makefile b/helm/software/components/content_pres/Makefile index 9c627cb23..fb6d0fe46 100644 --- a/helm/software/components/content_pres/Makefile +++ b/helm/software/components/content_pres/Makefile @@ -12,11 +12,6 @@ INTERFACE_FILES = \ cicNotationPres.mli \ boxPp.mli \ content2pres.mli \ - cicClassify.mli \ - proceduralConversion.mli \ - proceduralTypes.mli \ - acic2Procedural.mli \ - objPp.mli \ sequent2pres.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml deleted file mode 100644 index f83b18635..000000000 --- a/helm/software/components/content_pres/objPp.ml +++ /dev/null @@ -1,65 +0,0 @@ -(* 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/ - *) - -let remove_closed_substs s = - Pcre.replace ~pat:"{...}" ~templ:"" s - -let term2pres n ids_to_inner_sorts annterm = - let ast, ids_to_uris = - TermAcicContent.ast_of_acic ids_to_inner_sorts annterm - in - let bobj = - CicNotationPres.box_of_mpres ( - CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast) - ) - in - let render = function _::x::_ -> x | _ -> assert false in - let mpres = CicNotationPres.mpres_of_box bobj in - let s = BoxPp.render_to_string render n mpres in - remove_closed_substs s - -let obj_to_string n style prefix obj = - let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = - try Cic2acic.acic_object_of_cic_object obj - with e -> - let msg = "Cic2ACic: " ^ Printexc.to_string e in - failwith msg - in - match style with - | GrafiteAst.Declarative -> - let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in - let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in - remove_closed_substs ("\n\n" ^ - BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) - ) - | GrafiteAst.Procedural depth -> - let term_pp = term2pres (n - 8) ids_to_inner_sorts in - let lazy_term_pp = term_pp in - let obj_pp = CicNotationPp.pp_obj term_pp in - let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in - let script = Acic2Procedural.acic2procedural - ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in - "\n\n" ^ String.concat "" (List.map aux script) diff --git a/helm/software/components/content_pres/objPp.mli b/helm/software/components/content_pres/objPp.mli deleted file mode 100644 index de320bf14..000000000 --- a/helm/software/components/content_pres/objPp.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* 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/ - *) - -(* columns, rendering style, name prefix, object *) -val obj_to_string: - int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 9a0cc9f43..f3dd386a9 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -60,6 +60,10 @@ type by_continuation = | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term +let out = ref ignore + +let set_callback f = out := f + EXTEND GLOBAL: term statement; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; @@ -674,7 +678,8 @@ EXTEND (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> - let status = LexiconEngine.eval_command status scom in + !out scom; + let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file ] diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli index 6d941d5db..f38f0e5dc 100644 --- a/helm/software/components/grafite_parser/grafiteParser.mli +++ b/helm/software/components/grafite_parser/grafiteParser.mli @@ -38,6 +38,9 @@ type statement = LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option +(* this callback is called on every lexicon command *) +val set_callback: (LexiconAst.command -> unit) -> unit + val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) val statement: statement Grammar.Entry.e diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml index f2b1d0496..330984350 100644 --- a/helm/software/components/metadata/metadataDeps.ml +++ b/helm/software/components/metadata/metadataDeps.ml @@ -101,6 +101,34 @@ let topological_sort ~dbd uris = Topo.topological_sort uris (fun uri -> fst (List.split (direct_deps ~dbd uri))) +let sorted_uris_of_baseuri ~dbd baseuri = + let sql_pat = + Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" baseuri ^ "%" + in + let query = + Printf.sprintf + ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ + "SELECT source FROM %s WHERE source LIKE \"%s\"") + (MetadataTypes.name_tbl ()) sql_pat + MetadataTypes.library_name_tbl sql_pat + in + let result = HMysql.exec dbd query in + let map cols = match cols.(0) with + | Some s -> UriManager.uri_of_string s + | _ -> assert false + in + let uris = HMysql.map result map in + let sorted_uris = topological_sort ~dbd uris in + let filter_map uri = + let s = + Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" + (UriManager.string_of_uri uri) + in + try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None + with Not_found -> Some (UriManager.uri_of_string s) + in + HExtlib.filter_map filter_map sorted_uris + module DepGraph = struct module UriTbl = UriManager.UriHashtbl diff --git a/helm/software/components/metadata/metadataDeps.mli b/helm/software/components/metadata/metadataDeps.mli index f5a6ac22e..4def88d9e 100644 --- a/helm/software/components/metadata/metadataDeps.mli +++ b/helm/software/components/metadata/metadataDeps.mli @@ -38,6 +38,9 @@ val inverse_deps: val topological_sort: dbd:HMysql.dbd -> UriManager.uri list -> UriManager.uri list +val sorted_uris_of_baseuri: + dbd:HMysql.dbd -> string -> UriManager.uri list + (** Representation of a (lazy) dependency graph. * Imperative data structure. *) module DepGraph: diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index 8dd26ce54..8b943bb3d 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -11,13 +11,15 @@ lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi + matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \ + applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi + matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi gragrep.cmi + matitacLib.cmi matitaWiki.cmo gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -51,9 +53,11 @@ matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \ + applyTransformation.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmi matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ @@ -66,6 +70,10 @@ matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi +matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmi applyTransformation.cmi +matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt index 7860c2d16..b0119369b 100644 --- a/helm/software/matita/.depend.opt +++ b/helm/software/matita/.depend.opt @@ -11,13 +11,15 @@ lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ - matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi + matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \ + applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ - matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi + matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitacLib.cmi matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \ - matitacLib.cmi gragrep.cmi + matitacLib.cmi matitaWiki.cmx gragrep.cmi matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ - matitacLib.cmx gragrep.cmx + matitacLib.cmx matitaWiki.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -51,9 +53,11 @@ matitaMathView.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \ + applyTransformation.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmi matitaprover.cmi matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ @@ -66,6 +70,10 @@ matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi +matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmi applyTransformation.cmi +matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaGtkMisc.cmi: matitaGeneratedGui.cmx matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index ed5ebb320..1b73fe2da 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -34,9 +34,9 @@ CMOS = \ matitaInit.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ + applyTransformation.cmo \ matitacLib.cmo \ matitaprover.cmo \ - applyTransformation.cmo \ matitaGtkMisc.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ @@ -52,8 +52,8 @@ CCMOS = \ matitaInit.cmo \ matitaExcPp.cmo \ matitaEngine.cmo \ - matitacLib.cmo \ applyTransformation.cmo \ + matitacLib.cmo \ matitaWiki.cmo \ matitaprover.cmo \ $(NULL) diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index f27da2caa..0678887ce 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -97,3 +97,60 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let txt_of_cic_term size metasenv context t = let fake_sequent = (-1,context,t) in txt_of_cic_sequent_conclusion size metasenv fake_sequent + +(****************************************************************************) +(* txt_of_cic_object: IMPROVE ME *) + +let remove_closed_substs s = + Pcre.replace ~pat:"{...}" ~templ:"" s + +let term2pres n ids_to_inner_sorts annterm = + let ast, ids_to_uris = + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + in + let bobj = + CicNotationPres.box_of_mpres ( + CicNotationPres.render ~prec:90 ids_to_uris + (TermContentPres.pp_ast ast) + ) + in + let render = function _::x::_ -> x | _ -> assert false in + let mpres = CicNotationPres.mpres_of_box bobj in + let s = BoxPp.render_to_string render n mpres in + remove_closed_substs s + +let txt_of_cic_object n style prefix obj = + let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = + try Cic2acic.acic_object_of_cic_object obj + with e -> + let msg = "Cic2ACic: " ^ Printexc.to_string e in + failwith msg + in + match style with + | GrafiteAst.Declarative -> + let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in + let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in + remove_closed_substs ("\n\n" ^ + BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) + ) + | GrafiteAst.Procedural depth -> + let term_pp = term2pres (n - 8) ids_to_inner_sorts in + let lazy_term_pp = term_pp in + let obj_pp = CicNotationPp.pp_obj term_pp in + let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in + let script = Acic2Procedural.acic2procedural + ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in + "\n\n" ^ String.concat "" (List.map aux script) + +let txt_of_inline_macro style suri prefix = + let dbd = LibraryDb.instance () in + let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in + let map uri = + try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *) + (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) + with + | e -> + Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" + (UriManager.string_of_uri uri) (Printexc.to_string e) + in + String.concat "\n\n" (List.map map sorted_uris) diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 218a92ca9..8e0b19361 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -62,3 +62,10 @@ val txt_of_cic_sequent: val txt_of_cic_sequent_conclusion: int -> Cic.metasenv -> Cic.conjecture -> string +(* columns, rendering style, name prefix, object *) +val txt_of_cic_object: + int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string + +(* presentation_style, uri or baseuri, name prefix *) +val txt_of_inline_macro: + GrafiteAst.presentation_style -> string -> string -> string diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 46926ea9b..5717b710a 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -173,7 +173,7 @@ let _ = addDebugItem "Print current proof (natural language) to stderr" (fun _ -> prerr_endline - (ObjPp.obj_to_string 120 GrafiteAst.Declarative "" + (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative "" (match (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 9778f0900..191c60bb1 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -100,6 +100,10 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status exception TryingToAdd of string +let out = ref ignore + +let set_callback f = out := f + let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) ?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb @@ -122,6 +126,7 @@ let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) loop lexicon_status grafite_status (((grafite_status,lexicon_status),None)::statuses) | GrafiteParser.LSome ast -> + !out ast; cb grafite_status ast; let new_statuses = eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index 71bfff0b8..83b549ec4 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -61,3 +61,5 @@ val eval_from_stream : (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option ) list +(* this callback is called on every grafite command *) +val set_callback: (GrafiteParser.ast_statement -> unit) -> unit diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index f124bd5c9..8ab94d979 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -289,54 +289,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], "", parsed_text_length | TA.Inline (_,style,suri,prefix) -> - let dbd = LibraryDb.instance () in - let uris = - let sql_pat = - (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in - let query = - sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE source LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat in - let result = HMysql.exec dbd query in - HMysql.map result - (function cols -> - match cols.(0) with - Some s -> UriManager.uri_of_string s - | _ -> assert false) - in -prerr_endline "Inizio sorting"; - let sorted_uris = MetadataDeps.topological_sort ~dbd uris in -prerr_endline "Fine sorting"; - let sorted_uris_without_xpointer = - HExtlib.filter_map - (function uri -> - let s = - Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:"" - (UriManager.string_of_uri uri) in - try - ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); - None - with - Not_found -> - Some (UriManager.uri_of_string s) - ) sorted_uris - in - let declarative = - String.concat "\n\n" - (List.map - (fun uri -> -prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); - try - ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *) - (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) - with - | e (* BRRRRRRRRR *) -> - Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" - (UriManager.string_of_uri uri) (Printexc.to_string e) - ) sorted_uris_without_xpointer) - in - [],declarative,String.length parsed_text + let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index ba9af1302..52ad776e7 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -31,6 +31,10 @@ open GrafiteTypes exception AttemptToInsertAnAlias +let out = ref ignore + +let set_callback f = out := f + let pp_ast_statement = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) @@ -126,8 +130,14 @@ let rec interactive_loop () = "matita.includes")) with | GrafiteEngine.Drop -> pp_ocaml_mode () - | GrafiteEngine.Macro (floc,_) -> - let x, y = HExtlib.loc_of_floc floc in + | GrafiteEngine.Macro (floc, f) -> + begin match snd (f []) with + | GrafiteAst.Inline (_, style, suri, prefix) -> + let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + !out str + | _ -> () + end; + let x, y = HExtlib.loc_of_floc floc in HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); interactive_loop () diff --git a/helm/software/matita/matitacLib.mli b/helm/software/matita/matitacLib.mli index 636c51d57..5e8a2635b 100644 --- a/helm/software/matita/matitacLib.mli +++ b/helm/software/matita/matitacLib.mli @@ -35,3 +35,6 @@ val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit otherwise it performs the clean-up without exiting *) val clean_exit : int option -> unit + +(* this callback is called on the expansion of every inline macro *) +val set_callback: (string -> unit) -> unit diff --git a/helm/software/matita/tests/letrecand.ma b/helm/software/matita/tests/letrecand.ma index 017c2ae89..d9dfec329 100644 --- a/helm/software/matita/tests/letrecand.ma +++ b/helm/software/matita/tests/letrecand.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/letrecand". +set "baseuri" "cic:/matita/tests/letrecand". include "nat/nat.ma". @@ -71,4 +71,4 @@ qed. lemma test_dispari2: dispari2 (S O). simplify. constructor 1. -qed. \ No newline at end of file +qed. -- 2.39.2