- brgOutput: the nodes count is now implemented

- brgReduction: the type annotation in the beta-reductum is useless
- brgType: a never-occurring condition marked with assert false

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index eb7f894e20d9dd5fbf25cd73276212832864c851..1f272e29e7a071fa43b8606b0f9c29bf9cb275d3 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -35,9 +35,9 @@ basic_rg/brg.cmo: lib/nUri.cmi lib/log.cmi lib/cps.cmx automath/aut.cmx
 basic_rg/brg.cmx: lib/nUri.cmx lib/log.cmx lib/cps.cmx automath/aut.cmx 
 basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx 
 basic_rg/brgOutput.cmo: lib/output.cmi lib/nUri.cmi lib/log.cmi \
-    lib/hierarchy.cmi basic_rg/brg.cmx basic_rg/brgOutput.cmi 
+    lib/hierarchy.cmi lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
 basic_rg/brgOutput.cmx: lib/output.cmx lib/nUri.cmx lib/log.cmx \
-    lib/hierarchy.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
+    lib/hierarchy.cmx lib/cps.cmx basic_rg/brg.cmx basic_rg/brgOutput.cmi 
 basic_rg/brgEnvironment.cmi: lib/nUri.cmi basic_rg/brg.cmx 
 basic_rg/brgEnvironment.cmo: lib/nUri.cmi lib/log.cmi basic_rg/brg.cmx \
     basic_rg/brgEnvironment.cmi 

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 *********************************************)

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 87d093d82f47638ea9580a89996d7f632482e0d6..16dc395bbfe39c7eb6e4c94a1936ae2ff2874705 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -107,7 +107,7 @@ let rec step f ?(delta=false) ?(rt=false) c m x =
             P.add ~beta:1 ~upsilon:(List.length tl) ();
            let f mc sc = step f ~delta ~rt c {c = mc; s = sc} t in
            let f mc = lift_stack (f mc) tl in 
-           let f v = B.push f m.c a (B.Abbr (B.Cast ([], w, v))) in
+           let f v = B.push f m.c a (B.Abbr v (* (B.Cast ([], w, v)) *) ) in
            S.lift f h (0) v
       end
    | B.Bind (a, b, t)        -> 

diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml
index 4bf5882a4885a48cf53e1fc4af257e875820bc9e..85ecf995a5f711dec601dbec6dcdfaaae6320e8c 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgType.ml
+++ b/helm/software/lambda-delta/basic_rg/brgType.ml
@@ -80,7 +80,7 @@ let rec b_type_of f g c x =
       let f xv = B.push (f xv) c a (B.Abbr xv) in
       let f xv vv = match xv with 
         | B.Cast _ -> f xv
-         | _        -> f (B.Cast ([], vv, xv))
+         | _        -> assert false (* f (B.Cast ([], vv, xv)) *)
       in
       type_of f g c v
    | B.Bind (a, B.Abst u, t) ->