author  blanchet 
Tue, 17 Nov 2009 19:12:10 +0100  
changeset 33743  a58893035742 
parent 33706  7017aee615d6 
child 33747  3aa6b9911252 
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 

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, 

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

22 
user_axioms: bool option, 

23 
debug: bool, 

24 
destroy_constrs: bool, 

25 
specialize: bool, 

26 
skolemize: bool, 

27 
star_linear_preds: bool, 

28 
uncurry: bool, 

29 
fast_descrs: bool, 

30 
tac_timeout: Time.time option, 

31 
evals: term list, 

32 
case_names: (string * int) list, 

33 
def_table: const_table, 

34 
nondef_table: const_table, 

35 
user_nondefs: term list, 

36 
simp_table: const_table Unsynchronized.ref, 

37 
psimp_table: const_table, 

38 
intro_table: const_table, 

39 
ground_thm_table: term list Inttab.table, 

40 
ersatz_table: (string * string) list, 

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

42 
special_funs: special_fun list Unsynchronized.ref, 

43 
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

44 
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

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

47 
val name_sep : string 

48 
val numeral_prefix : string 

49 
val skolem_prefix : string 

50 
val eval_prefix : string 

51 
val original_name : string > string 

52 
val unbox_type : typ > typ 

53 
val string_for_type : Proof.context > typ > string 

54 
val prefix_name : string > string > string 

55 
val short_name : string > string 

56 
val short_const_name : string > string 

57 
val shorten_const_names_in_term : term > term 

58 
val type_match : theory > typ * typ > bool 

59 
val const_match : theory > styp * styp > bool 

60 
val term_match : theory > term * term > bool 

61 
val is_TFree : typ > bool 

62 
val is_higher_order_type : typ > bool 

63 
val is_fun_type : typ > bool 

64 
val is_set_type : typ > bool 

65 
val is_pair_type : typ > bool 

66 
val is_lfp_iterator_type : typ > bool 

67 
val is_gfp_iterator_type : typ > bool 

68 
val is_fp_iterator_type : typ > bool 

69 
val is_boolean_type : typ > bool 

70 
val is_integer_type : typ > bool 

71 
val is_record_type : typ > bool 

72 
val is_number_type : theory > typ > bool 

73 
val const_for_iterator_type : typ > styp 

74 
val nth_range_type : int > typ > typ 

75 
val num_factors_in_type : typ > int 

76 
val num_binder_types : typ > int 

77 
val curried_binder_types : typ > typ list 

78 
val mk_flat_tuple : typ > term list > term 

79 
val dest_n_tuple : int > term > term list 

80 
val instantiate_type : theory > typ > typ > typ > typ 

81 
val is_codatatype : theory > typ > bool 

82 
val is_pure_typedef : theory > typ > bool 

83 
val is_univ_typedef : theory > typ > bool 

84 
val is_datatype : theory > typ > bool 

85 
val is_record_constr : styp > bool 

86 
val is_record_get : theory > styp > bool 

87 
val is_record_update : theory > styp > bool 

88 
val is_abs_fun : theory > styp > bool 

89 
val is_rep_fun : theory > styp > bool 

90 
val is_constr : theory > styp > bool 

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

91 
val is_stale_constr : theory > styp > bool 
33192  92 
val is_sel : string > bool 
93 
val discr_for_constr : styp > styp 

94 
val num_sels_for_constr_type : typ > int 

95 
val nth_sel_name_for_constr_name : string > int > string 

96 
val nth_sel_for_constr : styp > int > styp 

97 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

98 
val sel_no_from_name : string > int 

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

100 
val extensionalize : term > term 

101 
val distinctness_formula : typ > term list > term 

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

103 
val unregister_frac_type : string > theory > theory 

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

105 
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

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

108 
val num_datatype_constrs : extended_context > typ > int 
33192  109 
val constr_name_for_sel_like : string > string 
110 
val boxed_constr_for_sel : extended_context > styp > styp 

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

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

113 
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

114 
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

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

118 
val is_built_in_const : bool > styp > bool 

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

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

121 
val const_nondef_table : term list > const_table 

122 
val const_simp_table : Proof.context > const_table 

123 
val const_psimp_table : Proof.context > const_table 

124 
val inductive_intro_table : Proof.context > const_table > const_table 

125 
val ground_theorem_table : theory > term list Inttab.table 

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

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

128 
val is_inductive_pred : extended_context > styp > bool 

129 
val is_constr_pattern_lhs : theory > term > bool 

130 
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

131 
val merge_type_vars_in_terms : term list > term list 
33192  132 
val ground_types_in_type : extended_context > typ > typ list 
133 
val ground_types_in_terms : extended_context > term list > typ list 

134 
val format_type : int list > int list > typ > typ 

135 
val format_term_type : 

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

137 
val user_friendly_const : 

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

139 
> styp > term * typ 

140 
val assign_operator_for_const : styp > string 

141 
val preprocess_term : 

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

143 
end; 

144 

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

145 
structure Nitpick_HOL : NITPICK_HOL = 
33192  146 
struct 
147 

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

148 
open Nitpick_Util 
33192  149 

150 
type const_table = term list Symtab.table 

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

152 
type unrolled = styp * styp 

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

154 

155 
type extended_context = { 

156 
thy: theory, 

157 
ctxt: Proof.context, 

158 
max_bisim_depth: int, 

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

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

161 
user_axioms: bool option, 

162 
debug: bool, 

163 
destroy_constrs: bool, 

164 
specialize: bool, 

165 
skolemize: bool, 

166 
star_linear_preds: bool, 

167 
uncurry: bool, 

168 
fast_descrs: bool, 

169 
tac_timeout: Time.time option, 

170 
evals: term list, 

171 
case_names: (string * int) list, 

172 
def_table: const_table, 

173 
nondef_table: const_table, 

174 
user_nondefs: term list, 

175 
simp_table: const_table Unsynchronized.ref, 

176 
psimp_table: const_table, 

177 
intro_table: const_table, 

178 
ground_thm_table: term list Inttab.table, 

179 
ersatz_table: (string * string) list, 

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

181 
special_funs: special_fun list Unsynchronized.ref, 

182 
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

183 
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

184 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  185 

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

186 
structure Data = Theory_Data( 
33192  187 
type T = {frac_types: (string * (string * string) list) list, 
188 
codatatypes: (string * (string * styp list)) list} 

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

190 
val extend = I 

33522  191 
fun merge ({frac_types = fs1, codatatypes = cs1}, 
192 
{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

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

194 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  195 

196 
(* term * term > term *) 

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

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

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

200 
else HOLogic.mk_conj (t1, t2) 

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

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

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

204 
else HOLogic.mk_disj (t1, t2) 

205 
(* term > term > term *) 

206 
fun mk_exists v t = 

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

208 

209 
(* term > term > term list *) 

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

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

212 
 strip_connective _ t = [t] 

213 
(* term > term list * term *) 

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

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

216 
(strip_connective t0 t, t0) 

217 
else 

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

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

220 
(* term > term list *) 

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

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

223 

224 
val name_sep = "$" 

225 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

226 
val sel_prefix = nitpick_prefix ^ "sel" 

227 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

228 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

229 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

230 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

231 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

232 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

233 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

234 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

235 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

236 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

237 
val skolem_prefix = nitpick_prefix ^ "sk" 

238 
val special_prefix = nitpick_prefix ^ "sp" 

239 
val uncurry_prefix = nitpick_prefix ^ "unc" 

240 
val eval_prefix = nitpick_prefix ^ "eval" 

241 
val bound_var_prefix = "b" 

242 
val cong_var_prefix = "c" 

243 
val iter_var_prefix = "i" 

244 
val val_var_prefix = nitpick_prefix ^ "v" 

245 
val arg_var_prefix = "x" 

246 

247 
(* int > string *) 

248 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

249 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

250 
(* int > int > string *) 

251 
fun skolem_prefix_for k j = 

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

253 
fun uncurry_prefix_for k j = 

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

255 

256 
(* string > string * string *) 

257 
val strip_first_name_sep = 

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

259 
#> pairself Substring.string 

260 
(* string > string *) 

261 
fun original_name s = 

262 
if String.isPrefix nitpick_prefix s then 

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

264 
else 

265 
s 

266 
val after_name_sep = snd o strip_first_name_sep 

267 

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

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

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

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

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

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

276 
(@{const_name Trueprop}, 1), 

277 
(@{const_name Not}, 1), 

278 
(@{const_name False}, 0), 

279 
(@{const_name True}, 0), 

280 
(@{const_name All}, 1), 

281 
(@{const_name Ex}, 1), 

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

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

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

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

286 
(@{const_name If}, 3), 

287 
(@{const_name Let}, 2), 

288 
(@{const_name Unity}, 0), 

289 
(@{const_name Pair}, 2), 

290 
(@{const_name fst}, 1), 

291 
(@{const_name snd}, 1), 

292 
(@{const_name Id}, 0), 

293 
(@{const_name insert}, 2), 

294 
(@{const_name converse}, 1), 

295 
(@{const_name trancl}, 1), 

296 
(@{const_name rel_comp}, 2), 

297 
(@{const_name image}, 2), 

298 
(@{const_name Suc}, 0), 

299 
(@{const_name finite}, 1), 

300 
(@{const_name nat}, 0), 

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

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

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

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

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

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

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

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

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

310 
(@{const_name nat_gcd}, 0), 

311 
(@{const_name nat_lcm}, 0), 

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

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

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

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

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

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

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

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

322 
(@{const_name Tha}, 1), 

323 
(@{const_name Frac}, 0), 

324 
(@{const_name norm_frac}, 0)] 

325 
val built_in_descr_consts = 

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

327 
(@{const_name Eps}, 1)] 

328 
val built_in_typed_consts = 

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

330 
val built_in_set_consts = 

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

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

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

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

335 

336 
(* typ > typ *) 

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

338 
Type ("fun", map unbox_type Ts) 

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

340 
Type ("*", map unbox_type Ts) 

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

342 
 unbox_type T = T 

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

344 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type 

345 

346 
(* string > string > string *) 

347 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

348 
(* string > string *) 

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

350 
(* string > term > term *) 

351 
val prefix_abs_vars = Term.map_abs_vars o prefix_name 

352 
(* term > term *) 

353 
val shorten_abs_vars = Term.map_abs_vars short_name 

354 
(* string > string *) 

355 
fun short_const_name s = 

356 
case space_explode name_sep s of 

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

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

359 
(* term > term *) 

360 
val shorten_const_names_in_term = 

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

362 

363 
(* theory > typ * typ > bool *) 

364 
fun type_match thy (T1, T2) = 

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

366 
handle Type.TYPE_MATCH => false 

367 
(* theory > styp * styp > bool *) 

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

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

370 
(* theory > term * term > bool *) 

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

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

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

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

375 

376 
(* typ > bool *) 

377 
fun is_TFree (TFree _) = true 

378 
 is_TFree _ = false 

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

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

381 
 is_higher_order_type _ = false 

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

383 
 is_fun_type _ = false 

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

385 
 is_set_type _ = false 

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

387 
 is_pair_type _ = false 

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

389 
 is_lfp_iterator_type _ = false 

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

391 
 is_gfp_iterator_type _ = false 

392 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

393 
val is_boolean_type = equal prop_T orf equal bool_T 

394 
val is_integer_type = 

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

396 
val is_record_type = not o null o Record.dest_recTs 

397 
(* theory > typ > bool *) 

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

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

399 
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) 
33192  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 

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

475 
val {frac_types, codatatypes} = Data.get thy 
33192  476 
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

477 
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end 
33192  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 

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

484 
val {frac_types, codatatypes} = Data.get thy 
33192  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 

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

492 
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end 
33192  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, _)) = 

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

526 
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s 
33192  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 

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

598 
val {codatatypes, ...} = Data.get thy 
33192  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 

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

615 
fun is_stale_constr thy (x as (_, T)) = 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

616 
is_codatatype thy (body_type T) andalso is_constr_like thy x 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

617 
andalso not (is_coconstr thy x) 
33192  618 
fun is_constr thy (x as (_, T)) = 
619 
is_constr_like thy x 

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

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

621 
andalso not (is_stale_constr thy x) 
33192  622 
(* string > bool *) 
623 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

624 
val is_sel_like_and_no_discr = 

625 
String.isPrefix sel_prefix 

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

627 

628 
datatype boxability = 

629 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

630 

631 
(* boxability > boxability *) 

632 
fun in_fun_lhs_for InConstr = InSel 

633 
 in_fun_lhs_for _ = InFunLHS 

634 
fun in_fun_rhs_for InConstr = InConstr 

635 
 in_fun_rhs_for InSel = InSel 

636 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

637 
 in_fun_rhs_for _ = InFunRHS1 

638 

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

640 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

641 
case T of 

642 
Type ("fun", _) => 

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

644 
 Type ("*", Ts) => 

645 
boxy mem [InPair, InFunRHS1, InFunRHS2] 

646 
orelse (boxy mem [InExpr, InFunLHS] 

647 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 

648 
(map (box_type ext_ctxt InPair) Ts)) 

649 
 _ => false 

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

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

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

653 
SOME (SOME box_me) => box_me 

654 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

655 
(* extended_context > boxability > typ > typ *) 

656 
and box_type ext_ctxt boxy T = 

657 
case T of 

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

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

660 
andalso should_box_type ext_ctxt boxy z then 

661 
Type (@{type_name fun_box}, 

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

663 
else 

664 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

665 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

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

667 
if should_box_type ext_ctxt boxy z then 

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

669 
else 

670 
Type ("*", map (box_type ext_ctxt 

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

672 
else InPair)) Ts) 

673 
 _ => T 

674 

675 
(* styp > styp *) 

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

677 

678 
(* typ > int *) 

679 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

680 
(* string > int > string *) 

681 
fun nth_sel_name_for_constr_name s n = 

682 
if s = @{const_name Pair} then 

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

684 
else 

685 
sel_prefix_for n ^ s 

686 
(* styp > int > styp *) 

687 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

688 
 nth_sel_for_constr (s, T) n = 

689 
(nth_sel_name_for_constr_name s n, 

690 
body_type T > nth (maybe_curried_binder_types T) n) 

691 
(* extended_context > styp > int > styp *) 

692 
fun boxed_nth_sel_for_constr ext_ctxt = 

693 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

694 

695 
(* string > int *) 

696 
fun sel_no_from_name s = 

697 
if String.isPrefix discr_prefix s then 

698 
~1 

699 
else if String.isPrefix sel_prefix s then 

700 
s > unprefix sel_prefix > Int.fromString > the 

701 
else if s = @{const_name snd} then 

702 
1 

703 
else 

704 
0 

705 

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

707 
fun eta_expand _ t 0 = t 

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

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

710 
 eta_expand Ts t n = 

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

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

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

714 

715 
(* term > term *) 

716 
fun extensionalize t = 

717 
case t of 

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

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

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

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

722 
end 

723 
 _ => t 

724 

725 
(* typ > term list > term *) 

726 
fun distinctness_formula T = 

727 
all_distinct_unordered_pairs_of 

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

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

730 

731 
(* typ > term *) 

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

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

734 

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

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

737 
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

738 
SOME (_, xs' as (_ :: _)) => 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

739 
map (apsnd (repair_constr_type thy T)) xs' 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

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

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

749 
> T)) constrs 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

757 
in [(s', T')] end 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

760 
[(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

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

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

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

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

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

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

767 
[]) 
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

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

770 
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

771 
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

772 
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

773 
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

774 
 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

775 
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

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

777 
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

778 
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

779 
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

780 
(* extended_context > typ > int *) 
33192  781 
val num_datatype_constrs = length oo datatype_constrs 
782 

783 
(* string > string *) 

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

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

786 
 constr_name_for_sel_like s' = original_name s' 

787 
(* extended_context > styp > styp *) 

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

789 
let val s = constr_name_for_sel_like s' in 

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

791 
> the > pair s 

792 
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

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

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

797 
Abs (Name.uu, dataT, 

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

799 
else if num_datatype_constrs ext_ctxt dataT >= 2 then 
33192  800 
Const (discr_for_constr x) 
801 
else 

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

803 
end 

804 

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

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

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

810 
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

811 
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

812 
 _ => betapply (discr_term_for_constr ext_ctxt x, t) 
33192  813 

814 
(* styp > term > term *) 

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

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

817 
if dataT = nat_T then 

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

819 
else if is_pair_type dataT then 

820 
Const (nth_sel_for_constr x n) 

821 
else 

822 
let 

823 
(* int > typ > int * term *) 

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

825 
let 

826 
val (m, t1) = aux m T1 

827 
val (m, t2) = aux m T2 

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

829 
 aux m T = 

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

831 
$ Bound 0) 

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

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

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

835 
end 

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

837 
fun select_nth_constr_arg thy x t n res_T = 

838 
case strip_comb t of 

839 
(Const x', args) => 

840 
if x = x' then nth args n 

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

842 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

844 

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

846 
fun construct_value _ x [] = Const x 

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

848 
let val args = map Envir.eta_contract args in 

849 
case hd args of 

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

851 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

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

853 
select_nth_constr_arg thy x t n dummyT = t') 

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

855 
t 

856 
else 

857 
list_comb (Const x, args) 

858 
 _ => list_comb (Const x, args) 

859 
end 

860 

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

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

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

865 
 _ => raise SAME ()) 

866 
handle SAME () => 

867 
let 

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

869 
if is_pair_type T then 

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

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

872 
end 

873 
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

874 
datatype_constrs ext_ctxt T > the_single 
33192  875 
val arg_Ts = binder_types T' 
876 
in 

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

878 
(index_seq 0 (length arg_Ts)) arg_Ts) 

879 
end 

880 

881 
(* (typ * int) list > typ > int *) 

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

883 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) 

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

885 
card_of_type asgns T1 * card_of_type asgns T2 

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

887 
 card_of_type _ @{typ prop} = 2 

888 
 card_of_type _ @{typ bool} = 2 

889 
 card_of_type _ @{typ unit} = 1 

890 
 card_of_type asgns T = 

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

892 
SOME k => k 

893 
 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

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

897 
let 

898 
val k1 = bounded_card_of_type max default_card asgns T1 

899 
val k2 = bounded_card_of_type max default_card asgns T2 

900 
in 

901 
if k1 = max orelse k2 = max then max 

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

903 
end 

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

905 
let 

906 
val k1 = bounded_card_of_type max default_card asgns T1 

907 
val k2 = bounded_card_of_type max default_card asgns T2 

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

909 
 bounded_card_of_type max default_card asgns T = 

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

911 
card_of_type asgns T 

912 
else 

913 
card_of_type asgns T 

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

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

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

917 
fun bounded_precise_card_of_type ext_ctxt max default_card asgns T = 
33192  918 
let 
919 
(* typ list > typ > int *) 

920 
fun aux avoid T = 

921 
(if T mem avoid then 

922 
0 

923 
else case T of 

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

925 
let 

926 
val k1 = aux avoid T1 

927 
val k2 = aux avoid T2 

928 
in 

929 
if k1 = 0 orelse k2 = 0 then 0 

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

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

932 
end 

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

934 
let 

935 
val k1 = aux avoid T1 

936 
val k2 = aux avoid T2 

937 
in 

938 
if k1 = 0 orelse k2 = 0 then 0 

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

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

941 
end 

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

943 
 @{typ prop} => 2 

944 
 @{typ bool} => 2 

945 
 @{typ unit} => 1 

946 
 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

947 
(case datatype_constrs ext_ctxt T of 
33192  948 
[] => if is_integer_type T then 0 else raise SAME () 
949 
 constrs => 

950 
let 

951 
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

952 
datatype_constrs ext_ctxt T 
33192  953 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
954 
o snd) 

955 
in 

956 
if exists (equal 0) constr_cards then 0 

957 
else Integer.sum constr_cards 

958 
end) 

959 
 _ => raise SAME ()) 

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

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

962 

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

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

964 
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

965 
not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 [] 
33192  966 

967 
(* term > bool *) 

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

969 
 is_ground_term (Const _) = true 

970 
 is_ground_term _ = false 

971 

972 
(* term > word > word *) 

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

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

975 
 hashw_term _ = 0w0 

976 
(* term > int *) 

977 
val hash_term = Word.toInt o hashw_term 

978 

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

980 
fun special_bounds ts = 

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

982 

983 
(* indexname * typ > term > term *) 

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

985 

33571  986 
(* theory > string > bool *) 
987 
fun is_funky_typedef_name thy s = 

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

989 
@{type_name int}] 

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

991 
(* theory > term > bool *) 

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

993 
 is_funky_typedef _ _ = false 

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

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

997 
 is_arity_type_axiom _ = false 

998 
(* theory > bool > term > bool *) 

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

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

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

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

1003 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1004 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1005 
 is_typedef_axiom _ _ _ = false 
1006 

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

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

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

1010 
using "typedef_info". *) 

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

1012 
fun partition_axioms_by_definitionality thy axioms def_names = 

1013 
let 

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

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

1016 
val nondefs = 

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

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

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

1020 

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

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

1022 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1023 
commands. *) 
1024 
(* theory > bool *) 

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

1026 

1027 
(* term > bool *) 

1028 
val is_plain_definition = 

1029 
let 

1030 
(* term > bool *) 

1031 
fun do_lhs t1 = 

1032 
case strip_comb t1 of 

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

1034 
andalso not (has_duplicates (op =) args) 

1035 
 _ => false 

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

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

1038 
do_lhs t1 

1039 
 do_eq _ = false 

1040 
in do_eq end 

1041 

1042 
(* theory > term list * term list * term list *) 

1043 
fun all_axioms_of thy = 

1044 
let 

1045 
(* theory list > term list *) 

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

1047 
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

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

1049 
> OrdList.make fast_string_ord 
33192  1050 
val thys = thy :: Theory.ancestors_of thy 
1051 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1052 
val built_in_axioms = axioms_of_thys built_in_thys 

1053 
val user_axioms = axioms_of_thys user_thys 

1054 
val (built_in_defs, built_in_nondefs) = 

1055 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1056 
> filter (is_typedef_axiom thy false) 
33192  1057 
val (user_defs, user_nondefs) = 
1058 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

1062 
val defs = (thy > PureThy.all_thms_of 
33192  1063 
> filter (equal Thm.definitionK o Thm.get_kind o snd) 
1064 
> map (prop_of o snd) > filter is_plain_definition) @ 

1065 
user_defs @ built_in_defs 

1066 
in (defs, built_in_nondefs, user_nondefs) end 

1067 

1068 
(* bool > styp > int option *) 

1069 
fun arity_of_built_in_const fast_descrs (s, T) = 

1070 
if s = @{const_name If} then 

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

1072 
else case AList.lookup (op =) 

1073 
(built_in_consts 

1074 
> fast_descrs ? append built_in_descr_consts) s of 

1075 
SOME n => SOME n 

1076 
 NONE => 

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

1078 
SOME n => SOME n 

1079 
 NONE => 

1080 
if is_fun_type T andalso is_set_type (domain_type T) then 

1081 
AList.lookup (op =) built_in_set_consts s 

1082 
else 

1083 
NONE 

1084 
(* bool > styp > bool *) 

1085 
val is_built_in_const = is_some oo arity_of_built_in_const 

1086 

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

1088 
simplification rules (equational specifications). *) 

1089 
(* term > term *) 

1090 
fun term_under_def t = 

1091 
case t of 

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

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

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

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

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

1097 
 t1 $ _ => term_under_def t1 

1098 
 _ => t 

1099 

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

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

1102 
be matched in the face of overloading. *) 

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

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

1105 
if is_built_in_const fast_descrs x then 

1106 
[] 

1107 
else 

1108 
these (Symtab.lookup table s) 

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

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

1111 

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

1112 
(* theory > term > term option *) 
33192  1113 
fun normalized_rhs_of thy t = 
1114 
let 

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

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

1116 
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

1117 
 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

1118 
 aux _ _ = NONE 
33192  1119 
val (lhs, rhs) = 
1120 
case t of 

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

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

1123 
(t1, t2) 

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

1124 
 _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1125 
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

1126 
in fold_rev aux args (SOME rhs) end 
33192  1127 

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

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

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

1131 
NONE 

1132 
else 

1133 
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

1134 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1135 
handle List.Empty => NONE 
1136 

1137 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1138 

1139 
(* term > fixpoint_kind *) 

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

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

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

1143 
 fixpoint_kind_of_rhs _ = NoFp 

1144 

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

1146 
fun is_mutually_inductive_pred_def thy table t = 

1147 
let 

1148 
(* term > bool *) 

1149 
fun is_good_arg (Bound _) = true 

1150 
 is_good_arg (Const (s, _)) = 

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

1152 
 is_good_arg _ = false 

1153 
in 

1154 
case t > strip_abs_body > strip_comb of 

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

1156 
(case def_of_const thy table x of 

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

1158 
 NONE => false) 

1159 
 _ => false 

1160 
end 

1161 
(* theory > const_table > term > term *) 

1162 
fun unfold_mutually_inductive_preds thy table = 

1163 
map_aterms (fn t as Const x => 

1164 
(case def_of_const thy table x of 

1165 
SOME t' => 

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

1167 
if is_mutually_inductive_pred_def thy table t' then t' 

1168 
else t 

1169 
end 

1170 
 NONE => t) 

1171 
 t => t) 

1172 

1173 
(* term > string * term *) 

1174 
fun pair_for_prop t = 

1175 
case term_under_def t of 

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

1177 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1181 
fun table_for get ctxt = 

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

1183 

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

1185 
fun case_const_names thy = 

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

1187 
if is_basic_datatype dtype_s then 

1188 
I 

1189 
else 

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

1191 
> the > #3 > length)) 

1192 
(Datatype.get_all thy) [] @ 

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

1193 
map (apsnd length o snd) (#codatatypes (Data.get thy)) 
33192  1194 

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

1196 
fun const_def_table ctxt ts = 

1197 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

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

1199 
(map pair_for_prop ts) 

1200 
(* term list > const_table *) 

1201 
fun const_nondef_table ts = 

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

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

1204 
(* Proof.context > const_table *) 

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

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

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

1208 
fun inductive_intro_table ctxt def_table = 

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

1210 
def_table o prop_of) 

1211 
o Nitpick_Intros.get) ctxt 

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

1213 
fun ground_theorem_table thy = 

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

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

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

1217 

1218 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1226 

1227 
(* theory > (string * string) list *) 

1228 
fun ersatz_table thy = 

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

1229 
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table 
33192  1230 

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

1232 
fun add_simps simp_table s eqs = 

1233 
Unsynchronized.change simp_table 

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

1235 

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

1237 
the first (preorder) match. *) 

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

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

1239 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1240 
let 
1241 
(* term > (typ * term) list > (typ * term) list *) 

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

1243 
if s = s' then 

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

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

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

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

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

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

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

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

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

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

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

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

1255 
\axiom involving " ^ quote s)) 
33192  1256 
else 
1257 
ys 

1258 
 aux _ ys = ys 

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

1260 

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

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

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

1263 
these (Symtab.lookup table s) > maps (multi_specialize_type thy slack x) 
33192  1264 

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

1266 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

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

1268 
if is_univ_typedef thy abs_T then 

1269 
[] 

1270 
else case typedef_info thy abs_s of 

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

1272 
...} => 

1273 
let 

1274 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

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

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

1277 
val set_t' = 

1278 
prop_of_Rep > HOLogic.dest_Trueprop 

1279 
> Refute.specialize_type thy (dest_Const rep_t) 

1280 
> HOLogic.dest_mem > snd 

1281 
in 

1282 
[HOLogic.all_const abs_T 

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

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

1285 
> map HOLogic.mk_Trueprop 

1286 
end 

1287 
 NONE => [] 

1288 
end 

1289 
(* theory > styp > term *) 

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

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

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

1293 

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

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

1296 
let val arg_Ts = binder_types T in 

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

1298 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1299 
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

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

1301 
fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t = 
33192  1302 
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

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

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

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

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

1308 
val xs = datatype_constrs ext_ctxt dataT 
33192  1309 
val func_Ts = map ((fn T => binder_types T > res_T) o snd) xs 
1310 
val (xs', x) = split_last xs 

1311 
in 

1312 
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

1313 
> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs') 
33192  1314 
> fold_rev (curry absdummy) (func_Ts @ [dataT]) 
1315 
end 

1316 

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

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

1318 
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

1319 
let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in 
33192  1320 
case no_of_record_field thy s rec_T of 
1321 
~1 => (case rec_T of 

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

1323 
let 

1324 
val rec_T' = List.last Ts 

1325 
val j = num_record_fields thy rec_T  1 

1326 
in 

1327 
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

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

1330 
 _ => 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

1331 
[])) 
33192  1332 
 j => select_nth_constr_arg thy constr_x t j res_T 
1333 
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

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

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

1337 
val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T) 
33192  1338 
val Ts = binder_types constr_T 
1339 
val n = length Ts 

1340 
val special_j = no_of_record_field thy s rec_T 

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

1342 
let 

1343 
val t = select_nth_constr_arg thy constr_x rec_t j T 

1344 
in 

1345 
if j = special_j then 

1346 
betapply (fun_t, t) 

1347 
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

1348 
optimized_record_update ext_ctxt s 
33192  1349 
(rec_T > dest_Type > snd > List.last) fun_t t 
1350 
else 

1351 
t 

1352 
end) (index_seq 0 n) Ts 

1353 
in list_comb (Const constr_x, ts) end 

1354 

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

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

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

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

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

1360 
fun has_trivial_definition thy table x = 

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

1362 

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

1364 
fun fixpoint_kind_of_const thy table x = 

