-lib/nUri.cmi:
lib/nUri.cmo: lib/nUri.cmi
lib/nUri.cmx: lib/nUri.cmi
-lib/cps.cmo:
-lib/cps.cmx:
-lib/share.cmo:
-lib/share.cmx:
-lib/log.cmi:
lib/log.cmo: lib/cps.cmx lib/log.cmi
lib/log.cmx: lib/cps.cmx lib/log.cmi
lib/time.cmo: lib/log.cmi
lib/time.cmx: lib/log.cmx
-lib/hierarchy.cmi:
lib/hierarchy.cmo: lib/cps.cmx lib/hierarchy.cmi
lib/hierarchy.cmx: lib/cps.cmx lib/hierarchy.cmi
-lib/output.cmi:
lib/output.cmo: lib/log.cmi lib/output.cmi
lib/output.cmx: lib/log.cmx lib/output.cmi
-automath/aut.cmo:
-automath/aut.cmx:
-automath/autOutput.cmi: automath/aut.cmx
-automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/aut.cmx \
- automath/autOutput.cmi
-automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/aut.cmx \
- automath/autOutput.cmi
+automath/autProcess.cmi: automath/aut.cmx
+automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi
+automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi
+automath/autOutput.cmi: automath/autProcess.cmi automath/aut.cmx
+automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/autProcess.cmi \
+ automath/aut.cmx automath/autOutput.cmi
+automath/autOutput.cmx: lib/log.cmx lib/cps.cmx automath/autProcess.cmx \
+ automath/aut.cmx automath/autOutput.cmi
automath/autParser.cmi: automath/aut.cmx
automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi
basic_rg/brgUntrusted.cmi basic_rg/brgType.cmi basic_rg/brgOutput.cmi \
basic_rg/brg.cmx basic_ag/bagUntrusted.cmi basic_ag/bagType.cmi \
basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
- automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
+ automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
+ automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx lib/output.cmx lib/nUri.cmx \
toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \
toplevel/metaAut.cmx lib/log.cmx lib/hierarchy.cmx lib/cps.cmx \
basic_rg/brgUntrusted.cmx basic_rg/brgType.cmx basic_rg/brgOutput.cmx \
basic_rg/brg.cmx basic_ag/bagUntrusted.cmx basic_ag/bagType.cmx \
basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
- automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
+ automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
+ automath/autLexer.cmx
$(H)./$(MAIN).opt -S 3 $(O) $(INPUT) > log.txt
test-si: $(MAIN).opt
- @echo " HELENA -u $(INPUT-ORIG)"
- $(H)./$(MAIN).opt -u -S 3 $(O) $(INPUT-ORIG) > log.txt
+ @echo " HELENA -c -u $(INPUT)"
+ $(H)./$(MAIN).opt -c -u -S 3 $(O) $(INPUT) > log.txt
meta: $(MAIN).opt
@echo " HELENA -m meta.txt $(INPUT)"
* type "make" or "make opt" to compile the native executable
-* type "make test" to parse the grundlagen
+* type "make test-si" to parse the grundlagen
it generates a log.txt with the grundlagen contents statistics
* type "make clean" to remove the products of compilation
-aut autOutput autParser autLexer
+aut autProcess autOutput autParser autLexer
| Appl of term * term (* application: argument, function *)
| Abst of id * term * term (* abstraction: name, type, body *)
-type item = Section of id option (* section: Some = open/reopen, None = close last *)
+type item = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *)
| Context of qid option (* context: Some = last node, None = root *)
| Block of id * term (* block opener: name, type *)
| Decl of id * term (* declaration: name, type *)
module P = Printf
module L = Log
module A = Aut
+module R = AutProcess
type counters = {
sections: int;
L.warn (P.sprintf " Global Int. Complexity: unknown");
L.warn (P.sprintf " + Abbreviation nodes: %7u" c.xnodes);
f ()
+
+let print_process_counters f c =
+ let f iao iar iac =
+ L.warn (P.sprintf " Automath process summary");
+ L.warn (P.sprintf " Implicit after opening: %7u" iao);
+ L.warn (P.sprintf " Implicit after reopening: %7u" iar);
+ L.warn (P.sprintf " Implicit after closing: %7u" iac);
+ f ()
+ in
+ R.get_counters f c
-(* 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/.
- *)
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
type counters
val count_item: (counters -> 'a) -> counters -> Aut.item -> 'a
val print_counters: (unit -> 'a) -> counters -> 'a
+
+val print_process_counters: (unit -> 'a) -> AutProcess.status -> 'a
| term CM terms { $1 :: $3 }
;
item:
- | PLUS IDENT { A.Section (Some $2) }
- | PLUS TIMES IDENT { A.Section (Some $3) }
- | MINUS IDENT { A.Section None }
- | EXIT { A.Section None }
- | star { A.Context None }
- | qid star { A.Context (Some $1) }
- | IDENT DEF EB sc term { A.Block ($1, $5) }
- | IDENT sc term DEF EB { A.Block ($1, $3) }
- | OB IDENT oftype term CB { A.Block ($2, $4) }
- | IDENT DEF PN sc term { A.Decl ($1, $5) }
- | IDENT sc term DEF PN { A.Decl ($1, $3) }
- | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) }
- | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) }
+ | PLUS IDENT { A.Section (Some (true, $2)) }
+ | PLUS TIMES IDENT { A.Section (Some (false, $3)) }
+ | MINUS IDENT { A.Section None }
+ | EXIT { A.Section None }
+ | star { A.Context None }
+ | qid star { A.Context (Some $1) }
+ | IDENT DEF EB sc term { A.Block ($1, $5) }
+ | IDENT sc term DEF EB { A.Block ($1, $3) }
+ | OB IDENT oftype term CB { A.Block ($2, $4) }
+ | IDENT DEF PN sc term { A.Decl ($1, $5) }
+ | IDENT sc term DEF PN { A.Decl ($1, $3) }
+ | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4) }
+ | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6) }
;
items:
| { [] }
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module A = Aut
+
+type status = {
+ opening : bool; (* just opened section *)
+ reopening: bool; (* just reopened section *)
+ closing : bool; (* just closed section *)
+ iao : int; (* implicit context after opening section *)
+ iar : int; (* implicit context after reopening section *)
+ iac : int (* implicit context after closing section *)
+}
+
+(* internal functions *******************************************************)
+
+let proc_section f st = function
+ | Some (true, _) -> f {st with opening = true}
+ | Some (false, _) -> f {st with reopening = true}
+ | None -> f {st with closing = true}
+
+let proc_context f st =
+ f {st with opening = false; reopening = false; closing = false}
+
+let proc_proper f st =
+ let st = if st.opening then {st with iao = succ st.iao} else st in
+ let st = if st.reopening then {st with iar = succ st.iar} else st in
+ let st = if st.closing then {st with iac = succ st.iac} else st in
+ proc_context f st
+
+let proc_item f st item = match item with
+ | A.Section section -> proc_section f st section item
+ | A.Context _ -> proc_context f st item
+ | _ -> proc_proper f st item
+
+(* interface functions ******************************************************)
+
+let initial_status = {
+ opening = false; reopening = false; closing = false;
+ iao = 0; iar = 0; iac = 0
+}
+
+let process_item = proc_item
+
+let get_counters f st = f st.iao st.iar st.iac
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+type status
+
+val initial_status: status
+
+val process_item: (status -> Aut.item -> 'a) -> status -> Aut.item -> 'a
+
+val get_counters: (int -> int -> int -> 'a) -> status -> 'a
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-
exception LRefNotFound of Bag.message
type ho_whd_result =
node: context_node; (* current context node *)
nodes: context_node list; (* context node list *)
line: int; (* line number *)
- explicit: bool (* need explicit context root? *)
+ cover: string (* initial segment of URI hierarchy *)
}
type resolver = Local of int
(* Internal functions *******************************************************)
-let initial_status size = {
- path = []; node = None; nodes = []; line = 1; explicit = true;
+let initial_status size cover = {
+ path = []; node = None; nodes = []; line = 1; cover = cover;
henv = H.create size; hcnt = H.create size
}
let id_of_name (id, _, _) = id
-let mk_qid id path =
- let str = String.concat "/" path in
- let str = Filename.concat str id in
+let mk_qid st id path =
+ let uripath = if st.cover = "" then path else st.cover :: path in
+ let str = String.concat "/" uripath in
+ let str = Filename.concat str id in
U.uri_of_string ("ld:/" ^ str), id, path
let uri_of_qid (uri, _, _) = uri
let complete_qid f st (id, is_local, qs) =
- let f qs = f (mk_qid id qs) in
+ let f qs = f (mk_qid st id qs) in
let f path = Cps.list_rev_append f path ~tail:qs in
let rec skip f = function
| phd :: ptl, qshd :: _ when phd = qshd -> f ptl
in
if is_local then f st.path else skip f (st.path, qs)
-let relax_qid f (_, id, path) =
- let f path = f (mk_qid id path) in
+let relax_qid f st (_, id, path) =
+ let f path = f (mk_qid st id path) in
let f = function
| _ :: tl -> Cps.list_rev f tl
| [] -> assert false
in
Cps.list_rev f path
-let relax_opt_qid f = function
+let relax_opt_qid f st = function
| None -> f None
- | Some qid -> let f qid = f (Some qid) in relax_qid f qid
+ | Some qid -> let f qid = f (Some qid) in relax_qid f st qid
let resolve_lref f st l lenv id =
let rec aux f i = function
let resolve_gref_relaxed f st qid =
let rec g qid = function
- | None -> relax_qid (resolve_gref g st) qid
+ | None -> relax_qid (resolve_gref g st) st qid
| Some args -> f qid args
in
resolve_gref g st qid
let get_pars_relaxed f st =
let rec g pars = function
| None -> f pars
- | Some node -> relax_opt_qid (get_pars g st) node
+ | Some node -> relax_opt_qid (get_pars g st) st node
in
get_pars g st st.node
resolve_lref f st l lenv (id_of_name name)
let xlate_item f st = function
- | A.Section (Some name) ->
+ | A.Section (Some (_, name)) ->
f {st with path = name :: st.path; nodes = st.node :: st.nodes} None
| A.Section None ->
begin match st.path, st.nodes with
(* Interface functions ******************************************************)
-let initial_status = initial_status hsize
+let initial_status ?(cover="") () =
+ initial_status hsize cover
let meta_of_aut = xlate_item
-(* 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/.
- *)
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
type status
-val initial_status: status
+val initial_status: ?cover:string -> unit -> status
val meta_of_aut: (status -> Meta.item -> 'a) -> status -> Aut.item -> 'a
module L = Log
module H = Hierarchy
module O = Output
+module AP = AutProcess
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
module BagU = BagUntrusted
type status = {
+ ast : AP.status;
mst : MA.status;
ac : AO.counters;
mc : MO.counters;
bagc: BagO.counters
}
-let initial_status = {
+let initial_status cover = {
ac = AO.initial_counters;
mc = MO.initial_counters;
brgc = BrgO.initial_counters;
bagc = BagO.initial_counters;
- mst = MA.initial_status
+ mst = MA.initial_status ~cover ();
+ ast = AP.initial_status
}
let count count_fun c item =
let brg_error s msg =
L.error BrgO.specs (L.Warn s :: L.Loc :: msg); flush ()
+let process_item f st =
+ let f ast = f {st with ast = ast} in
+ AP.process_item f st.ast
+
(* kernel related ***********************************************************)
type kernel = Brg | Bag
let main =
try
- let version_string = "Helena 0.8.0 M - June 2009" in
+ let version_string = "Helena 0.8.0 M - July 2009" in
let stage = ref 3 in
let meta_file = ref None in
let progress = ref false in
+ let use_cover = ref true in
let set_hierarchy s =
let f = function
| Some g -> H.graph := g
in
(* stage 0 *)
let st = {st with ac = count AO.count_item st.ac item} in
- let st =
- if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st
+ let f st item =
+ let st =
+ if !stage > 0 then MA.meta_of_aut (f st) st.mst item else st
+ in
+ aux st tl
in
- aux st tl
- in
+ process_item f st item
+ in
O.clear_reductions ();
- let st = aux initial_status book in
+ let cover =
+ if !use_cover then Filename.chop_extension (Filename.basename name)
+ else ""
+ in
+ let st = aux (initial_status cover) book in
if !L.level > 0 then Time.utime_stamp "processed";
if !L.level > 2 then AO.print_counters C.start st.ac;
+ if !L.level > 2 then AO.print_process_counters C.start st.ast;
if !L.level > 2 && !stage > 0 then MO.print_counters C.start st.mc;
if !L.level > 2 && !stage > 1 then print_counters st;
if !L.level > 2 && !stage > 1 then O.print_reductions ()
in
let help =
- "Usage: helena [ -Vipu | -Ss <number> | -m <file> | -hk <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -Vcipu | -Ss <number> | -m <file> | -hk <string> ] <file> ...\n\n" ^
"Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted\n"
in
let help_S = "<number> set summary level" in
let help_V = " show version information" in
+ let help_c = " disable initial segment of URI hierarchy" in
let help_h = "<string> set type hierarchy" in
let help_i = " show local references by index" in
let help_k = "<string> set kernel version" in
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
+ ("-c", Arg.Clear use_cover, help_c);
("-h", Arg.String set_hierarchy, help_h);
("-i", Arg.Set O.indexes, help_i);
("-k", Arg.String set_kernel, help_k);
projects / helm.git / commitdiff