module P = Printf
module F = Format
module U = NUri
-module C = Cps
module L = Log
+module O = Options
+module Y = Entity
module H = Hierarchy
module B = Bag
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 count_entity f c = function
+ | _, _, Y.Abst w ->
let c = {c with eabsts = succ c.eabsts} in
count_term f c w
- | B.Abbr v ->
+ | _, _, Y.Abbr v ->
let c = {c with eabbrs = succ c.eabbrs} in
count_term f c v
- | B.Void -> f c
-
-let count_obj f c (_, _, b) =
- count_obj_binder f c b
-
-let count_item f c = function
- | Some obj -> count_obj f c obj
- | None -> f c
+ | _, _, Y.Void -> assert false
let print_counters f c =
let terms =
let items = c.eabsts + c.eabbrs in
let locations = B.locations () in
L.warn (P.sprintf " Kernel representation summary (basic_ag)");
- 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 binder locations: %6u" locations);
+ 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);
+ L.warn (P.sprintf " Total binder locations: %7u" locations);
f ()
-let indexes = ref false
-
let res l id =
- if !indexes then P.sprintf "#%u" l else id
+ if !O.indexes then P.sprintf "#%u" l else id
let rec pp_term c frm = function
| B.Sort h ->
- let f = function
- | Some s -> F.fprintf frm "@[%s@]" s
- | None -> F.fprintf frm "@[*%u@]" h
- in
- H.get_sort f h
+ let err () = F.fprintf frm "@[*%u@]" h in
+ let f s = F.fprintf frm "@[%s@]" s in
+ H.string_of_sort err f h
| B.LRef i ->
let f = function
| Some (id, _) -> F.fprintf frm "@[%s@]" id
| None -> F.fprintf frm "@[#%u@]" i
in
- if !indexes then f None else B.get f c i
+ if !O.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) ->
F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
let f cc =
F.fprintf frm "@[[%s:%a].%a@]" (res l id) (pp_term c) w (pp_term cc) t
in
- B.push f c l id (B.Abst w)
+ B.push "output abst" f c l id (B.Abst w)
| B.Bind (l, id, B.Abbr v, t) ->
let f cc =
F.fprintf frm "@[[%s=%a].%a@]" (res l id) (pp_term c) v (pp_term cc) t
in
- B.push f c l id (B.Abbr v)
+ B.push "output abbr" f c l id (B.Abbr v)
| B.Bind (l, id, B.Void, t) ->
let f cc = F.fprintf frm "@[[%s].%a@]" (res l id) (pp_term cc) t in
- B.push f c l id B.Void
+ B.push "output void" f c l id B.Void
-let pp_context frm c =
+let pp_lenv frm c =
let pp_entry frm = function
| l, id, B.Abst w ->
F.fprintf frm "@,@[%s : %a@]" (res l id) (pp_term c) w
B.contents f c
let specs = {
- L.pp_term = pp_term; L.pp_context = pp_context
+ L.pp_term = pp_term; L.pp_lenv = pp_lenv
}