type input_entity = TxtEntity of Txt.command
| AutEntity of Aut.command
+ | NoEntity
let type_of_input name =
if F.check_suffix name ".hln" then Text
parbuf := TxtEntity command :: !parbuf
let entity_of_input lexbuf i = match i, !parbuf with
+ | Automath, _ ->
+ begin match AutParser.entry (token aut_xl) lexbuf with
+ | Some e -> aut_xl.unget <- true; AutEntity e
+ | None -> NoEntity
+ end
| Text, [] ->
begin match TxtParser.entry (token txt_xl) lexbuf with
- | Some e, unget -> txt_xl.unget <- unget; Some (TxtEntity e)
- | None, _ -> None
+ | Some e -> txt_xl.unget <- true; TxtEntity e
+ | None -> NoEntity
end
| Text, hd :: tl ->
- parbuf := tl; Some hd
- | Automath, _ ->
- begin match AutParser.entry (token aut_xl) lexbuf with
- | Some e, unget -> aut_xl.unget <- unget; Some (AutEntity e)
- | None, _ -> None
- end
+ parbuf := tl; hd
let process_input f st = function
| AutEntity e ->
let export = ref ""
let old = ref false
let st = ref (initial_status ())
+let streaming = ref false (* parsing style (temporary) *)
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
let process_0 st entity =
let f st entity =
if !stage = 0 then st else
- let frr mst = {st with mst = mst} in
- let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
- let err dst = {st with dst = dst} in
- let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
- let crr tst = {st with tst = tst} in
- let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
match entity, !old with
- | AutEntity e, true -> MA.meta_of_aut frr h st.mst e
- | AutEntity e, false -> DA.crg_of_aut err g st.dst e
- | TxtEntity e, false -> DT.crg_of_txt crr d gen_text st.tst e
- | _ -> assert false
+ | AutEntity e, true ->
+ let frr mst = {st with mst = mst} in
+ let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
+ MA.meta_of_aut frr h st.mst e
+ | AutEntity e, false ->
+ let err dst = {st with dst = dst} in
+ let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
+ DA.crg_of_aut err g st.dst e
+ | TxtEntity e, _ ->
+ let crr tst = {st with tst = tst} in
+ let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
+ DT.crg_of_txt crr d gen_text st.tst e
+ | NoEntity, _ -> assert false
in
let st = if !L.level > 2 then count_input st entity else st in
if !preprocess then process_input f st entity else f st entity
+let process_nostreaming st lexbuf input =
+ let rec aux1 book = match entity_of_input lexbuf input with
+ | NoEntity -> List.rev book
+ | e -> aux1 (e :: book)
+ in
+ let rec aux2 st = function
+ | [] -> st
+ | entity :: tl -> aux2 (process_0 st entity) tl
+ in
+ aux2 st (aux1 [])
+
+let rec process_streaming st lexbuf input = match entity_of_input lexbuf input with
+ | NoEntity -> st
+ | e -> process_streaming (process_0 st e) lexbuf input
+
+(****************************************************************************)
+
let process st name =
+ let process = if !streaming then process_streaming else process_nostreaming in
let input = type_of_input name in
let ich = open_in name in
let lexbuf = Lexing.from_channel ich in
- let rec aux st = match entity_of_input lexbuf input with
- | None -> close_in ich; st, input
- | Some e -> aux (process_0 st e)
- in
- aux st
-
-(****************************************************************************)
+ let st = process st lexbuf input in
+ close_in ich; st, input
let main =
try
- let version_string = "Helena 0.8.1 M - February 2010" in
+ let version_string = "Helena 0.8.1 M - August 2010" in
let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_hierarchy s =
if H.set_graph s then () else
stage := 3; moch := None; meta := false; progress := false;
preprocess := false; root := ""; cc := false; export := "";
old := false; kernel := Brg; st := initial_status ();
- L.clear (); O.clear (); H.clear (); Op.clear_reductions ()
+ L.clear (); O.clear (); H.clear (); Op.clear_reductions ();
+ streaming := false;
in
let process_file name =
if !L.level > 0 then T.gmtime version_string;
flush_all ()
in
let help =
- "Usage: helena [ -VXcgijmopqu | -Ss <number> | -x <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
+ "Usage: helena [ -LPVXcgijmopqu1 | -Ss <number> | -x <dir> | -hkr <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 (default)\n"
in
+ let help_L = " show lexer debug information" in
+ let help_P = " show parser debug information" in
let help_S = "<number> set summary level (see above)" in
let help_V = " show version information" in
let help_X = " clear options" in
let help_s = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
let help_x = "<dir> export kernel entities (XML) to <dir>" in
+
+ let help_1 = " parse files with streaming policy" in
L.box 0; L.box_err ();
at_exit exit;
Arg.parse [
+ ("-L", Arg.Set O.debug_lexer, help_L);
+ ("-P", Arg.Set O.debug_parser, help_P);
("-S", Arg.Int set_summary, help_S);
("-V", Arg.Unit print_version, help_V);
("-X", Arg.Unit clear_options, help_X);
("-k", Arg.String set_kernel, help_k);
("-m", Arg.Set meta, help_m);
("-o", Arg.Set old, help_o);
- ("-p", Arg.Set preprocess, help_p);
+ ("-p", Arg.Set preprocess, help_p);
("-q", Arg.Set O.unquote, help_q);
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set O.si, help_u);
- ("-x", Arg.String set_xdir, help_x)
+ ("-x", Arg.String set_xdir, help_x);
+ ("-1", Arg.Set streaming, help_1);
] process_file help;
with BagT.TypeError msg -> bag_error "Type Error" msg
projects / helm.git / blobdiff