helm/software/lambda-delta/toplevel/metaOutput.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module M = Meta
  27
  28 type counters = {
  29    eabsts: int;
  30    eabbrs: int;
  31    pabsts: int;
  32    tsorts: int;
  33    tlrefs: int;
  34    tgrefs: int;
  35    pappls: int;
  36    tappls: int;
  37    tabsts: int;
  38 }
  39
  40 let initial_counters = {
  41    eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0;
  42    tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0
  43 }
  44
  45 let rec count_term f c = function
  46    | M.Sort _         ->
  47       f {c with tsorts = succ c.tsorts}
  48    | M.LRef _         ->
  49       f {c with tlrefs = succ c.tlrefs}
  50    | M.GRef (_, ts)   ->
  51       let c = {c with tgrefs = succ c.tgrefs} in
  52       let c = {c with pappls = c.pappls + List.length ts} in
  53       Cps.list_fold_left f count_term c ts
  54    | M.Appl (v, t)    ->
  55       let c = {c with tappls = succ c.tappls} in
  56       let f c = count_term f c t in
  57       count_term f c v
  58    | M.Abst (_, w, t) ->
  59       let c = {c with tabsts = succ c.tabsts} in
  60       let f c = count_term f c t in
  61       count_term f c w
  62
  63 let count_par f c (_, w) = count_term f c w
  64
  65 let count_item f c = function
  66    | pars, _, w, None        ->
  67       let c = {c with eabsts = succ c.eabsts} in
  68       let c = {c with pabsts = c.pabsts + List.length pars} in
  69       let f c = count_term f c w in
  70       Cps.list_fold_left f count_par c pars
  71    | pars, _, w, Some (_, v) ->
  72       let c = {c with eabbrs = succ c.eabbrs} in
  73       let c = {c with pabsts = c.pabsts + List.length pars} in
  74       let f c = count_term f c v in
  75       let f c = count_term f c w in
  76       Cps.list_fold_left f count_par c pars
  77
  78 let count f c b =
  79    Cps.list_fold_left f count_item c b
  80
  81 let print_counters f c =
  82    let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in
  83    let pars = c.pabsts + c.pappls in
  84    let items = c.eabsts + c.eabbrs in
  85    Printf.printf "  Intermediate representation summary\n";
  86    Printf.printf "    Total entry items:        %6u\n" items;
  87    Printf.printf "      Declaration items:      %6u\n" c.eabsts;
  88    Printf.printf "      Definition items:       %6u\n" c.eabbrs;
  89    Printf.printf "    Total parameter items:    %6u\n" pars;
  90    Printf.printf "      Application items:      %6u\n" c.pappls;
  91    Printf.printf "      Abstraction items:      %6u\n" c.pabsts;
  92    Printf.printf "    Total term items:         %6u\n" terms;
  93    Printf.printf "      Sort items:             %6u\n" c.tsorts;
  94    Printf.printf "      Local reference items:  %6u\n" c.tlrefs;
  95    Printf.printf "      Global reference items: %6u\n" c.tgrefs;
  96    Printf.printf "      Application items:      %6u\n" c.tappls;
  97    Printf.printf "      Abstraction items:      %6u\n" c.tabsts;
  98    flush stdout; f ()
  99
 100 let string_of_qid (id, path) =
 101    let path = String.concat "/" path in
 102    Filename.concat path id
 103