1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Names
open Cic
open Declarations
open Environ

let memory_stat = ref false

let print_memory_stat () =
  if !memory_stat then begin
    Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
    Format.print_newline();
    Format.print_flush()
  end

let output_context = ref false

let pr_engagement impr_set =
  begin
    match impr_set with
    | ImpredicativeSet -> str "Theory: Set is impredicative"
    | PredicativeSet -> str "Theory: Set is predicative"
  end

let cst_filter f csts =
  Cmap_env.fold
    (fun c ce acc -> if f c ce then c::acc else acc)
    csts []

let is_ax _ cb = not (constant_has_body cb)

let pr_ax csts =
  let axs = cst_filter is_ax csts in
  if axs = [] then
    str "Axioms: <none>"
  else
    hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Indtypes.prcon axs)

let print_context env =
  if !output_context then begin
    let
      {env_globals=
        {env_constants=csts; env_inductives=inds;
         env_modules=mods; env_modtypes=mtys};
       env_stratification=
        {env_universes=univ; env_engagement=engt}} = env in
    Feedback.msg_notice
      (hov 0
      (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
      str"===============" ++ fnl() ++ fnl() ++
      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
      str "* " ++ hov 0 (pr_ax csts)));
  end

let stats () =
  print_context (Safe_typing.get_env());
  print_memory_stat ()