- new attributes system

[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index d5f639b392d6721e45c2cee02f1b1764b9040389..529a293e1a79d737d8775a9ec96f51e83330dcc9 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -13,8 +13,9 @@ module P = Printf
 module U = NUri
 module C = Cps
 module L = Log
-module E = Entity
+module J = Marks
 module N = Level
+module E = Entity
 module D = Crg
 
 (* nodes count **************************************************************)
@@ -90,15 +91,15 @@ and count_binder f c e a b = match b with
       D.push_bind (f c) a b e
 
 let count_entity f c = function
-   | _, u, E.Abst (_, w) -> 
+   | _, _, 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      ->  
+   | _, _, _, 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
+   | _, _, _, E.Void   -> assert false
 
 let print_counters f c =
    let terms =
@@ -107,6 +108,7 @@ let print_counters f c =
    in
    let items = c.eabsts + c.eabbrs in
    let nodes = c.nodes + c.xnodes in
+   let marks = J.marks () in
    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);
@@ -119,6 +121,7 @@ let print_counters f c =
    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 "  Ambiguous abstractions:   %7u" marks);   
    L.warn level (P.sprintf "  Global Int. Complexity:   %7u" c.nodes);
    L.warn level (P.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
@@ -126,15 +129,10 @@ let print_counters f c =
 (* term/environment pretty printer ******************************************)
 
 let pp_attrs out a =
-   let map = function
-      | E.Name (s, true)  -> out (P.sprintf "%s;" s)
-      | E.Name (s, false) -> out (P.sprintf "~%s;" s)
-      | E.Apix i          -> out (P.sprintf "+%i;" i)
-      | E.Mark i          -> out (P.sprintf "@%i;" i)
-      | E.Meta _          -> ()
-      | E.Info _          -> ()
-   in
-   List.iter map a
+   let f s b = if b then out (P.sprintf "%s;" s) else out (P.sprintf "~%s;" s) in
+   E.name ignore f a;
+   let f i = out (P.sprintf "+%i;" i) in
+   E.apix ignore f a
 
 let rec pp_term out = function
    | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
@@ -147,8 +145,7 @@ let rec pp_term out = function
 
 and pp_bind out = function
    | D.Abst (n, x) ->
-      out "[:"; pp_term out x; out "]";
-      if N.is_infinite n then () else out (N.to_string n)  
+      out "[:"; pp_term out x; out "]"; out (N.to_string n)  
    | D.Abbr x      -> out "[="; pp_term out x; out "]";
    | D.Void        -> out "[]"