From: Andrea Asperti Date: Tue, 26 Oct 2010 12:58:39 +0000 (+0000) Subject: cic module removed (RIP) X-Git-Tag: make_still_working~2768 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;p=helm.git cic module removed (RIP) --- 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/binaries/test_lexer/test_lexer.ml b/matita/components/binaries/test_lexer/test_lexer.ml new file mode 100644 index 000000000..587d87bd8 --- /dev/null +++ b/matita/components/binaries/test_lexer/test_lexer.ml @@ -0,0 +1,63 @@ +(* 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/ + *) + +(* $Id$ *) + +let _ = + let level = ref "2@" in + let ic = ref stdin in + let arg_spec = [ "-level", Arg.Set_string level, "set the notation level" ] in + let usage = "test_lexer [ -level level ] [ file ]" in + let open_file fname = + if !ic <> stdin then close_in !ic; + ic := open_in fname + in + Arg.parse arg_spec open_file usage; + let lexer = + match !level with + "1" -> CicNotationLexer.level1_pattern_lexer () + | "2@" -> CicNotationLexer.level2_ast_lexer () + | "2$" -> CicNotationLexer.level2_meta_lexer () + | l -> + prerr_endline (Printf.sprintf "Unsupported level %s" l); + exit 2 + in + let token_stream, loc_func = + lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_channel !ic)) in + Printf.printf "Lexing notation level %s\n" !level; flush stdout; + let tok_count = ref 0 in + let rec dump () = + let (a,b) = Stream.next token_stream in + if a = "EOI" then raise Stream.Failure; + let pos = loc_func !tok_count in + print_endline (Printf.sprintf "%s '%s' (@ %d-%d)" a b + (Stdpp.first_pos pos) (Stdpp.last_pos pos)); + incr tok_count; + dump () + in + try + dump () + with Stream.Failure -> () + 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/binaries/test_parser/print_grammar.ml b/matita/components/binaries/test_parser/print_grammar.ml new file mode 100644 index 000000000..893a3f53c --- /dev/null +++ b/matita/components/binaries/test_parser/print_grammar.ml @@ -0,0 +1,275 @@ +(* 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/ + *) + +(* $Id$ *) + +open Gramext + +let rec flatten_tree = function + | DeadEnd -> [] + | LocAct _ -> [[]] + | Node {node = n; brother = b; son = s} -> + List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b + +let tex_of_unicode s = s + +let rec clean_dummy_desc = function + | Dlevels l -> Dlevels (clean_levels l) + | x -> x + +and clean_levels = function + | [] -> [] + | l :: tl -> clean_level l @ clean_levels tl + +and clean_level = function + | x -> + let pref = clean_tree x.lprefix in + let suff = clean_tree x.lsuffix in + match pref,suff with + | DeadEnd, DeadEnd -> [] + | _ -> [{x with lprefix = pref; lsuffix = suff}] + +and clean_tree = function + | Node n -> clean_node n + | x -> x + +and clean_node = function + | {node=node;son=son;brother=brother} -> + let bn = is_symbol_dummy node in + let bs = is_tree_dummy son in + let bb = is_tree_dummy brother in + let son = if bs then DeadEnd else son in + let brother = if bb then DeadEnd else brother in + if bb && bs && bn then + DeadEnd + else + if bn then + Node {node=Sself;son=son;brother=brother} + else + Node {node=node;son=son;brother=brother} + +and is_level_dummy = function + | {lsuffix=lsuffix;lprefix=lprefix} -> + is_tree_dummy lsuffix && is_tree_dummy lprefix + +and is_desc_dummy = function + | Dlevels l -> List.for_all is_level_dummy l + | Dparser _ -> true + +and is_entry_dummy = function + | {edesc=edesc} -> is_desc_dummy edesc + +and is_symbol_dummy = function + | Stoken ("DUMMY", _) -> true + | Stoken _ -> false + | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt + | Snterm e | Snterml (e, _) -> is_entry_dummy e + | Slist1 x | Slist0 x -> is_symbol_dummy x + | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself | Snext -> false + | Stree t -> is_tree_dummy t + | _ -> assert false + +and is_tree_dummy = function + | Node {node=node} -> is_symbol_dummy node + | _ -> true + +let needs_brackets t = + let rec count_brothers = function + | Node {brother = brother} -> 1 + count_brothers brother + | _ -> 0 + in + count_brothers t > 1 + +let visit_description desc fmt self = + let skip s = true in + let inline s = List.mem s [ "int" ] in + + let rec visit_entry e ?level todo is_son = + let { ename = ename; edesc = desc } = e in + if inline ename then + visit_desc desc todo is_son + else + begin + (match level with + | None -> Format.fprintf fmt "%s " ename; + | Some _ -> Format.fprintf fmt "%s " ename;); + if skip ename then + todo + else + todo @ [e] + end + + and visit_desc d todo is_son = + match d with + | Dlevels l -> + List.fold_left + (fun acc l -> + Format.fprintf fmt "@ "; + visit_level l acc is_son ) + todo l; + | Dparser _ -> todo + + and visit_level l todo is_son = + let { lname = name ; lsuffix = suff ; lprefix = pref } = l in + visit_tree name + (List.map + (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref) + todo is_son + + and visit_tree name t todo is_son = + if List.for_all (List.for_all is_symbol_dummy) t then todo else ( + Format.fprintf fmt "@["; + (match name with + |Some name -> Format.fprintf fmt "Precedence %s:@ " name + | None -> ()); + Format.fprintf fmt "@["; + let todo = + List.fold_left + (fun acc x -> + if List.for_all is_symbol_dummy x then todo else ( + Format.fprintf fmt "@[ | "; + let todo = + List.fold_left + (fun acc x -> + let todo = visit_symbol x acc true in + Format.fprintf fmt "@ "; + todo) + acc x + in + Format.fprintf fmt "@]@ "; + todo)) + todo t + in + Format.fprintf fmt "@]"; + Format.fprintf fmt "@]"; + todo) + + and visit_symbol s todo is_son = + match s with + | Smeta (name, sl, _) -> + Format.fprintf fmt "%s " name; + List.fold_left ( + fun acc s -> + let todo = visit_symbol s acc is_son in + if is_son then + Format.fprintf fmt "@ "; + todo) + todo sl + | Snterm entry -> visit_entry entry todo is_son + | Snterml (entry,level) -> visit_entry entry ~level todo is_son + | Slist0 symbol -> + Format.fprintf fmt "{@[ "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]} @ "; + todo + | Slist0sep (symbol,sep) -> + Format.fprintf fmt "[@[ "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "{@[ "; + let todo = visit_symbol sep todo is_son in + Format.fprintf fmt " "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]} @]] @ "; + todo + | Slist1 symbol -> + Format.fprintf fmt "{@[ "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]}+ @ "; + todo + | Slist1sep (symbol,sep) -> + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "{@[ "; + let todo = visit_symbol sep todo is_son in + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]} @ "; + todo + | Sopt symbol -> + Format.fprintf fmt "[@[ "; + let todo = visit_symbol symbol todo is_son in + Format.fprintf fmt "@]] @ "; + todo + | Sself -> Format.fprintf fmt "%s " self; todo + | Snext -> Format.fprintf fmt "next "; todo + | Stoken pattern -> + let constructor, keyword = pattern in + if keyword = "" then + (if constructor <> "DUMMY" then + Format.fprintf fmt "`%s' " constructor) + else + Format.fprintf fmt "%s " (tex_of_unicode keyword); + todo + | Stree tree -> + visit_tree None (flatten_tree tree) todo is_son + | _ -> assert false + in + visit_desc desc [] false +;; + + +let rec visit_entries fmt todo pped = + match todo with + | [] -> () + | hd :: tl -> + let todo = + if not (List.memq hd pped) then + begin + let { ename = ename; edesc = desc } = hd in + Format.fprintf fmt "@[%s ::= " ename; + let desc = clean_dummy_desc desc in + let todo = visit_description desc fmt ename @ todo in + Format.fprintf fmt "@]\n\n"; + todo + end + else + todo + in + let clean_todo todo = + let name_of_entry e = e.ename in + let pped = hd :: pped in + let todo = tl @ todo in + let todo = List.filter (fun e -> not(List.memq e pped)) todo in + HExtlib.list_uniq + ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) + (List.sort + (fun e1 e2 -> + Pervasives.compare (name_of_entry e1) (name_of_entry e2)) + todo), + pped + in + let todo,pped = clean_todo todo in + visit_entries fmt todo pped +;; + +let ebnf_of_term () = + let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in + let buff = Buffer.create 100 in + let fmt = Format.formatter_of_buffer buff in + visit_entries fmt [g_entry] []; + Format.fprintf fmt "@?"; + let s = Buffer.contents buff in + s +;; diff --git a/matita/components/binaries/test_parser/test_dep.ml b/matita/components/binaries/test_parser/test_dep.ml new file mode 100644 index 000000000..b397df31b --- /dev/null +++ b/matita/components/binaries/test_parser/test_dep.ml @@ -0,0 +1,35 @@ +(* 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/ + *) + +(* $Id$ *) + +let _ = + let ic = ref "/dev/fd/0" in + let usage = "test_coarse_parser [ file ]" in + let open_file fname = ic := fname in + Arg.parse [] open_file usage; + let deps = DependenciesParser.deps_of_file !ic in + List.iter (fun dep -> print_endline (DependenciesParser.pp_dependency dep)) deps + diff --git a/matita/components/binaries/test_parser/test_parser.ml b/matita/components/binaries/test_parser/test_parser.ml new file mode 100644 index 000000000..7e2eb7955 --- /dev/null +++ b/matita/components/binaries/test_parser/test_parser.ml @@ -0,0 +1,125 @@ +(* 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/ + *) + +(* $Id$ *) + +open Printf + +let _ = Helm_registry.load_from "test_parser.conf.xml" + +let xml_stream_of_markup = + let rec print_box (t: CicNotationPres.boxml_markup) = + Box.box2xml print_mpres t + and print_mpres (t: CicNotationPres.mathml_markup) = + Mpresentation.print_mpres print_box t + in + print_mpres + +let dump_xml t id_to_uri fname = + prerr_endline (sprintf "dumping MathML to %s ..." fname); + flush stdout; + let oc = open_out fname in + let markup = + CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri id_to_uri)t in + let xml_stream = CicNotationPres.print_xml markup in + Xml.pp_to_outchan xml_stream oc; + close_out oc + +let extract_loc = + function + | GrafiteAst.Executable (loc, _) + | GrafiteAst.Comment (loc, _) -> loc + +let pp_associativity = function + | Gramext.LeftA -> "left" + | Gramext.RightA -> "right" + | Gramext.NonA -> "non" + +let pp_precedence = string_of_int + +(* let last_rule_id = ref None *) + +let process_stream istream = + let char_count = ref 0 in + let module P = NotationPt in + let module G = GrafiteAst in + let status = + ref + (CicNotation2.load_notation (new LexiconEngine.status) + ~include_paths:[] (Helm_registry.get "notation.core_file")) + in + try + while true do + try + match + GrafiteParser.parse_statement ~include_paths:[] istream !status + with + newstatus, GrafiteParser.LNone _ -> status := newstatus + | newstatus, GrafiteParser.LSome statement -> + status := newstatus; + let floc = extract_loc statement in + let (_, y) = HExtlib.loc_of_floc floc in + char_count := y + !char_count; + match statement with + (* | G.Executable (_, G.Macro (_, G.Check (_, + P.AttributedTerm (_, P.Ident _)))) -> + prerr_endline "mega hack"; + (match !last_rule_id with + | None -> () + | Some id -> + prerr_endline "removing last notation rule ..."; + NotationParser.delete id) *) + | statement -> + prerr_endline + ("Unsupported statement: " ^ + GrafiteAstPp.pp_statement statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex")) + with + | End_of_file -> raise End_of_file + | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> + let (x, y) = HExtlib.loc_of_floc floc in +(* let before = String.sub line 0 x in + let error = String.sub line x (y - x) in + let after = String.sub line y (String.length line - y) in + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) + prerr_endline (sprintf "Parse error at character %d-%d: %s" + (!char_count + x) (!char_count + y) msg) + | exn -> + prerr_endline + (sprintf "TestParser: Uncaught exception: %s" (Printexc.to_string exn)) + done + with End_of_file -> () + +let _ = + let arg_spec = [ ] in + let usage = "" in + Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + print_endline "Loading builtin notation ..."; + print_endline "done."; + flush stdout; + process_stream (Ulexing.from_utf8_channel stdin) + 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/content_pres/test_lexer.ml b/matita/components/content_pres/test_lexer.ml deleted file mode 100644 index 587d87bd8..000000000 --- a/matita/components/content_pres/test_lexer.ml +++ /dev/null @@ -1,63 +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/ - *) - -(* $Id$ *) - -let _ = - let level = ref "2@" in - let ic = ref stdin in - let arg_spec = [ "-level", Arg.Set_string level, "set the notation level" ] in - let usage = "test_lexer [ -level level ] [ file ]" in - let open_file fname = - if !ic <> stdin then close_in !ic; - ic := open_in fname - in - Arg.parse arg_spec open_file usage; - let lexer = - match !level with - "1" -> CicNotationLexer.level1_pattern_lexer () - | "2@" -> CicNotationLexer.level2_ast_lexer () - | "2$" -> CicNotationLexer.level2_meta_lexer () - | l -> - prerr_endline (Printf.sprintf "Unsupported level %s" l); - exit 2 - in - let token_stream, loc_func = - lexer.Token.tok_func (Obj.magic (Ulexing.from_utf8_channel !ic)) in - Printf.printf "Lexing notation level %s\n" !level; flush stdout; - let tok_count = ref 0 in - let rec dump () = - let (a,b) = Stream.next token_stream in - if a = "EOI" then raise Stream.Failure; - let pos = loc_func !tok_count in - print_endline (Printf.sprintf "%s '%s' (@ %d-%d)" a b - (Stdpp.first_pos pos) (Stdpp.last_pos pos)); - incr tok_count; - dump () - in - try - dump () - with Stream.Failure -> () - 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/grafite_parser/print_grammar.ml b/matita/components/grafite_parser/print_grammar.ml deleted file mode 100644 index 893a3f53c..000000000 --- a/matita/components/grafite_parser/print_grammar.ml +++ /dev/null @@ -1,275 +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/ - *) - -(* $Id$ *) - -open Gramext - -let rec flatten_tree = function - | DeadEnd -> [] - | LocAct _ -> [[]] - | Node {node = n; brother = b; son = s} -> - List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b - -let tex_of_unicode s = s - -let rec clean_dummy_desc = function - | Dlevels l -> Dlevels (clean_levels l) - | x -> x - -and clean_levels = function - | [] -> [] - | l :: tl -> clean_level l @ clean_levels tl - -and clean_level = function - | x -> - let pref = clean_tree x.lprefix in - let suff = clean_tree x.lsuffix in - match pref,suff with - | DeadEnd, DeadEnd -> [] - | _ -> [{x with lprefix = pref; lsuffix = suff}] - -and clean_tree = function - | Node n -> clean_node n - | x -> x - -and clean_node = function - | {node=node;son=son;brother=brother} -> - let bn = is_symbol_dummy node in - let bs = is_tree_dummy son in - let bb = is_tree_dummy brother in - let son = if bs then DeadEnd else son in - let brother = if bb then DeadEnd else brother in - if bb && bs && bn then - DeadEnd - else - if bn then - Node {node=Sself;son=son;brother=brother} - else - Node {node=node;son=son;brother=brother} - -and is_level_dummy = function - | {lsuffix=lsuffix;lprefix=lprefix} -> - is_tree_dummy lsuffix && is_tree_dummy lprefix - -and is_desc_dummy = function - | Dlevels l -> List.for_all is_level_dummy l - | Dparser _ -> true - -and is_entry_dummy = function - | {edesc=edesc} -> is_desc_dummy edesc - -and is_symbol_dummy = function - | Stoken ("DUMMY", _) -> true - | Stoken _ -> false - | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt - | Snterm e | Snterml (e, _) -> is_entry_dummy e - | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y - | Sopt x -> is_symbol_dummy x - | Sself | Snext -> false - | Stree t -> is_tree_dummy t - | _ -> assert false - -and is_tree_dummy = function - | Node {node=node} -> is_symbol_dummy node - | _ -> true - -let needs_brackets t = - let rec count_brothers = function - | Node {brother = brother} -> 1 + count_brothers brother - | _ -> 0 - in - count_brothers t > 1 - -let visit_description desc fmt self = - let skip s = true in - let inline s = List.mem s [ "int" ] in - - let rec visit_entry e ?level todo is_son = - let { ename = ename; edesc = desc } = e in - if inline ename then - visit_desc desc todo is_son - else - begin - (match level with - | None -> Format.fprintf fmt "%s " ename; - | Some _ -> Format.fprintf fmt "%s " ename;); - if skip ename then - todo - else - todo @ [e] - end - - and visit_desc d todo is_son = - match d with - | Dlevels l -> - List.fold_left - (fun acc l -> - Format.fprintf fmt "@ "; - visit_level l acc is_son ) - todo l; - | Dparser _ -> todo - - and visit_level l todo is_son = - let { lname = name ; lsuffix = suff ; lprefix = pref } = l in - visit_tree name - (List.map - (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref) - todo is_son - - and visit_tree name t todo is_son = - if List.for_all (List.for_all is_symbol_dummy) t then todo else ( - Format.fprintf fmt "@["; - (match name with - |Some name -> Format.fprintf fmt "Precedence %s:@ " name - | None -> ()); - Format.fprintf fmt "@["; - let todo = - List.fold_left - (fun acc x -> - if List.for_all is_symbol_dummy x then todo else ( - Format.fprintf fmt "@[ | "; - let todo = - List.fold_left - (fun acc x -> - let todo = visit_symbol x acc true in - Format.fprintf fmt "@ "; - todo) - acc x - in - Format.fprintf fmt "@]@ "; - todo)) - todo t - in - Format.fprintf fmt "@]"; - Format.fprintf fmt "@]"; - todo) - - and visit_symbol s todo is_son = - match s with - | Smeta (name, sl, _) -> - Format.fprintf fmt "%s " name; - List.fold_left ( - fun acc s -> - let todo = visit_symbol s acc is_son in - if is_son then - Format.fprintf fmt "@ "; - todo) - todo sl - | Snterm entry -> visit_entry entry todo is_son - | Snterml (entry,level) -> visit_entry entry ~level todo is_son - | Slist0 symbol -> - Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "@]} @ "; - todo - | Slist0sep (symbol,sep) -> - Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son in - Format.fprintf fmt " "; - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "@]} @]] @ "; - todo - | Slist1 symbol -> - Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "@]}+ @ "; - todo - | Slist1sep (symbol,sep) -> - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son in - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "@]} @ "; - todo - | Sopt symbol -> - Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son in - Format.fprintf fmt "@]] @ "; - todo - | Sself -> Format.fprintf fmt "%s " self; todo - | Snext -> Format.fprintf fmt "next "; todo - | Stoken pattern -> - let constructor, keyword = pattern in - if keyword = "" then - (if constructor <> "DUMMY" then - Format.fprintf fmt "`%s' " constructor) - else - Format.fprintf fmt "%s " (tex_of_unicode keyword); - todo - | Stree tree -> - visit_tree None (flatten_tree tree) todo is_son - | _ -> assert false - in - visit_desc desc [] false -;; - - -let rec visit_entries fmt todo pped = - match todo with - | [] -> () - | hd :: tl -> - let todo = - if not (List.memq hd pped) then - begin - let { ename = ename; edesc = desc } = hd in - Format.fprintf fmt "@[%s ::= " ename; - let desc = clean_dummy_desc desc in - let todo = visit_description desc fmt ename @ todo in - Format.fprintf fmt "@]\n\n"; - todo - end - else - todo - in - let clean_todo todo = - let name_of_entry e = e.ename in - let pped = hd :: pped in - let todo = tl @ todo in - let todo = List.filter (fun e -> not(List.memq e pped)) todo in - HExtlib.list_uniq - ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) - (List.sort - (fun e1 e2 -> - Pervasives.compare (name_of_entry e1) (name_of_entry e2)) - todo), - pped - in - let todo,pped = clean_todo todo in - visit_entries fmt todo pped -;; - -let ebnf_of_term () = - let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in - let buff = Buffer.create 100 in - let fmt = Format.formatter_of_buffer buff in - visit_entries fmt [g_entry] []; - Format.fprintf fmt "@?"; - let s = Buffer.contents buff in - s -;; diff --git a/matita/components/grafite_parser/test_dep.ml b/matita/components/grafite_parser/test_dep.ml deleted file mode 100644 index b397df31b..000000000 --- a/matita/components/grafite_parser/test_dep.ml +++ /dev/null @@ -1,35 +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/ - *) - -(* $Id$ *) - -let _ = - let ic = ref "/dev/fd/0" in - let usage = "test_coarse_parser [ file ]" in - let open_file fname = ic := fname in - Arg.parse [] open_file usage; - let deps = DependenciesParser.deps_of_file !ic in - List.iter (fun dep -> print_endline (DependenciesParser.pp_dependency dep)) deps - diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml deleted file mode 100644 index 7e2eb7955..000000000 --- a/matita/components/grafite_parser/test_parser.ml +++ /dev/null @@ -1,125 +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/ - *) - -(* $Id$ *) - -open Printf - -let _ = Helm_registry.load_from "test_parser.conf.xml" - -let xml_stream_of_markup = - let rec print_box (t: CicNotationPres.boxml_markup) = - Box.box2xml print_mpres t - and print_mpres (t: CicNotationPres.mathml_markup) = - Mpresentation.print_mpres print_box t - in - print_mpres - -let dump_xml t id_to_uri fname = - prerr_endline (sprintf "dumping MathML to %s ..." fname); - flush stdout; - let oc = open_out fname in - let markup = - CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri id_to_uri)t in - let xml_stream = CicNotationPres.print_xml markup in - Xml.pp_to_outchan xml_stream oc; - close_out oc - -let extract_loc = - function - | GrafiteAst.Executable (loc, _) - | GrafiteAst.Comment (loc, _) -> loc - -let pp_associativity = function - | Gramext.LeftA -> "left" - | Gramext.RightA -> "right" - | Gramext.NonA -> "non" - -let pp_precedence = string_of_int - -(* let last_rule_id = ref None *) - -let process_stream istream = - let char_count = ref 0 in - let module P = NotationPt in - let module G = GrafiteAst in - let status = - ref - (CicNotation2.load_notation (new LexiconEngine.status) - ~include_paths:[] (Helm_registry.get "notation.core_file")) - in - try - while true do - try - match - GrafiteParser.parse_statement ~include_paths:[] istream !status - with - newstatus, GrafiteParser.LNone _ -> status := newstatus - | newstatus, GrafiteParser.LSome statement -> - status := newstatus; - let floc = extract_loc statement in - let (_, y) = HExtlib.loc_of_floc floc in - char_count := y + !char_count; - match statement with - (* | G.Executable (_, G.Macro (_, G.Check (_, - P.AttributedTerm (_, P.Ident _)))) -> - prerr_endline "mega hack"; - (match !last_rule_id with - | None -> () - | Some id -> - prerr_endline "removing last notation rule ..."; - NotationParser.delete id) *) - | statement -> - prerr_endline - ("Unsupported statement: " ^ - GrafiteAstPp.pp_statement statement - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex")) - with - | End_of_file -> raise End_of_file - | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> - let (x, y) = HExtlib.loc_of_floc floc in -(* let before = String.sub line 0 x in - let error = String.sub line x (y - x) in - let after = String.sub line y (String.length line - y) in - eprintf "%s%s%s\n" before error after; - prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) - prerr_endline (sprintf "Parse error at character %d-%d: %s" - (!char_count + x) (!char_count + y) msg) - | exn -> - prerr_endline - (sprintf "TestParser: Uncaught exception: %s" (Printexc.to_string exn)) - done - with End_of_file -> () - -let _ = - let arg_spec = [ ] in - let usage = "" in - Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; - print_endline "Loading builtin notation ..."; - print_endline "done."; - flush stdout; - process_stream (Ulexing.from_utf8_channel stdin) - 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 ()