From: Ferruccio Guidi Date: Wed, 12 Nov 2014 21:47:20 +0000 (+0000) Subject: new message reporting system improves performance significatively X-Git-Tag: make_still_working~797 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f72311aa07e71090a24eef9e4fb97cc2e95e6b16;p=helm.git new message reporting system improves performance significatively --- diff --git a/helm/software/helena/.depend.opt b/helm/software/helena/.depend.opt index 8f1a57695..b2015af33 100644 --- a/helm/software/helena/.depend.opt +++ b/helm/software/helena/.depend.opt @@ -3,8 +3,8 @@ src/lib/cps.cmx: src/lib/share.cmo: src/lib/share.cmx: src/lib/log.cmi: -src/lib/log.cmo: src/lib/cps.cmx src/lib/log.cmi -src/lib/log.cmx: src/lib/cps.cmx src/lib/log.cmi +src/lib/log.cmo: src/lib/log.cmi +src/lib/log.cmx: src/lib/log.cmi src/lib/time.cmo: src/lib/log.cmi src/lib/time.cmx: src/lib/log.cmx src/common/hierarchy.cmi: @@ -142,37 +142,41 @@ src/basic_rg/brgSubstitution.cmx: src/common/options.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi: src/common/status.cmx src/lib/log.cmi \ src/common/entity.cmx src/basic_rg/brg.cmx src/basic_rg/brgReduction.cmo: src/common/status.cmx src/lib/share.cmx \ - src/common/output.cmi src/lib/log.cmi src/common/level.cmi \ - src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ - src/common/ccs.cmi src/basic_rg/brgOutput.cmi \ + src/common/output.cmi src/common/options.cmx src/lib/log.cmi \ + src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ + src/lib/cps.cmx src/common/ccs.cmi src/basic_rg/brgOutput.cmi \ src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brgReduction.cmx: src/common/status.cmx src/lib/share.cmx \ - src/common/output.cmx src/lib/log.cmx src/common/level.cmx \ - src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ - src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ + src/common/output.cmx src/common/options.cmx src/lib/log.cmx \ + src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/common/ccs.cmx src/basic_rg/brgOutput.cmx \ src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brgValidity.cmi: src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx -src/basic_rg/brgValidity.cmo: src/lib/log.cmi src/common/entity.cmx \ - src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi -src/basic_rg/brgValidity.cmx: src/lib/log.cmx src/common/entity.cmx \ - src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgValidity.cmi +src/basic_rg/brgValidity.cmo: src/common/status.cmx src/common/options.cmx \ + src/lib/log.cmi src/common/entity.cmx src/basic_rg/brgReduction.cmi \ + src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgValidity.cmi +src/basic_rg/brgValidity.cmx: src/common/status.cmx src/common/options.cmx \ + src/lib/log.cmx src/common/entity.cmx src/basic_rg/brgReduction.cmx \ + src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgValidity.cmi src/basic_rg/brgType.cmi: src/common/status.cmx src/basic_rg/brgReduction.cmi \ src/basic_rg/brg.cmx -src/basic_rg/brgType.cmo: src/lib/share.cmx src/lib/log.cmi \ - src/common/level.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brgSubstitution.cmi \ - src/basic_rg/brgReduction.cmi src/basic_rg/brgEnvironment.cmi \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi -src/basic_rg/brgType.cmx: src/lib/share.cmx src/lib/log.cmx \ - src/common/level.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_rg/brgSubstitution.cmx \ - src/basic_rg/brgReduction.cmx src/basic_rg/brgEnvironment.cmx \ - src/basic_rg/brg.cmx src/basic_rg/brgType.cmi +src/basic_rg/brgType.cmo: src/common/status.cmx src/lib/share.cmx \ + src/common/options.cmx src/lib/log.cmi src/common/level.cmi \ + src/common/hierarchy.cmi src/common/entity.cmx src/lib/cps.cmx \ + src/basic_rg/brgSubstitution.cmi src/basic_rg/brgReduction.cmi \ + src/basic_rg/brgEnvironment.cmi src/basic_rg/brg.cmx \ + src/basic_rg/brgType.cmi +src/basic_rg/brgType.cmx: src/common/status.cmx src/lib/share.cmx \ + src/common/options.cmx src/lib/log.cmx src/common/level.cmx \ + src/common/hierarchy.cmx src/common/entity.cmx src/lib/cps.cmx \ + src/basic_rg/brgSubstitution.cmx src/basic_rg/brgReduction.cmx \ + src/basic_rg/brgEnvironment.cmx src/basic_rg/brg.cmx \ + src/basic_rg/brgType.cmi src/basic_rg/brgUntrusted.cmi: src/common/status.cmx \ src/basic_rg/brgReduction.cmi src/basic_rg/brg.cmx src/basic_rg/brgUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ @@ -212,26 +216,28 @@ src/basic_ag/bagSubstitution.cmo: src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi src/basic_ag/bagSubstitution.cmx: src/lib/share.cmx src/basic_ag/bag.cmx \ src/basic_ag/bagSubstitution.cmi -src/basic_ag/bagReduction.cmi: src/basic_ag/bag.cmx -src/basic_ag/bagReduction.cmo: src/common/marks.cmi src/lib/log.cmi \ - src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ +src/basic_ag/bagReduction.cmi: src/common/status.cmx src/basic_ag/bag.cmx +src/basic_ag/bagReduction.cmo: src/common/status.cmx src/common/options.cmx \ + src/common/marks.cmi src/lib/log.cmi src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagSubstitution.cmi \ src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi -src/basic_ag/bagReduction.cmx: src/common/marks.cmx src/lib/log.cmx \ - src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ +src/basic_ag/bagReduction.cmx: src/common/status.cmx src/common/options.cmx \ + src/common/marks.cmx src/lib/log.cmx src/common/entity.cmx \ + src/lib/cps.cmx src/basic_ag/bagSubstitution.cmx \ src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \ src/basic_ag/bag.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagType.cmi: src/common/status.cmx src/basic_ag/bag.cmx src/basic_ag/bagType.cmo: src/common/status.cmx src/lib/share.cmx \ - src/lib/log.cmi src/common/hierarchy.cmi src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagReduction.cmi src/basic_ag/bagOutput.cmi \ - src/basic_ag/bagEnvironment.cmi src/basic_ag/bag.cmx \ - src/basic_ag/bagType.cmi + src/common/options.cmx src/lib/log.cmi src/common/hierarchy.cmi \ + src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagReduction.cmi \ + src/basic_ag/bagOutput.cmi src/basic_ag/bagEnvironment.cmi \ + src/basic_ag/bag.cmx src/basic_ag/bagType.cmi src/basic_ag/bagType.cmx: src/common/status.cmx src/lib/share.cmx \ - src/lib/log.cmx src/common/hierarchy.cmx src/common/entity.cmx \ - src/lib/cps.cmx src/basic_ag/bagReduction.cmx src/basic_ag/bagOutput.cmx \ - src/basic_ag/bagEnvironment.cmx src/basic_ag/bag.cmx \ - src/basic_ag/bagType.cmi + src/common/options.cmx src/lib/log.cmx src/common/hierarchy.cmx \ + src/common/entity.cmx src/lib/cps.cmx src/basic_ag/bagReduction.cmx \ + src/basic_ag/bagOutput.cmx src/basic_ag/bagEnvironment.cmx \ + src/basic_ag/bag.cmx src/basic_ag/bagType.cmi src/basic_ag/bagUntrusted.cmi: src/common/status.cmx src/basic_ag/bag.cmx src/basic_ag/bagUntrusted.cmo: src/lib/log.cmi src/common/entity.cmx \ src/basic_ag/bagType.cmi src/basic_ag/bagEnvironment.cmi \ diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 8a12c90a9..690c8c935 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -22,22 +22,22 @@ INPUTFAST = examples/grundlagen/grundlagen_1.aut test-si: $(MAIN).opt etc @echo " HELENA -p -o -c $(INPUT)" - $(H)./$(MAIN).opt -p -o -c -S 3 -O $(XMLDIR) $(O) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -T 2 -p -o -c -O $(XMLDIR) $(O) $(INPUT) > etc/log.txt test-si-fast: $(MAIN).opt etc @echo " HELENA -o -q $(INPUTFAST)" - $(H)./$(MAIN).opt -o -q -S 1 $(O) $(INPUTFAST) > etc/log.txt + $(H)./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) > etc/log.txt profile: $(MAIN).opt etc @echo " HELENA -o -q $(INPUTFAST) (30 TIMES)" $(H)rm etc/log.txt - $(H)for T in `seq 30`; do ./$(MAIN).opt -o -q -s 3 -S 1 $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)for T in `seq 30`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt xml-si: $(MAIN).opt etc @echo " HELENA -o -x -s 2 $(INPUT)" - $(H)./$(MAIN).opt -o -x -s 2 -S 1 -O $(XMLDIR) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -T 1 -o -x -s 2 -O $(XMLDIR) $(INPUT) > etc/log.txt xml-si-crg: $(MAIN).opt etc @echo " HELENA -o -x -s 1 $(INPUT)" - $(H)./$(MAIN).opt -o -x -s 1 -S 1 -O $(XMLDIR) $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -T 1 -o -x -s 1 -O $(XMLDIR) $(INPUT) > etc/log.txt diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll index c0bc55afd..67d8ccd55 100644 --- a/helm/software/helena/src/automath/autLexer.mll +++ b/helm/software/helena/src/automath/autLexer.mll @@ -13,8 +13,10 @@ module L = Log module G = Options module AP = AutParser + + let level = 0 - let out s = if !G.debug_lexer then L.warn s else () + let out s = if !G.debug_lexer then L.warn level s else () (* This turns an Automath identifier into an XML nmtoken *) let quote id = diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml index ddf2f30ed..41424b4db 100644 --- a/helm/software/helena/src/automath/autOutput.ml +++ b/helm/software/helena/src/automath/autOutput.ml @@ -29,6 +29,8 @@ type counters = { xnodes: int } +let level = 2 + let initial_counters = { sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0; sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0 @@ -70,31 +72,31 @@ let count_command f c = function let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in - L.warn (P.sprintf " Automath representation summary"); - L.warn (P.sprintf " Total book entities: %7u" entities); - L.warn (P.sprintf " Section entities: %7u" c.sections); - L.warn (P.sprintf " Context entities: %7u" c.contexts); - L.warn (P.sprintf " Block entities: %7u" c.blocks); - L.warn (P.sprintf " Declaration entities: %7u" c.decls); - L.warn (P.sprintf " Definition entities: %7u" c.defs); - L.warn (P.sprintf " Total Parameter items: %7u" c.pars); - L.warn (P.sprintf " Application items: %7u" c.pars); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.sorts); - L.warn (P.sprintf " Reference items: %7u" c.grefs); - L.warn (P.sprintf " Application items: %7u" c.appls); - L.warn (P.sprintf " Abstraction items: %7u" c.absts); - L.warn (P.sprintf " Global Int. Complexity: unknown"); - L.warn (P.sprintf " + Abbreviation nodes: %7u" c.xnodes); + L.warn level (P.sprintf "Automath representation summary"); + L.warn level (P.sprintf " Total book entities: %7u" entities); + L.warn level (P.sprintf " Section entities: %7u" c.sections); + L.warn level (P.sprintf " Context entities: %7u" c.contexts); + L.warn level (P.sprintf " Block entities: %7u" c.blocks); + L.warn level (P.sprintf " Declaration entities: %7u" c.decls); + L.warn level (P.sprintf " Definition entities: %7u" c.defs); + L.warn level (P.sprintf " Total Parameter items: %7u" c.pars); + L.warn level (P.sprintf " Application items: %7u" c.pars); + L.warn level (P.sprintf " Total term items: %7u" terms); + L.warn level (P.sprintf " Sort items: %7u" c.sorts); + L.warn level (P.sprintf " Reference items: %7u" c.grefs); + L.warn level (P.sprintf " Application items: %7u" c.appls); + L.warn level (P.sprintf " Abstraction items: %7u" c.absts); + L.warn level (P.sprintf " Global Int. Complexity: unknown"); + L.warn level (P.sprintf " + Abbreviation nodes: %7u" c.xnodes); f () let print_process_counters f c = let f iao iar iac iag = - 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); - L.warn (P.sprintf " Implicit after global: %7u" iag); + L.warn level (P.sprintf "Automath process summary"); + L.warn level (P.sprintf " Implicit after opening: %7u" iao); + L.warn level (P.sprintf " Implicit after reopening: %7u" iar); + L.warn level (P.sprintf " Implicit after closing: %7u" iac); + L.warn level (P.sprintf " Implicit after global: %7u" iag); f () in AA.get_counters f c diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml index feebca464..4d0a1c07b 100644 --- a/helm/software/helena/src/basic_ag/bagOutput.ml +++ b/helm/software/helena/src/basic_ag/bagOutput.ml @@ -10,7 +10,6 @@ V_______________________________________________________________ *) module P = Printf -module F = Format module U = NUri module L = Log module G = Options @@ -33,6 +32,8 @@ type counters = { tabbrs: int } +let level = 2 + let initial_counters = { eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 @@ -82,71 +83,71 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let locations = J.locations () in - L.warn (P.sprintf " Kernel representation summary (basic_ag)"); - L.warn (P.sprintf " Total entry items: %7u" items); - L.warn (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.tsorts); - L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn (P.sprintf " Application items: %7u" c.tappls); - L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn (P.sprintf " Total binder locations: %7u" locations); + L.warn level (P.sprintf "Kernel representation summary (basic_ag)"); + L.warn level (P.sprintf " Total entry items: %7u" items); + L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (P.sprintf " Total term items: %7u" terms); + L.warn level (P.sprintf " Sort items: %7u" c.tsorts); + L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (P.sprintf " Application items: %7u" c.tappls); + L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (P.sprintf " Total binder locations: %7u" locations); f () -let name err frm a = +let name err och a = let f n = function - | true -> F.fprintf frm "%s" n - | false -> F.fprintf frm "-%s" n + | true -> P.fprintf och "%s" n + | false -> P.fprintf och "-%s" n in E.name err f a -let res a l frm = - let err () = F.fprintf frm "@[#%u@]" l in - if !G.indexes then err () else name err frm a +let res a l och = + let err () = P.fprintf och "#%u" l in + if !G.indexes then err () else name err och a -let rec pp_term c frm = function +let rec pp_term c och = function | Z.Sort h -> - let err () = F.fprintf frm "@[*%u@]" h in - let f s = F.fprintf frm "@[%s@]" s in + let err () = P.fprintf och "*%u" h in + let f s = P.fprintf och "%s" s in H.string_of_sort err f h | Z.LRef i -> - let err () = F.fprintf frm "@[#%u@]" i in - let f a _ = name err frm a in + let err () = P.fprintf och "#%u" i in + let f a _ = name err och a in if !G.indexes then err () else Z.get err f c i - | Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) + | Z.GRef s -> P.fprintf och "$%s" (U.string_of_uri s) | Z.Cast (u, t) -> - F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t + P.fprintf och "{%a}.%a" (pp_term c) u (pp_term c) t | Z.Appl (v, t) -> - F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t + P.fprintf och "(%a).%a" (pp_term c) v (pp_term c) t | Z.Bind (a, l, Z.Abst w, t) -> let f cc = - F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t + P.fprintf och "[%t:%a].%a" (res a l) (pp_term c) w (pp_term cc) t in Z.push "output abst" f c a l (Z.Abst w) | Z.Bind (a, l, Z.Abbr v, t) -> let f cc = - F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t + P.fprintf och "[%t=%a].%a" (res a l) (pp_term c) v (pp_term cc) t in Z.push "output abbr" f c a l (Z.Abbr v) | Z.Bind (a, l, Z.Void, t) -> - let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in + let f cc = P.fprintf och "[%t].%a" (res a l) (pp_term cc) t in Z.push "output void" f c a l Z.Void -let pp_lenv frm c = - let pp_entry frm = function +let pp_lenv och c = + let pp_entry och = function | a, l, Z.Abst w -> - F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w + P.fprintf och "%t : %a\n" (res a l) (pp_term c) w | a, l, Z.Abbr v -> - F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v + P.fprintf och "%t = %a\n" (res a l) (pp_term c) v | a, l, Z.Void -> - F.fprintf frm "@,%t" (res a l) + P.fprintf och "%t\n" (res a l) in - let iter map frm l = List.iter (map frm) l in - let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in + let iter map och l = List.iter (map och) l in + let f es = P.fprintf och "%a" (iter pp_entry) (List.rev es) in Z.contents f c let specs = { diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index d22d2c730..c7d89bc84 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -13,7 +13,9 @@ module U = NUri module C = Cps module L = Log module E = Entity +module G = Options module J = Marks +module S = Status module Z = Bag module ZO = BagOutput module ZE = BagEnvironment @@ -37,14 +39,14 @@ type ho_whd_result = (* Internal functions *******************************************************) +let level = 4 + let term_of_whdr = function | Sort_ h -> Z.Sort h | LRef_ (i, _) -> Z.LRef i | GRef_ (_, uri, _) -> Z.GRef uri | Bind_ (a, l, w, t) -> Z.bind_abst a l w t -let level = 5 - let log1 s c t = let sc, st = s ^ " in the environment", "the term" in L.log ZO.specs level (L.et_items1 sc c st t) @@ -122,32 +124,31 @@ let rec ho_whd f c m x = in whd aux c m x -let ho_whd f c t = - let f r = L.unbox level; f r in - L.box level; log1 "Now scanning" c t; +let ho_whd f st c t = + if !G.trace >= level then log1 "Now scanning" c t; ho_whd f c empty_machine t -let rec are_convertible f ~si a c m1 t1 m2 t2 = +let rec are_convertible f st a c m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) let rec aux m1 r1 m2 r2 = (* L.warn "entering R.are_convertible_aux"; *) let u, t = term_of_whdr r1, term_of_whdr r2 in - log2 "Now really converting" c u c t; + if !G.trace >= level then log2 "Now really converting" c u c t; match r1, r2 with | Sort_ h1, Sort_ h2 -> if h1 = h2 then f a else f false | LRef_ (i1, _), LRef_ (i2, _) -> - if i1 = i2 then are_convertible_stacks f ~si a c m1 m2 else f false + if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false | GRef_ ((E.Apix a1 :: _), _, E.Abst _), GRef_ ((E.Apix a2 :: _), _, E.Abst _) -> - if a1 = a2 then are_convertible_stacks f ~si a c m1 m2 else f false + if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false | GRef_ ((E.Apix a1 :: _), _, E.Abbr v1), GRef_ ((E.Apix a2 :: _), _, E.Abbr v2) -> if a1 = a2 then let f a = - if a then f a else are_convertible f ~si true c m1 v1 m2 v2 + if a then f a else are_convertible f st true c m1 v1 m2 v2 in - are_convertible_stacks f ~si a c m1 m2 + are_convertible_stacks f st a c m1 m2 else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 @@ -159,25 +160,25 @@ let rec are_convertible f ~si a c m1 t1 m2 t2 = let l = J.new_location () in let h c = let m1, m2 = inc m1, inc m2 in - let f t1 = ZS.subst (are_convertible f ~si a c m1 t1 m2) l l2 t2 in + let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in ZS.subst f l l1 t1 in let f r = if r then push "!" h c m1 a1 l w1 else f false in - are_convertible f ~si a c m1 w1 m2 w2 + are_convertible f st a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (a2, l2, w2, t2) when si -> + | Sort_ _, Bind_ (a2, l2, w2, t2) when st.S.si -> let m1, m2 = inc m1, inc m2 in - let f c = are_convertible f ~si a c m1 (term_of_whdr r1) m2 t2 in + let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in push "nsi" f c m2 a2 l2 w2 | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in let g m1 r1 = whd (aux m1 r1) c m2 t2 in if a = false then f false else whd g c m1 t1 -and are_convertible_stacks f ~si a c m1 m2 = +and are_convertible_stacks f st a c m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in - let map f a v1 v2 = are_convertible f ~si a c mm1 v1 mm2 v2 in + let map f a v1 v2 = are_convertible f st a c mm1 v1 mm2 v2 in if List.length m1.s <> List.length m2.s then begin (* L.warn (Printf.sprintf "Different lengths: %u %u" @@ -188,7 +189,6 @@ and are_convertible_stacks f ~si a c m1 m2 = else C.list_fold_left2 f map a m1.s m2.s -let are_convertible f ?(si=false) c u t = - let f b = L.unbox level; f b in - L.box level; log2 "Now converting" c u c t; - are_convertible f ~si true c empty_machine u empty_machine t +let are_convertible f st c u t = + if !G.trace >= level then log2 "Now converting" c u c t; + are_convertible f st true c empty_machine u empty_machine t diff --git a/helm/software/helena/src/basic_ag/bagReduction.mli b/helm/software/helena/src/basic_ag/bagReduction.mli index 8f32faa0e..9a3c849fb 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.mli +++ b/helm/software/helena/src/basic_ag/bagReduction.mli @@ -14,7 +14,7 @@ type ho_whd_result = | Abst of Bag.term val ho_whd: - (ho_whd_result -> 'a) -> Bag.lenv -> Bag.term -> 'a + (ho_whd_result -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> 'a val are_convertible: - (bool -> 'a) -> ?si:bool -> Bag.lenv -> Bag.term -> Bag.term -> 'a + (bool -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index 4f447276b..aa4b821a8 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -13,55 +13,52 @@ module U = NUri module C = Cps module W = Share module L = Log -module E = Entity module H = Hierarchy +module E = Entity +module G = Options module S = Status module Z = Bag module ZO = BagOutput module ZE = BagEnvironment module ZR = BagReduction -exception TypeError of Z.message - (* Internal functions *******************************************************) -let level = 4 +let level = 3 let log1 s c t = let sc, st = s ^ " in the envireonment", "the term" in L.log ZO.specs level (L.et_items1 sc c st t) -let error1 st c t = +let error1 err st c t = let sc = "In the envireonment" in - raise (TypeError (L.et_items1 sc c st t)) + err (L.et_items1 sc c st t) -let error3 c t1 t2 t3 = +let error3 err c t1 t2 t3 = let sc, st1, st2, st3 = "In the envireonment", "the term", "is of type", "but must be of type" in - raise (TypeError (L.et_items3 sc c st1 t1 st2 t2 st3 t3)) + err (L.et_items3 sc c st1 t1 st2 t2 st3 t3) let mk_gref u l = let map t v = Z.Appl (v, t) in List.fold_left map (Z.GRef u) l -(* Interface functions ******************************************************) - -let rec b_type_of f st c x = +let rec b_type_of err f st c x = (* L.warn "Entering T.b_type_of"; *) - log1 "Now checking" c x; + if !G.trace >= level then log1 "Now checking" c x; match x with | Z.Sort h -> let h = H.apply h in f x (Z.Sort h) | Z.LRef i -> - let err () = error1 "variable not found" c x in + let err0 () = error1 err "variable not found" c x in let f _ = function | Z.Abst w -> f x w | Z.Abbr (Z.Cast (w, v)) -> f x w | Z.Abbr _ -> assert false - | Z.Void -> error1 "reference to excluded variable" c x + | Z.Void -> error1 err "reference to excluded variable" c x in - Z.get err f c i + Z.get err0 f c i | Z.GRef uri -> let f = function | _, _, E.Abst (_, w) -> f x w @@ -74,53 +71,51 @@ let rec b_type_of f st c x = let f xv xt tt = f (W.sh2 v xv t xt x (Z.bind_abbr a l)) (Z.bind_abbr a l xv tt) in - let f xv cc = b_type_of (f xv) st cc t in + let f xv cc = b_type_of err (f xv) st cc t in let f xv = Z.push "type abbr" (f xv) c a l (Z.Abbr xv) in let f xv vv = match xv with | Z.Cast _ -> f xv | _ -> f (Z.Cast (vv, xv)) in - type_of f st c v + type_of err f st c v | Z.Bind (a, l, Z.Abst u, t) -> let f xu xt tt = f (W.sh2 u xu t xt x (Z.bind_abst a l)) (Z.bind_abst a l xu tt) in - let f xu cc = b_type_of (f xu) st cc t in + let f xu cc = b_type_of err (f xu) st cc t in let f xu _ = Z.push "type abst" (f xu) c a l (Z.Abst xu) in - type_of f st c u + type_of err f st c u | Z.Bind (a, l, Z.Void, t) -> let f xt tt = f (W.sh1 t xt x (Z.bind a l Z.Void)) (Z.bind a l Z.Void tt) in - let f cc = b_type_of f st cc t in + let f cc = b_type_of err f st cc t in Z.push "type void" f c a l Z.Void | Z.Appl (v, t) -> let f xv vv xt tt = function | ZR.Abst w -> - L.box (succ level); - L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w); - L.unbox (succ level); + if !G.trace > level then L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w); let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt) - else error3 c xv vv w + else error3 err c xv vv w in - ZR.are_convertible f ~si:st.S.si c w vv + ZR.are_convertible f st c w vv | _ -> - error1 "not a function" c xt + error1 err "not a function" c xt in - let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) c tt in - let f xv vv = b_type_of (f xv vv) st c t in - type_of f st c v + let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in + let f xv vv = b_type_of err (f xv vv) st c t in + type_of err f st c v | Z.Cast (u, t) -> let f xu xt tt a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) - if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 c xt tt xu + if a then f (W.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu in - let f xu xt tt = ZR.are_convertible (f xu xt tt) ~si:st.S.si c xu tt in - let f xu _ = b_type_of (f xu) st c t in - type_of f st c u + let f xu xt tt = ZR.are_convertible (f xu xt tt) st c xu tt in + let f xu _ = b_type_of err (f xu) st c t in + type_of err f st c u + +(* Interface functions ******************************************************) -and type_of f st c x = - let f t u = L.unbox level; f t u in - L.box level; b_type_of f st c x +and type_of err f st c x = b_type_of err f st c x diff --git a/helm/software/helena/src/basic_ag/bagType.mli b/helm/software/helena/src/basic_ag/bagType.mli index ba0268e9c..8f343a624 100644 --- a/helm/software/helena/src/basic_ag/bagType.mli +++ b/helm/software/helena/src/basic_ag/bagType.mli @@ -9,8 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of Bag.message - val type_of: + (Bag.message -> 'a) -> (Bag.term -> Bag.term -> 'a) -> Status.status -> Bag.lenv -> Bag.term -> 'a diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.ml b/helm/software/helena/src/basic_ag/bagUntrusted.ml index 5d04a3bf4..c27ec5ed1 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.ml +++ b/helm/software/helena/src/basic_ag/bagUntrusted.ml @@ -19,11 +19,13 @@ module ZT = BagType (* Interface functions ******************************************************) (* to share *) -let type_check f st = function +let type_check err f st = function | a, uri, E.Abst (n, t) -> + let err msg = err (L.Uri uri :: msg) in let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abst (n, xt)) in - L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t + ZT.type_of err f st Z.empty_lenv t | a, uri, E.Abbr t -> + let err msg = err (L.Uri uri :: msg) in let f xt tt = ZE.set_entity (f tt) (a, uri, E.Abbr xt) in - L.loc := U.string_of_uri uri; ZT.type_of f st Z.empty_lenv t + ZT.type_of err f st Z.empty_lenv t | _, _, E.Void -> assert false diff --git a/helm/software/helena/src/basic_ag/bagUntrusted.mli b/helm/software/helena/src/basic_ag/bagUntrusted.mli index 5c609e804..d9ea41897 100644 --- a/helm/software/helena/src/basic_ag/bagUntrusted.mli +++ b/helm/software/helena/src/basic_ag/bagUntrusted.mli @@ -10,4 +10,5 @@ V_______________________________________________________________ *) val type_check: - (Bag.term -> Bag.entity -> 'a) -> Status.status -> Bag.entity -> 'a + (Bag.message -> 'a) -> (Bag.term -> Bag.entity -> 'a) -> + Status.status -> Bag.entity -> 'a diff --git a/helm/software/helena/src/basic_rg/brgOutput.ml b/helm/software/helena/src/basic_rg/brgOutput.ml index ed024a68e..978658caa 100644 --- a/helm/software/helena/src/basic_rg/brgOutput.ml +++ b/helm/software/helena/src/basic_rg/brgOutput.ml @@ -10,7 +10,6 @@ V_______________________________________________________________ *) module P = Printf -module F = Format module C = Cps module U = NUri module L = Log @@ -41,6 +40,8 @@ type counters = { xnodes: int } +let level = 2 + let initial_counters = { eabsts = 0; eabbrs = 0; evoids = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0; @@ -107,20 +108,20 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in - L.warn (P.sprintf " Kernel representation summary (basic_rg)"); - L.warn (P.sprintf " Total entry items: %7u" items); - L.warn (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.tsorts); - L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn (P.sprintf " Application items: %7u" c.tappls); - L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes); - L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes); + L.warn level (P.sprintf "Kernel representation summary (basic_rg)"); + L.warn level (P.sprintf " Total entry items: %7u" items); + L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (P.sprintf " Total term items: %7u" terms); + L.warn level (P.sprintf " Sort items: %7u" c.tsorts); + L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (P.sprintf " Application items: %7u" c.tappls); + L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes); + L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes); f () (* supplementary annotation *************************************************) @@ -149,63 +150,65 @@ let rename f e a = (* lenv/term pretty printing ************************************************) -let name err frm a = +let name err och a = let f n = function - | true -> F.fprintf frm "%s" n - | false -> F.fprintf frm "-%s" n + | true -> P.fprintf och "%s" n + | false -> P.fprintf och "-%s" n in E.name err f a -let pp_level frm n = - if N.is_infinite n then () else F.fprintf frm "^%s" (N.to_string n) +let pp_level och n = + if N.is_infinite n then () else P.fprintf och "^%s" (N.to_string n) -let rec pp_term e frm = function +let rec pp_term e och = function | B.Sort (_, h) -> - let err _ = F.fprintf frm "@[*%u@]" h in - let f s = F.fprintf frm "@[%s@]" s in + let err _ = P.fprintf och "*%u" h in + let f s = P.fprintf och "%s" s in H.string_of_sort err f h | B.LRef (_, i) -> - let err _ = F.fprintf frm "@[#%u@]" i in + let err _ = P.fprintf och "#%u" i in if !G.indexes then err () else let _, _, a, b = B.get e i in - F.fprintf frm "@[%a@]" (name err) a + P.fprintf och "%a" (name err) a | B.GRef (_, s) -> - F.fprintf frm "@[$%s@]" (U.string_of_uri s) + P.fprintf och "$%s" (U.string_of_uri s) | B.Cast (_, u, t) -> - F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t + P.fprintf och "{%a}.%a" (pp_term e) u (pp_term e) t | B.Appl (_, v, t) -> - F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t + P.fprintf och "(%a).%a" (pp_term e) v (pp_term e) t | B.Bind (a, B.Abst (n, w), t) -> let f a = let ee = B.push e B.empty a (B.abst n w) in - F.fprintf frm "@[[%a:%a]%a.%a@]" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t + P.fprintf och "[%a:%a]%a.%a" (name C.err) a (pp_term e) w pp_level n (pp_term ee) t in rename f e a | B.Bind (a, B.Abbr v, t) -> let f a = let ee = B.push e B.empty a (B.abbr v) in - F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t + P.fprintf och "[%a=%a].%a" (name C.err) a (pp_term e) v (pp_term ee) t in rename f e a | B.Bind (a, B.Void, t) -> let f a = let ee = B.push e B.empty a B.Void in - F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t + P.fprintf och "[%a].%a" (name C.err) a (pp_term ee) t in rename f e a -let pp_lenv frm e = - let pp_entry f e c a b x = f x (*match b with +let pp_lenv och e = + let pp_entry f e c a b x = f x (* match b with | B.Abst (a, w) -> - let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in + let f a = P.fprintf och "%a : %a\n" (name C.err) a (pp_term e) w; f a in rename f x a | B.Abbr (a, v) -> - let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in + let f a = P.fprintf och "%a = %a\n" (name C.err) a (pp_term e) v; f a in rename f c a | B.Void a -> - let f a = F.fprintf frm "@,%a" (name C.err) a; f a in + let f a = P.fprintf och "%a\n" (name C.err) a; f a in rename f c a *) in + let e = B.empty in + if e = B.empty then P.fprintf och "%s\n" "not shown" else B.fold_right ignore pp_entry e B.empty let specs = { diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index 2aba23fe3..c3ef9795b 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -14,8 +14,9 @@ module C = Cps module W = Share module L = Log module H = Hierarchy -module E = Entity module N = Level +module E = Entity +module G = Options module O = Output module Q = Ccs module S = Status @@ -35,7 +36,7 @@ type message = (kam, B.term) L.message (* Internal functions *******************************************************) -let level = 5 +let level = 4 let log1 s c t = let sc, st = s ^ " in the environment", "the term" in @@ -99,13 +100,13 @@ let rec step st m x = begin match BE.get_entity uri with | _, _, E.Abbr v -> if st.S.delta then begin - if st.S.tc then O.add ~gdelta:1 (); + if !G.summary then O.add ~gdelta:1 (); step st m v end else m, x, Some v | _, _, E.Abst (_, w) -> if assert_tstep m true then begin - if st.S.tc then O.add ~grt:1 (); + if !G.summary then O.add ~grt:1 (); step st (tstep m) w end else m, x, None @@ -115,11 +116,11 @@ let rec step st m x = | B.LRef (_, i) -> begin match get m i with | c, _, B.Abbr v -> - if st.S.tc then O.add ~ldelta:1 (); + if !G.summary then O.add ~ldelta:1 (); step st {m with e = c} v | c, a, B.Abst (_, w) -> if assert_tstep m true then begin - if st.S.tc then O.add ~lrt:1 (); + if !G.summary then O.add ~lrt:1 (); step st {(tstep m) with e = c} w end else m, B.LRef (a, i), None @@ -128,10 +129,10 @@ let rec step st m x = end | B.Cast (_, u, t) -> if assert_tstep m false then begin - if st.S.tc then O.add ~e:1 (); + if !G.summary then O.add ~e:1 (); step st (tstep m) u end else begin - if st.S.tc then O.add ~epsilon:1 (); + if !G.summary then O.add ~epsilon:1 (); step st m t end | B.Appl (_, v, t) -> @@ -144,13 +145,13 @@ let rec step st m x = m, B.Bind (a, B.Abst (n, w), t), None | (c, v) :: s -> if N.is_zero n then Q.add_nonzero st.S.cc a; - if st.S.tc then O.add ~beta:1 ~theta:(List.length s) (); + if !G.summary then O.add ~beta:1 ~theta:(List.length s) (); let v = if assert_tstep m false then B.Cast ([], w, v) else v in let e = B.push m.e c a (B.abbr v) in step st {m with e = e; s = s} t end | B.Bind (a, b, t) -> - if st.S.tc then O.add ~theta:(List.length m.s) (); + if !G.summary then O.add ~theta:(List.length m.s) (); let e = B.push m.e m.e a b in step st {m with e = e} t @@ -171,7 +172,7 @@ let push m a b = {m with e = e; l = l} let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = - log2 "Now converting nfs" m1.e t1 m2.e t2; + if !G.trace >= level then log2 "Now converting nfs" m1.e t1 m2.e t2; match t1, r1, t2, r2 with | B.Sort (_, h1), _, B.Sort (_, h2), _ -> h1 = h2 @@ -185,21 +186,21 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = let e1 = E.apix C.err C.start a1 in let e2 = E.apix C.err C.start a2 in if e1 < e2 then begin - if st.S.tc then O.add ~gdelta:1 (); + if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) end else if e2 < e1 then begin - if st.S.tc then O.add ~gdelta:1 (); + if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) end else if U.eq u1 u2 & assert_iterations m1 m2 && ac_stacks st m1 m2 then true else begin - if st.S.tc then O.add ~gdelta:2 (); + if !G.summary then O.add ~gdelta:2 (); ac st m1 v1 m2 v2 end | _, _, B.GRef _, Some v2 -> - if st.S.tc then O.add ~gdelta:1 (); + if !G.summary then O.add ~gdelta:1 (); ac_nfs st (m1, t1, r1) (step st m2 v2) | B.GRef _, Some v1, _, _ -> - if st.S.tc then O.add ~gdelta:1 (); + if !G.summary then O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, t2, r2) | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ -> @@ -209,7 +210,7 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) = else false | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ -> if N.is_zero n then () else Q.add_zero st.S.cc a; - if st.S.tc then O.add ~si:1 (); + if !G.summary then O.add ~si:1 (); ac st (push m1 a b) t1 (push m2 a b) t | _ -> false @@ -237,14 +238,14 @@ let get m i = let _, _, _, b = B.get m.e i in b let xwhd st m n t = - L.box level; log1 "Now scanning" m.e t; + if !G.trace >= level then log1 "Now scanning" m.e t; let m, t, _ = step {st with S.delta = true} (reset m n) t in - L.unbox level; m, t + m, t let are_convertible st m1 n1 t1 m2 n2 t2 = - L.box level; log2 "Now converting" m1.e t1 m2.e t2; - let r = ac {st with S.delta = st.S.expand} (reset m1 n1) t1 (reset m2 n2) t2 in - L.unbox level; r + if !G.trace >= level then log2 "Now converting" m1.e t1 m2.e t2; + let r = ac {st with S.delta = !G.expand} (reset m1 n1) t1 (reset m2 n2) t2 in + r (* let err _ = in if W.eq mu mw then are_alpha_convertible err f u w else err () *) diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml index 7c47ff12c..29b73beeb 100644 --- a/helm/software/helena/src/basic_rg/brgType.ml +++ b/helm/software/helena/src/basic_rg/brgType.ml @@ -14,8 +14,10 @@ module C = Cps module W = Share module L = Log module H = Hierarchy -module E = Entity module N = Level +module E = Entity +module G = Options +module S = Status module B = Brg module BE = BrgEnvironment module BS = BrgSubstitution @@ -23,7 +25,7 @@ module BR = BrgReduction (* Internal functions *******************************************************) -let level = 4 +let level = 3 let message1 st1 m t1 = L.et_items1 "In the environment" m st1 t1 @@ -64,7 +66,7 @@ let assert_applicability err f st m u w v = | _ -> assert false (**) let rec b_type_of err f st m x = - log1 "Now checking" m x; + if !G.trace >= level then log1 "Now checking" m x; match x with | B.Sort (a, h) -> let h = H.apply h in f x (B.Sort (a, h)) @@ -127,6 +129,4 @@ let rec b_type_of err f st m x = (* Interface functions ******************************************************) -and type_of err f st m x = - let f t u = L.unbox level; f t u in - L.box level; b_type_of err f st m x +and type_of err f st m x = b_type_of err f st m x diff --git a/helm/software/helena/src/basic_rg/brgUntrusted.ml b/helm/software/helena/src/basic_rg/brgUntrusted.ml index 373f94973..88edd46d8 100644 --- a/helm/software/helena/src/basic_rg/brgUntrusted.ml +++ b/helm/software/helena/src/basic_rg/brgUntrusted.ml @@ -23,11 +23,13 @@ module BV = BrgValidity (* to share *) let type_check err f st = function | a, uri, E.Abst (n, t) -> + let err msg = err (L.Uri uri :: msg) in let f xt tt = let e = BE.set_entity (a, uri, E.Abst (n, xt)) in f tt e in - L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t + BT.type_of err f st BR.empty_kam t | a, uri, E.Abbr t -> + let err msg = err (L.Uri uri :: msg) in let f xt tt = let xt = match xt with | B.Cast _ -> xt @@ -35,7 +37,7 @@ let type_check err f st = function in let e = BE.set_entity (a, uri, E.Abbr xt) in f tt e in - L.loc := U.string_of_uri uri; BT.type_of err f st BR.empty_kam t + BT.type_of err f st BR.empty_kam t | _, _, E.Void -> assert false let validate err f st e = @@ -44,5 +46,6 @@ let validate err f st e = | _, uri, E.Abbr t -> uri, t | _, _, E.Void -> assert false in + let err msg = err (L.Uri uri :: msg) in let f () = let _ = BE.set_entity e in f () in - L.loc := U.string_of_uri uri; BV.validate err f st BR.empty_kam t + BV.validate err f st BR.empty_kam t diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml index 18ec015df..e358d5a19 100644 --- a/helm/software/helena/src/basic_rg/brgValidity.ml +++ b/helm/software/helena/src/basic_rg/brgValidity.ml @@ -11,13 +11,15 @@ module L = Log module E = Entity +module G = Options +module S = Status module B = Brg module BE = BrgEnvironment module BR = BrgReduction (* Internal functions *******************************************************) -let level = 4 +let level = 3 let message1 st1 m t1 = L.et_items1 "In the environment" m st1 t1 @@ -55,7 +57,7 @@ let assert_applicability err f st m v t = | _ -> assert false (**) let rec b_validate err f st m x = - log1 "Now checking" m x; + if !G.trace >= level then log1 "Now checking" m x; match x with | B.Sort _ -> f () | B.LRef (_, i) -> @@ -90,6 +92,4 @@ let rec b_validate err f st m x = (* Interface functions ******************************************************) -and validate err f st m x = - let f () = L.unbox level; f () in - L.box level; b_validate err f st m x +and validate err f st m x = b_validate err f st m x diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index a2c749872..b77757ddb 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -18,9 +18,15 @@ type kernel = Crg | Brg | Bag (* interface functions ******************************************************) -let xdir = ref "" +let stage = ref 3 (* stage *) -let kernel = ref Brg +let trace = ref 0 (* trace level *) + +let summary = ref false (* log summary information *) + +let xdir = ref "" (* directory for XML output *) + +let kernel = ref Brg (* kernel type *) let si = ref false (* use sort inclusion *) @@ -57,6 +63,7 @@ let get_mk_uri () = fun s -> F.concat bu (s ^ ".ld") let clear () = + stage := 3; trace := 0; summary := false; xdir := ""; kernel := Brg; si := false; cover := ""; expand := false; indexes := false; icm := 0; unquote := false; debug_parser := false; debug_lexer := false diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml index 2af0b535b..7b9bd109b 100644 --- a/helm/software/helena/src/common/output.ml +++ b/helm/software/helena/src/common/output.ml @@ -26,6 +26,8 @@ type reductions = { e : int; } +let level = 2 + let initial_reductions = { beta = 0; theta = 0; epsilon = 0; zeta = 0; ldelta = 0; gdelta = 0; si = 0; lrt = 0; grt = 0; e = 0; @@ -56,20 +58,20 @@ let print_reductions () = let rs = r.beta + r.ldelta + r.zeta + r.theta + r.epsilon + r.gdelta in let prs = r.si + r.lrt + r.grt + r.e in let delta = r.ldelta + r.gdelta in - let rt = r.lrt + r.grt in - L.warn (P.sprintf " Reductions summary"); - L.warn (P.sprintf " Proper reductions: %7u" rs); - L.warn (P.sprintf " Beta: %7u" r.beta); - L.warn (P.sprintf " Delta: %7u" delta); - L.warn (P.sprintf " Local: %7u" r.ldelta); - L.warn (P.sprintf " Global: %7u" r.gdelta); - L.warn (P.sprintf " Theta: %7u" r.theta); - L.warn (P.sprintf " Zeta for abbreviation: %7u" r.zeta); - L.warn (P.sprintf " Zeta for cast: %7u" r.epsilon); - L.warn (P.sprintf " Pseudo reductions: %7u" prs); - L.warn (P.sprintf " Reference typing: %7u" rt); - L.warn (P.sprintf " Local: %7u" r.lrt); - L.warn (P.sprintf " Global: %7u" r.grt); - L.warn (P.sprintf " Cast typing: %7u" r.e); - L.warn (P.sprintf " Sort inclusion: %7u" r.si); - L.warn (P.sprintf " Relocated nodes (icm): %7u" !G.icm) + let rt = r.lrt + r.grt in + L.warn level (P.sprintf "Reductions summary"); + L.warn level (P.sprintf " Proper reductions: %7u" rs); + L.warn level (P.sprintf " Beta: %7u" r.beta); + L.warn level (P.sprintf " Delta: %7u" delta); + L.warn level (P.sprintf " Local: %7u" r.ldelta); + L.warn level (P.sprintf " Global: %7u" r.gdelta); + L.warn level (P.sprintf " Theta: %7u" r.theta); + L.warn level (P.sprintf " Zeta for abbreviation: %7u" r.zeta); + L.warn level (P.sprintf " Zeta for cast: %7u" r.epsilon); + L.warn level (P.sprintf " Pseudo reductions: %7u" prs); + L.warn level (P.sprintf " Reference typing: %7u" rt); + L.warn level (P.sprintf " Local: %7u" r.lrt); + L.warn level (P.sprintf " Global: %7u" r.grt); + L.warn level (P.sprintf " Cast typing: %7u" r.e); + L.warn level (P.sprintf " Sort inclusion: %7u" r.si); + L.warn level (P.sprintf "Relocated nodes (icm): %7u" !G.icm) diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml index e9c6e5620..3ae313608 100644 --- a/helm/software/helena/src/common/status.ml +++ b/helm/software/helena/src/common/status.ml @@ -13,22 +13,18 @@ module G = Options module Q = Ccs type status = { - ll: int; (* log level *) delta: bool; (* global delta-expansion *) - rt: bool; (* reference typing *) si: bool; (* sort inclusion *) - expand: bool; (* always expand global definitions *) cc: Q.csys; (* conversion constraints *) - tc: bool; (* trace constraints *) } (* helpers ******************************************************************) let initial_status () = { - ll = 0; delta = false; rt = false; tc = false; - si = !G.si; expand = !G.expand; cc = Q.init () + delta = false; + si = !G.si; cc = Q.init () } let refresh_status st = {st with - si = !G.si; expand = !G.expand; cc = Q.init () + si = !G.si; cc = Q.init () } diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml index 072073c18..49acbb49b 100644 --- a/helm/software/helena/src/complete_rg/crgOutput.ml +++ b/helm/software/helena/src/complete_rg/crgOutput.ml @@ -20,6 +20,8 @@ module D = Crg (* nodes count **************************************************************) +let level = 2 + type counters = { eabsts: int; eabbrs: int; @@ -118,20 +120,20 @@ let print_counters f c = in let items = c.eabsts + c.eabbrs in let nodes = c.nodes + c.xnodes in - L.warn (P.sprintf " Intermediate representation summary (crg)"); - L.warn (P.sprintf " Total entry items: %7u" items); - L.warn (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.tsorts); - L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn (P.sprintf " Application items: %7u" c.tappls); - L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes); - L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes); + L.warn level (P.sprintf "Intermediate representation summary (complete_rg)"); + L.warn level (P.sprintf " Total entry items: %7u" items); + L.warn level (P.sprintf " Declaration items: %7u" c.eabsts); + L.warn level (P.sprintf " Definition items: %7u" c.eabbrs); + L.warn level (P.sprintf " Total term items: %7u" terms); + L.warn level (P.sprintf " Sort items: %7u" c.tsorts); + L.warn level (P.sprintf " Local reference items: %7u" c.tlrefs); + L.warn level (P.sprintf " Global reference items: %7u" c.tgrefs); + L.warn level (P.sprintf " Explicit Cast items: %7u" c.tcasts); + L.warn level (P.sprintf " Application items: %7u" c.tappls); + L.warn level (P.sprintf " Abstraction items: %7u" c.tabsts); + L.warn level (P.sprintf " Abbreviation items: %7u" c.tabbrs); + L.warn level (P.sprintf " Global Int. Complexity: %7u" c.nodes); + L.warn level (P.sprintf " + Abbreviation nodes: %7u" nodes); f () (* term/environment pretty printer ******************************************) diff --git a/helm/software/helena/src/lib/log.ml b/helm/software/helena/src/lib/log.ml index 480e3c139..aeef7f9ee 100644 --- a/helm/software/helena/src/lib/log.ml +++ b/helm/software/helena/src/lib/log.ml @@ -9,61 +9,44 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module S = String module P = Printf -module F = Format -module C = Cps + +module U = NUri type ('a, 'b) item = Term of 'a * 'b | LEnv of 'a | Warn of string - | String of string - | Loc + | Uri of U.uri + | Flush type ('a, 'b) message = ('a, 'b) item list type ('a, 'b) specs = { - pp_term: 'a -> F.formatter -> 'b -> unit; - pp_lenv: F.formatter -> 'a -> unit + pp_term: 'a -> out_channel -> 'b -> unit; + pp_lenv: out_channel -> 'a -> unit } -let level = ref 0 - -let loc = ref "unknown location" - (* Internal functions *******************************************************) -let clear () = - level := 0; loc := "unknown location" +let std = stdout -let std = F.std_formatter +let err = stderr -let err = F.err_formatter - -let pp_items frm st l items = - let pp_item frm = function - | Term (c, t) -> F.fprintf frm "@ %a%!" (st.pp_term c) t - | LEnv c -> F.fprintf frm "%a%!" st.pp_lenv c - | Warn s -> F.fprintf frm "@ %s%!" s - | String s -> F.fprintf frm "%s " s - | Loc -> F.fprintf frm " <%s>" !loc +let pp_items och st l items = + let indent = S.make (l+l) ' ' in + let pp_item och = function + | Term (c, t) -> P.fprintf och "%s%a\n" indent (st.pp_term c) t + | LEnv c -> P.fprintf och "%s%a" indent st.pp_lenv c + | Warn s -> P.fprintf och "%s%s\n" indent s + | Uri u -> P.fprintf och "%s<%s>\n" indent (U.string_of_uri u) + | Flush -> P.fprintf och "%!" in - let iter map frm l = List.iter (map frm) l in - if !level >= l then F.fprintf frm "%a" (iter pp_item) items + let iter map och l = List.iter (map och) l in + P.fprintf och "%a" (iter pp_item) items (* Interface functions ******************************************************) -let box l = - if !level >= l then - begin F.fprintf std "@,@[%s" " "; F.pp_print_if_newline std () end - -let unbox l = if !level >= l then F.fprintf std "@]" - -let flush l = if !level >= l then F.fprintf std "@]@." - -let box_err () = F.fprintf err "@[" - -let flush_err () = F.fprintf err "@]@." - let log st l items = pp_items std st l items let error st items = pp_items err st 0 items @@ -92,4 +75,9 @@ let et_items3 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 ?sc3 ?c3 st3 t3 = in et_items2 sc1 c1 st1 t1 ?sc2 ?c2 st2 t2 @ tl -let warn msg = F.fprintf std "@,%s" msg +let specs = { + pp_term = (fun _ _ _ -> ()); + pp_lenv = (fun _ _ -> ()); +} + +let warn level str = log specs level (items1 str) diff --git a/helm/software/helena/src/lib/log.mli b/helm/software/helena/src/lib/log.mli index 9e0f054e1..df867a166 100644 --- a/helm/software/helena/src/lib/log.mli +++ b/helm/software/helena/src/lib/log.mli @@ -12,33 +12,17 @@ type ('a, 'b) item = Term of 'a * 'b | LEnv of 'a | Warn of string - | String of string - | Loc + | Uri of NUri.uri + | Flush type ('a, 'b) message = ('a, 'b) item list type ('a, 'b) specs = { - pp_term: 'a -> Format.formatter -> 'b -> unit; - pp_lenv: Format.formatter -> 'a -> unit + pp_term: 'a -> out_channel -> 'b -> unit; + pp_lenv: out_channel -> 'a -> unit } -val loc: string ref - -val level: int ref - -val clear: unit -> unit - -val warn: string -> unit - -val box: int -> unit - -val unbox: int -> unit - -val flush: int -> unit - -val box_err: unit -> unit - -val flush_err: unit -> unit +val specs: (unit, unit) specs val log: ('a, 'b) specs -> int -> ('a, 'b) message -> unit @@ -61,3 +45,5 @@ val et_items3: ?sc2:string -> ?c2:'a -> string -> 'b -> ?sc3:string -> ?c3:'a -> string -> 'b -> ('a, 'b) message + +val warn: int -> string -> unit diff --git a/helm/software/helena/src/lib/time.ml b/helm/software/helena/src/lib/time.ml index 42d7d39a7..7c59c22c5 100644 --- a/helm/software/helena/src/lib/time.ml +++ b/helm/software/helena/src/lib/time.ml @@ -12,13 +12,16 @@ module P = Printf module L = Log +let level = 1 + let utime_stamp = let old = ref 0.0 in fun msg -> let times = Unix.times () in let stamp = times.Unix.tms_utime in let lap = stamp -. !old in - L.warn (P.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap); + let str = P.sprintf "USR TIME STAMP (%s): %f (%f)" msg stamp lap in + L.warn level str; old := stamp let gmtime msg = @@ -29,6 +32,5 @@ let gmtime msg = let h = gmt.Unix.tm_hour in let m = gmt.Unix.tm_min in let s = gmt.Unix.tm_sec in - L.warn ( - P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s - ) + let str = P.sprintf "UTC TIME STAMP (%s): %u/%u/%u %u:%u:%u" msg yy mm dd h m s in + L.warn level str; diff --git a/helm/software/helena/src/modules.ml b/helm/software/helena/src/modules.ml index 63cadfb75..6f795219f 100644 --- a/helm/software/helena/src/modules.ml +++ b/helm/software/helena/src/modules.ml @@ -3,58 +3,58 @@ module U = NUri module K = NUri.UriHash -module C = cps -module W = share (**) -module L = log -module Y = time (**) - -module H = hierarchy -module N = level -module E = entity -module G = options -module O = output -module J = marks (**) -module R = alpha -module Q = ccs -module S = status - -module D = crg -module DO = crgOutput - -module T = txt -module TP = txtParser -module TL = txtLexer -module TT = txtTxt -module TD = txtCrg - -module A = aut -module AA = autProcess -module AO = autOutput -module AP = autParser -module AL = autLexer -module AD = autCrg - -module XL = xmlLibrary -module XD = xmlCrg - -module B = brg -module BD = brgCrg -module BO = brgOutput -module BE = brgEnvironment -module BS = brgSubstitution -module BR = brgReduction -module BT = brgType -module BV = brgValidity -module BU = brgUntrusted - -module Z = bag -module ZD = brgCrg -module ZO = bagOutput -module ZE = bagEnvironment -module ZS = bagSubstitution -module ZR = bagReduction -module ZT = bagType -module ZU = bagUntrusted +module C = Cps +module W = Share (**) +module L = Log +module Y = Time (**) + +module H = Hierarchy +module N = Level +module E = Entity +module G = Options +module O = Output +module J = Marks (**) +module R = Alpha +module Q = Ccs +module S = Status + +module D = Crg +module DO = CrgOutput + +module T = Txt +module TP = TxtParser +module TL = TxtLexer +module TT = TxtTxt +module TD = TxtCrg + +module A = Aut +module AA = AutProcess +module AO = AutOutput +module AP = AutParser +module AL = AutLexer +module AD = AutCrg + +module XL = XmlLibrary +module XD = XmlCrg + +module B = Brg +module BD = BrgCrg +module BO = BrgOutput +module BE = BrgEnvironment +module BS = BrgSubstitution +module BR = BrgReduction +module BT = BrgType +module BV = BrgValidity +module BU = BrgUntrusted + +module Z = Bag +module ZD = BrgCrg +module ZO = BagOutput +module ZE = BagEnvironment +module ZS = BagSubstitution +module ZR = BagReduction +module ZT = BagType +module ZU = BagUntrusted (* top *) diff --git a/helm/software/helena/src/text/txtLexer.mll b/helm/software/helena/src/text/txtLexer.mll index ea5c6e004..ec97a8b83 100644 --- a/helm/software/helena/src/text/txtLexer.mll +++ b/helm/software/helena/src/text/txtLexer.mll @@ -13,8 +13,10 @@ module L = Log module G = Options module TP = TxtParser + + let level = 0 - let out s = if !G.debug_lexer then L.warn s else () + let out s = if !G.debug_lexer then L.warn level s else () } let BS = "\\" diff --git a/helm/software/helena/src/toplevel/top.ml b/helm/software/helena/src/toplevel/top.ml index 52d2b0be2..afa62555d 100644 --- a/helm/software/helena/src/toplevel/top.ml +++ b/helm/software/helena/src/toplevel/top.ml @@ -47,13 +47,13 @@ type status = { zc : ZO.counters; } -let flush_all () = L.flush 0; L.flush_err () +let level = 0 let bag_error s msg = - L.error ZO.specs (L.Warn s :: L.Loc :: msg); flush_all () + L.error ZO.specs (L.Warn s :: msg) let brg_error s msg = - L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all () + L.error BR.specs (L.Warn s :: msg) let initial_status () = { kst = S.initial_status (); @@ -93,8 +93,8 @@ let xlate_entity entity = match !G.kernel, entity with let pp_progress e = let f a u = let s = U.string_of_uri u in - let err () = L.warn (P.sprintf "%s" s) in - let f i = L.warn (P.sprintf "[%u] %s" i s) in + let err () = L.warn 2 (P.sprintf "<%s>" s) in + let f i = L.warn 2 (P.sprintf "[%u] <%s>" i s) in E.apix err f a in match e with @@ -114,10 +114,11 @@ let export_entity = function let type_check st k = let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in + let bag_err msg = bag_error "Type Error" msg; failwith "Interrupted" in let ok _ _ = st in match k with | BrgEntity entity -> BU.type_check brg_err ok st.kst entity - | BagEntity entity -> ZU.type_check ok st.kst entity + | BagEntity entity -> ZU.type_check bag_err ok st.kst entity | CrgEntity _ -> st let validate st k = @@ -162,7 +163,7 @@ let type_of_input name = assert (H.set_graph "Z2"); Automath else begin - L.warn (P.sprintf "Unknown file type: %s" name); exit 2 + L.warn level (P.sprintf "Unknown file type: %s" name); exit 2 end let txt_xl = initial_lexer TxtLexer.token @@ -201,8 +202,6 @@ let count_input st = function (****************************************************************************) let version = ref true -let stage = ref 3 -let progress = ref false let preprocess = ref false let root = ref "" let export = ref false @@ -210,22 +209,22 @@ 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 st = if !G.summary then count_entity st entity else st in if !export then export_entity entity; - if !stage > 2 then + if !G.stage >= 3 then let f = if !version then validate else type_check in f st entity else st - + let process_1 st entity = - if !progress then pp_progress entity; - let st = if !L.level > 2 then count_entity st entity else st in - if !export && !stage = 1 then export_entity entity; - if !stage > 1 then process_2 st (xlate_entity entity) else st + if !G.trace >= 3 then pp_progress entity; + let st = if !G.summary then count_entity st entity else st in + if !export && !G.stage = 1 then export_entity entity; + if !G.stage >= 2 then process_2 st (xlate_entity entity) else st let process_0 st entity = let f st entity = - if !stage = 0 then st else + if !G.stage = 0 then st else match entity with | AutEntity e -> let err ast = {st with ast = ast} in @@ -237,7 +236,7 @@ let process_0 st entity = TD.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 + let st = if !G.summary 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 = @@ -268,76 +267,84 @@ let process st name = let lexbuf = Lexing.from_channel ich in let st = process st lexbuf input in close_in ich; - if !stage > 2 && !G.cc && !G.si then XL.export_csys st.kst.S.cc; + if !G.cc then XL.export_csys st.kst.S.cc; st, input -let main = -try +let main = let version_string = "Helena 0.8.2 M - November 2014" in - let print_version () = L.warn (version_string ^ "\n"); exit 0 in + let print_version () = L.warn level (version_string ^ "\n"); exit 0 in let set_hierarchy s = if H.set_graph s then () else - L.warn (P.sprintf "Unknown type hierarchy: %s" s) + L.warn level (P.sprintf "Unknown type hierarchy: %s" s) in let set_kernel = function | "brg" -> G.kernel := G.Brg | "bag" -> G.kernel := G.Bag - | s -> L.warn (P.sprintf "Unknown kernel version: %s" s) + | s -> L.warn level (P.sprintf "Unknown kernel version: %s" s) + in + let set_trace i = + if !G.trace = 0 && i > 0 then Y.gmtime version_string; + if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit"; + G.trace := i; + if i <= 1 then G.summary := false; + if i <= 1 then preprocess := false in - let set_summary i = L.level := i in - let set_stage i = stage := i in + let set_summary () = + if !G.trace >= 2 then G.summary := true + in + let set_preprocess () = + if !G.trace >= 2 then begin preprocess := true; G.summary := true end + in + let set_stage i = G.stage := i in let set_xdir s = G.xdir := s in let set_root s = root := s in let clear_options () = - progress := false; export := false; preprocess := false; - stage := 3; root := ""; + export := false; preprocess := false; + root := ""; st := initial_status (); - L.clear (); G.clear (); H.clear (); O.clear_reductions (); + G.clear (); H.clear (); O.clear_reductions (); streaming := false; version := true in let process_file name = - if !L.level > 0 then Y.gmtime version_string; - if !L.level > 1 then - L.warn (P.sprintf "Processing file: %s" name); - if !L.level > 0 then Y.utime_stamp "started"; + if !G.trace >= 2 then L.warn 1 (P.sprintf "Processing file: %s" name); + if !G.trace >= 2 then Y.utime_stamp "started"; let base_name = Filename.chop_extension (Filename.basename name) in let cover = F.concat !root base_name in - if !stage < 2 then G.kernel := G.Crg; + if !G.stage <= 1 then G.kernel := G.Crg; G.cover := cover; let sst, input = process (refresh_status !st) name in st := sst; - if !L.level > 0 then Y.utime_stamp "processed"; - if !L.level > 2 then begin + if !G.trace >= 2 then Y.utime_stamp "processed"; + if !G.summary then begin AO.print_counters C.start !st.ac; if !preprocess then AO.print_process_counters C.start !st.pst; - if !stage > 0 then print_counters !st G.Crg; - if !stage > 1 then print_counters !st !G.kernel; - if !stage > 2 then O.print_reductions () + if !G.stage >= 1 then print_counters !st G.Crg; + if !G.stage >= 2 then print_counters !st !G.kernel; + if !G.stage >= 3 then O.print_reductions () end in let exit () = - if !L.level > 0 then Y.utime_stamp "at exit"; - flush_all () + if !G.trace >= 1 then Y.utime_stamp "at exit" in let help = - "Usage: helena [ -LPVXcgijopqtx1 | -Ss | -O | -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" + "Usage: helena [ -LPVXcdgiopqtx1 | -Ts | -O | -hkr ]* [ ]*\n\n" ^ + "Trace levels: 0 just errors (default), 1 time stamps, 2 processed files, \ + 3 typing information, 4 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_O = " set location of output directory (XML) to (default: current directory)" in let help_P = " show parser debug information" in - let help_S = " set summary level (see above)" in + let help_T = " set trace level (see above)" in let help_V = " show version information" in let help_X = " clear options" in let help_c = " read/write conversion constraints" in + let help_d = " show summary information (requires trace >= 2)" in let help_g = " always expand global definitions" in let help_h = " set type hierarchy (default: \"Z1\")" in let help_i = " show local references by index" in - let help_j = " show URI of processed kernel objects" in let help_k = " set kernel version (default: \"brg\")" in let help_o = " activate sort inclusion" in let help_p = " preprocess source" in @@ -348,23 +355,22 @@ try let help_x = " export kernel entities (XML)" in let help_1 = " parse files with streaming policy" in - L.box 0; L.box_err (); at_exit exit; Arg.parse [ ("-L", Arg.Set G.debug_lexer, help_L); ("-O", Arg.String set_xdir, help_O); ("-P", Arg.Set G.debug_parser, help_P); - ("-S", Arg.Int set_summary, help_S); + ("-T", Arg.Int set_trace, help_T); ("-V", Arg.Unit print_version, help_V); ("-X", Arg.Unit clear_options, help_X); ("-c", Arg.Set G.cc, help_c); + ("-d", Arg.Unit set_summary, help_d); ("-g", Arg.Set G.expand, help_g); ("-h", Arg.String set_hierarchy, help_h); ("-i", Arg.Set G.indexes, help_i); - ("-j", Arg.Set progress, help_j); ("-k", Arg.String set_kernel, help_k); ("-o", Arg.Set G.si, help_o); - ("-p", Arg.Set preprocess, help_p); + ("-p", Arg.Unit set_preprocess, help_p); ("-q", Arg.Set G.unquote, help_q); ("-r", Arg.String set_root, help_r); ("-s", Arg.Int set_stage, help_s); @@ -372,4 +378,3 @@ try ("-x", Arg.Set export, help_x); ("-1", Arg.Set streaming, help_1); ] process_file help; -with ZT.TypeError msg -> bag_error "Type Error" msg