author  blanchet 
Tue, 23 Feb 2010 19:10:25 +0100  
changeset 35335  f715cfde056a 
parent 35334  b83b9f2a4b92 
child 35384  88dbcfe75c45 
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 
33192  11 
type params = { 
12 
cards_assigns: (typ option * int list) list, 

13 
maxes_assigns: (styp option * int list) list, 

14 
iters_assigns: (styp option * int list) list, 

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

15 
bitss: int list, 
33192  16 
bisim_depths: int list, 
17 
boxes: (typ option * bool option) list, 

18 
monos: (typ option * bool option) list, 

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

19 
stds: (typ option * bool) list, 
33192  20 
wfs: (styp option * bool option) list, 
21 
sat_solver: string, 

22 
blocking: bool, 

23 
falsify: bool, 

24 
debug: bool, 

25 
verbose: bool, 

26 
overlord: bool, 

27 
user_axioms: bool option, 

28 
assms: bool, 

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

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

30 
binary_ints: bool option, 
33192  31 
destroy_constrs: bool, 
32 
specialize: bool, 

33 
skolemize: bool, 

34 
star_linear_preds: bool, 

35 
uncurry: bool, 

36 
fast_descrs: bool, 

37 
peephole_optim: bool, 

38 
timeout: Time.time option, 

39 
tac_timeout: Time.time option, 

40 
sym_break: int, 

41 
sharing_depth: int, 

42 
flatten_props: bool, 

43 
max_threads: int, 

44 
show_skolems: bool, 

45 
show_datatypes: bool, 

46 
show_consts: bool, 

47 
evals: term list, 

48 
formats: (term option * int list) list, 

49 
max_potential: int, 

50 
max_genuine: int, 

51 
check_potential: bool, 

52 
check_genuine: bool, 

53 
batch_size: int, 

54 
expect: string} 

55 

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

57 
val unregister_frac_type : string > theory > theory 

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

59 
val unregister_codatatype : typ > theory > theory 

60 
val pick_nits_in_term : 

35335  61 
Proof.state > params > bool > int > int > int > (term * term) list 
62 
> term list > term > string * Proof.state 

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

64 
Proof.state > params > bool > int > int > string * Proof.state 
33192  65 
end; 
66 

67 
structure Nitpick : NITPICK = 

68 
struct 

69 

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

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

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

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

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

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

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

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

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

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

79 
open Nitpick_Model 
33192  80 

34126  81 
structure KK = Kodkod 
82 

33192  83 
type params = { 
84 
cards_assigns: (typ option * int list) list, 

85 
maxes_assigns: (styp option * int list) list, 

86 
iters_assigns: (styp option * int list) list, 

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

87 
bitss: int list, 
33192  88 
bisim_depths: int list, 
89 
boxes: (typ option * bool option) list, 

90 
monos: (typ option * bool option) list, 

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

91 
stds: (typ option * bool) list, 
33192  92 
wfs: (styp option * bool option) list, 
93 
sat_solver: string, 

94 
blocking: bool, 

95 
falsify: bool, 

96 
debug: bool, 

97 
verbose: bool, 

98 
overlord: bool, 

99 
user_axioms: bool option, 

100 
assms: bool, 

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

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

102 
binary_ints: bool option, 
33192  103 
destroy_constrs: bool, 
104 
specialize: bool, 

105 
skolemize: bool, 

106 
star_linear_preds: bool, 

107 
uncurry: bool, 

108 
fast_descrs: bool, 

109 
peephole_optim: bool, 

110 
timeout: Time.time option, 

111 
tac_timeout: Time.time option, 

112 
sym_break: int, 

113 
sharing_depth: int, 

114 
flatten_props: bool, 

115 
max_threads: int, 

116 
show_skolems: bool, 

117 
show_datatypes: bool, 

118 
show_consts: bool, 

119 
evals: term list, 

120 
formats: (term option * int list) list, 

121 
max_potential: int, 

122 
max_genuine: int, 

123 
check_potential: bool, 

124 
check_genuine: bool, 

125 
batch_size: int, 

126 
expect: string} 

127 

128 
type problem_extension = { 

129 
free_names: nut list, 

130 
sel_names: nut list, 

131 
nonsel_names: nut list, 

132 
rel_table: nut NameTable.table, 

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

133 
unsound: bool, 
33192  134 
scope: scope, 
34126  135 
core: KK.formula, 
136 
defs: KK.formula list} 

33192  137 

34126  138 
type rich_problem = KK.problem * problem_extension 
33192  139 

140 
(* Proof.context > string > term list > Pretty.T list *) 

141 
fun pretties_for_formulas _ _ [] = [] 

142 
 pretties_for_formulas ctxt s ts = 

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

144 
Pretty.indent indent_size (Pretty.chunks 

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

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

149 
(length ts downto 1) ts))] 

150 

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

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

152 
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

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

154 
\the package from Isabelle's web page and add the \"kodkodix.y.z\" \ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

155 
\directory's full path to \"" ^ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

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

159 

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

160 
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

161 
val max_unsound_delay_percent = 2 
33192  162 

163 
(* Time.time option > int *) 

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

164 
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

165 
 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

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

168 
* max_unsound_delay_percent div 100)) 
33192  169 

170 
(* Time.time option > bool *) 

171 
fun passed_deadline NONE = false 

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

173 

174 
(* ('a * bool option) list > bool *) 

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

175 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  176 

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

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

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

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

180 
(* typ > bool *) 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

181 
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

182 
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

183 
 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

184 
(* term > bool *) 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

185 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  186 

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

187 
(* (unit > string) > Pretty.T *) 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

188 
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

189 

35335  190 
(* Time.time > Proof.state > params > bool > int > int > int 
191 
> (term * term) list > term list > term > string * Proof.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

192 
fun pick_them_nits_in_term deadline state (params : params) auto i n step 
35335  193 
subst orig_assm_ts orig_t = 
33192  194 
let 
195 
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

196 
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

197 
val ctxt = Proof.context_of 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

198 
(* FIXME: reintroduce code before new release 
34039
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

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

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

201 
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

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

203 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

204 
boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

205 
user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

206 
specialize, skolemize, star_linear_preds, uncurry, fast_descrs, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

207 
peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

208 
max_threads, show_skolems, show_datatypes, show_consts, evals, formats, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

209 
max_potential, max_genuine, check_potential, check_genuine, batch_size, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

210 
...} = 
33192  211 
params 
212 
val state_ref = Unsynchronized.ref state 

213 
(* Pretty.T > unit *) 

214 
val pprint = 

215 
if auto then 

216 
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

217 
o Pretty.chunks o cons (Pretty.str "") o single 
33192  218 
o Pretty.mark Markup.hilite 
219 
else 

220 
priority o Pretty.string_of 

221 
(* (unit > Pretty.T) > unit *) 

222 
fun pprint_m f = () > not auto ? pprint o f 

223 
fun pprint_v f = () > verbose ? pprint o f 

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

225 
(* string > unit *) 

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

227 
(* (unit > string) > unit *) 

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

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

229 
val print_v = pprint_v o K o plazy 
33192  230 

231 
(* unit > unit *) 

232 
fun check_deadline () = 

233 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut 

234 
else () 

235 
(* unit > 'a *) 

236 
fun do_interrupted () = 

237 
if passed_deadline deadline then raise TimeLimit.TimeOut 

238 
else raise Interrupt 

239 

35335  240 
val orig_assm_ts = if assms orelse auto then orig_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

241 
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

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

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

244 
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

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

246 
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

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

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

249 
else 
35181
92d857a4e5e0
synchronize Nitpick's wellfoundedness formulas caching
blanchet
parents:
35177
diff
changeset

250 
"goal")) [Logic.list_implies (orig_assm_ts, orig_t)])) 
33192  251 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) 
252 
else orig_t 

35335  253 
val assms_t = Logic.mk_conjunction_list (neg_t :: orig_assm_ts) 
33192  254 
val (assms_t, evals) = 
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

255 
assms_t :: evals > merge_type_vars ? merge_type_vars_in_terms 
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

256 
> pairf hd tl 
33192  257 
val original_max_potential = max_potential 
258 
val original_max_genuine = max_genuine 

259 
(* 

260 
val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t) 

261 
val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t)) 

262 
orig_assm_ts 

263 
*) 

264 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

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

265 
val case_names = case_const_names thy stds 
35335  266 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst 
267 
val def_table = const_def_table ctxt subst defs 

33192  268 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 
35335  269 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
270 
val psimp_table = const_psimp_table ctxt subst 

271 
val intro_table = inductive_intro_table ctxt subst def_table 

33192  272 
val ground_thm_table = ground_theorem_table thy 
273 
val ersatz_table = ersatz_table thy 

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

274 
val (hol_ctxt as {wf_cache, ...}) = 
33192  275 
{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

276 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

277 
binary_ints = binary_ints, destroy_constrs = destroy_constrs, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

278 
specialize = specialize, skolemize = skolemize, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

279 
star_linear_preds = star_linear_preds, uncurry = uncurry, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

280 
fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

281 
case_names = case_names, def_table = def_table, 
33192  282 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
283 
simp_table = simp_table, psimp_table = psimp_table, 

284 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

285 
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], 

286 
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

287 
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

288 
constr_cache = Unsynchronized.ref []} 
33192  289 
val frees = Term.add_frees assms_t [] 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

290 
val _ = null (Term.add_tvars assms_t []) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

291 
raise NOT_SUPPORTED "schematic type variables" 
33192  292 
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

293 
core_t, binarize) = preprocess_term hol_ctxt assms_t 
33192  294 
val got_all_user_axioms = 
295 
got_all_mono_user_axioms andalso no_poly_user_axioms 

296 

297 
(* styp * (bool * bool) > unit *) 

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

299 
pprint (Pretty.blk (0, 

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

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

302 
pstrs (if wf then 

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

304 
\efficiently." 

305 
else 

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

307 
\unroll it."))) 

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

309 
val _ = 

310 
pprint_d (fn () => 

311 
Pretty.chunks 

312 
(pretties_for_formulas ctxt "Preprocessed formula" [core_t] @ 

313 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 

314 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 

315 
nondef_ts)) 

316 
val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts) 

317 
handle TYPE (_, Ts, ts) => 

318 
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) 

319 

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

320 
val core_u = nut_from_term hol_ctxt Eq core_t 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

321 
val def_us = map (nut_from_term hol_ctxt DefEq) def_ts 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

322 
val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

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

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

325 
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

326 
List.partition (is_sel o nickname_of) const_names 
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

327 
val genuine_means_genuine = got_all_user_axioms andalso none_true wfs 
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

328 
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

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

330 
val _ = List.app (priority o string_for_nut ctxt) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

331 
(core_u :: def_us @ nondef_us) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

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

333 

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

334 
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns 
33192  335 
(* typ > bool *) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

336 
fun is_type_always_monotonic T = 
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

337 
(is_datatype thy stds T andalso not (is_quot_type thy T) andalso 
34938  338 
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

339 
is_number_type thy T orelse is_bit_type T 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

340 
fun is_type_monotonic T = 
33192  341 
unique_scope orelse 
342 
case triple_lookup (type_match thy) monos T of 

343 
SOME (SOME b) => b 

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

344 
 _ => is_type_always_monotonic T orelse 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

345 
formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

346 
fun is_deep_datatype T = 
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

347 
is_datatype thy stds T andalso 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

348 
(not standard orelse T = nat_T orelse is_word_type T orelse 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

349 
exists (curry (op =) T o domain_type o type_of) sel_names) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

350 
val all_Ts = ground_types_in_terms hol_ctxt binarize 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

351 
(core_t :: def_ts @ nondef_ts) 
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

352 
> sort TermOrd.typ_ord 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

353 
val _ = if verbose andalso binary_ints = SOME true andalso 
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

354 
exists (member (op =) [nat_T, int_T]) all_Ts then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

355 
print_v (K "The option \"binary_ints\" will be ignored because \ 
34126  356 
\of the presence of rationals, reals, \"Suc\", \ 
357 
\\"gcd\", or \"lcm\" in the problem.") 

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

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

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

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

362 
if verbose andalso not unique_scope then 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

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

365 
 interesting_mono_Ts => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

366 
print_v (fn () => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

368 
val ss = map (quote o string_for_type ctxt) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

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

371 
"The type" ^ plural_s_for_list ss ^ " " ^ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

372 
space_implode " " (serial_commas "and" ss) ^ " " ^ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

373 
(if none_true monos then 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

374 
"passed the monotonicity test" 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

376 
(if length ss = 1 then "is" else "are") ^ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

377 
" considered monotonic") ^ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

378 
". Nitpick might be able to skip some scopes." 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

379 
end) 
33192  380 
else 
381 
() 

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

382 
val deep_dataTs = filter is_deep_datatype all_Ts 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

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

384 
provide a hint to the user. *) 
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

385 
(* string * (Rule_Cases.T * bool) > bool *) 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

398 
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

399 
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

400 
() 
33192  401 
(* 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

402 
val _ = priority "Monotonic types:" 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

403 
val _ = List.app (priority o string_for_type ctxt) mono_Ts 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

404 
val _ = priority "Nonmonotonic types:" 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

405 
val _ = List.app (priority o string_for_type ctxt) nonmono_Ts 
33192  406 
*) 
407 

408 
val need_incremental = Int.max (max_potential, max_genuine) >= 2 

409 
val effective_sat_solver = 

410 
if sat_solver <> "smart" then 

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

411 
if need_incremental andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

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

416 
"SAT4J") 

417 
else 

418 
sat_solver 

419 
else 

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

420 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  421 
val _ = 
422 
if sat_solver = "smart" then 

423 
print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^ 

424 
". The following" ^ 

425 
(if need_incremental then " incremental " else " ") ^ 

426 
"solvers are configured: " ^ 

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

427 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  428 
need_incremental)) ^ ".") 
429 
else 

430 
() 

431 

432 
val too_big_scopes = Unsynchronized.ref [] 

433 

434 
(* bool > scope > rich_problem option *) 

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

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

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

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

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

441 
\problem_for_scope", "too large scope") 
33192  442 
(* 
443 
val _ = priority "Offsets:" 

444 
val _ = List.app (fn (T, j0) => 

445 
priority (string_for_type ctxt T ^ " = " ^ 

446 
string_of_int j0)) 

447 
(Typtab.dest ofs) 

448 
*) 

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

449 
val all_exact = forall (is_exact_type datatypes) all_Ts 
33192  450 
(* nut list > rep NameTable.table > nut list * rep NameTable.table *) 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

451 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  452 
val main_j0 = offset_of_type ofs bool_T 
453 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

454 
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

455 
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

456 
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

457 
"bad offsets") 
33192  458 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
459 
val (free_names, rep_table) = 

460 
choose_reps_for_free_vars scope free_names NameTable.empty 

461 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

462 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

463 
val min_highest_arity = 

464 
NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1 

465 
val min_univ_card = 

466 
NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table 

34126  467 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  468 
val _ = check_arity min_univ_card min_highest_arity 
469 

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

470 
val core_u = choose_reps_in_nut scope unsound rep_table false core_u 
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

471 
val def_us = map (choose_reps_in_nut scope unsound rep_table true) 
33192  472 
def_us 
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

473 
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) 
33192  474 
nondef_us 
33745  475 
(* 
33192  476 
val _ = List.app (priority o string_for_nut ctxt) 
477 
(free_names @ sel_names @ nonsel_names @ 

478 
core_u :: def_us @ nondef_us) 

33745  479 
*) 
33192  480 
val (free_rels, pool, rel_table) = 
481 
rename_free_vars free_names initial_pool NameTable.empty 

482 
val (sel_rels, pool, rel_table) = 

483 
rename_free_vars sel_names pool rel_table 

484 
val (other_rels, pool, rel_table) = 

485 
rename_free_vars nonsel_names pool rel_table 

486 
val core_u = rename_vars_in_nut pool rel_table core_u 

487 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 

488 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 

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

489 
val core_f = kodkod_formula_from_nut ofs kk core_u 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

490 
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

491 
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us 
33192  492 
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f 
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

493 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
33192  494 
PrintMode.setmp [] multiline_string_for_scope scope 
34998  495 
val kodkod_sat_solver = 
35177  496 
Kodkod_SAT.sat_solver_spec effective_sat_solver > snd 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

497 
val bit_width = if bits = 0 then 16 else bits + 1 
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

498 
val delay = if unsound then 
33192  499 
Option.map (fn time => Time. (time, Time.now ())) 
500 
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

501 
> unsound_delay_for_timeout 
33192  502 
else 
503 
0 

504 
val settings = [("solver", commas (map quote kodkod_sat_solver)), 

505 
("skolem_depth", "1"), 

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

506 
("bit_width", string_of_int bit_width), 
33192  507 
("symmetry_breaking", signed_string_of_int sym_break), 
508 
("sharing", signed_string_of_int sharing_depth), 

509 
("flatten", Bool.toString flatten_props), 

510 
("delay", signed_string_of_int delay)] 

511 
val plain_rels = free_rels @ other_rels 

512 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

513 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

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

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

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

516 
declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

517 
rel_table datatypes 
33192  518 
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

519 
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

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

521 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
33192  522 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 
523 
univ_card nat_card int_card main_j0 formula 

524 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

525 
> not debug ? merge_bounds 

526 
val highest_arity = 

527 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

528 
val formula = fold_rev s_and declarative_axioms formula 

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

529 
val _ = if bits = 0 then () else check_bits bits formula 
34126  530 
val _ = if formula = KK.False then () 
33192  531 
else check_arity univ_card highest_arity 
532 
in 

533 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

534 
tuple_assigns = [], bounds = bounds, 

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

535 
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

536 
else pow_of_two_int_bounds bits main_j0, 
33192  537 
expr_assigns = [], formula = formula}, 
538 
{free_names = free_names, sel_names = sel_names, 

539 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

540 
unsound = unsound, scope = scope, core = core_f, 
33192  541 
defs = nondef_fs @ def_fs @ declarative_axioms}) 
542 
end 

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

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

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

545 
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

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

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

548 
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

549 
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

550 
ofs = Typtab.empty} 
33192  551 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
552 
\problem_for_scope" then 

553 
NONE 

554 
else 

555 
(Unsynchronized.change too_big_scopes (cons scope); 

556 
print_v (fn () => ("Limit reached: " ^ msg ^ 

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

557 
". Skipping " ^ (if unsound then "potential" 
33192  558 
else "genuine") ^ 
559 
" component of scope.")); 

560 
NONE) 

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

561 
 TOO_SMALL (_, msg) => 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

562 
(print_v (fn () => ("Limit reached: " ^ msg ^ 
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

563 
". Skipping " ^ (if unsound then "potential" 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

564 
else "genuine") ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

566 
NONE) 
33192  567 

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

568 
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

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

570 
> not standard ? prefix "nonstandard " 
33192  571 

572 
val scopes = Unsynchronized.ref [] 

573 
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

574 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  575 
val checked_problems = Unsynchronized.ref (SOME []) 
576 
val met_potential = Unsynchronized.ref 0 

577 

578 
(* rich_problem list > int list > unit *) 

579 
fun update_checked_problems problems = 

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

581 
o nth problems) 

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

582 
(* string > unit *) 
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

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

584 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  585 

34126  586 
(* bool > KK.raw_bound list > problem_extension > bool option *) 
33192  587 
fun print_and_check_model genuine bounds 
588 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

589 
: problem_extension) = 

590 
let 

591 
val (reconstructed_model, codatatypes_ok) = 

592 
reconstruct_hol_model {show_skolems = show_skolems, 

593 
show_datatypes = show_datatypes, 

594 
show_consts = show_consts} 

595 
scope formats frees free_names sel_names nonsel_names rel_table 

596 
bounds 

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

597 
val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok 
33192  598 
in 
599 
pprint (Pretty.chunks 

600 
[Pretty.blk (0, 

601 
(pstrs ("Nitpick found a" ^ 

602 
(if not genuine then " potential " 

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

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

604 
else " likely genuine ") ^ das_wort_model) @ 
33192  605 
(case pretties_for_scope scope verbose of 
606 
[] => [] 

607 
 pretties => pstrs " for " @ pretties) @ 

608 
[Pretty.str ":\n"])), 

609 
Pretty.indent indent_size reconstructed_model]); 

610 
if genuine 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

611 
(if check_genuine andalso standard then 
33192  612 
(case prove_hol_model scope tac_timeout free_names sel_names 
613 
rel_table bounds assms_t of 

614 
SOME true => print ("Confirmation by \"auto\": The above " ^ 

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

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

617 
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

618 
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

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

620 
\happen.\nPlease send a bug report to blanchet\ 
33192  621 
\te@in.tum.de.") 
622 
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

623 
print ("Refutation by \"auto\": The above " ^ das_wort_model ^ 
33192  624 
" is spurious.") 
625 
 NONE => print "No confirmation by \"auto\".") 

626 
else 

627 
(); 

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

628 
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

629 
print "The existence of a nonstandard model suggests that the \ 
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

630 
\induction hypothesis is not general enough or perhaps even \ 
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

631 
\wrong. See the \"Inductive Properties\" section of the \ 
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

632 
\Nitpick manual for details (\"isabelle doc nitpick\")." 
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

633 
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

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

635 
if has_syntactic_sorts orig_t then 
33192  636 
print "Hint: Maybe you forgot a type constraint?" 
637 
else 

638 
(); 

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

639 
if not genuine_means_genuine then 
33192  640 
if no_poly_user_axioms then 
641 
let 

642 
val options = 

643 
[] > not got_all_mono_user_axioms 

644 
? cons ("user_axioms", "\"true\"") 

645 
> not (none_true wfs) 

646 
? cons ("wf", "\"smart\" or \"false\"") 

647 
> not codatatypes_ok 

648 
? cons ("bisim_depth", "a nonnegative value") 

649 
val ss = 

650 
map (fn (name, value) => quote name ^ " set to " ^ value) 

651 
options 

652 
in 

653 
print ("Try again with " ^ 

654 
space_implode " " (serial_commas "and" ss) ^ 

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

655 
" to confirm that the " ^ 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

656 
" is genuine.") 
33192  657 
end 
658 
else 

659 
print ("Nitpick is unable to guarantee the authenticity of \ 

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

660 
\the " ^ das_wort_model ^ " in the presence of \ 
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

661 
\polymorphic axioms.") 
33192  662 
else 
663 
(); 

664 
NONE) 

665 
else 

666 
if not genuine then 

667 
(Unsynchronized.inc met_potential; 

668 
if check_potential then 

669 
let 

670 
val status = prove_hol_model scope tac_timeout free_names 

671 
sel_names rel_table bounds assms_t 

672 
in 

673 
(case status of 

674 
SOME true => print ("Confirmation by \"auto\": The above " ^ 

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

675 
das_wort_model ^ " is genuine.") 
33192  676 
 SOME false => print ("Refutation by \"auto\": The above " ^ 
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

677 
das_wort_model ^ " is spurious.") 
33192  678 
 NONE => print "No confirmation by \"auto\"."); 
679 
status 

680 
end 

681 
else 

682 
NONE) 

683 
else 

684 
NONE 

685 
end 

686 
(* int > int > int > bool > rich_problem list > int * int * int *) 

687 
fun solve_any_problem max_potential max_genuine donno first_time problems = 

688 
let 

689 
val max_potential = Int.max (0, max_potential) 

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

34126  691 
(* bool > int * KK.raw_bound list > bool option *) 
33192  692 
fun print_and_check genuine (j, bounds) = 
693 
print_and_check_model genuine bounds (snd (nth problems j)) 

694 
val max_solutions = max_potential + max_genuine 

695 
> not need_incremental ? curry Int.min 1 

696 
in 

697 
if max_solutions <= 0 then 

698 
(0, 0, donno) 

699 
else 

34126  700 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
701 
(map fst problems) of 

702 
KK.NotInstalled => 

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

703 
(print_m install_kodkodi_message; 
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

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

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

706 
(update_checked_problems problems unsat_js; show_kodkod_warning s; 
33192  707 
(max_potential, max_genuine, donno)) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

708 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  709 
let 
710 
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

711 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  712 
in 
713 
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

714 
show_kodkod_warning s; 
33192  715 
if null con_ps then 
716 
let 

33955  717 
val num_genuine = take max_potential lib_ps 
33192  718 
> map (print_and_check false) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

719 
> filter (curry (op =) (SOME true)) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

720 
> length 
33192  721 
val max_genuine = max_genuine  num_genuine 
722 
val max_potential = max_potential 

723 
 (length lib_ps  num_genuine) 

724 
in 

725 
if max_genuine <= 0 then 

726 
(0, 0, donno) 

727 
else 

728 
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

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

730 
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

731 
probably can't be satisfied themselves. *) 
33192  732 
val co_js = 
733 
map (fn j => j  1) unsat_js 

734 
> filter (fn j => 

735 
j >= 0 andalso 

736 
scopes_equivalent 

737 
(#scope (snd (nth problems j))) 

738 
(#scope (snd (nth problems (j + 1))))) 

739 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

740 
unsat_js @ co_js) 

741 
val problems = 

742 
problems > filter_out_indices bye_js 

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

744 
? filter_out (#unsound o snd) 
33192  745 
in 
746 
solve_any_problem max_potential max_genuine donno false 

747 
problems 

748 
end 

749 
end 

750 
else 

751 
let 

33955  752 
val _ = take max_genuine con_ps 
33192  753 
> List.app (ignore o print_and_check true) 
754 
val max_genuine = max_genuine  length con_ps 

755 
in 

756 
if max_genuine <= 0 orelse not first_time then 

757 
(0, max_genuine, donno) 

758 
else 

759 
let 

760 
val bye_js = sort_distinct int_ord 

761 
(map fst sat_ps @ unsat_js) 

762 
val problems = 

763 
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

764 
> filter_out (#unsound o snd) 
33192  765 
in solve_any_problem 0 max_genuine donno false problems end 
766 
end 

767 
end 

34126  768 
 KK.TimedOut unsat_js => 
33192  769 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  770 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
771 
 KK.Interrupted (SOME unsat_js) => 

33192  772 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  773 
 KK.Error (s, unsat_js) => 
33192  774 
(update_checked_problems problems unsat_js; 
775 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

776 
(max_potential, max_genuine, donno + 1)) 

777 
end 

778 

779 
(* int > int > scope list > int * int * int > int * int * int *) 

780 
fun run_batch j n scopes (max_potential, max_genuine, donno) = 

781 
let 

782 
val _ = 

783 
if null scopes then 

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

785 
else if verbose then 

786 
pprint (Pretty.chunks 

787 
[Pretty.blk (0, 

788 
pstrs ((if n > 1 then 

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

790 
signed_string_of_int n ^ ": " 

791 
else 

792 
"") ^ 

793 
"Trying " ^ string_of_int (length scopes) ^ 

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

795 
Pretty.indent indent_size 

796 
(Pretty.chunks (map2 

797 
(fn j => fn scope => 

798 
Pretty.block ( 

799 
(case pretties_for_scope scope true of 

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

801 
 pretties => pretties) @ 

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

803 
(length scopes downto 1) scopes))]) 

804 
else 

805 
() 

806 
(* scope * bool > rich_problem list * bool 

807 
> rich_problem list * bool *) 

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

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

810 
case problem_for_scope unsound scope of 
33192  811 
SOME problem => 
812 
(problems 

813 
> (null problems orelse 

34126  814 
not (KK.problems_equivalent (fst problem) 
815 
(fst (hd problems)))) 

33192  816 
? cons problem, donno) 
817 
 NONE => (problems, donno + 1)) 

818 
val (problems, donno) = 

819 
fold add_problem_for_scope 

820 
(map_product pair scopes 

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

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

823 
([], donno) 

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

825 
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

826 
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

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

833 
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

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

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

836 
"Warning: The conjecture either trivially holds for the \ 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

837 
\given scopes or (more likely) lies outside Nitpick's \ 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

838 
\supported 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

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

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

841 
" Only potential counterexamples may be found." 
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

842 
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

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

844 
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

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

846 
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

847 
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

848 
() 
33192  849 
in 
850 
solve_any_problem max_potential max_genuine donno true (rev problems) 

851 
end 

852 

853 
(* rich_problem list > scope > int *) 

854 
fun scope_count (problems : rich_problem list) scope = 

855 
length (filter (scopes_equivalent scope o #scope o snd) problems) 

856 
(* string > string *) 

857 
fun excipit did_so_and_so = 

858 
let 

859 
(* rich_problem list > rich_problem list *) 

860 
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

861 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  862 
else I 
863 
val total = length (!scopes) 

864 
val unsat = 

865 
fold (fn scope => 

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

867 
0 => I 

868 
 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

869 
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

870 
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

871 
? Integer.add 1) (!generated_scopes) 0 
33192  872 
in 
873 
"Nitpick " ^ did_so_and_so ^ 

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

875 
" after checking " ^ 

876 
string_of_int (Int.min (total  1, unsat)) ^ " of " ^ 

877 
string_of_int total ^ " scope" ^ plural_s total 

878 
else 

879 
"") ^ "." 

880 
end 

881 

34126  882 
(* int > int > scope list > int * int * int > KK.outcome *) 
33192  883 
fun run_batches _ _ [] (max_potential, max_genuine, donno) = 
884 
if donno > 0 andalso max_genuine > 0 then 

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

885 
(print_m (fn () => excipit "ran out of some resource"); "unknown") 
33192  886 
else if max_genuine = original_max_genuine then 
887 
if max_potential = original_max_potential then 

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

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

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

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

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

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

893 
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

894 
"")); "none") 
33192  895 
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

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

897 
"Nitpick could not find a" ^ 
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

898 
(if max_genuine = 1 then " better " ^ 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

899 
else "ny better " ^ das_wort_model ^ "s.")); "potential") 
33192  900 
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

901 
if genuine_means_genuine then "genuine" else "likely_genuine" 
33192  902 
 run_batches j n (batch :: batches) z = 
903 
let val (z as (_, max_genuine, _)) = run_batch j n batch z in 

904 
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z 

905 
end 

906 

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

907 
val (skipped, the_scopes) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

908 
all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

909 
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs 
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

910 
val _ = if skipped > 0 then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

911 
print_m (fn () => "Too many scopes. Skipping " ^ 
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

912 
string_of_int skipped ^ " scope" ^ 
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

913 
plural_s skipped ^ 
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

914 
". (Consider using \"mono\" or \ 
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

915 
\\"merge_type_vars\" to prevent this.)") 
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

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

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

918 
val _ = scopes := the_scopes 
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

919 

33192  920 
val batches = batch_list batch_size (!scopes) 
921 
val outcome_code = 

922 
(run_batches 0 (length batches) batches (max_potential, max_genuine, 0) 

923 
handle Exn.Interrupt => do_interrupted ()) 

924 
handle TimeLimit.TimeOut => 

925 
(print_m (fn () => excipit "ran out of time"); 

926 
if !met_potential > 0 then "potential" else "unknown") 

927 
 Exn.Interrupt => if auto orelse debug then raise Interrupt 

928 
else error (excipit "was interrupted") 

929 
val _ = print_v (fn () => "Total time: " ^ 

930 
signed_string_of_int (Time.toMilliseconds 

931 
(Timer.checkRealTimer timer)) ^ " ms.") 

932 
in (outcome_code, !state_ref) end 

933 
handle Exn.Interrupt => 

934 
if auto orelse #debug params then 

935 
raise Interrupt 

936 
else 

937 
if passed_deadline deadline then 

938 
(priority "Nitpick ran out of time."; ("unknown", state)) 

939 
else 

940 
error "Nitpick was interrupted." 

941 

35335  942 
(* Proof.state > params > bool > int > int > int > (term * term) list 
943 
> term list > term > string * Proof.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

944 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n 
35335  945 
step subst orig_assm_ts orig_t = 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

948 
else warning (Pretty.string_of (plazy 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

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

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

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

952 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

953 
val outcome as (outcome_code, _) = 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

954 
time_limit (if debug then NONE else timeout) 
35335  955 
(pick_them_nits_in_term deadline state params auto i n step subst 
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

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

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

958 
if expect = "" orelse outcome_code = expect then outcome 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

959 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

960 
end 
33192  961 

35335  962 
(* string list > term > bool *) 
963 
fun is_fixed_equation fixes 

964 
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = 

965 
member (op =) fixes s 

966 
 is_fixed_equation _ _ = false 

967 
(* Proof.context > term list * term > (term * term) list * term list * term *) 

968 
fun extract_fixed_frees ctxt (assms, t) = 

969 
let 

970 
val fixes = Variable.fixes_of ctxt > map snd 

971 
val (subst, other_assms) = 

972 
List.partition (is_fixed_equation fixes) assms 

973 
>> map Logic.dest_equals 

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

975 

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

976 
(* Proof.state > params > bool > int > int > string * Proof.state *) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

977 
fun pick_nits_in_subgoal state params auto i step = 
33192  978 
let 
979 
val ctxt = Proof.context_of state 

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

982 
case Logic.count_prems t of 
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

983 
0 => (priority "No subgoal!"; ("none", state)) 
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

984 
 n => 
33192  985 
let 
35335  986 
val (t, frees) = Logic.goal_params t i 
987 
val t = subst_bounds (frees, t) 

33192  988 
val assms = map term_of (Assumption.all_assms_of ctxt) 
35335  989 
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) 
990 
in pick_nits_in_term state params auto i n step subst assms t end 

33192  991 
end 
992 

993 
end; 