}
let rec count_term_binder f c e = function
- | B.Abst (_, w) ->
+ | B.Abst (_, _, w) ->
let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
count_term f c e w
- | B.Abbr v ->
+ | B.Abbr v ->
let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
count_term f c e v
- | B.Void ->
+ | B.Void ->
let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
f c
in
E.name err f a
+let pp_reduced och x =
+ if x then KP.fprintf och "%s" "^"
+
let pp_level st och n =
KP.fprintf och "%s" (N.to_string st n)
let rec pp_term st e och = function
- | B.Sort (_, h) ->
+ | B.Sort (_, h) ->
let err _ = KP.fprintf och "*%u" h in
let f s = KP.fprintf och "%s" s in
H.string_of_sort err f h
- | B.LRef (_, i) ->
+ | B.LRef (_, i) ->
let err _ = KP.fprintf och "#%u" i in
if !G.indexes then err () else
let _, _, a, b = B.get e i in
KP.fprintf och "%a" (name err) a
- | B.GRef (_, s) ->
+ | B.GRef (_, s) ->
KP.fprintf och "$%s" (U.string_of_uri s)
- | B.Cast (_, u, t) ->
+ | B.Cast (_, u, t) ->
KP.fprintf och "{%a}.%a" (pp_term st e) u (pp_term st e) t
- | B.Appl (_, v, t) ->
+ | B.Appl (_, v, t) ->
KP.fprintf och "(%a).%a" (pp_term st e) v (pp_term st e) t
- | B.Bind (a, B.Abst (n, w), t) ->
+ | B.Bind (a, B.Abst (x, n, w), t) ->
let a = R.alpha B.mem e a in
- let ee = B.push e B.empty a (B.abst n w) in
- KP.fprintf och "%a[%a:%a].%a" (pp_level st) n (name C.start) a (pp_term st e) w (pp_term st ee) t
- | B.Bind (a, B.Abbr v, t) ->
+ let ee = B.push e B.empty a (B.abst x n w) in
+ KP.fprintf och "%a%a[%a:%a].%a" (pp_level st) n pp_reduced x (name C.start) a (pp_term st e) w (pp_term st ee) t
+ | B.Bind (a, B.Abbr v, t) ->
let a = R.alpha B.mem e a in
let ee = B.push e B.empty a (B.abbr v) in
KP.fprintf och "[%a=%a].%a" (name C.start) a (pp_term st e) v (pp_term st ee) t
- | B.Bind (a, B.Void, t) ->
+ | B.Bind (a, B.Void, t) ->
let a = R.alpha B.mem e a in
let ee = B.push e B.empty a B.Void in
KP.fprintf och "[%a].%a" (name C.start) a (pp_term st ee) t