- brgOutput: the nodes count is now implemented

[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index 2d1fa96ae846b1f81cc10fa06ebc637af621ad2f..aaa559be687f46f0d89a8a1b3de72a00269a8731 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -22,59 +22,83 @@ module B = Brg
 type counters = {
    eabsts: int;
    eabbrs: int;
+   evoids: int;
    tsorts: int;
    tlrefs: int;
    tgrefs: int;
    tcasts: int;
    tappls: int;
    tabsts: int;
-   tabbrs: int
+   tabbrs: int;
+   tvoids: int;
+   uris  : U.uri list;
+   nodes : int;
+   xnodes: int
 }
 
 let initial_counters = {
-   eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
-   tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
+   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 count_term_binder f c = function
+let rec count_term_binder f c e = function
    | B.Abst w ->
-      let c = {c with tabsts = succ c.tabsts} in
-      count_term f c w
+      let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
+      count_term f c e w
    | B.Abbr v -> 
-      let c = {c with tabbrs = succ c.tabbrs} in
-      count_term f c v
-   | B.Void   -> f c
+      let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
+      count_term f c e v
+   | B.Void   ->
+      let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in   
+      f c
 
-and count_term f c = function
-   | B.Sort _            -> 
-      f {c with tsorts = succ c.tsorts}
-   | B.LRef _         -> 
-      f {c with tlrefs = succ c.tlrefs}
-   | B.GRef _         -> 
+and count_term f c e = function
+   | B.Sort _         -> 
+      f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
+   | B.LRef (_, i)    -> 
+      let f _ = function
+         | None
+        | Some (_, B.Abst _) ->
+           f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
+        | Some (_, B.Abbr _)
+        | Some (_, B.Void)   ->
+           f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
+      in        
+      B.get f e i
+   | B.GRef (_, u)    -> 
+      let c =    
+        if Cps.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}
    | B.Cast (_, v, t) -> 
       let c = {c with tcasts = succ c.tcasts} in
-      let f c = count_term f c t in
-      count_term f c v
+      let f c = count_term f c e t in
+      count_term f c e v
    | B.Appl (_, v, t) -> 
-      let c = {c with tappls = succ c.tappls} in
-      let f c = count_term f c t in
-      count_term f c v
-   | B.Bind (_, b, t) -> 
-      let f c = count_term_binder f c b in
-      count_term f c t
-
-let count_obj_binder f c = function
-   | B.Abst w -> 
-      let c = {c with eabsts = succ c.eabsts} in
-      count_term f c w
-   | B.Abbr v -> 
-      let c = {c with eabbrs = succ c.eabbrs} in
-      count_term f c v
-   | B.Void   -> f c
+      let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
+      let f c = count_term f c e t in
+      count_term f c e v
+   | B.Bind (a, b, t) -> 
+      let f c e = count_term f c e t in
+      let f c = B.push (f c) e a b in
+      count_term_binder f c e b
 
-let count_obj f c (_, _, b) =
-   count_obj_binder f c b
+let count_obj f c = function
+   | (_, u, B.Abst w) -> 
+      let c = {c with
+         eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
+      } in
+      count_term f c B.empty_context w
+   | (_, _, B.Abbr v) ->  
+      let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
+      count_term f c B.empty_context v
+   | (_, _, B.Void)   ->
+      let c = {c with evoids = succ c.evoids; xnodes = succ c.xnodes} in
+      f c
 
 let count_item f c = function
    | Some obj -> count_obj f c obj
@@ -86,6 +110,7 @@ let print_counters f c =
       c.tabbrs
    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);
@@ -98,6 +123,8 @@ let print_counters f c =
    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 ()
 
 (* context/term pretty printing *********************************************)