author  blanchet 
Tue, 02 Feb 2010 11:38:38 +0100  
changeset 34982  7b8c366e34a2 
parent 34938  f4d3daddac42 
child 34998  5e492a862b34 
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 : 

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

61 
Proof.state > params > bool > int > int > int > term list > term 
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

62 
> 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 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

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

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

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

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

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

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

78 
open Nitpick_Model 
33192  79 

34126  80 
structure KK = Kodkod 
81 

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

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

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

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

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

89 
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

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

93 
blocking: bool, 

94 
falsify: bool, 

95 
debug: bool, 

96 
verbose: bool, 

97 
overlord: bool, 

98 
user_axioms: bool option, 

99 
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

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

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

104 
skolemize: bool, 

105 
star_linear_preds: bool, 

106 
uncurry: bool, 

107 
fast_descrs: bool, 

108 
peephole_optim: bool, 

109 
timeout: Time.time option, 

110 
tac_timeout: Time.time option, 

111 
sym_break: int, 

112 
sharing_depth: int, 

113 
flatten_props: bool, 

114 
max_threads: int, 

115 
show_skolems: bool, 

116 
show_datatypes: bool, 

117 
show_consts: bool, 

118 
evals: term list, 

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

120 
max_potential: int, 

121 
max_genuine: int, 

122 
check_potential: bool, 

123 
check_genuine: bool, 

124 
batch_size: int, 

125 
expect: string} 

126 

127 
type problem_extension = { 

128 
free_names: nut list, 

129 
sel_names: nut list, 

130 
nonsel_names: nut list, 

131 
rel_table: nut NameTable.table, 

132 
liberal: bool, 

133 
scope: scope, 

34126  134 
core: KK.formula, 
135 
defs: KK.formula list} 

33192  136 

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

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

140 
fun pretties_for_formulas _ _ [] = [] 

141 
 pretties_for_formulas ctxt s ts = 

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

143 
Pretty.indent indent_size (Pretty.chunks 

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

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

148 
(length ts downto 1) ts))] 

149 

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

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

151 
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

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

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

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

155 
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

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

157 
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

158 

33192  159 
val max_liberal_delay_ms = 200 
160 
val max_liberal_delay_percent = 2 

161 

162 
(* Time.time option > int *) 

163 
fun liberal_delay_for_timeout NONE = max_liberal_delay_ms 

164 
 liberal_delay_for_timeout (SOME timeout) = 

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

166 
Time.toMilliseconds timeout 

167 
* max_liberal_delay_percent div 100)) 

168 

169 
(* Time.time option > bool *) 

170 
fun passed_deadline NONE = false 

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

172 

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

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

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

176 
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

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

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

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

180 
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

181 
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

182 
 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

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

184 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  185 

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

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

187 
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

188 

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

189 
(* Time.time > Proof.state > params > bool > int > int > int > term 
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

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

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

195 
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

196 
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

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

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

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

200 
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

201 
*) 
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, 
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

203 
boxes, monos, stds, wfs, sat_solver, blocking, falsify, debug, verbose, 
34124
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 

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

240 
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

241 
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

242 
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

243 
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

244 
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

245 
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

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

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

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

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

252 
val assms_t = if assms orelse auto then 

253 
Logic.mk_conjunction_list (neg_t :: orig_assm_ts) 

254 
else 

255 
neg_t 

256 
val (assms_t, evals) = 

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

257 
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

258 
> pairf hd tl 
33192  259 
val original_max_potential = max_potential 
260 
val original_max_genuine = max_genuine 

261 
(* 

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

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

264 
orig_assm_ts 

265 
*) 

266 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

267 
val case_names = case_const_names thy 

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

269 
val def_table = const_def_table ctxt defs 

270 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 

271 
val simp_table = Unsynchronized.ref (const_simp_table ctxt) 

272 
val psimp_table = const_psimp_table ctxt 

273 
val intro_table = inductive_intro_table ctxt def_table 

274 
val ground_thm_table = ground_theorem_table thy 

275 
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

276 
val (ext_ctxt as {wf_cache, ...}) = 
33192  277 
{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

278 
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

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

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

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

282 
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

283 
case_names = case_names, def_table = def_table, 
33192  284 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
285 
simp_table = simp_table, psimp_table = psimp_table, 

286 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

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

288 
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

289 
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

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

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

293 
raise NOT_SUPPORTED "schematic type variables" 
33192  294 
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), 
295 
core_t) = preprocess_term ext_ctxt assms_t 

296 
val got_all_user_axioms = 

297 
got_all_mono_user_axioms andalso no_poly_user_axioms 

298 

299 
(* styp * (bool * bool) > unit *) 

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

301 
pprint (Pretty.blk (0, 

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

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

304 
pstrs (if wf then 

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

306 
\efficiently." 

307 
else 

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

309 
\unroll it."))) 

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

311 
val _ = 

312 
pprint_d (fn () => 

313 
Pretty.chunks 

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

315 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 

316 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 

317 
nondef_ts)) 

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

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

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

321 

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

322 
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

323 
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

324 
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

325 
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

326 
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

327 
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

328 
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

329 
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

330 
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

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

332 
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

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

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

335 

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

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

338 
fun is_type_always_monotonic T = 
34938  339 
(is_datatype thy T andalso not (is_quot_type thy T) andalso 
340 
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse 

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

341 
is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>} 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

345 
SOME (SOME b) => b 

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

346 
 _ => is_type_always_monotonic T orelse 
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

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

348 
fun is_deep_datatype T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

349 
is_datatype thy T andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

350 
(is_word_type T orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

351 
exists (curry (op =) T o domain_type o type_of) sel_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

352 
val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) 
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

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

354 
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

355 
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

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

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

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

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

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

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

364 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

380 
end) 
33192  381 
else 
382 
() 

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

383 
val deep_dataTs = filter is_deep_datatype all_Ts 
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

384 
(* FIXME: Implement proper detection of induction datatypes. *) 
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 *) 
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

386 
fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) = 
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

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

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

389 
not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes 
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

390 
*) 
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

391 
(* unit > typ list *) 
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

392 
val induct_dataTs = 
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

393 
if exists is_inductive_case (ProofContext.cases_of ctxt) 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

394 
filter (is_datatype thy) all_Ts 
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 
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

396 
[] 
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 
val _ = if standard andalso not (null induct_dataTs) 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

398 
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

399 
pstrs "Hint: To check that the induction hypothesis is \ 
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 
\general enough, try the following command: " @ 
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

401 
[Pretty.mark Markup.sendback (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

402 
pstrs ("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

403 
commas (map (prefix "non_std " o maybe_quote 
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

404 
o unyxml o string_for_type ctxt) 
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

405 
induct_dataTs) ^ 
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

406 
", show_consts]")))] @ pstrs ".")) 
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

407 
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

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

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

411 
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

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

413 
val _ = List.app (priority o string_for_type ctxt) nonmono_Ts 
33192  414 
*) 
415 

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

417 
val effective_sat_solver = 

418 
if sat_solver <> "smart" then 

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

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

420 
not (member (op =) (Kodkod_SAT.configured_sat_solvers true) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

424 
"SAT4J") 

425 
else 

426 
sat_solver 

427 
else 

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

428 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  429 
val _ = 
430 
if sat_solver = "smart" then 

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

432 
". The following" ^ 

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

434 
"solvers are configured: " ^ 

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

435 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  436 
need_incremental)) ^ ".") 
437 
else 

438 
() 

439 

440 
val too_big_scopes = Unsynchronized.ref [] 

441 

442 
(* bool > scope > rich_problem option *) 

443 
fun problem_for_scope liberal 

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

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

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

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

449 
\problem_for_scope", "too large scope") 
33192  450 
(* 
451 
val _ = priority "Offsets:" 

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

453 
priority (string_for_type ctxt T ^ " = " ^ 

454 
string_of_int j0)) 

455 
(Typtab.dest ofs) 

456 
*) 

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

457 
val all_exact = forall (is_exact_type datatypes) all_Ts 
33192  458 
(* 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

459 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  460 
val main_j0 = offset_of_type ofs bool_T 
461 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

462 
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

463 
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

464 
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

465 
"bad offsets") 
33192  466 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
467 
val (free_names, rep_table) = 

468 
choose_reps_for_free_vars scope free_names NameTable.empty 

469 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

470 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

471 
val min_highest_arity = 

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

473 
val min_univ_card = 

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

34126  475 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  476 
val _ = check_arity min_univ_card min_highest_arity 
477 

478 
val core_u = choose_reps_in_nut scope liberal rep_table false core_u 

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

480 
def_us 

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

482 
nondef_us 

33745  483 
(* 
33192  484 
val _ = List.app (priority o string_for_nut ctxt) 
485 
(free_names @ sel_names @ nonsel_names @ 

486 
core_u :: def_us @ nondef_us) 

33745  487 
*) 
33192  488 
val (free_rels, pool, rel_table) = 
489 
rename_free_vars free_names initial_pool NameTable.empty 

490 
val (sel_rels, pool, rel_table) = 

491 
rename_free_vars sel_names pool rel_table 

492 
val (other_rels, pool, rel_table) = 

493 
rename_free_vars nonsel_names pool rel_table 

494 
val core_u = rename_vars_in_nut pool rel_table core_u 

495 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 

496 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 

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

498 
val to_f = kodkod_formula_from_nut bits ofs liberal kk 
33192  499 
val core_f = to_f core_u 
500 
val def_fs = map to_f def_us 

501 
val nondef_fs = map to_f nondef_us 

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

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

504 
PrintMode.setmp [] multiline_string_for_scope scope 

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

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

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

510 
deadline 

511 
> liberal_delay_for_timeout 

512 
else 

513 
0 

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

515 
("skolem_depth", "1"), 

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

516 
("bit_width", string_of_int bit_width), 
33192  517 
("symmetry_breaking", signed_string_of_int sym_break), 
518 
("sharing", signed_string_of_int sharing_depth), 

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

520 
("delay", signed_string_of_int delay)] 

521 
val plain_rels = free_rels @ other_rels 

522 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

523 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

524 
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

525 
val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk 
33192  526 
rel_table datatypes 
527 
val declarative_axioms = plain_axioms @ dtype_axioms 

528 
val univ_card = univ_card nat_card int_card main_j0 

529 
(plain_bounds @ sel_bounds) formula 

530 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 

531 
univ_card nat_card int_card main_j0 formula 

532 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

533 
> not debug ? merge_bounds 

534 
val highest_arity = 

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

536 
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

537 
val _ = if bits = 0 then () else check_bits bits formula 
34126  538 
val _ = if formula = KK.False then () 
33192  539 
else check_arity univ_card highest_arity 
540 
in 

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

542 
tuple_assigns = [], bounds = bounds, 

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

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

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

545 
else pow_of_two_int_bounds bits main_j0 univ_card, 
33192  546 
expr_assigns = [], formula = formula}, 
547 
{free_names = free_names, sel_names = sel_names, 

548 
nonsel_names = nonsel_names, rel_table = rel_table, 

549 
liberal = liberal, scope = scope, core = core_f, 

550 
defs = nondef_fs @ def_fs @ declarative_axioms}) 

551 
end 

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

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

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

554 
not (Typtab.is_empty ofs) then 
33192  555 
problem_for_scope liberal 
556 
{ext_ctxt = ext_ctxt, card_assigns = card_assigns, 

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

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

558 
datatypes = datatypes, ofs = Typtab.empty} 
33192  559 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
560 
\problem_for_scope" then 

561 
NONE 

562 
else 

563 
(Unsynchronized.change too_big_scopes (cons scope); 

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

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

565 
". Skipping " ^ (if liberal then "potential" 
33192  566 
else "genuine") ^ 
567 
" component of scope.")); 

568 
NONE) 

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

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

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

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

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

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

574 
NONE) 
33192  575 

34126  576 
(* int > (''a * int list list) list > ''a > KK.tuple_set *) 
33192  577 
fun tuple_set_for_rel univ_card = 
34126  578 
KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =) 
33192  579 

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

580 
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

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

582 
> not standard ? prefix "nonstandard " 
33192  583 

584 
val scopes = Unsynchronized.ref [] 

585 
val generated_scopes = Unsynchronized.ref [] 

586 
val generated_problems = Unsynchronized.ref [] 

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

588 
val met_potential = Unsynchronized.ref 0 

589 

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

591 
fun update_checked_problems problems = 

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

593 
o nth problems) 

594 

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

598 
: problem_extension) = 

599 
let 

600 
val (reconstructed_model, codatatypes_ok) = 

601 
reconstruct_hol_model {show_skolems = show_skolems, 

602 
show_datatypes = show_datatypes, 

603 
show_consts = show_consts} 

604 
scope formats frees free_names sel_names nonsel_names rel_table 

605 
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

606 
val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok 
33192  607 
in 
608 
pprint (Pretty.chunks 

609 
[Pretty.blk (0, 

610 
(pstrs ("Nitpick found a" ^ 

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

612 
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

613 
else " likely genuine ") ^ das_wort_model) @ 
33192  614 
(case pretties_for_scope scope verbose of 
615 
[] => [] 

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

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

618 
Pretty.indent indent_size reconstructed_model]); 

619 
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

620 
(if check_genuine andalso standard then 
33192  621 
(case prove_hol_model scope tac_timeout free_names sel_names 
622 
rel_table bounds assms_t of 

623 
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

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

626 
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

627 
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

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

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

632 
print ("Refutation by \"auto\": The above " ^ das_wort_model ^ 
33192  633 
" is spurious.") 
634 
 NONE => print "No confirmation by \"auto\".") 

635 
else 

636 
(); 

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

637 
if not standard andalso not (null induct_dataTs) 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

638 
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

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

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

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

642 
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

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

644 
if has_syntactic_sorts orig_t then 
33192  645 
print "Hint: Maybe you forgot a type constraint?" 
646 
else 

647 
(); 

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

648 
if not genuine_means_genuine then 
33192  649 
if no_poly_user_axioms then 
650 
let 

651 
val options = 

652 
[] > not got_all_mono_user_axioms 

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

654 
> not (none_true wfs) 

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

656 
> not codatatypes_ok 

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

658 
val ss = 

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

660 
options 

661 
in 

662 
print ("Try again with " ^ 

663 
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

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

665 
" is genuine.") 
33192  666 
end 
667 
else 

668 
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

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

670 
\polymorphic axioms.") 
33192  671 
else 
672 
(); 

673 
NONE) 

674 
else 

675 
if not genuine then 

676 
(Unsynchronized.inc met_potential; 

677 
if check_potential then 

678 
let 

679 
val status = prove_hol_model scope tac_timeout free_names 

680 
sel_names rel_table bounds assms_t 

681 
in 

682 
(case status of 

683 
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

684 
das_wort_model ^ " is genuine.") 
33192  685 
 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

686 
das_wort_model ^ " is spurious.") 
33192  687 
 NONE => print "No confirmation by \"auto\"."); 
688 
status 

689 
end 

690 
else 

691 
NONE) 

692 
else 

693 
NONE 

694 
end 

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

696 
fun solve_any_problem max_potential max_genuine donno first_time problems = 

697 
let 

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

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

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

703 
val max_solutions = max_potential + max_genuine 

704 
> not need_incremental ? curry Int.min 1 

705 
in 

706 
if max_solutions <= 0 then 

707 
(0, 0, donno) 

708 
else 

34126  709 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
710 
(map fst problems) of 

711 
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

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

713 
(max_potential, max_genuine, donno + 1)) 
34126  714 
 KK.Normal ([], unsat_js) => 
33192  715 
(update_checked_problems problems unsat_js; 
716 
(max_potential, max_genuine, donno)) 

34126  717 
 KK.Normal (sat_ps, unsat_js) => 
33192  718 
let 
719 
val (lib_ps, con_ps) = 

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

721 
in 

722 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

723 
if null con_ps then 

724 
let 

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

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

728 
> length 
33192  729 
val max_genuine = max_genuine  num_genuine 
730 
val max_potential = max_potential 

731 
 (length lib_ps  num_genuine) 

732 
in 

733 
if max_genuine <= 0 then 

734 
(0, 0, donno) 

735 
else 

736 
let 

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

738 
liberal pendants couldn't be satisfied and hence that 

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

740 
val co_js = 

741 
map (fn j => j  1) unsat_js 

742 
> filter (fn j => 

743 
j >= 0 andalso 

744 
scopes_equivalent 

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

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

747 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

748 
unsat_js @ co_js) 

749 
val problems = 

750 
problems > filter_out_indices bye_js 

751 
> max_potential <= 0 

752 
? filter_out (#liberal o snd) 

753 
in 

754 
solve_any_problem max_potential max_genuine donno false 

755 
problems 

756 
end 

757 
end 

758 
else 

759 
let 

33955  760 
val _ = take max_genuine con_ps 
33192  761 
> List.app (ignore o print_and_check true) 
762 
val max_genuine = max_genuine  length con_ps 

763 
in 

764 
if max_genuine <= 0 orelse not first_time then 

765 
(0, max_genuine, donno) 

766 
else 

767 
let 

768 
val bye_js = sort_distinct int_ord 

769 
(map fst sat_ps @ unsat_js) 

770 
val problems = 

771 
problems > filter_out_indices bye_js 

772 
> filter_out (#liberal o snd) 

773 
in solve_any_problem 0 max_genuine donno false problems end 

774 
end 

775 
end 

34126  776 
 KK.TimedOut unsat_js => 
33192  777 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  778 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
779 
 KK.Interrupted (SOME unsat_js) => 

33192  780 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  781 
 KK.Error (s, unsat_js) => 
33192  782 
(update_checked_problems problems unsat_js; 
783 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

784 
(max_potential, max_genuine, donno + 1)) 

785 
end 

786 

787 
(* int > int > scope list > int * int * int > int * int * int *) 

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

789 
let 

790 
val _ = 

791 
if null scopes then 

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

793 
else if verbose then 

794 
pprint (Pretty.chunks 

795 
[Pretty.blk (0, 

796 
pstrs ((if n > 1 then 

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

798 
signed_string_of_int n ^ ": " 

799 
else 

800 
"") ^ 

801 
"Trying " ^ string_of_int (length scopes) ^ 

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

803 
Pretty.indent indent_size 

804 
(Pretty.chunks (map2 

805 
(fn j => fn scope => 

806 
Pretty.block ( 

807 
(case pretties_for_scope scope true of 

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

809 
 pretties => pretties) @ 

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

811 
(length scopes downto 1) scopes))]) 

812 
else 

813 
() 

814 
(* scope * bool > rich_problem list * bool 

815 
> rich_problem list * bool *) 

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

817 
(problems, donno) = 

818 
(check_deadline (); 

819 
case problem_for_scope liberal scope of 

820 
SOME problem => 

821 
(problems 

822 
> (null problems orelse 

34126  823 
not (KK.problems_equivalent (fst problem) 
824 
(fst (hd problems)))) 

33192  825 
? cons problem, donno) 
826 
 NONE => (problems, donno + 1)) 

827 
val (problems, donno) = 

828 
fold add_problem_for_scope 

829 
(map_product pair scopes 

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

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

832 
([], donno) 

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

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

835 
in 

836 
solve_any_problem max_potential max_genuine donno true (rev problems) 

837 
end 

838 

839 
(* rich_problem list > scope > int *) 

840 
fun scope_count (problems : rich_problem list) scope = 

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

842 
(* string > string *) 

843 
fun excipit did_so_and_so = 

844 
let 

845 
(* rich_problem list > rich_problem list *) 

846 
val do_filter = 

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

848 
else I 

849 
val total = length (!scopes) 

850 
val unsat = 

851 
fold (fn scope => 

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

853 
0 => I 

854 
 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

855 
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

856 
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

857 
? Integer.add 1) (!generated_scopes) 0 
33192  858 
in 
859 
"Nitpick " ^ did_so_and_so ^ 

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

861 
" after checking " ^ 

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

863 
string_of_int total ^ " scope" ^ plural_s total 

864 
else 

865 
"") ^ "." 

866 
end 

867 

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

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

871 
(print_m (fn () => excipit "ran out of some resource"); "unknown") 
33192  872 
else if max_genuine = original_max_genuine then 
873 
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

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

875 
"Nitpick found no " ^ 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

876 
(if not standard andalso not (null induct_dataTs) 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

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

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

879 
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

880 
"")); "none") 
33192  881 
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

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

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

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

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

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

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

891 
end 

892 

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

893 
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

894 
all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns 
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

895 
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

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

897 
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

898 
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

899 
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

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

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

902 
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

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

904 
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

905 

33192  906 
val batches = batch_list batch_size (!scopes) 
907 
val outcome_code = 

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

909 
handle Exn.Interrupt => do_interrupted ()) 

910 
handle TimeLimit.TimeOut => 

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

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

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

914 
else error (excipit "was interrupted") 

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

916 
signed_string_of_int (Time.toMilliseconds 

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

918 
in (outcome_code, !state_ref) end 

919 
handle Exn.Interrupt => 

920 
if auto orelse #debug params then 

921 
raise Interrupt 

922 
else 

923 
if passed_deadline deadline then 

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

925 
else 

926 
error "Nitpick was interrupted." 

927 

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

928 
(* Proof.state > params > bool > int > int > int > term 
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

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

930 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i 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

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

932 
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

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

934 
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

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

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

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

938 
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

939 
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

940 
time_limit (if debug then NONE else timeout) 
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

941 
(pick_them_nits_in_term deadline state params auto i n step 
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

942 
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

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

944 
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

945 
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

946 
end 
33192  947 

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

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

949 
fun pick_nits_in_subgoal state params auto i step = 
33192  950 
let 
951 
val ctxt = Proof.context_of state 

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

954 
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

955 
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

956 
 n => 
33192  957 
let 
958 
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

959 
val (t, frees) = Logic.goal_params t i 
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

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

961 
pick_nits_in_term state params auto i n step assms 
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

962 
(subst_bounds (frees, t)) 
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

963 
end 
33192  964 
end 
965 

966 
end; 