author  blanchet 
Mon, 14 Dec 2009 16:48:49 +0100  
changeset 34123  c4988215a691 
parent 34121  5e831d805118 
child 34124  c4628a1dcf75 
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, 

24 
destroy_constrs: bool, 

25 
specialize: bool, 

26 
skolemize: bool, 

27 
star_linear_preds: bool, 

28 
uncurry: bool, 

29 
fast_descrs: bool, 

30 
tac_timeout: Time.time option, 

31 
evals: term list, 

32 
case_names: (string * int) list, 

33 
def_table: const_table, 

34 
nondef_table: const_table, 

35 
user_nondefs: term list, 

36 
simp_table: const_table Unsynchronized.ref, 

37 
psimp_table: const_table, 

38 
intro_table: const_table, 

39 
ground_thm_table: term list Inttab.table, 

40 
ersatz_table: (string * string) list, 

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

42 
special_funs: special_fun list Unsynchronized.ref, 

43 
unrolled_preds: unrolled list Unsynchronized.ref, 

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

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

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

47 
val name_sep : string 

48 
val numeral_prefix : string 

49 
val skolem_prefix : string 

50 
val eval_prefix : string 

51 
val original_name : string > string 

52 
val unbox_type : typ > typ 

53 
val string_for_type : Proof.context > typ > string 

54 
val prefix_name : string > string > string 

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

55 
val shortest_name : string > string 
33192  56 
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

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

60 
val term_match : theory > term * term > bool 

61 
val is_TFree : typ > bool 

62 
val is_higher_order_type : typ > bool 

63 
val is_fun_type : typ > bool 

64 
val is_set_type : typ > bool 

65 
val is_pair_type : typ > bool 

66 
val is_lfp_iterator_type : typ > bool 

67 
val is_gfp_iterator_type : typ > bool 

68 
val is_fp_iterator_type : typ > bool 

69 
val is_boolean_type : typ > bool 

70 
val is_integer_type : typ > bool 

71 
val is_record_type : typ > bool 

72 
val is_number_type : theory > typ > bool 

73 
val const_for_iterator_type : typ > styp 

74 
val nth_range_type : int > typ > typ 

75 
val num_factors_in_type : typ > int 

76 
val num_binder_types : typ > int 

77 
val curried_binder_types : typ > typ list 

78 
val mk_flat_tuple : typ > term list > term 

79 
val dest_n_tuple : int > term > term list 

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

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

81 
val is_real_datatype : theory > string > bool 
33192  82 
val is_codatatype : theory > typ > bool 
83 
val is_pure_typedef : theory > typ > bool 

84 
val is_univ_typedef : theory > typ > bool 

85 
val is_datatype : theory > typ > bool 

86 
val is_record_constr : styp > bool 

87 
val is_record_get : theory > styp > bool 

88 
val is_record_update : theory > styp > bool 

89 
val is_abs_fun : theory > styp > bool 

90 
val is_rep_fun : theory > styp > bool 

91 
val is_constr : theory > styp > bool 

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

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

95 
val num_sels_for_constr_type : typ > int 

96 
val nth_sel_name_for_constr_name : string > int > string 

97 
val nth_sel_for_constr : styp > int > styp 

98 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

99 
val sel_no_from_name : string > int 

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

101 
val extensionalize : term > term 

102 
val distinctness_formula : typ > term list > term 

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

104 
val unregister_frac_type : string > theory > theory 

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

106 
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

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

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

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

113 
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

114 
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

115 
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

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

119 
val is_built_in_const : bool > styp > bool 

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

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

122 
val const_nondef_table : term list > const_table 

123 
val const_simp_table : Proof.context > const_table 

124 
val const_psimp_table : Proof.context > const_table 

125 
val inductive_intro_table : Proof.context > const_table > const_table 

126 
val ground_theorem_table : theory > term list Inttab.table 

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

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

129 
val is_inductive_pred : extended_context > styp > bool 

130 
val is_constr_pattern_lhs : theory > term > bool 

131 
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

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

135 
val format_type : int list > int list > typ > typ 

136 
val format_term_type : 

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

138 
val user_friendly_const : 

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

140 
> styp > term * typ 

141 
val assign_operator_for_const : styp > string 

142 
val preprocess_term : 

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

144 
end; 

145 

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

146 
structure Nitpick_HOL : NITPICK_HOL = 
33192  147 
struct 
148 

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

149 
open Nitpick_Util 
33192  150 

151 
type const_table = term list Symtab.table 

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

153 
type unrolled = styp * styp 

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

155 

156 
type extended_context = { 

157 
thy: theory, 

158 
ctxt: Proof.context, 

159 
max_bisim_depth: int, 

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

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

162 
user_axioms: bool option, 

163 
debug: bool, 

164 
destroy_constrs: bool, 

165 
specialize: bool, 

166 
skolemize: bool, 

167 
star_linear_preds: bool, 

168 
uncurry: bool, 

169 
fast_descrs: bool, 

170 
tac_timeout: Time.time option, 

171 
evals: term list, 

172 
case_names: (string * int) list, 

173 
def_table: const_table, 

174 
nondef_table: const_table, 

175 
user_nondefs: term list, 

176 
simp_table: const_table Unsynchronized.ref, 

177 
psimp_table: const_table, 

178 
intro_table: const_table, 

179 
ground_thm_table: term list Inttab.table, 

180 
ersatz_table: (string * string) list, 

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

182 
special_funs: special_fun list Unsynchronized.ref, 

183 
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

184 
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

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

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

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

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

191 
val extend = I 

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

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

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

197 
(* term * term > term *) 

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

199 
 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

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

201 
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

202 
else HOLogic.mk_conj (t1, t2) 
33192  203 
fun s_disj (t1, @{const False}) = t1 
204 
 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

205 
 s_disj (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 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

207 
else HOLogic.mk_disj (t1, t2) 
33192  208 
(* term > term > term *) 
209 
fun mk_exists v t = 

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

211 

212 
(* term > term > term list *) 

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

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

215 
 strip_connective _ t = [t] 

216 
(* term > term list * term *) 

217 
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

218 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 
33192  219 
(strip_connective t0 t, t0) 
220 
else 

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

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

223 
(* term > term list *) 

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

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

226 

227 
val name_sep = "$" 

228 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

229 
val sel_prefix = nitpick_prefix ^ "sel" 

230 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

231 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

232 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

233 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

234 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

235 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

236 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

237 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

238 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

239 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

240 
val skolem_prefix = nitpick_prefix ^ "sk" 

241 
val special_prefix = nitpick_prefix ^ "sp" 

242 
val uncurry_prefix = nitpick_prefix ^ "unc" 

243 
val eval_prefix = nitpick_prefix ^ "eval" 

244 
val bound_var_prefix = "b" 

245 
val cong_var_prefix = "c" 

246 
val iter_var_prefix = "i" 

247 
val val_var_prefix = nitpick_prefix ^ "v" 

248 
val arg_var_prefix = "x" 

249 

250 
(* int > string *) 

251 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

252 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

253 
(* int > int > string *) 

254 
fun skolem_prefix_for k j = 

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

256 
fun uncurry_prefix_for k j = 

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

258 

259 
(* string > string * string *) 

260 
val strip_first_name_sep = 

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

262 
#> pairself Substring.string 

263 
(* string > string *) 

264 
fun original_name s = 

265 
if String.isPrefix nitpick_prefix s then 

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

267 
else 

268 
s 

269 
val after_name_sep = snd o strip_first_name_sep 

270 

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

272 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  273 
well. *) 
274 
val built_in_consts = 

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

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

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

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

279 
(@{const_name Trueprop}, 1), 

280 
(@{const_name Not}, 1), 

281 
(@{const_name False}, 0), 

282 
(@{const_name True}, 0), 

283 
(@{const_name All}, 1), 

284 
(@{const_name Ex}, 1), 

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

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

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

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

289 
(@{const_name If}, 3), 

290 
(@{const_name Let}, 2), 

291 
(@{const_name Unity}, 0), 

292 
(@{const_name Pair}, 2), 

293 
(@{const_name fst}, 1), 

294 
(@{const_name snd}, 1), 

295 
(@{const_name Id}, 0), 

296 
(@{const_name insert}, 2), 

297 
(@{const_name converse}, 1), 

298 
(@{const_name trancl}, 1), 

299 
(@{const_name rel_comp}, 2), 

300 
(@{const_name image}, 2), 

301 
(@{const_name Suc}, 0), 

302 
(@{const_name finite}, 1), 

303 
(@{const_name nat}, 0), 

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

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

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

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

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

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

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

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

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

313 
(@{const_name nat_gcd}, 0), 

314 
(@{const_name nat_lcm}, 0), 

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

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

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

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

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

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

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

33571  322 
(@{const_name uminus_int_inst.uminus_int}, 0), 
33192  323 
(@{const_name ord_int_inst.less_int}, 2), 
324 
(@{const_name ord_int_inst.less_eq_int}, 2), 

325 
(@{const_name Tha}, 1), 

326 
(@{const_name Frac}, 0), 

327 
(@{const_name norm_frac}, 0)] 

328 
val built_in_descr_consts = 

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

330 
(@{const_name Eps}, 1)] 

331 
val built_in_typed_consts = 

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

333 
val built_in_set_consts = 

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

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

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

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

338 

339 
(* typ > typ *) 

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

341 
Type ("fun", map unbox_type Ts) 

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

343 
Type ("*", map unbox_type Ts) 

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

345 
 unbox_type T = T 

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

347 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type 

348 

349 
(* string > string > string *) 

350 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

351 
(* string > string *) 

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

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

355 
(* term > term *) 

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

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

358 
fun short_name s = 
33192  359 
case space_explode name_sep s of 
360 
[_] => 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

361 
 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

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

363 
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

364 
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

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

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

368 
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

369 
#> map_types shorten_names_in_type 
33192  370 

371 
(* theory > typ * typ > bool *) 

372 
fun type_match thy (T1, T2) = 

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

374 
handle Type.TYPE_MATCH => false 

375 
(* theory > styp * styp > bool *) 

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

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

378 
(* theory > term * term > bool *) 

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

380 
 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

381 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
33192  382 
 term_match thy (t1, t2) = t1 aconv t2 
383 

384 
(* typ > bool *) 

385 
fun is_TFree (TFree _) = true 

386 
 is_TFree _ = false 

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

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

389 
 is_higher_order_type _ = false 

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

391 
 is_fun_type _ = false 

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

393 
 is_set_type _ = false 

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

395 
 is_pair_type _ = false 

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

397 
 is_lfp_iterator_type _ = false 

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

399 
 is_gfp_iterator_type _ = false 

400 
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

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

404 
val is_record_type = not o null o Record.dest_recTs 

405 
(* theory > typ > bool *) 

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

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

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

410 

411 
(* bool > styp > typ *) 

412 
fun iterator_type_for_const gfp (s, T) = 

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

414 
binder_types T) 

415 
(* typ > styp *) 

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

417 
 const_for_iterator_type T = 

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

418 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  419 

420 
(* int > typ > typ * typ *) 

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

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

423 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

426 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  427 
(* typ > typ *) 
428 
val nth_range_type = snd oo strip_n_binders 

429 

430 
(* typ > int *) 

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

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

433 
 num_factors_in_type _ = 1 

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

435 
 num_binder_types _ = 0 

436 
(* typ > typ list *) 

437 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

438 
fun maybe_curried_binder_types T = 

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

440 

441 
(* typ > term list > term *) 

442 
fun mk_flat_tuple _ [t] = t 

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

444 
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

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

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

449 

450 
(* int > typ > typ list *) 

451 
fun dest_n_tuple_type 1 T = [T] 

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

453 
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

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

455 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  456 

457 
(* (typ * typ) list > typ > typ *) 

458 
fun typ_subst [] T = T 

459 
 typ_subst ps T = 

460 
let 

461 
(* typ > typ *) 

462 
fun subst T = 

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

464 
SOME T' => T' 

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

466 
in subst T end 

467 

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

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

469 
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

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

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

472 
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

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

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

475 

33192  476 
(* theory > typ > typ > typ > typ *) 
477 
fun instantiate_type thy T1 T1' T2 = 

478 
Same.commit (Envir.subst_type_same 

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

480 
(Logic.varifyT T2) 

481 
handle Type.TYPE_MATCH => 

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

482 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  483 

484 
(* theory > typ > typ > styp *) 

485 
fun repair_constr_type thy body_T' T = 

486 
instantiate_type thy (body_type T) body_T' T 

487 

488 
(* string > (string * string) list > theory > theory *) 

489 
fun register_frac_type frac_s ersaetze thy = 

490 
let 

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

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

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

496 

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

498 
fun register_codatatype co_T case_name constr_xs thy = 

499 
let 

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

500 
val {frac_types, codatatypes} = Data.get thy 
33192  501 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
502 
val (co_s, co_Ts) = dest_Type co_T 

503 
val _ = 

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

504 
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

505 
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

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

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

508 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  509 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
510 
codatatypes 

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

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

514 

515 
type typedef_info = 

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

517 
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

518 
Abs_inverse: thm option, Rep_inverse: thm option} 
33192  519 

520 
(* theory > string > typedef_info *) 

521 
fun typedef_info thy s = 

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

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

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

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

526 
> Logic.varify, 

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

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

529 
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

530 
Rep_inverse, ...} => 
33192  531 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 
532 
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

533 
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

534 
Rep_inverse = SOME Rep_inverse} 
33192  535 
 NONE => NONE 
536 

537 
(* theory > string > bool *) 

538 
val is_typedef = is_some oo typedef_info 

539 
val is_real_datatype = is_some oo Datatype.get_info 

540 
(* theory > typ > bool *) 

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

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

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

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

546 
is_typedef thy s andalso 

547 
not (is_real_datatype thy s orelse is_codatatype thy T 

548 
orelse is_record_type T orelse is_integer_type T) 

549 
 is_pure_typedef _ _ = false 

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

551 
(case typedef_info thy s of 

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

553 
(case set_def of 

554 
SOME thm => 

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

556 
 NONE => 

557 
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

558 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} 
33192  559 
 NONE => false) 
560 
 is_univ_typedef _ _ = false 

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

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

563 
andalso not (is_basic_datatype s) 

564 
 is_datatype _ _ = false 

565 

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

567 
fun all_record_fields thy T = 

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

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

570 
end 

571 
handle TYPE _ => [] 

572 
(* styp > bool *) 

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

574 
String.isSuffix Record.extN s andalso 

575 
let val dataT = body_type T in 

576 
is_record_type dataT andalso 

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

578 
end 

579 
(* theory > typ > int *) 

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

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

582 
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

583 
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

584 
(Record.get_extT_fields thy T1 > single > op @) 
33192  585 
(* theory > styp > bool *) 
586 
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

587 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  588 
 is_record_get _ _ = false 
589 
fun is_record_update thy (s, T) = 

590 
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

591 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  592 
(all_record_fields thy (body_type T)) 
593 
handle TYPE _ => false 

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

595 
(case typedef_info thy s' of 

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

597 
 NONE => false) 

598 
 is_abs_fun _ _ = false 

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

600 
(case typedef_info thy s' of 

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

602 
 NONE => false) 

603 
 is_rep_fun _ _ = false 

604 

605 
(* theory > styp > styp *) 

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

607 
(case typedef_info thy s' of 

608 
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

609 
 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

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

612 
(* theory > styp > bool *) 

613 
fun is_coconstr thy (s, T) = 

614 
let 

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

615 
val {codatatypes, ...} = Data.get thy 
33192  616 
val co_T = body_type T 
617 
val co_s = dest_Type co_T > fst 

618 
in 

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

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

621 
end 

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

623 
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

624 
s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse 
33192  625 
let val (x as (s, T)) = (s, unbox_type T) in 
626 
Refute.is_IDT_constructor thy x orelse is_record_constr x 

627 
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

628 
orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} 
33192  629 
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) 
630 
orelse is_coconstr thy x 

631 
end 

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

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

633 
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

634 
andalso not (is_coconstr thy x) 
33192  635 
fun is_constr thy (x as (_, T)) = 
636 
is_constr_like thy x 

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

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

638 
andalso not (is_stale_constr thy x) 
33192  639 
(* string > bool *) 
640 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

641 
val is_sel_like_and_no_discr = 

642 
String.isPrefix sel_prefix 

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

644 

645 
datatype boxability = 

646 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

647 

648 
(* boxability > boxability *) 

649 
fun in_fun_lhs_for InConstr = InSel 

650 
 in_fun_lhs_for _ = InFunLHS 

651 
fun in_fun_rhs_for InConstr = InConstr 

652 
 in_fun_rhs_for InSel = InSel 

653 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

654 
 in_fun_rhs_for _ = InFunRHS1 

655 

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

657 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

658 
case T of 

659 
Type ("fun", _) => 

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

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

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

663 
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

664 
orelse ((boxy = InExpr orelse boxy = InFunLHS) 
33192  665 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 
666 
(map (box_type ext_ctxt InPair) Ts)) 

667 
 _ => false 

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

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

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

671 
SOME (SOME box_me) => box_me 

672 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

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

674 
and box_type ext_ctxt boxy T = 

675 
case T of 

676 
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

677 
if boxy <> InConstr andalso boxy <> InSel 
33192  678 
andalso should_box_type ext_ctxt boxy z then 
679 
Type (@{type_name fun_box}, 

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

681 
else 

682 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

683 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

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

685 
if should_box_type ext_ctxt boxy z then 

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

687 
else 

688 
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

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

690 
else InPair)) Ts) 
33192  691 
 _ => T 
692 

693 
(* styp > styp *) 

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

695 

696 
(* typ > int *) 

697 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

698 
(* string > int > string *) 

699 
fun nth_sel_name_for_constr_name s n = 

700 
if s = @{const_name Pair} then 

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

702 
else 

703 
sel_prefix_for n ^ s 

704 
(* styp > int > styp *) 

705 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

706 
 nth_sel_for_constr (s, T) n = 

707 
(nth_sel_name_for_constr_name s n, 

708 
body_type T > nth (maybe_curried_binder_types T) n) 

709 
(* extended_context > styp > int > styp *) 

710 
fun boxed_nth_sel_for_constr ext_ctxt = 

711 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

712 

713 
(* string > int *) 

714 
fun sel_no_from_name s = 

715 
if String.isPrefix discr_prefix s then 

716 
~1 

717 
else if String.isPrefix sel_prefix s then 

718 
s > unprefix sel_prefix > Int.fromString > the 

719 
else if s = @{const_name snd} then 

720 
1 

721 
else 

722 
0 

723 

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

725 
fun eta_expand _ t 0 = t 

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

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

728 
 eta_expand Ts t n = 

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

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

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

732 

733 
(* term > term *) 

734 
fun extensionalize t = 

735 
case t of 

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

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

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

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

740 
end 

741 
 _ => t 

742 

743 
(* typ > term list > term *) 

744 
fun distinctness_formula T = 

745 
all_distinct_unordered_pairs_of 

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

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

748 

749 
(* typ > term *) 

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

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

752 

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

754 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

788 
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

789 
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

790 
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

791 
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

792 
 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

793 
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

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

795 
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

796 
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

797 
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

798 
(* extended_context > typ > int *) 
33192  799 
val num_datatype_constrs = length oo datatype_constrs 
800 

801 
(* string > string *) 

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

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

804 
 constr_name_for_sel_like s' = original_name s' 

805 
(* extended_context > styp > styp *) 

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

807 
let val s = constr_name_for_sel_like s' in 

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

809 
> the > pair s 

810 
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

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

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

815 
Abs (Name.uu, dataT, 

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

817 
else if num_datatype_constrs ext_ctxt dataT >= 2 then 
33192  818 
Const (discr_for_constr x) 
819 
else 

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

821 
end 

822 

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

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

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

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

828 
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

829 
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

830 
 _ => betapply (discr_term_for_constr ext_ctxt x, t) 
33192  831 

832 
(* styp > term > term *) 

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

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

835 
if dataT = nat_T then 

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

837 
else if is_pair_type dataT then 

838 
Const (nth_sel_for_constr x n) 

839 
else 

840 
let 

841 
(* int > typ > int * term *) 

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

843 
let 

844 
val (m, t1) = aux m T1 

845 
val (m, t2) = aux m T2 

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

847 
 aux m T = 

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

849 
$ Bound 0) 

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

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

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

853 
end 

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

855 
fun select_nth_constr_arg thy x t n res_T = 

856 
case strip_comb t of 

857 
(Const x', args) => 

858 
if x = x' then nth args n 

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

860 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

862 

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

864 
fun construct_value _ x [] = Const x 

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

866 
let val args = map Envir.eta_contract args in 

867 
case hd args of 

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

869 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

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

871 
select_nth_constr_arg thy x t n dummyT = t') 

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

873 
t 

874 
else 

875 
list_comb (Const x, args) 

876 
 _ => list_comb (Const x, args) 

877 
end 

878 

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

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

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

883 
 _ => raise SAME ()) 

884 
handle SAME () => 

885 
let 

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

887 
if is_pair_type T then 

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

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

890 
end 

891 
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

892 
datatype_constrs ext_ctxt T > the_single 
33192  893 
val arg_Ts = binder_types T' 
894 
in 

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

896 
(index_seq 0 (length arg_Ts)) arg_Ts) 

897 
end 

898 

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

900 
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

901 
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

902 
 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

903 
card_of_type assigns T1 * card_of_type assigns T2 
33192  904 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
905 
 card_of_type _ @{typ prop} = 2 

906 
 card_of_type _ @{typ bool} = 2 

907 
 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

908 
 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

909 
case AList.lookup (op =) assigns T of 
33192  910 
SOME k => k 
911 
 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

912 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
33192  913 
(* 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

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

916 
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

917 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  918 
in 
919 
if k1 = max orelse k2 = max then max 

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

921 
end 

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

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

924 
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

925 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  926 
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

927 
 bounded_card_of_type max default_card assigns T = 
33192  928 
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

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

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

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

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

935 
fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = 
33192  936 
let 
937 
(* typ list > typ > int *) 

938 
fun aux avoid T = 

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

939 
(if member (op =) avoid T then 
33192  940 
0 
941 
else case T of 

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

943 
let 

944 
val k1 = aux avoid T1 

945 
val k2 = aux avoid T2 

946 
in 

947 
if k1 = 0 orelse k2 = 0 then 0 

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

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

950 
end 

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

952 
let 

953 
val k1 = aux avoid T1 

954 
val k2 = aux avoid T2 

955 
in 

956 
if k1 = 0 orelse k2 = 0 then 0 

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

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

959 
end 

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

961 
 @{typ prop} => 2 

962 
 @{typ bool} => 2 

963 
 @{typ unit} => 1 

964 
 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

965 
(case datatype_constrs ext_ctxt T of 
33192  966 
[] => if is_integer_type T then 0 else raise SAME () 
967 
 constrs => 

968 
let 

969 
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

970 
datatype_constrs ext_ctxt T 
33192  971 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
972 
o snd) 

973 
in 

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

974 
if exists (curry (op =) 0) constr_cards then 0 
33192  975 
else Integer.sum constr_cards 
976 
end) 

977 
 _ => raise SAME ()) 

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

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

979 
AList.lookup (op =) assigns T > the_default default_card 
33192  980 
in Int.min (max, aux [] T) end 
981 

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

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

983 
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

984 
not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] 
33192  985 

986 
(* term > bool *) 

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

988 
 is_ground_term (Const _) = true 

989 
 is_ground_term _ = false 

990 

991 
(* term > word > word *) 

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

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

994 
 hashw_term _ = 0w0 

995 
(* term > int *) 

996 
val hash_term = Word.toInt o hashw_term 

997 

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

999 
fun special_bounds ts = 

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

1001 

1002 
(* indexname * typ > term > term *) 

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

1004 

33571  1005 
(* theory > string > bool *) 
1006 
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

1007 
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

1008 
@{type_name int}] s 
33571  1009 
orelse is_frac_type thy (Type (s, [])) 
1010 
(* theory > term > bool *) 

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

1012 
 is_funky_typedef _ _ = false 

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

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

1016 
 is_arity_type_axiom _ = false 

1017 
(* theory > bool > term > bool *) 

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

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

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

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

1022 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1023 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1024 
 is_typedef_axiom _ _ _ = false 
1025 

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

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

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

1029 
using "typedef_info". *) 

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

1031 
fun partition_axioms_by_definitionality thy axioms def_names = 

1032 
let 

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

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

1035 
val nondefs = 

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

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

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

1039 

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

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

1041 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1042 
commands. *) 
1043 
(* theory > bool *) 

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

1045 

1046 
(* term > bool *) 

1047 
val is_plain_definition = 

1048 
let 

1049 
(* term > bool *) 

1050 
fun do_lhs t1 = 

1051 
case strip_comb t1 of 

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

1053 
andalso not (has_duplicates (op =) args) 

1054 
 _ => false 

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

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

1057 
do_lhs t1 

1058 
 do_eq _ = false 

1059 
in do_eq end 

1060 

1061 
(* theory > term list * term list * term list *) 

1062 
fun all_axioms_of thy = 

1063 
let 

1064 
(* theory list > term list *) 

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

1066 
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

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

1068 
> OrdList.make fast_string_ord 
33192  1069 
val thys = thy :: Theory.ancestors_of thy 
1070 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1071 
val built_in_axioms = axioms_of_thys built_in_thys 

1072 
val user_axioms = axioms_of_thys user_thys 

1073 
val (built_in_defs, built_in_nondefs) = 

1074 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1075 
> filter (is_typedef_axiom thy false) 
33192  1076 
val (user_defs, user_nondefs) = 
1077 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

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

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

1085 
user_defs @ built_in_defs 
33192  1086 
in (defs, built_in_nondefs, user_nondefs) end 
1087 

1088 
(* bool > styp > int option *) 

1089 
fun arity_of_built_in_const fast_descrs (s, T) = 

1090 
if s = @{const_name If} then 

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

1092 
else case AList.lookup (op =) 

1093 
(built_in_consts 

1094 
> fast_descrs ? append built_in_descr_consts) s of 

1095 
SOME n => SOME n 

1096 
 NONE => 

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

1098 
SOME n => SOME n 

1099 
 NONE => 

1100 
if is_fun_type T andalso is_set_type (domain_type T) then 

1101 
AList.lookup (op =) built_in_set_consts s 

1102 
else 

1103 
NONE 

1104 
(* bool > styp > bool *) 

1105 
val is_built_in_const = is_some oo arity_of_built_in_const 

1106 

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

1108 
simplification rules (equational specifications). *) 

1109 
(* term > term *) 

1110 
fun term_under_def t = 

1111 
case t of 

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

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

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

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

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

1117 
 t1 $ _ => term_under_def t1 

1118 
 _ => t 

1119 

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

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

1122 
be matched in the face of overloading. *) 

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

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

1125 
if is_built_in_const fast_descrs x then 

1126 
[] 

1127 
else 

1128 
these (Symtab.lookup table s) 

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

1130 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1131 

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

1132 
(* theory > term > term option *) 
33192  1133 
fun normalized_rhs_of thy t = 
1134 
let 

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

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

1136 
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

1137 
 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

1138 
 aux _ _ = NONE 
33192  1139 
val (lhs, rhs) = 
1140 
case t of 

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

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

1143 
(t1, t2) 

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

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

1146 
in fold_rev aux args (SOME rhs) end 
33192  1147 

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

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

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

1151 
NONE 

1152 
else 

1153 
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

1154 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1155 
handle List.Empty => NONE 
1156 

1157 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1158 

1159 
(* term > fixpoint_kind *) 

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

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

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

1163 
 fixpoint_kind_of_rhs _ = NoFp 

1164 

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

1166 
fun is_mutually_inductive_pred_def thy table t = 

1167 
let 

1168 
(* term > bool *) 

1169 
fun is_good_arg (Bound _) = true 

1170 
 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

1171 
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

1172 
orelse s = @{const_name undefined} 
33192  1173 
 is_good_arg _ = false 
1174 
in 

1175 
case t > strip_abs_body > strip_comb of 

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

1177 
(case def_of_const thy table x of 

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

1179 
 NONE => false) 

1180 
 _ => false 

1181 
end 

1182 
(* theory > const_table > term > term *) 

1183 
fun unfold_mutually_inductive_preds thy table = 

1184 
map_aterms (fn t as Const x => 

1185 
(case def_of_const thy table x of 

1186 
SOME t' => 

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

1188 
if is_mutually_inductive_pred_def thy table t' then t' 

1189 
else t 

1190 
end 

1191 
 NONE => t) 

1192 
 t => t) 

1193 

1194 
(* term > string * term *) 

1195 
fun pair_for_prop t = 

1196 
case term_under_def t of 

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

1198 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1202 
fun table_for get ctxt = 

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

1204 

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

1206 
fun case_const_names thy = 

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

1208 
if is_basic_datatype dtype_s then 

1209 
I 

1210 
else 

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

1212 
> the > #3 > length)) 

1213 
(Datatype.get_all thy) [] @ 

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

1214 
map (apsnd length o snd) (#codatatypes (Data.get thy)) 
33192  1215 

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

1217 
fun const_def_table ctxt ts = 

1218 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

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

1220 
(map pair_for_prop ts) 

1221 
(* term list > const_table *) 

1222 
fun const_nondef_table ts = 

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

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

1225 
(* Proof.context > const_table *) 

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

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

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

1229 
fun inductive_intro_table ctxt def_table = 

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

1231 
def_table o prop_of) 

1232 
o Nitpick_Intros.get) ctxt 

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

1234 
fun ground_theorem_table thy = 

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

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

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

1238 

1239 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1247 

1248 
(* theory > (string * string) list *) 

1249 
fun ersatz_table thy = 

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

1250 
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table 
33192  1251 

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

1253 
fun add_simps simp_table s eqs = 

1254 
Unsynchronized.change simp_table 

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

1256 

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

1258 
the first (preorder) match. *) 

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

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

1260 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1261 
let 
1262 
(* term > (typ * term) list > (typ * term) list *) 

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

1264 
if s = s' then 

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

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

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

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

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

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

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

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

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

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

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

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

1276 
\axiom involving " ^ quote s)) 
33192  1277 
else 
1278 
ys 

1279 
 aux _ ys = ys 

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

1281 

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

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

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

1284 
these (Symtab.lookup table s) > maps (multi_specialize_type thy slack x) 
33192  1285 

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

1287 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

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

1289 
if is_univ_typedef thy abs_T then 

1290 
[] 

1291 
else case typedef_info thy abs_s of 

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

1293 
...} => 

1294 
let 

1295 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

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

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

1298 
val set_t' = 

1299 
prop_of_Rep > HOLogic.dest_Trueprop 

1300 
> Refute.specialize_type thy (dest_Const rep_t) 

1301 
> HOLogic.dest_mem > snd 

1302 
in 

1303 
[HOLogic.all_const abs_T 

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

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

1306 
> map HOLogic.mk_Trueprop 

1307 
end 

1308 
 NONE => [] 

1309 
end 

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

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

1311 
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

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

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

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

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

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

1317 
end 
33192  1318 

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

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

1321 
let val arg_Ts = binder_types T in 

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

1323 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1324 
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

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

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

1328 
$ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x) 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

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

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

1331 
fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T = 
33192  1332 
let 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

1333 
val xs = datatype_constrs ext_ctxt dataT 
33192  1334 
val func_Ts = map ((fn T => binder_types T > res_T) o snd) xs 
1335 
val (xs', x) = split_last xs 

1336 
in 

1337 
constr_case_body thy (1, x) 

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

1338 
> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs') 
33192  1339 
> fold_rev (curry absdummy) (func_Ts @ [dataT]) 
1340 