]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/automath/autOutput.ml
update in basic_2
[helm.git] / helm / software / helena / src / automath / autOutput.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 KP = Printf
13
14 module C  = Cps
15 module L  = Log
16 module A  = Aut
17 module AA = AutProcess
18
19 type counters = {
20    sections: int;
21    contexts: int;
22    blocks:   int;
23    decls:    int;
24    defs:     int;
25    sorts:    int;
26    grefs:    int;
27    appls:    int;
28    absts:    int;
29    pars:     int;
30    xnodes:   int
31 }
32
33 let level = 2
34
35 let initial_counters = {
36    sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0;
37    sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0
38 }
39
40 IFDEF SUMMARY THEN
41
42 let rec count_term f c = function
43    | A.Sort _         -> 
44       f {c with sorts = succ c.sorts; xnodes = succ c.xnodes}
45    | A.GRef (_, ts)   -> 
46       let c = {c with grefs = succ c.grefs} in
47       let c = {c with pars = c.pars + List.length ts} in
48       let c = {c with xnodes = succ c.xnodes + List.length ts} in
49       C.list_fold_left f count_term c ts
50    | A.Appl (v, t)    -> 
51       let c = {c with appls = succ c.appls; xnodes = succ c.xnodes} in
52       let f c = count_term f c t in
53       count_term f c v
54    | A.Abst (_, w, t) -> 
55       let c = {c with absts = succ c.absts; xnodes = succ c.xnodes} in
56       let f c = count_term f c t in
57       count_term f c w
58
59 let count_command f c = function
60    | A.Section _        ->
61       f {c with sections = succ c.sections}
62    | A.Context _        ->
63       f {c with contexts = succ c.contexts}
64    | A.Block (_, w)     -> 
65       let c = {c with blocks = succ c.blocks; xnodes = succ c.xnodes} in
66       count_term f c w
67    | A.Decl (_, w)      -> 
68       let c = {c with decls = succ c.decls; xnodes = succ c.xnodes} in
69       count_term f c w
70    | A.Def (_, w, _, t) -> 
71       let c = {c with defs = succ c.defs; xnodes = succ c.xnodes} in
72       let f c = count_term f c t in
73       count_term f c w
74
75 let print_counters f c =
76    let terms = c.sorts + c.grefs + c.appls + c.absts in
77    let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in
78    L.warn level (KP.sprintf "Automath representation summary");
79    L.warn level (KP.sprintf "  Total book entities:      %7u" entities);
80    L.warn level (KP.sprintf "    Section entities:       %7u" c.sections);
81    L.warn level (KP.sprintf "    Context entities:       %7u" c.contexts);
82    L.warn level (KP.sprintf "    Block entities:         %7u" c.blocks);
83    L.warn level (KP.sprintf "    Declaration entities:   %7u" c.decls);
84    L.warn level (KP.sprintf "    Definition entities:    %7u" c.defs);
85    L.warn level (KP.sprintf "  Total Parameter items:    %7u" c.pars);
86    L.warn level (KP.sprintf "    Application items:      %7u" c.pars);
87    L.warn level (KP.sprintf "  Total term items:         %7u" terms);
88    L.warn level (KP.sprintf "    Sort items:             %7u" c.sorts);
89    L.warn level (KP.sprintf "    Reference items:        %7u" c.grefs);
90    L.warn level (KP.sprintf "    Application items:      %7u" c.appls);
91    L.warn level (KP.sprintf "    Abstraction items:      %7u" c.absts);
92    L.warn level (KP.sprintf "  Global Int. Complexity:   unknown");
93    L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" c.xnodes);
94    f ()
95
96 IFDEF PREPROCESS THEN
97
98 let print_process_counters f c =
99    let f iao iar iac iag =
100       L.warn level (KP.sprintf "Automath process summary");
101       L.warn level (KP.sprintf "  Implicit after opening:   %7u" iao);
102       L.warn level (KP.sprintf "  Implicit after reopening: %7u" iar);
103       L.warn level (KP.sprintf "  Implicit after closing:   %7u" iac);
104       L.warn level (KP.sprintf "  Implicit after global:    %7u" iag);
105       f ()
106    in
107    AA.get_counters f c
108
109 END
110
111 END