author  blanchet 
Thu, 17 Dec 2009 15:22:11 +0100  
changeset 34124  c4628a1dcf75 
parent 34123  c4988215a691 
child 34126  8a2c5d7aff51 
permissions  rwrr 
33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

1 
(* Title: HOL/Tools/Nitpick/nitpick_hol.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
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, 

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

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

27 
skolemize: bool, 

28 
star_linear_preds: bool, 

29 
uncurry: bool, 

30 
fast_descrs: bool, 

31 
tac_timeout: Time.time option, 

32 
evals: term list, 

33 
case_names: (string * int) list, 

34 
def_table: const_table, 

35 
nondef_table: const_table, 

36 
user_nondefs: term list, 

37 
simp_table: const_table Unsynchronized.ref, 

38 
psimp_table: const_table, 

39 
intro_table: const_table, 

40 
ground_thm_table: term list Inttab.table, 

41 
ersatz_table: (string * string) list, 

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

43 
special_funs: special_fun list Unsynchronized.ref, 

44 
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

45 
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

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

48 
val name_sep : string 

49 
val numeral_prefix : string 

50 
val skolem_prefix : string 

51 
val eval_prefix : string 

52 
val original_name : string > string 

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

53 
val unbit_and_unbox_type : typ > typ 
33192  54 
val string_for_type : Proof.context > typ > string 
55 
val prefix_name : string > string > string 

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

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

58 
val shorten_names_in_term : term > term 
33192  59 
val type_match : theory > typ * typ > bool 
60 
val const_match : theory > styp * styp > bool 

61 
val term_match : theory > term * term > bool 

62 
val is_TFree : typ > bool 

63 
val is_higher_order_type : typ > bool 

64 
val is_fun_type : typ > bool 

65 
val is_set_type : typ > bool 

66 
val is_pair_type : typ > bool 

67 
val is_lfp_iterator_type : typ > bool 

68 
val is_gfp_iterator_type : typ > bool 

69 
val is_fp_iterator_type : typ > bool 

70 
val is_boolean_type : typ > bool 

71 
val is_integer_type : typ > bool 

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

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

73 
val is_word_type : typ > bool 
33192  74 
val is_record_type : typ > bool 
75 
val is_number_type : theory > typ > bool 

76 
val const_for_iterator_type : typ > styp 

77 
val nth_range_type : int > typ > typ 

78 
val num_factors_in_type : typ > int 

79 
val num_binder_types : typ > int 

80 
val curried_binder_types : typ > typ list 

81 
val mk_flat_tuple : typ > term list > term 

82 
val dest_n_tuple : int > term > term list 

83 
val instantiate_type : theory > typ > typ > typ > typ 

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

84 
val is_real_datatype : theory > string > bool 
33192  85 
val is_codatatype : theory > typ > bool 
86 
val is_pure_typedef : theory > typ > bool 

87 
val is_univ_typedef : theory > typ > bool 

88 
val is_datatype : theory > typ > bool 

89 
val is_record_constr : styp > bool 

90 
val is_record_get : theory > styp > bool 

91 
val is_record_update : theory > styp > bool 

92 
val is_abs_fun : theory > styp > bool 

93 
val is_rep_fun : theory > styp > bool 

94 
val is_constr : theory > styp > bool 

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

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

97 
val is_sel_like_and_no_discr : string > bool 
33192  98 
val discr_for_constr : styp > styp 
99 
val num_sels_for_constr_type : typ > int 

100 
val nth_sel_name_for_constr_name : string > int > string 

101 
val nth_sel_for_constr : styp > int > styp 

102 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

103 
val sel_no_from_name : string > int 

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

105 
val extensionalize : term > term 

106 
val distinctness_formula : typ > term list > term 

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

108 
val unregister_frac_type : string > theory > theory 

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

110 
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

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

113 
val num_datatype_constrs : extended_context > typ > int 
33192  114 
val constr_name_for_sel_like : string > string 
115 
val boxed_constr_for_sel : extended_context > styp > styp 

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

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

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

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

119 
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

120 
val is_finite_type : extended_context > typ > bool 
33192  121 
val all_axioms_of : theory > term list * term list * term list 
122 
val arity_of_built_in_const : bool > styp > int option 

123 
val is_built_in_const : bool > styp > bool 

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

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

126 
val const_nondef_table : term list > const_table 

127 
val const_simp_table : Proof.context > const_table 

128 
val const_psimp_table : Proof.context > const_table 

129 
val inductive_intro_table : Proof.context > const_table > const_table 

130 
val ground_theorem_table : theory > term list Inttab.table 

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

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

133 
val is_inductive_pred : extended_context > styp > bool 

134 
val is_constr_pattern_lhs : theory > term > bool 

135 
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

136 
val merge_type_vars_in_terms : term list > term list 
33192  137 
val ground_types_in_type : extended_context > typ > typ list 
138 
val ground_types_in_terms : extended_context > term list > typ list 

139 
val format_type : int list > int list > typ > typ 

140 
val format_term_type : 

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

142 
val user_friendly_const : 

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

144 
> styp > term * typ 

145 
val assign_operator_for_const : styp > string 

146 
val preprocess_term : 

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

148 
end; 

149 

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

150 
structure Nitpick_HOL : NITPICK_HOL = 
33192  151 
struct 
152 

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

153 
open Nitpick_Util 
33192  154 

155 
type const_table = term list Symtab.table 

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

157 
type unrolled = styp * styp 

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

159 

160 
type extended_context = { 

161 
thy: theory, 

162 
ctxt: Proof.context, 

163 
max_bisim_depth: int, 

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

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

166 
user_axioms: bool option, 

167 
debug: bool, 

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

168 
binary_ints: bool option, 
33192  169 
destroy_constrs: bool, 
170 
specialize: bool, 

171 
skolemize: bool, 

172 
star_linear_preds: bool, 

173 
uncurry: bool, 

174 
fast_descrs: bool, 

175 
tac_timeout: Time.time option, 

176 
evals: term list, 

177 
case_names: (string * int) list, 

178 
def_table: const_table, 

179 
nondef_table: const_table, 

180 
user_nondefs: term list, 

181 
simp_table: const_table Unsynchronized.ref, 

182 
psimp_table: const_table, 

183 
intro_table: const_table, 

184 
ground_thm_table: term list Inttab.table, 

185 
ersatz_table: (string * string) list, 

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

187 
special_funs: special_fun list Unsynchronized.ref, 

188 
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

189 
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

190 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  191 

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

192 
structure Data = Theory_Data( 
33192  193 
type T = {frac_types: (string * (string * string) list) list, 
194 
codatatypes: (string * (string * styp list)) list} 

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

196 
val extend = I 

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

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

200 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  201 

202 
(* term * term > term *) 

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

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

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

205 
 s_conj (t1, t2) = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

206 
if t1 = @{const False} orelse t2 = @{const False} then @{const False} 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

207 
else HOLogic.mk_conj (t1, t2) 
33192  208 
fun s_disj (t1, @{const False}) = t1 
209 
 s_disj (@{const False}, t2) = t2 

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

210 
 s_disj (t1, t2) = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

211 
if t1 = @{const True} orelse t2 = @{const True} then @{const True} 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

212 
else HOLogic.mk_disj (t1, t2) 
33192  213 
(* term > term > term *) 
214 
fun mk_exists v t = 

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

216 

217 
(* term > term > term list *) 

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

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

220 
 strip_connective _ t = [t] 

221 
(* term > term list * term *) 

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

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

223 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 
33192  224 
(strip_connective t0 t, t0) 
225 
else 

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

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

228 
(* term > term list *) 

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

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

231 

232 
val name_sep = "$" 

233 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

234 
val sel_prefix = nitpick_prefix ^ "sel" 

235 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

236 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

237 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

238 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

239 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

240 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

241 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

242 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

243 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

244 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

245 
val skolem_prefix = nitpick_prefix ^ "sk" 

246 
val special_prefix = nitpick_prefix ^ "sp" 

247 
val uncurry_prefix = nitpick_prefix ^ "unc" 

248 
val eval_prefix = nitpick_prefix ^ "eval" 

249 
val bound_var_prefix = "b" 

250 
val cong_var_prefix = "c" 

251 
val iter_var_prefix = "i" 

252 
val val_var_prefix = nitpick_prefix ^ "v" 

253 
val arg_var_prefix = "x" 

254 

255 
(* int > string *) 

256 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

257 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

258 
(* int > int > string *) 

259 
fun skolem_prefix_for k j = 

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

261 
fun uncurry_prefix_for k j = 

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

263 

264 
(* string > string * string *) 

265 
val strip_first_name_sep = 

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

267 
#> pairself Substring.string 

268 
(* string > string *) 

269 
fun original_name s = 

270 
if String.isPrefix nitpick_prefix s then 

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

272 
else 

273 
s 

274 
val after_name_sep = snd o strip_first_name_sep 

275 

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

277 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  278 
well. *) 
279 
val built_in_consts = 

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

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

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

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

284 
(@{const_name Trueprop}, 1), 

285 
(@{const_name Not}, 1), 

286 
(@{const_name False}, 0), 

287 
(@{const_name True}, 0), 

288 
(@{const_name All}, 1), 

289 
(@{const_name Ex}, 1), 

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

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

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

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

294 
(@{const_name If}, 3), 

295 
(@{const_name Let}, 2), 

296 
(@{const_name Unity}, 0), 

297 
(@{const_name Pair}, 2), 

298 
(@{const_name fst}, 1), 

299 
(@{const_name snd}, 1), 

300 
(@{const_name Id}, 0), 

301 
(@{const_name insert}, 2), 

302 
(@{const_name converse}, 1), 

303 
(@{const_name trancl}, 1), 

304 
(@{const_name rel_comp}, 2), 

305 
(@{const_name image}, 2), 

306 
(@{const_name Suc}, 0), 

307 
(@{const_name finite}, 1), 

308 
(@{const_name nat}, 0), 

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

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

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

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

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

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

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

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

317 
(@{const_name nat_gcd}, 0), 

318 
(@{const_name nat_lcm}, 0), 

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

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

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

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

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

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

33571  325 
(@{const_name uminus_int_inst.uminus_int}, 0), 
33192  326 
(@{const_name ord_int_inst.less_int}, 2), 
327 
(@{const_name ord_int_inst.less_eq_int}, 2), 

328 
(@{const_name Tha}, 1), 

329 
(@{const_name Frac}, 0), 

330 
(@{const_name norm_frac}, 0)] 

331 
val built_in_descr_consts = 

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

333 
(@{const_name Eps}, 1)] 

334 
val built_in_typed_consts = 

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

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

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

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

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

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

342 

343 
(* typ > typ *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

360 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type 
33192  361 

362 
(* string > string > string *) 

363 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

364 
(* string > string *) 

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

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

368 
(* term > term *) 

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

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

371 
fun short_name s = 
33192  372 
case space_explode name_sep s of 
373 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix 

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

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

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

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

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

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

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

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

382 
#> map_types shorten_names_in_type 
33192  383 

384 
(* theory > typ * typ > bool *) 

385 
fun type_match thy (T1, T2) = 

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

387 
handle Type.TYPE_MATCH => false 

388 
(* theory > styp * styp > bool *) 

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

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

391 
(* theory > term * term > bool *) 

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

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

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

394 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
33192  395 
 term_match thy (t1, t2) = t1 aconv t2 
396 

397 
(* typ > bool *) 

398 
fun is_TFree (TFree _) = true 

399 
 is_TFree _ = false 

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

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

402 
 is_higher_order_type _ = false 

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

404 
 is_fun_type _ = false 

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

406 
 is_set_type _ = false 

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

408 
 is_pair_type _ = false 

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

410 
 is_lfp_iterator_type _ = false 

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

412 
 is_gfp_iterator_type _ = false 

413 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

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

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

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

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

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

419 
 is_word_type _ = false 
33192  420 
val is_record_type = not o null o Record.dest_recTs 
421 
(* theory > typ > bool *) 

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

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

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

426 

427 
(* bool > styp > typ *) 

428 
fun iterator_type_for_const gfp (s, T) = 

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

430 
binder_types T) 

431 
(* typ > styp *) 

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

433 
 const_for_iterator_type T = 

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

434 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  435 

436 
(* int > typ > typ * typ *) 

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

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

439 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

442 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  443 
(* typ > typ *) 
444 
val nth_range_type = snd oo strip_n_binders 

445 

446 
(* typ > int *) 

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

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

449 
 num_factors_in_type _ = 1 

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

451 
 num_binder_types _ = 0 

452 
(* typ > typ list *) 

453 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

454 
fun maybe_curried_binder_types T = 

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

456 

457 
(* typ > term list > term *) 

458 
fun mk_flat_tuple _ [t] = t 

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

460 
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

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

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

465 

466 
(* int > typ > typ list *) 

467 
fun dest_n_tuple_type 1 T = [T] 

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

469 
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

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

471 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  472 

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

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

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

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

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

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

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

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

480 

33192  481 
(* theory > typ > typ > typ > typ *) 
482 
fun instantiate_type thy T1 T1' T2 = 

483 
Same.commit (Envir.subst_type_same 

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

485 
(Logic.varifyT T2) 

486 
handle Type.TYPE_MATCH => 

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

487 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  488 

489 
(* theory > typ > typ > styp *) 

490 
fun repair_constr_type thy body_T' T = 

491 
instantiate_type thy (body_type T) body_T' T 

492 

493 
(* string > (string * string) list > theory > theory *) 

494 
fun register_frac_type frac_s ersaetze thy = 

495 
let 

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

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

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

501 

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

503 
fun register_codatatype co_T case_name constr_xs thy = 

504 
let 

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

505 
val {frac_types, codatatypes} = Data.get thy 
33192  506 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
507 
val (co_s, co_Ts) = dest_Type co_T 

508 
val _ = 

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

509 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

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

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

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

513 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  514 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
515 
codatatypes 

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

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

519 

520 
type typedef_info = 

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

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

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

523 
Abs_inverse: thm option, Rep_inverse: thm option} 
33192  524 

525 
(* theory > string > typedef_info *) 

526 
fun typedef_info thy s = 

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

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

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

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

531 
> Logic.varify, 

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

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

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

535 
Rep_inverse, ...} => 
33192  536 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 
537 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 

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

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

539 
Rep_inverse = SOME Rep_inverse} 
33192  540 
 NONE => NONE 
541 

542 
(* theory > string > bool *) 

543 
val is_typedef = is_some oo typedef_info 

544 
val is_real_datatype = is_some oo Datatype.get_info 

545 
(* theory > typ > bool *) 

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

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

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

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

551 
is_typedef thy s andalso 

552 
not (is_real_datatype thy s orelse is_codatatype thy T 

553 
orelse is_record_type T orelse is_integer_type T) 

554 
 is_pure_typedef _ _ = false 

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

556 
(case typedef_info thy s of 

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

558 
(case set_def of 

559 
SOME thm => 

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

561 
 NONE => 

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

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

563 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} 
33192  564 
 NONE => false) 
565 
 is_univ_typedef _ _ = false 

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

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

568 
andalso not (is_basic_datatype s) 

569 
 is_datatype _ _ = false 

570 

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

572 
fun all_record_fields thy T = 

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

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

575 
end 

576 
handle TYPE _ => [] 

577 
(* styp > bool *) 

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

579 
String.isSuffix Record.extN s andalso 

580 
let val dataT = body_type T in 

581 
is_record_type dataT andalso 

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

583 
end 

584 
(* theory > typ > int *) 

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

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

587 
fun no_of_record_field thy s T1 = 

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

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

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

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

592 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  593 
 is_record_get _ _ = false 
594 
fun is_record_update thy (s, T) = 

595 
String.isSuffix Record.updateN s andalso 

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

596 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  597 
(all_record_fields thy (body_type T)) 
598 
handle TYPE _ => false 

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

600 
(case typedef_info thy s' of 

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

602 
 NONE => false) 

603 
 is_abs_fun _ _ = false 

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

605 
(case typedef_info thy s' of 

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

607 
 NONE => false) 

608 
 is_rep_fun _ _ = false 

609 

610 
(* theory > styp > styp *) 

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

612 
(case typedef_info thy s' of 

613 
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

614 
 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

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

617 
(* theory > styp > bool *) 

618 
fun is_coconstr thy (s, T) = 

619 
let 

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

620 
val {codatatypes, ...} = Data.get thy 
33192  621 
val co_T = body_type T 
622 
val co_s = dest_Type co_T > fst 

623 
in 

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

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

626 
end 

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

628 
fun is_constr_like thy (s, T) = 

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

629 
s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

630 
let val (x as (s, T)) = (s, unbit_and_unbox_type T) in 
33192  631 
Refute.is_IDT_constructor thy x orelse is_record_constr x 
632 
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) 

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

633 
orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} 
33192  634 
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) 
635 
orelse is_coconstr thy x 

636 
end 

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

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

638 
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

639 
andalso not (is_coconstr thy x) 
33192  640 
fun is_constr thy (x as (_, T)) = 
641 
is_constr_like thy x 

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

642 
andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

643 
andalso not (is_stale_constr thy x) 
33192  644 
(* string > bool *) 
645 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

646 
val is_sel_like_and_no_discr = 

647 
String.isPrefix sel_prefix 

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

649 

650 
datatype boxability = 

651 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

652 

653 
(* boxability > boxability *) 

654 
fun in_fun_lhs_for InConstr = InSel 

655 
 in_fun_lhs_for _ = InFunLHS 

656 
fun in_fun_rhs_for InConstr = InConstr 

657 
 in_fun_rhs_for InSel = InSel 

658 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

659 
 in_fun_rhs_for _ = InFunRHS1 

660 

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

662 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

663 
case T of 

664 
Type ("fun", _) => 

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

665 
(boxy = InPair orelse boxy = InFunLHS) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

666 
andalso not (is_boolean_type (body_type T)) 
33192  667 
 Type ("*", Ts) => 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

668 
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

669 
orelse ((boxy = InExpr orelse boxy = InFunLHS) 
33192  670 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 
671 
(map (box_type ext_ctxt InPair) Ts)) 

672 
 _ => false 

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

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

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

676 
SOME (SOME box_me) => box_me 

677 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

678 
(* extended_context > boxability > typ > typ *) 

679 
and box_type ext_ctxt boxy T = 

680 
case T of 

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

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

682 
if boxy <> InConstr andalso boxy <> InSel 
33192  683 
andalso should_box_type ext_ctxt boxy z then 
684 
Type (@{type_name fun_box}, 

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

686 
else 

687 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

688 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

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

690 
if should_box_type ext_ctxt boxy z then 

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

692 
else 

693 
Type ("*", map (box_type ext_ctxt 

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

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

695 
else InPair)) Ts) 
33192  696 
 _ => T 
697 

698 
(* styp > styp *) 

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

700 

701 
(* typ > int *) 

702 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

703 
(* string > int > string *) 

704 
fun nth_sel_name_for_constr_name s n = 

705 
if s = @{const_name Pair} then 

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

707 
else 

708 
sel_prefix_for n ^ s 

709 
(* styp > int > styp *) 

710 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

711 
 nth_sel_for_constr (s, T) n = 

712 
(nth_sel_name_for_constr_name s n, 

713 
body_type T > nth (maybe_curried_binder_types T) n) 

714 
(* extended_context > styp > int > styp *) 

715 
fun boxed_nth_sel_for_constr ext_ctxt = 

716 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

717 

718 
(* string > int *) 

719 
fun sel_no_from_name s = 

720 
if String.isPrefix discr_prefix s then 

721 
~1 

722 
else if String.isPrefix sel_prefix s then 

723 
s > unprefix sel_prefix > Int.fromString > the 

724 
else if s = @{const_name snd} then 

725 
1 

726 
else 

727 
0 

728 

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

730 
fun eta_expand _ t 0 = t 

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

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

733 
 eta_expand Ts t n = 

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

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

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

737 

738 
(* term > term *) 

739 
fun extensionalize t = 

740 
case t of 

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

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

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

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

745 
end 

746 
 _ => t 

747 

748 
(* typ > term list > term *) 

749 
fun distinctness_formula T = 

750 
all_distinct_unordered_pairs_of 

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

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

753 

754 
(* typ > term *) 

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

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

757 

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

759 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

793 
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

794 
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

795 
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

796 
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

797 
 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

798 
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

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

800 
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

801 
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

802 
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

803 
(* extended_context > typ > int *) 
33192  804 
val num_datatype_constrs = length oo datatype_constrs 
805 

806 
(* string > string *) 

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

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

809 
 constr_name_for_sel_like s' = original_name s' 

810 
(* extended_context > styp > styp *) 

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

812 
let val s = constr_name_for_sel_like s' in 

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

814 
> the > pair s 

815 
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

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

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

820 
Abs (Name.uu, dataT, 

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

822 
else if num_datatype_constrs ext_ctxt dataT >= 2 then 
33192  823 
Const (discr_for_constr x) 
824 
else 

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

826 
end 

827 

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

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

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

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

833 
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

834 
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

835 
 _ => betapply (discr_term_for_constr ext_ctxt x, t) 
33192  836 

837 
(* styp > term > term *) 

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

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

840 
if dataT = nat_T then 

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

842 
else if is_pair_type dataT then 

843 
Const (nth_sel_for_constr x n) 

844 
else 

845 
let 

846 
(* int > typ > int * term *) 

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

848 
let 

849 
val (m, t1) = aux m T1 

850 
val (m, t2) = aux m T2 

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

852 
 aux m T = 

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

854 
$ Bound 0) 

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

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

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

858 
end 

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

860 
fun select_nth_constr_arg thy x t n res_T = 

861 
case strip_comb t of 

862 
(Const x', args) => 

863 
if x = x' then nth args n 

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

865 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

867 

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

869 
fun construct_value _ x [] = Const x 

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

871 
let val args = map Envir.eta_contract args in 

872 
case hd args of 

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

874 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

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

876 
select_nth_constr_arg thy x t n dummyT = t') 

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

878 
t 

879 
else 

880 
list_comb (Const x, args) 

881 
 _ => list_comb (Const x, args) 

882 
end 

883 

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

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

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

888 
 _ => raise SAME ()) 

889 
handle SAME () => 

890 
let 

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

892 
if is_pair_type T then 

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

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

894 
(@{const_name Pair}, T1 > T2 > T) 
33192  895 
end 
896 
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

897 
datatype_constrs ext_ctxt T > the_single 
33192  898 
val arg_Ts = binder_types T' 
899 
in 

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

901 
(index_seq 0 (length arg_Ts)) arg_Ts) 

902 
end 

903 

904 
(* (typ * int) list > typ > int *) 

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

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

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

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

908 
card_of_type assigns T1 * card_of_type assigns T2 
33192  909 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
910 
 card_of_type _ @{typ prop} = 2 

911 
 card_of_type _ @{typ bool} = 2 

912 
 card_of_type _ @{typ unit} = 1 

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

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

914 
case AList.lookup (op =) assigns T of 
33192  915 
SOME k => k 
916 
 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

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

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

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

922 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  923 
in 
924 
if k1 = max orelse k2 = max then max 

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

926 
end 

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

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

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

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

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

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

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

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

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

940 
fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = 
33192  941 
let 
942 
(* typ list > typ > int *) 

943 
fun aux avoid T = 

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

944 
(if member (op =) avoid T then 
33192  945 
0 
946 
else case T of 

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

948 
let 

949 
val k1 = aux avoid T1 

950 
val k2 = aux avoid T2 

951 
in 

952 
if k1 = 0 orelse k2 = 0 then 0 

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

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

955 
end 

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

957 
let 

958 
val k1 = aux avoid T1 

959 
val k2 = aux avoid T2 

960 
in 

961 
if k1 = 0 orelse k2 = 0 then 0 

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

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

964 
end 

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

966 
 @{typ prop} => 2 

967 
 @{typ bool} => 2 

968 
 @{typ unit} => 1 

969 
 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

970 
(case datatype_constrs ext_ctxt T of 
33192  971 
[] => if is_integer_type T then 0 else raise SAME () 
972 
 constrs => 

973 
let 

974 
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

975 
datatype_constrs ext_ctxt T 
33192  976 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
977 
o snd) 

978 
in 

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

979 
if exists (curry (op =) 0) constr_cards then 0 
33192  980 
else Integer.sum constr_cards 
981 
end) 

982 
 _ => raise SAME ()) 

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

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

984 
AList.lookup (op =) assigns T > the_default default_card 
33192  985 
in Int.min (max, aux [] T) end 
986 

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

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

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

989 
not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] 
33192  990 

991 
(* term > bool *) 

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

993 
 is_ground_term (Const _) = true 

994 
 is_ground_term _ = false 

995 

996 
(* term > word > word *) 

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

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

999 
 hashw_term _ = 0w0 

1000 
(* term > int *) 

1001 
val hash_term = Word.toInt o hashw_term 

1002 

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

1004 
fun special_bounds ts = 

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

1006 

1007 
(* indexname * typ > term > term *) 

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

1009 

33571  1010 
(* theory > string > bool *) 
1011 
fun is_funky_typedef_name thy s = 

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

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

1013 
@{type_name int}] s 
33571  1014 
orelse is_frac_type thy (Type (s, [])) 
1015 
(* theory > term > bool *) 

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

1017 
 is_funky_typedef _ _ = false 

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

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

1021 
 is_arity_type_axiom _ = false 

1022 
(* theory > bool > term > bool *) 

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

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

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

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

1027 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1028 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1029 
 is_typedef_axiom _ _ _ = false 
1030 

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

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

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

1034 
using "typedef_info". *) 

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

1036 
fun partition_axioms_by_definitionality thy axioms def_names = 

1037 
let 

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

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

1040 
val nondefs = 

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

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

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

1044 

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

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

1046 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1047 
commands. *) 
1048 
(* theory > bool *) 

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

1050 

1051 
(* term > bool *) 

1052 
val is_plain_definition = 

1053 
let 

1054 
(* term > bool *) 

1055 
fun do_lhs t1 = 

1056 
case strip_comb t1 of 

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

1058 
andalso not (has_duplicates (op =) args) 

1059 
 _ => false 

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

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

1062 
do_lhs t1 

1063 
 do_eq _ = false 

1064 
in do_eq end 

1065 

1066 
(* theory > term list * term list * term list *) 

1067 
fun all_axioms_of thy = 

1068 
let 

1069 
(* theory list > term list *) 

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

1071 
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

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

1073 
> OrdList.make fast_string_ord 
33192  1074 
val thys = thy :: Theory.ancestors_of thy 
1075 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1076 
val built_in_axioms = axioms_of_thys built_in_thys 

1077 
val user_axioms = axioms_of_thys user_thys 

1078 
val (built_in_defs, built_in_nondefs) = 

1079 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1080 
> filter (is_typedef_axiom thy false) 
33192  1081 
val (user_defs, user_nondefs) = 
1082 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

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

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

1090 
user_defs @ built_in_defs 
33192  1091 
in (defs, built_in_nondefs, user_nondefs) end 
1092 

1093 
(* bool > styp > int option *) 

1094 
fun arity_of_built_in_const fast_descrs (s, T) = 

1095 
if s = @{const_name If} then 

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

1097 
else case AList.lookup (op =) 

1098 
(built_in_consts 

1099 
> fast_descrs ? append built_in_descr_consts) s of 

1100 
SOME n => SOME n 

1101 
 NONE => 

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

1103 
SOME n => SOME n 

1104 
 NONE => 

1105 
if is_fun_type T andalso is_set_type (domain_type T) then 

1106 
AList.lookup (op =) built_in_set_consts s 

1107 
else 

1108 
NONE 

1109 
(* bool > styp > bool *) 

1110 
val is_built_in_const = is_some oo arity_of_built_in_const 

1111 

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

1113 
simplification rules (equational specifications). *) 

1114 
(* term > term *) 

1115 
fun term_under_def t = 

1116 
case t of 

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

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

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

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

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

1122 
 t1 $ _ => term_under_def t1 

1123 
 _ => t 

1124 

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

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

1127 
be matched in the face of overloading. *) 

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

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

1130 
if is_built_in_const fast_descrs x then 

1131 
[] 

1132 
else 

1133 
these (Symtab.lookup table s) 

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

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

1135 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1136 

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

1137 
(* theory > term > term option *) 
33192  1138 
fun normalized_rhs_of thy t = 
1139 
let 

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

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

1141 
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

1142 
 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

1143 
 aux _ _ = NONE 
33192  1144 
val (lhs, rhs) = 
1145 
case t of 

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

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

1148 
(t1, t2) 

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

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

1151 
in fold_rev aux args (SOME rhs) end 
33192  1152 

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

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

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

1156 
NONE 

1157 
else 

1158 
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

1159 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1160 
handle List.Empty => NONE 
1161 

1162 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1163 

1164 
(* term > fixpoint_kind *) 

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

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

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

1168 
 fixpoint_kind_of_rhs _ = NoFp 

1169 

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

1171 
fun is_mutually_inductive_pred_def thy table t = 

1172 
let 

1173 
(* term > bool *) 

1174 
fun is_good_arg (Bound _) = true 

1175 
 is_good_arg (Const (s, _)) = 

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

1176 
s = @{const_name True} orelse s = @{const_name False} 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1177 
orelse s = @{const_name undefined} 
33192  1178 
 is_good_arg _ = false 
1179 
in 

1180 
case t > strip_abs_body > strip_comb of 

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

1182 
(case def_of_const thy table x of 

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

1184 
 NONE => false) 

1185 
 _ => false 

1186 
end 

1187 
(* theory > const_table > term > term *) 

1188 
fun unfold_mutually_inductive_preds thy table = 

1189 
map_aterms (fn t as Const x => 

1190 
(case def_of_const thy table x of 

1191 
SOME t' => 

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

1193 
if is_mutually_inductive_pred_def thy table t' then t' 

1194 
else t 

1195 
end 

1196 
 NONE => t) 

1197 
 t => t) 

1198 

1199 
(* term > string * term *) 

1200 
fun pair_for_prop t = 

1201 
case term_under_def t of 

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

1203 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1207 
fun table_for get ctxt = 

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

1209 

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

1211 
fun case_const_names thy = 

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

1213 
if is_basic_datatype dtype_s then 

1214 
I 

1215 
else 

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

1217 
> the > #3 > length)) 

1218 
(Datatype.get_all thy) [] @ 

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

1219 
map (apsnd length o snd) (#codatatypes (Data.get thy)) 
33192  1220 

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

1222 
fun const_def_table ctxt ts = 

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

1223 
table_for (rev o map prop_of o Nitpick_Defs.get) ctxt 
33192  1224 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) 
1225 
(map pair_for_prop ts) 

1226 
(* term list > const_table *) 

1227 
fun const_nondef_table ts = 

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

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

1230 
(* Proof.context > const_table *) 

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

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

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

1234 
fun inductive_intro_table ctxt def_table = 

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

1236 
def_table o prop_of) 

1237 
o Nitpick_Intros.get) ctxt 

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

1239 
fun ground_theorem_table thy = 

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

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

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

1243 

1244 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1252 

1253 
(* theory > (string * string) list *) 

1254 
fun ersatz_table thy = 

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

1255 
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table 
33192  1256 

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

1258 
fun add_simps simp_table s eqs = 

1259 
Unsynchronized.change simp_table 

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

1261 

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

1263 
the first (preorder) match. *) 

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

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

1265 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1266 
let 
1267 
(* term > (typ * term) list > (typ * term) list *) 

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

1269 
if s = s' then 

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

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

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

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

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

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

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

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

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

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

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

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

1281 
\axiom involving " ^ quote s)) 
33192  1282 
else 
1283 
ys 

1284 
 aux _ ys = ys 

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

1286 

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

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

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

1289 
these (Symtab.lookup table s) > maps (multi_specialize_type thy slack x) 
33192  1290 

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

1292 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

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

1294 
if is_univ_typedef thy abs_T then 

1295 
[] 

1296 
else case typedef_info thy abs_s of 

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

1298 
...} => 

1299 
let 

1300 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

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

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

1303 
val set_t' = 

1304 
prop_of_Rep > HOLogic.dest_Trueprop 

1305 
> Refute.specialize_type thy (dest_Const rep_t) 

1306 
> HOLogic.dest_mem > snd 

1307 
in 

1308 
[HOLogic.all_const abs_T 

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

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

1311 
> map HOLogic.mk_Trueprop 

1312 
end 

1313 
 NONE => [] 

1314 
end 

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

1315 
(* theory > styp > term list *) 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

1316 
fun inverse_axioms_for_rep_fun thy (x as (_, T)) = 
33864
232daf7eafaf
fix Nitpick soundness bugs related to integration (in particular, "code_numeral")
blanchet
parents:
33851
diff
changeset

1317 
let val abs_T = domain_type T in 
33876
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

1318 
typedef_info thy (fst (dest_Type abs_T)) > the 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

1319 
> pairf #Abs_inverse #Rep_inverse 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

1320 
> pairself (Refute.specialize_type thy x o prop_of o the) 
62bcf6a52493
fixed soundness bug in Nitpick's handling of typedefs
blanchet
parents:
33864
diff
changeset

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

1322 
end 
33192  1323 

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

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

1326 
let val arg_Ts = binder_types T in 

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

1328 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1329 
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

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

1331 
fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1332 
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

1333 
$ 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: 