X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;h=f068181a789e034488563d970cde256d181d0969;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=49acbb49bbd421594510bff97bdc9e2c74b610a0;hpb=f72311aa07e71090a24eef9e4fb97cc2e95e6b16;p=helm.git

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 49acbb49b..f068181a7 100644
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -9,13 +9,14 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P = Printf
+module KP = Printf
+
 module U = NUri
 module C = Cps
 module L = Log
-module H = Hierarchy
+module P = Marks
+module N = Layer
 module E = Entity
-module N = Level
 module D = Crg
 
 (* nodes count **************************************************************)
@@ -46,72 +47,62 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term f c e = function
-   | D.TSort _          -> 
+   | D.TSort _         -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
-   | D.TLRef (_, i, j)  -> 
+   | D.TLRef (_, i)    -> 
       begin match D.get e i with
-	 | _, _, D.Abbr vs when j < List.length vs ->
+	 | _, _, _, D.Abbr _ ->
 	    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)     -> 
+   | 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)  -> 
+   | 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
+   | D.TAppl (_, v, t) -> 
+      let c = {c with tappls = succ c.tappls} 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 (D.tshift d t)
-   | D.TBind (a, b, t)  -> 
+      count_term f c e v
+   | D.TProj (d, t)    ->
+      D.shift (count_term f c e) d t
+   | D.TBind (y, 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
+      count_binder f c e y b
+
+and count_binder f c e y b = match b with
+   | D.Abst (_, _, w) ->
+      let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
+      let f c = D.push_bind (f c) E.empty_node y b e in
+      count_term f c e w
+   | D.Abbr v         -> 
+      let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
+      let f c = D.push_bind (f c) E.empty_node y b e in
+      count_term f c e v     
+   | D.Void           ->
+      let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
+      D.push_bind (f c) E.empty_node y 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 =
@@ -120,60 +111,54 @@ let print_counters f c =
    in
    let items = c.eabsts + c.eabbrs in
    let nodes = c.nodes + c.xnodes 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);
-   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);
+   let marks = P.marks () in
+   L.warn level (KP.sprintf "Intermediate representation summary (complete_rg)");
+   L.warn level (KP.sprintf "  Total entry items:        %7u" items);
+   L.warn level (KP.sprintf "    Declaration items:      %7u" c.eabsts);
+   L.warn level (KP.sprintf "    Definition items:       %7u" c.eabbrs);
+   L.warn level (KP.sprintf "  Total term items:         %7u" terms);
+   L.warn level (KP.sprintf "    Sort items:             %7u" c.tsorts);
+   L.warn level (KP.sprintf "    Local reference items:  %7u" c.tlrefs);
+   L.warn level (KP.sprintf "    Global reference items: %7u" c.tgrefs);
+   L.warn level (KP.sprintf "    Explicit Cast items:    %7u" c.tcasts);
+   L.warn level (KP.sprintf "    Application items:      %7u" c.tappls);
+   L.warn level (KP.sprintf "    Abstraction items:      %7u" c.tabsts);
+   L.warn level (KP.sprintf "    Abbreviation items:     %7u" c.tabbrs);
+   L.warn level (KP.sprintf "  Ambiguous abstractions:   %7u" marks);   
+   L.warn level (KP.sprintf "  Global Int. Complexity:   %7u" c.nodes);
+   L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
 
+END
+
 (* 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 rec pp_term out = function
-   | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
-   | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
-   | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
-   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
-   | D.TProj (a, x, y) -> assert false
-   | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
-
-and pp_terms bg eg out vs =
-   let rec aux = function
-      | []      -> ()
-      | [v]     -> pp_term out v
-      | v :: vs -> pp_term out v; out ", "; aux vs
-   in
-   out bg; aux vs; out (eg ^ ".")
-
-and pp_bind out = function
-   | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x
-   | D.Abst (n, x)                      -> 
-      pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x
-   | D.Abbr x                           -> pp_terms "[=" "]" out x
-   | D.Void x                           -> out (P.sprintf "[%u]" x)
-
-let rec pp_lenv out = 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
+let pp_b_attrs out a =
+   let f s b = if b then out (KP.sprintf "%s;" s) else out (KP.sprintf "~%s;" s) in
+   E.name ignore f a
+
+let pp_n_attrs out a =
+   out (KP.sprintf "+%i;" a.E.n_apix)
+
+let pp_state out x = if x then out "^"
+
+let rec pp_term out st = function
+   | D.TSort k         -> out (KP.sprintf "*%u" k)
+   | D.TLRef (a, i)    -> pp_n_attrs out a; out (KP.sprintf "#%u" i)
+   | D.TGRef (a, u)    -> pp_n_attrs out a; out (KP.sprintf "$")
+   | D.TCast (u, t)    -> out "<"; pp_term out st u; out ">."; pp_term out st t
+   | D.TAppl (_, u, t) -> out "("; pp_term out st u; out ")."; pp_term out st t
+   | D.TBind (y, u, t) -> pp_b_attrs out y; pp_bind out st u; out "."; pp_term out st t
+   | D.TProj (u, t)    -> out "{"; pp_lenv out st u; out "}."; pp_term out st t
+
+and pp_bind out st = function
+   | D.Abst (r, n, u) ->
+      out "[:"; pp_term out st u; out "]"; pp_state out r; out (N.to_string st n); out " "  
+   | D.Abbr u         -> out "[="; pp_term out st u; out "] ";
+   | D.Void           -> out "[] "
+
+and pp_lenv out st = function
+   | D.ESort              -> ()
+   | D.EBind (u, a, y, t) -> pp_lenv out st u; pp_b_attrs out y; pp_n_attrs out a; pp_bind out st t
+   | D.EAppl (u, _, t)    -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+   | D.EProj (u, t)       -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "