author  blanchet 
Thu, 17 Mar 2011 22:07:17 +0100  
changeset 41993  bd6296de1432 
parent 41992  0e4716fa330a 
child 41995  03c2d29ec790 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Finite model generation for HOL formulas using Kodkod. 

6 
*) 

7 

8 
signature NITPICK = 

9 
sig 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

10 
type styp = Nitpick_Util.styp 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

11 
type term_postprocessor = Nitpick_Model.term_postprocessor 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

12 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

13 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

14 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

15 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

16 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

17 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

18 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

19 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

20 
monos: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

21 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

22 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

23 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

24 
blocking: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

25 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

26 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

27 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

28 
overlord: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

29 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

30 
assms: bool, 
38209  31 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

32 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

33 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

34 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

35 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

36 
star_linear_preds: bool, 
41856  37 
total_consts: bool option, 
41876  38 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

39 
peephole_optim: bool, 
38124  40 
datatype_sym_break: int, 
41 
kodkod_sym_break: int, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

42 
timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

43 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

44 
max_threads: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

45 
show_datatypes: bool, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

46 
show_skolems: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

47 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

48 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

49 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

50 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

51 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

52 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

53 
check_potential: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

54 
check_genuine: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

55 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

56 
expect: string} 
33192  57 

58 
val register_frac_type : string > (string * string) list > theory > theory 

59 
val unregister_frac_type : string > theory > theory 

60 
val register_codatatype : typ > string > styp list > theory > theory 

61 
val unregister_codatatype : typ > theory > theory 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

62 
val register_term_postprocessor : 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

63 
typ > term_postprocessor > theory > theory 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

64 
val unregister_term_postprocessor : typ > theory > theory 
33192  65 
val pick_nits_in_term : 
35335  66 
Proof.state > params > bool > int > int > int > (term * term) list 
67 
> term list > term > string * Proof.state 

33192  68 
val pick_nits_in_subgoal : 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

69 
Proof.state > params > bool > int > int > string * Proof.state 
33192  70 
end; 
71 

72 
structure Nitpick : NITPICK = 

73 
struct 

74 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

75 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

76 
open Nitpick_HOL 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

77 
open Nitpick_Preproc 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

78 
open Nitpick_Mono 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

79 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

80 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

81 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

82 
open Nitpick_Nut 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

83 
open Nitpick_Kodkod 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

84 
open Nitpick_Model 
33192  85 

34126  86 
structure KK = Kodkod 
87 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

88 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

89 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

90 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

91 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

92 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

93 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

94 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

95 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

96 
monos: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

97 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

98 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

99 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

100 
blocking: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

101 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

102 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

103 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

104 
overlord: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

105 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

106 
assms: bool, 
38209  107 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

108 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

109 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

110 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

111 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

112 
star_linear_preds: bool, 
41856  113 
total_consts: bool option, 
41876  114 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

115 
peephole_optim: bool, 
38124  116 
datatype_sym_break: int, 
117 
kodkod_sym_break: int, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

118 
timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

119 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

120 
max_threads: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

121 
show_datatypes: bool, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

122 
show_skolems: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

123 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

124 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

125 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

126 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

127 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

128 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

129 
check_potential: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

130 
check_genuine: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

131 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

132 
expect: string} 
33192  133 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

134 
(* TODO: eliminate these historical aliases *) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

135 
val register_frac_type = Nitpick_HOL.register_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

136 
val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

137 
val register_codatatype = Nitpick_HOL.register_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

138 
val unregister_codatatype = Nitpick_HOL.unregister_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

139 
val register_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

140 
Nitpick_Model.register_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

141 
val unregister_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

142 
Nitpick_Model.unregister_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

143 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

144 
type problem_extension = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

145 
{free_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

146 
sel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

147 
nonsel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

148 
rel_table: nut NameTable.table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

149 
unsound: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

150 
scope: scope} 
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
38857
diff
changeset

151 

34126  152 
type rich_problem = KK.problem * problem_extension 
33192  153 

154 
fun pretties_for_formulas _ _ [] = [] 

155 
 pretties_for_formulas ctxt s ts = 

156 
[Pretty.str (s ^ plural_s_for_list ts ^ ":"), 

157 
Pretty.indent indent_size (Pretty.chunks 

158 
(map2 (fn j => fn t => 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

159 
Pretty.block [t > shorten_names_in_term 
33192  160 
> Syntax.pretty_term ctxt, 
161 
Pretty.str (if j = 1 then "." else ";")]) 

162 
(length ts downto 1) ts))] 

163 

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

164 
fun install_java_message () = 
38517  165 
"Nitpick requires a Java 1.5 virtual machine called \"java\"." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

166 
fun install_kodkodi_message () = 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

167 
"Nitpick requires the external Java program Kodkodi. To install it, download \ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

168 
\the package from Isabelle's web page and add the \"kodkodix.y.z\" \ 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41897
diff
changeset

169 
\directory's full path to " ^ 
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41897
diff
changeset

170 
Path.print (Path.expand (Path.appends 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

171 
(Path.variable "ISABELLE_HOME_USER" :: 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41897
diff
changeset

172 
map Path.basic ["etc", "components"]))) ^ " on a line of its own." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

173 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

174 
val max_unsound_delay_ms = 200 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

175 
val max_unsound_delay_percent = 2 
33192  176 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

177 
fun unsound_delay_for_timeout NONE = max_unsound_delay_ms 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

178 
 unsound_delay_for_timeout (SOME timeout) = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

179 
Int.max (0, Int.min (max_unsound_delay_ms, 
33192  180 
Time.toMilliseconds timeout 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

181 
* max_unsound_delay_percent div 100)) 
33192  182 

183 
fun passed_deadline NONE = false 

184 
 passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS 

185 

34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

186 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  187 

41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

188 
fun has_lonely_bool_var (@{const Pure.conjunction} 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

189 
$ (@{const Trueprop} $ Free _) $ _) = true 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

190 
 has_lonely_bool_var _ = false 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

191 

34038
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

192 
val syntactic_sorts = 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38517
diff
changeset

193 
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ 
34038
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

194 
@{sort number} 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

195 
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

196 
subset (op =) (S, syntactic_sorts) 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

197 
 has_tfree_syntactic_sort _ = false 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

198 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  199 

33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

200 
fun plazy f = Pretty.blk (0, pstrs (f ())) 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

201 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

202 
fun pick_them_nits_in_term deadline state (params : params) auto i n step 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

203 
subst assm_ts orig_t = 
33192  204 
let 
205 
val timer = Timer.startRealTimer () 

34935
cb011ba38950
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents:
34126
diff
changeset

206 
val thy = Proof.theory_of state 
cb011ba38950
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents:
34126
diff
changeset

207 
val ctxt = Proof.context_of state 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

208 
(* FIXME: reintroduce code before new release: 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

209 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37213
diff
changeset

210 
val nitpick_thy = Thy_Info.get_theory "Nitpick" 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

211 
val _ = Theory.subthy (nitpick_thy, thy) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

212 
error "You must import the theory \"Nitpick\" to use Nitpick" 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

213 
*) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

214 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

215 
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, 
38209  216 
verbose, overlord, user_axioms, assms, whacks, merge_type_vars, 
217 
binary_ints, destroy_constrs, specialize, star_linear_preds, 

41875  218 
total_consts, needs, peephole_optim, datatype_sym_break, 
41856  219 
kodkod_sym_break, tac_timeout, max_threads, show_datatypes, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

220 
show_skolems, show_consts, evals, formats, atomss, max_potential, 
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

221 
max_genuine, check_potential, check_genuine, batch_size, ...} = params 
33192  222 
val state_ref = Unsynchronized.ref state 
223 
val pprint = 

224 
if auto then 

225 
Unsynchronized.change state_ref o Proof.goal_message o K 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33558
diff
changeset

226 
o Pretty.chunks o cons (Pretty.str "") o single 
33192  227 
o Pretty.mark Markup.hilite 
228 
else 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39361
diff
changeset

229 
(fn s => (Output.urgent_message s; if debug then tracing s else ())) 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

230 
o Pretty.string_of 
33192  231 
fun pprint_m f = () > not auto ? pprint o f 
232 
fun pprint_v f = () > verbose ? pprint o f 

233 
fun pprint_d f = () > debug ? pprint o f 

234 
val print = pprint o curry Pretty.blk 0 o pstrs 

39345  235 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

236 
val print_g = pprint o Pretty.str 
39345  237 
*) 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

238 
val print_m = pprint_m o K o plazy 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

239 
val print_v = pprint_v o K o plazy 
33192  240 

241 
fun check_deadline () = 

41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

242 
if passed_deadline deadline then raise TimeLimit.TimeOut else () 
33192  243 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

244 
val assm_ts = if assms orelse auto then assm_ts else [] 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

245 
val _ = 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

246 
if step = 0 then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

247 
print_m (fn () => "Nitpicking formula...") 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

248 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

249 
pprint_m (fn () => Pretty.chunks ( 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

250 
pretties_for_formulas ctxt ("Nitpicking " ^ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

251 
(if i <> 1 orelse n <> 1 then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

252 
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

253 
else 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

254 
"goal")) [Logic.list_implies (assm_ts, orig_t)])) 
41278
8e1cde88aae6
added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents:
41052
diff
changeset

255 
val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" 
8e1cde88aae6
added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents:
41052
diff
changeset

256 
o Date.fromTimeLocal o Time.now) 
33192  257 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) 
258 
else orig_t 

41876  259 
val conj_ts = neg_t :: assm_ts @ evals @ these needs 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

260 
val tfree_table = 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

261 
if merge_type_vars then merged_type_var_table_for_terms thy conj_ts 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

262 
else [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

263 
val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

264 
val neg_t = neg_t > merge_tfrees 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

265 
val assm_ts = assm_ts > map merge_tfrees 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

266 
val evals = evals > map merge_tfrees 
41876  267 
val needs = needs > Option.map (map merge_tfrees) 
268 
val conj_ts = neg_t :: assm_ts @ evals @ these needs 

33192  269 
val original_max_potential = max_potential 
270 
val original_max_genuine = max_genuine 

271 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

272 
val case_names = case_const_names ctxt stds 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

273 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

274 
val def_tables = const_def_tables ctxt subst defs 
33192  275 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 
35335  276 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
277 
val psimp_table = const_psimp_table ctxt subst 

35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

278 
val choice_spec_table = const_choice_spec_table ctxt subst 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

279 
val user_nondefs = 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

280 
user_nondefs > filter_out (is_choice_spec_axiom thy choice_spec_table) 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

281 
val intro_table = inductive_intro_table ctxt subst def_tables 
33192  282 
val ground_thm_table = ground_theorem_table thy 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

283 
val ersatz_table = ersatz_table ctxt 
41007
75275c796b46
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout  this becomes necessary with the new, more powerful monotonicity calculus
blanchet
parents:
41001
diff
changeset

284 
val hol_ctxt as {wf_cache, ...} = 
33192  285 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

286 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
38209  287 
whacks = whacks, binary_ints = binary_ints, 
288 
destroy_constrs = destroy_constrs, specialize = specialize, 

41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

289 
star_linear_preds = star_linear_preds, total_consts = total_consts, 
41875  290 
needs = needs, tac_timeout = tac_timeout, evals = evals, 
41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

291 
case_names = case_names, def_tables = def_tables, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

292 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

293 
simp_table = simp_table, psimp_table = psimp_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

294 
choice_spec_table = choice_spec_table, intro_table = intro_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

295 
ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

296 
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

297 
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

298 
constr_cache = Unsynchronized.ref []} 
41789
7c7b68b06c1a
don't distinguish between "fixes" and other free variables  this confuses users
blanchet
parents:
41772
diff
changeset

299 
val pseudo_frees = [] 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

300 
val real_frees = fold Term.add_frees conj_ts [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

301 
val _ = null (fold Term.add_tvars conj_ts []) orelse 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

302 
error "Nitpick cannot handle goals with schematic type variables." 
41875  303 
val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

304 
no_poly_user_axioms, binarize) = 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

305 
preprocess_formulas hol_ctxt assm_ts neg_t 
33192  306 
val got_all_user_axioms = 
307 
got_all_mono_user_axioms andalso no_poly_user_axioms 

308 

309 
fun print_wf (x, (gfp, wf)) = 

310 
pprint (Pretty.blk (0, 

311 
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"") 

312 
@ Syntax.pretty_term ctxt (Const x) :: 

313 
pstrs (if wf then 

314 
"\" was proved wellfounded. Nitpick can compute it \ 

315 
\efficiently." 

316 
else 

317 
"\" could not be proved wellfounded. Nitpick might need to \ 

318 
\unroll it."))) 

319 
val _ = if verbose then List.app print_wf (!wf_cache) else () 

38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

320 
val das_wort_formula = if falsify then "Negated conjecture" else "Formula" 
33192  321 
val _ = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

322 
pprint_d (fn () => Pretty.chunks 
38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

323 
(pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

324 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

325 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

326 
(tl nondef_ts))) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

327 
val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts) 
33192  328 
handle TYPE (_, Ts, ts) => 
329 
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) 

330 

41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

331 
val nondef_us = nondef_ts > map (nut_from_term hol_ctxt Eq) 
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

332 
val def_us = def_ts > map (nut_from_term hol_ctxt DefEq) 
41875  333 
val need_us = need_ts > map (nut_from_term hol_ctxt Eq) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

334 
val (free_names, const_names) = 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

335 
fold add_free_and_const_names (nondef_us @ def_us @ need_us) ([], []) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

336 
val (sel_names, nonsel_names) = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

337 
List.partition (is_sel o nickname_of) const_names 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

338 
val sound_finitizes = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

339 
none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

340 
 _ => false) finitizes) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

341 
val standard = forall snd stds 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

342 
(* 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

343 
val _ = 
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

344 
List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

345 
*) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

346 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

347 
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

348 
fun monotonicity_message Ts extra = 
38188  349 
let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in 
350 
Pretty.blk (0, 

351 
pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @ 

352 
pretty_serial_commas "and" pretties @ 

353 
pstrs (" " ^ 

354 
(if none_true monos then 

355 
"passed the monotonicity test" 

356 
else 

357 
(if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^ 

358 
". " ^ extra)) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

359 
end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

360 
fun is_type_fundamentally_monotonic T = 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

361 
(is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

362 
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

363 
is_number_type ctxt T orelse is_bit_type T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

364 
fun is_type_actually_monotonic T = 
41001
11715564e2ad
removed old baggage from monotonicity calculus  the "calculus" option didn't really work anyway because of onthefly simplifications
blanchet
parents:
40993
diff
changeset

365 
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

366 
fun is_type_kind_of_monotonic T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

367 
case triple_lookup (type_match thy) monos T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

368 
SOME (SOME false) => false 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

369 
 _ => is_type_actually_monotonic T 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

370 
fun is_type_monotonic T = 
33192  371 
unique_scope orelse 
372 
case triple_lookup (type_match thy) monos T of 

373 
SOME (SOME b) => b 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

374 
 _ => is_type_fundamentally_monotonic T orelse 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

375 
is_type_actually_monotonic T 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

376 
fun is_deep_datatype_finitizable T = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

377 
triple_lookup (type_match thy) finitizes T = SOME (SOME true) 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41051
diff
changeset

378 
fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

379 
is_type_kind_of_monotonic T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

380 
 is_shallow_datatype_finitizable T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

381 
case triple_lookup (type_match thy) finitizes T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

382 
SOME (SOME b) => b 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

383 
 _ => is_type_kind_of_monotonic T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

384 
fun is_datatype_deep T = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

385 
not standard orelse T = nat_T orelse is_word_type T orelse 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

386 
exists (curry (op =) T o domain_type o type_of) sel_names 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

387 
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) 
35408  388 
> sort Term_Ord.typ_ord 
38214  389 
val _ = 
390 
if verbose andalso binary_ints = SOME true andalso 

391 
exists (member (op =) [nat_T, int_T]) all_Ts then 

392 
print_v (K "The option \"binary_ints\" will be ignored because of the \ 

393 
\presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \ 

394 
\in the problem or because of the \"non_std\" option.") 

395 
else 

396 
() 

397 
val _ = 

398 
if not auto andalso 

399 
exists (fn Type (@{type_name Datatype.node}, _) => true  _ => false) 

400 
all_Ts then 

401 
print_m (K ("Warning: The problem involves directly or indirectly the \ 

402 
\internal type " ^ quote @{type_name Datatype.node} ^ 

403 
". This type is very Nitpickunfriendly, and its presence \ 

39361  404 
\usually indicates either a failure of abstraction or a \ 
405 
\quirk in Nitpick.")) 

38214  406 
else 
407 
() 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

408 
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts 
33192  409 
val _ = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

410 
if verbose andalso not unique_scope then 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

411 
case filter_out is_type_fundamentally_monotonic mono_Ts of 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

412 
[] => () 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

413 
 interesting_mono_Ts => 
38188  414 
pprint_v (K (monotonicity_message interesting_mono_Ts 
415 
"Nitpick might be able to skip some scopes.")) 

33192  416 
else 
417 
() 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

418 
val (deep_dataTs, shallow_dataTs) = 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

419 
all_Ts > filter (is_datatype ctxt stds) 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

420 
> List.partition is_datatype_deep 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

421 
val finitizable_dataTs = 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

422 
(deep_dataTs > filter_out (is_finite_type hol_ctxt) 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

423 
> filter is_deep_datatype_finitizable) @ 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

424 
(shallow_dataTs > filter_out (is_finite_type hol_ctxt) 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

425 
> filter is_shallow_datatype_finitizable) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

426 
val _ = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

427 
if verbose andalso not (null finitizable_dataTs) then 
38188  428 
pprint_v (K (monotonicity_message finitizable_dataTs 
429 
"Nitpick can use a more precise finite encoding.")) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

430 
else 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

431 
() 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

432 
(* This detection code is an ugly hack. Fortunately, it is used only to 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

433 
provide a hint to the user. *) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

434 
fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) = 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

435 
not (null fixes) andalso 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

436 
exists (String.isSuffix ".hyps" o fst) assumes andalso 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

437 
exists (exists (curry (op =) name o shortest_name o fst) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

438 
o datatype_constrs hol_ctxt) deep_dataTs 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

439 
val likely_in_struct_induct_step = 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

440 
exists is_struct_induct_step (ProofContext.cases_of ctxt) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

441 
val _ = if standard andalso likely_in_struct_induct_step then 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

442 
pprint_m (fn () => Pretty.blk (0, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

443 
pstrs "Hint: To check that the induction hypothesis is \ 
35177  444 
\general enough, try this command: " @ 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

445 
[Pretty.mark Markup.sendback (Pretty.blk (0, 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

446 
pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

447 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

448 
() 
33192  449 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

450 
val _ = print_g "Monotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

451 
val _ = List.app (print_g o string_for_type ctxt) mono_Ts 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

452 
val _ = print_g "Nonmonotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

453 
val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts 
33192  454 
*) 
455 

36384  456 
val incremental = Int.max (max_potential, max_genuine) >= 2 
457 
val actual_sat_solver = 

33192  458 
if sat_solver <> "smart" then 
36384  459 
if incremental andalso 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

460 
not (member (op =) (Kodkod_SAT.configured_sat_solvers true) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

461 
sat_solver) then 
33192  462 
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ 
463 
\be used instead of " ^ quote sat_solver ^ ".")); 

464 
"SAT4J") 

465 
else 

466 
sat_solver 

467 
else 

36384  468 
Kodkod_SAT.smart_sat_solver_name incremental 
33192  469 
val _ = 
470 
if sat_solver = "smart" then 

36384  471 
print_v (fn () => 
472 
"Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^ 

473 
(if incremental then " incremental " else " ") ^ 

474 
"solvers are configured: " ^ 

475 
commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".") 

33192  476 
else 
477 
() 

478 

479 
val too_big_scopes = Unsynchronized.ref [] 

480 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

481 
fun problem_for_scope unsound 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

482 
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = 
33192  483 
let 
484 
val _ = not (exists (fn other => scope_less_eq other scope) 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

485 
(!too_big_scopes)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

486 
raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

487 
\problem_for_scope", "too large scope") 
33192  488 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

489 
val _ = print_g "Offsets:" 
33192  490 
val _ = List.app (fn (T, j0) => 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

491 
print_g (string_for_type ctxt T ^ " = " ^ 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

492 
string_of_int j0)) 
33192  493 
(Typtab.dest ofs) 
494 
*) 

41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

495 
val effective_total_consts = 
41856  496 
case total_consts of 
497 
SOME b => b 

498 
 NONE => forall (is_exact_type datatypes true) all_Ts 

33192  499 
val main_j0 = offset_of_type ofs bool_T 
500 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

501 
val (int_card, int_j0) = spec_of_type scope int_T 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

502 
val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

503 
raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope", 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

504 
"bad offsets") 
33192  505 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
506 
val (free_names, rep_table) = 

38170  507 
choose_reps_for_free_vars scope pseudo_frees free_names 
508 
NameTable.empty 

33192  509 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 
38170  510 
val (nonsel_names, rep_table) = 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

511 
choose_reps_for_consts scope effective_total_consts nonsel_names 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

512 
rep_table 
38182  513 
val (guiltiest_party, min_highest_arity) = 
514 
NameTable.fold (fn (name, R) => fn (s, n) => 

515 
let val n' = arity_of_rep R in 

516 
if n' > n then (nickname_of name, n') else (s, n) 

517 
end) rep_table ("", 1) 

33192  518 
val min_univ_card = 
36384  519 
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table 
34126  520 
(univ_card nat_card int_card main_j0 [] KK.True) 
41897
c24e7fd17464
perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents:
41888
diff
changeset

521 
val _ = if debug then () 
c24e7fd17464
perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents:
41888
diff
changeset

522 
else check_arity guiltiest_party min_univ_card min_highest_arity 
33192  523 

41802  524 
val def_us = 
525 
def_us > map (choose_reps_in_nut scope unsound rep_table true) 

526 
val nondef_us = 

527 
nondef_us > map (choose_reps_in_nut scope unsound rep_table false) 

41875  528 
val need_us = 
529 
need_us > map (choose_reps_in_nut scope unsound rep_table false) 

33745  530 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

531 
val _ = List.app (print_g o string_for_nut ctxt) 
33192  532 
(free_names @ sel_names @ nonsel_names @ 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

533 
nondef_us @ def_us @ need_us) 
33745  534 
*) 
33192  535 
val (free_rels, pool, rel_table) = 
536 
rename_free_vars free_names initial_pool NameTable.empty 

537 
val (sel_rels, pool, rel_table) = 

538 
rename_free_vars sel_names pool rel_table 

539 
val (other_rels, pool, rel_table) = 

540 
rename_free_vars nonsel_names pool rel_table 

41802  541 
val nondef_us = nondef_us > map (rename_vars_in_nut pool rel_table) 
542 
val def_us = def_us > map (rename_vars_in_nut pool rel_table) 

41875  543 
val need_us = need_us > map (rename_vars_in_nut pool rel_table) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

544 
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

545 
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

546 
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

547 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
36913
diff
changeset

548 
Print_Mode.setmp [] multiline_string_for_scope scope 
34998  549 
val kodkod_sat_solver = 
36384  550 
Kodkod_SAT.sat_solver_spec actual_sat_solver > snd 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

551 
val bit_width = if bits = 0 then 16 else bits + 1 
36384  552 
val delay = 
553 
if unsound then 

554 
Option.map (fn time => Time. (time, Time.now ())) deadline 

555 
> unsound_delay_for_timeout 

556 
else 

557 
0 

558 
val settings = [("solver", commas_quote kodkod_sat_solver), 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

559 
("bit_width", string_of_int bit_width), 
38124  560 
("symmetry_breaking", string_of_int kodkod_sym_break), 
36386
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

561 
("sharing", "3"), 
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

562 
("flatten", "false"), 
33192  563 
("delay", signed_string_of_int delay)] 
564 
val plain_rels = free_rels @ other_rels 

565 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

566 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

567 
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

568 
val dtype_axioms = 
41875  569 
declarative_axioms_for_datatypes hol_ctxt binarize need_us 
41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

570 
datatype_sym_break bits ofs kk rel_table datatypes 
33192  571 
val declarative_axioms = plain_axioms @ dtype_axioms 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

572 
val univ_card = Int.max (univ_card nat_card int_card main_j0 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

573 
(plain_bounds @ sel_bounds) formula, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

574 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
38126  575 
val (built_in_bounds, built_in_axioms) = 
39345  576 
bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card 
577 
nat_card int_card main_j0 (formula :: declarative_axioms) 

33192  578 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 
579 
> not debug ? merge_bounds 

38126  580 
val axioms = built_in_axioms @ declarative_axioms 
33192  581 
val highest_arity = 
582 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

38126  583 
val formula = fold_rev s_and axioms formula 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

584 
val _ = if bits = 0 then () else check_bits bits formula 
41897
c24e7fd17464
perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet
parents:
41888
diff
changeset

585 
val _ = if debug orelse formula = KK.False then () 
38182  586 
else check_arity "" univ_card highest_arity 
33192  587 
in 
588 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

589 
tuple_assigns = [], bounds = bounds, 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

590 
int_bounds = if bits = 0 then sequential_int_bounds univ_card 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

591 
else pow_of_two_int_bounds bits main_j0, 
33192  592 
expr_assigns = [], formula = formula}, 
593 
{free_names = free_names, sel_names = sel_names, 

594 
nonsel_names = nonsel_names, rel_table = rel_table, 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

595 
unsound = unsound, scope = scope}) 
33192  596 
end 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

597 
handle TOO_LARGE (loc, msg) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

598 
if loc = "Nitpick_Kodkod.check_arity" andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

599 
not (Typtab.is_empty ofs) then 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

600 
problem_for_scope unsound 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

601 
{hol_ctxt = hol_ctxt, binarize = binarize, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

602 
card_assigns = card_assigns, bits = bits, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

603 
bisim_depth = bisim_depth, datatypes = datatypes, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

604 
ofs = Typtab.empty} 
33192  605 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
606 
\problem_for_scope" then 

607 
NONE 

608 
else 

609 
(Unsynchronized.change too_big_scopes (cons scope); 

41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

610 
print_v (fn () => 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

611 
"Limit reached: " ^ msg ^ ". Skipping " ^ 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

612 
(if unsound then "potential component of " else "") ^ 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

613 
"scope."); 
33192  614 
NONE) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

615 
 TOO_SMALL (_, msg) => 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

616 
(print_v (fn () => 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

617 
"Limit reached: " ^ msg ^ ". Skipping " ^ 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

618 
(if unsound then "potential component of " else "") ^ 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

619 
"scope."); 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

620 
NONE) 
33192  621 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

622 
val das_wort_model = 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

623 
(if falsify then "counterexample" else "model") 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

624 
> not standard ? prefix "nonstandard " 
33192  625 

626 
val scopes = Unsynchronized.ref [] 

627 
val generated_scopes = Unsynchronized.ref [] 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

628 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  629 
val checked_problems = Unsynchronized.ref (SOME []) 
630 
val met_potential = Unsynchronized.ref 0 

631 

632 
fun update_checked_problems problems = 

633 
List.app (Unsynchronized.change checked_problems o Option.map o cons 

634 
o nth problems) 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

635 
fun show_kodkod_warning "" = () 
35334
b83b9f2a4b92
show Kodkod warning message even in nonverbose mode
blanchet
parents:
35333
diff
changeset

636 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  637 

638 
fun print_and_check_model genuine bounds 

639 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

640 
: problem_extension) = 

641 
let 

642 
val (reconstructed_model, codatatypes_ok) = 

41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

643 
reconstruct_hol_model 
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

644 
{show_datatypes = show_datatypes, show_skolems = show_skolems, 
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

645 
show_consts = show_consts} 
38170  646 
scope formats atomss real_frees pseudo_frees free_names sel_names 
647 
nonsel_names rel_table bounds 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

648 
val genuine_means_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

649 
got_all_user_axioms andalso none_true wfs andalso 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

650 
sound_finitizes andalso total_consts <> SOME true andalso 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

651 
codatatypes_ok 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

652 
fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) 
33192  653 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

654 
(pprint (Pretty.chunks 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

655 
[Pretty.blk (0, 
40223  656 
(pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^ 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

657 
(if not genuine then " potentially spurious " 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

658 
else if genuine_means_genuine then " " 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

659 
else " quasi genuine ") ^ das_wort_model) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

660 
(case pretties_for_scope scope verbose of 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

661 
[] => [] 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

662 
 pretties => pstrs " for " @ pretties) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

663 
[Pretty.str ":\n"])), 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

664 
Pretty.indent indent_size reconstructed_model]); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

665 
if genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

666 
(if check_genuine andalso standard then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

667 
case prove_hol_model scope tac_timeout free_names sel_names 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

668 
rel_table bounds (assms_prop ()) of 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

669 
SOME true => 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

670 
print ("Confirmation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

671 
das_wort_model ^ " is really genuine.") 
33192  672 
 SOME false => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

673 
if genuine_means_genuine then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

674 
error ("A supposedly genuine " ^ das_wort_model ^ " was \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

675 
\shown to be spurious by \"auto\".\nThis should never \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

676 
\happen.\nPlease send a bug report to blanchet\ 
33192  677 
\te@in.tum.de.") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

678 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

679 
print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

680 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

681 
 NONE => print "No confirmation by \"auto\"." 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

682 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

683 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

684 
if not standard andalso likely_in_struct_induct_step then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

685 
print "The existence of a nonstandard model suggests that the \ 
36126  686 
\induction hypothesis is not general enough or may even be \ 
687 
\wrong. See the Nitpick manual's \"Inductive Properties\" \ 

688 
\section for details (\"isabelle doc nitpick\")." 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

689 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

690 
(); 
41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

691 
if has_lonely_bool_var orig_t then 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

692 
print "Hint: Maybe you forgot a colon after the lemma's name?" 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

693 
else if has_syntactic_sorts orig_t then 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

694 
print "Hint: Maybe you forgot a type constraint?" 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

695 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

696 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

697 
if not genuine_means_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

698 
if no_poly_user_axioms then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

699 
let 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

700 
val options = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

701 
[] > not got_all_mono_user_axioms 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

702 
? cons ("user_axioms", "\"true\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

703 
> not (none_true wfs) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

704 
? cons ("wf", "\"smart\" or \"false\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

705 
> not sound_finitizes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

706 
? cons ("finitize", "\"smart\" or \"false\"") 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

707 
> total_consts = SOME true 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

708 
? cons ("total_consts", "\"smart\" or \"false\"") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

709 
> not codatatypes_ok 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

710 
? cons ("bisim_depth", "a nonnegative value") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

711 
val ss = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

712 
map (fn (name, value) => quote name ^ " set to " ^ value) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

713 
options 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

714 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

715 
print ("Try again with " ^ 
41872  716 
space_implode " " (serial_commas "and" ss) ^ 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

717 
" to confirm that the " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

718 
" is genuine.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

719 
end 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

720 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

721 
print ("Nitpick is unable to guarantee the authenticity of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

722 
\the " ^ das_wort_model ^ " in the presence of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

723 
\polymorphic axioms.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

724 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

725 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

726 
NONE) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

727 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

728 
if not genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

729 
(Unsynchronized.inc met_potential; 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

730 
if check_potential then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

731 
let 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

732 
val status = prove_hol_model scope tac_timeout free_names 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

733 
sel_names rel_table bounds 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

734 
(assms_prop ()) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

735 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

736 
(case status of 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

737 
SOME true => print ("Confirmation by \"auto\": The \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

738 
\above " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

739 
" is genuine.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

740 
 SOME false => print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

741 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

742 
 NONE => print "No confirmation by \"auto\"."); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

743 
status 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

744 
end 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

745 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

746 
NONE) 
33192  747 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

748 
NONE) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

749 
> pair genuine_means_genuine 
33192  750 
end 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

751 
fun solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

752 
donno) first_time problems = 
33192  753 
let 
754 
val max_potential = Int.max (0, max_potential) 

755 
val max_genuine = Int.max (0, max_genuine) 

756 
fun print_and_check genuine (j, bounds) = 

757 
print_and_check_model genuine bounds (snd (nth problems j)) 

758 
val max_solutions = max_potential + max_genuine 

36384  759 
> not incremental ? Integer.min 1 
33192  760 
in 
761 
if max_solutions <= 0 then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

762 
(found_really_genuine, 0, 0, donno) 
33192  763 
else 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

764 
case KK.solve_any_problem debug overlord deadline max_threads 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

765 
max_solutions (map fst problems) of 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

766 
KK.JavaNotInstalled => 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

767 
(print_m install_java_message; 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

768 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

769 
 KK.JavaTooOld => 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

770 
(print_m install_java_message; 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

771 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

772 
 KK.KodkodiNotInstalled => 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

773 
(print_m install_kodkodi_message; 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

774 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

775 
 KK.Normal ([], unsat_js, s) => 
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

776 
(update_checked_problems problems unsat_js; show_kodkod_warning s; 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

777 
(found_really_genuine, max_potential, max_genuine, donno)) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

778 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  779 
let 
780 
val (lib_ps, con_ps) = 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

781 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  782 
in 
783 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

784 
show_kodkod_warning s; 
33192  785 
if null con_ps then 
786 
let 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

787 
val genuine_codes = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

788 
lib_ps > take max_potential 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

789 
> map (print_and_check false) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

790 
> filter (curry (op =) (SOME true) o snd) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

791 
val found_really_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

792 
found_really_genuine orelse exists fst genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

793 
val num_genuine = length genuine_codes 
33192  794 
val max_genuine = max_genuine  num_genuine 
795 
val max_potential = max_potential 

796 
 (length lib_ps  num_genuine) 

797 
in 

798 
if max_genuine <= 0 then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

799 
(found_really_genuine, 0, 0, donno) 
33192  800 
else 
801 
let 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

802 
(* "co_js" is the list of sound problems whose unsound 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

803 
pendants couldn't be satisfied and hence that most 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

804 
probably can't be satisfied themselves. *) 
33192  805 
val co_js = 
806 
map (fn j => j  1) unsat_js 

807 
> filter (fn j => 

808 
j >= 0 andalso 

809 
scopes_equivalent 

35814  810 
(#scope (snd (nth problems j)), 
811 
#scope (snd (nth problems (j + 1))))) 

33192  812 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 
813 
unsat_js @ co_js) 

814 
val problems = 

815 
problems > filter_out_indices bye_js 

816 
> max_potential <= 0 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

817 
? filter_out (#unsound o snd) 
33192  818 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

819 
solve_any_problem (found_really_genuine, max_potential, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

820 
max_genuine, donno) false problems 
33192  821 
end 
822 
end 

823 
else 

824 
let 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

825 
val genuine_codes = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

826 
con_ps > take max_genuine 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

827 
> map (print_and_check true) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

828 
val max_genuine = max_genuine  length genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

829 
val found_really_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

830 
found_really_genuine orelse exists fst genuine_codes 
33192  831 
in 
832 
if max_genuine <= 0 orelse not first_time then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

833 
(found_really_genuine, 0, max_genuine, donno) 
33192  834 
else 
835 
let 

836 
val bye_js = sort_distinct int_ord 

837 
(map fst sat_ps @ unsat_js) 

838 
val problems = 

839 
problems > filter_out_indices bye_js 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

840 
> filter_out (#unsound o snd) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

841 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

842 
solve_any_problem (found_really_genuine, 0, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

843 
donno) false problems 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

844 
end 
33192  845 
end 
846 
end 

34126  847 
 KK.TimedOut unsat_js => 
33192  848 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  849 
 KK.Error (s, unsat_js) => 
33192  850 
(update_checked_problems problems unsat_js; 
851 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

852 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  853 
end 
854 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

855 
fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

856 
donno) = 
33192  857 
let 
858 
val _ = 

859 
if null scopes then 

860 
print_m (K "The scope specification is inconsistent.") 

861 
else if verbose then 

862 
pprint (Pretty.chunks 

863 
[Pretty.blk (0, 

864 
pstrs ((if n > 1 then 

865 
"Batch " ^ string_of_int (j + 1) ^ " of " ^ 

866 
signed_string_of_int n ^ ": " 

867 
else 

868 
"") ^ 

869 
"Trying " ^ string_of_int (length scopes) ^ 

870 
" scope" ^ plural_s_for_list scopes ^ ":")), 

871 
Pretty.indent indent_size 

872 
(Pretty.chunks (map2 

873 
(fn j => fn scope => 

874 
Pretty.block ( 

875 
(case pretties_for_scope scope true of 

876 
[] => [Pretty.str "Empty"] 

877 
 pretties => pretties) @ 

878 
[Pretty.str (if j = 1 then "." else ";")])) 

879 
(length scopes downto 1) scopes))]) 

880 
else 

881 
() 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

882 
fun add_problem_for_scope (scope, unsound) (problems, donno) = 
33192  883 
(check_deadline (); 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

884 
case problem_for_scope unsound scope of 
33192  885 
SOME problem => 
886 
(problems 

887 
> (null problems orelse 

35814  888 
not (KK.problems_equivalent (fst problem, fst (hd problems)))) 
33192  889 
? cons problem, donno) 
890 
 NONE => (problems, donno + 1)) 

891 
val (problems, donno) = 

892 
fold add_problem_for_scope 

893 
(map_product pair scopes 

894 
((if max_genuine > 0 then [false] else []) @ 

895 
(if max_potential > 0 then [true] else []))) 

896 
([], donno) 

897 
val _ = Unsynchronized.change generated_problems (append problems) 

898 
val _ = Unsynchronized.change generated_scopes (append scopes) 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

899 
val _ = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

900 
if j + 1 = n then 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

901 
let 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

902 
val (unsound_problems, sound_problems) = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

903 
List.partition (#unsound o snd) (!generated_problems) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

904 
in 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

905 
if not (null sound_problems) andalso 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

906 
forall (KK.is_problem_trivially_false o fst) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

907 
sound_problems then 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

908 
print_m (fn () => 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

909 
"Warning: The conjecture either trivially holds for the \ 
35384  910 
\given scopes or lies outside Nitpick's supported \ 
911 
\fragment." ^ 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

912 
(if exists (not o KK.is_problem_trivially_false o fst) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

913 
unsound_problems then 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

914 
" Only potentially spurious " ^ das_wort_model ^ 
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

915 
"s may be found." 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

916 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

917 
"")) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

918 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

919 
() 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

920 
end 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

921 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

922 
() 
33192  923 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

924 
solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

925 
donno) true (rev problems) 
33192  926 
end 
927 

928 
fun scope_count (problems : rich_problem list) scope = 

35814  929 
length (filter (curry scopes_equivalent scope o #scope o snd) problems) 
33192  930 
fun excipit did_so_and_so = 
931 
let 

932 
val do_filter = 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

933 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  934 
else I 
935 
val total = length (!scopes) 

936 
val unsat = 

937 
fold (fn scope => 

938 
case scope_count (do_filter (!generated_problems)) scope of 

939 
0 => I 

940 
 n => 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

941 
scope_count (do_filter (these (!checked_problems))) 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

942 
scope = n 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

943 
? Integer.add 1) (!generated_scopes) 0 
33192  944 
in 
945 
"Nitpick " ^ did_so_and_so ^ 

946 
(if is_some (!checked_problems) andalso total > 0 then 

39361  947 
" " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" 
948 
^ plural_s total 

33192  949 
else 
950 
"") ^ "." 

951 
end 

952 

37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

953 
val (skipped, the_scopes) = 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

954 
all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

955 
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

956 
finitizable_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

957 
val _ = if skipped > 0 then 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

958 
print_m (fn () => "Too many scopes. Skipping " ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

959 
string_of_int skipped ^ " scope" ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

960 
plural_s skipped ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

961 
". (Consider using \"mono\" or \ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

962 
\\"merge_type_vars\" to prevent this.)") 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

963 
else 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

964 
() 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

965 
val _ = scopes := the_scopes 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

966 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

967 
fun run_batches _ _ [] 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

968 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  969 
if donno > 0 andalso max_genuine > 0 then 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

970 
(print_m (fn () => excipit "checked"); "unknown") 
33192  971 
else if max_genuine = original_max_genuine then 
972 
if max_potential = original_max_potential then 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

973 
(print_m (fn () => 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

974 
"Nitpick found no " ^ das_wort_model ^ "." ^ 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

975 
(if not standard andalso likely_in_struct_induct_step then 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

976 
" This suggests that the induction hypothesis might be \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

977 
\general enough to prove this subgoal." 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

978 
else 
37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

979 
"")); if skipped > 0 then "unknown" else "none") 
33192  980 
else 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

981 
(print_m (fn () => 
38123
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

982 
excipit ("could not find a" ^ 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

983 
(if max_genuine = 1 then 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

984 
" better " ^ das_wort_model ^ "." 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

985 
else 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

986 
"ny better " ^ das_wort_model ^ "s.") ^ 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

987 
" It checked")); 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

988 
"potential") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

989 
else if found_really_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

990 
"genuine" 
33192  991 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

992 
"quasi_genuine" 
33192  993 
 run_batches j n (batch :: batches) z = 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

994 
let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in 
33192  995 
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z 
996 
end 

997 

998 
val batches = batch_list batch_size (!scopes) 

999 
val outcome_code = 

40411
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

1000 
run_batches 0 (length batches) batches 
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

1001 
(false, max_potential, max_genuine, 0) 
33192  1002 
handle TimeLimit.TimeOut => 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

1003 
(print_m (fn () => excipit "ran out of time after checking"); 
33192  1004 
if !met_potential > 0 then "potential" else "unknown") 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1005 
val _ = print_v (fn () => 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1006 
"Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1007 
".") 
33192  1008 
in (outcome_code, !state_ref) end 
1009 

41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1010 
(* Give the inner timeout a chance. *) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1011 
val timeout_bonus = seconds 1.0 
41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1012 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1013 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

1014 
step subst assm_ts orig_t = 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1015 
let val print_m = if auto then K () else Output.urgent_message in 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1016 
if getenv "KODKODI" = "" then 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1017 
(* The "expect" argument is deliberately ignored if Kodkodi is missing so 
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1018 
that the "Nitpick_Examples" can be processed on any machine. *) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1019 
(print_m (Pretty.string_of (plazy install_kodkodi_message)); 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1020 
("no_kodkodi", state)) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1021 
else 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1022 
let 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1023 
val unknown_outcome = ("unknown", state) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1024 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1025 
val outcome as (outcome_code, _) = 
41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1026 
time_limit (if debug orelse is_none timeout then NONE 
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1027 
else SOME (Time.+ (the timeout, timeout_bonus))) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1028 
(pick_them_nits_in_term deadline state params auto i n step subst 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

1029 
assm_ts) orig_t 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1030 
handle TOO_LARGE (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1031 
(print_m ("Limit reached: " ^ details ^ "."); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1032 
 TOO_SMALL (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1033 
(print_m ("Limit reached: " ^ details ^ "."); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1034 
 Kodkod.SYNTAX (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1035 
(print_m ("Malformed Kodkodi output: " ^ details ^ "."); 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1036 
unknown_outcome) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1037 
 TimeLimit.TimeOut => 
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1038 
(print_m "Nitpick ran out of time."; unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1039 
in 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1040 
if expect = "" orelse outcome_code = expect then outcome 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1041 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1042 
end 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1043 
end 
33192  1044 

35335  1045 
fun is_fixed_equation fixes 
1046 
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = 

1047 
member (op =) fixes s 

1048 
 is_fixed_equation _ _ = false 

1049 
fun extract_fixed_frees ctxt (assms, t) = 

1050 
let 

1051 
val fixes = Variable.fixes_of ctxt > map snd 

1052 
val (subst, other_assms) = 

1053 
List.partition (is_fixed_equation fixes) assms 

1054 
>> map Logic.dest_equals 

1055 
in (subst, other_assms, subst_atomic subst t) end 

1056 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1057 
fun pick_nits_in_subgoal state params auto i step = 
33192  1058 
let 
1059 
val ctxt = Proof.context_of state 

33292  1060 
val t = state > Proof.raw_goal > #goal > prop_of 
33192  1061 
in 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1062 
case Logic.count_prems t of 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39361
diff
changeset

1063 
0 => (Output.urgent_message "No subgoal!"; ("none", state)) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1064 
 n => 
33192  1065 
let 
36406  1066 
val t = Logic.goal_params t i > fst 
33192  1067 
val assms = map term_of (Assumption.all_assms_of ctxt) 
35335  1068 
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) 
1069 
in pick_nits_in_term state params auto i n step subst assms t end 

33192  1070 
end 
1071 

1072 
end; 