author  blanchet 
Thu, 05 Nov 2009 19:06:35 +0100  
changeset 33581  e1e77265fb1d 
parent 33580  45c33e97cb86 
child 33583  b5e0909cd5ea 
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 

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

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

93 
val num_sels_for_constr_type : typ > int 

94 
val nth_sel_name_for_constr_name : string > int > string 

95 
val nth_sel_for_constr : styp > int > styp 

96 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

97 
val sel_no_from_name : string > int 

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

99 
val extensionalize : term > term 

100 
val distinctness_formula : typ > term list > term 

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

102 
val unregister_frac_type : string > theory > theory 

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

104 
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

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

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

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

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

112 
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

113 
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

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

117 
val is_built_in_const : bool > styp > bool 

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

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

120 
val const_nondef_table : term list > const_table 

121 
val const_simp_table : Proof.context > const_table 

122 
val const_psimp_table : Proof.context > const_table 

123 
val inductive_intro_table : Proof.context > const_table > const_table 

124 
val ground_theorem_table : theory > term list Inttab.table 

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

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

127 
val is_inductive_pred : extended_context > styp > bool 

128 
val is_constr_pattern_lhs : theory > term > bool 

129 
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

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

133 
val format_type : int list > int list > typ > typ 

134 
val format_term_type : 

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

136 
val user_friendly_const : 

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

138 
> styp > term * typ 

139 
val assign_operator_for_const : styp > string 

140 
val preprocess_term : 

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

142 
end; 

143 

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

144 
structure Nitpick_HOL : NITPICK_HOL = 
33192  145 
struct 
146 

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

147 
open Nitpick_Util 
33192  148 

149 
type const_table = term list Symtab.table 

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

151 
type unrolled = styp * styp 

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

153 

154 
type extended_context = { 

155 
thy: theory, 

156 
ctxt: Proof.context, 

157 
max_bisim_depth: int, 

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

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

160 
user_axioms: bool option, 

161 
debug: bool, 

162 
destroy_constrs: bool, 

163 
specialize: bool, 

164 
skolemize: bool, 

165 
star_linear_preds: bool, 

166 
uncurry: bool, 

167 
fast_descrs: bool, 

168 
tac_timeout: Time.time option, 

169 
evals: term list, 

170 
case_names: (string * int) list, 

171 
def_table: const_table, 

172 
nondef_table: const_table, 

173 
user_nondefs: term list, 

174 
simp_table: const_table Unsynchronized.ref, 

175 
psimp_table: const_table, 

176 
intro_table: const_table, 

177 
ground_thm_table: term list Inttab.table, 

178 
ersatz_table: (string * string) list, 

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

180 
special_funs: special_fun list Unsynchronized.ref, 

181 
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

182 
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

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

185 
structure TheoryData = TheoryDataFun( 

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

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

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

189 
val copy = I 

190 
val extend = I 

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

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

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

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

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, [])) = 

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

400 
s))) 

401 
 is_frac_type _ _ = false 

402 
fun is_number_type thy = is_integer_type orf is_frac_type thy 

403 

404 
(* bool > styp > typ *) 

405 
fun iterator_type_for_const gfp (s, T) = 

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

407 
binder_types T) 

408 
(* typ > styp *) 

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

410 
 const_for_iterator_type T = 

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

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

413 
(* int > typ > typ * typ *) 

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

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

416 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

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

422 

423 
(* typ > int *) 

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

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

426 
 num_factors_in_type _ = 1 

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

428 
 num_binder_types _ = 0 

429 
(* typ > typ list *) 

430 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

431 
fun maybe_curried_binder_types T = 

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

433 

434 
(* typ > term list > term *) 

435 
fun mk_flat_tuple _ [t] = t 

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

437 
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

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

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

442 

443 
(* int > typ > typ list *) 

444 
fun dest_n_tuple_type 1 T = [T] 

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

446 
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

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

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

450 
(* (typ * typ) list > typ > typ *) 

451 
fun typ_subst [] T = T 

452 
 typ_subst ps T = 

453 
let 

454 
(* typ > typ *) 

455 
fun subst T = 

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

457 
SOME T' => T' 

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

459 
in subst T end 

460 

461 
(* theory > typ > typ > typ > typ *) 

462 
fun instantiate_type thy T1 T1' T2 = 

463 
Same.commit (Envir.subst_type_same 

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

465 
(Logic.varifyT T2) 

466 
handle Type.TYPE_MATCH => 

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

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

469 
(* theory > typ > typ > styp *) 

470 
fun repair_constr_type thy body_T' T = 

471 
instantiate_type thy (body_type T) body_T' T 

472 

473 
(* string > (string * string) list > theory > theory *) 

474 
fun register_frac_type frac_s ersaetze thy = 

475 
let 

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

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

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

479 
(* string > theory > theory *) 

480 
fun unregister_frac_type frac_s = register_frac_type frac_s [] 

481 

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

483 
fun register_codatatype co_T case_name constr_xs thy = 

484 
let 

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

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

487 
val (co_s, co_Ts) = dest_Type co_T 

488 
val _ = 

489 
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

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

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

494 
(* typ > theory > theory *) 

495 
fun unregister_codatatype co_T = register_codatatype co_T "" [] 

496 

497 
type typedef_info = 

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

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

500 
Rep_inverse: thm option} 

501 

502 
(* theory > string > typedef_info *) 

503 
fun typedef_info thy s = 

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

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

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

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

508 
> Logic.varify, 

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

510 
else case Typedef.get_info thy s of 

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

512 
...} => 

513 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 

514 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 

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

516 
 NONE => NONE 

517 

518 
(* string > bool *) 

519 
fun is_basic_datatype s = 

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

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

522 
(* theory > string > bool *) 

523 
val is_typedef = is_some oo typedef_info 

524 
val is_real_datatype = is_some oo Datatype.get_info 

525 
(* theory > typ > bool *) 

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

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

528 
> Option.map snd > these)) 

529 
 is_codatatype _ _ = false 

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

531 
is_typedef thy s andalso 

532 
not (is_real_datatype thy s orelse is_codatatype thy T 

533 
orelse is_record_type T orelse is_integer_type T) 

534 
 is_pure_typedef _ _ = false 

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

536 
(case typedef_info thy s of 

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

538 
(case set_def of 

539 
SOME thm => 

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

541 
 NONE => 

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

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

544 
 NONE => false) 

545 
 is_univ_typedef _ _ = false 

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

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

548 
andalso not (is_basic_datatype s) 

549 
 is_datatype _ _ = false 

550 

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

552 
fun all_record_fields thy T = 

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

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

555 
end 

556 
handle TYPE _ => [] 

557 
(* styp > bool *) 

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

559 
String.isSuffix Record.extN s andalso 

560 
let val dataT = body_type T in 

561 
is_record_type dataT andalso 

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

563 
end 

564 
(* theory > typ > int *) 

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

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

567 
fun no_of_record_field thy s T1 = 

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

569 
(* theory > styp > bool *) 

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

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

572 
 is_record_get _ _ = false 

573 
fun is_record_update thy (s, T) = 

574 
String.isSuffix Record.updateN s andalso 

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

576 
(all_record_fields thy (body_type T)) 

577 
handle TYPE _ => false 

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

579 
(case typedef_info thy s' of 

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

581 
 NONE => false) 

582 
 is_abs_fun _ _ = false 

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

584 
(case typedef_info thy s' of 

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

586 
 NONE => false) 

587 
 is_rep_fun _ _ = false 

588 

589 
(* theory > styp > styp *) 

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

591 
(case typedef_info thy s' of 

592 
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

593 
 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

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

596 
(* theory > styp > bool *) 

597 
fun is_coconstr thy (s, T) = 

598 
let 

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

600 
val co_T = body_type T 

601 
val co_s = dest_Type co_T > fst 

602 
in 

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

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

605 
end 

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

607 
fun is_constr_like thy (s, T) = 

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

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

610 
Refute.is_IDT_constructor thy x orelse is_record_constr x 

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

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

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

614 
orelse is_coconstr thy x 

615 
end 

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

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

617 
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

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

621 
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

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

625 
val is_sel_like_and_no_discr = 

626 
String.isPrefix sel_prefix 

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

628 

629 
datatype boxability = 

630 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

631 

632 
(* boxability > boxability *) 

633 
fun in_fun_lhs_for InConstr = InSel 

634 
 in_fun_lhs_for _ = InFunLHS 

635 
fun in_fun_rhs_for InConstr = InConstr 

636 
 in_fun_rhs_for InSel = InSel 

637 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

638 
 in_fun_rhs_for _ = InFunRHS1 

639 

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

641 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

642 
case T of 

643 
Type ("fun", _) => 

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

645 
 Type ("*", Ts) => 

646 
boxy mem [InPair, InFunRHS1, InFunRHS2] 

647 
orelse (boxy mem [InExpr, InFunLHS] 

648 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 

649 
(map (box_type ext_ctxt InPair) Ts)) 

650 
 _ => false 

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

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

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

654 
SOME (SOME box_me) => box_me 

655 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

656 
(* extended_context > boxability > typ > typ *) 

657 
and box_type ext_ctxt boxy T = 

658 
case T of 

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

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

661 
andalso should_box_type ext_ctxt boxy z then 

662 
Type (@{type_name fun_box}, 

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

664 
else 

665 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

666 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

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

668 
if should_box_type ext_ctxt boxy z then 

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

670 
else 

671 
Type ("*", map (box_type ext_ctxt 

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

673 
else InPair)) Ts) 

674 
 _ => T 

675 

676 
(* styp > styp *) 

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

678 

679 
(* typ > int *) 

680 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

681 
(* string > int > string *) 

682 
fun nth_sel_name_for_constr_name s n = 

683 
if s = @{const_name Pair} then 

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

685 
else 

686 
sel_prefix_for n ^ s 

687 
(* styp > int > styp *) 

688 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

689 
 nth_sel_for_constr (s, T) n = 

690 
(nth_sel_name_for_constr_name s n, 

691 
body_type T > nth (maybe_curried_binder_types T) n) 

692 
(* extended_context > styp > int > styp *) 

693 
fun boxed_nth_sel_for_constr ext_ctxt = 

694 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

695 

696 
(* string > int *) 

697 
fun sel_no_from_name s = 

698 
if String.isPrefix discr_prefix s then 

699 
~1 

700 
else if String.isPrefix sel_prefix s then 

701 
s > unprefix sel_prefix > Int.fromString > the 

702 
else if s = @{const_name snd} then 

703 
1 

704 
else 

705 
0 

706 

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

708 
fun eta_expand _ t 0 = t 

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

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

711 
 eta_expand Ts t n = 

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

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

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

715 

716 
(* term > term *) 

717 
fun extensionalize t = 

718 
case t of 

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

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

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

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

723 
end 

724 
 _ => t 

725 

726 
(* typ > term list > term *) 

727 
fun distinctness_formula T = 

728 
all_distinct_unordered_pairs_of 

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

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

731 

732 
(* typ > term *) 

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

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

735 

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

737 
fun uncached_datatype_constrs thy (T as Type (s, Ts)) = 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

771 
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

772 
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

773 
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

774 
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

775 
 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

776 
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

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

778 
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

779 
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

780 
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

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

784 
(* string > string *) 

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

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

787 
 constr_name_for_sel_like s' = original_name s' 

788 
(* extended_context > styp > styp *) 

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

790 
let val s = constr_name_for_sel_like s' in 

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

792 
> the > pair s 

793 
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

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

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

798 
Abs (Name.uu, dataT, 

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

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

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

804 
end 

805 

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

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

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

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

811 
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

812 
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

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

815 
(* styp > term > term *) 

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

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

818 
if dataT = nat_T then 

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

820 
else if is_pair_type dataT then 

821 
Const (nth_sel_for_constr x n) 

822 
else 

823 
let 

824 
(* int > typ > int * term *) 

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

826 
let 

827 
val (m, t1) = aux m T1 

828 
val (m, t2) = aux m T2 

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

830 
 aux m T = 

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

832 
$ Bound 0) 

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

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

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

836 
end 

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

838 
fun select_nth_constr_arg thy x t n res_T = 

839 
case strip_comb t of 

840 
(Const x', args) => 

841 
if x = x' then nth args n 

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

843 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

845 

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

847 
fun construct_value _ x [] = Const x 

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

849 
let val args = map Envir.eta_contract args in 

850 
case hd args of 

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

852 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

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

854 
select_nth_constr_arg thy x t n dummyT = t') 

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

856 
t 

857 
else 

858 
list_comb (Const x, args) 

859 
 _ => list_comb (Const x, args) 

860 
end 

861 

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

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

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

866 
 _ => raise SAME ()) 

867 
handle SAME () => 

868 
let 

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

870 
if is_pair_type T then 

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

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

873 
end 

874 
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

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

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

879 
(index_seq 0 (length arg_Ts)) arg_Ts) 

880 
end 

881 

882 
(* (typ * int) list > typ > int *) 

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

884 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) 

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

886 
card_of_type asgns T1 * card_of_type asgns T2 

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

888 
 card_of_type _ @{typ prop} = 2 

889 
 card_of_type _ @{typ bool} = 2 

890 
 card_of_type _ @{typ unit} = 1 

891 
 card_of_type asgns T = 

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

893 
SOME k => k 

894 
 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

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

898 
let 

899 
val k1 = bounded_card_of_type max default_card asgns T1 

900 
val k2 = bounded_card_of_type max default_card asgns T2 

901 
in 

902 
if k1 = max orelse k2 = max then max 

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

904 
end 

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

906 
let 

907 
val k1 = bounded_card_of_type max default_card asgns T1 

908 
val k2 = bounded_card_of_type max default_card asgns T2 

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

910 
 bounded_card_of_type max default_card asgns T = 

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

912 
card_of_type asgns T 

913 
else 

914 
card_of_type asgns T 

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

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

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

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

921 
fun aux avoid T = 

922 
(if T mem avoid then 

923 
0 

924 
else case T of 

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

926 
let 

927 
val k1 = aux avoid T1 

928 
val k2 = aux avoid T2 

929 
in 

930 
if k1 = 0 orelse k2 = 0 then 0 

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

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

933 
end 

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

935 
let 

936 
val k1 = aux avoid T1 

937 
val k2 = aux avoid T2 

938 
in 

939 
if k1 = 0 orelse k2 = 0 then 0 

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

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

942 
end 

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

944 
 @{typ prop} => 2 

945 
 @{typ bool} => 2 

946 
 @{typ unit} => 1 

947 
 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

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

951 
let 

952 
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

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

956 
in 

957 
if exists (equal 0) constr_cards then 0 

958 
else Integer.sum constr_cards 

959 
end) 

960 
 _ => raise SAME ()) 

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

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

963 

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

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

965 
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

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

968 
(* term > bool *) 

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

970 
 is_ground_term (Const _) = true 

971 
 is_ground_term _ = false 

972 

973 
(* term > word > word *) 

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

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

976 
 hashw_term _ = 0w0 

977 
(* term > int *) 

978 
val hash_term = Word.toInt o hashw_term 

979 

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

981 
fun special_bounds ts = 

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

983 

984 
(* indexname * typ > term > term *) 

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

986 

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

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

990 
@{type_name int}] 

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

992 
(* theory > term > bool *) 

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

994 
 is_funky_typedef _ _ = false 

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

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

998 
 is_arity_type_axiom _ = false 

999 
(* theory > bool > term > bool *) 

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

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

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

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

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

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

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

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

1011 
using "typedef_info". *) 

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

1013 
fun partition_axioms_by_definitionality thy axioms def_names = 

1014 
let 

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

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

1017 
val nondefs = 

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

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

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

1021 

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

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

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

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

1027 

1028 
(* term > bool *) 

1029 
val is_plain_definition = 

1030 
let 

1031 
(* term > bool *) 

1032 
fun do_lhs t1 = 

1033 
case strip_comb t1 of 

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

1035 
andalso not (has_duplicates (op =) args) 

1036 
 _ => false 

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

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

1039 
do_lhs t1 

1040 
 do_eq _ = false 

1041 
in do_eq end 

1042 

1043 
(* theory > term list * term list * term list *) 

1044 
fun all_axioms_of thy = 

1045 
let 

1046 
(* theory list > term list *) 

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

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

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

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

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

1053 
val built_in_axioms = axioms_of_thys built_in_thys 

1054 
val user_axioms = axioms_of_thys user_thys 

1055 
val (built_in_defs, built_in_nondefs) = 

1056 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

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

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

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

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

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

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

1066 
user_defs @ built_in_defs 

1067 
in (defs, built_in_nondefs, user_nondefs) end 

1068 

1069 
(* bool > styp > int option *) 

1070 
fun arity_of_built_in_const fast_descrs (s, T) = 

1071 
if s = @{const_name If} then 

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

1073 
else case AList.lookup (op =) 

1074 
(built_in_consts 

1075 
> fast_descrs ? append built_in_descr_consts) s of 

1076 
SOME n => SOME n 

1077 
 NONE => 

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

1079 
SOME n => SOME n 

1080 
 NONE => 

1081 
if is_fun_type T andalso is_set_type (domain_type T) then 

1082 
AList.lookup (op =) built_in_set_consts s 

1083 
else 

1084 
NONE 

1085 
(* bool > styp > bool *) 

1086 
val is_built_in_const = is_some oo arity_of_built_in_const 

1087 

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

1089 
simplification rules (equational specifications). *) 

1090 
(* term > term *) 

1091 
fun term_under_def t = 

1092 
case t of 

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

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

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

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

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

1098 
 t1 $ _ => term_under_def t1 

1099 
 _ => t 

1100 

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

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

1103 
be matched in the face of overloading. *) 

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

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

1106 
if is_built_in_const fast_descrs x then 

1107 
[] 

1108 
else 

1109 
these (Symtab.lookup table s) 

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

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

1112 

1113 
(* term > term *) 

1114 
fun normalized_rhs_of thy t = 

1115 
let 

1116 
(* term > term *) 

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

1118 
 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

1119 
 aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1120 
val (lhs, rhs) = 
1121 
case t of 

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

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

1124 
(t1, t2) 

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

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

1128 

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

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

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

1132 
NONE 

1133 
else 

1134 
x > def_props_for_const thy false table > List.last 

1135 
> normalized_rhs_of thy > prefix_abs_vars s > SOME 

1136 
handle List.Empty => NONE 

1137 

1138 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1139 

1140 
(* term > fixpoint_kind *) 

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

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

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

1144 
 fixpoint_kind_of_rhs _ = NoFp 

1145 

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

1147 
fun is_mutually_inductive_pred_def thy table t = 

1148 
let 

1149 
(* term > bool *) 

1150 
fun is_good_arg (Bound _) = true 

1151 
 is_good_arg (Const (s, _)) = 

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

1153 
 is_good_arg _ = false 

1154 
in 

1155 
case t > strip_abs_body > strip_comb of 

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

1157 
(case def_of_const thy table x of 

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

1159 
 NONE => false) 

1160 
 _ => false 

1161 
end 

1162 
(* theory > const_table > term > term *) 

1163 
fun unfold_mutually_inductive_preds thy table = 

1164 
map_aterms (fn t as Const x => 

1165 
(case def_of_const thy table x of 

1166 
SOME t' => 

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

1168 
if is_mutually_inductive_pred_def thy table t' then t' 

1169 
else t 

1170 
end 

1171 
 NONE => t) 

1172 
 t => t) 

1173 

1174 
(* term > string * term *) 

1175 
fun pair_for_prop t = 

1176 
case term_under_def t of 

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

1178 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1182 
fun table_for get ctxt = 

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

1184 

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

1186 
fun case_const_names thy = 

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

1188 
if is_basic_datatype dtype_s then 

1189 
I 

1190 
else 

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

1192 
> the > #3 > length)) 

1193 
(Datatype.get_all thy) [] @ 

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

1195 

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

1197 
fun const_def_table ctxt ts = 

1198 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

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

1200 
(map pair_for_prop ts) 

1201 
(* term list > const_table *) 

1202 
fun const_nondef_table ts = 

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

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

1205 
(* Proof.context > const_table *) 

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

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

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

1209 
fun inductive_intro_table ctxt def_table = 

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

1211 
def_table o prop_of) 

1212 
o Nitpick_Intros.get) ctxt 

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

1214 
fun ground_theorem_table thy = 

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

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

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

1218 

1219 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1227 

1228 
(* theory > (string * string) list *) 

1229 
fun ersatz_table thy = 

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

1231 

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

1233 
fun add_simps simp_table s eqs = 

1234 
Unsynchronized.change simp_table 

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

1236 

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

1238 
the first (preorder) match. *) 

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

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

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

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

1244 
if s = s' then 

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

1245 
ys > (if AList.defined (op =) ys T' 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 
cons (T', Refute.monomorphic_term 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

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

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

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

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

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

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

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

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

1259 
 aux _ ys = ys 

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

1261 

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

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

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

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

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

1267 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

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

1269 
if is_univ_typedef thy abs_T then 

1270 
[] 

1271 
else case typedef_info thy abs_s of 

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

1273 
...} => 

1274 
let 

1275 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

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

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

1278 
val set_t' = 

1279 
prop_of_Rep > HOLogic.dest_Trueprop 

1280 
> Refute.specialize_type thy (dest_Const rep_t) 

1281 
> HOLogic.dest_mem > snd 

1282 
in 

1283 
[HOLogic.all_const abs_T 

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

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

1286 
> map HOLogic.mk_Trueprop 

1287 
end 

1288 
 NONE => [] 

1289 
end 

1290 
(* theory > styp > term *) 

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

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

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

1294 

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

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

1297 
let val arg_Ts = binder_types T in 

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

1299 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1300 
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

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

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

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

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

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

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

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

1312 
in 

1313 
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

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

1317 

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

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

1319 
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

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

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

1324 
let 

1325 
val rec_T' = List.last Ts 

1326 
val j = num_record_fields thy rec_T  1 

1327 
in 

1328 
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

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

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

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

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

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

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

1341 
val special_j = no_of_record_field thy s rec_T 

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

1343 
let 

1344 
val t = select_nth_constr_arg thy constr_x rec_t j T 

1345 
in 

1346 
if j = special_j then 

1347 
betapply (fun_t, t) 

1348 
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

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

1352 
t 

1353 
end) (index_seq 0 n) Ts 

1354 
in list_comb (Const constr_x, ts) end 

1355 

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

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

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

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

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

1361 
fun has_trivial_definition thy table x = 

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

1363 

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

1365 
fun fixpoint_kind_of_const thy table x = 

1366 
if is_built_in_const false x then 

1367 
NoFp 

1368 
else 

1369 
fixpoint_kind_of_rhs (the (def_of_const thy table x)) 

1370 
handle Option.Option => NoFp 

1371 

1372 
(* extended_context > styp > bool *) 

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

1374 
: extended_context) x = 
