From 0d2bfb98d8343b4e6cefdb506a813b7cb5749630 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 26 Oct 2010 12:58:39 +0000 Subject: [PATCH] cic module removed (RIP) --- matita/components/METAS/meta.helm-cic.src | 5 -- matita/components/METAS/meta.helm-extlib.src | 2 +- matita/components/METAS/meta.helm-grafite.src | 2 +- .../METAS/meta.helm-grafite_engine.src | 2 +- matita/components/METAS/meta.helm-library.src | 2 +- .../components/METAS/meta.helm-ng_kernel.src | 2 +- .../METAS/meta.helm-ng_paramodulation.src | 2 +- matita/components/Makefile | 1 - .../components/binaries/test_lexer/Makefile | 33 +++++++++++ .../test_lexer}/test_lexer.ml | 0 .../components/binaries/test_parser/Makefile | 53 ++++++++++++++++++ .../test_parser}/print_grammar.ml | 0 .../test_parser}/test_dep.ml | 0 .../test_parser}/test_parser.ml | 0 matita/components/cic/.depend | 0 matita/components/cic/.depend.opt | 8 --- matita/components/cic/Makefile | 11 ---- matita/components/cic/cic.ml | 55 ------------------- matita/components/content/interpretations.ml | 6 +- matita/components/content/interpretations.mli | 2 + matita/components/content/notationPp.ml | 15 +---- matita/components/content/notationPt.ml | 2 +- matita/components/content/notationUtil.ml | 13 ----- matita/components/content/notationUtil.mli | 3 - matita/components/content_pres/Makefile | 11 +--- .../content_pres/cicNotationPres.mli | 5 +- matita/components/grafite_parser/Makefile | 19 +------ .../grafite_parser/grafiteParser.ml | 30 +--------- .../ng_disambiguation/nCicDisambiguate.ml | 19 ++----- matita/components/ng_kernel/nCic.ml | 2 +- matita/components/ng_kernel/nCicPp.ml | 13 +++-- matita/components/ng_kernel/nCicPp.mli | 2 + matita/matita/library/depends | 14 ++--- matita/matita/matitadep.ml | 12 ++-- 34 files changed, 138 insertions(+), 208 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-cic.src create mode 100644 matita/components/binaries/test_lexer/Makefile rename matita/components/{content_pres => binaries/test_lexer}/test_lexer.ml (100%) create mode 100644 matita/components/binaries/test_parser/Makefile rename matita/components/{grafite_parser => binaries/test_parser}/print_grammar.ml (100%) rename matita/components/{grafite_parser => binaries/test_parser}/test_dep.ml (100%) rename matita/components/{grafite_parser => binaries/test_parser}/test_parser.ml (100%) delete mode 100644 matita/components/cic/.depend delete mode 100644 matita/components/cic/.depend.opt delete mode 100644 matita/components/cic/Makefile delete mode 100644 matita/components/cic/cic.ml diff --git a/matita/components/METAS/meta.helm-cic.src b/matita/components/METAS/meta.helm-cic.src deleted file mode 100644 index 525cc9c22..000000000 --- a/matita/components/METAS/meta.helm-cic.src +++ /dev/null @@ -1,5 +0,0 @@ -requires="helm-urimanager helm-xml expat" -version="0.0.1" -archive(byte)="cic.cma" -archive(native)="cic.cmxa" -linkopts="" diff --git a/matita/components/METAS/meta.helm-extlib.src b/matita/components/METAS/meta.helm-extlib.src index 2002fccf1..a355cb2da 100644 --- a/matita/components/METAS/meta.helm-extlib.src +++ b/matita/components/METAS/meta.helm-extlib.src @@ -1,4 +1,4 @@ -requires="unix camlp5.gramlib" +requires="str unix camlp5.gramlib" version="0.0.1" archive(byte)="extlib.cma" archive(native)="extlib.cmxa" diff --git a/matita/components/METAS/meta.helm-grafite.src b/matita/components/METAS/meta.helm-grafite.src index f45beff90..f86ae35e7 100644 --- a/matita/components/METAS/meta.helm-grafite.src +++ b/matita/components/METAS/meta.helm-grafite.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-content helm-ng_kernel" +requires="helm-content helm-ng_kernel" version="0.0.1" archive(byte)="grafite.cma" archive(native)="grafite.cmxa" diff --git a/matita/components/METAS/meta.helm-grafite_engine.src b/matita/components/METAS/meta.helm-grafite_engine.src index 469912fa4..2362f2e6c 100644 --- a/matita/components/METAS/meta.helm-grafite_engine.src +++ b/matita/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-cic helm-ng_tactics helm-ng_library" +requires="helm-library helm-grafite helm-ng_tactics helm-ng_library" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/matita/components/METAS/meta.helm-library.src b/matita/components/METAS/meta.helm-library.src index ee7026024..2fd9b2917 100644 --- a/matita/components/METAS/meta.helm-library.src +++ b/matita/components/METAS/meta.helm-library.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-getter" +requires="helm-getter" version="0.0.1" archive(byte)="library.cma" archive(native)="library.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src index 7e913b61d..df165a210 100644 --- a/matita/components/METAS/meta.helm-ng_kernel.src +++ b/matita/components/METAS/meta.helm-ng_kernel.src @@ -1,4 +1,4 @@ -requires="helm-cic" +requires="" version="0.0.1" archive(byte)="ng_kernel.cma" archive(native)="ng_kernel.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_paramodulation.src b/matita/components/METAS/meta.helm-ng_paramodulation.src index ed8772dea..e09fa226a 100644 --- a/matita/components/METAS/meta.helm-ng_paramodulation.src +++ b/matita/components/METAS/meta.helm-ng_paramodulation.src @@ -1,4 +1,4 @@ -requires="helm-cic helm-ng_refiner" +requires="helm-ng_refiner" version="0.0.1" archive(byte)="ng_paramodulation.cma" archive(native)="ng_paramodulation.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index d536ec37b..3f3b5dea9 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -14,7 +14,6 @@ MODULES = \ urimanager \ logger \ getter \ - cic \ library \ ng_kernel \ content \ diff --git a/matita/components/binaries/test_lexer/Makefile b/matita/components/binaries/test_lexer/Makefile new file mode 100644 index 000000000..ef32e9e2d --- /dev/null +++ b/matita/components/binaries/test_lexer/Makefile @@ -0,0 +1,33 @@ +H=@ + +REQUIRES = helm-content_pres + +INTERFACE_FILES = +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = \ + test_lexer test_lexer.opt + +all: test_lexer + $(H)echo -n +opt: test_lexer.opt + $(H)echo -n + +test_lexer: test_lexer.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +test_lexer.opt: test_lexer.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +clean: + $(H)rm -f *.cm[iox] *.a *.o + $(H)rm -f test_lexer test_lexer.opt + +depend: +depend.opt: + +include ../../../Makefile.defs diff --git a/matita/components/content_pres/test_lexer.ml b/matita/components/binaries/test_lexer/test_lexer.ml similarity index 100% rename from matita/components/content_pres/test_lexer.ml rename to matita/components/binaries/test_lexer/test_lexer.ml diff --git a/matita/components/binaries/test_parser/Makefile b/matita/components/binaries/test_parser/Makefile new file mode 100644 index 000000000..7d5981a57 --- /dev/null +++ b/matita/components/binaries/test_parser/Makefile @@ -0,0 +1,53 @@ +H=@ + +REQUIRES = str helm-grafite_parser + +INTERFACE_FILES = +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = \ + test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt + +all: test_parser test_dep print_grammar + $(H)echo -n +opt: test_parser.opt test_dep.opt print_grammar.opt + $(H)echo -n + +test_parser: test_parser.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +test_parser.opt: test_parser.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +test_dep: test_dep.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +test_dep.opt: test_dep.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +print_grammar: print_grammar.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +print_grammar.opt: print_grammar.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $< + +clean: + $(H)rm -f *.cm[iox] *.a *.o + $(H)rm -f test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt + +depend: +depend.opt: + +include ../../../Makefile.defs diff --git a/matita/components/grafite_parser/print_grammar.ml b/matita/components/binaries/test_parser/print_grammar.ml similarity index 100% rename from matita/components/grafite_parser/print_grammar.ml rename to matita/components/binaries/test_parser/print_grammar.ml diff --git a/matita/components/grafite_parser/test_dep.ml b/matita/components/binaries/test_parser/test_dep.ml similarity index 100% rename from matita/components/grafite_parser/test_dep.ml rename to matita/components/binaries/test_parser/test_dep.ml diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/binaries/test_parser/test_parser.ml similarity index 100% rename from matita/components/grafite_parser/test_parser.ml rename to matita/components/binaries/test_parser/test_parser.ml diff --git a/matita/components/cic/.depend b/matita/components/cic/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/matita/components/cic/.depend.opt b/matita/components/cic/.depend.opt deleted file mode 100644 index 34fcd83c2..000000000 --- a/matita/components/cic/.depend.opt +++ /dev/null @@ -1,8 +0,0 @@ -cicUniv.cmi: -cicPp.cmi: cic.cmx -cic.cmo: cicUniv.cmi -cic.cmx: cicUniv.cmx -cicUniv.cmo: cicUniv.cmi -cicUniv.cmx: cicUniv.cmi -cicPp.cmo: cic.cmx cicPp.cmi -cicPp.cmx: cic.cmx cicPp.cmi diff --git a/matita/components/cic/Makefile b/matita/components/cic/Makefile deleted file mode 100644 index 09b39139b..000000000 --- a/matita/components/cic/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -PACKAGE = cic -PREDICATES = - -INTERFACE_FILES = -IMPLEMENTATION_FILES = \ - cic.ml $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi -EXTRA_OBJECTS_TO_CLEAN = - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/cic/cic.ml b/matita/components/cic/cic.ml deleted file mode 100644 index 8b1d379b7..000000000 --- a/matita/components/cic/cic.ml +++ /dev/null @@ -1,55 +0,0 @@ -(* Copyright (C) 2000, 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 *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* This module defines the internal representation of the objects (variables,*) -(* blocks of (co)inductive definitions and constants) and the terms of cic *) -(* *) -(*****************************************************************************) - -(* $Id$ *) - -type id = string (* the abstract type of the (annotated) node identifiers *) - -type name = - | Name of string - | Anonymous - -type object_flavour = - [ `Definition - | `MutualDefinition - | `Fact - | `Lemma - | `Remark - | `Theorem - | `Variant - | `Axiom - ] diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index 1f16df421..8059eeaae 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -36,9 +36,11 @@ type interpretation_id = int let idref id t = Ast.AttributedTerm (`IdRef id, t) +type cic_id = string + type term_info = - { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; - uri: (Cic.id, UriManager.uri) Hashtbl.t; + { sort: (cic_id, Ast.sort_kind) Hashtbl.t; + uri: (cic_id, UriManager.uri) Hashtbl.t; } (* persistent state *) diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli index 222a340f4..10a2f093e 100644 --- a/matita/components/content/interpretations.mli +++ b/matita/components/content/interpretations.mli @@ -28,6 +28,8 @@ type interpretation_id +type cic_id = string + val add_interpretation: string -> (* id / description *) string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index 30abf348e..59df4ffdd 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -279,17 +279,6 @@ let pp_params pp_term = function | [] -> "" | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) -let pp_flavour = function - | `Definition -> "definition" - | `MutualDefinition -> assert false - | `Fact -> "fact" - | `Goal -> "goal" - | `Lemma -> "lemma" - | `Remark -> "remark" - | `Theorem -> "theorem" - | `Variant -> "variant" - | `Axiom -> "axiom" - let pp_fields pp_term fields = (if fields <> [] then "\n" else "") ^ String.concat ";\n" @@ -322,11 +311,9 @@ let pp_obj pp_term = function (pp_term typ) (pp_constructors constructors) in fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Ast.Theorem (`MutualDefinition, name, typ, body,_) -> - sprintf "<>" | Ast.Theorem (flavour, name, typ, body,_) -> sprintf "%s %s:\n %s\n%s" - (pp_flavour flavour) + (NCicPp.string_of_flavour flavour) name (pp_term typ) (match body with diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index 90990300a..aa83b20f3 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -178,7 +178,7 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list type 'term obj = | Inductive of 'term capture_variable list * 'term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma + | Theorem of NCic.def_flavour * string * 'term * 'term option * NCic.def_pragma (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 9b663dfc6..52abe4564 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -350,19 +350,6 @@ let rec find_branch = | Ast.Magic (Ast.If (_, t, _)) -> find_branch t | t -> t -let cic_name_of_name = function - | Ast.Ident ("_", None) -> Cic.Anonymous - | Ast.Ident (name, None) -> Cic.Name name - | _ -> assert false - -let name_of_cic_name = -(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *) - (* ZACK why we used to generate dummy xrefs? *) - let add_dummy_xref t = t in - function - | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None)) - | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None)) - let fresh_index = ref ~-1 type notation_id = int diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli index 6194fc855..daca93587 100644 --- a/matita/components/content/notationUtil.mli +++ b/matita/components/content/notationUtil.mli @@ -82,9 +82,6 @@ val find_appl_pattern_uris: val find_branch: NotationPt.term -> NotationPt.term -val cic_name_of_name: NotationPt.term -> Cic.name -val name_of_cic_name: Cic.name -> NotationPt.term - (** Symbol/Numbers instances *) val freshen_term: NotationPt.term -> NotationPt.term diff --git a/matita/components/content_pres/Makefile b/matita/components/content_pres/Makefile index 7501004fb..e3e223d72 100644 --- a/matita/components/content_pres/Makefile +++ b/matita/components/content_pres/Makefile @@ -21,17 +21,10 @@ cicNotationPres.cmi: OCAMLOPTIONS += -rectypes cicNotationPres.cmo: OCAMLOPTIONS += -rectypes cicNotationPres.cmx: OCAMLOPTIONS += -rectypes -all: test_lexer -clean: clean_tests +all: +clean: LOCAL_LINKOPTS = -package helm-content_pres -linkpkg -test: test_lexer -test_lexer: test_lexer.ml $(PACKAGE).cma - @echo " OCAMLC $<" - @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< - -clean_tests: - rm -f test_lexer{,.opt} cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4) cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4) diff --git a/matita/components/content_pres/cicNotationPres.mli b/matita/components/content_pres/cicNotationPres.mli index 3c9f0ce15..5961b8887 100644 --- a/matita/components/content_pres/cicNotationPres.mli +++ b/matita/components/content_pres/cicNotationPres.mli @@ -35,13 +35,14 @@ val box_of_mpres: mathml_markup -> boxml_markup (** {2 Rendering} *) -val lookup_uri: (Cic.id,UriManager.uri) Hashtbl.t -> Cic.id -> string option +val lookup_uri: (Interpretations.cic_id,UriManager.uri) Hashtbl.t -> + Interpretations.cic_id -> string option (** level 1 -> level 0 * @param ids_to_uris mapping id -> uri for hyperlinking * @param prec precedence level *) val render: - lookup_uri:(Cic.id -> string option) -> ?prec:int -> NotationPt.term -> + lookup_uri:(Interpretations.cic_id -> string option) -> ?prec:int -> NotationPt.term -> markup (** level 0 -> xml stream *) diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 892325d52..45ee2aa0f 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -11,8 +11,8 @@ INTERFACE_FILES = \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -all: test_parser test_dep -clean: clean_tests +all: +clean: # cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by @@ -29,20 +29,5 @@ depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) -clean_tests: - rm -f test_parser{,.opt} test_dep{,.opt} print_grammar{,.opt} - -LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg -test: test_parser print_grammar test_dep -test_parser: test_parser.ml $(PACKAGE).cma - @echo " OCAMLC $<" - @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -print_grammar: print_grammar.ml $(PACKAGE).cma - @echo " OCAMLC $<" - @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -test_dep: test_dep.ml $(PACKAGE).cma - @echo " OCAMLC $<" - @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< - include ../../Makefile.defs include ../Makefile.common diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 837a82910..110c9e912 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -70,11 +70,6 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA let mk_rec_corec ind_kind defs loc = - (* In case of mutual definitions here we produce just - the syntax tree for the first one. The others will be - generated from the completely specified term just before - insertion in the environment. We use the flavour - `MutualDefinition to rememer this. *) let name,ty = match defs with | (params,(N.Ident (name, None), ty),_,_) :: _ -> @@ -88,13 +83,7 @@ let mk_rec_corec ind_kind defs loc = | _ -> assert false in let body = N.Ident (name,None) in - let flavour = - if List.length defs = 1 then - `Definition - else - `MutualDefinition - in - (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) + (loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular)) let nmk_rec_corec ind_kind defs loc = let loc,t = mk_rec_corec ind_kind defs loc in @@ -411,24 +400,11 @@ EXTEND [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact | [ IDENT "lemma" ] -> `Lemma - | [ IDENT "remark" ] -> `Remark - | [ IDENT "theorem" ] -> `Theorem - ] - ]; - theorem_flavour: [ - [ [ IDENT "definition" ] -> `Definition - | [ IDENT "fact" ] -> `Fact - | [ IDENT "lemma" ] -> `Lemma - | [ IDENT "remark" ] -> `Remark + | [ IDENT "example" ] -> `Example | [ IDENT "theorem" ] -> `Theorem + | [ IDENT "corollary" ] -> `Corollary ] ]; - inline_flavour: [ - [ attr = theorem_flavour -> attr - | [ IDENT "axiom" ] -> `Axiom - | [ IDENT "variant" ] -> `Variant - ] - ]; inductive_spec: [ [ fst_name = IDENT; params = LIST0 protected_binder_vars; diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index f3341a5f7..8d0935abc 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -410,17 +410,6 @@ let disambiguate_path path = ~uri:None ~is_path:true ~localization_tbl) ~context:[] path ;; -let new_flavour_of_flavour = function - | `Definition -> `Definition - | `MutualDefinition -> `Definition - | `Fact -> `Fact - | `Lemma -> `Lemma - | `Remark -> `Example - | `Theorem -> `Theorem - | `Variant -> `Corollary - | `Axiom -> `Fact -;; - let ncic_name_of_ident = function | Ast.Ident (name, None) -> name | _ -> assert false @@ -447,11 +436,11 @@ let interpretate_obj uri, height, [], [], (match bo,flavour with | None,`Axiom -> - let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,None,ty',attrs) | Some _,`Axiom -> assert false | None,_ -> - let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> (match bo with @@ -488,14 +477,14 @@ let interpretate_obj ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body)) defs in - let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + let attrs = `Provided, flavour, pragma in NCic.Fixpoint (inductive,inductiveFuns,attrs) | bo -> let bo = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in - let attrs = `Provided, new_flavour_of_flavour flavour, pragma in + let attrs = `Provided, flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) | NotationPt.Inductive (params,tyl) -> let context,params = diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml index 4490ee048..fa204588d 100644 --- a/matita/components/ng_kernel/nCic.ml +++ b/matita/components/ng_kernel/nCic.ml @@ -87,7 +87,7 @@ type inductiveType = (* relevance, typename, arity, constructors *) type def_flavour = (* presentational *) - [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ] + [ `Axiom | `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ] type def_pragma = (* pragmatic of the object *) [ `Coercion of int diff --git a/matita/components/ng_kernel/nCicPp.ml b/matita/components/ng_kernel/nCicPp.ml index 1a793b92f..523b3d4e1 100644 --- a/matita/components/ng_kernel/nCicPp.ml +++ b/matita/components/ng_kernel/nCicPp.ml @@ -272,12 +272,13 @@ let string_of_generated = function ;; let string_of_flavour = function - | `Definition -> "Definition" - | `Fact -> "Fact" - | `Lemma -> "Lemma" - | `Theorem -> "Theorem" - | `Corollary -> "Corollary" - | `Example -> "Example" + | `Axiom -> "axiom" + | `Definition -> "definition" + | `Fact -> "fact" + | `Lemma -> "lemma" + | `Theorem -> "theorem" + | `Corollary -> "corollary" + | `Example -> "example" ;; let string_of_pragma = function diff --git a/matita/components/ng_kernel/nCicPp.mli b/matita/components/ng_kernel/nCicPp.mli index a01895678..39fe4f2f6 100644 --- a/matita/components/ng_kernel/nCicPp.mli +++ b/matita/components/ng_kernel/nCicPp.mli @@ -16,6 +16,8 @@ val set_get_obj: (NUri.uri -> NCic.obj) -> unit val r2s: bool -> NReference.reference -> string +val string_of_flavour: NCic.def_flavour -> string + val ppterm: context:NCic.context -> subst:NCic.substitution -> diff --git a/matita/matita/library/depends b/matita/matita/library/depends index 0c04be486..e255f2bf2 100644 --- a/matita/matita/library/depends +++ b/matita/matita/library/depends @@ -13,8 +13,8 @@ formal_topology/basic_topologies_to_o-basic_topologies.ma formal_topology/basic_ dama/models/nat_order_continuous.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_ordered_uniform.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma nat/orders.ma higher_order_defs/ordering.ma nat/nat.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma nat/sieve.ma list/sort.ma nat/primes.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma formal_topology/subsets.ma formal_topology/categories.ma nat/div_and_mod_diseq.ma nat/lt_arith.ma logic/cprop_connectives.ma logic/connectives.ma @@ -86,14 +86,14 @@ algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma -dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma +dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma formal_topology/relations.ma formal_topology/subsets.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma +formal_topology/r-o-basic_pairs.ma formal_topology/apply_functor.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/o-basic_pairs_to_o-basic_topologies.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma -formal_topology/r-o-basic_pairs.ma formal_topology/apply_functor.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/o-basic_pairs_to_o-basic_topologies.ma logic/equality.ma demo/toolbox.ma logic/cprop_connectives.ma nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma logic/coimplication.ma logic/connectives.ma @@ -115,8 +115,8 @@ higher_order_defs/ordering.ma logic/equality.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma logic/equality.ma higher_order_defs/relations.ma formal_topology/o-concrete_spaces.ma formal_topology/o-basic_pairs.ma formal_topology/o-saturations.ma -formal_topology/o-basic_topologies.ma formal_topology/o-algebra.ma formal_topology/o-saturations.ma formal_topology/concrete_spaces_to_o-concrete_spaces.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/concrete_spaces.ma formal_topology/o-concrete_spaces.ma +formal_topology/o-basic_topologies.ma formal_topology/o-algebra.ma formal_topology/o-saturations.ma dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma Z/compare.ma Z/orders.ma nat/compare.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma @@ -126,14 +126,14 @@ algebra/monoids.ma algebra/semigroups.ma nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma datatypes/categories.ma logic/cprop_connectives.ma -formal_topology/o-basic_pairs.ma formal_topology/notation.ma formal_topology/o-algebra.ma formal_topology/categories.ma formal_topology/cprop_connectives.ma logic/equality.ma +formal_topology/o-basic_pairs.ma formal_topology/notation.ma formal_topology/o-algebra.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma formal_topology/notation.ma dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma -formal_topology/relations_to_o-algebra.ma formal_topology/o-algebra.ma formal_topology/relations.ma +formal_topology/relations_to_o-algebra.ma formal_topology/notation.ma formal_topology/o-algebra.ma formal_topology/relations.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma @@ -145,10 +145,10 @@ didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduct Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma nat/plus.ma nat/nat.ma formal_topology/o-formal_topologies.ma formal_topology/o-basic_topologies.ma +list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma dama/sequence.ma nat/nat.ma nat/primes.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma nat/gcd_properties1.ma nat/gcd.ma -list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma formal_topology/basic_pairs_to_o-basic_pairs.ma formal_topology/basic_pairs.ma formal_topology/o-basic_pairs.ma formal_topology/relations_to_o-algebra.ma dama/bishop_set_rewrite.ma dama/bishop_set.ma diff --git a/matita/matita/matitadep.ml b/matita/matita/matitadep.ml index af811b140..73ce0cd81 100644 --- a/matita/matita/matitadep.ml +++ b/matita/matita/matitadep.ml @@ -68,7 +68,7 @@ let generate_theory theory_file deps = end let main () = -(* let _ = print_times "inizio" in *) + let _ = print_times "inizio" in let include_paths = ref [] in let use_stdout = ref false in let theory_file = ref "" in @@ -155,9 +155,9 @@ let main () = Hashtbl.add include_deps ma_file ma_file Hashtbl.add include_deps_dot ma_file baseuri *) -(* let _ = print_times "prima di iter1" in *) + let _ = print_times "prima di iter1" in List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files; -(* let _ = print_times "in mezzo alle due iter" in *) + let _ = print_times "in mezzo alle due iter" in let map s _ l = s :: l in let ma_files = Hashtbl.fold map baseuri_of [] in List.iter @@ -168,9 +168,11 @@ let main () = in let ma_baseuri = baseuri_of_script ma_file in let dependencies = + let _ = print_times "prima deps_of_iter" in try DependenciesParser.deps_of_file ma_file with Sys_error _ -> [] in + let _ = print_times "dopo deps_of_iter" in let handle_uri uri = if not (Http_getter_storage.is_legacy uri) then let dep = resolve uri ma_baseuri in @@ -198,7 +200,7 @@ let main () = dependencies) ma_files; (* generate regular depend output *) -(* let _ = print_times "dopo di iter2" in *) + let _ = print_times "dopo di iter2" in let deps = List.fold_left (fun acc ma_file -> @@ -247,4 +249,4 @@ let main () = ignore(Sys.command ("tred "^ !dot_file^"| dot -Tpng -o"^dot_name^".png")); HLog.message ("Type 'eog "^dot_name^".png' to view the graph"); end; -(* let _ = print_times "fine" in () *) + let _ = print_times "fine" in () -- 2.39.2