helm/software/helena/src/basic_ag/bagOutput.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 G  = Options
  17 module E  = Entity
  18 module J  = Marks
  19 module H  = Hierarchy
  20 module XD = XmlCrg
  21 module Z  = Bag
  22 module ZD = BagCrg
  23
  24 type counters = {
  25    eabsts: int;
  26    eabbrs: int;
  27    tsorts: int;
  28    tlrefs: int;
  29    tgrefs: int;
  30    tcasts: int;
  31    tappls: int;
  32    tabsts: int;
  33    tabbrs: int
  34 }
  35
  36 let initial_counters = {
  37    eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0;
  38    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
  39 }
  40
  41 let rec count_term_binder f c = function
  42    | Z.Abst w ->
  43       let c = {c with tabsts = succ c.tabsts} in
  44       count_term f c w
  45    | Z.Abbr v ->
  46       let c = {c with tabbrs = succ c.tabbrs} in
  47       count_term f c v
  48    | Z.Void   -> f c
  49
  50 and count_term f c = function
  51    | Z.Sort _            ->
  52       f {c with tsorts = succ c.tsorts}
  53    | Z.LRef _            ->
  54       f {c with tlrefs = succ c.tlrefs}
  55    | Z.GRef _            ->
  56       f {c with tgrefs = succ c.tgrefs}
  57    | Z.Cast (v, t)       ->
  58       let c = {c with tcasts = succ c.tcasts} in
  59       let f c = count_term f c t in
  60       count_term f c v
  61    | Z.Appl (v, t)       ->
  62       let c = {c with tappls = succ c.tappls} in
  63       let f c = count_term f c t in
  64       count_term f c v
  65    | Z.Bind (_, _, b, t) ->
  66       let f c = count_term_binder f c b in
  67       count_term f c t
  68
  69 let count_entity f c = function
  70    | _, _, E.Abst (_, w) ->
  71       let c = {c with eabsts = succ c.eabsts} in
  72       count_term f c w
  73    | _, _, E.Abbr v      ->
  74       let c = {c with eabbrs = succ c.eabbrs} in
  75       count_term f c v
  76    | _, _, E.Void        -> assert false
  77
  78 let print_counters f c =
  79    let terms =
  80       c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
  81       c.tabbrs
  82    in
  83    let items = c.eabsts + c.eabbrs in
  84    let locations = J.locations () in
  85    L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
  86    L.warn (P.sprintf "    Total entry items:        %7u" items);
  87    L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
  88    L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
  89    L.warn (P.sprintf "    Total term items:         %7u" terms);
  90    L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
  91    L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
  92    L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
  93    L.warn (P.sprintf "      Explicit Cast items:    %7u" c.tcasts);
  94    L.warn (P.sprintf "      Application items:      %7u" c.tappls);
  95    L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
  96    L.warn (P.sprintf "      Abbreviation items:     %7u" c.tabbrs);
  97    L.warn (P.sprintf "    Total binder locations:   %7u" locations);
  98    f ()
  99
 100 let name err frm a =
 101    let f n = function
 102       | true  -> F.fprintf frm "%s" n
 103       | false -> F.fprintf frm "-%s" n
 104    in
 105    E.name err f a
 106
 107 let res a l frm =
 108    let err () = F.fprintf frm "@[#%u@]" l in
 109    if !G.indexes then err () else name err frm a
 110
 111 let rec pp_term c frm = function
 112    | Z.Sort h                 ->
 113       let err () = F.fprintf frm "@[*%u@]" h in
 114       let f s = F.fprintf frm "@[%s@]" s in
 115       H.string_of_sort err f h
 116    | Z.LRef i                 ->
 117       let err () = F.fprintf frm "@[#%u@]" i in
 118       let f a _ = name err frm a in
 119       if !G.indexes then err () else Z.get err f c i
 120    | Z.GRef s                    -> F.fprintf frm "@[$%s@]" (U.string_of_uri s)
 121    | Z.Cast (u, t)               ->
 122       F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t
 123    | Z.Appl (v, t)               ->
 124       F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t
 125    | Z.Bind (a, l, Z.Abst w, t) ->
 126       let f cc =
 127          F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t
 128       in
 129       Z.push "output abst" f c a l (Z.Abst w)
 130    | Z.Bind (a, l, Z.Abbr v, t) ->
 131       let f cc =
 132          F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t
 133       in
 134       Z.push "output abbr" f c a l (Z.Abbr v)
 135    | Z.Bind (a, l, Z.Void, t)   ->
 136       let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in
 137       Z.push "output void" f c a l Z.Void
 138
 139 let pp_lenv frm c =
 140    let pp_entry frm = function
 141       | a, l, Z.Abst w ->
 142          F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w
 143       | a, l, Z.Abbr v ->
 144          F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v
 145       | a, l, Z.Void   ->
 146          F.fprintf frm "@,%t" (res a l)
 147    in
 148    let iter map frm l = List.iter (map frm) l in
 149    let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in
 150    Z.contents f c
 151
 152 let specs = {
 153    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 154 }
 155
 156 (* term xml printing ********************************************************)
 157
 158 let export_term =
 159    ZD.crg_of_bag XD.export_term