new intermediate language complete_rg,

[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 49acbb49bbd421594510bff97bdc9e2c74b610a0..d5f639b392d6721e45c2cee02f1b1764b9040389 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -13,7 +13,6 @@ module P = Printf
 module U = NUri
 module C = Cps
 module L = Log
-module H = Hierarchy
 module E = Entity
 module N = Level
 module D = Crg
@@ -49,11 +48,11 @@ let initial_counters = {
 let rec count_term f c e = function
    | 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)     -> 
@@ -67,40 +66,28 @@ let rec count_term f c e = function
       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)
+      count_term f c e v
+   | D.TProj (_, d, t)  ->
+      D.shift (count_term f c e) d t
    | D.TBind (a, 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
+and count_binder f c e a 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) a 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) a 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) a b e
 
 let count_entity f c = function
    | _, u, E.Abst (_, w) -> 
@@ -151,29 +138,22 @@ let pp_attrs out 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.TLRef (a, i   ) -> pp_attrs out a; out (P.sprintf "#%u" i)
    | 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 ^ ".")
+   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out x; out ")."; pp_term out y
+   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; out "."; pp_term out y
+   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out x; out "}."; pp_term out y
 
 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)
+   | D.Abst (n, x) ->
+      out "[:"; pp_term out x; out "]";
+      if N.is_infinite n then () else out (N.to_string n)  
+   | D.Abbr x      -> out "[="; pp_term out x; out "]";
+   | D.Void        -> out "[]"
 
-let rec pp_lenv out = function
+and 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
+   | D.EAppl (x, a, y) -> pp_lenv out x; out "("; pp_term out y; out ")"
+   | D.EProj (x, a, y) -> pp_lenv out x; out "{"; pp_lenv out y; out "}"