author  blanchet 
Tue, 09 Mar 2010 14:18:21 +0100  
changeset 35671  ed2c3830d881 
parent 35665  ff2bf50505ab 
child 35696  17ae461d6133 
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, 

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

18 
finitizes: (typ option * bool option) list, 
33192  19 
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

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

23 
blocking: bool, 

24 
falsify: bool, 

25 
debug: bool, 

26 
verbose: bool, 

27 
overlord: bool, 

28 
user_axioms: bool option, 

29 
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

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

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

34 
skolemize: bool, 

35 
star_linear_preds: bool, 

36 
uncurry: bool, 

37 
fast_descrs: bool, 

38 
peephole_optim: bool, 

39 
timeout: Time.time option, 

40 
tac_timeout: Time.time option, 

41 
sym_break: int, 

42 
sharing_depth: int, 

43 
flatten_props: bool, 

44 
max_threads: int, 

45 
show_skolems: bool, 

46 
show_datatypes: bool, 

47 
show_consts: bool, 

48 
evals: term list, 

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

50 
max_potential: int, 

51 
max_genuine: int, 

52 
check_potential: bool, 

53 
check_genuine: bool, 

54 
batch_size: int, 

55 
expect: string} 

56 

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

58 
val unregister_frac_type : string > theory > theory 

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

60 
val unregister_codatatype : typ > theory > theory 

61 
val pick_nits_in_term : 

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

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

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

68 
structure Nitpick : NITPICK = 

69 
struct 

70 

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

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

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

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

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

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

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

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

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

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

80 
open Nitpick_Model 
33192  81 

34126  82 
structure KK = Kodkod 
83 

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

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

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

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

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

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

91 
finitizes: (typ option * bool option) list, 
33192  92 
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

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

96 
blocking: bool, 

97 
falsify: bool, 

98 
debug: bool, 

99 
verbose: bool, 

100 
overlord: bool, 

101 
user_axioms: bool option, 

102 
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

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

104 
binary_ints: bool option, 
33192  105 
destroy_constrs: bool, 
106 
specialize: bool, 

107 
skolemize: bool, 

108 
star_linear_preds: bool, 

109 
uncurry: bool, 

110 
fast_descrs: bool, 

111 
peephole_optim: bool, 

112 
timeout: Time.time option, 

113 
tac_timeout: Time.time option, 

114 
sym_break: int, 

115 
sharing_depth: int, 

116 
flatten_props: bool, 

117 
max_threads: int, 

118 
show_skolems: bool, 

119 
show_datatypes: bool, 

120 
show_consts: bool, 

121 
evals: term list, 

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

123 
max_potential: int, 

124 
max_genuine: int, 

125 
check_potential: bool, 

126 
check_genuine: bool, 

127 
batch_size: int, 

128 
expect: string} 

129 

130 
type problem_extension = { 

131 
free_names: nut list, 

132 
sel_names: nut list, 

133 
nonsel_names: nut list, 

134 
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

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

136 
scope: scope} 
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 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

199 

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

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

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

202 
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

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

204 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

205 
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

206 
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

207 
destroy_constrs, specialize, skolemize, star_linear_preds, uncurry, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

208 
fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

209 
flatten_props, max_threads, show_skolems, show_datatypes, show_consts, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

210 
evals, formats, max_potential, max_genuine, check_potential, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

211 
check_genuine, batch_size, ...} = 
33192  212 
params 
213 
val state_ref = Unsynchronized.ref state 

214 
(* Pretty.T > unit *) 

215 
val pprint = 

216 
if auto then 

217 
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

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

221 
priority o Pretty.string_of 

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

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

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

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

226 
(* string > unit *) 

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

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

229 
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

230 
val print_v = pprint_v o K o plazy 
33192  231 

232 
(* unit > unit *) 

233 
fun check_deadline () = 

234 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut 

235 
else () 

236 
(* unit > 'a *) 

237 
fun do_interrupted () = 

238 
if passed_deadline deadline then raise TimeLimit.TimeOut 

239 
else raise Interrupt 

240 

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

242 
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

243 
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

244 
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

245 
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

246 
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

247 
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

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

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

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

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

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

256 
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

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

260 
(* 

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

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

263 
orig_assm_ts 

264 
*) 

265 
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

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

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

272 
val intro_table = inductive_intro_table ctxt subst def_table 

33192  273 
val ground_thm_table = ground_theorem_table thy 
274 
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

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

277 
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

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

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

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

281 
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

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

285 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

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

287 
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

288 
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

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

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

292 
raise NOT_SUPPORTED "schematic type variables" 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

293 
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

294 
binarize) = preprocess_term hol_ctxt finitizes monos assms_t 
33192  295 
val got_all_user_axioms = 
296 
got_all_mono_user_axioms andalso no_poly_user_axioms 

297 

298 
(* styp * (bool * bool) > unit *) 

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

300 
pprint (Pretty.blk (0, 

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

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

303 
pstrs (if wf then 

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

305 
\efficiently." 

306 
else 

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

308 
\unroll it."))) 

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

310 
val _ = 

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

311 
pprint_d (fn () => Pretty.chunks 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

312 
(pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

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

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

319 

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

320 
val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts 
35070
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 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

322 
val (free_names, const_names) = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

324 
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

325 
List.partition (is_sel o nickname_of) const_names 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

326 
val sound_finitizes = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

327 
none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

329 
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

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

331 
val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us) 
33558
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 *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

347 
fun is_type_fundamentally_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 = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

352 
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

354 
case triple_lookup (type_match thy) monos T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

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

357 
fun is_type_monotonic T = 
33192  358 
unique_scope orelse 
359 
case triple_lookup (type_match thy) monos T of 

360 
SOME (SOME b) => b 

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

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

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

363 
fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

365 
 is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

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

368 
case triple_lookup (type_match thy) finitizes T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

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

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

372 
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

373 
exists (curry (op =) T o domain_type o type_of) sel_names 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

374 
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) 
35408  375 
> sort Term_Ord.typ_ord 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

376 
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

377 
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

378 
print_v (K "The option \"binary_ints\" will be ignored because \ 
34126  379 
\of the presence of rationals, reals, \"Suc\", \ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

380 
\\"gcd\", or \"lcm\" in the problem or because of the \ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

381 
\\"non_std\" option.") 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

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

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

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

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

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

391 
"Nitpick might be able to skip some scopes.")) 
33192  392 
else 
393 
() 

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

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

395 
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

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

397 
shallow_dataTs > filter_out (is_finite_type hol_ctxt) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

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

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

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

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

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

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

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

406 
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

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

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

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

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

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

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

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

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

415 
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

416 
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

417 
pstrs "Hint: To check that the induction hypothesis is \ 
35177  418 
\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

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

420 
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

421 
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

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

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

425 
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

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

427 
val _ = List.app (priority o string_for_type ctxt) nonmono_Ts 
33192  428 
*) 
429 

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

431 
val effective_sat_solver = 

432 
if sat_solver <> "smart" then 

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

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

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

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

438 
"SAT4J") 

439 
else 

440 
sat_solver 

441 
else 

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

442 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  443 
val _ = 
444 
if sat_solver = "smart" then 

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

446 
". The following" ^ 

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

448 
"solvers are configured: " ^ 

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

449 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  450 
need_incremental)) ^ ".") 
451 
else 

452 
() 

453 

454 
val too_big_scopes = Unsynchronized.ref [] 

455 

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

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

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

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

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

463 
\problem_for_scope", "too large scope") 
33192  464 
(* 
465 
val _ = priority "Offsets:" 

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

467 
priority (string_for_type ctxt T ^ " = " ^ 

468 
string_of_int j0)) 

469 
(Typtab.dest ofs) 

470 
*) 

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

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

473 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  474 
val main_j0 = offset_of_type ofs bool_T 
475 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

476 
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

477 
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

478 
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

479 
"bad offsets") 
33192  480 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
481 
val (free_names, rep_table) = 

482 
choose_reps_for_free_vars scope free_names NameTable.empty 

483 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

484 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

485 
val min_highest_arity = 

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

487 
val min_univ_card = 

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

34126  489 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  490 
val _ = check_arity min_univ_card min_highest_arity 
491 

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

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

494 
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) 
33192  495 
nondef_us 
33745  496 
(* 
33192  497 
val _ = List.app (priority o string_for_nut ctxt) 
498 
(free_names @ sel_names @ nonsel_names @ 

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

499 
nondef_us @ def_us) 
33745  500 
*) 
33192  501 
val (free_rels, pool, rel_table) = 
502 
rename_free_vars free_names initial_pool NameTable.empty 

503 
val (sel_rels, pool, rel_table) = 

504 
rename_free_vars sel_names pool rel_table 

505 
val (other_rels, pool, rel_table) = 

506 
rename_free_vars nonsel_names pool rel_table 

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

507 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 
33192  508 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

509 
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

510 
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

511 
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

512 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
33192  513 
PrintMode.setmp [] multiline_string_for_scope scope 
34998  514 
val kodkod_sat_solver = 
35177  515 
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

516 
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

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

520 
> unsound_delay_for_timeout 
33192  521 
else 
522 
0 

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

524 
("skolem_depth", "1"), 

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

525 
("bit_width", string_of_int bit_width), 
33192  526 
("symmetry_breaking", signed_string_of_int sym_break), 
527 
("sharing", signed_string_of_int sharing_depth), 

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

529 
("delay", signed_string_of_int delay)] 

530 
val plain_rels = free_rels @ other_rels 

531 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

532 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

533 
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

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

535 
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

536 
rel_table datatypes 
33192  537 
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

538 
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

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

540 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
33192  541 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 
542 
univ_card nat_card int_card main_j0 formula 

543 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

544 
> not debug ? merge_bounds 

545 
val highest_arity = 

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

547 
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

548 
val _ = if bits = 0 then () else check_bits bits formula 
34126  549 
val _ = if formula = KK.False then () 
33192  550 
else check_arity univ_card highest_arity 
551 
in 

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

553 
tuple_assigns = [], bounds = bounds, 

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

554 
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

555 
else pow_of_two_int_bounds bits main_j0, 
33192  556 
expr_assigns = [], formula = formula}, 
557 
{free_names = free_names, sel_names = sel_names, 

558 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

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

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

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

563 
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

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

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

566 
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

567 
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

568 
ofs = Typtab.empty} 
33192  569 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
570 
\problem_for_scope" then 

571 
NONE 

572 
else 

573 
(Unsynchronized.change too_big_scopes (cons scope); 

574 
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

575 
". Skipping " ^ (if unsound then "potential" 
33192  576 
else "genuine") ^ 
577 
" component of scope.")); 

578 
NONE) 

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

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

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

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

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

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

584 
NONE) 
33192  585 

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

586 
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

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

588 
> not standard ? prefix "nonstandard " 
33192  589 

590 
val scopes = Unsynchronized.ref [] 

591 
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

592 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  593 
val checked_problems = Unsynchronized.ref (SOME []) 
594 
val met_potential = Unsynchronized.ref 0 

595 

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

597 
fun update_checked_problems problems = 

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

599 
o nth problems) 

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

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

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

602 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  603 

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

604 
(* bool > KK.raw_bound list > problem_extension > bool * bool option *) 
33192  605 
fun print_and_check_model genuine bounds 
606 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

607 
: problem_extension) = 

608 
let 

609 
val (reconstructed_model, codatatypes_ok) = 

610 
reconstruct_hol_model {show_skolems = show_skolems, 

611 
show_datatypes = show_datatypes, 

612 
show_consts = show_consts} 

613 
scope formats frees free_names sel_names nonsel_names rel_table 

614 
bounds 

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

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

616 
got_all_user_axioms andalso none_true wfs andalso 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

617 
sound_finitizes andalso codatatypes_ok 
33192  618 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

620 
[Pretty.blk (0, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

621 
(pstrs ("Nitpick found a" ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

622 
(if not genuine then " potential " 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

623 
else if genuine_means_genuine then " " 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

624 
else " quasi genuine ") ^ das_wort_model) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

625 
(case pretties_for_scope scope verbose of 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

627 
 pretties => pstrs " for " @ pretties) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

628 
[Pretty.str ":\n"])), 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

629 
Pretty.indent indent_size reconstructed_model]); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

630 
if genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

631 
(if check_genuine andalso standard then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

632 
case prove_hol_model scope tac_timeout free_names sel_names 
33192  633 
rel_table bounds assms_t of 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

635 
print ("Confirmation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

638 
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

639 
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

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

641 
\happen.\nPlease send a bug report to blanchet\ 
33192  642 
\te@in.tum.de.") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

644 
print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

645 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

646 
 NONE => print "No confirmation by \"auto\"." 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

649 
if not standard andalso likely_in_struct_induct_step then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

650 
print "The existence of a nonstandard model suggests that the \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

651 
\induction hypothesis is not general enough or perhaps \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

652 
\even wrong. See the \"Inductive Properties\" section of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

653 
\the Nitpick manual for details (\"isabelle doc nitpick\")." 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

656 
if has_syntactic_sorts orig_t then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

657 
print "Hint: Maybe you forgot a type constraint?" 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

660 
if not genuine_means_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

661 
if no_poly_user_axioms then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

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

665 
? cons ("user_axioms", "\"true\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

667 
? cons ("wf", "\"smart\" or \"false\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

669 
? cons ("finitize", "\"smart\" or \"false\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

671 
? cons ("bisim_depth", "a nonnegative value") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

673 
map (fn (name, value) => quote name ^ " set to " ^ value) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

676 
print ("Try again with " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

678 
" to confirm that the " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

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

682 
print ("Nitpick is unable to guarantee the authenticity of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

683 
\the " ^ das_wort_model ^ " in the presence of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

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

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

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

689 
if not genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

691 
if check_potential then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

693 
val status = prove_hol_model scope tac_timeout free_names 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

694 
sel_names rel_table bounds assms_t 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

697 
SOME true => print ("Confirmation by \"auto\": The \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

698 
\above " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

700 
 SOME false => print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

701 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

702 
 NONE => print "No confirmation by \"auto\"."); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

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

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

706 
NONE) 
33192  707 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

709 
> pair genuine_means_genuine 
33192  710 
end 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

711 
(* bool * int * int * int > bool > rich_problem list 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

712 
> bool * int * int * int *) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

713 
fun solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

714 
donno) first_time problems = 
33192  715 
let 
716 
val max_potential = Int.max (0, max_potential) 

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

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

718 
(* bool > int * KK.raw_bound list > bool * bool option *) 
33192  719 
fun print_and_check genuine (j, bounds) = 
720 
print_and_check_model genuine bounds (snd (nth problems j)) 

721 
val max_solutions = max_potential + max_genuine 

722 
> not need_incremental ? curry Int.min 1 

723 
in 

724 
if max_solutions <= 0 then 

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

725 
(found_really_genuine, 0, 0, donno) 
33192  726 
else 
34126  727 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
728 
(map fst problems) of 

729 
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

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

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

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

733 
(update_checked_problems problems unsat_js; show_kodkod_warning s; 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

735 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  736 
let 
737 
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

738 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  739 
in 
740 
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

741 
show_kodkod_warning s; 
33192  742 
if null con_ps then 
743 
let 

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

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

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

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

747 
> filter (curry (op =) (SOME true) o snd) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

749 
found_really_genuine orelse exists fst genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

750 
val num_genuine = length genuine_codes 
33192  751 
val max_genuine = max_genuine  num_genuine 
752 
val max_potential = max_potential 

753 
 (length lib_ps  num_genuine) 

754 
in 

755 
if max_genuine <= 0 then 

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

756 
(found_really_genuine, 0, 0, donno) 
33192  757 
else 
758 
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

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

760 
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

761 
probably can't be satisfied themselves. *) 
33192  762 
val co_js = 
763 
map (fn j => j  1) unsat_js 

764 
> filter (fn j => 

765 
j >= 0 andalso 

766 
scopes_equivalent 

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

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

769 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

770 
unsat_js @ co_js) 

771 
val problems = 

772 
problems > filter_out_indices bye_js 

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

774 
? filter_out (#unsound o snd) 
33192  775 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

776 
solve_any_problem (found_really_genuine, max_potential, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

777 
max_genuine, donno) false problems 
33192  778 
end 
779 
end 

780 
else 

781 
let 

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

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

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

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

785 
val max_genuine = max_genuine  length genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

787 
found_really_genuine orelse exists fst genuine_codes 
33192  788 
in 
789 
if max_genuine <= 0 orelse not first_time then 

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

790 
(found_really_genuine, 0, max_genuine, donno) 
33192  791 
else 
792 
let 

793 
val bye_js = sort_distinct int_ord 

794 
(map fst sat_ps @ unsat_js) 

795 
val problems = 

796 
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

797 
> filter_out (#unsound o snd) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

799 
solve_any_problem (found_really_genuine, 0, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

801 
end 
33192  802 
end 
803 
end 

34126  804 
 KK.TimedOut unsat_js => 
33192  805 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  806 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
807 
 KK.Interrupted (SOME unsat_js) => 

33192  808 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  809 
 KK.Error (s, unsat_js) => 
33192  810 
(update_checked_problems problems unsat_js; 
811 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

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

812 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  813 
end 
814 

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

815 
(* int > int > scope list > bool * int * int * int 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

816 
> bool * int * int * int *) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

817 
fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

818 
donno) = 
33192  819 
let 
820 
val _ = 

821 
if null scopes then 

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

823 
else if verbose then 

824 
pprint (Pretty.chunks 

825 
[Pretty.blk (0, 

826 
pstrs ((if n > 1 then 

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

828 
signed_string_of_int n ^ ": " 

829 
else 

830 
"") ^ 

831 
"Trying " ^ string_of_int (length scopes) ^ 

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

833 
Pretty.indent indent_size 

834 
(Pretty.chunks (map2 

835 
(fn j => fn scope => 

836 
Pretty.block ( 

837 
(case pretties_for_scope scope true of 

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

839 
 pretties => pretties) @ 

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

841 
(length scopes downto 1) scopes))]) 

842 
else 

843 
() 

844 
(* scope * bool > rich_problem list * bool 

845 
> rich_problem list * bool *) 

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

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

848 
case problem_for_scope unsound scope of 
33192  849 
SOME problem => 
850 
(problems 

851 
> (null problems orelse 

34126  852 
not (KK.problems_equivalent (fst problem) 
853 
(fst (hd problems)))) 

33192  854 
? cons problem, donno) 
855 
 NONE => (problems, donno + 1)) 

856 
val (problems, donno) = 

857 
fold add_problem_for_scope 

858 
(map_product pair scopes 

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

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

861 
([], donno) 

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

863 
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

864 
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

865 
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

866 
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

867 
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

868 
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

869 
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

870 
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

871 
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

872 
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

873 
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

874 
"Warning: The conjecture either trivially holds for the \ 
35384  875 
\given scopes or lies outside Nitpick's supported \ 
876 
\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

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

878 
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

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

880 
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

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

882 
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

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

884 
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

885 
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

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

888 
solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

889 
donno) true (rev problems) 
33192  890 
end 
891 

892 
(* rich_problem list > scope > int *) 

893 
fun scope_count (problems : rich_problem list) scope = 

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

895 
(* string > string *) 

896 
fun excipit did_so_and_so = 

897 
let 

898 
(* rich_problem list > rich_problem list *) 

899 
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

900 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  901 
else I 
902 
val total = length (!scopes) 

903 
val unsat = 

904 
fold (fn scope => 

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

906 
0 => I 

907 
 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

908 
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

909 
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

910 
? Integer.add 1) (!generated_scopes) 0 
33192  911 
in 
912 
"Nitpick " ^ did_so_and_so ^ 

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

914 
" after checking " ^ 

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

916 
string_of_int total ^ " scope" ^ plural_s total 

917 
else 

918 
"") ^ "." 

919 
end 

920 

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

921 
(* int > int > scope list > bool * int * int * int > KK.outcome *) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

923 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  924 
if donno > 0 andalso max_genuine > 0 then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

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

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

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

933 
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

934 
"")); "none") 
33192  935 
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

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

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

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

939 
else "ny better " ^ das_wort_model ^ "s.")); "potential") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

940 
else if found_really_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

941 
"genuine" 
33192  942 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

943 
"quasi_genuine" 
33192  944 
 run_batches j n (batch :: batches) z = 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

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

948 

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

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

950 
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

951 
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

952 
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

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

954 
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

955 
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

956 
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

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

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

959 
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

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

961 
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

962 

33192  963 
val batches = batch_list batch_size (!scopes) 
964 
val outcome_code = 

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

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

966 
(false, max_potential, max_genuine, 0) 
33192  967 
handle Exn.Interrupt => do_interrupted ()) 
968 
handle TimeLimit.TimeOut => 

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

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

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

972 
else error (excipit "was interrupted") 

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

974 
signed_string_of_int (Time.toMilliseconds 

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

976 
in (outcome_code, !state_ref) end 

977 
handle Exn.Interrupt => 

978 
if auto orelse #debug params then 

979 
raise Interrupt 

980 
else 

981 
if passed_deadline deadline then 

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

983 
else 

984 
error "Nitpick was interrupted." 

985 

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

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

990 
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

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

992 
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

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

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

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

996 
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

997 
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

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

1000 
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

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

1002 
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

1003 
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

1004 
end 
33192  1005 

35335  1006 
(* string list > term > bool *) 
1007 
fun is_fixed_equation fixes 

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

1009 
member (op =) fixes s 

1010 
 is_fixed_equation _ _ = false 

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

1012 
fun extract_fixed_frees ctxt (assms, t) = 

1013 
let 

1014 
val fixes = Variable.fixes_of ctxt > map snd 

1015 
val (subst, other_assms) = 

1016 
List.partition (is_fixed_equation fixes) assms 

1017 
>> map Logic.dest_equals 

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

1019 

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

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

1021 
fun pick_nits_in_subgoal state params auto i step = 
33192  1022 
let 
1023 
val ctxt = Proof.context_of state 

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

1026 
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

1027 
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

1028 
 n => 
33192  1029 
let 
35335  1030 
val (t, frees) = Logic.goal_params t i 
1031 
val t = subst_bounds (frees, t) 

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

33192  1035 
end 
1036 

1037 
end; 