author  blanchet 
Thu, 25 Feb 2010 16:33:39 +0100  
changeset 35385  29f81babefd7 
parent 35384  88dbcfe75c45 
child 35386  45a4e19d3ebd 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Finite model generation for HOL formulas using Kodkod. 

6 
*) 

7 

8 
signature NITPICK = 

9 
sig 

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

10 
type styp = Nitpick_Util.styp 
33192  11 
type params = { 
12 
cards_assigns: (typ option * int list) list, 

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

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

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

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

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

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

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

22 
blocking: bool, 

23 
falsify: bool, 

24 
debug: bool, 

25 
verbose: bool, 

26 
overlord: bool, 

27 
user_axioms: bool option, 

28 
assms: bool, 

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

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

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

33 
skolemize: bool, 

34 
star_linear_preds: bool, 

35 
uncurry: bool, 

36 
fast_descrs: bool, 

37 
peephole_optim: bool, 

38 
timeout: Time.time option, 

39 
tac_timeout: Time.time option, 

40 
sym_break: int, 

41 
sharing_depth: int, 

42 
flatten_props: bool, 

43 
max_threads: int, 

44 
show_skolems: bool, 

45 
show_datatypes: bool, 

46 
show_consts: bool, 

47 
evals: term list, 

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

49 
max_potential: int, 

50 
max_genuine: int, 

51 
check_potential: bool, 

52 
check_genuine: bool, 

53 
batch_size: int, 

54 
expect: string} 

55 

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

57 
val unregister_frac_type : string > theory > theory 

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

59 
val unregister_codatatype : typ > theory > theory 

60 
val pick_nits_in_term : 

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

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

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

67 
structure Nitpick : NITPICK = 

68 
struct 

69 

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

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

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

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

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

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

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

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

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

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

79 
open Nitpick_Model 
33192  80 

34126  81 
structure KK = Kodkod 
82 

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

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

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

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

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

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

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

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

94 
blocking: bool, 

95 
falsify: bool, 

96 
debug: bool, 

97 
verbose: bool, 

98 
overlord: bool, 

99 
user_axioms: bool option, 

100 
assms: bool, 

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

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

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

105 
skolemize: bool, 

106 
star_linear_preds: bool, 

107 
uncurry: bool, 

108 
fast_descrs: bool, 

109 
peephole_optim: bool, 

110 
timeout: Time.time option, 

111 
tac_timeout: Time.time option, 

112 
sym_break: int, 

113 
sharing_depth: int, 

114 
flatten_props: bool, 

115 
max_threads: int, 

116 
show_skolems: bool, 

117 
show_datatypes: bool, 

118 
show_consts: bool, 

119 
evals: term list, 

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

121 
max_potential: int, 

122 
max_genuine: int, 

123 
check_potential: bool, 

124 
check_genuine: bool, 

125 
batch_size: int, 

126 
expect: string} 

127 

128 
type problem_extension = { 

129 
free_names: nut list, 

130 
sel_names: nut list, 

131 
nonsel_names: nut list, 

132 
rel_table: nut NameTable.table, 

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

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

33192  137 

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

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

141 
fun pretties_for_formulas _ _ [] = [] 

142 
 pretties_for_formulas ctxt s ts = 

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

144 
Pretty.indent indent_size (Pretty.chunks 

145 
(map2 (fn j => fn t => 

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

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

149 
(length ts downto 1) ts))] 

150 

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

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

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

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

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

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

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

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

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

159 

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

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

161 
val max_unsound_delay_percent = 2 
33192  162 

163 
(* Time.time option > int *) 

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

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

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

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

168 
* max_unsound_delay_percent div 100)) 
33192  169 

170 
(* Time.time option > bool *) 

171 
fun passed_deadline NONE = false 

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

173 

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

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

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

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

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

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

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

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

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

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

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

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

185 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  186 

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

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

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

189 

35335  190 
(* Time.time > Proof.state > params > bool > int > int > int 
191 
> (term * term) list > term list > term > string * Proof.state *) 

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

192 
fun pick_them_nits_in_term deadline state (params : params) auto i n step 
35335  193 
subst orig_assm_ts orig_t = 
33192  194 
let 
195 
val timer = Timer.startRealTimer () 

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

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

197 
val ctxt = Proof.context_of state 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

213 
(* Pretty.T > unit *) 

214 
val pprint = 

215 
if auto then 

216 
Unsynchronized.change state_ref o Proof.goal_message o K 

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

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

220 
priority o Pretty.string_of 

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

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

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

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

225 
(* string > unit *) 

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

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

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

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

229 
val print_v = pprint_v o K o plazy 
33192  230 

231 
(* unit > unit *) 

232 
fun check_deadline () = 

233 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut 

234 
else () 

235 
(* unit > 'a *) 

236 
fun do_interrupted () = 

237 
if passed_deadline deadline then raise TimeLimit.TimeOut 

238 
else raise Interrupt 

239 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

259 
(* 

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

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

262 
orig_assm_ts 

263 
*) 

264 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

271 
val intro_table = inductive_intro_table ctxt subst def_table 

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

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

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

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

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

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

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

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

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

284 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

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

286 
special_funs = Unsynchronized.ref [], 

33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

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

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

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

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

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

296 

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

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

299 
pprint (Pretty.blk (0, 

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

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

302 
pstrs (if wf then 

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

304 
\efficiently." 

305 
else 

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

307 
\unroll it."))) 

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

309 
val _ = 

310 
pprint_d (fn () => 

311 
Pretty.chunks 

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

313 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 

314 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 

315 
nondef_ts)) 

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

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

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

319 

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

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

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

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

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

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

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

326 
List.partition (is_sel o nickname_of) const_names 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

327 
val genuine_means_genuine = got_all_user_axioms andalso none_true wfs 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

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

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

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

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

333 

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

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

335 
(* typ list > string > string *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

336 
fun monotonicity_message Ts extra = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

337 
let val ss = map (quote o string_for_type ctxt) Ts in 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

338 
"The type" ^ plural_s_for_list ss ^ " " ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

339 
space_implode " " (serial_commas "and" ss) ^ " " ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

340 
(if none_true monos then 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

341 
"passed the monotonicity test" 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

343 
(if length ss = 1 then "is" else "are") ^ " considered monotonic") ^ 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

344 
". " ^ extra 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

345 
end 
33192  346 
(* typ > bool *) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

347 
fun is_type_always_monotonic T = 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

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

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

353 
fun is_type_monotonic T = 
33192  354 
unique_scope orelse 
355 
case triple_lookup (type_match thy) monos T of 

356 
SOME (SOME b) => b 

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

357 
 _ => is_type_always_monotonic T orelse is_type_actually_monotonic T 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

359 
case triple_lookup (type_match thy) monos T of 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

360 
SOME (SOME false) => false 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

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

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

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

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

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

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

368 
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

369 
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

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

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

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

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

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

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

378 
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

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

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

381 
print_v (K (monotonicity_message interesting_mono_Ts 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

382 
"Nitpick might be able to skip some scopes.")) 
33192  383 
else 
384 
() 

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

385 
val (deep_dataTs, shallow_dataTs) = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

386 
all_Ts > filter (is_datatype thy stds) > List.partition is_datatype_deep 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

388 
shallow_dataTs > filter_out (is_finite_type hol_ctxt) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

389 
> filter is_type_finitizable 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

391 
if verbose andalso not (null finitizable_dataTs) then 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

392 
print_v (K (monotonicity_message finitizable_dataTs 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

393 
"Nitpick can use a more precise finite encoding.")) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

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

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

397 
provide a hint to the user. *) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

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

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

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

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

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

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

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

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

407 
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

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

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

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

412 
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

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

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

416 
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

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

418 
val _ = List.app (priority o string_for_type ctxt) nonmono_Ts 
33192  419 
*) 
420 

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

422 
val effective_sat_solver = 

423 
if sat_solver <> "smart" then 

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

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

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

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

429 
"SAT4J") 

430 
else 

431 
sat_solver 

432 
else 

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

433 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  434 
val _ = 
435 
if sat_solver = "smart" then 

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

437 
". The following" ^ 

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

439 
"solvers are configured: " ^ 

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

440 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  441 
need_incremental)) ^ ".") 
442 
else 

443 
() 

444 

445 
val too_big_scopes = Unsynchronized.ref [] 

446 

447 
(* bool > scope > rich_problem option *) 

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

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

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

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

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

454 
\problem_for_scope", "too large scope") 
33192  455 
(* 
456 
val _ = priority "Offsets:" 

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

458 
priority (string_for_type ctxt T ^ " = " ^ 

459 
string_of_int j0)) 

460 
(Typtab.dest ofs) 

461 
*) 

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

462 
val all_exact = forall (is_exact_type datatypes true) all_Ts 
33192  463 
(* 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

464 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  465 
val main_j0 = offset_of_type ofs bool_T 
466 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

467 
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

468 
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

469 
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

470 
"bad offsets") 
33192  471 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
472 
val (free_names, rep_table) = 

473 
choose_reps_for_free_vars scope free_names NameTable.empty 

474 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

475 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

476 
val min_highest_arity = 

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

478 
val min_univ_card = 

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

34126  480 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  481 
val _ = check_arity min_univ_card min_highest_arity 
482 

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

483 
val core_u = choose_reps_in_nut scope unsound rep_table false core_u 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

484 
val def_us = map (choose_reps_in_nut scope unsound rep_table true) 
33192  485 
def_us 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

486 
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) 
33192  487 
nondef_us 
33745  488 
(* 
33192  489 
val _ = List.app (priority o string_for_nut ctxt) 
490 
(free_names @ sel_names @ nonsel_names @ 

491 
core_u :: def_us @ nondef_us) 

33745  492 
*) 
33192  493 
val (free_rels, pool, rel_table) = 
494 
rename_free_vars free_names initial_pool NameTable.empty 

495 
val (sel_rels, pool, rel_table) = 

496 
rename_free_vars sel_names pool rel_table 

497 
val (other_rels, pool, rel_table) = 

498 
rename_free_vars nonsel_names pool rel_table 

499 
val core_u = rename_vars_in_nut pool rel_table core_u 

500 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 

501 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 

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

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

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

504 
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us 
33192  505 
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

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

510 
val bit_width = if bits = 0 then 16 else bits + 1 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

511 
val delay = if unsound then 
33192  512 
Option.map (fn time => Time. (time, Time.now ())) 
513 
deadline 

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

514 
> unsound_delay_for_timeout 
33192  515 
else 
516 
0 

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

518 
("skolem_depth", "1"), 

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

519 
("bit_width", string_of_int bit_width), 
33192  520 
("symmetry_breaking", signed_string_of_int sym_break), 
521 
("sharing", signed_string_of_int sharing_depth), 

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

523 
("delay", signed_string_of_int delay)] 

524 
val plain_rels = free_rels @ other_rels 

525 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

526 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

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

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

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

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

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

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

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

534 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
33192  535 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 
536 
univ_card nat_card int_card main_j0 formula 

537 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

538 
> not debug ? merge_bounds 

539 
val highest_arity = 

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

541 
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

542 
val _ = if bits = 0 then () else check_bits bits formula 
34126  543 
val _ = if formula = KK.False then () 
33192  544 
else check_arity univ_card highest_arity 
545 
in 

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

547 
tuple_assigns = [], bounds = bounds, 

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

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

549 
else pow_of_two_int_bounds bits main_j0, 
33192  550 
expr_assigns = [], formula = formula}, 
551 
{free_names = free_names, sel_names = sel_names, 

552 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

553 
unsound = unsound, scope = scope, core = core_f, 
33192  554 
defs = nondef_fs @ def_fs @ declarative_axioms}) 
555 
end 

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

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

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

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

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

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

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

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

563 
ofs = Typtab.empty} 
33192  564 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
565 
\problem_for_scope" then 

566 
NONE 

567 
else 

568 
(Unsynchronized.change too_big_scopes (cons scope); 

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

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

570 
". Skipping " ^ (if unsound then "potential" 
33192  571 
else "genuine") ^ 
572 
" component of scope.")); 

573 
NONE) 

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

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

575 
(print_v (fn () => ("Limit reached: " ^ msg ^ 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

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

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

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

579 
NONE) 
33192  580 

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

581 
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

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

583 
> not standard ? prefix "nonstandard " 
33192  584 

585 
val scopes = Unsynchronized.ref [] 

586 
val generated_scopes = Unsynchronized.ref [] 

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

587 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  588 
val checked_problems = Unsynchronized.ref (SOME []) 
589 
val met_potential = Unsynchronized.ref 0 

590 

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

592 
fun update_checked_problems problems = 

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

594 
o nth problems) 

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

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

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

597 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  598 

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

602 
: problem_extension) = 

603 
let 

604 
val (reconstructed_model, codatatypes_ok) = 

605 
reconstruct_hol_model {show_skolems = show_skolems, 

606 
show_datatypes = show_datatypes, 

607 
show_consts = show_consts} 

608 
scope formats frees free_names sel_names nonsel_names rel_table 

609 
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

610 
val genuine_means_genuine = genuine_means_genuine andalso codatatypes_ok 
33192  611 
in 
612 
pprint (Pretty.chunks 

613 
[Pretty.blk (0, 

614 
(pstrs ("Nitpick found a" ^ 

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

616 
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

617 
else " likely genuine ") ^ das_wort_model) @ 
33192  618 
(case pretties_for_scope scope verbose of 
619 
[] => [] 

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

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

622 
Pretty.indent indent_size reconstructed_model]); 

623 
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

624 
(if check_genuine andalso standard then 
33192  625 
(case prove_hol_model scope tac_timeout free_names sel_names 
626 
rel_table bounds assms_t of 

627 
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

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

630 
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

631 
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

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

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

636 
print ("Refutation by \"auto\": The above " ^ das_wort_model ^ 
33192  637 
" is spurious.") 
638 
 NONE => print "No confirmation by \"auto\".") 

639 
else 

640 
(); 

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

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

642 
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

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

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

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

646 
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

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

648 
if has_syntactic_sorts orig_t then 
33192  649 
print "Hint: Maybe you forgot a type constraint?" 
650 
else 

651 
(); 

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

652 
if not genuine_means_genuine then 
33192  653 
if no_poly_user_axioms then 
654 
let 

655 
val options = 

656 
[] > not got_all_mono_user_axioms 

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

658 
> not (none_true wfs) 

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

660 
> not codatatypes_ok 

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

662 
val ss = 

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

664 
options 

665 
in 

666 
print ("Try again with " ^ 

667 
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

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

669 
" is genuine.") 
33192  670 
end 
671 
else 

672 
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

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

674 
\polymorphic axioms.") 
33192  675 
else 
676 
(); 

677 
NONE) 

678 
else 

679 
if not genuine then 

680 
(Unsynchronized.inc met_potential; 

681 
if check_potential then 

682 
let 

683 
val status = prove_hol_model scope tac_timeout free_names 

684 
sel_names rel_table bounds assms_t 

685 
in 

686 
(case status of 

687 
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

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

690 
das_wort_model ^ " is spurious.") 
33192  691 
 NONE => print "No confirmation by \"auto\"."); 
692 
status 

693 
end 

694 
else 

695 
NONE) 

696 
else 

697 
NONE 

698 
end 

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

700 
fun solve_any_problem max_potential max_genuine donno first_time problems = 

701 
let 

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

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

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

707 
val max_solutions = max_potential + max_genuine 

708 
> not need_incremental ? curry Int.min 1 

709 
in 

710 
if max_solutions <= 0 then 

711 
(0, 0, donno) 

712 
else 

34126  713 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
714 
(map fst problems) of 

715 
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

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

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

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

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

721 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  722 
let 
723 
val (lib_ps, con_ps) = 

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

724 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  725 
in 
726 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

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

727 
show_kodkod_warning s; 
33192  728 
if null con_ps then 
729 
let 

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

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

733 
> length 
33192  734 
val max_genuine = max_genuine  num_genuine 
735 
val max_potential = max_potential 

736 
 (length lib_ps  num_genuine) 

737 
in 

738 
if max_genuine <= 0 then 

739 
(0, 0, donno) 

740 
else 

741 
let 

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

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

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

744 
probably can't be satisfied themselves. *) 
33192  745 
val co_js = 
746 
map (fn j => j  1) unsat_js 

747 
> filter (fn j => 

748 
j >= 0 andalso 

749 
scopes_equivalent 

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

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

752 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

753 
unsat_js @ co_js) 

754 
val problems = 

755 
problems > filter_out_indices bye_js 

756 
> max_potential <= 0 

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

757 
? filter_out (#unsound o snd) 
33192  758 
in 
759 
solve_any_problem max_potential max_genuine donno false 

760 
problems 

761 
end 

762 
end 

763 
else 

764 
let 

33955  765 
val _ = take max_genuine con_ps 
33192  766 
> List.app (ignore o print_and_check true) 
767 
val max_genuine = max_genuine  length con_ps 

768 
in 

769 
if max_genuine <= 0 orelse not first_time then 

770 
(0, max_genuine, donno) 

771 
else 

772 
let 

773 
val bye_js = sort_distinct int_ord 

774 
(map fst sat_ps @ unsat_js) 

775 
val problems = 

776 
problems > filter_out_indices bye_js 

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

777 
> filter_out (#unsound o snd) 
33192  778 
in solve_any_problem 0 max_genuine donno false problems end 
779 
end 

780 
end 

34126  781 
 KK.TimedOut unsat_js => 
33192  782 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  783 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
784 
 KK.Interrupted (SOME unsat_js) => 

33192  785 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  786 
 KK.Error (s, unsat_js) => 
33192  787 
(update_checked_problems problems unsat_js; 
788 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

789 
(max_potential, max_genuine, donno + 1)) 

790 
end 

791 

792 
(* int > int > scope list > int * int * int > int * int * int *) 

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

794 
let 

795 
val _ = 

796 
if null scopes then 

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

798 
else if verbose then 

799 
pprint (Pretty.chunks 

800 
[Pretty.blk (0, 

801 
pstrs ((if n > 1 then 

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

803 
signed_string_of_int n ^ ": " 

804 
else 

805 
"") ^ 

806 
"Trying " ^ string_of_int (length scopes) ^ 

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

808 
Pretty.indent indent_size 

809 
(Pretty.chunks (map2 

810 
(fn j => fn scope => 

811 
Pretty.block ( 

812 
(case pretties_for_scope scope true of 

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

814 
 pretties => pretties) @ 

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

816 
(length scopes downto 1) scopes))]) 

817 
else 

818 
() 

819 
(* scope * bool > rich_problem list * bool 

820 
> rich_problem list * bool *) 

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

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

823 
case problem_for_scope unsound scope of 
33192  824 
SOME problem => 
825 
(problems 

826 
> (null problems orelse 

34126  827 
not (KK.problems_equivalent (fst problem) 
828 
(fst (hd problems)))) 

33192  829 
? cons problem, donno) 
830 
 NONE => (problems, donno + 1)) 

831 
val (problems, donno) = 

832 
fold add_problem_for_scope 

833 
(map_product pair scopes 

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

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

836 
([], donno) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

861 
() 
33192  862 
in 
863 
solve_any_problem max_potential max_genuine donno true (rev problems) 

864 
end 

865 

866 
(* rich_problem list > scope > int *) 

867 
fun scope_count (problems : rich_problem list) scope = 

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

869 
(* string > string *) 

870 
fun excipit did_so_and_so = 

871 
let 

872 
(* rich_problem list > rich_problem list *) 

873 
val do_filter = 

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

874 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  875 
else I 
876 
val total = length (!scopes) 

877 
val unsat = 

878 
fold (fn scope => 

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

880 
0 => I 

881 
 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

882 
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

883 
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

884 
? Integer.add 1) (!generated_scopes) 0 
33192  885 
in 
886 
"Nitpick " ^ did_so_and_so ^ 

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

888 
" after checking " ^ 

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

890 
string_of_int total ^ " scope" ^ plural_s total 

891 
else 

892 
"") ^ "." 

893 
end 

894 

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

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

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

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

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

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

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

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

906 
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

907 
"")); "none") 
33192  908 
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

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

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

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

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

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

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

918 
end 

919 

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

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

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

922 
iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

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

925 
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

926 
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

927 
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

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

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

930 
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

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

932 
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

933 

33192  934 
val batches = batch_list batch_size (!scopes) 
935 
val outcome_code = 

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

937 
handle Exn.Interrupt => do_interrupted ()) 

938 
handle TimeLimit.TimeOut => 

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

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

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

942 
else error (excipit "was interrupted") 

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

944 
signed_string_of_int (Time.toMilliseconds 

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

946 
in (outcome_code, !state_ref) end 

947 
handle Exn.Interrupt => 

948 
if auto orelse #debug params then 

949 
raise Interrupt 

950 
else 

951 
if passed_deadline deadline then 

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

953 
else 

954 
error "Nitpick was interrupted." 

955 

35335  956 
(* Proof.state > params > bool > int > int > int > (term * term) list 
957 
> term list > term > string * Proof.state *) 

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

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

960 
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

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

962 
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

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

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

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

966 
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

967 
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

968 
time_limit (if debug then NONE else timeout) 
35335  969 
(pick_them_nits_in_term deadline state params auto i n step subst 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

970 
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

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

972 
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

973 
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

974 
end 
33192  975 

35335  976 
(* string list > term > bool *) 
977 
fun is_fixed_equation fixes 

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

979 
member (op =) fixes s 

980 
 is_fixed_equation _ _ = false 

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

982 
fun extract_fixed_frees ctxt (assms, t) = 

983 
let 

984 
val fixes = Variable.fixes_of ctxt > map snd 

985 
val (subst, other_assms) = 

986 
List.partition (is_fixed_equation fixes) assms 

987 
>> map Logic.dest_equals 

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

989 

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

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

991 
fun pick_nits_in_subgoal state params auto i step = 
33192  992 
let 
993 
val ctxt = Proof.context_of state 

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

996 
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

997 
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

998 
 n => 
33192  999 
let 
35335  1000 
val (t, frees) = Logic.goal_params t i 
1001 
val t = subst_bounds (frees, t) 

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

33192  1005 
end 
1006 

1007 
end; 