X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftoplevel%2Ftop.ml;h=579f5e6585211f665c3119548ebca5a44d79d10b;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=4a1446734153a79cd18e110ac973274a6ae7ad7e;hpb=f7988fc51f7c96617aa2b3320628645480af681a;p=helm.git

diff --git a/helm/software/lambda-delta/src/toplevel/top.ml b/helm/software/lambda-delta/src/toplevel/top.ml
index 4a1446734..579f5e658 100644
--- a/helm/software/lambda-delta/src/toplevel/top.ml
+++ b/helm/software/lambda-delta/src/toplevel/top.ml
@@ -20,34 +20,37 @@ module H  = Hierarchy
 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 ()
@@ -59,22 +62,23 @@ let brg_error s msg =
    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 ***********************************************************)
@@ -85,9 +89,9 @@ type kernel_entity = BrgEntity  of Brg.entity
 		   | 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  -> 
@@ -106,16 +110,16 @@ let pp_progress 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
@@ -194,8 +198,8 @@ let entity_of_input lexbuf i = match i, !parbuf with
 
 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
@@ -233,9 +237,9 @@ let process_0 st entity =
             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
@@ -314,8 +318,10 @@ try
       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