helm/software/lambda-delta/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 P = Printf
  13 module L = Log
  14 module A = Aut
  15
  16 type counters = {
  17    sections: int;
  18    contexts: int;
  19    blocks:   int;
  20    decls:    int;
  21    defs:     int;
  22    sorts:    int;
  23    grefs:    int;
  24    appls:    int;
  25    absts:    int;
  26    pars:     int
  27 }
  28
  29 let initial_counters = {
  30    sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0;
  31    sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0
  32 }
  33
  34 let rec count_term f c = function
  35    | A.Sort _         ->
  36       f {c with sorts = succ c.sorts}
  37    | A.GRef (_, ts)   ->
  38       let c = {c with grefs = succ c.grefs} in
  39       let c = {c with pars = c.pars + List.length ts} in
  40       Cps.list_fold_left f count_term c ts
  41    | A.Appl (v, t)    ->
  42       let c = {c with appls = succ c.appls} in
  43       let f c = count_term f c t in
  44       count_term f c v
  45    | A.Abst (_, w, t) ->
  46       let c = {c with absts = succ c.absts} in
  47       let f c = count_term f c t in
  48       count_term f c w
  49
  50 let count_item f c = function
  51    | A.Section _        ->
  52       f {c with sections = succ c.sections}
  53    | A.Context _        ->
  54       f {c with contexts = succ c.contexts}
  55    | A.Block (_, w)     ->
  56       let c = {c with blocks = succ c.blocks} in
  57       count_term f c w
  58    | A.Decl (_, w)      ->
  59       let c = {c with decls = succ c.decls} in
  60       count_term f c w
  61    | A.Def (_, w, _, t) ->
  62       let c = {c with defs = succ c.defs} in
  63       let f c = count_term f c t in
  64       count_term f c w
  65
  66 let print_counters f c =
  67    let terms = c.sorts + c.grefs + c.appls + c.absts in
  68    let items = c.sections + c.contexts + c.blocks + c.decls + c.defs in
  69    L.warn (P.sprintf "  Automath representation summary");
  70    L.warn (P.sprintf "    Total book items:         %7u" items);
  71    L.warn (P.sprintf "      Section items:          %7u" c.sections);
  72    L.warn (P.sprintf "      Context items:          %7u" c.contexts);
  73    L.warn (P.sprintf "      Block items:            %7u" c.blocks);
  74    L.warn (P.sprintf "      Declaration items:      %7u" c.decls);
  75    L.warn (P.sprintf "      Definition items:       %7u" c.defs);
  76    L.warn (P.sprintf "    Total Parameter items:    %7u" c.pars);
  77    L.warn (P.sprintf "      Application items:      %7u" c.pars);
  78    L.warn (P.sprintf "    Total term items:         %7u" terms);
  79    L.warn (P.sprintf "      Sort items:             %7u" c.sorts);
  80    L.warn (P.sprintf "      Reference items:        %7u" c.grefs);
  81    L.warn (P.sprintf "      Application items:      %7u" c.appls);
  82    L.warn (P.sprintf "      Abstraction items:      %7u" c.absts);
  83    f ()