author  wenzelm 
Fri, 25 Sep 2020 15:40:35 +0200  
changeset 72298  a540283d6b58 
parent 72205  bc71db05abe3 
child 72327  da2cbe54e53e 
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 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

10 
type term_postprocessor = Nitpick_Model.term_postprocessor 
43022  11 

47560  12 
datatype mode = Auto_Try  Try  Normal  TPTP 
43022  13 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

14 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

15 
{cards_assigns: (typ option * int list) list, 
55889  16 
maxes_assigns: ((string * typ) option * int list) list, 
17 
iters_assigns: ((string * typ) option * int list) list, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

18 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

19 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

20 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

21 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

22 
monos: (typ option * bool option) list, 
55889  23 
wfs: ((string * typ) option * bool option) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

24 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

25 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

26 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

27 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

28 
overlord: bool, 
53802  29 
spy: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

30 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

31 
assms: bool, 
38209  32 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

33 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

34 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

35 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

36 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

37 
star_linear_preds: bool, 
41856  38 
total_consts: bool option, 
41876  39 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

40 
peephole_optim: bool, 
38124  41 
datatype_sym_break: int, 
42 
kodkod_sym_break: int, 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

43 
timeout: Time.time, 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

44 
tac_timeout: Time.time, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

45 
max_threads: int, 
55889  46 
show_types: bool, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

47 
show_skolems: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

48 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

49 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

50 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

51 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

52 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

53 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

54 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

55 
expect: string} 
33192  56 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

57 
val genuineN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

58 
val quasi_genuineN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

59 
val potentialN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

60 
val noneN : string 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

61 
val unknownN : string 
33192  62 
val register_frac_type : string > (string * string) list > theory > theory 
63 
val unregister_frac_type : string > theory > theory 

55889  64 
val register_codatatype : typ > string > (string * typ) list > theory > 
65 
theory 

33192  66 
val unregister_codatatype : typ > theory > theory 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

67 
val register_term_postprocessor : 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

68 
typ > term_postprocessor > theory > theory 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

69 
val unregister_term_postprocessor : typ > theory > theory 
33192  70 
val pick_nits_in_term : 
43022  71 
Proof.state > params > mode > int > int > int > (term * term) list 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

72 
> term list > term list > term > string * string list 
33192  73 
val pick_nits_in_subgoal : 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

74 
Proof.state > params > mode > int > int > string * string list 
33192  75 
end; 
76 

77 
structure Nitpick : NITPICK = 

78 
struct 

79 

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

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

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

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

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

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

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

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

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

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

89 
open Nitpick_Model 
33192  90 

34126  91 
structure KK = Kodkod 
92 

47560  93 
datatype mode = Auto_Try  Try  Normal  TPTP 
94 

95 
fun is_mode_nt mode = (mode = Normal orelse mode = TPTP) 

43022  96 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

97 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

98 
{cards_assigns: (typ option * int list) list, 
55889  99 
maxes_assigns: ((string * typ) option * int list) list, 
100 
iters_assigns: ((string * typ) option * int list) list, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

101 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

102 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

103 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

104 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

105 
monos: (typ option * bool option) list, 
55889  106 
wfs: ((string * typ) option * bool option) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

107 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

108 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

109 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

110 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

111 
overlord: bool, 
53802  112 
spy: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

113 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

114 
assms: bool, 
38209  115 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

116 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

117 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

118 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

119 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

120 
star_linear_preds: bool, 
41856  121 
total_consts: bool option, 
41876  122 
needs: term list option, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

123 
peephole_optim: bool, 
38124  124 
datatype_sym_break: int, 
125 
kodkod_sym_break: int, 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

126 
timeout: Time.time, 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

127 
tac_timeout: Time.time, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

128 
max_threads: int, 
55889  129 
show_types: bool, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

130 
show_skolems: bool, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

131 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

132 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

133 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

134 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

135 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

136 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

137 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

138 
expect: string} 
33192  139 

43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

140 
val genuineN = "genuine" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

141 
val quasi_genuineN = "quasi_genuine" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

142 
val potentialN = "potential" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

143 
val noneN = "none" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

144 
val unknownN = "unknown" 
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

145 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

146 
(* TODO: eliminate these historical aliases *) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

147 
val register_frac_type = Nitpick_HOL.register_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

148 
val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

149 
val register_codatatype = Nitpick_HOL.register_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

150 
val unregister_codatatype = Nitpick_HOL.unregister_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

151 
val register_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

152 
Nitpick_Model.register_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

153 
val unregister_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

154 
Nitpick_Model.unregister_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

155 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

156 
type problem_extension = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

157 
{free_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

158 
sel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

159 
nonsel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

160 
rel_table: nut NameTable.table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

161 
unsound: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

162 
scope: scope} 
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
38857
diff
changeset

163 

34126  164 
type rich_problem = KK.problem * problem_extension 
33192  165 

166 
fun pretties_for_formulas _ _ [] = [] 

167 
 pretties_for_formulas ctxt s ts = 

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

169 
Pretty.indent indent_size (Pretty.chunks 

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

171 
Pretty.block [t > shorten_names_in_term 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

172 
> Syntax.pretty_term ctxt]) 
33192  173 
(length ts downto 1) ts))] 
174 

49024  175 
val isabelle_wrong_message = 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

176 
"something appears to be wrong with your Isabelle installation" 
55889  177 
val java_not_found_message = 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

178 
"Java could not be launched  " ^ isabelle_wrong_message 
55889  179 
val kodkodi_not_installed_message = 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

180 
"Nitpick requires the external Java program Kodkodi" 
55889  181 

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

182 
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

183 
val max_unsound_delay_percent = 2 
33192  184 

54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

185 
fun unsound_delay_for_timeout timeout = 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

186 
Int.max (0, Int.min (max_unsound_delay_ms, 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

187 
Time.toMilliseconds timeout 
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

188 
* max_unsound_delay_percent div 100)) 
33192  189 

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

190 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  191 

69597  192 
fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> 
193 
$ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true 

41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

194 
 has_lonely_bool_var _ = false 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

195 

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

196 
val syntactic_sorts = 
69593  197 
\<^sort>\<open>{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}\<close> @ 
198 
\<^sort>\<open>numeral\<close> 

55889  199 

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

200 
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

201 
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

202 
 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

203 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  204 

59432  205 
fun plazy f = Pretty.para (f ()) 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

206 

43022  207 
fun pick_them_nits_in_term deadline state (params : params) mode i n step 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

208 
subst def_assm_ts nondef_assm_ts orig_t = 
33192  209 
let 
62519  210 
val time_start = Time.now () 
33192  211 
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

212 
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

213 
val ctxt = Proof.context_of state 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58892
diff
changeset

214 
val keywords = Thy_Header.get_keywords thy 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

216 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37213
diff
changeset

217 
val nitpick_thy = Thy_Info.get_theory "Nitpick" 
60948  218 
val _ = Context.subthy (nitpick_thy, thy) orelse 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

219 
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

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

221 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
55888  222 
boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose, 
223 
overlord, spy, user_axioms, assms, whacks, merge_type_vars, 

38209  224 
binary_ints, destroy_constrs, specialize, star_linear_preds, 
41875  225 
total_consts, needs, peephole_optim, datatype_sym_break, 
55889  226 
kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems, 
227 
show_consts, evals, formats, atomss, max_potential, max_genuine, 

60310  228 
batch_size, ...} = params 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

229 
val outcome = Synchronized.var "Nitpick.outcome" (Queue.empty: string Queue.T) 
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

230 
fun pprint print prt = 
43022  231 
if mode = Auto_Try then 
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
58928
diff
changeset

232 
Synchronized.change outcome (Queue.enqueue (Pretty.string_of prt)) 
33192  233 
else 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

234 
print (Pretty.string_of prt) 
58843  235 
val pprint_a = pprint writeln 
236 
fun pprint_nt f = () > is_mode_nt mode ? pprint writeln o f 

237 
fun pprint_v f = () > verbose ? pprint writeln o f 

46086  238 
fun pprint_d f = () > debug ? pprint tracing o f 
59432  239 
val print = pprint writeln o Pretty.para 
47560  240 
fun print_t f = () > mode = TPTP ? print o f 
39345  241 
(* 
46086  242 
val print_g = pprint tracing o Pretty.str 
39345  243 
*) 
47560  244 
val print_nt = pprint_nt o K o plazy 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

245 
val print_v = pprint_v o K o plazy 
33192  246 

247 
fun check_deadline () = 

62519  248 
let val t = Time.now () in 
249 
if Time.compare (t, deadline) <> LESS 

62826  250 
then raise Timeout.TIMEOUT (t  time_start) 
62519  251 
else () 
252 
end 

33192  253 

47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

254 
val (def_assm_ts, nondef_assm_ts) = 
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

255 
if assms orelse mode <> Normal then (def_assm_ts, nondef_assm_ts) 
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

256 
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

257 
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

258 
if step = 0 then 
47560  259 
print_nt (fn () => "Nitpicking formula...") 
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

260 
else 
47560  261 
pprint_nt (fn () => Pretty.chunks ( 
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

262 
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

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

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

265 
else 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

266 
"goal")) [Logic.list_implies (nondef_assm_ts, orig_t)])) 
69593  267 
val _ = spying spy (fn () => (state, i, "starting " ^ \<^make_string> mode ^ " mode")) 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

268 
val _ = print_v (prefix "Timestamp: " o Date.fmt "%H:%M:%S" 
41278
8e1cde88aae6
added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents:
41052
diff
changeset

269 
o Date.fromTimeLocal o Time.now) 
69593  270 
val neg_t = if falsify then Logic.mk_implies (orig_t, \<^prop>\<open>False\<close>) 
33192  271 
else orig_t 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

272 
val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

273 
val tfree_table = 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

274 
if merge_type_vars then merged_type_var_table_for_terms thy conj_ts 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

275 
else [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

276 
val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

277 
val neg_t = neg_t > merge_tfrees 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

278 
val def_assm_ts = def_assm_ts > map merge_tfrees 
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

279 
val nondef_assm_ts = nondef_assm_ts > map merge_tfrees 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

280 
val evals = evals > map merge_tfrees 
41876  281 
val needs = needs > Option.map (map merge_tfrees) 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

282 
val conj_ts = neg_t :: def_assm_ts @ nondef_assm_ts @ evals @ these needs 
33192  283 
val original_max_potential = max_potential 
284 
val original_max_genuine = max_genuine 

285 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

55888  286 
val case_names = case_const_names ctxt 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

287 
val defs = def_assm_ts @ all_defs_of thy subst 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

288 
val nondefs = all_nondefs_of ctxt subst 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

289 
val def_tables = const_def_tables ctxt subst defs 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

290 
val nondef_table = const_nondef_table nondefs 
35335  291 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
292 
val psimp_table = const_psimp_table ctxt subst 

35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

293 
val choice_spec_table = const_choice_spec_table ctxt subst 
42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

294 
val nondefs = 
59970  295 
nondefs > filter_out (is_choice_spec_axiom ctxt choice_spec_table) 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

296 
val intro_table = inductive_intro_table ctxt subst def_tables 
33192  297 
val ground_thm_table = ground_theorem_table thy 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

298 
val ersatz_table = ersatz_table ctxt 
41007
75275c796b46
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout  this becomes necessary with the new, more powerful monotonicity calculus
blanchet
parents:
41001
diff
changeset

299 
val hol_ctxt as {wf_cache, ...} = 
33192  300 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
55888  301 
wfs = wfs, user_axioms = user_axioms, debug = debug, whacks = whacks, 
302 
binary_ints = binary_ints, destroy_constrs = destroy_constrs, 

303 
specialize = specialize, star_linear_preds = star_linear_preds, 

304 
total_consts = total_consts, needs = needs, tac_timeout = tac_timeout, 

305 
evals = evals, case_names = case_names, def_tables = def_tables, 

42415
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

306 
nondef_table = nondef_table, nondefs = nondefs, simp_table = simp_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

307 
psimp_table = psimp_table, choice_spec_table = choice_spec_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

308 
intro_table = intro_table, ground_thm_table = ground_thm_table, 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

309 
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], 
10accf397ab6
use "Spec_Rules" for finding axioms  more reliable and cleaner
blanchet
parents:
42361
diff
changeset

310 
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

311 
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

312 
constr_cache = Unsynchronized.ref []} 
41789
7c7b68b06c1a
don't distinguish between "fixes" and other free variables  this confuses users
blanchet
parents:
41772
diff
changeset

313 
val pseudo_frees = [] 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

314 
val real_frees = fold Term.add_frees conj_ts [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

315 
val _ = null (fold Term.add_tvars conj_ts []) orelse 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

316 
error "Nitpick cannot handle goals with schematic type variables" 
41875  317 
val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

318 
no_poly_user_axioms, binarize) = 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

319 
preprocess_formulas hol_ctxt nondef_assm_ts neg_t 
33192  320 
val got_all_user_axioms = 
321 
got_all_mono_user_axioms andalso no_poly_user_axioms 

322 

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

47560  324 
pprint_nt (fn () => Pretty.blk (0, 
60023
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

325 
Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @ 
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

326 
[Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @ 
59432  327 
Pretty.text (if wf then 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

328 
"was proved wellfounded; Nitpick can compute it \ 
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

329 
\efficiently" 
33192  330 
else 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

331 
"could not be proved wellfounded; Nitpick might need to \ 
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

332 
\unroll it"))) 
33192  333 
val _ = if verbose then List.app print_wf (!wf_cache) else () 
38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

334 
val das_wort_formula = if falsify then "Negated conjecture" else "Formula" 
33192  335 
val _ = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

336 
pprint_d (fn () => Pretty.chunks 
38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

337 
(pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

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

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

344 

41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

345 
val nondef_us = nondef_ts > map (nut_from_term hol_ctxt Eq) 
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

346 
val def_us = def_ts > map (nut_from_term hol_ctxt DefEq) 
41875  347 
val need_us = need_ts > map (nut_from_term hol_ctxt Eq) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

348 
val (free_names, const_names) = 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

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

350 
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

351 
List.partition (is_sel o nickname_of) const_names 
46114
e6d33b200f42
remove subtlety whose justification got lost in time  the new code is possibly less precise but sounder
blanchet
parents:
46103
diff
changeset

352 
val sound_finitizes = none_true finitizes 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

353 
(* 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

354 
val _ = 
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

355 
List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us @ need_us) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

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

357 

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

358 
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

359 
fun monotonicity_message Ts extra = 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58892
diff
changeset

360 
let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in 
38188  361 
Pretty.blk (0, 
60023
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

362 
Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @ 
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

363 
pretty_serial_commas "and" pretties @ [Pretty.brk 1] @ 
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

364 
Pretty.text ( 
42959  365 
(if none_true monos then 
366 
"passed the monotonicity test" 

367 
else 

368 
(if length pretties = 1 then "is" else "are") ^ 

369 
" considered monotonic") ^ 

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

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

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

372 
fun is_type_fundamentally_monotonic T = 
55890  373 
(is_data_type ctxt T andalso not (is_quot_type ctxt T) andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

374 
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

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

376 
fun is_type_actually_monotonic T = 
62519  377 
Timeout.apply tac_timeout (formulas_monotonic hol_ctxt binarize T) 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53815
diff
changeset

378 
(nondef_ts, def_ts) 
62519  379 
handle Timeout.TIMEOUT _ => false 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

381 
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

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

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

384 
fun is_type_monotonic T = 
33192  385 
unique_scope orelse 
386 
case triple_lookup (type_match thy) monos T of 

387 
SOME (SOME b) => b 

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

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

389 
is_type_actually_monotonic T 
55890  390 
fun is_deep_data_type_finitizable T = 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

391 
triple_lookup (type_match thy) finitizes T = SOME (SOME true) 
69593  392 
fun is_shallow_data_type_finitizable (T as Type (\<^type_name>\<open>fun_box\<close>, _)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

393 
is_type_kind_of_monotonic T 
55890  394 
 is_shallow_data_type_finitizable T = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

395 
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

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

397 
 _ => is_type_kind_of_monotonic T 
55890  398 
fun is_data_type_deep T = 
69593  399 
T = \<^typ>\<open>unit\<close> orelse T = nat_T orelse is_word_type T orelse 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

400 
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

401 
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) 
35408  402 
> sort Term_Ord.typ_ord 
38214  403 
val _ = 
404 
if verbose andalso binary_ints = SOME true andalso 

405 
exists (member (op =) [nat_T, int_T]) all_Ts then 

406 
print_v (K "The option \"binary_ints\" will be ignored because of the \ 

407 
\presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \ 

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

408 
\in the problem") 
38214  409 
else 
410 
() 

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

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

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

414 
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

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

416 
 interesting_mono_Ts => 
38188  417 
pprint_v (K (monotonicity_message interesting_mono_Ts 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

418 
"Nitpick might be able to skip some scopes")) 
33192  419 
else 
420 
() 

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

421 
val (deep_dataTs, shallow_dataTs) = 
55890  422 
all_Ts > filter (is_data_type ctxt) 
423 
> List.partition is_data_type_deep 

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

424 
val finitizable_dataTs = 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

425 
(deep_dataTs > filter_out (is_finite_type hol_ctxt) 
55890  426 
> filter is_deep_data_type_finitizable) @ 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

427 
(shallow_dataTs > filter_out (is_finite_type hol_ctxt) 
55890  428 
> filter is_shallow_data_type_finitizable) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

430 
if verbose andalso not (null finitizable_dataTs) then 
38188  431 
pprint_v (K (monotonicity_message finitizable_dataTs 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

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

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

434 
() 
33192  435 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

436 
val _ = print_g "Monotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

437 
val _ = List.app (print_g o string_for_type ctxt) mono_Ts 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

438 
val _ = print_g "Nonmonotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

439 
val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts 
33192  440 
*) 
441 

36384  442 
val incremental = Int.max (max_potential, max_genuine) >= 2 
443 
val actual_sat_solver = 

33192  444 
if sat_solver <> "smart" then 
36384  445 
if incremental andalso 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

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

447 
sat_solver) then 
47560  448 
(print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \ 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

449 
\be used instead of " ^ quote sat_solver)); 
33192  450 
"SAT4J") 
451 
else 

452 
sat_solver 

453 
else 

36384  454 
Kodkod_SAT.smart_sat_solver_name incremental 
33192  455 
val _ = 
456 
if sat_solver = "smart" then 

36384  457 
print_v (fn () => 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

458 
"Using SAT solver " ^ quote actual_sat_solver ^ "\nThe following" ^ 
36384  459 
(if incremental then " incremental " else " ") ^ 
460 
"solvers are configured: " ^ 

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

461 
commas_quote (Kodkod_SAT.configured_sat_solvers incremental)) 
33192  462 
else 
463 
() 

464 

465 
val too_big_scopes = Unsynchronized.ref [] 

466 

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

467 
fun problem_for_scope unsound 
55890  468 
(scope as {card_assigns, bits, bisim_depth, data_types, ofs, ...}) = 
33192  469 
let 
470 
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

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

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

473 
\problem_for_scope", "too large scope") 
33192  474 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

475 
val _ = print_g "Offsets:" 
33192  476 
val _ = List.app (fn (T, j0) => 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

477 
print_g (string_for_type ctxt T ^ " = " ^ 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

478 
string_of_int j0)) 
33192  479 
(Typtab.dest ofs) 
480 
*) 

41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

481 
val effective_total_consts = 
41856  482 
case total_consts of 
483 
SOME b => b 

55890  484 
 NONE => forall (is_exact_type data_types true) all_Ts 
33192  485 
val main_j0 = offset_of_type ofs bool_T 
486 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

487 
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

488 
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

489 
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

490 
"bad offsets") 
33192  491 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
492 
val (free_names, rep_table) = 

38170  493 
choose_reps_for_free_vars scope pseudo_frees free_names 
494 
NameTable.empty 

33192  495 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 
38170  496 
val (nonsel_names, rep_table) = 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

497 
choose_reps_for_consts scope effective_total_consts nonsel_names 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

498 
rep_table 
38182  499 
val (guiltiest_party, min_highest_arity) = 
500 
NameTable.fold (fn (name, R) => fn (s, n) => 

501 
let val n' = arity_of_rep R in 

502 
if n' > n then (nickname_of name, n') else (s, n) 

503 
end) rep_table ("", 1) 

33192  504 
val min_univ_card = 
36384  505 
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table 
34126  506 
(univ_card nat_card int_card main_j0 [] KK.True) 
52202  507 
val _ = check_arity guiltiest_party min_univ_card min_highest_arity 
33192  508 

41802  509 
val def_us = 
510 
def_us > map (choose_reps_in_nut scope unsound rep_table true) 

511 
val nondef_us = 

512 
nondef_us > map (choose_reps_in_nut scope unsound rep_table false) 

41875  513 
val need_us = 
514 
need_us > map (choose_reps_in_nut scope unsound rep_table false) 

33745  515 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

516 
val _ = List.app (print_g o string_for_nut ctxt) 
33192  517 
(free_names @ sel_names @ nonsel_names @ 
41888
79f837c2e33b
don't forget to look for constants appearing only in "need" option  otherwise we get exceptions in "the_name" later on
blanchet
parents:
41876
diff
changeset

518 
nondef_us @ def_us @ need_us) 
33745  519 
*) 
33192  520 
val (free_rels, pool, rel_table) = 
521 
rename_free_vars free_names initial_pool NameTable.empty 

522 
val (sel_rels, pool, rel_table) = 

523 
rename_free_vars sel_names pool rel_table 

524 
val (other_rels, pool, rel_table) = 

525 
rename_free_vars nonsel_names pool rel_table 

41802  526 
val nondef_us = nondef_us > map (rename_vars_in_nut pool rel_table) 
527 
val def_us = def_us > map (rename_vars_in_nut pool rel_table) 

41875  528 
val need_us = need_us > map (rename_vars_in_nut pool rel_table) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

529 
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

530 
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

531 
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

532 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
72195  533 
multiline_string_for_scope scope 
34998  534 
val kodkod_sat_solver = 
36384  535 
Kodkod_SAT.sat_solver_spec actual_sat_solver > snd 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

536 
val bit_width = if bits = 0 then 16 else bits + 1 
36384  537 
val delay = 
538 
if unsound then 

62826  539 
unsound_delay_for_timeout (deadline  Time.now ()) 
36384  540 
else 
541 
0 

542 
val settings = [("solver", commas_quote kodkod_sat_solver), 

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

543 
("bit_width", string_of_int bit_width), 
38124  544 
("symmetry_breaking", string_of_int kodkod_sym_break), 
36386
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

545 
("sharing", "3"), 
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

546 
("flatten", "false"), 
33192  547 
("delay", signed_string_of_int delay)] 
548 
val plain_rels = free_rels @ other_rels 

549 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

550 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

41995  551 
val need_vals = 
552 
map (fn dtype as {typ, ...} => 

55890  553 
(typ, needed_values_for_data_type need_us ofs dtype)) 
554 
data_types 

41995  555 
val sel_bounds = 
55890  556 
map (bound_for_sel_rel ctxt debug need_vals data_types) sel_rels 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

557 
val dtype_axioms = 
55890  558 
declarative_axioms_for_data_types hol_ctxt binarize need_us need_vals 
559 
datatype_sym_break bits ofs kk rel_table data_types 

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

561 
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

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

563 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
38126  564 
val (built_in_bounds, built_in_axioms) = 
39345  565 
bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card 
566 
nat_card int_card main_j0 (formula :: declarative_axioms) 

33192  567 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 
568 
> not debug ? merge_bounds 

38126  569 
val axioms = built_in_axioms @ declarative_axioms 
33192  570 
val highest_arity = 
571 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

38126  572 
val formula = fold_rev s_and axioms formula 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

573 
val _ = if bits = 0 then () else check_bits bits formula 
52202  574 
val _ = if formula = KK.False then () 
38182  575 
else check_arity "" univ_card highest_arity 
33192  576 
in 
577 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

578 
tuple_assigns = [], bounds = bounds, 

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

579 
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

580 
else pow_of_two_int_bounds bits main_j0, 
33192  581 
expr_assigns = [], formula = formula}, 
582 
{free_names = free_names, sel_names = sel_names, 

583 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

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

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

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

588 
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

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

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

591 
card_assigns = card_assigns, bits = bits, 
55890  592 
bisim_depth = bisim_depth, data_types = data_types, 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

593 
ofs = Typtab.empty} 
33192  594 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
595 
\problem_for_scope" then 

596 
NONE 

597 
else 

598 
(Unsynchronized.change too_big_scopes (cons scope); 

41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

599 
print_v (fn () => 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

600 
"Limit reached: " ^ msg ^ "; skipping " ^ 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

601 
(if unsound then "potential component of " else "") ^ 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

602 
"scope"); 
33192  603 
NONE) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

604 
 TOO_SMALL (_, msg) => 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

605 
(print_v (fn () => 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

606 
"Limit reached: " ^ msg ^ "; skipping " ^ 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

607 
(if unsound then "potential component of " else "") ^ 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

608 
"scope"); 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

609 
NONE) 
33192  610 

55888  611 
val das_wort_model = if falsify then "counterexample" else "model" 
33192  612 

613 
val scopes = Unsynchronized.ref [] 

614 
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

615 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  616 
val checked_problems = Unsynchronized.ref (SOME []) 
617 
val met_potential = Unsynchronized.ref 0 

618 

619 
fun update_checked_problems problems = 

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

621 
o nth problems) 

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

622 
fun show_kodkod_warning "" = () 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

623 
 show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s) 
33192  624 

625 
fun print_and_check_model genuine bounds 

626 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

627 
: problem_extension) = 

628 
let 

47752  629 
val _ = 
630 
print_t (fn () => 

631 
"% SZS status " ^ 

632 
(if genuine then 

633 
if falsify then "CounterSatisfiable" else "Satisfiable" 

634 
else 

61310  635 
"GaveUp") ^ "\n" ^ 
47752  636 
"% SZS output start FiniteModel") 
33192  637 
val (reconstructed_model, codatatypes_ok) = 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

638 
reconstruct_hol_model 
55889  639 
{show_types = show_types, show_skolems = show_skolems, 
41993
bd6296de1432
reintroduced "show_skolems" option  useful when too many Skolems are displayed
blanchet
parents:
41992
diff
changeset

640 
show_consts = show_consts} 
38170  641 
scope formats atomss real_frees pseudo_frees free_names sel_names 
642 
nonsel_names rel_table 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

643 
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

644 
got_all_user_axioms andalso none_true wfs andalso 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

645 
sound_finitizes andalso total_consts <> SOME true andalso 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

646 
codatatypes_ok 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

647 
fun assms_prop () = 
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

648 
Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts) 
33192  649 
in 
47752  650 
(pprint_a (Pretty.chunks 
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

651 
[Pretty.blk (0, 
59432  652 
(Pretty.text ((if mode = Auto_Try then "Auto " else "") ^ 
43022  653 
"Nitpick found a" ^ 
41992
0e4716fa330a
reword Nitpick's wording concerning potential counterexamples
blanchet
parents:
41985
diff
changeset

654 
(if not genuine then " potentially spurious " 
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

655 
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

656 
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

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

658 
[] => [] 
60023
f3e70d74a686
proper Pretty.brk  redundant spaces do not survive Pretty.text (see also 42b7b76b37b8, e06eabc421e7);
wenzelm
parents:
59970
diff
changeset

659 
 pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @ 
72298  660 
[Pretty.str ":"])), 
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

661 
Pretty.indent indent_size reconstructed_model]); 
47564  662 
print_t (K "% SZS output end FiniteModel"); 
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

663 
if genuine then 
60310  664 
(if has_lonely_bool_var orig_t then 
41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

665 
print "Hint: Maybe you forgot a colon after the lemma's name?" 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

666 
else if has_syntactic_sorts orig_t 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

667 
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

668 
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

669 
(); 
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 
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

671 
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

672 
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

673 
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

674 
[] > 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

675 
? 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

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

677 
? 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

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

679 
? cons ("finitize", "\"smart\" or \"false\"") 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

680 
> total_consts = SOME true 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

681 
? cons ("total_consts", "\"smart\" or \"false\"") 
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

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

683 
? 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

684 
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

685 
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

686 
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

687 
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

688 
print ("Try again with " ^ 
41872  689 
space_implode " " (serial_commas "and" ss) ^ 
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

690 
" to confirm that the " ^ das_wort_model ^ 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

691 
" is 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

692 
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

693 
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

694 
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

695 
\the " ^ das_wort_model ^ " in the presence of \ 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

696 
\polymorphic axioms") 
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

697 
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

698 
(); 
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 
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

700 
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

701 
if not genuine then 
60310  702 
(Unsynchronized.inc met_potential; NONE) 
33192  703 
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

704 
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

705 
> pair genuine_means_genuine 
33192  706 
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

707 
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

708 
donno) first_time problems = 
33192  709 
let 
710 
val max_potential = Int.max (0, max_potential) 

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

712 
fun print_and_check genuine (j, bounds) = 

713 
print_and_check_model genuine bounds (snd (nth problems j)) 

714 
val max_solutions = max_potential + max_genuine 

36384  715 
> not incremental ? Integer.min 1 
33192  716 
in 
717 
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

718 
(found_really_genuine, 0, 0, donno) 
33192  719 
else 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

720 
case KK.solve_any_problem debug overlord deadline max_threads 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

721 
max_solutions (map fst problems) of 
49024  722 
KK.JavaNotFound => 
55889  723 
(print_nt (K java_not_found_message); 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

724 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

725 
 KK.KodkodiNotInstalled => 
55889  726 
(print_nt (K kodkodi_not_installed_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

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

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

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

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

731 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  732 
let 
733 
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

734 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  735 
in 
736 
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

737 
show_kodkod_warning s; 
33192  738 
if null con_ps then 
739 
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

740 
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

741 
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

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

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

744 
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

745 
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

746 
val num_genuine = length genuine_codes 
33192  747 
val max_genuine = max_genuine  num_genuine 
748 
val max_potential = max_potential 

749 
 (length lib_ps  num_genuine) 

750 
in 

751 
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

752 
(found_really_genuine, 0, 0, donno) 
33192  753 
else 
754 
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

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

756 
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

757 
probably can't be satisfied themselves. *) 
33192  758 
val co_js = 
759 
map (fn j => j  1) unsat_js 

760 
> filter (fn j => 

761 
j >= 0 andalso 

762 
scopes_equivalent 

35814  763 
(#scope (snd (nth problems j)), 
764 
#scope (snd (nth problems (j + 1))))) 

33192  765 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 
766 
unsat_js @ co_js) 

767 
val problems = 

768 
problems > filter_out_indices bye_js 

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

770 
? filter_out (#unsound o snd) 
33192  771 
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

772 
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

773 
max_genuine, donno) false problems 
33192  774 
end 
775 
end 

776 
else 

777 
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

778 
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

779 
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

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

781 
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

782 
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

783 
found_really_genuine orelse exists fst genuine_codes 
33192  784 
in 
785 
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

786 
(found_really_genuine, 0, max_genuine, donno) 
33192  787 
else 
788 
let 

789 
val bye_js = sort_distinct int_ord 

790 
(map fst sat_ps @ unsat_js) 

791 
val problems = 

792 
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

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

794 
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

795 
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

796 
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

797 
end 
33192  798 
end 
799 
end 

34126  800 
 KK.TimedOut unsat_js => 
62519  801 
(update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime) 
34126  802 
 KK.Error (s, unsat_js) => 
33192  803 
(update_checked_problems problems unsat_js; 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

804 
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

805 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  806 
end 
807 

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

808 
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

809 
donno) = 
33192  810 
let 
811 
val _ = 

812 
if null scopes then 

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

813 
print_nt (K "The scope specification is inconsistent") 
33192  814 
else if verbose then 
47560  815 
pprint_nt (fn () => Pretty.chunks 
33192  816 
[Pretty.blk (0, 
59432  817 
Pretty.text ((if n > 1 then 
33192  818 
"Batch " ^ string_of_int (j + 1) ^ " of " ^ 
819 
signed_string_of_int n ^ ": " 

820 
else 

821 
"") ^ 

822 
"Trying " ^ string_of_int (length scopes) ^ 

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

824 
Pretty.indent indent_size 

825 
(Pretty.chunks (map2 

826 
(fn j => fn scope => 

827 
Pretty.block ( 

828 
(case pretties_for_scope scope true of 

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

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

830 
 pretties => pretties))) 
33192  831 
(length scopes downto 1) scopes))]) 
832 
else 

833 
() 

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

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

836 
case problem_for_scope unsound scope of 
33192  837 
SOME problem => 
838 
(problems 

839 
> (null problems orelse 

35814  840 
not (KK.problems_equivalent (fst problem, fst (hd problems)))) 
33192  841 
? cons problem, donno) 
842 
 NONE => (problems, donno + 1)) 

843 
val (problems, donno) = 

844 
fold add_problem_for_scope 

845 
(map_product pair scopes 

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

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

848 
([], donno) 

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

850 
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

851 
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

852 
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

853 
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

854 
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

855 
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

856 
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

857 
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

858 
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

859 
sound_problems then 
47560  860 
print_nt (fn () => 
44395  861 
"Warning: The conjecture " ^ 
862 
(if falsify then "either trivially holds" 

863 
else "is either trivially unsatisfiable") ^ 

864 
" for the given scopes or lies outside Nitpick's supported \ 

63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

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

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

867 
unsound_problems then 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

868 
"; only potentially spurious " ^ das_wort_model ^ 
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

869 
"s may be found" 
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

870 
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

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

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

874 
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

875 
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

876 
() 
33192  877 
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

878 
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

879 
donno) true (rev problems) 
33192  880 
end 
881 

882 
fun scope_count (problems : rich_problem list) scope = 

35814  883 
length (filter (curry scopes_equivalent scope o #scope o snd) problems) 
33192  884 
fun excipit did_so_and_so = 
885 
let 

886 
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

887 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  888 
else I 
889 
val total = length (!scopes) 

890 
val unsat = 

891 
fold (fn scope => 

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

893 
0 => I 

894 
 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

895 
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

896 
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

897 
? Integer.add 1) (!generated_scopes) 0 
33192  898 
in 
61365  899 
(if mode = TPTP then "% SZS status GaveUp\n" else "") ^ 
33192  900 
"Nitpick " ^ did_so_and_so ^ 
901 
(if is_some (!checked_problems) andalso total > 0 then 

39361  902 
" " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" 
903 
^ plural_s total 

33192  904 
else 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

905 
"") 
33192  906 
end 
907 

37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

908 
val (skipped, the_scopes) = 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

909 
all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

910 
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

911 
finitizable_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

912 
val _ = if skipped > 0 then 
62319  913 
print_nt (fn () => "Skipping " ^ string_of_int skipped ^ 
914 
" scope" ^ plural_s skipped ^ 

47560  915 
". (Consider using \"mono\" or \ 
916 
\\"merge_type_vars\" to prevent this.)") 

37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

917 
else 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

918 
() 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

919 
val _ = scopes := the_scopes 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

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

922 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  923 
if donno > 0 andalso max_genuine > 0 then 
47560  924 
(print_nt (fn () => excipit "checked"); unknownN) 
33192  925 
else if max_genuine = original_max_genuine then 
926 
if max_potential = original_max_potential then 

61365  927 
(print_t (K "% SZS status GaveUp"); 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

928 
print_nt (fn () => "Nitpick found no " ^ das_wort_model); 
55888  929 
if skipped > 0 then unknownN else noneN) 
33192  930 
else 
47560  931 
(print_nt (fn () => 
38123
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

932 
excipit ("could not find a" ^ 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

933 
(if max_genuine = 1 then 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

934 
" better " ^ das_wort_model 
38123
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

935 
else 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

936 
"ny better " ^ das_wort_model ^ "s") ^ 
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

937 
"\nIt checked")); 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

938 
potentialN) 
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

939 
else if found_really_genuine then 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

940 
genuineN 
33192  941 
else 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

942 
quasi_genuineN 
33192  943 
 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

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

947 

48323  948 
val batches = chunk_list batch_size (!scopes) 
33192  949 
val outcome_code = 
40411
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

950 
run_batches 0 (length batches) batches 
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

951 
(false, max_potential, max_genuine, 0) 
62519  952 
handle Timeout.TIMEOUT _ => 
47560  953 
(print_nt (fn () => excipit "ran out of time after checking"); 
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
42959
diff
changeset

954 
if !met_potential > 0 then potentialN else unknownN) 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

955 
val _ = print_v (fn () => 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

956 
"Total time: " ^ string_of_time (Timer.checkRealTimer timer)) 
53815
e8aa538e959e
encode goal digest in spying log (to detect duplicates)
blanchet
parents:
53802
diff
changeset

957 
val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code)) 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

958 
in (outcome_code, Queue.content (Synchronized.value outcome)) end 
33192  959 

41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

960 
(* Give the inner timeout a chance. *) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

961 
val timeout_bonus = seconds 1.0 
41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

962 

55539
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
54816
diff
changeset

963 
fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step 
0819931d652d
simplified data structure by reducing the incidence of clumsy indices
blanchet
parents:
54816
diff
changeset

964 
subst def_assm_ts nondef_assm_ts orig_t = 
47670  965 
let 
58843  966 
val print_nt = if is_mode_nt mode then writeln else K () 
967 
val print_t = if mode = TPTP then writeln else K () 

47670  968 
in 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

969 
if getenv "KODKODI" = "" then 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

970 
(* The "expect" argument is deliberately ignored if Kodkodi is missing so 
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

971 
that the "Nitpick_Examples" can be processed on any machine. *) 
55889  972 
(print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message))); 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

973 
("no_kodkodi", [])) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

974 
else 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

975 
let 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

976 
val unknown_outcome = (unknownN, []) 
62826  977 
val deadline = Time.now () + timeout 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

978 
val outcome as (outcome_code, _) = 
62826  979 
Timeout.apply (timeout + timeout_bonus) 
43022  980 
(pick_them_nits_in_term deadline state params mode i n step subst 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

981 
def_assm_ts nondef_assm_ts) orig_t 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

982 
handle TOO_LARGE (_, details) => 
61365  983 
(print_t "% SZS status GaveUp"; 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

984 
print_nt ("Limit reached: " ^ details); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

985 
 TOO_SMALL (_, details) => 
61365  986 
(print_t "% SZS status GaveUp"; 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

987 
print_nt ("Limit reached: " ^ details); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

988 
 Kodkod.SYNTAX (_, details) => 
61365  989 
(print_t "% SZS status GaveUp"; 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

990 
print_nt ("Malformed Kodkodi output: " ^ details); 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

991 
unknown_outcome) 
62519  992 
 Timeout.TIMEOUT _ => 
47670  993 
(print_t "% SZS status TimedOut"; 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

994 
print_nt "Nitpick ran out of time"; unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

995 
in 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

996 
if expect = "" orelse outcome_code = expect then outcome 
63693
5b02f7757a4c
removed trailing final stops in Nitpick messages
blanchet
parents:
62826
diff
changeset

997 
else error ("Unexpected outcome: " ^ quote outcome_code) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

998 
end 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

999 
end 
33192  1000 

42486  1001 
fun is_fixed_equation ctxt 
69593  1002 
(Const (\<^const_name>\<open>Pure.eq\<close>, _) $ Free (s, _) $ Const _) = 
42486  1003 
Variable.is_fixed ctxt s 
35335  1004 
 is_fixed_equation _ _ = false 
55889  1005 

35335  1006 
fun extract_fixed_frees ctxt (assms, t) = 
1007 
let 

1008 
val (subst, other_assms) = 

42486  1009 
List.partition (is_fixed_equation ctxt) assms 
35335  1010 
>> map Logic.dest_equals 
1011 
in (subst, other_assms, subst_atomic subst t) end 

1012 

43022  1013 
fun pick_nits_in_subgoal state params mode i step = 
33192  1014 
let 
1015 
val ctxt = Proof.context_of state 

59582  1016 
val t = state > Proof.raw_goal > #goal > Thm.prop_of 
33192  1017 
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

1018 
case Logic.count_prems t of 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58843
diff
changeset

1019 
0 => (writeln "No subgoal!"; (noneN, [])) 
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 
 n => 
33192  1021 
let 
36406  1022 
val t = Logic.goal_params t i > fst 
59582  1023 
val assms = map Thm.term_of (Assumption.all_assms_of ctxt) 
35335  1024 
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) 
47715
04400144c6fc
handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents:
47670
diff
changeset

1025 
in pick_nits_in_term state params mode i n step subst [] assms t end 
33192  1026 
end 
1027 

1028 
end; 