helm/software/lambda-delta/basic_rg/brgOutput.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 C = Cps
  15 module U = NUri
  16 module L = Log
  17 module Y = Entity
  18 module X = Library
  19 module H = Hierarchy
  20 module O = Output
  21 module B = Brg
  22
  23 (* nodes count **************************************************************)
  24
  25 type counters = {
  26    eabsts: int;
  27    eabbrs: int;
  28    evoids: int;
  29    tsorts: int;
  30    tlrefs: int;
  31    tgrefs: int;
  32    tcasts: int;
  33    tappls: int;
  34    tabsts: int;
  35    tabbrs: int;
  36    tvoids: int;
  37    uris  : B.uri list;
  38    nodes : int;
  39    xnodes: int
  40 }
  41
  42 let initial_counters = {
  43    eabsts = 0; eabbrs = 0; evoids = 0;
  44    tsorts = 0; tlrefs = 0; tgrefs = 0; tcasts = 0; tappls = 0;
  45    tabsts = 0; tabbrs = 0; tvoids = 0;
  46    uris = []; nodes = 0; xnodes = 0
  47 }
  48
  49 let rec count_term_binder f c e = function
  50    | B.Abst w ->
  51       let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
  52       count_term f c e w
  53    | B.Abbr v ->
  54       let c = {c with tabbrs = succ c.tabbrs; xnodes = succ c.xnodes} in
  55       count_term f c e v
  56    | B.Void   ->
  57       let c = {c with tvoids = succ c.tvoids; xnodes = succ c.xnodes} in
  58       f c
  59
  60 and count_term f c e = function
  61    | B.Sort _         ->
  62       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
  63    | B.LRef (_, i)    ->
  64       begin match B.get e i with
  65          | _, _, _, B.Abst _
  66          | _, _, _, B.Void   ->
  67             f {c with tlrefs = succ c.tlrefs; nodes = succ c.nodes}
  68          | _, _, _, B.Abbr _ ->
  69             f {c with tlrefs = succ c.tlrefs; xnodes = succ c.xnodes}
  70       end
  71    | B.GRef (_, u)    ->
  72       let c =
  73          if Cps.list_mem ~eq:U.eq u c.uris
  74          then {c with nodes = succ c.nodes}
  75          else {c with xnodes = succ c.xnodes}
  76       in
  77       f {c with tgrefs = succ c.tgrefs}
  78    | B.Cast (_, v, t) ->
  79       let c = {c with tcasts = succ c.tcasts} in
  80       let f c = count_term f c e t in
  81       count_term f c e v
  82    | B.Appl (_, v, t) ->
  83       let c = {c with tappls = succ c.tappls; nodes = succ c.nodes} in
  84       let f c = count_term f c e t in
  85       count_term f c e v
  86    | B.Bind (a, b, t) ->
  87       let f c = count_term f c (B.push e B.empty a b) t in
  88       count_term_binder f c e b
  89
  90 let count_entity f c = function
  91    | _, u, Y.Abst w ->
  92       let c = {c with
  93          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
  94       } in
  95       count_term f c B.empty w
  96    | _, _, Y.Abbr v ->
  97       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
  98       count_term f c B.empty v
  99    | _, _, Y.Void   -> assert false
 100
 101 let print_counters f c =
 102    let terms =
 103       c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts +
 104       c.tabbrs
 105    in
 106    let items = c.eabsts + c.eabbrs in
 107    let nodes = c.nodes + c.xnodes in
 108    L.warn (P.sprintf "  Kernel representation summary (basic_rg)");
 109    L.warn (P.sprintf "    Total entry items:        %7u" items);
 110    L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
 111    L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
 112    L.warn (P.sprintf "    Total term items:         %7u" terms);
 113    L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
 114    L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
 115    L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
 116    L.warn (P.sprintf "      Explicit Cast items:    %7u" c.tcasts);
 117    L.warn (P.sprintf "      Application items:      %7u" c.tappls);
 118    L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
 119    L.warn (P.sprintf "      Abbreviation items:     %7u" c.tabbrs);
 120    L.warn (P.sprintf "    Global Int. Complexity:   %7u" c.nodes);
 121    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" nodes);
 122    f ()
 123
 124 (* supplementary annotation *************************************************)
 125
 126 let rec does_not_occur f n r = function
 127    | B.Null              -> f true
 128    | B.Cons (e, _, a, _) ->
 129       let f n1 r1 =
 130          if n1 = n && r1 = r then f false else does_not_occur f n r e
 131       in
 132       Y.name C.err f a
 133
 134 let rename f e a =
 135    let rec aux f e n r =
 136       let f = function
 137          | true  -> f n r
 138          | false -> aux f e (n ^ "'") r
 139       in
 140       does_not_occur f n r e
 141    in
 142    let f n0 r0 =
 143       let f n r = if n = n0 && r = r0 then f a else f (Y.Name (n, r) :: a) in
 144       aux f e n0 r0
 145    in
 146    Y.name C.err f a
 147
 148 (* lenv/term pretty printing ************************************************)
 149
 150 let name err frm a =
 151    let f n = function
 152       | true  -> F.fprintf frm "%s" n
 153       | false -> F.fprintf frm "^%s" n
 154    in
 155    Y.name err f a
 156
 157 let rec pp_term e frm = function
 158    | B.Sort (_, h)           ->
 159       let err _ = F.fprintf frm "@[*%u@]" h in
 160       let f s = F.fprintf frm "@[%s@]" s in
 161       H.get_sort err f h
 162    | B.LRef (_, i)           ->
 163       let err _ = F.fprintf frm "@[#%u@]" i in
 164       if !O.indexes then err () else
 165       let _, _, a, b = B.get e i in
 166       F.fprintf frm "@[%a@]" (name err) a
 167    | B.GRef (_, s)           ->
 168       F.fprintf frm "@[$%s@]" (U.string_of_uri s)
 169    | B.Cast (_, u, t)        ->
 170       F.fprintf frm "@[{%a}.%a@]" (pp_term e) u (pp_term e) t
 171    | B.Appl (_, v, t)        ->
 172       F.fprintf frm "@[(%a).%a@]" (pp_term e) v (pp_term e) t
 173    | B.Bind (a, B.Abst w, t) ->
 174       let f a =
 175          let ee = B.push e B.empty a (B.abst w) in
 176          F.fprintf frm "@[[%a:%a].%a@]" (name C.err) a (pp_term e) w (pp_term ee) t
 177       in
 178       rename f e a
 179    | B.Bind (a, B.Abbr v, t) ->
 180       let f a =
 181          let ee = B.push e B.empty a (B.abbr v) in
 182          F.fprintf frm "@[[%a=%a].%a@]" (name C.err) a (pp_term e) v (pp_term ee) t
 183       in
 184       rename f e a
 185    | B.Bind (a, B.Void, t)   ->
 186       let f a =
 187          let ee = B.push e B.empty a B.Void in
 188          F.fprintf frm "@[[%a].%a@]" (name C.err) a (pp_term ee) t
 189       in
 190       rename f e a
 191
 192 let pp_lenv frm e =
 193    let pp_entry f e c a b x = f x (*match b with
 194       | B.Abst (a, w) ->
 195          let f a = F.fprintf frm "@,@[%a : %a@]" (name C.err) a (pp_term e) w; f a in
 196          rename f x a
 197       | B.Abbr (a, v) ->
 198          let f a = F.fprintf frm "@,@[%a = %a@]" (name C.err) a (pp_term e) v; f a in
 199          rename f c a
 200       | B.Void a      ->
 201          let f a = F.fprintf frm "@,%a" (name C.err) a; f a in
 202          rename f c a
 203 *)   in
 204    B.fold_right ignore pp_entry e B.empty
 205
 206 let specs = {
 207    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 208 }
 209
 210 (* term xml printing ********************************************************)
 211
 212 let rec exp_term e t out tab = match t with
 213    | B.Sort (a, l)    ->
 214       let a =
 215          let err _ = a in
 216          let f s = Y.Name (s, true) :: a in
 217          H.get_sort err f l
 218       in
 219       let attrs = [X.position l; X.name a] in
 220       X.tag X.sort attrs out tab
 221    | B.LRef (a, i)    ->
 222       let a =
 223          let err _ = a in
 224          let f n r = Y.Name (n, r) :: a in
 225          let _, _, a, b = B.get e i in
 226          Y.name err f a
 227       in
 228       let attrs = [X.position i; X.name a] in
 229       X.tag X.lref attrs out tab
 230    | B.GRef (a, n)    ->
 231       let a = Y.Name (U.name_of_uri n, true) :: a in
 232       let attrs = [X.uri n; X.name a] in
 233       X.tag X.gref attrs out tab
 234    | B.Cast (a, u, t) ->
 235       let attrs = [] in
 236       X.tag X.cast attrs ~contents:(exp_term e u) out tab;
 237       exp_term e t out tab
 238    | B.Appl (a, v, t) ->
 239       let attrs = [] in
 240       X.tag X.appl attrs ~contents:(exp_term e v) out tab;
 241       exp_term e t out tab
 242    | B.Bind (a, b, t)    ->
 243       let a = rename C.start e a in
 244       exp_bind e a b out tab;
 245       exp_term (B.push e B.empty a b) t out tab
 246
 247 and exp_bind e a b out tab = match b with
 248    | B.Abst w ->
 249       let attrs = [X.name a; X.mark a] in
 250       X.tag X.abst attrs ~contents:(exp_term e w) out tab
 251    | B.Abbr v ->
 252       let attrs = [X.name a; X.mark a] in
 253       X.tag X.abbr attrs ~contents:(exp_term e v) out tab
 254    | B.Void   ->
 255       let attrs = [X.name a; X.mark a] in
 256       X.tag X.void attrs out tab
 257
 258 let export_term = exp_term B.empty