let initial_counters = {
eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
let initial_counters = {
eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
- L.warn (P.sprintf " Total entry items: %6u" items);
- L.warn (P.sprintf " Declaration items: %6u" c.eabsts);
- L.warn (P.sprintf " Definition items: %6u" c.eabbrs);
- L.warn (P.sprintf " Total term items: %6u" terms);
- L.warn (P.sprintf " Sort items: %6u" c.tsorts);
- L.warn (P.sprintf " Local reference items: %6u" c.tlrefs);
- L.warn (P.sprintf " Global reference items: %6u" c.tgrefs);
- L.warn (P.sprintf " Explicit Cast items: %6u" c.tcasts);
- L.warn (P.sprintf " Application items: %6u" c.tappls);
- L.warn (P.sprintf " Abstraction items: %6u" c.tabsts);
- L.warn (P.sprintf " Abbreviation items: %6u" c.tabbrs);
+ L.warn (P.sprintf " Total entry items: %7u" items);
+ L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
+ L.warn (P.sprintf " Definition items: %7u" c.eabbrs);
+ L.warn (P.sprintf " Total term items: %7u" terms);
+ L.warn (P.sprintf " Sort items: %7u" c.tsorts);
+ L.warn (P.sprintf " Local reference items: %7u" c.tlrefs);
+ L.warn (P.sprintf " Global reference items: %7u" c.tgrefs);
+ L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts);
+ 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);
- | B.LRef i ->
- let f = function
- | Some (id, _) -> F.fprintf frm "@[%s@]" id
- | None -> F.fprintf frm "@[#%u@]" i
+ | B.LRef (_, i) ->
+ let f _ = function
+ | Some (a, _) -> F.fprintf frm "@[%a@]" id a
+ | None -> F.fprintf frm "@[#%u@]" i
- if !indexes then f None else B.get f c i
- | B.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
- | B.Cast (u, t) ->
+ if !O.indexes then f 0 None else B.get f c i
+ | B.GRef (_, s) -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
+ | B.Cast (_, u, t) ->
- B.push f c id (B.Abst w)
- | B.Bind (id, B.Abbr v, t) ->
+ B.push f c a (B.Abst w)
+ | B.Bind (a, B.Abbr v, t) ->
- B.push f c id (B.Abbr v)
- | B.Bind (id, B.Void, t) ->
- let f cc = F.fprintf frm "@[[%s].%a@]" id (pp_term cc) t in
- B.push f c id B.Void
+ B.push f c a (B.Abbr v)
+ | B.Bind (a, B.Void, t) ->
+ let f cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in
+ B.push f c a B.Void
- | id, B.Abst w ->
- F.fprintf frm "@,@[%s : %a@]" id (pp_term c) w
- | id, B.Abbr v ->
- F.fprintf frm "@,@[%s = %a@]" id (pp_term c) v
- | id, B.Void ->
- F.fprintf frm "@,%s" id
+ | a, B.Abst w ->
+ F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w
+ | a, B.Abbr v ->
+ F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v
+ | a, B.Void ->
+ F.fprintf frm "@,%a" id a