text/txt.cmo:
text/txt.cmx:
text/txtParser.cmi: text/txt.cmx
-text/txtParser.cmo: text/txt.cmx text/txtParser.cmi
-text/txtParser.cmx: text/txt.cmx text/txtParser.cmi
-text/txtLexer.cmo: text/txtParser.cmi lib/log.cmi
-text/txtLexer.cmx: text/txtParser.cmx lib/log.cmx
+text/txtParser.cmo: text/txt.cmx common/options.cmx text/txtParser.cmi
+text/txtParser.cmx: text/txt.cmx common/options.cmx text/txtParser.cmi
+text/txtLexer.cmo: text/txtParser.cmi common/options.cmx lib/log.cmi
+text/txtLexer.cmx: text/txtParser.cmx common/options.cmx lib/log.cmx
text/txtTxt.cmi: text/txt.cmx
text/txtTxt.cmo: text/txt.cmx lib/cps.cmx text/txtTxt.cmi
text/txtTxt.cmx: text/txt.cmx lib/cps.cmx text/txtTxt.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
+automath/autParser.cmo: common/options.cmx automath/aut.cmx \
+ automath/autParser.cmi
+automath/autParser.cmx: common/options.cmx automath/aut.cmx \
+ automath/autParser.cmi
automath/autLexer.cmo: common/options.cmx lib/log.cmi automath/autParser.cmi
automath/autLexer.cmx: common/options.cmx lib/log.cmx automath/autParser.cmx
basic_ag/bag.cmo: lib/log.cmi common/entity.cmx lib/cps.cmx
INPUT = examples/grundlagen/grundlagen.aut
-test-si: $(MAIN).opt
+test-si: $(MAIN).opt etc
@echo " HELENA -p -u $(INPUT)"
$(H)./$(MAIN).opt -p -u -S 3 $(O) $(INPUT) > etc/log.txt
-test-si-fast: $(MAIN).opt
+test-si-fast: $(MAIN).opt etc
@echo " HELENA -u -q $(INPUT)"
$(H)./$(MAIN).opt -u -q -S 1 $(O) $(INPUT) > etc/log.txt
-profile: $(MAIN).opt
+profile: $(MAIN).opt etc
@echo " HELENA -u -q $(INPUT) (30 TIMES)"
$(H)rm etc/log.txt
- $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 0 -S 1 $(O) $(INPUT) >> etc/log.txt; done
- $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt
+ $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done
+ $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
-hal: $(MAIN).opt
+hal: $(MAIN).opt etc
@echo " HELENA -o -x -m $(INPUT)"
$(H)./$(MAIN).opt -o -x $(HOME) -m -s 1 -S 1 $(INPUT) > etc/log.txt
-xml-si: $(MAIN).opt
+xml-si: $(MAIN).opt etc
@echo " HELENA -u -x -s 2 $(INPUT)"
$(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
-xml-si-crg: $(MAIN).opt
+xml-si-crg: $(MAIN).opt etc
@echo " HELENA -u -x -s 1 $(INPUT)"
$(H)./$(MAIN).opt -u -x $(HOME) -s 1 -S 1 $(INPUT) > etc/log.txt
+etc:
+ @echo " MKDIR etc"
+ $(H)mkdir etc
+
%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
%.ld:
# old targets ##########################################################
-test: $(MAIN).opt
+test: $(MAIN).opt etc
@echo " HELENA -o -p $(INPUT)"
$(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt
-test-si-old: $(MAIN).opt
+test-si-old: $(MAIN).opt etc
@echo " HELENA -o -p -u $(INPUT)"
$(H)./$(MAIN).opt -o -p -u -S 3 $(O) $(INPUT) > etc/log.txt
-test-si-fast-old: $(MAIN).opt
+test-si-fast-old: $(MAIN).opt etc
@echo " HELENA -o -u -q $(INPUT)"
$(H)./$(MAIN).opt -o -u -q -S 1 $(O) $(INPUT) > etc/log.txt
-xml-si-old: $(MAIN).opt
+xml-si-old: $(MAIN).opt etc
@echo " HELENA -o -u -x -s 2 $(INPUT)"
$(H)./$(MAIN).opt -o -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
module O = Options
module P = AutParser
- let debug = false
- let out s = if debug then L.warn s else ()
+ let out s = if !O.debug_lexer then L.warn s else ()
(* This turns an Automath identifier into an XML nmtoken *)
let quote id =
*/
%{
+ module O = Options
module A = Aut
- let debug = false
-
- let _ = Parsing.set_trace debug
+ let _ = Parsing.set_trace !O.debug_parser
%}
%token <int> NUM
%token <string> IDENT
%token TYPE PROP DEF EB E PN EXIT
%start entry
- %type <Aut.command option * bool> entry
+ %type <Aut.command option> entry
%%
path: MINUS {} | FS {} ;
oftype: CN {} | CM {} ;
| star {} | IDENT {} | OB {}
;
entity:
- | PLUS IDENT { Some (A.Section (Some (true, $2))) }
- | PLUS TIMES IDENT { Some (A.Section (Some (false, $3))) }
- | MINUS IDENT { Some (A.Section None) }
- | EXIT { Some (A.Section None) }
- | star { Some (A.Context None) }
- | qid star { Some (A.Context (Some $1)) }
- | IDENT DEF EB sc term { Some (A.Block ($1, $5)) }
- | IDENT sc term DEF EB { Some (A.Block ($1, $3)) }
- | OB IDENT oftype term CB { Some (A.Block ($2, $4)) }
- | IDENT DEF PN sc term { Some (A.Decl ($1, $5)) }
- | IDENT sc term DEF PN { Some (A.Decl ($1, $3)) }
- | IDENT DEF expand term sc term { Some (A.Def ($1, $6, $3, $4)) }
- | IDENT sc term DEF expand term { Some (A.Def ($1, $3, $5, $6)) }
- | eof { None }
+ | 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) }
;
entry:
- | entity { $1, false }
- | entity start { $1, true }
-
+ | entity start { Some $1 }
+ | eof { None }
+ ;
(* interface functions ******************************************************)
-let indexes = ref false (* show de Bruijn indexes *)
+let indexes = ref false (* show de Bruijn indexes *)
-let expand = ref false (* always expand global definitions *)
+let expand = ref false (* always expand global definitions *)
-let si = ref false (* use sort inclusion *)
+let si = ref false (* use sort inclusion *)
-let unquote = ref false (* do not quote identifiers when lexing *)
+let unquote = ref false (* do not quote identifiers when lexing *)
-let icm = ref 0 (* complexity measure of relocated terms *)
+let icm = ref 0 (* complexity measure of relocated terms *)
-let cover = ref "" (* initial uri segment *)
+let cover = ref "" (* initial uri segment *)
+
+let debug_parser = ref false (* output parser debug information *)
+
+let debug_lexer = ref false (* output lexer debug information *)
let mk_uri = ref (fun _ _ -> C.err : bool -> string -> uri_generator)
let clear () =
expand := false; si := false; cover := ""; indexes := false; icm := 0;
+ debug_parser := false; debug_lexer := false;
mk_uri := fun _ _ -> C.err
let resolve_lref err f id lenv =
let rec aux f i k = function
| ESort -> err ()
- | EBind (tl, _, Abst [])
- | EBind (tl, _, Abbr [])
- | EBind (tl, _, Void 0) -> aux f i k tl
| EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
let f j = f i j (k + j) in
let rec get_name err f i j = function
| ESort -> err i
- | EBind (tl, _, Abst [])
- | EBind (tl, _, Abbr [])
- | EBind (tl, _, Void 0) -> get_name err f i j tl
| EBind (_, a, _) when i = 0 ->
let err () = err i in
Entity.get_name err f j a
let get_index err f i j lenv =
let rec aux f i k = function
| ESort -> err i
- | EBind (tl, _, Abst [])
- | EBind (tl, _, Abbr [])
- | EBind (tl, _, Void 0) -> aux f i k tl
| EBind (_, a, _) when i = 0 ->
if Entity.count_names a > j then f (k + j) else err i
| EBind (tl, a, _) ->
{
module L = Log
+ module O = Options
module P = TxtParser
- let debug = false
- let out s = if debug then L.warn s else ()
+ let out s = if !O.debug_lexer then L.warn s else ()
}
let BS = "\\"
*/
%{
+ module O = Options
module T = Txt
- let debug = false
-
- let _ = Parsing.set_trace debug
+ let _ = Parsing.set_trace !O.debug_parser
%}
%token <int> IX
%token <string> ID STR
%token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
%start entry
- %type <Txt.command option * bool> entry
+ %type <Txt.command option> entry
%nonassoc CP CB CA
%right WTO STO
;
xentity:
| GRAPH ID
- { Some (T.Graph $2) }
+ { T.Graph $2 }
| decl comment ID CN term
- { Some (T.Entity ($1, $3, $2, $5)) }
+ { T.Entity ($1, $3, $2, $5) }
| def comment ID EQ term
- { Some (T.Entity ($1, $3, $2, $5)) }
+ { T.Entity ($1, $3, $2, $5) }
| def comment ID EQ term CN term
- { Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+ { T.Entity ($1, $3, $2, T.Cast ($7, $5)) }
| GEN term
- { Some (T.Generate [$2]) }
+ { T.Generate [$2] }
| GEN terms
- { Some (T.Generate $2) }
+ { T.Generate $2 }
| REQ ids
- { Some (T.Require $2) }
+ { T.Require $2 }
| OPEN ID
- { Some (T.Section (Some $2)) }
+ { T.Section (Some $2) }
| CLOSE
- { Some (T.Section None) }
+ { T.Section None }
| SORTS sorts
- { Some (T.Sorts $2) }
- | EOF
- { None }
+ { T.Sorts $2 }
;
start:
| GRAPH {} | decl {} | def {} | GEN {} |
| REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
;
entry:
- | xentity { $1, false }
- | xentity start { $1, true }
+ | xentity start { Some $1 }
+ | EOF { None }
;
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 / commitdiff