From a3b9fc77770f42070632bcb575546678025e09b2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 3 Aug 2010 20:54:58 +0000 Subject: [PATCH] - we simplified the parser return values - now the display of parser and lexer debug information is controlled from the command line (with the options -P and -L) complete_rg: now the empty binders are not treated especially top: we isolated a fragment of slow code (process_streaming) to be investigated. It can be enabled with the -1 command line option) Makefile: we now create the etc directory when it is missing --- helm/software/lambda-delta/.depend.opt | 14 +-- helm/software/lambda-delta/Makefile | 28 +++--- .../lambda-delta/automath/autLexer.mll | 3 +- .../lambda-delta/automath/autParser.mly | 40 ++++----- helm/software/lambda-delta/common/options.ml | 17 ++-- helm/software/lambda-delta/complete_rg/crg.ml | 9 -- helm/software/lambda-delta/text/txtLexer.mll | 4 +- helm/software/lambda-delta/text/txtParser.mly | 33 ++++--- helm/software/lambda-delta/toplevel/top.ml | 86 ++++++++++++------- 9 files changed, 128 insertions(+), 106 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index d85664986..4d5194ea4 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -28,10 +28,10 @@ common/library.cmx: lib/nUri.cmx common/hierarchy.cmx common/entity.cmx \ 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 @@ -46,8 +46,10 @@ automath/autOutput.cmo: lib/log.cmi lib/cps.cmx automath/autProcess.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 diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile index 3d8b6be48..6a0724a87 100644 --- a/helm/software/lambda-delta/Makefile +++ b/helm/software/lambda-delta/Makefile @@ -19,32 +19,36 @@ HOME = . 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: @@ -74,18 +78,18 @@ install-xml: etc/make-html.sh # 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 diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll index 51f1e7cb9..cb33d0c3f 100644 --- a/helm/software/lambda-delta/automath/autLexer.mll +++ b/helm/software/lambda-delta/automath/autLexer.mll @@ -14,8 +14,7 @@ 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 = diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly index ed5da5a64..e90ba3b7c 100644 --- a/helm/software/lambda-delta/automath/autParser.mly +++ b/helm/software/lambda-delta/automath/autParser.mly @@ -24,11 +24,10 @@ */ %{ + module O = Options module A = Aut - let debug = false - - let _ = Parsing.set_trace debug + let _ = Parsing.set_trace !O.debug_parser %} %token NUM %token IDENT @@ -36,7 +35,7 @@ %token TYPE PROP DEF EB E PN EXIT %start entry - %type entry + %type entry %% path: MINUS {} | FS {} ; oftype: CN {} | CM {} ; @@ -81,22 +80,21 @@ | 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 } + ; diff --git a/helm/software/lambda-delta/common/options.ml b/helm/software/lambda-delta/common/options.ml index 53693174b..d9783c766 100644 --- a/helm/software/lambda-delta/common/options.ml +++ b/helm/software/lambda-delta/common/options.ml @@ -15,17 +15,21 @@ type uri_generator = string -> string (* 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) @@ -34,4 +38,5 @@ let get_mk_uri () = let clear () = expand := false; si := false; cover := ""; indexes := false; icm := 0; + debug_parser := false; debug_lexer := false; mk_uri := fun _ _ -> C.err diff --git a/helm/software/lambda-delta/complete_rg/crg.ml b/helm/software/lambda-delta/complete_rg/crg.ml index 0b0853386..0b02f1c48 100644 --- a/helm/software/lambda-delta/complete_rg/crg.ml +++ b/helm/software/lambda-delta/complete_rg/crg.ml @@ -56,9 +56,6 @@ let push2 err f lenv attr ?t () = match lenv, t with 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 @@ -69,9 +66,6 @@ let resolve_lref err f id lenv = 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 @@ -84,9 +78,6 @@ let rec get_name err f i j = function 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, _) -> diff --git a/helm/software/lambda-delta/text/txtLexer.mll b/helm/software/lambda-delta/text/txtLexer.mll index 073fabcba..624454b67 100644 --- a/helm/software/lambda-delta/text/txtLexer.mll +++ b/helm/software/lambda-delta/text/txtLexer.mll @@ -11,10 +11,10 @@ { 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 = "\\" diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly index 6aafbb551..694e30891 100644 --- a/helm/software/lambda-delta/text/txtParser.mly +++ b/helm/software/lambda-delta/text/txtParser.mly @@ -24,11 +24,10 @@ */ %{ + module O = Options module T = Txt - let debug = false - - let _ = Parsing.set_trace debug + let _ = Parsing.set_trace !O.debug_parser %} %token IX %token ID STR @@ -36,7 +35,7 @@ %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF %start entry - %type entry + %type entry %nonassoc CP CB CA %right WTO STO @@ -124,33 +123,31 @@ ; 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 } ; diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml index 245c00d4a..57bdfdae8 100644 --- a/helm/software/lambda-delta/toplevel/top.ml +++ b/helm/software/lambda-delta/toplevel/top.ml @@ -165,6 +165,7 @@ type input = Text | Automath 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 @@ -186,18 +187,18 @@ let gen_text command = 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 -> @@ -221,6 +222,7 @@ let cc = ref false 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 @@ -236,36 +238,52 @@ let process_1 st entity = 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 @@ -292,7 +310,8 @@ try 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; @@ -326,11 +345,13 @@ try flush_all () in let help = - "Usage: helena [ -VXcgijmopqu | -Ss | -x | -hkr ]* [ ]*\n\n" ^ + "Usage: helena [ -LPVXcgijmopqu1 | -Ss | -x | -hkr ]* [ ]*\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 = " set summary level (see above)" in let help_V = " show version information" in let help_X = " clear options" in @@ -349,9 +370,13 @@ try let help_s = " set translation stage (see above)" in let help_u = " activate sort inclusion" in let help_x = " export kernel entities (XML) to " 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); @@ -363,11 +388,12 @@ try ("-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 -- 2.39.2