]> matita.cs.unibo.it Git - helm.git/blob - helm/software/lambda-delta/basic_rg/brgOutput.ml
some interfaces improved
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 module P = Printf
13 module F = Format
14 module C = Cps
15 module U = NUri
16 module L = Log
17 module Y = Entity
18 module X = Library
19 module H = Hierarchy
20 module O = Output
21 module B = Brg
22
23 (* nodes count **************************************************************)
24
25 type counters = {
26    eabsts: int;
27    eabbrs: int;
28    evoids: int;
29    tsorts: int;
30    tlrefs: int;
31    tgrefs: int;
32    tcasts: int;
33    tappls: int;
34    tabsts: int;
35    tabbrs: int;
36    tvoids: int;
37    uris  : B.uri list;
38    nodes : int;
39    xnodes: int
40 }
41
42 let initial_counters = {
43    eabsts = 0; eabbrs = 0; evoids = 0; 
44    tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
45    tabsts = 0; tabbrs = 0; tvoids = 0;
46    uris = []; nodes = 0; xnodes = 0
47 }
48
49 let rec count_term_binder f c e = function
50    | B.Abst w ->
51       let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
52       count_term f c e w
53    | B.Abbr v -> 
54       let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
55       count_term f c e v
56    | B.Void   ->
57       let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in   
58       f c
59
60 and count_term f c e = function
61    | B.Sort _         -> 
62       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
63    | B.LRef (_, i)    -> 
64       begin match B.get e i with
65          | _, _, _, B.Abst _
66          | _, _, _, B.Void   ->
67             f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
68          | _, _, _, B.Abbr _ ->
69             f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
70       end      
71    | B.GRef (_, u)    -> 
72       let c =    
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}
76       in
77       f {c with tgrefs = succ c.tgrefs}
78    | B.Cast (_, v, t) -> 
79       let c = {c with tcasts = succ c.tcasts} in
80       let f c = count_term f c e t in
81       count_term f c e v
82    | B.Appl (_, v, t) -> 
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
85       count_term f c e v
86    | B.Bind (a, b, t) -> 
87       let f c = count_term f c (B.push e B.empty a b) t in
88       count_term_binder f c e b
89
90 let count_entity f c = function
91    | _, u, Y.Abst w -> 
92       let c = {c with
93          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
94       } in
95       count_term f c B.empty w
96    | _, _, Y.Abbr v ->  
97       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
98       count_term f c B.empty v
99    | _, _, Y.Void   -> assert false
100
101 let print_counters f c =
102    let terms =
103       c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
104       c.tabbrs
105    in
106    let items = c.eabsts + c.eabbrs in
107    let nodes = c.nodes + c.xnodes in
108    L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
109    L.warn (P.sprintf "    Total entry items:        %7u" items);
110    L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
111    L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
112    L.warn (P.sprintf "    Total term items:         %7u" terms);
113    L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
114    L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
115    L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
116    L.warn (P.sprintf "      Explicit Cast items:    %7u" c.tcasts);
117    L.warn (P.sprintf "      Application items:      %7u" c.tappls);
118    L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
119    L.warn (P.sprintf "      Abbreviation items:     %7u" c.tabbrs);
120    L.warn (P.sprintf "    Global Int. Complexity:   %7u" c.nodes);
121    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" nodes);
122    f ()
123
124 (* supplementary annotation *************************************************)
125
126 let rec does_not_occur f n r = function
127    | B.Null              -> f true
128    | B.Cons (e, _, a, _) ->
129       let f n1 r1 =
130          if n1 = n && r1 = r then f false else does_not_occur f n r e
131       in
132       Y.name C.err f a 
133
134 let rename f e a =
135    let rec aux f e n r =
136       let f = function
137          | true  -> f n r
138          | false -> aux f e (n ^ "'") r
139       in
140       does_not_occur f n r e
141    in
142    let f n0 r0 =
143       let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in
144       aux f e n0 r0 
145    in
146    Y.name C.err f a
147
148 (* lenv/term pretty printing ************************************************)
149
150 let name err frm a =
151    let f n = function 
152       | true  -> F.fprintf frm "%s" n
153       | false -> F.fprintf frm "^%s" n
154    in      
155    Y.name err f a
156
157 let rec pp_term e frm = function
158    | B.Sort (_, h)           -> 
159       let err _ = F.fprintf frm "@[*%u@]" h in
160       let f s = F.fprintf frm "@[%s@]" s in
161       H.get_sort err f h 
162    | B.LRef (_, i)           -> 
163       let err _ = F.fprintf frm "@[#%u@]" i in
164       if !O.indexes then err () else      
165       let _, _, a, b = B.get e i in
166       F.fprintf frm "@[%a@]" (name err) a
167    | B.GRef (_, s)           ->
168       F.fprintf frm "@[$%s@]" (U.string_of_uri s)
169    | B.Cast (_, u, t)        ->
170       F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
171    | B.Appl (_, v, t)        ->
172       F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
173    | B.Bind (a, B.Abst w, t) ->
174       let f a =
175          let ee = B.push e B.empty a (B.abst w) in
176          F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t
177       in
178       rename f e a
179    | B.Bind (a, B.Abbr v, t) ->
180       let f a = 
181          let ee = B.push e B.empty a (B.abbr v) in
182          F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
183       in
184       rename f e a
185    | B.Bind (a, B.Void, t)   ->
186       let f a = 
187          let ee = B.push e B.empty a B.Void in
188          F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
189       in
190       rename f e a
191
192 let pp_lenv frm e =
193    let pp_entry f e c a b x = f x (*match b with
194       | B.Abst (a, w) -> 
195          let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
196          rename f x a
197       | B.Abbr (a, v) -> 
198          let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
199          rename f c a
200       | B.Void a      -> 
201          let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
202          rename f c a
203 *)   in
204    B.fold_right ignore pp_entry e B.empty
205
206 let specs = {
207    L.pp_term = pp_term; L.pp_lenv = pp_lenv
208 }
209
210 (* term xml printing ********************************************************)
211
212 let rec exp_term e t out tab = match t with
213    | B.Sort (a, l)    ->
214       let a =
215          let err _ = a in
216          let f s = Y.Name (s, true) :: a in
217          H.get_sort err f l
218       in
219       let attrs = [X.position l; X.name a] in
220       X.tag X.sort attrs out tab
221    | B.LRef (a, i)    ->
222       let a = 
223          let err _ = a in
224          let f n r = Y.Name (n, r) :: a in
225          let _, _, a, b = B.get e i in
226          Y.name err f a
227       in
228       let attrs = [X.position i; X.name a] in
229       X.tag X.lref attrs out tab
230    | B.GRef (a, n)    ->
231       let a = Y.Name (U.name_of_uri n, true) :: a in
232       let attrs = [X.uri n; X.name a] in
233       X.tag X.gref attrs out tab
234    | B.Cast (a, u, t) ->
235       let attrs = [] in
236       X.tag X.cast attrs ~contents:(exp_term e u) out tab;
237       exp_term e t out tab
238    | B.Appl (a, v, t) ->
239       let attrs = [] in
240       X.tag X.appl attrs ~contents:(exp_term e v) out tab;
241       exp_term e t out tab
242    | B.Bind (a, b, t)    ->
243       let a = rename C.start e a in
244       exp_bind e a b out tab; 
245       exp_term (B.push e B.empty a b) t out tab 
246
247 and exp_bind e a b out tab = match b with
248    | B.Abst w ->
249       let attrs = [X.name a; X.mark a] in
250       X.tag X.abst attrs ~contents:(exp_term e w) out tab
251    | B.Abbr v ->
252       let attrs = [X.name a; X.mark a] in
253       X.tag X.abbr attrs ~contents:(exp_term e v) out tab
254    | B.Void   ->
255       let attrs = [X.name a; X.mark a] in
256       X.tag X.void attrs out tab
257
258 let export_term = exp_term B.empty