author  blanchet 
Sun, 22 Apr 2012 14:16:46 +0200  
changeset 47670  24babc4b1925 
parent 47564  8074b18d8d76 
child 47715  04400144c6fc 
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 
43022  12 

47560  13 
datatype mode = Auto_Try  Try  Normal  TPTP 
43022  14 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

42 
peephole_optim: bool, 
38124  43 
datatype_sym_break: int, 
44 
kodkod_sym_break: int, 

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

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

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

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

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

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

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

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

52 
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

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

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

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

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

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

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

59 
expect: string} 
33192  60 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

61 
val genuineN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

62 
val quasi_genuineN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

63 
val potentialN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

64 
val noneN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

65 
val unknownN : string 
33192  66 
val register_frac_type : string > (string * string) list > theory > theory 
67 
val unregister_frac_type : string > theory > theory 

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

69 
val unregister_codatatype : typ > theory > theory 

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

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

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

72 
val unregister_term_postprocessor : typ > theory > theory 
33192  73 
val pick_nits_in_term : 
43022  74 
Proof.state > params > mode > int > int > int > (term * term) list 
35335  75 
> term list > term > string * Proof.state 
33192  76 
val pick_nits_in_subgoal : 
43022  77 
Proof.state > params > mode > int > int > string * Proof.state 
33192  78 
end; 
79 

80 
structure Nitpick : NITPICK = 

81 
struct 

82 

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

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

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

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

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

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

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

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

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

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

92 
open Nitpick_Model 
33192  93 

34126  94 
structure KK = Kodkod 
95 

47560  96 
datatype mode = Auto_Try  Try  Normal  TPTP 
97 

98 
fun is_mode_nt mode = (mode = Normal orelse mode = TPTP) 

43022  99 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

127 
peephole_optim: bool, 
38124  128 
datatype_sym_break: int, 
129 
kodkod_sym_break: int, 

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

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

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

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

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

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

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

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

137 
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

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

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

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

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

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

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

144 
expect: string} 
33192  145 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

146 
val genuineN = "genuine" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

147 
val quasi_genuineN = "quasi_genuine" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

148 
val potentialN = "potential" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

149 
val noneN = "none" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

150 
val unknownN = "unknown" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

151 

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

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

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

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

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

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

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

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

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

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

161 

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

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

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

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

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

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

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

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

169 

34126  170 
type rich_problem = KK.problem * problem_extension 
33192  171 

172 
fun pretties_for_formulas _ _ [] = [] 

173 
 pretties_for_formulas ctxt s ts = 

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

175 
Pretty.indent indent_size (Pretty.chunks 

176 
(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

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

180 
(length ts downto 1) ts))] 

181 

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

182 
fun install_java_message () = 
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
47108
diff
changeset

183 
"Nitpick requires Java Development Kit 1.6/1.7 via ISABELLE_JDK_HOME setting." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

184 
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

185 
"Nitpick requires the external Java program Kodkodi. To install it, download \ 
46243  186 
\the package from \"http://www21.in.tum.de/~blanchet/#software\" and add the \ 
187 
\\"kodkodix.y.z\" directory's full path to " ^ 

43602  188 
Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^ 
189 
" 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

190 

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

191 
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

192 
val max_unsound_delay_percent = 2 
33192  193 

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

194 
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

195 
 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

196 
Int.max (0, Int.min (max_unsound_delay_ms, 
33192  197 
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

198 
* max_unsound_delay_percent div 100)) 
33192  199 

200 
fun passed_deadline NONE = false 

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

202 

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

203 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  204 

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

205 
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

206 
$ (@{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

207 
 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

208 

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

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

210 
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46243
diff
changeset

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

212 
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

213 
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

214 
 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

215 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  216 

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

217 
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

218 

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

220 
subst assm_ts orig_t = 
33192  221 
let 
222 
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

223 
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

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

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

226 

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

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

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

229 
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

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

231 
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

232 
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, 
38209  233 
verbose, overlord, user_axioms, assms, whacks, merge_type_vars, 
234 
binary_ints, destroy_constrs, specialize, star_linear_preds, 

41875  235 
total_consts, needs, peephole_optim, datatype_sym_break, 
41856  236 
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

237 
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

238 
max_genuine, check_potential, check_genuine, batch_size, ...} = params 
33192  239 
val state_ref = Unsynchronized.ref state 
46086  240 
fun pprint print = 
43022  241 
if mode = Auto_Try then 
33192  242 
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

243 
o Pretty.chunks o cons (Pretty.str "") o single 
45666  244 
o Pretty.mark Isabelle_Markup.hilite 
33192  245 
else 
46086  246 
print o Pretty.string_of 
47559  247 
val pprint_a = pprint Output.urgent_message 
47560  248 
fun pprint_nt f = () > is_mode_nt mode ? pprint Output.urgent_message o f 
46086  249 
fun pprint_v f = () > verbose ? pprint Output.urgent_message o f 
250 
fun pprint_d f = () > debug ? pprint tracing o f 

251 
val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs 

47560  252 
fun print_t f = () > mode = TPTP ? print o f 
39345  253 
(* 
46086  254 
val print_g = pprint tracing o Pretty.str 
39345  255 
*) 
47560  256 
val print_nt = pprint_nt o K o plazy 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

257 
val print_v = pprint_v o K o plazy 
33192  258 

259 
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

260 
if passed_deadline deadline then raise TimeLimit.TimeOut else () 
33192  261 

43022  262 
val assm_ts = if assms orelse mode <> Normal 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

263 
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

264 
if step = 0 then 
47560  265 
print_nt (fn () => "Nitpicking formula...") 
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

266 
else 
47560  267 
pprint_nt (fn () => Pretty.chunks ( 
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

268 
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

269 
(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

270 
"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

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

272 
"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

273 
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

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

41876  277 
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

278 
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

279 
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

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

281 
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

282 
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

283 
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

284 
val evals = evals > map merge_tfrees 
41876  285 
val needs = needs > Option.map (map merge_tfrees) 
286 
val conj_ts = neg_t :: assm_ts @ evals @ these needs 

33192  287 
val original_max_potential = max_potential 
288 
val original_max_genuine = max_genuine 

289 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

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

290 
val case_names = case_const_names ctxt stds 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

291 
val defs = all_defs_of thy subst 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

292 
val nondefs = all_nondefs_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

293 
val def_tables = const_def_tables ctxt subst defs 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

294 
val nondef_table = const_nondef_table nondefs 
35335  295 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
296 
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

297 
val choice_spec_table = const_choice_spec_table ctxt subst 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

298 
val nondefs = 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

299 
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

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

302 
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

303 
val hol_ctxt as {wf_cache, ...} = 
33192  304 
{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

305 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
38209  306 
whacks = whacks, binary_ints = binary_ints, 
307 
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

308 
star_linear_preds = star_linear_preds, total_consts = total_consts, 
41875  309 
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

310 
case_names = case_names, def_tables = def_tables, 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

311 
nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

312 
psimp_table = psimp_table, choice_spec_table = choice_spec_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

313 
intro_table = intro_table, ground_thm_table = ground_thm_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

314 
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

315 
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

316 
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

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

318 
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

319 
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

320 
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

321 
error "Nitpick cannot handle goals with schematic type variables." 
41875  322 
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

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

324 
preprocess_formulas hol_ctxt assm_ts neg_t 
33192  325 
val got_all_user_axioms = 
326 
got_all_mono_user_axioms andalso no_poly_user_axioms 

327 

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

47560  329 
pprint_nt (fn () => Pretty.blk (0, 
33192  330 
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"") 
331 
@ Syntax.pretty_term ctxt (Const x) :: 

332 
pstrs (if wf then 

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

334 
\efficiently." 

335 
else 

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

337 
\unroll it."))) 

338 
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

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

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

342 
(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

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

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

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

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

349 

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

350 
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

351 
val def_us = def_ts > map (nut_from_term hol_ctxt DefEq) 
41875  352 
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

353 
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

354 
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

355 
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

356 
List.partition (is_sel o nickname_of) const_names 
46114
e6d33b200f42
remove subtlety whose justification got lost in time  the new code is possibly less precise but sounder
blanchet
parents:
46103
diff
changeset

357 
val sound_finitizes = none_true 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

358 
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

359 
(* 
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

360 
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

361 
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

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

363 

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

364 
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

365 
fun monotonicity_message Ts extra = 
38188  366 
let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in 
367 
Pretty.blk (0, 

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

369 
pretty_serial_commas "and" pretties @ 

370 
pstrs (" " ^ 

42959  371 
(if none_true monos then 
372 
"passed the monotonicity test" 

373 
else 

374 
(if length pretties = 1 then "is" else "are") ^ 

375 
" considered monotonic") ^ 

376 
". " ^ extra)) 

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

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

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

379 
(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

380 
(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

381 
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

382 
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

383 
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

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

385 
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

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

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

388 
fun is_type_monotonic T = 
33192  389 
unique_scope orelse 
390 
case triple_lookup (type_match thy) monos T of 

391 
SOME (SOME b) => b 

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

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

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

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

395 
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

396 
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

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

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

399 
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

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

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

402 
fun is_datatype_deep T = 
46103
1e35730bd869
always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
blanchet
parents:
46086
diff
changeset

403 
not standard orelse T = @{typ unit} orelse T = nat_T orelse 
1e35730bd869
always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
blanchet
parents:
46086
diff
changeset

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

405 
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

406 
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) 
35408  407 
> sort Term_Ord.typ_ord 
38214  408 
val _ = 
409 
if verbose andalso binary_ints = SOME true andalso 

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

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

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

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

414 
else 

415 
() 

416 
val _ = 

43022  417 
if mode = Normal andalso 
38214  418 
exists (fn Type (@{type_name Datatype.node}, _) => true  _ => false) 
419 
all_Ts then 

47560  420 
print_nt (K ("Warning: The problem involves directly or indirectly the \ 
421 
\internal type " ^ quote @{type_name Datatype.node} ^ 

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

423 
\usually indicates either a failure of abstraction or a \ 

424 
\quirk in Nitpick.")) 

38214  425 
else 
426 
() 

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

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

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

430 
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

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

432 
 interesting_mono_Ts => 
38188  433 
pprint_v (K (monotonicity_message interesting_mono_Ts 
434 
"Nitpick might be able to skip some scopes.")) 

33192  435 
else 
436 
() 

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

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

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

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

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

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

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

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

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

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

446 
if verbose andalso not (null finitizable_dataTs) then 
38188  447 
pprint_v (K (monotonicity_message finitizable_dataTs 
448 
"Nitpick can use a more precise finite encoding.")) 

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

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

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

451 
(* 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

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

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

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

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

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

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

458 
val likely_in_struct_induct_step = 
42361  459 
exists is_struct_induct_step (Proof_Context.cases_of ctxt) 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

460 
val _ = if standard andalso likely_in_struct_induct_step then 
47560  461 
pprint_nt (fn () => Pretty.blk (0, 
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

462 
pstrs "Hint: To check that the induction hypothesis is \ 
35177  463 
\general enough, try this command: " @ 
45666  464 
[Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0, 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

465 
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

466 
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

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

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

470 
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

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

472 
val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts 
33192  473 
*) 
474 

36384  475 
val incremental = Int.max (max_potential, max_genuine) >= 2 
476 
val actual_sat_solver = 

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

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

480 
sat_solver) then 
47560  481 
(print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \ 
482 
\be used instead of " ^ quote sat_solver ^ ".")); 

33192  483 
"SAT4J") 
484 
else 

485 
sat_solver 

486 
else 

36384  487 
Kodkod_SAT.smart_sat_solver_name incremental 
33192  488 
val _ = 
489 
if sat_solver = "smart" then 

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

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

493 
"solvers are configured: " ^ 

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

33192  495 
else 
496 
() 

497 

498 
val too_big_scopes = Unsynchronized.ref [] 

499 

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

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

501 
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = 
33192  502 
let 
503 
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

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

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

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

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

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

511 
string_of_int j0)) 
33192  512 
(Typtab.dest ofs) 
513 
*) 

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

514 
val effective_total_consts = 
41856  515 
case total_consts of 
516 
SOME b => b 

517 
 NONE => forall (is_exact_type datatypes true) all_Ts 

33192  518 
val main_j0 = offset_of_type ofs bool_T 
519 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

520 
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

521 
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

522 
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

523 
"bad offsets") 
33192  524 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
525 
val (free_names, rep_table) = 

38170  526 
choose_reps_for_free_vars scope pseudo_frees free_names 
527 
NameTable.empty 

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

530 
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

531 
rep_table 
38182  532 
val (guiltiest_party, min_highest_arity) = 
533 
NameTable.fold (fn (name, R) => fn (s, n) => 

534 
let val n' = arity_of_rep R in 

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

536 
end) rep_table ("", 1) 

33192  537 
val min_univ_card = 
36384  538 
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table 
34126  539 
(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

540 
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

541 
else check_arity guiltiest_party min_univ_card min_highest_arity 
33192  542 

41802  543 
val def_us = 
544 
def_us > map (choose_reps_in_nut scope unsound rep_table true) 

545 
val nondef_us = 

546 
nondef_us > map (choose_reps_in_nut scope unsound rep_table false) 

41875  547 
val need_us = 
548 
need_us > map (choose_reps_in_nut scope unsound rep_table false) 

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

550 
val _ = List.app (print_g o string_for_nut ctxt) 
33192  551 
(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

552 
nondef_us @ def_us @ need_us) 
33745  553 
*) 
33192  554 
val (free_rels, pool, rel_table) = 
555 
rename_free_vars free_names initial_pool NameTable.empty 

556 
val (sel_rels, pool, rel_table) = 

557 
rename_free_vars sel_names pool rel_table 

558 
val (other_rels, pool, rel_table) = 

559 
rename_free_vars nonsel_names pool rel_table 

41802  560 
val nondef_us = nondef_us > map (rename_vars_in_nut pool rel_table) 
561 
val def_us = def_us > map (rename_vars_in_nut pool rel_table) 

41875  562 
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

563 
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

564 
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

565 
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

566 
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

567 
Print_Mode.setmp [] multiline_string_for_scope scope 
34998  568 
val kodkod_sat_solver = 
36384  569 
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

570 
val bit_width = if bits = 0 then 16 else bits + 1 
36384  571 
val delay = 
572 
if unsound then 

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

574 
> unsound_delay_for_timeout 

575 
else 

576 
0 

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

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

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

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

581 
("flatten", "false"), 
33192  582 
("delay", signed_string_of_int delay)] 
583 
val plain_rels = free_rels @ other_rels 

584 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

585 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

41995  586 
val need_vals = 
587 
map (fn dtype as {typ, ...} => 

588 
(typ, needed_values_for_datatype need_us ofs dtype)) datatypes 

589 
val sel_bounds = 

590 
map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels 

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

591 
val dtype_axioms = 
41995  592 
declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals 
41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

593 
datatype_sym_break bits ofs kk rel_table datatypes 
33192  594 
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

595 
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

596 
(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

597 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
38126  598 
val (built_in_bounds, built_in_axioms) = 
39345  599 
bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card 
600 
nat_card int_card main_j0 (formula :: declarative_axioms) 

33192  601 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 
602 
> not debug ? merge_bounds 

38126  603 
val axioms = built_in_axioms @ declarative_axioms 
33192  604 
val highest_arity = 
605 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

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

607 
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

608 
val _ = if debug orelse formula = KK.False then () 
38182  609 
else check_arity "" univ_card highest_arity 
33192  610 
in 
611 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

612 
tuple_assigns = [], bounds = bounds, 

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

613 
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

614 
else pow_of_two_int_bounds bits main_j0, 
33192  615 
expr_assigns = [], formula = formula}, 
616 
{free_names = free_names, sel_names = sel_names, 

617 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

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

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

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

622 
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

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

624 
{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

625 
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

626 
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

627 
ofs = Typtab.empty} 
33192  628 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
629 
\problem_for_scope" then 

630 
NONE 

631 
else 

632 
(Unsynchronized.change too_big_scopes (cons scope); 

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

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

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

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

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

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

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

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

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

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

643 
NONE) 
33192  644 

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

645 
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

646 
(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

647 
> not standard ? prefix "nonstandard " 
33192  648 

649 
val scopes = Unsynchronized.ref [] 

650 
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

651 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  652 
val checked_problems = Unsynchronized.ref (SOME []) 
653 
val met_potential = Unsynchronized.ref 0 

654 

655 
fun update_checked_problems problems = 

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

657 
o nth problems) 

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

658 
fun show_kodkod_warning "" = () 
47560  659 
 show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  660 

661 
fun print_and_check_model genuine bounds 

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

663 
: problem_extension) = 

664 
let 

665 
val (reconstructed_model, codatatypes_ok) = 

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

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

667 
{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

668 
show_consts = show_consts} 
38170  669 
scope formats atomss real_frees pseudo_frees free_names sel_names 
670 
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

671 
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

672 
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

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

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

675 
fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) 
33192  676 
in 
47560  677 
(print_t (fn () => 
678 
"% SZS status " ^ 

679 
(if genuine then 

680 
if falsify then "CounterSatisfiable" else "Satisfiable" 

681 
else 

682 
"Unknown") ^ "\n" ^ 

47562  683 
"% SZS output start FiniteModel"); 
47560  684 
pprint_a (Pretty.chunks 
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

685 
[Pretty.blk (0, 
43022  686 
(pstrs ((if mode = Auto_Try then "Auto " else "") ^ 
687 
"Nitpick found a" ^ 

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

688 
(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

689 
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

690 
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

691 
(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

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

693 
 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

694 
[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

695 
Pretty.indent indent_size reconstructed_model]); 
47564  696 
print_t (K "% SZS output end FiniteModel"); 
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

697 
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

698 
(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

699 
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

700 
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

701 
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

702 
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

703 
das_wort_model ^ " is really genuine.") 
33192  704 
 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

705 
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

706 
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

707 
\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

708 
\happen.\nPlease send a bug report to blanchet\ 
33192  709 
\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

710 
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

711 
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

712 
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

713 
 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

714 
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

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

716 
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

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

720 
\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

721 
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

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

723 
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

724 
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

725 
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

726 
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

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 
(); 
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 
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

730 
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

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 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

733 
[] > 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

734 
? 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

735 
> 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

736 
? 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

737 
> 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

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

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

740 
? 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

741 
> 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

742 
? 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

743 
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

744 
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

745 
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

746 
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

747 
print ("Try again with " ^ 
41872  748 
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

749 
" 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

750 
" 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

751 
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

752 
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

753 
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

754 
\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

755 
\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

756 
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

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

758 
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

759 
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

760 
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

761 
(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

762 
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

763 
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

764 
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

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

766 
(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

767 
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

768 
(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

769 
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

770 
\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

771 
" 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

772 
 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

773 
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

774 
 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

775 
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

776 
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

777 
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

778 
NONE) 
33192  779 
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

780 
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

781 
> pair genuine_means_genuine 
33192  782 
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

783 
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

784 
donno) first_time problems = 
33192  785 
let 
786 
val max_potential = Int.max (0, max_potential) 

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

788 
fun print_and_check genuine (j, bounds) = 

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

790 
val max_solutions = max_potential + max_genuine 

36384  791 
> not incremental ? Integer.min 1 
33192  792 
in 
793 
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

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

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

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

798 
KK.JavaNotInstalled => 
47560  799 
(print_nt install_java_message; 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

800 
(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

801 
 KK.JavaTooOld => 
47560  802 
(print_nt install_java_message; 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

803 
(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

804 
 KK.KodkodiNotInstalled => 
47560  805 
(print_nt 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

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

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

808 
(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

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

810 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  811 
let 
812 
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

813 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  814 
in 
815 
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

816 
show_kodkod_warning s; 
33192  817 
if null con_ps then 
818 
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

819 
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

820 
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

821 
> 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

822 
> 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

823 
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

824 
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

825 
val num_genuine = length genuine_codes 
33192  826 
val max_genuine = max_genuine  num_genuine 
827 
val max_potential = max_potential 

828 
 (length lib_ps  num_genuine) 

829 
in 

830 
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

831 
(found_really_genuine, 0, 0, donno) 
33192  832 
else 
833 
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

834 
(* "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

835 
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

836 
probably can't be satisfied themselves. *) 
33192  837 
val co_js = 
838 
map (fn j => j  1) unsat_js 

839 
> filter (fn j => 

840 
j >= 0 andalso 

841 
scopes_equivalent 

35814  842 
(#scope (snd (nth problems j)), 
843 
#scope (snd (nth problems (j + 1))))) 

33192  844 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 
845 
unsat_js @ co_js) 

846 
val problems = 

847 
problems > filter_out_indices bye_js 

848 
> 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

849 
? filter_out (#unsound o snd) 
33192  850 
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

851 
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

852 
max_genuine, donno) false problems 
33192  853 
end 
854 
end 

855 
else 

856 
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

857 
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

858 
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

859 
> 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

860 
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

861 
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

862 
found_really_genuine orelse exists fst genuine_codes 
33192  863 
in 
864 
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

865 
(found_really_genuine, 0, max_genuine, donno) 
33192  866 
else 
867 
let 

868 
val bye_js = sort_distinct int_ord 

869 
(map fst sat_ps @ unsat_js) 

870 
val problems = 

871 
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

872 
> 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

873 
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

874 
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

875 
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

876 
end 
33192  877 
end 
878 
end 

34126  879 
 KK.TimedOut unsat_js => 
33192  880 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  881 
 KK.Error (s, unsat_js) => 
33192  882 
(update_checked_problems problems unsat_js; 
883 
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

884 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  885 
end 
886 

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

887 
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

888 
donno) = 
33192  889 
let 
890 
val _ = 

891 
if null scopes then 

47560  892 
print_nt (K "The scope specification is inconsistent.") 
33192  893 
else if verbose then 
47560  894 
pprint_nt (fn () => Pretty.chunks 
33192  895 
[Pretty.blk (0, 
896 
pstrs ((if n > 1 then 

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

898 
signed_string_of_int n ^ ": " 

899 
else 

900 
"") ^ 

901 
"Trying " ^ string_of_int (length scopes) ^ 

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

903 
Pretty.indent indent_size 

904 
(Pretty.chunks (map2 

905 
(fn j => fn scope => 

906 
Pretty.block ( 

907 
(case pretties_for_scope scope true of 

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

909 
 pretties => pretties) @ 

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

911 
(length scopes downto 1) scopes))]) 

912 
else 

913 
() 

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

914 
fun add_problem_for_scope (scope, unsound) (problems, donno) = 
33192  915 
(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

916 
case problem_for_scope unsound scope of 
33192  917 
SOME problem => 
918 
(problems 

919 
> (null problems orelse 

35814  920 
not (KK.problems_equivalent (fst problem, fst (hd problems)))) 
33192  921 
? cons problem, donno) 
922 
 NONE => (problems, donno + 1)) 

923 
val (problems, donno) = 

924 
fold add_problem_for_scope 

925 
(map_product pair scopes 

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

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

928 
([], donno) 

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

930 
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

931 
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

932 
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

933 
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

934 
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

935 
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

936 
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

937 
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

938 
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

939 
sound_problems then 
47560  940 
print_nt (fn () => 
44395  941 
"Warning: The conjecture " ^ 
942 
(if falsify then "either trivially holds" 

943 
else "is either trivially unsatisfiable") ^ 

944 
" for the given scopes or lies outside Nitpick's supported \ 

35384  945 
\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

946 
(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

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

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

949 
"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

950 
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

951 
"")) 
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

952 
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

953 
() 
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

954 
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

955 
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

956 
() 
33192  957 
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

958 
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

959 
donno) true (rev problems) 
33192  960 
end 
961 

962 
fun scope_count (problems : rich_problem list) scope = 

35814  963 
length (filter (curry scopes_equivalent scope o #scope o snd) problems) 
33192  964 
fun excipit did_so_and_so = 
965 
let 

966 
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

967 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  968 
else I 
969 
val total = length (!scopes) 

970 
val unsat = 

971 
fold (fn scope => 

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

973 
0 => I 

974 
 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

975 
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

976 
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

977 
? Integer.add 1) (!generated_scopes) 0 
33192  978 
in 
47560  979 
(if mode = TPTP then "% SZS status Unknown\n" else "") ^ 
33192  980 
"Nitpick " ^ did_so_and_so ^ 
981 
(if is_some (!checked_problems) andalso total > 0 then 

39361  982 
" " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" 
983 
^ plural_s total 

33192  984 
else 
985 
"") ^ "." 

986 
end 

987 

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

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

989 
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

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

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

992 
val _ = if skipped > 0 then 
47560  993 
print_nt (fn () => "Too many scopes. Skipping " ^ 
994 
string_of_int skipped ^ " scope" ^ 

995 
plural_s skipped ^ 

996 
". (Consider using \"mono\" or \ 

997 
\\"merge_type_vars\" to prevent this.)") 

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

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

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

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

1001 

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

1002 
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

1003 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  1004 
if donno > 0 andalso max_genuine > 0 then 
47560  1005 
(print_nt (fn () => excipit "checked"); unknownN) 
33192  1006 
else if max_genuine = original_max_genuine then 
1007 
if max_potential = original_max_potential then 

47562  1008 
(print_t (K "% SZS status Unknown"); 
47560  1009 
print_nt (fn () => 
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

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

1011 
(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

1012 
" 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

1013 
\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

1014 
else 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1015 
"")); if skipped > 0 then unknownN else noneN) 
33192  1016 
else 
47560  1017 
(print_nt (fn () => 
38123
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

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

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

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

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

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

1023 
" It checked")); 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1024 
potentialN) 
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

1025 
else if found_really_genuine then 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1026 
genuineN 
33192  1027 
else 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1028 
quasi_genuineN 
33192  1029 
 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

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

1033 

1034 
val batches = batch_list batch_size (!scopes) 

1035 
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

1036 
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

1037 
(false, max_potential, max_genuine, 0) 
33192  1038 
handle TimeLimit.TimeOut => 
47560  1039 
(print_nt (fn () => excipit "ran out of time after checking"); 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1040 
if !met_potential > 0 then potentialN else unknownN) 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

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

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

1043 
".") 
33192  1044 
in (outcome_code, !state_ref) end 
1045 

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

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

1047 
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

1048 

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

1050 
step subst assm_ts orig_t = 
47670  1051 
let 
1052 
val print_nt = if is_mode_nt mode then Output.urgent_message else K () 

1053 
val print_t = if mode = TPTP then Output.urgent_message else K () 

1054 
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

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

1056 
(* 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

1057 
that the "Nitpick_Examples" can be processed on any machine. *) 
47560  1058 
(print_nt (Pretty.string_of (plazy install_kodkodi_message)); 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1059 
("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

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

1061 
let 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1062 
val unknown_outcome = (unknownN, 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

1063 
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

1064 
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

1065 
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

1066 
else SOME (Time.+ (the timeout, timeout_bonus))) 
43022  1067 
(pick_them_nits_in_term deadline state params mode i n step subst 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

1068 
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

1069 
handle TOO_LARGE (_, details) => 
47670  1070 
(print_t "% SZS status Unknown"; 
1071 
print_nt ("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

1072 
 TOO_SMALL (_, details) => 
47670  1073 
(print_t "% SZS status Unknown"; 
1074 
print_nt ("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

1075 
 Kodkod.SYNTAX (_, details) => 
47670  1076 
(print_t "% SZS status Unknown"; 
1077 
print_nt ("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

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

1079 
 TimeLimit.TimeOut => 
47670  1080 
(print_t "% SZS status TimedOut"; 
1081 
print_nt "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

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

1083 
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

1084 
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

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

1086 
end 
33192  1087 

42486  1088 
fun is_fixed_equation ctxt 
35335  1089 
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = 
42486  1090 
Variable.is_fixed ctxt s 
35335  1091 
 is_fixed_equation _ _ = false 
1092 
fun extract_fixed_frees ctxt (assms, t) = 

1093 
let 

1094 
val (subst, other_assms) = 

42486  1095 
List.partition (is_fixed_equation ctxt) assms 
35335  1096 
>> map Logic.dest_equals 
1097 
in (subst, other_assms, subst_atomic subst t) end 

1098 

43022  1099 
fun pick_nits_in_subgoal state params mode i step = 
33192  1100 
let 
1101 
val ctxt = Proof.context_of state 

33292  1102 
val t = state > Proof.raw_goal > #goal > prop_of 
33192  1103 
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

1104 
case Logic.count_prems t of 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

1105 
0 => (Output.urgent_message "No subgoal!"; (noneN, 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

1106 
 n => 
33192  1107 
let 
36406  1108 
val t = Logic.goal_params t i > fst 
33192  1109 
val assms = map term_of (Assumption.all_assms_of ctxt) 
35335  1110 
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) 
43022  1111 
in pick_nits_in_term state params mode i n step subst assms t end 
33192  1112 
end 
1113 

1114 
end; 