+++ /dev/null
-requires="helm-urimanager helm-xml expat"
-version="0.0.1"
-archive(byte)="cic.cma"
-archive(native)="cic.cmxa"
-linkopts=""
-requires="unix camlp5.gramlib"
+requires="str unix camlp5.gramlib"
version="0.0.1"
archive(byte)="extlib.cma"
archive(native)="extlib.cmxa"
-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"
-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"
-requires="helm-cic helm-getter"
+requires="helm-getter"
version="0.0.1"
archive(byte)="library.cma"
archive(native)="library.cmxa"
-requires="helm-cic"
+requires=""
version="0.0.1"
archive(byte)="ng_kernel.cma"
archive(native)="ng_kernel.cmxa"
-requires="helm-cic helm-ng_refiner"
+requires="helm-ng_refiner"
version="0.0.1"
archive(byte)="ng_paramodulation.cma"
archive(native)="ng_paramodulation.cmxa"
urimanager \
logger \
getter \
- cic \
library \
ng_kernel \
content \
--- /dev/null
+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
--- /dev/null
+(* 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 -> ()
+
--- /dev/null
+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
--- /dev/null
+(* 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 "@[<v>";
+ (match name with
+ |Some name -> Format.fprintf fmt "Precedence %s:@ " name
+ | None -> ());
+ Format.fprintf fmt "@[<v>";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ if List.for_all is_symbol_dummy x then todo else (
+ Format.fprintf fmt "@[<h> | ";
+ 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 "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Slist0sep (symbol,sep) ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "{@[<hov2> ";
+ 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 "{@[<hov2> ";
+ 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 "{@[<hov2> ";
+ 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 "[@[<hov2> ";
+ 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 "@[<hv 2>%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
+;;
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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\e[01;31m%s\e[00m%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)
+
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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
- ]
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 *)
type interpretation_id
+type cic_id = string
+
val add_interpretation:
string -> (* id / description *)
string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *)
| [] -> ""
| 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"
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
- sprintf "<<pretty printing of mutual definitions not implemented yet>>"
| 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
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
| 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
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
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)
(** {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 *)
+++ /dev/null
-(* 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 -> ()
-
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
-all: test_parser test_dep
-clean: clean_tests
+all:
+clean:
# <cross> 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
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
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),_,_) :: _ ->
| _ -> 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
[ [ 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;
+++ /dev/null
-(* 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 "@[<v>";
- (match name with
- |Some name -> Format.fprintf fmt "Precedence %s:@ " name
- | None -> ());
- Format.fprintf fmt "@[<v>";
- let todo =
- List.fold_left
- (fun acc x ->
- if List.for_all is_symbol_dummy x then todo else (
- Format.fprintf fmt "@[<h> | ";
- 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 "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]} @ ";
- todo
- | Slist0sep (symbol,sep) ->
- Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "[@[<hov2> ";
- 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 "@[<hv 2>%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
-;;
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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\e[01;31m%s\e[00m%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)
-
~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
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
([],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 =
(* 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
;;
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
val r2s: bool -> NReference.reference -> string
+val string_of_flavour: NCic.def_flavour -> string
+
val ppterm:
context:NCic.context ->
subst:NCic.substitution ->
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
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
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
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
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
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
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
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
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 ->
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 ()
projects / helm.git / commitdiff