author  blanchet 
Thu, 05 Nov 2009 17:03:22 +0100  
changeset 33580  45c33e97cb86 
parent 33578  0c3ba1e010d2 
child 33581  e1e77265fb1d 
permissions  rwrr 
33192  1 
(* Title: HOL/Nitpick/Tools/nitpick_hol.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Copyright 2008, 2009 

4 

5 
Auxiliary HOLrelated functions used by Nitpick. 

6 
*) 

7 

8 
signature NITPICK_HOL = 

9 
sig 

10 
type const_table = term list Symtab.table 

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

12 
type unrolled = styp * styp 

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

14 

15 
type extended_context = { 

16 
thy: theory, 

17 
ctxt: Proof.context, 

18 
max_bisim_depth: int, 

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

20 
wfs: (styp option * bool option) list, 

21 
user_axioms: bool option, 

22 
debug: bool, 

23 
destroy_constrs: bool, 

24 
specialize: bool, 

25 
skolemize: bool, 

26 
star_linear_preds: bool, 

27 
uncurry: bool, 

28 
fast_descrs: bool, 

29 
tac_timeout: Time.time option, 

30 
evals: term list, 

31 
case_names: (string * int) list, 

32 
def_table: const_table, 

33 
nondef_table: const_table, 

34 
user_nondefs: term list, 

35 
simp_table: const_table Unsynchronized.ref, 

36 
psimp_table: const_table, 

37 
intro_table: const_table, 

38 
ground_thm_table: term list Inttab.table, 

39 
ersatz_table: (string * string) list, 

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

41 
special_funs: special_fun list Unsynchronized.ref, 

42 
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

43 
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

44 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  45 

46 
val name_sep : string 

47 
val numeral_prefix : string 

48 
val skolem_prefix : string 

49 
val eval_prefix : string 

50 
val original_name : string > string 

51 
val unbox_type : typ > typ 

52 
val string_for_type : Proof.context > typ > string 

53 
val prefix_name : string > string > string 

54 
val short_name : string > string 

55 
val short_const_name : string > string 

56 
val shorten_const_names_in_term : term > term 

57 
val type_match : theory > typ * typ > bool 

58 
val const_match : theory > styp * styp > bool 

59 
val term_match : theory > term * term > bool 

60 
val is_TFree : typ > bool 

61 
val is_higher_order_type : typ > bool 

62 
val is_fun_type : typ > bool 

63 
val is_set_type : typ > bool 

64 
val is_pair_type : typ > bool 

65 
val is_lfp_iterator_type : typ > bool 

66 
val is_gfp_iterator_type : typ > bool 

67 
val is_fp_iterator_type : typ > bool 

68 
val is_boolean_type : typ > bool 

69 
val is_integer_type : typ > bool 

70 
val is_record_type : typ > bool 

71 
val is_number_type : theory > typ > bool 

72 
val const_for_iterator_type : typ > styp 

73 
val nth_range_type : int > typ > typ 

74 
val num_factors_in_type : typ > int 

75 
val num_binder_types : typ > int 

76 
val curried_binder_types : typ > typ list 

77 
val mk_flat_tuple : typ > term list > term 

78 
val dest_n_tuple : int > term > term list 

79 
val instantiate_type : theory > typ > typ > typ > typ 

80 
val is_codatatype : theory > typ > bool 

81 
val is_pure_typedef : theory > typ > bool 

82 
val is_univ_typedef : theory > typ > bool 

83 
val is_datatype : theory > typ > bool 

84 
val is_record_constr : styp > bool 

85 
val is_record_get : theory > styp > bool 

86 
val is_record_update : theory > styp > bool 

87 
val is_abs_fun : theory > styp > bool 

88 
val is_rep_fun : theory > styp > bool 

89 
val is_constr : theory > styp > bool 

90 
val is_sel : string > bool 

91 
val discr_for_constr : styp > styp 

92 
val num_sels_for_constr_type : typ > int 

93 
val nth_sel_name_for_constr_name : string > int > string 

94 
val nth_sel_for_constr : styp > int > styp 

95 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

96 
val sel_no_from_name : string > int 

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

98 
val extensionalize : term > term 

99 
val distinctness_formula : typ > term list > term 

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

101 
val unregister_frac_type : string > theory > theory 

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

103 
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

104 
val datatype_constrs : extended_context > typ > styp list 
33192  105 
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

106 
val num_datatype_constrs : extended_context > typ > int 
33192  107 
val constr_name_for_sel_like : string > string 
108 
val boxed_constr_for_sel : extended_context > styp > styp 

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

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

111 
val bounded_precise_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

112 
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

113 
val is_finite_type : extended_context > typ > bool 
33192  114 
val all_axioms_of : theory > term list * term list * term list 
115 
val arity_of_built_in_const : bool > styp > int option 

116 
val is_built_in_const : bool > styp > bool 

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

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

119 
val const_nondef_table : term list > const_table 

120 
val const_simp_table : Proof.context > const_table 

121 
val const_psimp_table : Proof.context > const_table 

122 
val inductive_intro_table : Proof.context > const_table > const_table 

123 
val ground_theorem_table : theory > term list Inttab.table 

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

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

126 
val is_inductive_pred : extended_context > styp > bool 

127 
val is_constr_pattern_lhs : theory > term > bool 

128 
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

129 
val merge_type_vars_in_terms : term list > term list 
33192  130 
val ground_types_in_type : extended_context > typ > typ list 
131 
val ground_types_in_terms : extended_context > term list > typ list 

132 
val format_type : int list > int list > typ > typ 

133 
val format_term_type : 

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

135 
val user_friendly_const : 

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

137 
> styp > term * typ 

138 
val assign_operator_for_const : styp > string 

139 
val preprocess_term : 

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

141 
end; 

142 

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

143 
structure Nitpick_HOL : NITPICK_HOL = 
33192  144 
struct 
145 

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

146 
open Nitpick_Util 
33192  147 

148 
type const_table = term list Symtab.table 

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

150 
type unrolled = styp * styp 

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

152 

153 
type extended_context = { 

154 
thy: theory, 

155 
ctxt: Proof.context, 

156 
max_bisim_depth: int, 

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

158 
wfs: (styp option * bool option) list, 

159 
user_axioms: bool option, 

160 
debug: bool, 

161 
destroy_constrs: bool, 

162 
specialize: bool, 

163 
skolemize: bool, 

164 
star_linear_preds: bool, 

165 
uncurry: bool, 

166 
fast_descrs: bool, 

167 
tac_timeout: Time.time option, 

168 
evals: term list, 

169 
case_names: (string * int) list, 

170 
def_table: const_table, 

171 
nondef_table: const_table, 

172 
user_nondefs: term list, 

173 
simp_table: const_table Unsynchronized.ref, 

174 
psimp_table: const_table, 

175 
intro_table: const_table, 

176 
ground_thm_table: term list Inttab.table, 

177 
ersatz_table: (string * string) list, 

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

179 
special_funs: special_fun list Unsynchronized.ref, 

180 
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

181 
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

182 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  183 

184 
structure TheoryData = TheoryDataFun( 

185 
type T = {frac_types: (string * (string * string) list) list, 

186 
codatatypes: (string * (string * styp list)) list} 

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

188 
val copy = I 

189 
val extend = I 

190 
fun merge _ ({frac_types = fs1, codatatypes = cs1}, 

191 
{frac_types = fs2, codatatypes = cs2}) = 

192 
{frac_types = AList.merge (op =) (op =) (fs1, fs2), 

193 
codatatypes = AList.merge (op =) (op =) (cs1, cs2)}) 

194 

195 
(* term * term > term *) 

196 
fun s_conj (t1, @{const True}) = t1 

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

198 
 s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False} 

199 
else HOLogic.mk_conj (t1, t2) 

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

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

202 
 s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True} 

203 
else HOLogic.mk_disj (t1, t2) 

204 
(* term > term > term *) 

205 
fun mk_exists v t = 

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

207 

208 
(* term > term > term list *) 

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

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

211 
 strip_connective _ t = [t] 

212 
(* term > term list * term *) 

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

214 
if t0 mem [@{const "op &"}, @{const "op "}] then 

215 
(strip_connective t0 t, t0) 

216 
else 

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

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

219 
(* term > term list *) 

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

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

222 

223 
val name_sep = "$" 

224 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

225 
val sel_prefix = nitpick_prefix ^ "sel" 

226 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

227 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

228 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

229 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

230 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

231 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

232 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

233 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

234 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

235 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

236 
val skolem_prefix = nitpick_prefix ^ "sk" 

237 
val special_prefix = nitpick_prefix ^ "sp" 

238 
val uncurry_prefix = nitpick_prefix ^ "unc" 

239 
val eval_prefix = nitpick_prefix ^ "eval" 

240 
val bound_var_prefix = "b" 

241 
val cong_var_prefix = "c" 

242 
val iter_var_prefix = "i" 

243 
val val_var_prefix = nitpick_prefix ^ "v" 

244 
val arg_var_prefix = "x" 

245 

246 
(* int > string *) 

247 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

248 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

249 
(* int > int > string *) 

250 
fun skolem_prefix_for k j = 

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

252 
fun uncurry_prefix_for k j = 

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

254 

255 
(* string > string * string *) 

256 
val strip_first_name_sep = 

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

258 
#> pairself Substring.string 

259 
(* string > string *) 

260 
fun original_name s = 

261 
if String.isPrefix nitpick_prefix s then 

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

263 
else 

264 
s 

265 
val after_name_sep = snd o strip_first_name_sep 

266 

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

268 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  269 
well. *) 
270 
val built_in_consts = 

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

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

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

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

275 
(@{const_name Trueprop}, 1), 

276 
(@{const_name Not}, 1), 

277 
(@{const_name False}, 0), 

278 
(@{const_name True}, 0), 

279 
(@{const_name All}, 1), 

280 
(@{const_name Ex}, 1), 

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

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

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

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

285 
(@{const_name If}, 3), 

286 
(@{const_name Let}, 2), 

287 
(@{const_name Unity}, 0), 

288 
(@{const_name Pair}, 2), 

289 
(@{const_name fst}, 1), 

290 
(@{const_name snd}, 1), 

291 
(@{const_name Id}, 0), 

292 
(@{const_name insert}, 2), 

293 
(@{const_name converse}, 1), 

294 
(@{const_name trancl}, 1), 

295 
(@{const_name rel_comp}, 2), 

296 
(@{const_name image}, 2), 

297 
(@{const_name Suc}, 0), 

298 
(@{const_name finite}, 1), 

299 
(@{const_name nat}, 0), 

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

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

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

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

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

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

306 
(@{const_name div_nat_inst.mod_nat}, 0), 

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

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

309 
(@{const_name nat_gcd}, 0), 

310 
(@{const_name nat_lcm}, 0), 

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

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

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

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

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

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

317 
(@{const_name div_int_inst.mod_int}, 0), 

33571  318 
(@{const_name uminus_int_inst.uminus_int}, 0), 
33192  319 
(@{const_name ord_int_inst.less_int}, 2), 
320 
(@{const_name ord_int_inst.less_eq_int}, 2), 

321 
(@{const_name Tha}, 1), 

322 
(@{const_name Frac}, 0), 

323 
(@{const_name norm_frac}, 0)] 

324 
val built_in_descr_consts = 

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

326 
(@{const_name Eps}, 1)] 

327 
val built_in_typed_consts = 

328 
[((@{const_name of_nat}, nat_T > int_T), 0)] 

329 
val built_in_set_consts = 

330 
[(@{const_name lower_semilattice_fun_inst.inf_fun}, 2), 

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

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

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

334 

335 
(* typ > typ *) 

336 
fun unbox_type (Type (@{type_name fun_box}, Ts)) = 

337 
Type ("fun", map unbox_type Ts) 

338 
 unbox_type (Type (@{type_name pair_box}, Ts)) = 

339 
Type ("*", map unbox_type Ts) 

340 
 unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts) 

341 
 unbox_type T = T 

342 
(* Proof.context > typ > string *) 

343 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type 

344 

345 
(* string > string > string *) 

346 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

347 
(* string > string *) 

348 
fun short_name s = List.last (space_explode "." s) handle List.Empty => "" 

349 
(* string > term > term *) 

350 
val prefix_abs_vars = Term.map_abs_vars o prefix_name 

351 
(* term > term *) 

352 
val shorten_abs_vars = Term.map_abs_vars short_name 

353 
(* string > string *) 

354 
fun short_const_name s = 

355 
case space_explode name_sep s of 

356 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix 

357 
 ss => map short_name ss > space_implode "_" 

358 
(* term > term *) 

359 
val shorten_const_names_in_term = 

360 
map_aterms (fn Const (s, T) => Const (short_const_name s, T)  t => t) 

361 

362 
(* theory > typ * typ > bool *) 

363 
fun type_match thy (T1, T2) = 

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

365 
handle Type.TYPE_MATCH => false 

366 
(* theory > styp * styp > bool *) 

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

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

369 
(* theory > term * term > bool *) 

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

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

372 
const_match thy ((short_name s1, T1), (short_name s2, T2)) 

373 
 term_match thy (t1, t2) = t1 aconv t2 

374 

375 
(* typ > bool *) 

376 
fun is_TFree (TFree _) = true 

377 
 is_TFree _ = false 

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

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

380 
 is_higher_order_type _ = false 

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

382 
 is_fun_type _ = false 

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

384 
 is_set_type _ = false 

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

386 
 is_pair_type _ = false 

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

388 
 is_lfp_iterator_type _ = false 

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

390 
 is_gfp_iterator_type _ = false 

391 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

392 
val is_boolean_type = equal prop_T orf equal bool_T 

393 
val is_integer_type = 

394 
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type 

395 
val is_record_type = not o null o Record.dest_recTs 

396 
(* theory > typ > bool *) 

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

398 
not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy)) 

399 
s))) 

400 
 is_frac_type _ _ = false 

401 
fun is_number_type thy = is_integer_type orf is_frac_type thy 

402 

403 
(* bool > styp > typ *) 

404 
fun iterator_type_for_const gfp (s, T) = 

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

406 
binder_types T) 

407 
(* typ > styp *) 

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

409 
 const_for_iterator_type T = 

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

410 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  411 

412 
(* int > typ > typ * typ *) 

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

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

415 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

418 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  419 
(* typ > typ *) 
420 
val nth_range_type = snd oo strip_n_binders 

421 

422 
(* typ > int *) 

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

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

425 
 num_factors_in_type _ = 1 

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

427 
 num_binder_types _ = 0 

428 
(* typ > typ list *) 

429 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

430 
fun maybe_curried_binder_types T = 

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

432 

433 
(* typ > term list > term *) 

434 
fun mk_flat_tuple _ [t] = t 

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

436 
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

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

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

441 

442 
(* int > typ > typ list *) 

443 
fun dest_n_tuple_type 1 T = [T] 

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

445 
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

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

447 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  448 

449 
(* (typ * typ) list > typ > typ *) 

450 
fun typ_subst [] T = T 

451 
 typ_subst ps T = 

452 
let 

453 
(* typ > typ *) 

454 
fun subst T = 

455 
case AList.lookup (op =) ps T of 

456 
SOME T' => T' 

457 
 NONE => case T of Type (s, Ts) => Type (s, map subst Ts)  _ => T 

458 
in subst T end 

459 

460 
(* theory > typ > typ > typ > typ *) 

461 
fun instantiate_type thy T1 T1' T2 = 

462 
Same.commit (Envir.subst_type_same 

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

464 
(Logic.varifyT T2) 

465 
handle Type.TYPE_MATCH => 

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

466 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  467 

468 
(* theory > typ > typ > styp *) 

469 
fun repair_constr_type thy body_T' T = 

470 
instantiate_type thy (body_type T) body_T' T 

471 

472 
(* string > (string * string) list > theory > theory *) 

473 
fun register_frac_type frac_s ersaetze thy = 

474 
let 

475 
val {frac_types, codatatypes} = TheoryData.get thy 

476 
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types 

477 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end 

478 
(* string > theory > theory *) 

479 
fun unregister_frac_type frac_s = register_frac_type frac_s [] 

480 

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

482 
fun register_codatatype co_T case_name constr_xs thy = 

483 
let 

484 
val {frac_types, codatatypes} = TheoryData.get thy 

485 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 

486 
val (co_s, co_Ts) = dest_Type co_T 

487 
val _ = 

488 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then () 

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

489 
else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  490 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
491 
codatatypes 

492 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end 

493 
(* typ > theory > theory *) 

494 
fun unregister_codatatype co_T = register_codatatype co_T "" [] 

495 

496 
type typedef_info = 

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

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

499 
Rep_inverse: thm option} 

500 

501 
(* theory > string > typedef_info *) 

502 
fun typedef_info thy s = 

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

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

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

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

507 
> Logic.varify, 

508 
set_name = @{const_name Frac}, Rep_inverse = NONE} 

509 
else case Typedef.get_info thy s of 

510 
SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse, 

511 
...} => 

512 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 

513 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 

514 
set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse} 

515 
 NONE => NONE 

516 

517 
(* string > bool *) 

518 
fun is_basic_datatype s = 

519 
s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit}, 

520 
@{type_name nat}, @{type_name int}] 

521 
(* theory > string > bool *) 

522 
val is_typedef = is_some oo typedef_info 

523 
val is_real_datatype = is_some oo Datatype.get_info 

524 
(* theory > typ > bool *) 

525 
fun is_codatatype thy (T as Type (s, _)) = 

526 
not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s 

527 
> Option.map snd > these)) 

528 
 is_codatatype _ _ = false 

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

530 
is_typedef thy s andalso 

531 
not (is_real_datatype thy s orelse is_codatatype thy T 

532 
orelse is_record_type T orelse is_integer_type T) 

533 
 is_pure_typedef _ _ = false 

534 
fun is_univ_typedef thy (Type (s, _)) = 

535 
(case typedef_info thy s of 

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

537 
(case set_def of 

538 
SOME thm => 

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

540 
 NONE => 

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

542 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV} 

543 
 NONE => false) 

544 
 is_univ_typedef _ _ = false 

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

546 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind}) 

547 
andalso not (is_basic_datatype s) 

548 
 is_datatype _ _ = false 

549 

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

551 
fun all_record_fields thy T = 

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

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

554 
end 

555 
handle TYPE _ => [] 

556 
(* styp > bool *) 

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

558 
String.isSuffix Record.extN s andalso 

559 
let val dataT = body_type T in 

560 
is_record_type dataT andalso 

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

562 
end 

563 
(* theory > typ > int *) 

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

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

566 
fun no_of_record_field thy s T1 = 

567 
find_index (equal s o fst) (Record.get_extT_fields thy T1 > single > op @) 

568 
(* theory > styp > bool *) 

569 
fun is_record_get thy (s, Type ("fun", [T1, _])) = 

570 
exists (equal s o fst) (all_record_fields thy T1) 

571 
 is_record_get _ _ = false 

572 
fun is_record_update thy (s, T) = 

573 
String.isSuffix Record.updateN s andalso 

574 
exists (equal (unsuffix Record.updateN s) o fst) 

575 
(all_record_fields thy (body_type T)) 

576 
handle TYPE _ => false 

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

578 
(case typedef_info thy s' of 

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

580 
 NONE => false) 

581 
 is_abs_fun _ _ = false 

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

583 
(case typedef_info thy s' of 

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

585 
 NONE => false) 

586 
 is_rep_fun _ _ = false 

587 

588 
(* theory > styp > styp *) 

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

590 
(case typedef_info thy s' of 

591 
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

592 
 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

593 
 mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) 
33192  594 

595 
(* theory > styp > bool *) 

596 
fun is_coconstr thy (s, T) = 

597 
let 

598 
val {codatatypes, ...} = TheoryData.get thy 

599 
val co_T = body_type T 

600 
val co_s = dest_Type co_T > fst 

601 
in 

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

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

604 
end 

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

606 
fun is_constr_like thy (s, T) = 

607 
s mem [@{const_name FunBox}, @{const_name PairBox}] orelse 

608 
let val (x as (s, T)) = (s, unbox_type T) in 

609 
Refute.is_IDT_constructor thy x orelse is_record_constr x 

610 
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) 

611 
orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}] 

612 
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) 

613 
orelse is_coconstr thy x 

614 
end 

615 
fun is_constr thy (x as (_, T)) = 

616 
is_constr_like thy x 

617 
andalso not (is_basic_datatype (fst (dest_Type (body_type T)))) 

618 
(* string > bool *) 

619 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

620 
val is_sel_like_and_no_discr = 

621 
String.isPrefix sel_prefix 

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

623 

624 
datatype boxability = 

625 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

626 

627 
(* boxability > boxability *) 

628 
fun in_fun_lhs_for InConstr = InSel 

629 
 in_fun_lhs_for _ = InFunLHS 

630 
fun in_fun_rhs_for InConstr = InConstr 

631 
 in_fun_rhs_for InSel = InSel 

632 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

633 
 in_fun_rhs_for _ = InFunRHS1 

634 

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

636 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

637 
case T of 

638 
Type ("fun", _) => 

639 
boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T)) 

640 
 Type ("*", Ts) => 

641 
boxy mem [InPair, InFunRHS1, InFunRHS2] 

642 
orelse (boxy mem [InExpr, InFunLHS] 

643 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 

644 
(map (box_type ext_ctxt InPair) Ts)) 

645 
 _ => false 

646 
(* extended_context > boxability > string * typ list > string *) 

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

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

649 
SOME (SOME box_me) => box_me 

650 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

651 
(* extended_context > boxability > typ > typ *) 

652 
and box_type ext_ctxt boxy T = 

653 
case T of 

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

655 
if not (boxy mem [InConstr, InSel]) 

656 
andalso should_box_type ext_ctxt boxy z then 

657 
Type (@{type_name fun_box}, 

658 
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) 

659 
else 

660 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

661 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

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

663 
if should_box_type ext_ctxt boxy z then 

664 
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts) 

665 
else 

666 
Type ("*", map (box_type ext_ctxt 

667 
(if boxy mem [InConstr, InSel] then boxy 

668 
else InPair)) Ts) 

669 
 _ => T 

670 

671 
(* styp > styp *) 

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

673 

674 
(* typ > int *) 

675 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

676 
(* string > int > string *) 

677 
fun nth_sel_name_for_constr_name s n = 

678 
if s = @{const_name Pair} then 

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

680 
else 

681 
sel_prefix_for n ^ s 

682 
(* styp > int > styp *) 

683 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

684 
 nth_sel_for_constr (s, T) n = 

685 
(nth_sel_name_for_constr_name s n, 

686 
body_type T > nth (maybe_curried_binder_types T) n) 

687 
(* extended_context > styp > int > styp *) 

688 
fun boxed_nth_sel_for_constr ext_ctxt = 

689 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

690 

691 
(* string > int *) 

692 
fun sel_no_from_name s = 

693 
if String.isPrefix discr_prefix s then 

694 
~1 

695 
else if String.isPrefix sel_prefix s then 

696 
s > unprefix sel_prefix > Int.fromString > the 

697 
else if s = @{const_name snd} then 

698 
1 

699 
else 

700 
0 

701 

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

703 
fun eta_expand _ t 0 = t 

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

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

706 
 eta_expand Ts t n = 

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

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

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

710 

711 
(* term > term *) 

712 
fun extensionalize t = 

713 
case t of 

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

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

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

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

718 
end 

719 
 _ => t 

720 

721 
(* typ > term list > term *) 

722 
fun distinctness_formula T = 

723 
all_distinct_unordered_pairs_of 

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

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

726 

727 
(* typ > term *) 

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

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

730 

731 
(* theory > 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

732 
fun uncached_datatype_constrs thy (T as Type (s, Ts)) = 
33192  733 
if is_datatype thy T then 
734 
case Datatype.get_info thy s of 

735 
SOME {index, descr, ...} => 

736 
let val (_, dtyps, constrs) = AList.lookup (op =) descr index > the in 

737 
map (fn (s', Us) => 

738 
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us > T)) 

739 
constrs 

740 
end 

741 
 NONE => 

742 
case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of 

743 
SOME (_, xs' as (_ :: _)) => 

744 
map (apsnd (repair_constr_type thy T)) xs' 

745 
 _ => 

746 
if is_record_type T then 

747 
let 

748 
val s' = unsuffix Record.ext_typeN s ^ Record.extN 

749 
val T' = (Record.get_extT_fields thy T 

750 
> apsnd single > uncurry append > map snd) > T 

751 
in [(s', T')] end 

752 
else case typedef_info thy s of 

753 
SOME {abs_type, rep_type, Abs_name, ...} => 

754 
[(Abs_name, instantiate_type thy abs_type T rep_type > T)] 

755 
 NONE => 

756 
if T = @{typ ind} then 

757 
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] 

758 
else 

759 
[] 

760 
else 

761 
[] 

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

762 
 uncached_datatype_constrs _ _ = [] 
33192  763 
(* 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

764 
fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context) 
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

765 
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

766 
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

767 
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

768 
 NONE => 
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

769 
let val xs = uncached_datatype_constrs thy T in 
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

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

771 
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

772 
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

773 
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

774 
(* extended_context > typ > int *) 
33192  775 
val num_datatype_constrs = length oo datatype_constrs 
776 

777 
(* string > string *) 

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

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

780 
 constr_name_for_sel_like s' = original_name s' 

781 
(* extended_context > styp > styp *) 

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

783 
let val s = constr_name_for_sel_like s' in 

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

785 
> the > pair s 

786 
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

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

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

791 
Abs (Name.uu, dataT, 

792 
@{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

793 
else if num_datatype_constrs ext_ctxt dataT >= 2 then 
33192  794 
Const (discr_for_constr x) 
795 
else 

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

797 
end 

798 

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

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

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

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

804 
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

805 
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

806 
 _ => betapply (discr_term_for_constr ext_ctxt x, t) 
33192  807 

808 
(* styp > term > term *) 

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

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

811 
if dataT = nat_T then 

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

813 
else if is_pair_type dataT then 

814 
Const (nth_sel_for_constr x n) 

815 
else 

816 
let 

817 
(* int > typ > int * term *) 

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

819 
let 

820 
val (m, t1) = aux m T1 

821 
val (m, t2) = aux m T2 

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

823 
 aux m T = 

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

825 
$ Bound 0) 

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

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

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

829 
end 

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

831 
fun select_nth_constr_arg thy x t n res_T = 

832 
case strip_comb t of 

833 
(Const x', args) => 

834 
if x = x' then nth args n 

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

836 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

838 

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

840 
fun construct_value _ x [] = Const x 

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

842 
let val args = map Envir.eta_contract args in 

843 
case hd args of 

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

845 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

846 
andalso forall (fn (n, t') => 

847 
select_nth_constr_arg thy x t n dummyT = t') 

848 
(index_seq 0 (length args) ~~ args) then 

849 
t 

850 
else 

851 
list_comb (Const x, args) 

852 
 _ => list_comb (Const x, args) 

853 
end 

854 

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

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

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

859 
 _ => raise SAME ()) 

860 
handle SAME () => 

861 
let 

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

863 
if is_pair_type T then 

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

865 
(@{const_name Pair}, [T1, T2] > T) 

866 
end 

867 
else 

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

868 
datatype_constrs ext_ctxt T > the_single 
33192  869 
val arg_Ts = binder_types T' 
870 
in 

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

872 
(index_seq 0 (length arg_Ts)) arg_Ts) 

873 
end 

874 

875 
(* (typ * int) list > typ > int *) 

876 
fun card_of_type asgns (Type ("fun", [T1, T2])) = 

877 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) 

878 
 card_of_type asgns (Type ("*", [T1, T2])) = 

879 
card_of_type asgns T1 * card_of_type asgns T2 

880 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 

881 
 card_of_type _ @{typ prop} = 2 

882 
 card_of_type _ @{typ bool} = 2 

883 
 card_of_type _ @{typ unit} = 1 

884 
 card_of_type asgns T = 

885 
case AList.lookup (op =) asgns T of 

886 
SOME k => k 

887 
 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

888 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
33192  889 
(* int > (typ * int) list > typ > int *) 
890 
fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = 

891 
let 

892 
val k1 = bounded_card_of_type max default_card asgns T1 

893 
val k2 = bounded_card_of_type max default_card asgns T2 

894 
in 

895 
if k1 = max orelse k2 = max then max 

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

897 
end 

898 
 bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) = 

899 
let 

900 
val k1 = bounded_card_of_type max default_card asgns T1 

901 
val k2 = bounded_card_of_type max default_card asgns T2 

902 
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end 

903 
 bounded_card_of_type max default_card asgns T = 

904 
Int.min (max, if default_card = ~1 then 

905 
card_of_type asgns T 

906 
else 

907 
card_of_type asgns T 

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

908 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
33192  909 
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

910 
(* extended_context > 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

911 
fun bounded_precise_card_of_type ext_ctxt max default_card asgns T = 
33192  912 
let 
913 
(* typ list > typ > int *) 

914 
fun aux avoid T = 

915 
(if T mem avoid then 

916 
0 

917 
else case T of 

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

919 
let 

920 
val k1 = aux avoid T1 

921 
val k2 = aux avoid T2 

922 
in 

923 
if k1 = 0 orelse k2 = 0 then 0 

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

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

926 
end 

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

928 
let 

929 
val k1 = aux avoid T1 

930 
val k2 = aux avoid T2 

931 
in 

932 
if k1 = 0 orelse k2 = 0 then 0 

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

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

935 
end 

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

937 
 @{typ prop} => 2 

938 
 @{typ bool} => 2 

939 
 @{typ unit} => 1 

940 
 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

941 
(case datatype_constrs ext_ctxt T of 
33192  942 
[] => if is_integer_type T then 0 else raise SAME () 
943 
 constrs => 

944 
let 

945 
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

946 
datatype_constrs ext_ctxt T 
33192  947 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
948 
o snd) 

949 
in 

950 
if exists (equal 0) constr_cards then 0 

951 
else Integer.sum constr_cards 

952 
end) 

953 
 _ => raise SAME ()) 

954 
handle SAME () => AList.lookup (op =) asgns T > the_default default_card 

955 
in Int.min (max, aux [] T) end 

956 

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

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

958 
fun is_finite_type 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

959 
not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 [] 
33192  960 

961 
(* term > bool *) 

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

963 
 is_ground_term (Const _) = true 

964 
 is_ground_term _ = false 

965 

966 
(* term > word > word *) 

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

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

969 
 hashw_term _ = 0w0 

970 
(* term > int *) 

971 
val hash_term = Word.toInt o hashw_term 

972 

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

974 
fun special_bounds ts = 

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

976 

977 
(* indexname * typ > term > term *) 

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

979 

33571  980 
(* theory > string > bool *) 
981 
fun is_funky_typedef_name thy s = 

982 
s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, 

983 
@{type_name int}] 

984 
orelse is_frac_type thy (Type (s, [])) 

985 
(* theory > term > bool *) 

986 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 

987 
 is_funky_typedef _ _ = false 

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

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

991 
 is_arity_type_axiom _ = false 

992 
(* theory > bool > term > bool *) 

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

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

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

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

997 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  998 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  999 
 is_typedef_axiom _ _ _ = false 
1000 

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

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

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

1004 
using "typedef_info". *) 

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

1006 
fun partition_axioms_by_definitionality thy axioms def_names = 

1007 
let 

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

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

1010 
val nondefs = 

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

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

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

1014 

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

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

1016 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1017 
commands. *) 
1018 
(* theory > bool *) 

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

1020 

1021 
(* term > bool *) 

1022 
val is_plain_definition = 

1023 
let 

1024 
(* term > bool *) 

1025 
fun do_lhs t1 = 

1026 
case strip_comb t1 of 

1027 
(Const _, args) => forall is_Var args 

1028 
andalso not (has_duplicates (op =) args) 

1029 
 _ => false 

1030 
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 

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

1032 
do_lhs t1 

1033 
 do_eq _ = false 

1034 
in do_eq end 

1035 

1036 
(* theory > term list * term list * term list *) 

1037 
fun all_axioms_of thy = 

1038 
let 

1039 
(* theory list > term list *) 

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

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

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

1042 
val def_names = specs > maps snd > filter #is_def > map #name 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1043 
> OrdList.make fast_string_ord 
33192  1044 
val thys = thy :: Theory.ancestors_of thy 
1045 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1046 
val built_in_axioms = axioms_of_thys built_in_thys 

1047 
val user_axioms = axioms_of_thys user_thys 

1048 
val (built_in_defs, built_in_nondefs) = 

1049 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1050 
> filter (is_typedef_axiom thy false) 
33192  1051 
val (user_defs, user_nondefs) = 
1052 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

1055 
>> append built_in_nondefs 
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

1056 
val defs = (thy > PureThy.all_thms_of 
33192  1057 
> filter (equal Thm.definitionK o Thm.get_kind o snd) 
1058 
> map (prop_of o snd) > filter is_plain_definition) @ 

1059 
user_defs @ built_in_defs 

1060 
in (defs, built_in_nondefs, user_nondefs) end 

1061 

1062 
(* bool > styp > int option *) 

1063 
fun arity_of_built_in_const fast_descrs (s, T) = 

1064 
if s = @{const_name If} then 

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

1066 
else case AList.lookup (op =) 

1067 
(built_in_consts 

1068 
> fast_descrs ? append built_in_descr_consts) s of 

1069 
SOME n => SOME n 

1070 
 NONE => 

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

1072 
SOME n => SOME n 

1073 
 NONE => 

1074 
if is_fun_type T andalso is_set_type (domain_type T) then 

1075 
AList.lookup (op =) built_in_set_consts s 

1076 
else 

1077 
NONE 

1078 
(* bool > styp > bool *) 

1079 
val is_built_in_const = is_some oo arity_of_built_in_const 

1080 

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

1082 
simplification rules (equational specifications). *) 

1083 
(* term > term *) 

1084 
fun term_under_def t = 

1085 
case t of 

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

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

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

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

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

1091 
 t1 $ _ => term_under_def t1 

1092 
 _ => t 

1093 

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

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

1096 
be matched in the face of overloading. *) 

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

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

1099 
if is_built_in_const fast_descrs x then 

1100 
[] 

1101 
else 

1102 
these (Symtab.lookup table s) 

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

1104 
> filter (equal (Const x) o term_under_def) 

1105 

1106 
(* term > term *) 

1107 
fun normalized_rhs_of thy t = 

1108 
let 

1109 
(* term > term *) 

1110 
fun aux (v as Var _) t = lambda v t 

1111 
 aux (c as Const (@{const_name TYPE}, T)) t = lambda c t 

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

1112 
 aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1113 
val (lhs, rhs) = 
1114 
case t of 

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

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

1117 
(t1, t2) 

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

1118 
 _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1119 
val args = strip_comb lhs > snd 
1120 
in fold_rev aux args rhs end 

1121 

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

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

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

1125 
NONE 

1126 
else 

1127 
x > def_props_for_const thy false table > List.last 

1128 
> normalized_rhs_of thy > prefix_abs_vars s > SOME 

1129 
handle List.Empty => NONE 

1130 

1131 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1132 

1133 
(* term > fixpoint_kind *) 

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

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

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

1137 
 fixpoint_kind_of_rhs _ = NoFp 

1138 

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

1140 
fun is_mutually_inductive_pred_def thy table t = 

1141 
let 

1142 
(* term > bool *) 

1143 
fun is_good_arg (Bound _) = true 

1144 
 is_good_arg (Const (s, _)) = 

1145 
s mem [@{const_name True}, @{const_name False}, @{const_name undefined}] 

1146 
 is_good_arg _ = false 

1147 
in 

1148 
case t > strip_abs_body > strip_comb of 

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

1150 
(case def_of_const thy table x of 

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

1152 
 NONE => false) 

1153 
 _ => false 

1154 
end 

1155 
(* theory > const_table > term > term *) 

1156 
fun unfold_mutually_inductive_preds thy table = 

1157 
map_aterms (fn t as Const x => 

1158 
(case def_of_const thy table x of 

1159 
SOME t' => 

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

1161 
if is_mutually_inductive_pred_def thy table t' then t' 

1162 
else t 

1163 
end 

1164 
 NONE => t) 

1165 
 t => t) 

1166 

1167 
(* term > string * term *) 

1168 
fun pair_for_prop t = 

1169 
case term_under_def t of 

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

1171 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1175 
fun table_for get ctxt = 

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

1177 

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

1179 
fun case_const_names thy = 

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

1181 
if is_basic_datatype dtype_s then 

1182 
I 

1183 
else 

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

1185 
> the > #3 > length)) 

1186 
(Datatype.get_all thy) [] @ 

1187 
map (apsnd length o snd) (#codatatypes (TheoryData.get thy)) 

1188 

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

1190 
fun const_def_table ctxt ts = 

1191 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

1192 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) 

1193 
(map pair_for_prop ts) 

1194 
(* term list > const_table *) 

1195 
fun const_nondef_table ts = 

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

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

1198 
(* Proof.context > const_table *) 

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

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

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

1202 
fun inductive_intro_table ctxt def_table = 

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

1204 
def_table o prop_of) 

1205 
o Nitpick_Intros.get) ctxt 

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

1207 
fun ground_theorem_table thy = 

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

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

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

1211 

1212 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1220 

1221 
(* theory > (string * string) list *) 

1222 
fun ersatz_table thy = 

1223 
fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table 

1224 

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

1226 
fun add_simps simp_table s eqs = 

1227 
Unsynchronized.change simp_table 

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

1229 

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

1231 
the first (preorder) match. *) 

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

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

1233 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1234 
let 
1235 
(* term > (typ * term) list > (typ * term) list *) 

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

1237 
if s = s' then 

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

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

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

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

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

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

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

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

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

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

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

1248 
raise NOT_SUPPORTED ("too much polymorphism in \ 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1249 
\axiom involving " ^ quote s)) 
33192  1250 
else 
1251 
ys 

1252 
 aux _ ys = ys 

1253 
in map snd (fold_aterms aux t []) end 

1254 

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

1255 
(* theory > bool > const_table > styp > term list *) 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1256 
fun nondef_props_for_const thy slack table (x as (s, _)) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1257 
these (Symtab.lookup table s) > maps (multi_specialize_type thy slack x) 
33192  1258 

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

1260 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

1261 
let val abs_T = Type (abs_s, abs_Ts) in 

1262 
if is_univ_typedef thy abs_T then 

1263 
[] 

1264 
else case typedef_info thy abs_s of 

1265 
SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name, 

1266 
...} => 

1267 
let 

1268 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

1269 
val rep_t = Const (Rep_name, abs_T > rep_T) 

1270 
val set_t = Const (set_name, rep_T > bool_T) 

1271 
val set_t' = 

1272 
prop_of_Rep > HOLogic.dest_Trueprop 

1273 
> Refute.specialize_type thy (dest_Const rep_t) 

1274 
> HOLogic.dest_mem > snd 

1275 
in 

1276 
[HOLogic.all_const abs_T 

1277 
$ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))] 

1278 
> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t')) 

1279 
> map HOLogic.mk_Trueprop 

1280 
end 

1281 
 NONE => [] 

1282 
end 

1283 
(* theory > styp > term *) 

1284 
fun inverse_axiom_for_rep_fun thy (x as (_, T)) = 

1285 
typedef_info thy (fst (dest_Type (domain_type T))) 

1286 
> the > #Rep_inverse > the > prop_of > Refute.specialize_type thy x 

1287 

1288 
(* theory > int * styp > term *) 

1289 
fun constr_case_body thy (j, (x as (_, T))) = 

1290 
let val arg_Ts = binder_types T in 

1291 
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0)) 

1292 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1293 
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

1294 
(* extended_context > typ > int * 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

1295 
fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t = 
33192  1296 
Const (@{const_name If}, [bool_T, res_T, res_T] > res_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

1297 
$ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x) 
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

1298 
$ res_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

1299 
(* extended_context > typ > typ > 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

1300 
fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T = 
33192  1301 
let 
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

1302 
val xs = datatype_constrs ext_ctxt dataT 
33192  1303 
val func_Ts = map ((fn T => binder_types T > res_T) o snd) xs 
1304 
val (xs', x) = split_last xs 

1305 
in 

1306 
constr_case_body thy (1, x) 

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

1307 
> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs') 
33192  1308 
> fold_rev (curry absdummy) (func_Ts @ [dataT]) 
1309 
end 

1310 

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

1311 
(* extended_context > string > typ > 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

1312 
fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T 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

1313 
let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in 
33192  1314 
case no_of_record_field thy s rec_T of 
1315 
~1 => (case rec_T of 

1316 
Type (_, Ts as _ :: _) => 

1317 
let 

1318 
val rec_T' = List.last Ts 

1319 
val j = num_record_fields thy rec_T  1 

1320 
in 

1321 
select_nth_constr_arg thy constr_x t j res_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

1322 
> optimized_record_get ext_ctxt s rec_T' res_T 
33192  1323 
end 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1324 
 _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1325 
[])) 
33192  1326 
 j => select_nth_constr_arg thy constr_x t j res_T 
1327 
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

1328 
(* extended_context > string > typ > term > 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

1329 
fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t = 
33192  1330 
let 
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

1331 
val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T) 
33192  1332 
val Ts = binder_types constr_T 
1333 
val n = length Ts 

1334 
val special_j = no_of_record_field thy s rec_T 

1335 
val ts = map2 (fn j => fn T => 

1336 
let 

1337 
val t = select_nth_constr_arg thy constr_x rec_t j T 

1338 
in 

1339 
if j = special_j then 

1340 
betapply (fun_t, t) 

1341 
else if j = n  1 andalso special_j = ~1 then 

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

1342 
optimized_record_update ext_ctxt s 
33192  1343 
(rec_T > dest_Type > snd > List.last) fun_t t 
1344 
else 

1345 
t 

1346 
end) (index_seq 0 n) Ts 

1347 
in list_comb (Const constr_x, ts) end 

1348 

1349 
(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a 

1350 
constant, are said to be trivial. For those, we ignore the simplification 

1351 
rules and use the definition instead, to ensure that builtin symbols like 

1352 
"ord_nat_inst.less_eq_nat" are picked up correctly. *) 

1353 
(* theory > const_table > styp > bool *) 

1354 
fun has_trivial_definition thy table x = 

1355 
case def_of_const thy table x of SOME (Const _) => true  _ => false 

1356 

1357 
(* theory > const_table > string * typ > fixpoint_kind *) 

1358 
fun fixpoint_kind_of_const thy table x = 

1359 
if is_built_in_const false x then 

1360 
NoFp 

1361 
else 

1362 
fixpoint_kind_of_rhs (the (def_of_const thy table x)) 

1363 
handle Option.Option => NoFp 

1364 

1365 
(* extended_context > styp > bool *) 

1366 
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...} 

1367 
: extended_context) x = 

1368 
not (null (def_props_for_const thy fast_descrs intro_table x)) 

1369 
andalso fixpoint_kind_of_const thy def_table x <> NoFp 

1370 
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...} 

1371 
: extended_context) x = 

1372 
exists (fn table => not (null (def_props_for_const thy fast_descrs table x))) 

1373 
[!simp_table, psimp_table] 

1374 
fun is_inductive_pred ext_ctxt = 

1375 
is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt) 

1376 
fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) = 

1377 
(is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt 

1378 
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) 

1379 
andf (not o has_trivial_definition thy def_table) 
