blob: ee7170df48747e30a15b670e1f0dea1248c3fec0 (
plain)
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
66
67
68
69
70
71
72
73
74
75
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open Names
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 env =
begin
match engagement env with
| ImpredicativeSet -> str "Theory: Set is impredicative"
| PredicativeSet -> str "Theory: Set is predicative"
end
let pr_assumptions ass axs =
if axs = [] then
str ass ++ str ": <none>"
else
hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
let pr_axioms env =
let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Constant.to_string c :: acc else acc) env [] in
pr_assumptions "Axioms" csts
let pr_type_in_type env =
let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_universes then Constant.to_string c :: acc else acc) env [] in
let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_universes then MutInd.to_string c :: acc else acc) env csts in
pr_assumptions "Constants/Inductives relying on type-in-type" csts
let pr_unguarded env =
let csts = fold_constants (fun c cb acc -> if not cb.const_typing_flags.check_guarded then Constant.to_string c :: acc else acc) env [] in
let csts = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_guarded then MutInd.to_string c :: acc else acc) env csts in
pr_assumptions "Constants/Inductives relying on unsafe (co)fixpoints" csts
let pr_nonpositive env =
let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
pr_assumptions "Inductives whose positivity is assumed" inds
let print_context env =
if !output_context then begin
Feedback.msg_notice
(hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_nonpositive env ++ fnl()))
)
end
let stats env =
print_context env;
print_memory_stat ()
|
