author  blanchet 
Fri, 18 Dec 2009 12:00:29 +0100  
changeset 34126  8a2c5d7aff51 
parent 34124  c4628a1dcf75 
child 34935  cb011ba38950 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2008, 2009 

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, 

19 
wfs: (styp option * bool option) list, 

20 
sat_solver: string, 

21 
blocking: bool, 

22 
falsify: bool, 

23 
debug: bool, 

24 
verbose: bool, 

25 
overlord: bool, 

26 
user_axioms: bool option, 

27 
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

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

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

32 
skolemize: bool, 

33 
star_linear_preds: bool, 

34 
uncurry: bool, 

35 
fast_descrs: bool, 

36 
peephole_optim: bool, 

37 
timeout: Time.time option, 

38 
tac_timeout: Time.time option, 

39 
sym_break: int, 

40 
sharing_depth: int, 

41 
flatten_props: bool, 

42 
max_threads: int, 

43 
show_skolems: bool, 

44 
show_datatypes: bool, 

45 
show_consts: bool, 

46 
evals: term list, 

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

48 
max_potential: int, 

49 
max_genuine: int, 

50 
check_potential: bool, 

51 
check_genuine: bool, 

52 
batch_size: int, 

53 
expect: string} 

54 

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

56 
val unregister_frac_type : string > theory > theory 

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

58 
val unregister_codatatype : typ > theory > theory 

59 
val pick_nits_in_term : 

60 
Proof.state > params > bool > term list > term > string * Proof.state 

61 
val pick_nits_in_subgoal : 

62 
Proof.state > params > bool > int > string * Proof.state 

63 
end; 

64 

65 
structure Nitpick : NITPICK = 

66 
struct 

67 

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

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

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

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

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

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

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

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

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

76 
open Nitpick_Model 
33192  77 

34126  78 
structure KK = Kodkod 
79 

33192  80 
type params = { 
81 
cards_assigns: (typ option * int list) list, 

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

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

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

84 
bitss: int list, 
33192  85 
bisim_depths: int list, 
86 
boxes: (typ option * bool option) list, 

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

88 
wfs: (styp option * bool option) list, 

89 
sat_solver: string, 

90 
blocking: bool, 

91 
falsify: bool, 

92 
debug: bool, 

93 
verbose: bool, 

94 
overlord: bool, 

95 
user_axioms: bool option, 

96 
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

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

98 
binary_ints: bool option, 
33192  99 
destroy_constrs: bool, 
100 
specialize: bool, 

101 
skolemize: bool, 

102 
star_linear_preds: bool, 

103 
uncurry: bool, 

104 
fast_descrs: bool, 

105 
peephole_optim: bool, 

106 
timeout: Time.time option, 

107 
tac_timeout: Time.time option, 

108 
sym_break: int, 

109 
sharing_depth: int, 

110 
flatten_props: bool, 

111 
max_threads: int, 

112 
show_skolems: bool, 

113 
show_datatypes: bool, 

114 
show_consts: bool, 

115 
evals: term list, 

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

117 
max_potential: int, 

118 
max_genuine: int, 

119 
check_potential: bool, 

120 
check_genuine: bool, 

121 
batch_size: int, 

122 
expect: string} 

123 

124 
type problem_extension = { 

125 
free_names: nut list, 

126 
sel_names: nut list, 

127 
nonsel_names: nut list, 

128 
rel_table: nut NameTable.table, 

129 
liberal: bool, 

130 
scope: scope, 

34126  131 
core: KK.formula, 
132 
defs: KK.formula list} 

33192  133 

34126  134 
type rich_problem = KK.problem * problem_extension 
33192  135 

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

137 
fun pretties_for_formulas _ _ [] = [] 

138 
 pretties_for_formulas ctxt s ts = 

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

140 
Pretty.indent indent_size (Pretty.chunks 

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

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

145 
(length ts downto 1) ts))] 

146 

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

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

148 
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

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

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

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

152 
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

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

154 
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

155 

33192  156 
val max_liberal_delay_ms = 200 
157 
val max_liberal_delay_percent = 2 

158 

159 
(* Time.time option > int *) 

160 
fun liberal_delay_for_timeout NONE = max_liberal_delay_ms 

161 
 liberal_delay_for_timeout (SOME timeout) = 

162 
Int.max (0, Int.min (max_liberal_delay_ms, 

163 
Time.toMilliseconds timeout 

164 
* max_liberal_delay_percent div 100)) 

165 

166 
(* Time.time option > bool *) 

167 
fun passed_deadline NONE = false 

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

169 

170 
(* ('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

171 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  172 

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

173 
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

174 
@{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

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

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

177 
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

178 
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

179 
 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

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

181 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  182 

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

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

184 
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

185 

33192  186 
(* Time.time > Proof.state > params > bool > term > string * Proof.state *) 
187 
fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts 

188 
orig_t = 

189 
let 

190 
val timer = Timer.startRealTimer () 

34039
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

191 
val user_thy = Proof.theory_of state 
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

192 
val nitpick_thy = ThyInfo.get_theory "Nitpick" 
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

193 
val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy)) 
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

194 
val thy = if nitpick_thy_missing then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

195 
Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY" 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

196 
[nitpick_thy, user_thy] 
34039
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

197 
> Theory.checkpoint 
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

198 
else 
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

199 
user_thy 
33192  200 
val ctxt = Proof.context_of state 
34039
1fba360b5443
made Nitpick work also for people who import "Plain" instead of "Main"
blanchet
parents:
34038
diff
changeset

201 
> nitpick_thy_missing ? Context.raw_transfer thy 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

202 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

203 
boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

204 
overlord, user_axioms, assms, merge_type_vars, binary_ints, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

205 
destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

206 
fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

207 
flatten_props, max_threads, show_skolems, show_datatypes, show_consts, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

208 
evals, formats, max_potential, max_genuine, check_potential, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

209 
check_genuine, batch_size, ...} = 
33192  210 
params 
211 
val state_ref = Unsynchronized.ref state 

212 
(* Pretty.T > unit *) 

213 
val pprint = 

214 
if auto then 

215 
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

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

219 
priority o Pretty.string_of 

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

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

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

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

224 
(* string > unit *) 

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

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

227 
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

228 
val print_v = pprint_v 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_d = pprint_d 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 

240 
val _ = print_m (K "Nitpicking...") 

241 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) 

242 
else orig_t 

243 
val assms_t = if assms orelse auto then 

244 
Logic.mk_conjunction_list (neg_t :: orig_assm_ts) 

245 
else 

246 
neg_t 

247 
val (assms_t, evals) = 

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

248 
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

249 
> pairf hd tl 
33192  250 
val original_max_potential = max_potential 
251 
val original_max_genuine = max_genuine 

252 
(* 

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

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

255 
orig_assm_ts 

256 
*) 

257 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

258 
val case_names = case_const_names thy 

259 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy 

260 
val def_table = const_def_table ctxt defs 

261 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 

262 
val simp_table = Unsynchronized.ref (const_simp_table ctxt) 

263 
val psimp_table = const_psimp_table ctxt 

264 
val intro_table = inductive_intro_table ctxt def_table 

265 
val ground_thm_table = ground_theorem_table thy 

266 
val ersatz_table = ersatz_table thy 

33877
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33745
diff
changeset

267 
val (ext_ctxt as {wf_cache, ...}) = 
33192  268 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
269 
user_axioms = user_axioms, debug = debug, wfs = wfs, 

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

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

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

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

273 
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

274 
case_names = case_names, def_table = def_table, 
33192  275 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
276 
simp_table = simp_table, psimp_table = psimp_table, 

277 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

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

279 
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

280 
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

281 
constr_cache = Unsynchronized.ref []} 
33192  282 
val frees = Term.add_frees assms_t [] 
283 
val _ = null (Term.add_tvars assms_t []) 

284 
orelse raise NOT_SUPPORTED "schematic type variables" 

285 
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), 

286 
core_t) = preprocess_term ext_ctxt assms_t 

287 
val got_all_user_axioms = 

288 
got_all_mono_user_axioms andalso no_poly_user_axioms 

289 

290 
(* styp * (bool * bool) > unit *) 

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

292 
pprint (Pretty.blk (0, 

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

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

295 
pstrs (if wf then 

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

297 
\efficiently." 

298 
else 

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

300 
\unroll it."))) 

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

302 
val _ = 

303 
pprint_d (fn () => 

304 
Pretty.chunks 

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

306 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 

307 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 

308 
nondef_ts)) 

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

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

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

312 

33877
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33745
diff
changeset

313 
val core_u = nut_from_term ext_ctxt Eq core_t 
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33745
diff
changeset

314 
val def_us = map (nut_from_term ext_ctxt DefEq) def_ts 
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33745
diff
changeset

315 
val nondef_us = map (nut_from_term ext_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

316 
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

317 
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

318 
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

319 
List.partition (is_sel o nickname_of) const_names 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

320 
val would_be_genuine = got_all_user_axioms andalso none_true wfs 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

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

322 
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

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

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

325 

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

326 
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns 
33192  327 
(* typ > bool *) 
328 
fun is_free_type_monotonic T = 

329 
unique_scope orelse 

330 
case triple_lookup (type_match thy) monos T of 

331 
SOME (SOME b) => b 

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

332 
 _ => is_bit_type T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

333 
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t 
33192  334 
fun is_datatype_monotonic T = 
335 
unique_scope orelse 

336 
case triple_lookup (type_match thy) monos T of 

337 
SOME (SOME b) => b 

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

338 
 _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

339 
orelse is_number_type thy T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

340 
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

341 
fun is_datatype_deep T = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

343 
orelse exists (curry (op =) T o domain_type o type_of) sel_names 
33192  344 
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) 
345 
> sort TermOrd.typ_ord 

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

346 
val _ = if verbose andalso binary_ints = SOME true 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

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

352 
() 
33192  353 
val (all_dataTs, all_free_Ts) = 
354 
List.partition (is_integer_type orf is_datatype thy) Ts 

355 
val (mono_dataTs, nonmono_dataTs) = 

356 
List.partition is_datatype_monotonic all_dataTs 

357 
val (mono_free_Ts, nonmono_free_Ts) = 

358 
List.partition is_free_type_monotonic all_free_Ts 

359 

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

360 
val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts 
33192  361 
val _ = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

362 
if not unique_scope andalso not (null interesting_mono_free_Ts) then 
33192  363 
print_v (fn () => 
364 
let 

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

365 
val ss = map (quote o string_for_type ctxt) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

366 
interesting_mono_free_Ts 
33192  367 
in 
368 
"The type" ^ plural_s_for_list ss ^ " " ^ 

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

370 
(if none_true monos then 

371 
"passed the monotonicity test" 

372 
else 

373 
(if length ss = 1 then "is" else "are") ^ 

374 
" considered monotonic") ^ 

375 
". Nitpick might be able to skip some scopes." 

376 
end) 

377 
else 

378 
() 

379 
val mono_Ts = mono_dataTs @ mono_free_Ts 

380 
val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts 

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

381 
val shallow_dataTs = filter_out is_datatype_deep mono_dataTs 
33192  382 
(* 
383 
val _ = priority "Monotonic datatypes:" 

384 
val _ = List.app (priority o string_for_type ctxt) mono_dataTs 

385 
val _ = priority "Nonmonotonic datatypes:" 

386 
val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs 

387 
val _ = priority "Monotonic free types:" 

388 
val _ = List.app (priority o string_for_type ctxt) mono_free_Ts 

389 
val _ = priority "Nonmonotonic free types:" 

390 
val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts 

391 
*) 

392 

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

394 
val effective_sat_solver = 

395 
if sat_solver <> "smart" then 

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

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

397 
andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

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

401 
"SAT4J") 

402 
else 

403 
sat_solver 

404 
else 

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

405 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  406 
val _ = 
407 
if sat_solver = "smart" then 

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

409 
". The following" ^ 

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

411 
"solvers are configured: " ^ 

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

412 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  413 
need_incremental)) ^ ".") 
414 
else 

415 
() 

416 

417 
val too_big_scopes = Unsynchronized.ref [] 

418 

419 
(* bool > scope > rich_problem option *) 

420 
fun problem_for_scope liberal 

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

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

424 
(!too_big_scopes)) 

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

425 
orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

426 
\problem_for_scope", "too large scope") 
33192  427 
(* 
428 
val _ = priority "Offsets:" 

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

430 
priority (string_for_type ctxt T ^ " = " ^ 

431 
string_of_int j0)) 

432 
(Typtab.dest ofs) 

433 
*) 

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

434 
val all_exact = forall (is_exact_type datatypes) Ts 
33192  435 
(* 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

436 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  437 
val main_j0 = offset_of_type ofs bool_T 
438 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

439 
val (int_card, int_j0) = spec_of_type scope int_T 

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

440 
val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) 
33192  441 
orelse raise BAD ("Nitpick.pick_them_nits_in_term.\ 
442 
\problem_for_scope", "bad offsets") 

443 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 

444 
val (free_names, rep_table) = 

445 
choose_reps_for_free_vars scope free_names NameTable.empty 

446 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

447 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

448 
val min_highest_arity = 

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

450 
val min_univ_card = 

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

34126  452 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  453 
val _ = check_arity min_univ_card min_highest_arity 
454 

455 
val core_u = choose_reps_in_nut scope liberal rep_table false core_u 

456 
val def_us = map (choose_reps_in_nut scope liberal rep_table true) 

457 
def_us 

458 
val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) 

459 
nondef_us 

33745  460 
(* 
33192  461 
val _ = List.app (priority o string_for_nut ctxt) 
462 
(free_names @ sel_names @ nonsel_names @ 

463 
core_u :: def_us @ nondef_us) 

33745  464 
*) 
33192  465 
val (free_rels, pool, rel_table) = 
466 
rename_free_vars free_names initial_pool NameTable.empty 

467 
val (sel_rels, pool, rel_table) = 

468 
rename_free_vars sel_names pool rel_table 

469 
val (other_rels, pool, rel_table) = 

470 
rename_free_vars nonsel_names pool rel_table 

471 
val core_u = rename_vars_in_nut pool rel_table core_u 

472 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 

473 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 

34126  474 
(* nut > KK.formula *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

475 
val to_f = kodkod_formula_from_nut bits ofs liberal kk 
33192  476 
val core_f = to_f core_u 
477 
val def_fs = map to_f def_us 

478 
val nondef_fs = map to_f nondef_us 

479 
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f 

480 
val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ 

481 
PrintMode.setmp [] multiline_string_for_scope scope 

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

482 
val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver 
33192  483 
> snd 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

484 
val bit_width = if bits = 0 then 16 else bits + 1 
33192  485 
val delay = if liberal then 
486 
Option.map (fn time => Time. (time, Time.now ())) 

487 
deadline 

488 
> liberal_delay_for_timeout 

489 
else 

490 
0 

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

492 
("skolem_depth", "1"), 

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

493 
("bit_width", string_of_int bit_width), 
33192  494 
("symmetry_breaking", signed_string_of_int sym_break), 
495 
("sharing", signed_string_of_int sharing_depth), 

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

497 
("delay", signed_string_of_int delay)] 

498 
val plain_rels = free_rels @ other_rels 

499 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

500 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

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

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

502 
val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk 
33192  503 
rel_table datatypes 
504 
val declarative_axioms = plain_axioms @ dtype_axioms 

505 
val univ_card = univ_card nat_card int_card main_j0 

506 
(plain_bounds @ sel_bounds) formula 

507 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 

508 
univ_card nat_card int_card main_j0 formula 

509 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

510 
> not debug ? merge_bounds 

511 
val highest_arity = 

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

513 
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

514 
val _ = if bits = 0 then () else check_bits bits formula 
34126  515 
val _ = if formula = KK.False then () 
33192  516 
else check_arity univ_card highest_arity 
517 
in 

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

519 
tuple_assigns = [], bounds = bounds, 

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

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

521 
if bits = 0 then sequential_int_bounds univ_card 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

522 
else pow_of_two_int_bounds bits main_j0 univ_card, 
33192  523 
expr_assigns = [], formula = formula}, 
524 
{free_names = free_names, sel_names = sel_names, 

525 
nonsel_names = nonsel_names, rel_table = rel_table, 

526 
liberal = liberal, scope = scope, core = core_f, 

527 
defs = nondef_fs @ def_fs @ declarative_axioms}) 

528 
end 

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

529 
handle TOO_LARGE (loc, msg) => 
34126  530 
if loc = "Nitpick_KK.check_arity" 
33192  531 
andalso not (Typtab.is_empty ofs) then 
532 
problem_for_scope liberal 

533 
{ext_ctxt = ext_ctxt, card_assigns = card_assigns, 

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

534 
bits = bits, bisim_depth = bisim_depth, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

535 
datatypes = datatypes, ofs = Typtab.empty} 
33192  536 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
537 
\problem_for_scope" then 

538 
NONE 

539 
else 

540 
(Unsynchronized.change too_big_scopes (cons scope); 

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

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

542 
". Skipping " ^ (if liberal then "potential" 
33192  543 
else "genuine") ^ 
544 
" component of scope.")); 

545 
NONE) 

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

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

547 
(print_v (fn () => ("Limit reached: " ^ msg ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

551 
NONE) 
33192  552 

34126  553 
(* int > (''a * int list list) list > ''a > KK.tuple_set *) 
33192  554 
fun tuple_set_for_rel univ_card = 
34126  555 
KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =) 
33192  556 

557 
val word_model = if falsify then "counterexample" else "model" 

558 

559 
val scopes = Unsynchronized.ref [] 

560 
val generated_scopes = Unsynchronized.ref [] 

561 
val generated_problems = Unsynchronized.ref [] 

562 
val checked_problems = Unsynchronized.ref (SOME []) 

563 
val met_potential = Unsynchronized.ref 0 

564 

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

566 
fun update_checked_problems problems = 

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

568 
o nth problems) 

569 

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

573 
: problem_extension) = 

574 
let 

575 
val (reconstructed_model, codatatypes_ok) = 

576 
reconstruct_hol_model {show_skolems = show_skolems, 

577 
show_datatypes = show_datatypes, 

578 
show_consts = show_consts} 

579 
scope formats frees free_names sel_names nonsel_names rel_table 

580 
bounds 

581 
val would_be_genuine = would_be_genuine andalso codatatypes_ok 

582 
in 

583 
pprint (Pretty.chunks 

584 
[Pretty.blk (0, 

585 
(pstrs ("Nitpick found a" ^ 

586 
(if not genuine then " potential " 

587 
else if would_be_genuine then " " 

588 
else " likely genuine ") ^ word_model) @ 

589 
(case pretties_for_scope scope verbose of 

590 
[] => [] 

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

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

593 
Pretty.indent indent_size reconstructed_model]); 

594 
if genuine then 

595 
(if check_genuine then 

596 
(case prove_hol_model scope tac_timeout free_names sel_names 

597 
rel_table bounds assms_t of 

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

599 
word_model ^ " is really genuine.") 

600 
 SOME false => 

601 
if would_be_genuine then 

602 
error ("A supposedly genuine " ^ word_model ^ " was shown to\ 

603 
\be spurious by \"auto\".\nThis should never happen.\n\ 

604 
\Please send a bug report to blanchet\ 

605 
\te@in.tum.de.") 

606 
else 

607 
print ("Refutation by \"auto\": The above " ^ word_model ^ 

608 
" is spurious.") 

609 
 NONE => print "No confirmation by \"auto\".") 

610 
else 

611 
(); 

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

612 
if has_syntactic_sorts orig_t then 
33192  613 
print "Hint: Maybe you forgot a type constraint?" 
614 
else 

615 
(); 

616 
if not would_be_genuine then 

617 
if no_poly_user_axioms then 

618 
let 

619 
val options = 

620 
[] > not got_all_mono_user_axioms 

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

622 
> not (none_true wfs) 

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

624 
> not codatatypes_ok 

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

626 
val ss = 

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

628 
options 

629 
in 

630 
print ("Try again with " ^ 

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

632 
" to confirm that the " ^ word_model ^ " is genuine.") 

633 
end 

634 
else 

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

636 
\the " ^ word_model ^ " in the presence of polymorphic \ 

637 
\axioms.") 

638 
else 

639 
(); 

640 
NONE) 

641 
else 

642 
if not genuine then 

643 
(Unsynchronized.inc met_potential; 

644 
if check_potential then 

645 
let 

646 
val status = prove_hol_model scope tac_timeout free_names 

647 
sel_names rel_table bounds assms_t 

648 
in 

649 
(case status of 

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

651 
word_model ^ " is genuine.") 

652 
 SOME false => print ("Refutation by \"auto\": The above " ^ 

653 
word_model ^ " is spurious.") 

654 
 NONE => print "No confirmation by \"auto\"."); 

655 
status 

656 
end 

657 
else 

658 
NONE) 

659 
else 

660 
NONE 

661 
end 

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

663 
fun solve_any_problem max_potential max_genuine donno first_time problems = 

664 
let 

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

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

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

670 
val max_solutions = max_potential + max_genuine 

671 
> not need_incremental ? curry Int.min 1 

672 
in 

673 
if max_solutions <= 0 then 

674 
(0, 0, donno) 

675 
else 

34126  676 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
677 
(map fst problems) of 

678 
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

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

680 
(max_potential, max_genuine, donno + 1)) 
34126  681 
 KK.Normal ([], unsat_js) => 
33192  682 
(update_checked_problems problems unsat_js; 
683 
(max_potential, max_genuine, donno)) 

34126  684 
 KK.Normal (sat_ps, unsat_js) => 
33192  685 
let 
686 
val (lib_ps, con_ps) = 

687 
List.partition (#liberal o snd o nth problems o fst) sat_ps 

688 
in 

689 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

690 
if null con_ps then 

691 
let 

33955  692 
val num_genuine = take max_potential lib_ps 
33192  693 
> 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

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

695 
> length 
33192  696 
val max_genuine = max_genuine  num_genuine 
697 
val max_potential = max_potential 

698 
 (length lib_ps  num_genuine) 

699 
in 

700 
if max_genuine <= 0 then 

701 
(0, 0, donno) 

702 
else 

703 
let 

704 
(* "co_js" is the list of conservative problems whose 

705 
liberal pendants couldn't be satisfied and hence that 

706 
most probably can't be satisfied themselves. *) 

707 
val co_js = 

708 
map (fn j => j  1) unsat_js 

709 
> filter (fn j => 

710 
j >= 0 andalso 

711 
scopes_equivalent 

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

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

714 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

715 
unsat_js @ co_js) 

716 
val problems = 

717 
problems > filter_out_indices bye_js 

718 
> max_potential <= 0 

719 
? filter_out (#liberal o snd) 

720 
in 

721 
solve_any_problem max_potential max_genuine donno false 

722 
problems 

723 
end 

724 
end 

725 
else 

726 
let 

33955  727 
val _ = take max_genuine con_ps 
33192  728 
> List.app (ignore o print_and_check true) 
729 
val max_genuine = max_genuine  length con_ps 

730 
in 

731 
if max_genuine <= 0 orelse not first_time then 

732 
(0, max_genuine, donno) 

733 
else 

734 
let 

735 
val bye_js = sort_distinct int_ord 

736 
(map fst sat_ps @ unsat_js) 

737 
val problems = 

738 
problems > filter_out_indices bye_js 

739 
> filter_out (#liberal o snd) 

740 
in solve_any_problem 0 max_genuine donno false problems end 

741 
end 

742 
end 

34126  743 
 KK.TimedOut unsat_js => 
33192  744 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  745 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
746 
 KK.Interrupted (SOME unsat_js) => 

33192  747 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  748 
 KK.Error (s, unsat_js) => 
33192  749 
(update_checked_problems problems unsat_js; 
750 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

751 
(max_potential, max_genuine, donno + 1)) 

752 
end 

753 

754 
(* int > int > scope list > int * int * int > int * int * int *) 

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

756 
let 

757 
val _ = 

758 
if null scopes then 

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

760 
else if verbose then 

761 
pprint (Pretty.chunks 

762 
[Pretty.blk (0, 

763 
pstrs ((if n > 1 then 

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

765 
signed_string_of_int n ^ ": " 

766 
else 

767 
"") ^ 

768 
"Trying " ^ string_of_int (length scopes) ^ 

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

770 
Pretty.indent indent_size 

771 
(Pretty.chunks (map2 

772 
(fn j => fn scope => 

773 
Pretty.block ( 

774 
(case pretties_for_scope scope true of 

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

776 
 pretties => pretties) @ 

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

778 
(length scopes downto 1) scopes))]) 

779 
else 

780 
() 

781 
(* scope * bool > rich_problem list * bool 

782 
> rich_problem list * bool *) 

783 
fun add_problem_for_scope (scope as {datatypes, ...}, liberal) 

784 
(problems, donno) = 

785 
(check_deadline (); 

786 
case problem_for_scope liberal scope of 

787 
SOME problem => 

788 
(problems 

789 
> (null problems orelse 

34126  790 
not (KK.problems_equivalent (fst problem) 
791 
(fst (hd problems)))) 

33192  792 
? cons problem, donno) 
793 
 NONE => (problems, donno + 1)) 

794 
val (problems, donno) = 

795 
fold add_problem_for_scope 

796 
(map_product pair scopes 

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

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

799 
([], donno) 

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

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

802 
in 

803 
solve_any_problem max_potential max_genuine donno true (rev problems) 

804 
end 

805 

806 
(* rich_problem list > scope > int *) 

807 
fun scope_count (problems : rich_problem list) scope = 

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

809 
(* string > string *) 

810 
fun excipit did_so_and_so = 

811 
let 

812 
(* rich_problem list > rich_problem list *) 

813 
val do_filter = 

814 
if !met_potential = max_potential then filter_out (#liberal o snd) 

815 
else I 

816 
val total = length (!scopes) 

817 
val unsat = 

818 
fold (fn scope => 

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

820 
0 => I 

821 
 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

822 
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

823 
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

824 
? Integer.add 1) (!generated_scopes) 0 
33192  825 
in 
826 
"Nitpick " ^ did_so_and_so ^ 

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

828 
" after checking " ^ 

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

830 
string_of_int total ^ " scope" ^ plural_s total 

831 
else 

832 
"") ^ "." 

833 
end 

834 

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

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

838 
(print_m (fn () => excipit "ran out of some resource"); "unknown") 
33192  839 
else if max_genuine = original_max_genuine then 
840 
if max_potential = original_max_potential then 

841 
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none") 

842 
else 

843 
(print_m (K ("Nitpick could not find " ^ 

844 
(if max_genuine = 1 then "a better " ^ word_model ^ "." 

845 
else "any better " ^ word_model ^ "s."))); 

846 
"potential") 

847 
else 

848 
if would_be_genuine then "genuine" else "likely_genuine" 

849 
 run_batches j n (batch :: batches) z = 

850 
let val (z as (_, max_genuine, _)) = run_batch j n batch z in 

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

852 
end 

853 

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

854 
val (skipped, 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

855 
all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

856 
bitss bisim_depths mono_Ts nonmono_Ts shallow_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

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

858 
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

859 
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

860 
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

861 
". (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

862 
\\"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

863 
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

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

865 
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

866 

33192  867 
val batches = batch_list batch_size (!scopes) 
868 
val outcome_code = 

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

870 
handle Exn.Interrupt => do_interrupted ()) 

871 
handle TimeLimit.TimeOut => 

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

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

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

875 
else error (excipit "was interrupted") 

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

877 
signed_string_of_int (Time.toMilliseconds 

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

879 
in (outcome_code, !state_ref) end 

880 
handle Exn.Interrupt => 

881 
if auto orelse #debug params then 

882 
raise Interrupt 

883 
else 

884 
if passed_deadline deadline then 

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

886 
else 

887 
error "Nitpick was interrupted." 

888 

889 
(* Proof.state > params > bool > term > string * Proof.state *) 

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

890 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

891 
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

892 
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

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

894 
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

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

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

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

898 
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

899 
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

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

901 
(pick_them_nits_in_term deadline state params auto orig_assm_ts) 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

904 
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

905 
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

906 
end 
33192  907 

908 
(* Proof.state > params > thm > int > string * Proof.state *) 

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

909 
fun pick_nits_in_subgoal state params auto i = 
33192  910 
let 
911 
val ctxt = Proof.context_of state 

33292  912 
val t = state > Proof.raw_goal > #goal > prop_of 
33192  913 
in 
914 
if Logic.count_prems t = 0 then 

915 
(priority "No subgoal!"; ("none", state)) 

916 
else 

917 
let 

918 
val assms = map term_of (Assumption.all_assms_of ctxt) 

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

919 
val (t, frees) = Logic.goal_params t i 
33192  920 
in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end 
921 
end 

922 

923 
end; 