2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
21 (* nodes count **************************************************************)
40 let initial_counters = {
41 eabsts = 0; eabbrs = 0; evoids = 0;
42 tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
43 tabsts = 0; tabbrs = 0; tvoids = 0;
44 uris = []; nodes = 0; xnodes = 0
47 let rec count_term_binder f c e = function
49 let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
52 let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
55 let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
58 and count_term f c e = function
60 f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
62 let err _ = f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes} in
66 f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
68 f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
73 if Cps.list_mem ~eq:U.eq u c.uris
74 then {c with nodes = succ c.nodes}
75 else {c with xnodes = succ c.xnodes}
77 f {c with tgrefs = succ c.tgrefs}
79 let c = {c with tcasts = succ c.tcasts} in
80 let f c = count_term f c e t in
83 let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
84 let f c = count_term f c e t in
87 let f c e = count_term f c e t in
88 let f c = B.push (f c) e b in
89 count_term_binder f c e b
91 let count_entry f c = function
92 | (_, u, B.Abst (_, w)) ->
94 eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
96 count_term f c B.empty_lenv w
97 | (_, _, B.Abbr (_, v)) ->
98 let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
99 count_term f c B.empty_lenv v
100 | (_, u, B.Void _) ->
102 evoids = succ c.evoids; nodes = succ c.nodes; uris = u :: c.uris
106 let count_entity f c = function
107 | Some entry -> count_entry f c entry
110 let print_counters f c =
112 c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
115 let items = c.eabsts + c.eabbrs in
116 let nodes = c.nodes + c.xnodes in
117 L.warn (P.sprintf " Kernel representation summary (basic_rg)");
118 L.warn (P.sprintf " Total entry items: %7u" items);
119 L.warn (P.sprintf " Declaration items: %7u" c.eabsts);
120 L.warn (P.sprintf " Definition items: %7u" c.eabbrs);
121 L.warn (P.sprintf " Total term items: %7u" terms);
122 L.warn (P.sprintf " Sort items: %7u" c.tsorts);
123 L.warn (P.sprintf " Local reference items: %7u" c.tlrefs);
124 L.warn (P.sprintf " Global reference items: %7u" c.tgrefs);
125 L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts);
126 L.warn (P.sprintf " Application items: %7u" c.tappls);
127 L.warn (P.sprintf " Abstraction items: %7u" c.tabsts);
128 L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs);
129 L.warn (P.sprintf " Global Int. Complexity: %7u" c.nodes);
130 L.warn (P.sprintf " + Abbreviation nodes: %7u" nodes);
133 (* supplementary annotation *************************************************)
135 let attrs_of_binder f = function
140 let rec does_not_occur f n r = function
142 | B.Cons (c, _, b) ->
144 if n1 = n && r1 = r then f false else does_not_occur f n r c
146 attrs_of_binder (B.name C.err f) b
149 let rec aux f c n r =
152 | false -> aux f c (n ^ "'") r
154 does_not_occur f n r c
157 let f n r = if n = n0 && r = r0 then f a else f (B.Name (r, n) :: a) in
162 let rename_bind f c = function
163 | B.Abst (a, w) -> let f a = f (B.abst a w) in rename f c a
164 | B.Abbr (a, v) -> let f a = f (B.abbr a v) in rename f c a
165 | B.Void a -> let f a = f (B.Void a) in rename f c a
167 (* lenv/term pretty printing ************************************************)
171 | true -> F.fprintf frm "%s" n
172 | false -> F.fprintf frm "^%s" n
176 let rec pp_term c frm = function
178 let err _ = F.fprintf frm "@[*%u@]" h in
179 let f s = F.fprintf frm "@[%s@]" s in
182 let err _ = F.fprintf frm "@[#%u@]" i in
186 | B.Void a -> F.fprintf frm "@[%a@]" id a
188 if !O.indexes then err () else B.get err f c i
190 F.fprintf frm "@[$%s@]" (U.string_of_uri s)
191 | B.Cast (_, u, t) ->
192 F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
193 | B.Appl (_, v, t) ->
194 F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
195 | B.Bind (B.Abst (a, w), t) ->
197 F.fprintf frm "@[[%a:%a].%a@]" id a (pp_term c) w (pp_term cc) t
199 let f a = B.push (f a) c (B.abst a w) in
201 | B.Bind (B.Abbr (a, v), t) ->
203 F.fprintf frm "@[[%a=%a].%a@]" id a (pp_term c) v (pp_term cc) t
205 let f a = B.push (f a) c (B.abbr a v) in
207 | B.Bind (B.Void a, t) ->
208 let f a cc = F.fprintf frm "@[[%a].%a@]" id a (pp_term cc) t in
209 let f a = B.push (f a) c (B.Void a) in
213 let pp_entry f c = function
215 let f a = F.fprintf frm "@,@[%a : %a@]" id a (pp_term c) w; f () in
218 let f a = F.fprintf frm "@,@[%a = %a@]" id a (pp_term c) v; f () in
221 let f a = F.fprintf frm "@,%a" id a; f () in
224 B.rev_iter C.start pp_entry c
227 L.pp_term = pp_term; L.pp_lenv = pp_lenv
230 (* term xml printing ********************************************************)
234 | true -> F.fprintf frm " name=%S" s
235 | false -> F.fprintf frm " name=%S" ("^" ^ s)
239 let rec exp_term c frm = function
243 let f s = B.Name (true, s) :: a in
246 F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) id a
250 let f n r = B.Name (r, n) :: a in
251 let f _ b = attrs_of_binder (B.name err f) b in
254 F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) id a
256 let a = B.Name (true, U.name_of_uri u) :: a in
257 F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) id a
258 | B.Cast (a, w, t) ->
259 F.fprintf frm "<Cast%a>%a</Cast>@,%a" id a (exp_boxed c) w (exp_term c) t
260 | B.Appl (a, v, t) ->
261 F.fprintf frm "<Appl%a>%a</Appl>@,%a" id a (exp_boxed c) v (exp_term c) t
263 let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in
264 let f b = B.push (f b) c b in
267 and exp_boxed c frm t =
268 F.fprintf frm "@,@[<v3> %a@]@," (exp_term c) t
270 and exp_bind c frm = function
272 F.fprintf frm "<Abst%a>%a</Abst>" id a (exp_boxed c) w
274 F.fprintf frm "<Abbr%a/>%a</Abbr>" id a (exp_boxed c) v
276 F.fprintf frm "<Void%a/>" id a
278 let exp_entry c frm = function
279 | _, u, B.Abst (a, w) ->
280 let str = U.string_of_uri u in
281 let a = B.Name (true, U.name_of_uri u) :: a in
282 F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str id a (exp_boxed c) w
283 | _, u, B.Abbr (a, v) ->
284 let str = U.string_of_uri u in
285 let a = B.Name (true, U.name_of_uri u) :: a in
286 F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str id a (exp_boxed c) v
288 let str = U.string_of_uri u in
289 let a = B.Name (true, U.name_of_uri u) :: a in
290 F.fprintf frm "<VOID uri=%S%a/>" str id a
292 let export_entry frm entry =
293 F.fprintf frm "@,@[<v3> %a@]@," (exp_entry B.empty_lenv) entry