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