new syntax of abstractions propagated to 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 7c9ab81724ec0befa9d37f77bf44ab07cc5a4ce1..dc5d78ce1f8f8dcb9f47d0aac9390fd7c2f7bf2d 100644 (file)
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -79,15 +79,15 @@ let rec count_term f c e = function
       count_binder f c e a b
 
 and count_binder f c e a b = match b with
-   | D.Abst (_, w) ->
+   | 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      -> 
+   | 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        ->
+   | D.Void           ->
       let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
       D.push_bind (f c) a b e
 
@@ -134,23 +134,25 @@ let pp_attrs out a =
    E.name ignore f 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 (a, l)    -> pp_attrs out a; out (KP.sprintf "*%u" l)
    | D.TLRef (a, i   ) -> pp_attrs out a; out (KP.sprintf "#%u" i)
    | D.TGRef (a, u)    -> pp_attrs out a; out (KP.sprintf "$")
-   | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out st x; out ">."; pp_term out st y
-   | D.TAppl (a, x, y) -> pp_attrs out a; out "("; pp_term out st x; out ")."; pp_term out st y
-   | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out st x; out "."; pp_term out st y
-   | D.TProj (a, x, y) -> pp_attrs out a; out "{"; pp_lenv out st x; out "}."; pp_term out st y
+   | D.TCast (a, u, t) -> pp_attrs out a; out "<"; pp_term out st u; out ">."; pp_term out st t
+   | D.TAppl (a, u, t) -> pp_attrs out a; out "("; pp_term out st u; out ")."; pp_term out st t
+   | D.TBind (a, u, t) -> pp_attrs out a; pp_bind out st u; out "."; pp_term out st t
+   | D.TProj (a, u, t) -> pp_attrs out a; out "{"; pp_lenv out st u; out "}."; pp_term out st t
 
 and pp_bind out st = function
-   | D.Abst (n, x) ->
-      out "[:"; pp_term out st x; out "]"; out (N.to_string st n); out " "  
-   | D.Abbr x      -> out "[="; pp_term out st x; out "] ";
-   | D.Void        -> out "[] "
+   | D.Abst (x, n, u) ->
+      out "[:"; pp_term out st u; out "]"; pp_state out x; 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 (x, a, y) -> pp_lenv out st x; pp_attrs out a; pp_bind out st y
-   | D.EAppl (x, a, y) -> pp_lenv out st x; out "("; pp_term out st y; out ") "
-   | D.EProj (x, a, y) -> pp_lenv out st x; out "{"; pp_lenv out st y; out "} "
+   | D.EBind (u, a, t) -> pp_lenv out st u; pp_attrs out a; pp_bind out st t
+   | D.EAppl (u, a, t) -> pp_lenv out st u; out "("; pp_term out st t; out ") "
+   | D.EProj (u, a, t) -> pp_lenv out st u; out "{"; pp_lenv out st t; out "} "