-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
-automath/aut.cmo:
-automath/aut.cmx:
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/autParser.cmx: automath/aut.cmx automath/autParser.cmi
automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi
automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx
-common/hierarchy.cmi:
common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi
common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi
-common/output.cmi:
common/output.cmo: lib/log.cmi common/output.cmi
common/output.cmx: lib/log.cmx common/output.cmi
common/item.cmo: lib/nUri.cmi automath/aut.cmx
lib/cps.cmx toplevel/metaOutput.cmi
toplevel/metaOutput.cmx: lib/nUri.cmx toplevel/meta.cmx lib/log.cmx \
lib/cps.cmx toplevel/metaOutput.cmi
+toplevel/metaLibrary.cmi: toplevel/meta.cmx
+toplevel/metaLibrary.cmo: toplevel/metaOutput.cmi toplevel/metaLibrary.cmi
+toplevel/metaLibrary.cmx: toplevel/metaOutput.cmx toplevel/metaLibrary.cmi
toplevel/metaAut.cmi: toplevel/meta.cmx automath/aut.cmx
toplevel/metaAut.cmo: lib/nUri.cmi toplevel/meta.cmx lib/cps.cmx \
automath/aut.cmx toplevel/metaAut.cmi
toplevel/metaBrg.cmx: toplevel/meta.cmx lib/cps.cmx basic_rg/brg.cmx \
toplevel/metaBrg.cmi
toplevel/top.cmo: lib/time.cmx common/output.cmi lib/nUri.cmi \
- toplevel/metaOutput.cmi toplevel/metaBrg.cmi toplevel/metaBag.cmi \
- toplevel/metaAut.cmi lib/log.cmi common/library.cmi common/hierarchy.cmi \
- lib/cps.cmx basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
- basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
- basic_ag/bagReduction.cmi basic_ag/bagOutput.cmi basic_ag/bag.cmx \
- automath/autProcess.cmi automath/autParser.cmi automath/autOutput.cmi \
- automath/autLexer.cmx
+ toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
+ toplevel/metaBag.cmi toplevel/metaAut.cmi lib/log.cmi common/library.cmi \
+ common/hierarchy.cmi lib/cps.cmx basic_rg/brgUntrusted.cmi \
+ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi basic_rg/brg.cmx \
+ basic_ag/bagUntrusted.cmi basic_ag/bagReduction.cmi \
+ basic_ag/bagOutput.cmi basic_ag/bag.cmx automath/autProcess.cmi \
+ automath/autParser.cmi automath/autOutput.cmi automath/autLexer.cmx
toplevel/top.cmx: lib/time.cmx common/output.cmx lib/nUri.cmx \
- toplevel/metaOutput.cmx toplevel/metaBrg.cmx toplevel/metaBag.cmx \
- toplevel/metaAut.cmx lib/log.cmx common/library.cmx common/hierarchy.cmx \
- lib/cps.cmx basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
- basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
- basic_ag/bagReduction.cmx basic_ag/bagOutput.cmx basic_ag/bag.cmx \
- automath/autProcess.cmx automath/autParser.cmx automath/autOutput.cmx \
- automath/autLexer.cmx
+ toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
+ toplevel/metaBag.cmx toplevel/metaAut.cmx lib/log.cmx common/library.cmx \
+ common/hierarchy.cmx lib/cps.cmx basic_rg/brgUntrusted.cmx \
+ basic_rg/brgReduction.cmx basic_rg/brgOutput.cmx basic_rg/brg.cmx \
+ basic_ag/bagUntrusted.cmx basic_ag/bagReduction.cmx \
+ basic_ag/bagOutput.cmx basic_ag/bag.cmx automath/autProcess.cmx \
+ automath/autParser.cmx automath/autOutput.cmx automath/autLexer.cmx
CLEAN = log.txt
-TAGS = test test-si meta export-si
+TAGS = test test-si test-si-fast hir xml-si
include Makefile.common
INPUT-ORIG = automath/grundlagen-orig.aut
test: $(MAIN).opt
- @echo " HELENA $(INPUT)"
- $(H)./$(MAIN).opt -S 3 $(O) $(INPUT) > log.txt
+ @echo " HELENA -a -c $(INPUT)"
+ $(H)./$(MAIN).opt -a -c -S 3 $(O) $(INPUT) > log.txt
test-si: $(MAIN).opt
- @echo " HELENA -c -u $(INPUT)"
- $(H)./$(MAIN).opt -c -u -S 3 $(O) $(INPUT) > log.txt
+ @echo " HELENA -a -c -u $(INPUT)"
+ $(H)./$(MAIN).opt -a -c -u -S 3 $(O) $(INPUT) > log.txt
-meta: $(MAIN).opt
- @echo " HELENA -m meta.txt $(INPUT)"
- $(H)./$(MAIN).opt -m meta.txt -s 1 -S 1 $(INPUT) > log.txt
- $(H)$(GZIP) meta.txt
+test-si-fast: $(MAIN).opt
+ @echo " HELENA -u $(INPUT)"
+ $(H)./$(MAIN).opt -u -S 1 $(O) $(INPUT) > log.txt
-export-si: $(MAIN).opt
- @echo " HELENA -u -x xml $(INPUT)"
- $(H)./$(MAIN).opt -u -x xml -s 2 -S 1 $(INPUT) > log.txt
+hir: $(MAIN).opt
+ @echo " HELENA -m $(INPUT)"
+ $(H)./$(MAIN).opt -m -s 1 -S 1 $(INPUT) > log.txt
+
+xml-si: $(MAIN).opt
+ @echo " HELENA -u -x $(INPUT)"
+ $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > log.txt
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
TAR = tar -czf $(MAIN:%=%.tgz)
-GZIP = gzip
define DIR_TEMPLATE
MODULES += $$(addprefix $(1)/,$$(shell cat $(1)/Make))
let rec pp_term c frm = function
| B.Sort h ->
- let f = function
- | Some s -> F.fprintf frm "@[%s@]" s
- | None -> F.fprintf frm "@[*%u@]" h
- in
- H.get_sort f h
+ let err () = F.fprintf frm "@[*%u@]" h in
+ let f s = F.fprintf frm "@[%s@]" s in
+ H.get_sort err f h
| B.LRef i ->
let f = function
| Some (id, _) -> F.fprintf frm "@[%s@]" id
(* context/term pretty printing *********************************************)
let id frm a =
- let err () = assert false in
let f n = function
| true -> F.fprintf frm "%s" n
| false -> F.fprintf frm "^%s" n
in
- B.name err f a
+ B.name C.err f a
let rec pp_term c frm = function
| B.Sort (_, h) ->
- let f = function
- | Some s -> F.fprintf frm "@[%s@]" s
- | None -> F.fprintf frm "@[*%u@]" h
- in
- H.get_sort f h
+ let err () = F.fprintf frm "@[*%u@]" h in
+ let f s = F.fprintf frm "@[%s@]" s in
+ H.get_sort err f h
| B.LRef (_, i) ->
let err i = F.fprintf frm "@[#%u@]" i in
let f _ a _ = F.fprintf frm "@[%a@]" id a in
in
raise (TypeError (L.ct_items3 sc c st1 t1 st2 t2 st3 t3))
-let err () = assert false
-
let get f m i =
B.get error0 f m.c i
f {m with c = c} None x
| b ->
let f e = f {m with c = c} (Some (e, b)) x in
- B.apix err f a
+ B.apix C.err f a
in
get f m i
| B.Cast (_, _, t) ->
let f i = index := i; f i in
C.list_fold_left f set_sort !index ss
-let get_sort f h =
- try f (Some (H.find sort h))
- with Not_found -> f None
+let get_sort err f h =
+ try f (H.find sort h) with Not_found -> err ()
let string_of_graph f (s, _) = f s
let apply f (_, g) h = f (g h)
-let graph_of_string f s =
+let graph_of_string err f s =
try
let x = S.sscanf s "Z%u" C.start in
- if x > 0 then f (Some (s, fun h -> x + h)) else f None
+ if x > 0 then f (s, fun h -> x + h) else err ()
with
- S.Scan_failure _ | Failure _ | End_of_file -> f None
-
-let graph =
- ref (graph_of_string (function Some g -> g | None -> assert false) "Z2")
+ S.Scan_failure _ | Failure _ | End_of_file -> err ()
val set_new_sorts: (int -> 'a) -> string list -> 'a
-val get_sort: (string option -> 'a) -> int -> 'a
+val get_sort: (unit -> 'a) -> (string -> 'a) -> int -> 'a
-val graph_of_string: (graph option -> 'a) -> string -> 'a
+val graph_of_string: (unit -> 'a) -> (graph -> 'a) -> string -> 'a
val string_of_graph: (string -> 'a) -> graph -> 'a
val apply: (int -> 'a) -> graph -> int -> 'a
-
-val graph: graph ref
(* internal functions *******************************************************)
+let base = "xml"
+
let obj_ext = ".ld.xml"
-let system = "http://helm.cs.unibo.it/lambda-delta/xml/ld.dtd"
+let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
-let path_of_uri base uri =
+let path_of_uri uri =
F.concat base (Str.string_after (U.string_of_uri uri) 3)
let pp_head frm =
(* interface functions ******************************************************)
-let export_item export_obj si g base = function
+let export_item export_obj si g = function
| Some obj ->
let _, uri, bind = obj in
- let path = path_of_uri base uri in
+ let path = path_of_uri uri in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let och = open_out (path ^ obj_ext) in
let frm = Format.formatter_of_out_channel och in
val export_item:
(Format.formatter -> 'bind Item.obj -> unit) ->
- bool -> Hierarchy.graph -> string -> 'bind Item.item -> unit
+ bool -> Hierarchy.graph -> 'bind Item.item -> unit
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+let err () = assert false
+
let start x = x
let id f x = f x
--- /dev/null
+parsed : 0.7
+intermediate: 1.6
+untrusted : 0.4
+trusted : 6.5 + 3 with upsilon relocations
+------------------
+total : 9.2
-meta metaOutput metaAut metaBag metaBrg top
+meta metaOutput metaLibrary metaAut metaBag metaBrg top
--- /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 F = Format
+module O = MetaOutput
+
+type out_channel = Pervasives.out_channel * F.formatter
+
+(* internal functions *******************************************************)
+
+let hal_dir = "hal"
+
+let hal_ext = ".hal"
+
+(* interface functions ******************************************************)
+
+let open_out f name =
+ let _ = Sys.command (Printf.sprintf "mkdir -p %s" hal_dir) in
+ let och = open_out (Filename.concat hal_dir (name ^ hal_ext)) in
+ let frm = F.formatter_of_out_channel och in
+ F.pp_set_margin frm max_int;
+ f (och, frm)
+
+let write_item f (_, frm) item =
+ O.pp_item f frm item
+
+let close_out f (och, _) =
+ close_out och; f ()
--- /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 out_channel
+
+val open_out: (out_channel -> 'a) -> string -> 'a
+
+val write_item: (unit -> 'a) -> out_channel -> Meta.item -> 'a
+
+val close_out: (unit -> 'a) -> out_channel -> 'a
module AO = AutOutput
module MA = MetaAut
module MO = MetaOutput
+module ML = MetaLibrary
module MBrg = MetaBrg
module G = Library
module BrgO = BrgOutput
| BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item}
| BagItem item -> {st with bagc = count BagO.count_item st.bagc item}
-let export_item si g base = function
- | BrgItem item -> G.export_item BrgO.export_obj si g base item
+let export_item si g = function
+ | BrgItem item -> G.export_item BrgO.export_obj si g item
| BagItem _ -> ()
let type_check f st si g k =
try
let version_string = "Helena 0.8.0 M - August 2009" in
let stage = ref 3 in
- let meta_file = ref None in
+ let moch = ref None in
+ let meta = ref false in
let progress = ref false in
+ let process = ref false in
let use_cover = ref true in
let si = ref false in
- let library_dir = ref None in
+ let export = ref false in
+ let graph = ref (H.graph_of_string C.err C.start "Z2") in
let set_hierarchy s =
- let f = function
- | Some g -> H.graph := g
- | None -> L.warn (P.sprintf "Unknown type hierarchy: %s" s)
- in
- H.graph_of_string f s
+ let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in
+ let f g = graph := g in
+ H.graph_of_string err f s
in
let set_kernel = function
| "brg" -> kernel := Brg
let set_summary i = L.level := i in
let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_stage i = stage := i in
- let close = function
- | None -> ()
- | Some (och, _) -> close_out och
- in
let set_meta_file name =
- close !meta_file;
- let och = open_out name in
- let frm = Format.formatter_of_out_channel och in
- Format.pp_set_margin frm max_int;
- meta_file := Some (och, frm)
+ let f och = moch := Some och in
+ ML.open_out f name
in
- let set_library_dir name =
- library_dir := Some name
+ let close = function
+ | None -> ()
+ | Some och -> ML.close_out C.start och
in
let read_file name =
if !L.level > 0 then T.gmtime version_string;
if !L.level > 1 then
L.warn (P.sprintf "Processing file: %s" name);
if !L.level > 0 then T.utime_stamp "started";
+ let base_name = Filename.chop_extension (Filename.basename name) in
+ if !meta then set_meta_file base_name;
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
let book = AutParser.book AutLexer.token lexbuf in
(* stage 2 *)
let f st item =
let st = count_item st item in
- begin match !library_dir with
- | None -> ()
- | Some base -> export_item !si !H.graph base item
- end;
- if !stage > 2 then type_check f st !si !H.graph item else st
+ if !export then export_item !si !graph item;
+ if !stage > 2 then type_check f st !si !graph item else st
in
(* stage 1 *)
let f st mst item =
let st = {st with
mst = mst; mc = count MO.count_item st.mc item
} in
- begin match !meta_file with
- | None -> ()
- | Some (_, frm) -> MO.pp_item C.start frm item
+ begin match !moch with
+ | None -> ()
+ | Some och -> ML.write_item C.start och item
end;
if !stage > 1 then kernel_of_meta f st item else st
in
in
aux st tl
in
- process_item f st item
+ if !process then process_item f st item else f st item
in
O.clear_reductions ();
- let cover =
- if !use_cover then Filename.chop_extension (Filename.basename name)
- else ""
- in
+ let cover = if !use_cover then base_name else "" in
let st = aux (initial_status cover) book in
if !L.level > 0 then T.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 && !process 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 exit () =
+ close !moch;
+ if !L.level > 0 then T.utime_stamp "at exit";
+ flush ()
+ in
let help =
- "Usage: helena [ -Vcipu | -Ss <number> | -m <file> | -hk <string> ] <file> ...\n\n" ^
- "Summary levels: 0 just errors, 1 time stamps, 2 processed file names, \
+ "Usage: helena [ -Vacimpux | -Ss <number> | -hk <string> ] <file> ...\n\n" ^
+ "Summary levels: 0 just errors (default), 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"
+ "Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
in
- let help_S = "<number> set summary level" in
+ let help_S = "<number> set summary level (see above)" in
let help_V = " show version information" in
+
+ let help_a = " analyze source files" in
let help_c = " disable initial segment of URI hierarchy" in
- let help_h = "<string> set type hierarchy" in
+ let help_h = "<string> set type hierarchy (default: Z2)" in
let help_i = " show local references by index" in
- let help_k = "<string> set kernel version" in
- let help_m = "<file> output intermediate representation" in
+ let help_k = "<string> set kernel version (default: brg)" in
+ let help_m = " output intermediate representation (HAL)" in
let help_p = " activate progress indicator" in
let help_u = " activate sort inclusion" in
- let help_s = "<number> Set translation stage" in
- let help_x = "<directory> export kernel objects (XML)" in
+ let help_s = "<number> set translation stage (see above)" in
+ let help_x = " export kernel objects (XML)" in
L.box 0; L.box_err ();
H.set_new_sorts ignore ["Set"; "Prop"];
+ at_exit exit;
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
+ ("-a", Arg.Set process, help_a);
("-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);
- ("-m", Arg.String set_meta_file, help_m);
+ ("-m", Arg.Set meta, help_m);
("-p", Arg.Set progress, help_p);
("-u", Arg.Set si, help_u);
("-s", Arg.Int set_stage, help_s);
- ("-x", Arg.String set_library_dir, help_x)
+ ("-x", Arg.Set export, help_x)
] read_file help;
- if !L.level > 0 then T.utime_stamp "at exit";
- flush ()
with BagR.TypeError msg -> bag_error "Type Error" msg
| BrgR.TypeError msg -> brg_error "Type Error" msg
projects / helm.git / commitdiff