1signature Sanity =
2sig
3
4 type term = Term.term
5 type thm = Thm.thm
6 type theory = Hol_pp.theory
7 type tactic = Abbrev.tactic
8
9 val accepted_axioms  : string list ref;
10 val accepted_oracles : string list ref;
11
12 (* Traces
13
14    "Santity Check Strict":
15    ------------------------
16    Turn warnings or exception on or off.
17    Default: true (through exception)
18
19    "Santity Check Verbose":
20    ------------------------
21    Turn verbose reporting on or off.
22    Default: true
23
24
25    "Santity Check Free Vars":
26    --------------------------
27    Turn checking for free top-level variables to different levels:
28      0 : allow no free vars
29      1 : if theorem starts with an allquantor, then allow no free vars
30      2 : no check
31    Default: 1
32
33
34    "Santity Check Var-Const Clash":
35    --------------------------------
36    Turn checks whether constant names are used as variables on or off.
37    Default: true
38
39
40    "Santity Check Thm-Name Clash":
41    -------------------------------
42    Turn checks whether the same theorem name is used in multiple theories.
43    Default: true
44
45  *)
46
47
48 (* sanity checks the given theory *)
49 val sanity_check_theory    : string -> bool
50
51 (* sanity checks the current theory *)
52 val sanity_check           : unit   -> bool
53
54 (* sanity checks all loaded theories *)
55 val sanity_check_all       : unit   -> bool
56
57 (* sanity checks a theorem *)
58 val sanity_check_thm       : thm -> bool
59
60 (* sanity checks a theorem with a given name *)
61 val sanity_check_named_thm : (string * thm) -> bool
62
63
64 (* versions of prove, store_thm and save_thm that perform checks,
65    see trace "Sanity Check Strict" *)
66 val sanity_prove : (term * tactic) -> thm
67 val save_thm     : (string * thm) -> thm
68 val store_thm    : (string * term * tactic) -> thm
69
70end
71