src/complete_rg/crg.cmo: src/common/level.cmi src/common/entity.cmx
src/complete_rg/crg.cmx: src/common/level.cmx src/common/entity.cmx
src/complete_rg/crgOutput.cmi: src/complete_rg/crg.cmx
-src/complete_rg/crgOutput.cmo: src/common/level.cmi src/common/hierarchy.cmi \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/complete_rg/crgOutput.cmi
-src/complete_rg/crgOutput.cmx: src/common/level.cmx src/common/hierarchy.cmx \
- src/common/entity.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmo: src/lib/log.cmi src/common/level.cmi \
+ src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
+src/complete_rg/crgOutput.cmx: src/lib/log.cmx src/common/level.cmx \
+ src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crg.cmx \
+ src/lib/cps.cmx src/complete_rg/crgOutput.cmi
src/complete_rg/crgTxt.cmi: src/text/txt.cmx src/complete_rg/crg.cmx
src/complete_rg/crgTxt.cmo: src/text/txtTxt.cmi src/text/txt.cmx \
src/common/options.cmx src/common/hierarchy.cmi src/common/entity.cmx \
src/toplevel/metaBrg.cmi src/toplevel/metaBag.cmi \
src/toplevel/metaAut.cmi src/toplevel/meta.cmx src/lib/log.cmi \
src/common/hierarchy.cmi src/common/entity.cmx src/complete_rg/crgTxt.cmi \
- src/complete_rg/crgAut.cmi src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/basic_rg/brgUntrusted.cmi src/basic_rg/brgReduction.cmi \
- src/basic_rg/brgOutput.cmi src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
+ src/complete_rg/crgOutput.cmi src/complete_rg/crgAut.cmi \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmi \
+ src/basic_rg/brgReduction.cmi src/basic_rg/brgOutput.cmi \
+ src/basic_rg/brgCrg.cmi src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmi src/basic_ag/bagType.cmi \
src/basic_ag/bagOutput.cmi src/basic_ag/bag.cmx \
src/automath/autProcess.cmi src/automath/autParser.cmi \
src/toplevel/metaBrg.cmx src/toplevel/metaBag.cmx \
src/toplevel/metaAut.cmx src/toplevel/meta.cmx src/lib/log.cmx \
src/common/hierarchy.cmx src/common/entity.cmx src/complete_rg/crgTxt.cmx \
- src/complete_rg/crgAut.cmx src/complete_rg/crg.cmx src/lib/cps.cmx \
- src/basic_rg/brgUntrusted.cmx src/basic_rg/brgReduction.cmx \
- src/basic_rg/brgOutput.cmx src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
+ src/complete_rg/crgOutput.cmx src/complete_rg/crgAut.cmx \
+ src/complete_rg/crg.cmx src/lib/cps.cmx src/basic_rg/brgUntrusted.cmx \
+ src/basic_rg/brgReduction.cmx src/basic_rg/brgOutput.cmx \
+ src/basic_rg/brgCrg.cmx src/basic_rg/brg.cmx \
src/basic_ag/bagUntrusted.cmx src/basic_ag/bagType.cmx \
src/basic_ag/bagOutput.cmx src/basic_ag/bag.cmx \
src/automath/autProcess.cmx src/automath/autParser.cmx \
$(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt
test-si-old: $(MAIN).opt etc
- @echo " HELENA -o -p -u $(INPUT)"
- $(H)./$(MAIN).opt -o -p -u -S 3 $(O) $(INPUT) > etc/log.txt
+ @echo " HELENA -o -p -u -c $(INPUT)"
+ $(H)./$(MAIN).opt -o -p -u -c -S 3 $(O) $(INPUT) > etc/log.txt
test-si-fast-old: $(MAIN).opt etc
@echo " HELENA -o -u -q $(INPUT)"
let push_proj f lenv a e = f (EProj (lenv, a, e))
-let push2 err f lenv attr ?t () = match lenv, t with
- | EBind (e, a, Abst (n, ws)), Some t ->
+let push2 err f lenv ?attr ?t () = match lenv, attr, t with
+ | EBind (e, a, Abst (n, ws)), Some attr, Some t ->
f (EBind (e, (attr :: a), Abst (n, t :: ws)))
- | EBind (e, a, Abbr vs), Some t ->
+ | EBind (e, a, Abst (n, ws)), None, Some t ->
+ f (EBind (e, a, Abst (n, t :: ws)))
+ | EBind (e, a, Abbr vs), Some attr, Some t ->
f (EBind (e, (attr :: a), Abbr (t :: vs)))
- | EBind (e, a, Void n), None ->
+ | EBind (e, a, Abbr vs), None, Some t ->
+ f (EBind (e, a, Abbr (t :: vs)))
+ | EBind (e, a, Void n), Some attr, None ->
f (EBind (e, (attr :: a), Void (succ n)))
- | _ -> err ()
+ | EBind (e, a, Void n), None, None ->
+ f (EBind (e, a, Void (succ n)))
+ | _ -> err ()
(* this id not tail recursive *)
let resolve_lref err f id lenv =
| ESort -> ns
| EBind (tl, a, _) -> names_of_lenv (E.rev_append_names ns a) tl
| EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
+
+let rec get i = function
+ | ESort -> ESort, [], Void 0
+ | EBind (e, _, Abst (_, []))
+ | EBind (e, _, Abbr [])
+ | EBind (e, _, Void 0) -> get i e
+ | EBind (e, a, b) when i = 0 -> e, a, b
+ | EBind (e, _, _) -> get (pred i) e
+ | EProj _ -> assert false (* TODO *)
+
+let get e i = get i e
module P = Printf
module U = NUri
module C = Cps
+module L = Log
module H = Hierarchy
module E = Entity
module N = Level
module D = Crg
-(****************************************************************************)
+(* nodes count **************************************************************)
+
+type counters = {
+ eabsts: int;
+ eabbrs: int;
+ evoids: int;
+ tsorts: int;
+ tlrefs: int;
+ tgrefs: int;
+ tcasts: int;
+ tappls: int;
+ tabsts: int;
+ tabbrs: int;
+ tvoids: int;
+ uris : D.uri list;
+ nodes : int;
+ xnodes: int
+}
+
+let initial_counters = {
+ eabsts = 0; eabbrs = 0; evoids = 0;
+ tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
+ tabsts = 0; tabbrs = 0; tvoids = 0;
+ uris = []; nodes = 0; xnodes = 0
+}
+
+let rec shift t = function
+ | D.ESort -> t
+ | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e
+ | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e
+
+let rec count_term f c e = function
+ | D.TSort _ ->
+ f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
+ | D.TLRef (_, i, j) ->
+ begin match D.get e i with
+ | _, _, D.Abbr vs when j < List.length vs ->
+ f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
+ | _ ->
+ f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
+ end
+ | D.TGRef (_, u) ->
+ let c =
+ if C.list_mem ~eq:U.eq u c.uris
+ then {c with nodes = succ c.nodes}
+ else {c with xnodes = succ c.xnodes}
+ in
+ f {c with tgrefs = succ c.tgrefs}
+ | D.TCast (_, v, t) ->
+ let c = {c with tcasts = succ c.tcasts} in
+ let f c = count_term f c e t in
+ count_term f c e v
+ | D.TAppl (_, vs, t) ->
+ let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
+ let f c = count_term f c e t in
+ C.list_fold_right f (map1 e) vs c
+ | D.TProj (a, d, t) ->
+ count_term f c e (shift t d)
+ | D.TBind (a, b, t) ->
+ let f c e = count_term f c e t in
+ count_binder f c e a b
+
+and count_binder f c e a = function
+ | D.Abst (n, ws) ->
+ let k = List.length ws in
+ let c = {c with tabsts = c.tabsts + k; nodes = c.nodes + k} in
+ let e = D.push_bind C.start e a (D.Abst (n, [])) in
+ let f (c, e) = f c e in
+ C.list_fold_right f map2 ws (c, e)
+ | D.Abbr vs ->
+ let k = List.length vs in
+ let c = {c with tabbrs = c.tabbrs + k; xnodes = c.xnodes + k} in
+ let e = D.push_bind C.start e a (D.Abbr []) in
+ let f (c, e) = f c e in
+ C.list_fold_right f map2 vs (c, e)
+ | D.Void k ->
+ let c = {c with tvoids = c.tvoids + k; xnodes = c.xnodes + k} in
+ let e = D.push_bind C.start e a (D.Void k) in
+ f c e
+
+and map1 e f t c = count_term f c e t
+
+and map2 f t (c, e) =
+ let f c e = f (c, e) in
+ let f c = D.push2 C.err (f c) e ~t () in
+ count_term f c e t
+
+let count_entity f c = function
+ | _, u, E.Abst (_, w) ->
+ let c = {c with
+ eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
+ } in
+ count_term f c D.ESort w
+ | _, _, E.Abbr v ->
+ let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
+ count_term f c D.ESort v
+ | _, _, E.Void -> assert false
+
+let print_counters f c =
+ let terms =
+ c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
+ c.tabbrs
+ 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);
+ f ()
+
+(* term/environment pretty printer ******************************************)
let pp_attrs out a =
let map = function
| D.ESort -> ()
| D.EProj (x, a, y) -> assert false
| D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
-
-(****************************************************************************)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+type counters
+
+val initial_counters: counters
+
+val count_entity: (counters -> 'a) -> counters -> Crg.entity -> 'a
+
+val print_counters: (unit -> 'a) -> counters -> 'a
+
val pp_term: (string -> unit) -> Crg.term -> unit
let abst_map (lenv, a, wws) (id, r, w) =
let attr = name_of_id ~r id in
let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+ D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
in
let abbr_map (lenv, a, wws) (id, w) =
let attr = name_of_id id in
let ww = xlate_term C.start st lenv w in
- D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+ D.push2 C.err C.start lenv ~attr ~t:ww (), attr :: a, ww :: wws
in
let void_map (lenv, a, n) id =
let attr = name_of_id id in
- D.push2 C.err C.start lenv attr (), attr :: a, succ n
+ D.push2 C.err C.start lenv ~attr (), attr :: a, succ n
in
let lenv, aa, bb = match b with
| T.Abst xws ->
let pars = c.pabsts + c.pappls in
let entries = c.eabsts + c.eabbrs in
let nodes = c.nodes + c.xnodes in
- L.warn (P.sprintf " Intermediate representation summary");
+ L.warn (P.sprintf " Intermediate representation summary (meta)");
L.warn (P.sprintf " Total entries: %7u" entries);
L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
L.warn (P.sprintf " Definition items: %7u" c.eabbrs);
module O = Output
module E = Entity
module S = Status
-module XL = XmlLibrary
-module XD = XmlCrg
+module TD = CrgTxt
module AA = AutProcess
module AO = AutOutput
-module TD = CrgTxt
module AD = CrgAut
-module MA = MetaAut
-module MO = MetaOutput
-module MB = MetaBrg
+module DO = CrgOutput
+module XL = XmlLibrary
+module XD = XmlCrg
module BD = BrgCrg
module BO = BrgOutput
module BR = BrgReduction
module BU = BrgUntrusted
-module MZ = MetaBag
module ZO = BagOutput
module ZT = BagType
module ZU = BagUntrusted
+module MA = MetaAut
+module MO = MetaOutput
+module MB = MetaBrg
+module MZ = MetaBag
+
type status = {
- ast : AA.status;
- dst : AD.status;
- mst : MA.status;
- tst : TD.status;
- ac : AO.counters;
- mc : MO.counters;
- brgc: BO.counters;
- bagc: ZO.counters;
- kst : S.status
+ kst: S.status;
+ tst: TD.status;
+ pst: AA.status;
+ ast: AD.status;
+ ac : AO.counters;
+ dc : DO.counters;
+ bc : BO.counters;
+ zc : ZO.counters;
+ mst: MA.status;
+ mc : MO.counters;
}
let flush_all () = L.flush 0; L.flush_err ()
L.error BR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
let initial_status () = {
- ac = AO.initial_counters;
- mc = MO.initial_counters;
- brgc = BO.initial_counters;
- bagc = ZO.initial_counters;
- mst = MA.initial_status ();
- dst = AD.initial_status ();
- tst = TD.initial_status ();
- ast = AA.initial_status ();
- kst = S.initial_status ()
+ kst = S.initial_status ();
+ tst = TD.initial_status ();
+ pst = AA.initial_status ();
+ ast = AD.initial_status ();
+ ac = AO.initial_counters;
+ dc = DO.initial_counters;
+ bc = BO.initial_counters;
+ zc = ZO.initial_counters;
+ mst = MA.initial_status ();
+ mc = MO.initial_counters;
}
let refresh_status st = {st with
- mst = MA.refresh_status st.mst;
- dst = AD.refresh_status st.dst;
+ kst = S.refresh_status st.kst;
tst = TD.refresh_status st.tst;
- kst = S.refresh_status st.kst
+ ast = AD.refresh_status st.ast;
+ mst = MA.refresh_status st.mst;
}
(* kernel related ***********************************************************)
| MetaEntity of Meta.entity
let print_counters st = function
- | G.Brg -> BO.print_counters C.start st.brgc
- | G.Bag -> ZO.print_counters C.start st.bagc
- | G.Crg -> ()
+ | G.Crg -> DO.print_counters C.start st.dc
+ | G.Brg -> BO.print_counters C.start st.bc
+ | G.Bag -> ZO.print_counters C.start st.zc
let xlate_entity entity = match !G.kernel, entity with
| G.Brg, CrgEntity e ->
E.mark err f a
in
match e with
- | CrgEntity e -> E.common f e
- | BrgEntity e -> E.common f e
- | BagEntity e -> E.common f e
+ | CrgEntity e -> E.common f e
+ | BrgEntity e -> E.common f e
+ | BagEntity e -> E.common f e
| MetaEntity e -> E.common f e
let count_entity st = function
+ | BrgEntity e -> {st with bc = BO.count_entity C.start st.bc e}
+ | BagEntity e -> {st with zc = ZO.count_entity C.start st.zc e}
+ | CrgEntity e -> {st with dc = DO.count_entity C.start st.dc e}
| MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e}
- | BrgEntity e -> {st with brgc = BO.count_entity C.start st.brgc e}
- | BagEntity e -> {st with bagc = ZO.count_entity C.start st.bagc e}
- | _ -> st
let export_entity = function
| CrgEntity e -> XL.export_entity XD.export_term e
let process_input f st = function
| AutEntity e ->
- let f ast e = f {st with ast = ast} (AutEntity e) in
- AA.process_command f st.ast e
+ let f pst e = f {st with pst = pst} (AutEntity e) in
+ AA.process_command f st.pst e
| xe -> f st xe
let count_input st = function
let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
MA.meta_of_aut frr h st.mst e
| AutEntity e, false ->
- let err dst = {st with dst = dst} in
- let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
- AD.crg_of_aut err g st.dst e
+ let err ast = {st with ast = ast} in
+ let g ast e = process_1 {st with ast = ast} (CrgEntity e) in
+ AD.crg_of_aut err g st.ast e
| TxtEntity e, _ ->
let crr tst = {st with tst = tst} in
let d tst e = process_1 {st with tst = tst} (CrgEntity e) in
if !L.level > 0 then Y.utime_stamp "processed";
if !L.level > 2 then begin
AO.print_counters C.start !st.ac;
- if !preprocess then AO.print_process_counters C.start !st.ast;
- if !stage > 0 then MO.print_counters C.start !st.mc;
+ if !preprocess then AO.print_process_counters C.start !st.pst;
+ if !stage > 0 then
+ if !old then MO.print_counters C.start !st.mc
+ else print_counters !st G.Crg;
if !stage > 1 then print_counters !st !G.kernel;
if !stage > 2 then O.print_reductions ()
end
pp_lenv print_string e; print_string " |- ";
pp_term print_string hd; print_newline ();
*)
- map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+ map e hd out tab; f (D.push2 C.err C.start e ~attr:n ~t:hd ())
in
aux err f e (ns, tl)
| _ -> err ()
let a, ns = Y.get_names f a in
match b with
| D.Abst (n, ws) ->
- let e = D.push_bind C.start e a (D.Abst (n, ws)) in
+ let e = D.push_bind C.start e a (D.Abst (n, [])) in
let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
| D.Abbr vs ->
- let e = D.push_bind C.start e a (D.Abbr vs) in
+ let e = D.push_bind C.start e a (D.Abbr []) in
let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
| D.Void n ->
projects / helm.git / commitdiff