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:
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 \
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 \
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
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 =
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
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
V_______________________________________________________________ *)
module P = Printf
-module F = Format
module U = NUri
module L = Log
module G = Options
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
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 = {
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
(* 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)
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
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"
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
| 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
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
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
\ / 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
(* 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
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
V_______________________________________________________________ *)
module P = Printf
-module F = Format
module C = Cps
module U = NUri
module L = Log
xnodes: int
}
+let level = 2
+
let initial_counters = {
eabsts = 0; eabbrs = 0; evoids = 0;
tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
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 *************************************************)
(* 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 = {
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
(* Internal functions *******************************************************)
-let level = 5
+let level = 4
let log1 s c t =
let sc, st = s ^ " in the environment", "the term" in
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
| 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
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) ->
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
{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
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), _ ->
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
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 () *)
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
(* Internal functions *******************************************************)
-let level = 4
+let level = 3
let message1 st1 m t1 =
L.et_items1 "In the environment" m st1 t1
| _ -> 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))
(* 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
(* 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
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 =
| _, 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
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
| _ -> 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) ->
(* 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
(* 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 *)
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
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;
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)
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 ()
}
(* nodes count **************************************************************)
+let level = 2
+
type counters = {
eabsts: int;
eabbrs: int;
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 ******************************************)
\ / 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 "@,@[<v 2>%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 "@[<v>"
-
-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
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)
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
?sc2:string -> ?c2:'a -> string -> 'b ->
?sc3:string -> ?c3:'a -> string -> 'b ->
('a, 'b) message
+
+val warn: int -> string -> unit
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 =
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;
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
*)
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 = "\\"
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 ();
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
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 =
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
(****************************************************************************)
let version = ref true
-let stage = ref 3
-let progress = ref false
let preprocess = ref false
let root = ref ""
let export = ref false
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
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 =
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 <number> | -O <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"
+ "Usage: helena [ -LPVXcdgiopqtx1 | -Ts <number> | -O <dir> | -hkr <string> ]* [ <file> ]*\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 = "<dir> set location of output directory (XML) to <dir> (default: current directory)" in
let help_P = " show parser debug information" in
- let help_S = "<number> set summary level (see above)" in
+ let help_T = "<number> 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 = "<string> 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 = "<string> set kernel version (default: \"brg\")" in
let help_o = " activate sort inclusion" in
let help_p = " preprocess source" in
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);
("-x", Arg.Set export, help_x);
("-1", Arg.Set streaming, help_1);
] process_file help;
-with ZT.TypeError msg -> bag_error "Type Error" msg
projects / helm.git / commitdiff