helm/software/lambda-delta/toplevel/metaOutput.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 U = NUri
  15 module L = Log
  16 module M = Meta
  17
  18 type counters = {
  19    eabsts: int;
  20    eabbrs: int;
  21    pabsts: int;
  22    tsorts: int;
  23    tlrefs: int;
  24    tgrefs: int;
  25    pappls: int;
  26    tappls: int;
  27    tabsts: int;
  28 }
  29
  30 let initial_counters = {
  31    eabsts = 0; eabbrs = 0; pabsts = 0; pappls = 0;
  32    tsorts = 0; tlrefs = 0; tgrefs = 0; tappls = 0; tabsts = 0
  33 }
  34
  35 let rec count_term f c = function
  36    | M.Sort _          ->
  37       f {c with tsorts = succ c.tsorts}
  38    | M.LRef _          ->
  39       f {c with tlrefs = succ c.tlrefs}
  40    | M.GRef (_, _, ts) ->
  41       let c = {c with tgrefs = succ c.tgrefs} in
  42       let c = {c with pappls = c.pappls + List.length ts} in
  43       Cps.list_fold_left f count_term c ts
  44    | M.Appl (v, t)     ->
  45       let c = {c with tappls = succ c.tappls} in
  46       let f c = count_term f c t in
  47       count_term f c v
  48    | M.Abst (_, w, t)  ->
  49       let c = {c with tabsts = succ c.tabsts} in
  50       let f c = count_term f c t in
  51       count_term f c w
  52
  53 let count_par f c (_, w) = count_term f c w
  54
  55 let count_entry f c = function
  56    | _, pars, _, w, None        ->
  57       let c = {c with eabsts = succ c.eabsts} in
  58       let c = {c with pabsts = c.pabsts + List.length pars} in
  59       let f c = count_term f c w in
  60       Cps.list_fold_left f count_par c pars
  61    | _, pars, _, w, Some (_, v) ->
  62       let c = {c with eabbrs = succ c.eabbrs} in
  63       let c = {c with pabsts = c.pabsts + List.length pars} in
  64       let f c = count_term f c v in
  65       let f c = count_term f c w in
  66       Cps.list_fold_left f count_par c pars
  67
  68 let count_item f c = function
  69    | Some e -> count_entry f c e
  70    | None   -> f c
  71
  72 let print_counters f c =
  73    let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in
  74    let pars = c.pabsts + c.pappls in
  75    let items = c.eabsts + c.eabbrs in
  76    L.warn (P.sprintf "  Intermediate representation summary");
  77    L.warn (P.sprintf "    Total entry items:        %7u" items);
  78    L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
  79    L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
  80    L.warn (P.sprintf "    Total parameter items:    %7u" pars);
  81    L.warn (P.sprintf "      Application items:      %7u" c.pappls);
  82    L.warn (P.sprintf "      Abstraction items:      %7u" c.pabsts);
  83    L.warn (P.sprintf "    Total term items:         %7u" terms);
  84    L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
  85    L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
  86    L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
  87    L.warn (P.sprintf "      Application items:      %7u" c.tappls);
  88    L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
  89    f ()
  90
  91 let string_of_sort = function
  92    | true -> "Type"
  93    | false -> "Prop"
  94
  95 let string_of_transparent = function
  96    | true  -> "="
  97    | false -> "~"
  98
  99 let pp_list pp opend sep closed frm l =
 100    let rec aux frm = function
 101       | []       -> ()
 102       | [hd]     -> pp frm hd
 103       | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl
 104    in
 105    if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
 106
 107 let pp_rev_list pp opend sep closed frm l =
 108    pp_list pp opend sep closed frm (List.rev l)
 109
 110 let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
 111
 112 and pp_term frm = function
 113    | M.Sort s            ->
 114       F.fprintf frm "@[*%s@]" (string_of_sort s)
 115    | M.LRef (l, i)       ->
 116       F.fprintf frm "@[%u@@#%u@]" l i
 117    | M.GRef (l, uri, ts) ->
 118       F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts
 119    | M.Appl (v, t)       ->
 120       F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
 121    | M.Abst (id, w, t)   ->
 122       F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
 123
 124 let pp_par frm (id, w) =
 125     F.fprintf frm "%s:%a" id pp_term w
 126
 127 let pp_pars = pp_rev_list pp_par "[" "," "]"
 128
 129 let pp_body frm = function
 130    | None            -> ()
 131    | Some (trans, t) ->
 132       F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t
 133
 134 let pp_entry frm (l, pars, uri, u, body) =
 135    F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
 136       l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u
 137
 138 let pp_item f frm = function
 139    | Some entry -> pp_entry frm entry; f ()
 140    | None       -> f ()