module P = Printf
module F = Format
module U = NUri
+module C = Cps
module L = Log
+module Y = Entity
module M = Meta
type counters = {
let count_par f c (_, w) = count_term f c w
-let count_entry f c = function
- | _, pars, u, w, None ->
+let count_xterm f c = function
+ | None -> f c
+ | Some v -> count_term f c v
+
+let count_entity f c = function
+ | _, u, Y.Abst (pars, w, xv) ->
let c = {c with eabsts = succ c.eabsts} in
let c = {c with pabsts = c.pabsts + List.length pars} in
let c = {c with uris = u :: c.uris; nodes = succ c.nodes + List.length pars} in
+ let f c = count_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
- | _, pars, _, w, Some (_, v) ->
+ | _, _, Y.Abbr (pars, w, xv) ->
let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
let c = {c with pabsts = c.pabsts + List.length pars} in
let c = {c with nodes = c.nodes + List.length pars} in
- let f c = count_term f c v in
+ let f c = count_xterm f c xv in
let f c = count_term f c w in
Cps.list_fold_left f count_par c pars
-let count_entity f c = function
- | Some e -> count_entry f c e
- | None -> f c
-
let print_counters f c =
let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
let pars = c.pabsts + c.pappls in
| true -> "Type"
| false -> "Prop"
-let string_of_transparent = function
- | true -> "="
- | false -> "~"
+let pp_transparent frm a =
+ let err () = F.fprintf frm "%s" "=" in
+ let f () = F.fprintf frm "%s" "~" in
+ Y.priv err f a
let pp_list pp opend sep closed frm l =
let rec aux frm = function
F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
let pp_par frm (id, w) =
- F.fprintf frm "%s:%a" id pp_term w
+ F.fprintf frm "%s:%a" id pp_term w
let pp_pars = pp_rev_list pp_par "[" "," "]"
-let pp_body frm = function
- | None -> ()
- | Some (trans, t) ->
- F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
+let pp_body a frm = function
+ | None -> ()
+ | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t
-let pp_entry frm (l, pars, uri, u, body) =
- F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
- l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
+let pp_entity frm = function
+ | a, uri, Y.Abst (pars, u, body)
+ | a, uri, Y.Abbr (pars, u, body) ->
+ F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
+ (Y.mark C.err C.start a) (U.string_of_uri uri)
+ pp_pars pars (pp_body a) body pp_term u
-let pp_entity f frm = function
- | Some entry -> pp_entry frm entry; f ()
- | None -> f ()
+let pp_entity f frm entity =
+ pp_entity frm entity; f ()