author  blanchet 
Sun, 25 Apr 2010 00:25:44 +0200  
changeset 36390  eee4ee6a5cbe 
parent 36389  8228b3a4a2ba 
child 36397  2a5c6e7b55cb 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Finite model generation for HOL formulas using Kodkod. 

6 
*) 

7 

8 
signature NITPICK = 

9 
sig 

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

10 
type styp = Nitpick_Util.styp 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

11 
type term_postprocessor = Nitpick_Model.term_postprocessor 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

13 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

14 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

15 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

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

22 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

24 
blocking: bool, 
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, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

44 
formats: (term option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

50 
expect: string} 
33192  51 

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

53 
val unregister_frac_type : string > theory > theory 

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

55 
val unregister_codatatype : typ > theory > theory 

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

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

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

58 
val unregister_term_postprocessor : typ > theory > theory 
33192  59 
val pick_nits_in_term : 
35335  60 
Proof.state > params > bool > int > int > int > (term * term) list 
61 
> term list > term > string * Proof.state 

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

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

66 
structure Nitpick : NITPICK = 

67 
struct 

68 

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

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

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

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

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

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

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

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

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

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

78 
open Nitpick_Model 
33192  79 

34126  80 
structure KK = Kodkod 
81 

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

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

83 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

84 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

85 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

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

92 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

114 
formats: (term option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

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

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

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

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

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

120 
expect: string} 
33192  121 

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

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

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

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

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

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

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

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

129 

34126  130 
type rich_problem = KK.problem * problem_extension 
33192  131 

132 
fun pretties_for_formulas _ _ [] = [] 

133 
 pretties_for_formulas ctxt s ts = 

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

135 
Pretty.indent indent_size (Pretty.chunks 

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

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

140 
(length ts downto 1) ts))] 

141 

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

142 
fun install_java_message () = 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

143 
"Nitpick requires a Java 1.5 virtual machine called \"java\"." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

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

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

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

149 
(Path.variable "ISABELLE_HOME_USER" :: 
36266  150 
map Path.basic ["etc", "components"]))) ^ "\" on a line of its own." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

151 

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

152 
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

153 
val max_unsound_delay_percent = 2 
33192  154 

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

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

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

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

159 
* max_unsound_delay_percent div 100)) 
33192  160 

161 
fun passed_deadline NONE = false 

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

163 

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

164 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  165 

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

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

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

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

169 
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

170 
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

171 
 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

172 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  173 

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

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

175 

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

176 
fun pick_them_nits_in_term deadline state (params : params) auto i n step 
35335  177 
subst orig_assm_ts orig_t = 
33192  178 
let 
179 
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

180 
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

181 
val ctxt = Proof.context_of state 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

183 

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

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

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

186 
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

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

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

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

190 
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints, 
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

191 
destroy_constrs, specialize, star_linear_preds, fast_descrs, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

192 
peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

193 
evals, formats, max_potential, max_genuine, check_potential, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

194 
check_genuine, batch_size, ...} = params 
33192  195 
val state_ref = Unsynchronized.ref state 
196 
val pprint = 

197 
if auto then 

198 
Unsynchronized.change state_ref o Proof.goal_message o K 

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

199 
o Pretty.chunks o cons (Pretty.str "") o single 
33192  200 
o Pretty.mark Markup.hilite 
201 
else 

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

202 
(fn s => (priority s; if debug then tracing s else ())) 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

203 
o Pretty.string_of 
33192  204 
fun pprint_m f = () > not auto ? pprint o f 
205 
fun pprint_v f = () > verbose ? pprint o f 

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

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

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

208 
val print_g = pprint o Pretty.str 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

210 
val print_v = pprint_v o K o plazy 
33192  211 

212 
fun check_deadline () = 

213 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut 

214 
else () 

215 
fun do_interrupted () = 

216 
if passed_deadline deadline then raise TimeLimit.TimeOut 

217 
else raise Interrupt 

218 

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

220 
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

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

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

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

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

225 
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

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

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

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

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

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

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

235 
> pairf hd tl 
33192  236 
val original_max_potential = max_potential 
237 
val original_max_genuine = max_genuine 

238 
(* 

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

239 
val _ = print_g ("*** " ^ Syntax.string_of_term ctxt orig_t) 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

240 
val _ = List.app (fn t => print_g ("*** " ^ Syntax.string_of_term ctxt t)) 
33192  241 
orig_assm_ts 
242 
*) 

243 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

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

244 
val case_names = case_const_names thy stds 
35335  245 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy subst 
246 
val def_table = const_def_table ctxt subst defs 

33192  247 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 
35335  248 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
249 
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

250 
val choice_spec_table = const_choice_spec_table ctxt subst 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

251 
val user_nondefs = 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

252 
user_nondefs > filter_out (is_choice_spec_axiom thy choice_spec_table) 
35335  253 
val intro_table = inductive_intro_table ctxt subst def_table 
33192  254 
val ground_thm_table = ground_theorem_table thy 
255 
val ersatz_table = ersatz_table thy 

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

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

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

259 
binary_ints = binary_ints, destroy_constrs = destroy_constrs, 
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

260 
specialize = specialize, star_linear_preds = star_linear_preds, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

261 
fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

262 
case_names = case_names, def_table = def_table, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

263 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

264 
simp_table = simp_table, psimp_table = psimp_table, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

265 
choice_spec_table = choice_spec_table, intro_table = intro_table, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

266 
ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, 
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset

267 
skolems = Unsynchronized.ref [], 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

268 
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

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

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

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

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

274 
binarize) = preprocess_term hol_ctxt finitizes monos assms_t 
33192  275 
val got_all_user_axioms = 
276 
got_all_mono_user_axioms andalso no_poly_user_axioms 

277 

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

279 
pprint (Pretty.blk (0, 

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

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

282 
pstrs (if wf then 

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

284 
\efficiently." 

285 
else 

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

287 
\unroll it."))) 

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

289 
val _ = 

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

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

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

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

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

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

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

298 

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

299 
val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

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

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

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

303 
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

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

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

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

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

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

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

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

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

312 

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

313 
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

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

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

316 
"The type" ^ plural_s_for_list ss ^ " " ^ 
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
36266
diff
changeset

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

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

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

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

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

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

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

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

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

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

328 
fun is_type_actually_monotonic T = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

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

331 
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

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

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

334 
fun is_type_monotonic T = 
33192  335 
unique_scope orelse 
336 
case triple_lookup (type_match thy) monos T of 

337 
SOME (SOME b) => b 

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

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

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

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

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

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

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

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

345 
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

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

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

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

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

350 
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

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

353 
val _ = if verbose andalso binary_ints = SOME true andalso 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

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

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

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

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

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

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

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

364 
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

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

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

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

368 
"Nitpick might be able to skip some scopes.")) 
33192  369 
else 
370 
() 

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

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

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

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

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

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

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

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

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

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

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

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

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

383 
provide a hint to the user. *) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

401 
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

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

403 
val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts 
33192  404 
*) 
405 

36384  406 
val incremental = Int.max (max_potential, max_genuine) >= 2 
407 
val actual_sat_solver = 

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

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

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

414 
"SAT4J") 

415 
else 

416 
sat_solver 

417 
else 

36384  418 
Kodkod_SAT.smart_sat_solver_name incremental 
33192  419 
val _ = 
420 
if sat_solver = "smart" then 

36384  421 
print_v (fn () => 
422 
"Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^ 

423 
(if incremental then " incremental " else " ") ^ 

424 
"solvers are configured: " ^ 

425 
commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".") 

33192  426 
else 
427 
() 

428 

429 
val too_big_scopes = Unsynchronized.ref [] 

430 

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

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

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

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

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

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

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

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

442 
string_of_int j0)) 
33192  443 
(Typtab.dest ofs) 
444 
*) 

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

445 
val all_exact = forall (is_exact_type datatypes true) all_Ts 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

446 
val repify_consts = choose_reps_for_consts scope all_exact 
33192  447 
val main_j0 = offset_of_type ofs bool_T 
448 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

449 
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

450 
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

451 
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

452 
"bad offsets") 
33192  453 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
454 
val (free_names, rep_table) = 

455 
choose_reps_for_free_vars scope free_names NameTable.empty 

456 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

457 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

458 
val min_highest_arity = 

36384  459 
NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1 
33192  460 
val min_univ_card = 
36384  461 
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table 
34126  462 
(univ_card nat_card int_card main_j0 [] KK.True) 
33192  463 
val _ = check_arity min_univ_card min_highest_arity 
464 

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

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

467 
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false) 
33192  468 
nondef_us 
33745  469 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

470 
val _ = List.app (print_g o string_for_nut ctxt) 
33192  471 
(free_names @ sel_names @ nonsel_names @ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

472 
nondef_us @ def_us) 
33745  473 
*) 
33192  474 
val (free_rels, pool, rel_table) = 
475 
rename_free_vars free_names initial_pool NameTable.empty 

476 
val (sel_rels, pool, rel_table) = 

477 
rename_free_vars sel_names pool rel_table 

478 
val (other_rels, pool, rel_table) = 

479 
rename_free_vars nonsel_names pool rel_table 

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

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

482 
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

483 
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

484 
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

485 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
33192  486 
PrintMode.setmp [] multiline_string_for_scope scope 
34998  487 
val kodkod_sat_solver = 
36384  488 
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

489 
val bit_width = if bits = 0 then 16 else bits + 1 
36384  490 
val delay = 
491 
if unsound then 

492 
Option.map (fn time => Time. (time, Time.now ())) deadline 

493 
> unsound_delay_for_timeout 

494 
else 

495 
0 

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

33192  497 
("skolem_depth", "1"), 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

498 
("bit_width", string_of_int bit_width), 
36386
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

499 
("symmetry_breaking", "20"), 
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

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

501 
("flatten", "false"), 
33192  502 
("delay", signed_string_of_int delay)] 
503 
val plain_rels = free_rels @ other_rels 

504 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

505 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

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

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

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

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

509 
rel_table datatypes 
33192  510 
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

511 
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

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

513 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
33192  514 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 
515 
univ_card nat_card int_card main_j0 formula 

516 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

517 
> not debug ? merge_bounds 

518 
val highest_arity = 

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

520 
val formula = fold_rev s_and declarative_axioms formula 

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

521 
val _ = if bits = 0 then () else check_bits bits formula 
34126  522 
val _ = if formula = KK.False then () 
33192  523 
else check_arity univ_card highest_arity 
524 
in 

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

526 
tuple_assigns = [], bounds = bounds, 

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

527 
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

528 
else pow_of_two_int_bounds bits main_j0, 
33192  529 
expr_assigns = [], formula = formula}, 
530 
{free_names = free_names, sel_names = sel_names, 

531 
nonsel_names = nonsel_names, rel_table = rel_table, 

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

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

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

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

536 
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

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

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

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

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

541 
ofs = Typtab.empty} 
33192  542 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
543 
\problem_for_scope" then 

544 
NONE 

545 
else 

546 
(Unsynchronized.change too_big_scopes (cons scope); 

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

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

548 
". Skipping " ^ (if unsound then "potential" 
33192  549 
else "genuine") ^ 
550 
" component of scope.")); 

551 
NONE) 

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

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

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

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

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

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

557 
NONE) 
33192  558 

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

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

560 
(if falsify then "counterexample" else "model") 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

561 
> not standard ? prefix "nonstandard " 
33192  562 

563 
val scopes = Unsynchronized.ref [] 

564 
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

565 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  566 
val checked_problems = Unsynchronized.ref (SOME []) 
567 
val met_potential = Unsynchronized.ref 0 

568 

569 
fun update_checked_problems problems = 

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

571 
o nth problems) 

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

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

573 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  574 

575 
fun print_and_check_model genuine bounds 

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

577 
: problem_extension) = 

578 
let 

579 
val (reconstructed_model, codatatypes_ok) = 

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

580 
reconstruct_hol_model {show_datatypes = show_datatypes, 
33192  581 
show_consts = show_consts} 
582 
scope formats frees free_names sel_names nonsel_names rel_table 

583 
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

584 
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

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

586 
sound_finitizes andalso codatatypes_ok 
33192  587 
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

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

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

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

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

592 
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

593 
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

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

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

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

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

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

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

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

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

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

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

605 
das_wort_model ^ " is really genuine.") 
33192  606 
 SOME false => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

608 
error ("A supposedly genuine " ^ das_wort_model ^ " was \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

609 
\shown to be spurious by \"auto\".\nThis should never \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

612 
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

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

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

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

616 
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

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

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

619 
print "The existence of a nonstandard model suggests that the \ 
36126  620 
\induction hypothesis is not general enough or may even be \ 
621 
\wrong. See the Nitpick manual's \"Inductive Properties\" \ 

622 
\section for details (\"isabelle doc nitpick\")." 

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

623 
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

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

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

626 
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

627 
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

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

629 
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

630 
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

631 
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

632 
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

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

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

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

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

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

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

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

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

641 
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

642 
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

643 
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

644 
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

645 
print ("Try again with " ^ 
36380
1e8fcaccb3e8
stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
blanchet
parents:
36266
diff
changeset

646 
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

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

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

649 
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

650 
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

651 
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

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

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

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

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

656 
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

657 
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

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

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

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

661 
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

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

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

664 
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

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

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

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

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

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

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

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

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

673 
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

674 
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

675 
NONE) 
33192  676 
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

677 
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

678 
> pair genuine_means_genuine 
33192  679 
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

680 
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

681 
donno) first_time problems = 
33192  682 
let 
683 
val max_potential = Int.max (0, max_potential) 

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

685 
fun print_and_check genuine (j, bounds) = 

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

687 
val max_solutions = max_potential + max_genuine 

36384  688 
> not incremental ? Integer.min 1 
33192  689 
in 
690 
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

691 
(found_really_genuine, 0, 0, donno) 
33192  692 
else 
34126  693 
case KK.solve_any_problem overlord deadline max_threads max_solutions 
694 
(map fst problems) of 

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

695 
KK.JavaNotInstalled => 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

696 
(print_m install_java_message; 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

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

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

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

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

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

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

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

704 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  705 
let 
706 
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

707 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  708 
in 
709 
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

710 
show_kodkod_warning s; 
33192  711 
if null con_ps then 
712 
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

713 
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

714 
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

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

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

717 
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

718 
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

719 
val num_genuine = length genuine_codes 
33192  720 
val max_genuine = max_genuine  num_genuine 
721 
val max_potential = max_potential 

722 
 (length lib_ps  num_genuine) 

723 
in 

724 
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

725 
(found_really_genuine, 0, 0, donno) 
33192  726 
else 
727 
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

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

729 
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

730 
probably can't be satisfied themselves. *) 
33192  731 
val co_js = 
732 
map (fn j => j  1) unsat_js 

733 
> filter (fn j => 

734 
j >= 0 andalso 

735 
scopes_equivalent 

35814  736 
(#scope (snd (nth problems j)), 
737 
#scope (snd (nth problems (j + 1))))) 

33192  738 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 
739 
unsat_js @ co_js) 

740 
val problems = 

741 
problems > filter_out_indices bye_js 

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

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

745 
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

746 
max_genuine, donno) false problems 
33192  747 
end 
748 
end 

749 
else 

750 
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

751 
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

752 
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

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

754 
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

755 
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

756 
found_really_genuine orelse exists fst genuine_codes 
33192  757 
in 
758 
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

759 
(found_really_genuine, 0, max_genuine, donno) 
33192  760 
else 
761 
let 

762 
val bye_js = sort_distinct int_ord 

763 
(map fst sat_ps @ unsat_js) 

764 
val problems = 

765 
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

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

767 
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

768 
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

769 
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

770 
end 
33192  771 
end 
772 
end 

34126  773 
 KK.TimedOut unsat_js => 
33192  774 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  775 
 KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) 
776 
 KK.Interrupted (SOME unsat_js) => 

33192  777 
(update_checked_problems problems unsat_js; do_interrupted ()) 
34126  778 
 KK.Error (s, unsat_js) => 
33192  779 
(update_checked_problems problems unsat_js; 
780 
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

781 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  782 
end 
783 

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

784 
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

785 
donno) = 
33192  786 
let 
787 
val _ = 

788 
if null scopes then 

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

790 
else if verbose then 

791 
pprint (Pretty.chunks 

792 
[Pretty.blk (0, 

793 
pstrs ((if n > 1 then 

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

795 
signed_string_of_int n ^ ": " 

796 
else 

797 
"") ^ 

798 
"Trying " ^ string_of_int (length scopes) ^ 

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

800 
Pretty.indent indent_size 

801 
(Pretty.chunks (map2 

802 
(fn j => fn scope => 

803 
Pretty.block ( 

804 
(case pretties_for_scope scope true of 

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

806 
 pretties => pretties) @ 

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

808 
(length scopes downto 1) scopes))]) 

809 
else 

810 
() 

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

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

813 
case problem_for_scope unsound scope of 
33192  814 
SOME problem => 
815 
(problems 

816 
> (null problems orelse 

35814  817 
not (KK.problems_equivalent (fst problem, fst (hd problems)))) 
33192  818 
? cons problem, donno) 
819 
 NONE => (problems, donno + 1)) 

820 
val (problems, donno) = 

821 
fold add_problem_for_scope 

822 
(map_product pair scopes 

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

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

825 
([], donno) 

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

827 
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

828 
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

829 
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

830 
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

831 
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

832 
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

833 
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

834 
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

835 
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

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

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

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

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

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

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

844 
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

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

846 
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

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

848 
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

849 
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

850 
() 
33192  851 
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

852 
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

853 
donno) true (rev problems) 
33192  854 
end 
855 

856 
fun scope_count (problems : rich_problem list) scope = 

35814  857 
length (filter (curry scopes_equivalent scope o #scope o snd) problems) 
33192  858 
fun excipit did_so_and_so = 
859 
let 

860 
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

861 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  862 
else I 
863 
val total = length (!scopes) 

864 
val unsat = 

865 
fold (fn scope => 

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

867 
0 => I 

868 
 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

869 
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

870 
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

871 
? Integer.add 1) (!generated_scopes) 0 
33192  872 
in 
873 
"Nitpick " ^ did_so_and_so ^ 

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

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

875 
" " ^ string_of_int (Int.min (total  1, unsat)) ^ " of " ^ 
33192  876 
string_of_int total ^ " scope" ^ plural_s total 
877 
else 

878 
"") ^ "." 

879 
end 

880 

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

881 
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

882 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  883 
if donno > 0 andalso max_genuine > 0 then 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

884 
(print_m (fn () => excipit "checked"); "unknown") 
33192  885 
else if max_genuine = original_max_genuine then 
886 
if max_potential = original_max_potential then 

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

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

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

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

890 
" This suggests that the induction hypothesis might be \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

891 
\general enough to prove this subgoal." 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

893 
"")); "none") 
33192  894 
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

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

896 
"Nitpick could not find a" ^ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

897 
(if max_genuine = 1 then " better " ^ das_wort_model ^ "." 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

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

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

900 
"genuine" 
33192  901 
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

902 
"quasi_genuine" 
33192  903 
 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

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

907 

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

908 
val (skipped, the_scopes) = 
36386
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

909 
all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns 
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

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

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

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

913 
print_m (fn () => "Too many scopes. Skipping " ^ 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

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

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

916 
". (Consider using \"mono\" or \ 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

917 
\\"merge_type_vars\" to prevent this.)") 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

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

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

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

921 

33192  922 
val batches = batch_list batch_size (!scopes) 
923 
val outcome_code = 

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

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

925 
(false, max_potential, max_genuine, 0) 
33192  926 
handle Exn.Interrupt => do_interrupted ()) 
927 
handle TimeLimit.TimeOut => 

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

928 
(print_m (fn () => excipit "ran out of time after checking"); 
33192  929 
if !met_potential > 0 then "potential" else "unknown") 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

930 
 Exn.Interrupt => 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

931 
if auto orelse debug then raise Interrupt 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

932 
else error (excipit "was interrupted after checking") 
33192  933 
val _ = print_v (fn () => "Total time: " ^ 
934 
signed_string_of_int (Time.toMilliseconds 

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

936 
in (outcome_code, !state_ref) end 

937 
handle Exn.Interrupt => 

938 
if auto orelse #debug params then 

939 
raise Interrupt 

940 
else 

941 
if passed_deadline deadline then 

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

943 
else 

944 
error "Nitpick was interrupted." 

945 

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

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

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

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

950 
else warning (Pretty.string_of (plazy install_kodkodi_message)); 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

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

954 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

955 
val outcome as (outcome_code, _) = 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

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

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

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

960 
if expect = "" orelse outcome_code = expect then outcome 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

961 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

962 
end 
33192  963 

35335  964 
fun is_fixed_equation fixes 
965 
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = 

966 
member (op =) fixes s 

967 
 is_fixed_equation _ _ = false 

968 
fun extract_fixed_frees ctxt (assms, t) = 

969 
let 

970 
val fixes = Variable.fixes_of ctxt > map snd 

971 
val (subst, other_assms) = 

972 
List.partition (is_fixed_equation fixes) assms 

973 
>> map Logic.dest_equals 

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

975 

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

976 
fun pick_nits_in_subgoal state params auto i step = 
33192  977 
let 
978 
val ctxt = Proof.context_of state 

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

981 
case Logic.count_prems t of 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

982 
0 => (priority "No subgoal!"; ("none", state)) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

983 
 n => 
33192  984 
let 
35335  985 
val (t, frees) = Logic.goal_params t i 
986 
val t = subst_bounds (frees, t) 

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

33192  990 
end 
991 

992 
end; 