author  blanchet 
Thu, 04 Feb 2010 13:36:52 +0100  
changeset 34998  5e492a862b34 
parent 34982  7b8c366e34a2 
child 35028  108662d50512 
child 35070  96136eb6218f 
permissions  rwrr 
33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

1 
(* Title: HOL/Tools/Nitpick/nitpick_hol.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:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Auxiliary HOLrelated functions used by Nitpick. 

6 
*) 

7 

8 
signature NITPICK_HOL = 

9 
sig 

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

10 
type styp = Nitpick_Util.styp 
33192  11 
type const_table = term list Symtab.table 
12 
type special_fun = (styp * int list * term list) * styp 

13 
type unrolled = styp * styp 

14 
type wf_cache = (styp * (bool * bool)) list 

15 

16 
type extended_context = { 

17 
thy: theory, 

18 
ctxt: Proof.context, 

19 
max_bisim_depth: int, 

20 
boxes: (typ option * bool option) list, 

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

21 
stds: (typ option * bool) list, 
33192  22 
wfs: (styp option * bool option) list, 
23 
user_axioms: bool option, 

24 
debug: bool, 

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

25 
binary_ints: bool option, 
33192  26 
destroy_constrs: bool, 
27 
specialize: bool, 

28 
skolemize: bool, 

29 
star_linear_preds: bool, 

30 
uncurry: bool, 

31 
fast_descrs: bool, 

32 
tac_timeout: Time.time option, 

33 
evals: term list, 

34 
case_names: (string * int) list, 

35 
def_table: const_table, 

36 
nondef_table: const_table, 

37 
user_nondefs: term list, 

38 
simp_table: const_table Unsynchronized.ref, 

39 
psimp_table: const_table, 

40 
intro_table: const_table, 

41 
ground_thm_table: term list Inttab.table, 

42 
ersatz_table: (string * string) list, 

43 
skolems: (string * string list) list Unsynchronized.ref, 

44 
special_funs: special_fun list Unsynchronized.ref, 

45 
unrolled_preds: unrolled list 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:
33578
diff
changeset

46 
wf_cache: 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:
33578
diff
changeset

47 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  48 

49 
val name_sep : string 

50 
val numeral_prefix : string 

51 
val skolem_prefix : string 

52 
val eval_prefix : string 

53 
val original_name : string > string 

34998  54 
val s_conj : term * term > term 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

55 
val unbit_and_unbox_type : typ > typ 
33192  56 
val string_for_type : Proof.context > typ > string 
57 
val prefix_name : string > string > string 

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

58 
val shortest_name : string > string 
33192  59 
val short_name : string > string 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

60 
val shorten_names_in_term : term > term 
33192  61 
val type_match : theory > typ * typ > bool 
62 
val const_match : theory > styp * styp > bool 

63 
val term_match : theory > term * term > bool 

64 
val is_TFree : typ > bool 

65 
val is_higher_order_type : typ > bool 

66 
val is_fun_type : typ > bool 

67 
val is_set_type : typ > bool 

68 
val is_pair_type : typ > bool 

69 
val is_lfp_iterator_type : typ > bool 

70 
val is_gfp_iterator_type : typ > bool 

71 
val is_fp_iterator_type : typ > bool 

72 
val is_boolean_type : typ > bool 

73 
val is_integer_type : typ > bool 

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

74 
val is_bit_type : typ > bool 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

75 
val is_word_type : typ > bool 
33192  76 
val is_record_type : typ > bool 
77 
val is_number_type : theory > typ > bool 

78 
val const_for_iterator_type : typ > styp 

79 
val nth_range_type : int > typ > typ 

80 
val num_factors_in_type : typ > int 

81 
val num_binder_types : typ > int 

82 
val curried_binder_types : typ > typ list 

83 
val mk_flat_tuple : typ > term list > term 

84 
val dest_n_tuple : int > term > term list 

85 
val instantiate_type : theory > typ > typ > typ > typ 

33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

86 
val is_real_datatype : theory > string > bool 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

87 
val is_quot_type : theory > typ > bool 
33192  88 
val is_codatatype : theory > typ > bool 
89 
val is_pure_typedef : theory > typ > bool 

90 
val is_univ_typedef : theory > typ > bool 

91 
val is_datatype : theory > typ > bool 

92 
val is_record_constr : styp > bool 

93 
val is_record_get : theory > styp > bool 

94 
val is_record_update : theory > styp > bool 

95 
val is_abs_fun : theory > styp > bool 

96 
val is_rep_fun : theory > styp > bool 

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

97 
val is_quot_abs_fun : Proof.context > styp > bool 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

98 
val is_quot_rep_fun : Proof.context > styp > bool 
33192  99 
val is_constr : theory > styp > bool 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

100 
val is_stale_constr : theory > styp > bool 
33192  101 
val is_sel : string > bool 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

102 
val is_sel_like_and_no_discr : string > bool 
33192  103 
val discr_for_constr : styp > styp 
104 
val num_sels_for_constr_type : typ > int 

105 
val nth_sel_name_for_constr_name : string > int > string 

106 
val nth_sel_for_constr : styp > int > styp 

107 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

108 
val sel_no_from_name : string > int 

109 
val eta_expand : typ list > term > int > term 

110 
val extensionalize : term > term 

111 
val distinctness_formula : typ > term list > term 

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

113 
val unregister_frac_type : string > theory > theory 

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

115 
val unregister_codatatype : typ > theory > theory 

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

116 
val datatype_constrs : extended_context > typ > styp list 
33192  117 
val boxed_datatype_constrs : extended_context > typ > styp list 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

118 
val num_datatype_constrs : extended_context > typ > int 
33192  119 
val constr_name_for_sel_like : string > string 
120 
val boxed_constr_for_sel : extended_context > styp > styp 

121 
val card_of_type : (typ * int) list > typ > int 

122 
val bounded_card_of_type : int > int > (typ * int) list > typ > int 

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

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

124 
extended_context > int > int > (typ * int) list > typ > int 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

125 
val is_finite_type : extended_context > typ > bool 
33192  126 
val all_axioms_of : theory > term list * term list * term list 
127 
val arity_of_built_in_const : bool > styp > int option 

128 
val is_built_in_const : bool > styp > bool 

129 
val case_const_names : theory > (string * int) list 

130 
val const_def_table : Proof.context > term list > const_table 

131 
val const_nondef_table : term list > const_table 

132 
val const_simp_table : Proof.context > const_table 

133 
val const_psimp_table : Proof.context > const_table 

134 
val inductive_intro_table : Proof.context > const_table > const_table 

135 
val ground_theorem_table : theory > term list Inttab.table 

136 
val ersatz_table : theory > (string * string) list 

137 
val def_of_const : theory > const_table > styp > term option 

138 
val is_inductive_pred : extended_context > styp > bool 

139 
val is_constr_pattern_lhs : theory > term > bool 

140 
val is_constr_pattern_formula : theory > term > bool 

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

141 
val merge_type_vars_in_terms : term list > term list 
33192  142 
val ground_types_in_type : extended_context > typ > typ list 
143 
val ground_types_in_terms : extended_context > term list > typ list 

144 
val format_type : int list > int list > typ > typ 

145 
val format_term_type : 

146 
theory > const_table > (term option * int list) list > term > typ 

147 
val user_friendly_const : 

148 
extended_context > string * string > (term option * int list) list 

149 
> styp > term * typ 

150 
val assign_operator_for_const : styp > string 

151 
val preprocess_term : 

152 
extended_context > term > ((term list * term list) * (bool * bool)) * term 

153 
end; 

154 

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

155 
structure Nitpick_HOL : NITPICK_HOL = 
33192  156 
struct 
157 

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

158 
open Nitpick_Util 
33192  159 

160 
type const_table = term list Symtab.table 

161 
type special_fun = (styp * int list * term list) * styp 

162 
type unrolled = styp * styp 

163 
type wf_cache = (styp * (bool * bool)) list 

164 

165 
type extended_context = { 

166 
thy: theory, 

167 
ctxt: Proof.context, 

168 
max_bisim_depth: int, 

169 
boxes: (typ option * bool option) list, 

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

170 
stds: (typ option * bool) list, 
33192  171 
wfs: (styp option * bool option) list, 
172 
user_axioms: bool option, 

173 
debug: bool, 

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

174 
binary_ints: bool option, 
33192  175 
destroy_constrs: bool, 
176 
specialize: bool, 

177 
skolemize: bool, 

178 
star_linear_preds: bool, 

179 
uncurry: bool, 

180 
fast_descrs: bool, 

181 
tac_timeout: Time.time option, 

182 
evals: term list, 

183 
case_names: (string * int) list, 

184 
def_table: const_table, 

185 
nondef_table: const_table, 

186 
user_nondefs: term list, 

187 
simp_table: const_table Unsynchronized.ref, 

188 
psimp_table: const_table, 

189 
intro_table: const_table, 

190 
ground_thm_table: term list Inttab.table, 

191 
ersatz_table: (string * string) list, 

192 
skolems: (string * string list) list Unsynchronized.ref, 

193 
special_funs: special_fun list Unsynchronized.ref, 

194 
unrolled_preds: unrolled list 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:
33578
diff
changeset

195 
wf_cache: 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:
33578
diff
changeset

196 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  197 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

198 
structure Data = Theory_Data( 
33192  199 
type T = {frac_types: (string * (string * string) list) list, 
200 
codatatypes: (string * (string * styp list)) list} 

201 
val empty = {frac_types = [], codatatypes = []} 

202 
val extend = I 

33522  203 
fun merge ({frac_types = fs1, codatatypes = cs1}, 
204 
{frac_types = fs2, codatatypes = cs2}) : T = 

33699
f33b036ef318
permissive AList.merge  most likely setup for theory data (beware of spurious AList.DUP);
wenzelm
parents:
33583
diff
changeset

205 
{frac_types = AList.merge (op =) (K true) (fs1, fs2), 
f33b036ef318
permissive AList.merge  most likely setup for theory data (beware of spurious AList.DUP);
wenzelm
parents:
33583
diff
changeset

206 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  207 

208 
val name_sep = "$" 

209 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

210 
val sel_prefix = nitpick_prefix ^ "sel" 

211 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

212 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

213 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

214 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

215 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

216 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

217 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

218 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

219 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

220 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

221 
val skolem_prefix = nitpick_prefix ^ "sk" 

222 
val special_prefix = nitpick_prefix ^ "sp" 

223 
val uncurry_prefix = nitpick_prefix ^ "unc" 

224 
val eval_prefix = nitpick_prefix ^ "eval" 

225 
val bound_var_prefix = "b" 

226 
val cong_var_prefix = "c" 

227 
val iter_var_prefix = "i" 

228 
val val_var_prefix = nitpick_prefix ^ "v" 

229 
val arg_var_prefix = "x" 

230 

231 
(* int > string *) 

232 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

233 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

234 
(* int > int > string *) 

235 
fun skolem_prefix_for k j = 

236 
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 

237 
fun uncurry_prefix_for k j = 

238 
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 

239 

240 
(* string > string * string *) 

241 
val strip_first_name_sep = 

242 
Substring.full #> Substring.position name_sep ##> Substring.triml 1 

243 
#> pairself Substring.string 

244 
(* string > string *) 

245 
fun original_name s = 

246 
if String.isPrefix nitpick_prefix s then 

247 
case strip_first_name_sep s of (s1, "") => s1  (_, s2) => original_name s2 

248 
else 

249 
s 

250 
val after_name_sep = snd o strip_first_name_sep 

251 

34998  252 
(* term * term > term *) 
253 
fun s_conj (t1, @{const True}) = t1 

254 
 s_conj (@{const True}, t2) = t2 

255 
 s_conj (t1, t2) = 

256 
if t1 = @{const False} orelse t2 = @{const False} then @{const False} 

257 
else HOLogic.mk_conj (t1, t2) 

258 
fun s_disj (t1, @{const False}) = t1 

259 
 s_disj (@{const False}, t2) = t2 

260 
 s_disj (t1, t2) = 

261 
if t1 = @{const True} orelse t2 = @{const True} then @{const True} 

262 
else HOLogic.mk_disj (t1, t2) 

263 
(* term > term > term *) 

264 
fun mk_exists v t = 

265 
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) 

266 

267 
(* term > term > term list *) 

268 
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = 

269 
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t] 

270 
 strip_connective _ t = [t] 

271 
(* term > term list * term *) 

272 
fun strip_any_connective (t as (t0 $ t1 $ t2)) = 

273 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 

274 
(strip_connective t0 t, t0) 

275 
else 

276 
([t], @{const Not}) 

277 
 strip_any_connective t = ([t], @{const Not}) 

278 
(* term > term list *) 

279 
val conjuncts = strip_connective @{const "op &"} 

280 
val disjuncts = strip_connective @{const "op "} 

281 

33192  282 
(* When you add constants to these lists, make sure to handle them in 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

283 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  284 
well. *) 
285 
val built_in_consts = 

286 
[(@{const_name all}, 1), 

287 
(@{const_name "=="}, 2), 

288 
(@{const_name "==>"}, 2), 

289 
(@{const_name Pure.conjunction}, 2), 

290 
(@{const_name Trueprop}, 1), 

291 
(@{const_name Not}, 1), 

292 
(@{const_name False}, 0), 

293 
(@{const_name True}, 0), 

294 
(@{const_name All}, 1), 

295 
(@{const_name Ex}, 1), 

296 
(@{const_name "op ="}, 2), 

297 
(@{const_name "op &"}, 2), 

298 
(@{const_name "op "}, 2), 

299 
(@{const_name "op >"}, 2), 

300 
(@{const_name If}, 3), 

301 
(@{const_name Let}, 2), 

302 
(@{const_name Unity}, 0), 

303 
(@{const_name Pair}, 2), 

304 
(@{const_name fst}, 1), 

305 
(@{const_name snd}, 1), 

306 
(@{const_name Id}, 0), 

307 
(@{const_name insert}, 2), 

308 
(@{const_name converse}, 1), 

309 
(@{const_name trancl}, 1), 

310 
(@{const_name rel_comp}, 2), 

311 
(@{const_name image}, 2), 

312 
(@{const_name Suc}, 0), 

313 
(@{const_name finite}, 1), 

314 
(@{const_name nat}, 0), 

315 
(@{const_name zero_nat_inst.zero_nat}, 0), 

316 
(@{const_name one_nat_inst.one_nat}, 0), 

317 
(@{const_name plus_nat_inst.plus_nat}, 0), 

318 
(@{const_name minus_nat_inst.minus_nat}, 0), 

319 
(@{const_name times_nat_inst.times_nat}, 0), 

320 
(@{const_name div_nat_inst.div_nat}, 0), 

321 
(@{const_name ord_nat_inst.less_nat}, 2), 

322 
(@{const_name ord_nat_inst.less_eq_nat}, 2), 

323 
(@{const_name nat_gcd}, 0), 

324 
(@{const_name nat_lcm}, 0), 

325 
(@{const_name zero_int_inst.zero_int}, 0), 

326 
(@{const_name one_int_inst.one_int}, 0), 

327 
(@{const_name plus_int_inst.plus_int}, 0), 

328 
(@{const_name minus_int_inst.minus_int}, 0), 

329 
(@{const_name times_int_inst.times_int}, 0), 

330 
(@{const_name div_int_inst.div_int}, 0), 

33571  331 
(@{const_name uminus_int_inst.uminus_int}, 0), 
33192  332 
(@{const_name ord_int_inst.less_int}, 2), 
333 
(@{const_name ord_int_inst.less_eq_int}, 2), 

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

334 
(@{const_name unknown}, 0), 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

335 
(@{const_name is_unknown}, 1), 
33192  336 
(@{const_name Tha}, 1), 
337 
(@{const_name Frac}, 0), 

338 
(@{const_name norm_frac}, 0)] 

339 
val built_in_descr_consts = 

340 
[(@{const_name The}, 1), 

341 
(@{const_name Eps}, 1)] 

342 
val built_in_typed_consts = 

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

343 
[((@{const_name of_nat}, nat_T > int_T), 0), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

344 
((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)] 
33192  345 
val built_in_set_consts = 
346 
[(@{const_name lower_semilattice_fun_inst.inf_fun}, 2), 

347 
(@{const_name upper_semilattice_fun_inst.sup_fun}, 2), 

348 
(@{const_name minus_fun_inst.minus_fun}, 2), 

349 
(@{const_name ord_fun_inst.less_eq_fun}, 2)] 

350 

351 
(* typ > typ *) 

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

352 
fun unbit_type @{typ "unsigned_bit word"} = nat_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

353 
 unbit_type @{typ "signed_bit word"} = int_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

354 
 unbit_type @{typ bisim_iterator} = nat_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

355 
 unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

356 
 unbit_type T = T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

357 
fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

358 
unbit_and_unbox_type (Type ("fun", Ts)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

359 
 unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

360 
Type ("*", map unbit_and_unbox_type Ts) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

361 
 unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

362 
 unbit_and_unbox_type @{typ "signed_bit word"} = int_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

363 
 unbit_and_unbox_type @{typ bisim_iterator} = nat_T 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

364 
 unbit_and_unbox_type (Type (s, Ts as _ :: _)) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

365 
Type (s, map unbit_and_unbox_type Ts) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

366 
 unbit_and_unbox_type T = T 
33192  367 
(* Proof.context > typ > string *) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

368 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type 
33192  369 

370 
(* string > string > string *) 

371 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

372 
(* string > string *) 

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

373 
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => "" 
33192  374 
(* string > term > term *) 
375 
val prefix_abs_vars = Term.map_abs_vars o prefix_name 

376 
(* term > term *) 

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

377 
val shorten_abs_vars = Term.map_abs_vars shortest_name 
33192  378 
(* string > string *) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

379 
fun short_name s = 
33192  380 
case space_explode name_sep s of 
381 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix 

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

382 
 ss => map shortest_name ss > space_implode "_" 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

383 
(* typ > typ *) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

384 
fun shorten_names_in_type (Type (s, Ts)) = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

385 
Type (short_name s, map shorten_names_in_type Ts) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

386 
 shorten_names_in_type T = T 
33192  387 
(* term > term *) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

388 
val shorten_names_in_term = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

389 
map_aterms (fn Const (s, T) => Const (short_name s, T)  t => t) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

390 
#> map_types shorten_names_in_type 
33192  391 

392 
(* theory > typ * typ > bool *) 

393 
fun type_match thy (T1, T2) = 

394 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 

395 
handle Type.TYPE_MATCH => false 

396 
(* theory > styp * styp > bool *) 

397 
fun const_match thy ((s1, T1), (s2, T2)) = 

398 
s1 = s2 andalso type_match thy (T1, T2) 

399 
(* theory > term * term > bool *) 

400 
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) 

401 
 term_match thy (Free (s1, T1), Free (s2, T2)) = 

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

402 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
33192  403 
 term_match thy (t1, t2) = t1 aconv t2 
404 

405 
(* typ > bool *) 

406 
fun is_TFree (TFree _) = true 

407 
 is_TFree _ = false 

408 
fun is_higher_order_type (Type ("fun", _)) = true 

409 
 is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts 

410 
 is_higher_order_type _ = false 

411 
fun is_fun_type (Type ("fun", _)) = true 

412 
 is_fun_type _ = false 

413 
fun is_set_type (Type ("fun", [_, @{typ bool}])) = true 

414 
 is_set_type _ = false 

415 
fun is_pair_type (Type ("*", _)) = true 

416 
 is_pair_type _ = false 

417 
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s 

418 
 is_lfp_iterator_type _ = false 

419 
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s 

420 
 is_gfp_iterator_type _ = false 

421 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

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

422 
fun is_boolean_type T = (T = prop_T orelse T = bool_T) 
33192  423 
val is_integer_type = 
424 
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type 

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

425 
fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit}) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

426 
fun is_word_type (Type (@{type_name word}, _)) = true 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

427 
 is_word_type _ = false 
33192  428 
val is_record_type = not o null o Record.dest_recTs 
429 
(* theory > typ > bool *) 

430 
fun is_frac_type thy (Type (s, [])) = 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

431 
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) 
33192  432 
 is_frac_type _ _ = false 
433 
fun is_number_type thy = is_integer_type orf is_frac_type thy 

434 

435 
(* bool > styp > typ *) 

436 
fun iterator_type_for_const gfp (s, T) = 

437 
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, 

438 
binder_types T) 

439 
(* typ > styp *) 

440 
fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts > bool_T) 

441 
 const_for_iterator_type T = 

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

442 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  443 

444 
(* int > typ > typ * typ *) 

445 
fun strip_n_binders 0 T = ([], T) 

446 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

447 
strip_n_binders (n  1) T2 >> cons T1 

448 
 strip_n_binders n (Type (@{type_name fun_box}, Ts)) = 

449 
strip_n_binders n (Type ("fun", Ts)) 

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

450 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  451 
(* typ > typ *) 
452 
val nth_range_type = snd oo strip_n_binders 

453 

454 
(* typ > int *) 

455 
fun num_factors_in_type (Type ("*", [T1, T2])) = 

456 
fold (Integer.add o num_factors_in_type) [T1, T2] 0 

457 
 num_factors_in_type _ = 1 

458 
fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2 

459 
 num_binder_types _ = 0 

460 
(* typ > typ list *) 

461 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

462 
fun maybe_curried_binder_types T = 

463 
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T 

464 

465 
(* typ > term list > term *) 

466 
fun mk_flat_tuple _ [t] = t 

467 
 mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) = 

468 
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) 

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

469 
 mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) 
33192  470 
(* int > term > term list *) 
471 
fun dest_n_tuple 1 t = [t] 

472 
 dest_n_tuple n t = HOLogic.dest_prod t > dest_n_tuple (n  1) > op :: 

473 

474 
(* int > typ > typ list *) 

475 
fun dest_n_tuple_type 1 T = [T] 

476 
 dest_n_tuple_type n (Type (_, [T1, T2])) = 

477 
T1 :: dest_n_tuple_type (n  1) T2 

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

478 
 dest_n_tuple_type _ T = 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

479 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  480 

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

481 
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype", 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

482 
e.g., by adding a field to "Datatype_Aux.info". *) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

483 
(* string > bool *) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

484 
val is_basic_datatype = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

485 
member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit}, 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

486 
@{type_name nat}, @{type_name int}, 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

487 
"Code_Numeral.code_numeral"] 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

488 

33192  489 
(* theory > typ > typ > typ > typ *) 
490 
fun instantiate_type thy T1 T1' T2 = 

491 
Same.commit (Envir.subst_type_same 

492 
(Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty)) 

493 
(Logic.varifyT T2) 

494 
handle Type.TYPE_MATCH => 

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

495 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  496 

497 
(* theory > typ > typ > styp *) 

498 
fun repair_constr_type thy body_T' T = 

499 
instantiate_type thy (body_type T) body_T' T 

500 

501 
(* string > (string * string) list > theory > theory *) 

502 
fun register_frac_type frac_s ersaetze thy = 

503 
let 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

504 
val {frac_types, codatatypes} = Data.get thy 
33192  505 
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

506 
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end 
33192  507 
(* string > theory > theory *) 
508 
fun unregister_frac_type frac_s = register_frac_type frac_s [] 

509 

510 
(* typ > string > styp list > theory > theory *) 

511 
fun register_codatatype co_T case_name constr_xs thy = 

512 
let 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

513 
val {frac_types, codatatypes} = Data.get thy 
33192  514 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
515 
val (co_s, co_Ts) = dest_Type co_T 

516 
val _ = 

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

517 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

518 
co_s <> "fun" andalso not (is_basic_datatype co_s) then 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

519 
() 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

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

521 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  522 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
523 
codatatypes 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

524 
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end 
33192  525 
(* typ > theory > theory *) 
526 
fun unregister_codatatype co_T = register_codatatype co_T "" [] 

527 

528 
type typedef_info = 

529 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 

530 
set_def: thm option, prop_of_Rep: thm, set_name: string, 

33876
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

531 
Abs_inverse: thm option, Rep_inverse: thm option} 
33192  532 

533 
(* theory > string > typedef_info *) 

534 
fun typedef_info thy s = 

535 
if is_frac_type thy (Type (s, [])) then 

536 
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, 

537 
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, 

538 
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"} 

539 
> Logic.varify, 

33876
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

540 
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} 
33192  541 
else case Typedef.get_info thy s of 
33876
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

542 
SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

543 
Rep_inverse, ...} => 
33192  544 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 
545 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 

33876
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

546 
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

547 
Rep_inverse = SOME Rep_inverse} 
33192  548 
 NONE => NONE 
549 

550 
(* theory > string > bool *) 

551 
val is_typedef = is_some oo typedef_info 

552 
val is_real_datatype = is_some oo Datatype.get_info 

553 
(* theory > typ > bool *) 

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

554 
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *) 
34998  555 
 is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

556 
 is_quot_type _ _ = false 
33192  557 
fun is_codatatype thy (T as Type (s, _)) = 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

558 
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s 
33192  559 
> Option.map snd > these)) 
560 
 is_codatatype _ _ = false 

561 
fun is_pure_typedef thy (T as Type (s, _)) = 

562 
is_typedef thy s andalso 

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

563 
not (is_real_datatype thy s orelse is_quot_type thy T orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

564 
is_codatatype thy T orelse is_record_type T orelse is_integer_type T) 
33192  565 
 is_pure_typedef _ _ = false 
566 
fun is_univ_typedef thy (Type (s, _)) = 

567 
(case typedef_info thy s of 

568 
SOME {set_def, prop_of_Rep, ...} => 

569 
(case set_def of 

570 
SOME thm => 

571 
try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm 

572 
 NONE => 

573 
try (fst o dest_Const o snd o HOLogic.dest_mem 

33864
232daf7eafaf
fix Nitpick soundness bugs related to integration (in particular, "code_numeral")
blanchet
parents:
33851
diff
changeset

574 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} 
33192  575 
 NONE => false) 
576 
 is_univ_typedef _ _ = false 

577 
fun is_datatype thy (T as Type (s, _)) = 

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

578 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

579 
is_quot_type thy T) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

580 
not (is_basic_datatype s) 
33192  581 
 is_datatype _ _ = false 
582 

583 
(* theory > typ > (string * typ) list * (string * typ) *) 

584 
fun all_record_fields thy T = 

585 
let val (recs, more) = Record.get_extT_fields thy T in 

586 
recs @ more :: all_record_fields thy (snd more) 

587 
end 

588 
handle TYPE _ => [] 

589 
(* styp > bool *) 

590 
fun is_record_constr (x as (s, T)) = 

591 
String.isSuffix Record.extN s andalso 

592 
let val dataT = body_type T in 

593 
is_record_type dataT andalso 

594 
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN 

595 
end 

596 
(* theory > typ > int *) 

597 
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields 

598 
(* theory > string > typ > int *) 

599 
fun no_of_record_field thy s T1 = 

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

600 
find_index (curry (op =) s o fst) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

601 
(Record.get_extT_fields thy T1 > single > op @) 
33192  602 
(* theory > styp > bool *) 
603 
fun is_record_get thy (s, Type ("fun", [T1, _])) = 

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

604 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  605 
 is_record_get _ _ = false 
606 
fun is_record_update thy (s, T) = 

607 
String.isSuffix Record.updateN s andalso 

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

608 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  609 
(all_record_fields thy (body_type T)) 
610 
handle TYPE _ => false 

611 
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) = 

612 
(case typedef_info thy s' of 

613 
SOME {Abs_name, ...} => s = Abs_name 

614 
 NONE => false) 

615 
 is_abs_fun _ _ = false 

616 
fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) = 

617 
(case typedef_info thy s' of 

618 
SOME {Rep_name, ...} => s = Rep_name 

619 
 NONE => false) 

620 
 is_rep_fun _ _ = false 

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

621 
(* Proof.context > styp > bool *) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

622 
fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *) 
34998  623 
 is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

624 
 is_quot_abs_fun _ _ = 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:
34936
diff
changeset

625 
fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *) 
34998  626 
 is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

627 
 is_quot_rep_fun _ _ = false 
33192  628 

629 
(* theory > styp > styp *) 

630 
fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) = 

631 
(case typedef_info thy s' of 

632 
SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1])) 

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

633 
 NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

634 
 mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

635 
(* theory > typ > typ *) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

636 
fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"} 
34998  637 
 rep_type_for_quot_type _ (Type ("FSet.fset", [T])) = 
638 
Type (@{type_name list}, [T]) 

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

639 
 rep_type_for_quot_type _ T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

640 
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], []) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

641 
(* theory > typ > term *) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

642 
fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

643 
Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"}) 
34998  644 
 equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) = 
645 
Const ("FSet.list_eq", 

646 
Type (@{type_name list}, [T]) > Type (@{type_name list}, [T]) 

647 
> bool_T) 

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

648 
 equiv_relation_for_quot_type _ T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

649 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  650 

651 
(* theory > styp > bool *) 

652 
fun is_coconstr thy (s, T) = 

653 
let 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

654 
val {codatatypes, ...} = Data.get thy 
33192  655 
val co_T = body_type T 
656 
val co_s = dest_Type co_T > fst 

657 
in 

658 
exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T) 

659 
(AList.lookup (op =) codatatypes co_s > Option.map snd > these) 

660 
end 

661 
handle TYPE ("dest_Type", _, _) => false 

662 
fun is_constr_like thy (s, T) = 

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

663 
member (op =) [@{const_name FunBox}, @{const_name PairBox}, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

664 
@{const_name Quot}, @{const_name Zero_Rep}, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

665 
@{const_name Suc_Rep}] s orelse 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

666 
let val (x as (s, T)) = (s, unbit_and_unbox_type T) in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

667 
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

668 
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

669 
x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

670 
is_coconstr thy x 
33192  671 
end 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

672 
fun is_stale_constr thy (x as (_, T)) = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

673 
is_codatatype thy (body_type T) andalso is_constr_like thy x andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

674 
not (is_coconstr thy x) 
33192  675 
fun is_constr thy (x as (_, T)) = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

676 
is_constr_like thy x andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

677 
not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

678 
not (is_stale_constr thy x) 
33192  679 
(* string > bool *) 
680 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

681 
val is_sel_like_and_no_discr = 

682 
String.isPrefix sel_prefix 

683 
orf (member (op =) [@{const_name fst}, @{const_name snd}]) 

684 

685 
datatype boxability = 

686 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

687 

688 
(* boxability > boxability *) 

689 
fun in_fun_lhs_for InConstr = InSel 

690 
 in_fun_lhs_for _ = InFunLHS 

691 
fun in_fun_rhs_for InConstr = InConstr 

692 
 in_fun_rhs_for InSel = InSel 

693 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

694 
 in_fun_rhs_for _ = InFunRHS1 

695 

696 
(* extended_context > boxability > typ > bool *) 

697 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

698 
case T of 

699 
Type ("fun", _) => 

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

700 
(boxy = InPair orelse boxy = InFunLHS) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

701 
not (is_boolean_type (body_type T)) 
33192  702 
 Type ("*", Ts) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

703 
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

704 
((boxy = InExpr orelse boxy = InFunLHS) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

705 
exists (is_boxing_worth_it ext_ctxt InPair) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

706 
(map (box_type ext_ctxt InPair) Ts)) 
33192  707 
 _ => false 
708 
(* extended_context > boxability > string * typ list > string *) 

709 
and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = 

710 
case triple_lookup (type_match thy) boxes (Type z) of 

711 
SOME (SOME box_me) => box_me 

712 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

713 
(* extended_context > boxability > typ > typ *) 

714 
and box_type ext_ctxt boxy T = 

715 
case T of 

716 
Type (z as ("fun", [T1, T2])) => 

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

717 
if boxy <> InConstr andalso boxy <> InSel andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

718 
should_box_type ext_ctxt boxy z then 
33192  719 
Type (@{type_name fun_box}, 
720 
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) 

721 
else 

722 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

723 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

724 
 Type (z as ("*", Ts)) => 

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

725 
if boxy <> InConstr andalso boxy <> InSel 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

726 
andalso should_box_type ext_ctxt boxy z then 
33192  727 
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts) 
728 
else 

729 
Type ("*", map (box_type ext_ctxt 

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

730 
(if boxy = InConstr orelse boxy = InSel then boxy 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

731 
else InPair)) Ts) 
33192  732 
 _ => T 
733 

734 
(* styp > styp *) 

735 
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T > bool_T) 

736 

737 
(* typ > int *) 

738 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

739 
(* string > int > string *) 

740 
fun nth_sel_name_for_constr_name s n = 

741 
if s = @{const_name Pair} then 

742 
if n = 0 then @{const_name fst} else @{const_name snd} 

743 
else 

744 
sel_prefix_for n ^ s 

745 
(* styp > int > styp *) 

746 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

747 
 nth_sel_for_constr (s, T) n = 

748 
(nth_sel_name_for_constr_name s n, 

749 
body_type T > nth (maybe_curried_binder_types T) n) 

750 
(* extended_context > styp > int > styp *) 

751 
fun boxed_nth_sel_for_constr ext_ctxt = 

752 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

753 

754 
(* string > int *) 

755 
fun sel_no_from_name s = 

756 
if String.isPrefix discr_prefix s then 

757 
~1 

758 
else if String.isPrefix sel_prefix s then 

759 
s > unprefix sel_prefix > Int.fromString > the 

760 
else if s = @{const_name snd} then 

761 
1 

762 
else 

763 
0 

764 

765 
(* typ list > term > int > term *) 

766 
fun eta_expand _ t 0 = t 

767 
 eta_expand Ts (Abs (s, T, t')) n = 

768 
Abs (s, T, eta_expand (T :: Ts) t' (n  1)) 

769 
 eta_expand Ts t n = 

770 
fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n)) 

771 
(List.take (binder_types (fastype_of1 (Ts, t)), n)) 

772 
(list_comb (incr_boundvars n t, map Bound (n  1 downto 0))) 

773 

774 
(* term > term *) 

775 
fun extensionalize t = 

776 
case t of 

777 
(t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1 

778 
 Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) => 

779 
let val v = Var ((s, maxidx_of_term t + 1), T) in 

780 
extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2))) 

781 
end 

782 
 _ => t 

783 

784 
(* typ > term list > term *) 

785 
fun distinctness_formula T = 

786 
all_distinct_unordered_pairs_of 

787 
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) 

788 
#> List.foldr (s_conj o swap) @{const True} 

789 

790 
(* typ > term *) 

791 
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T) 

792 
fun suc_const T = Const (@{const_name Suc}, T > T) 

793 

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

794 
(* extended_context > typ > styp list *) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

795 
fun uncached_datatype_constrs ({thy, stds, ...} : extended_context) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

796 
(T as Type (s, Ts)) = 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

797 
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

798 
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

799 
 _ => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

800 
if is_datatype thy T then 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

801 
case Datatype.get_info thy s of 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

802 
SOME {index, descr, ...} => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

803 
let 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

804 
val (_, dtyps, constrs) = AList.lookup (op =) descr index > the 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

805 
in 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

806 
map (fn (s', Us) => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

807 
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

809 
> (triple_lookup (type_match thy) stds T > the > not) ? 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

810 
cons (@{const_name NonStd}, @{typ \<xi>} > T) 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

811 
end 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

812 
 NONE => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

813 
if is_record_type T then 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

814 
let 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

815 
val s' = unsuffix Record.ext_typeN s ^ Record.extN 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

816 
val T' = (Record.get_extT_fields thy T 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

817 
> apsnd single > uncurry append > map snd) > T 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

818 
in [(s', T')] end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

819 
else if is_quot_type thy T then 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

820 
[(@{const_name Quot}, rep_type_for_quot_type thy T > T)] 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

821 
else case typedef_info thy s of 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

822 
SOME {abs_type, rep_type, Abs_name, ...} => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

823 
[(Abs_name, instantiate_type thy abs_type T rep_type > T)] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

824 
 NONE => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

825 
if T = @{typ ind} then 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

826 
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

827 
else 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

828 
[] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

829 
else 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

831 
 uncached_datatype_constrs _ _ = [] 
33192  832 
(* extended_context > typ > styp list *) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

833 
fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T = 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

834 
case AList.lookup (op =) (!constr_cache) T of 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

835 
SOME xs => xs 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

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

837 
let val xs = uncached_datatype_constrs ext_ctxt T in 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

838 
(Unsynchronized.change constr_cache (cons (T, xs)); xs) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

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

840 
fun boxed_datatype_constrs ext_ctxt = 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

841 
map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

842 
(* extended_context > typ > int *) 
33192  843 
val num_datatype_constrs = length oo datatype_constrs 
844 

845 
(* string > string *) 

846 
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair} 

847 
 constr_name_for_sel_like @{const_name snd} = @{const_name Pair} 

848 
 constr_name_for_sel_like s' = original_name s' 

849 
(* extended_context > styp > styp *) 

850 
fun boxed_constr_for_sel ext_ctxt (s', T') = 

851 
let val s = constr_name_for_sel_like s' in 

852 
AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s 

853 
> the > pair s 

854 
end 

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

855 

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

856 
(* extended_context > styp > term *) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

857 
fun discr_term_for_constr ext_ctxt (x as (s, T)) = 
33192  858 
let val dataT = body_type T in 
859 
if s = @{const_name Suc} then 

860 
Abs (Name.uu, dataT, 

861 
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) 

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

862 
else if num_datatype_constrs ext_ctxt dataT >= 2 then 
33192  863 
Const (discr_for_constr x) 
864 
else 

865 
Abs (Name.uu, dataT, @{const True}) 

866 
end 

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

867 
(* extended_context > styp > term > term *) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

868 
fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t = 
33192  869 
case strip_comb t of 
870 
(Const x', args) => 

871 
if x = x' then @{const True} 

872 
else if is_constr_like thy x' then @{const False} 

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

873 
else betapply (discr_term_for_constr ext_ctxt x, t) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

874 
 _ => betapply (discr_term_for_constr ext_ctxt x, t) 
33192  875 

876 
(* styp > term > term *) 

877 
fun nth_arg_sel_term_for_constr (x as (s, T)) n = 

878 
let val (arg_Ts, dataT) = strip_type T in 

879 
if dataT = nat_T then 

880 
@{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"} 

881 
else if is_pair_type dataT then 

882 
Const (nth_sel_for_constr x n) 

883 
else 

884 
let 

885 
(* int > typ > int * term *) 

886 
fun aux m (Type ("*", [T1, T2])) = 

887 
let 

888 
val (m, t1) = aux m T1 

889 
val (m, t2) = aux m T2 

890 
in (m, HOLogic.mk_prod (t1, t2)) end 

891 
 aux m T = 

892 
(m + 1, Const (nth_sel_name_for_constr_name s m, dataT > T) 

893 
$ Bound 0) 

894 
val m = fold (Integer.add o num_factors_in_type) 

895 
(List.take (arg_Ts, n)) 0 

896 
in Abs ("x", dataT, aux m (nth arg_Ts n) > snd) end 

897 
end 

898 
(* theory > styp > term > int > typ > term *) 

899 
fun select_nth_constr_arg thy x t n res_T = 

900 
case strip_comb t of 

901 
(Const x', args) => 

902 
if x = x' then nth args n 

903 
else if is_constr_like thy x' then Const (@{const_name unknown}, res_T) 

904 
else betapply (nth_arg_sel_term_for_constr x n, t) 

905 
 _ => betapply (nth_arg_sel_term_for_constr x n, t) 

906 

907 
(* theory > styp > term list > term *) 

908 
fun construct_value _ x [] = Const x 

909 
 construct_value thy (x as (s, _)) args = 

910 
let val args = map Envir.eta_contract args in 

911 
case hd args of 

912 
Const (x' as (s', _)) $ t => 

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

913 
if is_sel_like_and_no_discr s' andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

914 
constr_name_for_sel_like s' = s andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

915 
forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t') 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

916 
(index_seq 0 (length args) ~~ args) then 
33192  917 
t 
918 
else 

919 
list_comb (Const x, args) 

920 
 _ => list_comb (Const x, args) 

921 
end 

922 

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

923 
(* extended_context > typ > term > term *) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

924 
fun constr_expand (ext_ctxt as {thy, ...}) T t = 
33192  925 
(case head_of t of 
926 
Const x => if is_constr_like thy x then t else raise SAME () 

927 
 _ => raise SAME ()) 

928 
handle SAME () => 

929 
let 

930 
val x' as (_, T') = 

931 
if is_pair_type T then 

932 
let val (T1, T2) = HOLogic.dest_prodT T in 

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

933 
(@{const_name Pair}, T1 > T2 > T) 
33192  934 
end 
935 
else 

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

936 
datatype_constrs ext_ctxt T > hd 
33192  937 
val arg_Ts = binder_types T' 
938 
in 

939 
list_comb (Const x', map2 (select_nth_constr_arg thy x' t) 

940 
(index_seq 0 (length arg_Ts)) arg_Ts) 

941 
end 

942 

943 
(* (typ * int) list > typ > int *) 

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

944 
fun card_of_type assigns (Type ("fun", [T1, T2])) = 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

945 
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

946 
 card_of_type assigns (Type ("*", [T1, T2])) = 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

947 
card_of_type assigns T1 * card_of_type assigns T2 
33192  948 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
949 
 card_of_type _ @{typ prop} = 2 

950 
 card_of_type _ @{typ bool} = 2 

951 
 card_of_type _ @{typ unit} = 1 

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

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

953 
case AList.lookup (op =) assigns T of 
33192  954 
SOME k => k 
955 
 NONE => if T = @{typ bisim_iterator} then 0 

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

956 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
33192  957 
(* int > (typ * int) list > typ > int *) 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

958 
fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) = 
33192  959 
let 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

960 
val k1 = bounded_card_of_type max default_card assigns T1 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

961 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  962 
in 
963 
if k1 = max orelse k2 = max then max 

964 
else Int.min (max, reasonable_power k2 k1) 

965 
end 

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

966 
 bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) = 
33192  967 
let 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

968 
val k1 = bounded_card_of_type max default_card assigns T1 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

969 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  970 
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

971 
 bounded_card_of_type max default_card assigns T = 
33192  972 
Int.min (max, if default_card = ~1 then 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

973 
card_of_type assigns T 
33192  974 
else 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

975 
card_of_type assigns T 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

976 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
33192  977 
default_card) 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

978 
(* extended_context > int > (typ * int) list > typ > int *) 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

979 
fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = 
33192  980 
let 
981 
(* typ list > typ > int *) 

982 
fun aux avoid T = 

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

983 
(if member (op =) avoid T then 
33192  984 
0 
985 
else case T of 

986 
Type ("fun", [T1, T2]) => 

987 
let 

988 
val k1 = aux avoid T1 

989 
val k2 = aux avoid T2 

990 
in 

991 
if k1 = 0 orelse k2 = 0 then 0 

992 
else if k1 >= max orelse k2 >= max then max 

993 
else Int.min (max, reasonable_power k2 k1) 

994 
end 

995 
 Type ("*", [T1, T2]) => 

996 
let 

997 
val k1 = aux avoid T1 

998 
val k2 = aux avoid T2 

999 
in 

1000 
if k1 = 0 orelse k2 = 0 then 0 

1001 
else if k1 >= max orelse k2 >= max then max 

1002 
else Int.min (max, k1 * k2) 

1003 
end 

1004 
 Type (@{type_name itself}, _) => 1 

1005 
 @{typ prop} => 2 

1006 
 @{typ bool} => 2 

1007 
 @{typ unit} => 1 

1008 
 Type _ => 

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

1009 
(case datatype_constrs ext_ctxt T of 
34126  1010 
[] => if is_integer_type T orelse is_bit_type T then 0 
1011 
else raise SAME () 

33192  1012 
 constrs => 
1013 
let 

1014 
val constr_cards = 

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

1015 
datatype_constrs ext_ctxt T 
33192  1016 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
1017 
o snd) 

1018 
in 

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

1019 
if exists (curry (op =) 0) constr_cards then 0 
33192  1020 
else Integer.sum constr_cards 
1021 
end) 

1022 
 _ => raise SAME ()) 

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

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

1024 
AList.lookup (op =) assigns T > the_default default_card 
33192  1025 
in Int.min (max, aux [] T) end 
1026 

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

1027 
(* extended_context > typ > bool *) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

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

1029 
not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] 
33192  1030 

1031 
(* term > bool *) 

1032 
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 

1033 
 is_ground_term (Const _) = true 

1034 
 is_ground_term _ = false 

1035 

1036 
(* term > word > word *) 

1037 
fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2) 

1038 
 hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0) 

1039 
 hashw_term _ = 0w0 

1040 
(* term > int *) 

1041 
val hash_term = Word.toInt o hashw_term 

1042 

1043 
(* term list > (indexname * typ) list *) 

1044 
fun special_bounds ts = 

1045 
fold Term.add_vars ts [] > sort (TermOrd.fast_indexname_ord o pairself fst) 

1046 

1047 
(* indexname * typ > term > term *) 

1048 
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) 

1049 

33571  1050 
(* theory > string > bool *) 
1051 
fun is_funky_typedef_name thy s = 

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

1052 
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1053 
@{type_name int}] s orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1054 
is_frac_type thy (Type (s, [])) 
33571  1055 
(* theory > term > bool *) 
1056 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 

1057 
 is_funky_typedef _ _ = false 

33192  1058 
(* term > bool *) 
1059 
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _) 

1060 
$ Const (@{const_name TYPE}, _)) = true 

1061 
 is_arity_type_axiom _ = false 

1062 
(* theory > bool > term > bool *) 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1063 
fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1064 
is_typedef_axiom thy boring t2 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1065 
 is_typedef_axiom thy boring 
33192  1066 
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1067 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1068 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1069 
 is_typedef_axiom _ _ _ = false 
1070 

1071 
(* Distinguishes between (1) constant definition axioms, (2) type arity and 

1072 
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)). 

1073 
Typedef axioms are uninteresting to Nitpick, because it can retrieve them 

1074 
using "typedef_info". *) 

1075 
(* theory > (string * term) list > string list > term list * term list *) 

1076 
fun partition_axioms_by_definitionality thy axioms def_names = 

1077 
let 

1078 
val axioms = sort (fast_string_ord o pairself fst) axioms 

1079 
val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms 

1080 
val nondefs = 

1081 
OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms 

1082 
> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd) 

1083 
in pairself (map snd) (defs, nondefs) end 

1084 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1085 
(* Ideally we would check against "Complex_Main", not "Refute", but any theory 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1086 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1087 
commands. *) 
1088 
(* theory > bool *) 

1089 
fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute}) 

1090 

1091 
(* term > bool *) 

1092 
val is_plain_definition = 

1093 
let 

1094 
(* term > bool *) 

1095 
fun do_lhs t1 = 

1096 
case strip_comb t1 of 

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

1097 
(Const _, args) => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1098 
forall is_Var args andalso not (has_duplicates (op =) args) 
33192  1099 
 _ => false 
1100 
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 

1101 
 do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) = 

1102 
do_lhs t1 

1103 
 do_eq _ = false 

1104 
in do_eq end 

1105 

1106 
(* theory > term list * term list * term list *) 

1107 
fun all_axioms_of thy = 

1108 
let 

1109 
(* theory list > term list *) 

1110 
val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of) 

1111 
val specs = Defs.all_specifications_of (Theory.defs_of thy) 

33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33699
diff
changeset

1112 
val def_names = specs > maps snd > map_filter #def 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1113 
> OrdList.make fast_string_ord 
33192  1114 
val thys = thy :: Theory.ancestors_of thy 
1115 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1116 
val built_in_axioms = axioms_of_thys built_in_thys 

1117 
val user_axioms = axioms_of_thys user_thys 

1118 
val (built_in_defs, built_in_nondefs) = 

1119 
partition_axioms_by_definitionality thy built_in_axioms def_names 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1120 
> filter (is_typedef_axiom thy false) 
33192  1121 
val (user_defs, user_nondefs) = 
1122 
partition_axioms_by_definitionality thy user_axioms def_names 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1123 
val (built_in_nondefs, user_nondefs) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1124 
List.partition (is_typedef_axiom thy false) user_nondefs 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1125 
>> append built_in_nondefs 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1126 
val defs = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1127 
(thy > PureThy.all_thms_of 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1128 
> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1129 
> map (prop_of o snd) > filter is_plain_definition) @ 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1130 
user_defs @ built_in_defs 
33192  1131 
in (defs, built_in_nondefs, user_nondefs) end 
1132 

1133 
(* bool > styp > int option *) 

1134 
fun arity_of_built_in_const fast_descrs (s, T) = 

1135 
if s = @{const_name If} then 

1136 
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3 

1137 
else case AList.lookup (op =) 

1138 
(built_in_consts 

1139 
> fast_descrs ? append built_in_descr_consts) s of 

1140 
SOME n => SOME n 

1141 
 NONE => 

1142 
case AList.lookup (op =) built_in_typed_consts (s, T) of 

1143 
SOME n => SOME n 

1144 
 NONE => 

1145 
if is_fun_type T andalso is_set_type (domain_type T) then 

1146 
AList.lookup (op =) built_in_set_consts s 

1147 
else 

1148 
NONE 

1149 
(* bool > styp > bool *) 

1150 
val is_built_in_const = is_some oo arity_of_built_in_const 

1151 

1152 
(* This function is designed to work for both real definition axioms and 

1153 
simplification rules (equational specifications). *) 

1154 
(* term > term *) 

1155 
fun term_under_def t = 

1156 
case t of 

1157 
@{const "==>"} $ _ $ t2 => term_under_def t2 

1158 
 Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1 

1159 
 @{const Trueprop} $ t1 => term_under_def t1 

1160 
 Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1 

1161 
 Abs (_, _, t') => term_under_def t' 

1162 
 t1 $ _ => term_under_def t1 

1163 
 _ => t 

1164 

1165 
(* Here we crucially rely on "Refute.specialize_type" performing a preorder 

1166 
traversal of the term, without which the wrong occurrence of a constant could 

1167 
be matched in the face of overloading. *) 

1168 
(* theory > bool > const_table > styp > term list *) 

1169 
fun def_props_for_const thy fast_descrs table (x as (s, _)) = 

1170 
if is_built_in_const fast_descrs x then 

1171 
[] 

1172 
else 

1173 
these (Symtab.lookup table s) 

1174 
> map_filter (try (Refute.specialize_type thy x)) 

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

1175 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1176 

33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1177 
(* theory > term > term option *) 
33192  1178 
fun normalized_rhs_of thy t = 
1179 
let 

33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1180 
(* term option > term option *) 
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1181 
fun aux (v as Var _) (SOME t) = SOME (lambda v t) 
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1182 
 aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t) 
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1183 
 aux _ _ = NONE 
33192  1184 
val (lhs, rhs) = 
1185 
case t of 

1186 
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2) 

1187 
 @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) => 

1188 
(t1, t2) 

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

1189 
 _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1190 
val args = strip_comb lhs > snd 
33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1191 
in fold_rev aux args (SOME rhs) end 
33192  1192 

1193 
(* theory > const_table > styp > term option *) 

1194 
fun def_of_const thy table (x as (s, _)) = 

1195 
if is_built_in_const false x orelse original_name s <> s then 

1196 
NONE 

1197 
else 

1198 
x > def_props_for_const thy false table > List.last 

33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1199 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1200 
handle List.Empty => NONE 
1201 

1202 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1203 

1204 
(* term > fixpoint_kind *) 

1205 
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t 

1206 
 fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp 

1207 
 fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp 

1208 
 fixpoint_kind_of_rhs _ = NoFp 

1209 

1210 
(* theory > const_table > term > bool *) 

1211 
fun is_mutually_inductive_pred_def thy table t = 

1212 
let 

1213 
(* term > bool *) 

1214 
fun is_good_arg (Bound _) = true 

1215 
 is_good_arg (Const (s, _)) = 

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

1216 
s = @{const_name True} orelse s = @{const_name False} orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1217 
s = @{const_name undefined} 
33192  1218 
 is_good_arg _ = false 
1219 
in 

1220 
case t > strip_abs_body > strip_comb of 

1221 
(Const x, ts as (_ :: _)) => 

1222 
(case def_of_const thy table x of 

1223 
SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts 

1224 
 NONE => false) 

1225 
 _ => false 

1226 
end 

1227 
(* theory > const_table > term > term *) 

1228 
fun unfold_mutually_inductive_preds thy table = 

1229 
map_aterms (fn t as Const x => 

1230 
(case def_of_const thy table x of 

1231 
SOME t' => 

1232 
let val t' = Envir.eta_contract t' in 

1233 
if is_mutually_inductive_pred_def thy table t' then t' 

1234 
else t 

1235 
end 

1236 
 NONE => t) 

1237 
 t => t) 

1238 

1239 
(* term > string * term *) 

1240 
fun pair_for_prop t = 

1241 
case term_under_def t of 

1242 
Const (s, _) => (s, t) 

1243 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

1244 
 t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) 
33192  1245 

1246 
(* (Proof.context > term list) > Proof.context > const_table *) 

1247 
fun table_for get ctxt = 

1248 
get ctxt > map pair_for_prop > AList.group (op =) > Symtab.make 

1249 

1250 
(* theory > (string * int) list *) 

1251 
fun case_const_names thy = 

1252 
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => 

1253 
if is_basic_datatype dtype_s then 

1254 
I 

1255 
else 

1256 
cons (case_name, AList.lookup (op =) descr index 

1257 
> the > #3 > length)) 

1258 
(Datatype.get_all thy) [] @ 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

1259 
map (apsnd length o snd) (#codatatypes (Data.get thy)) 
33192  1260 

1261 
(* Proof.context > term list > const_table *) 

1262 
fun const_def_table ctxt ts = 

34126  1263 
table_for (map prop_of o Nitpick_Defs.get) ctxt 
33192  1264 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) 
1265 
(map pair_for_prop ts) 

1266 
(* term list > const_table *) 

1267 
fun const_nondef_table ts = 

1268 
fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] 

1269 
> AList.group (op =) > Symtab.make 

1270 
(* Proof.context > const_table *) 

1271 
val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) 

1272 
val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) 

1273 
(* Proof.context > const_table > const_table *) 

1274 
fun inductive_intro_table ctxt def_table = 

1275 
table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) 

1276 
def_table o prop_of) 

1277 
o Nitpick_Intros.get) ctxt 

1278 
(* theory > term list Inttab.table *) 

1279 
fun ground_theorem_table thy = 

1280 
fold ((fn @{const Trueprop} $ t1 => 

1281 
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) 

1282 
 _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty 

1283 

1284 
val basic_ersatz_table = 

1285 
[(@{const_name prod_case}, @{const_name split}), 

1286 
(@{const_name card}, @{const_name card'}), 

1287 
(@{const_name setsum}, @{const_name setsum'}), 

1288 
(@{const_name fold_graph}, @{const_name fold_graph'}), 

1289 
(@{const_name wf}, @{const_name wf'}), 

1290 
(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), 

1291 
(@{const_name wfrec}, @{const_name wfrec'})] 

1292 

1293 
(* theory > (string * string) list *) 

1294 
fun ersatz_table thy = 

33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

1295 
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table 
33192  1296 

1297 
(* const_table Unsynchronized.ref > string > term list > unit *) 

1298 
fun add_simps simp_table s eqs = 

1299 
Unsynchronized.change simp_table 

1300 
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) 

1301 

1302 
(* Similar to "Refute.specialize_type" but returns all matches rather than only 

1303 
the first (preorder) match. *) 

1304 
(* theory > styp > term > term list *) 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1305 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1306 
let 
1307 
(* term > (typ * term) list > (typ * term) list *) 

1308 
fun aux (Const (s', T')) ys = 

1309 
if s = s' then 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1310 
ys > (if AList.defined (op =) ys T' then 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1311 
I 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

1312 
else 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1313 
cons (T', Refute.monomorphic_term 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1314 
(Sign.typ_match thy (T', T) Vartab.empty) t) 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1315 
handle Type.TYPE_MATCH => I 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1316 
 Refute.REFUTE _ => 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1317 
if slack then 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1318 
I 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1319 
else 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
