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
76
77
78
79
80
81
82
|
(************************************************************************)
(* * 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_impredicative_set env =
if is_impredicative_set env then str "Theory: Set is impredicative"
else str "Theory: Set is predicative"
let pr_rewrite_rules env =
if rewrite_rules_allowed env then str "Theory: Rewrite rules are allowed (consistency, subject reduction, confluence and normalization might be broken)"
else str "Theory: Rewrite rules are not allowed"
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 opac =
let add c cb acc =
if Declareops.constant_has_body cb then acc else
match Cmap.find_opt c opac with
| None -> Cset.add c acc
| Some s -> Cset.union s acc in
let csts = fold_constants add env Cset.empty in
let csts = Cset.fold (fun c acc -> Constant.to_string c :: acc) csts [] 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 opac =
if !output_context then begin
Feedback.msg_notice
(hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_impredicative_set env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_rewrite_rules env ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_axioms env opac ++ 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 opac =
print_context env opac;
print_memory_stat ()
|
