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