author  blanchet 
Mon, 14 Dec 2009 12:30:26 +0100  
changeset 34121  5e831d805118 
parent 33978  2380c1dac86e 
child 34123  c4988215a691 
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 

114 
val bounded_precise_card_of_type : 

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

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

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

901 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) 

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

903 
card_of_type asgns T1 * card_of_type asgns T2 

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 

908 
 card_of_type asgns T = 

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

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 *) 
914 
fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = 

915 
let 

916 
val k1 = bounded_card_of_type max default_card asgns T1 

917 
val k2 = bounded_card_of_type max default_card asgns T2 

918 
in 

919 
if k1 = max orelse k2 = max then max 

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

921 
end 

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

923 
let 

924 
val k1 = bounded_card_of_type max default_card asgns T1 

925 
val k2 = bounded_card_of_type max default_card asgns T2 

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

927 
 bounded_card_of_type max default_card asgns T = 

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

929 
card_of_type asgns T 

930 
else 

931 
card_of_type asgns 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 *) 
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

935 
fun bounded_precise_card_of_type ext_ctxt max default_card asgns 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 ()) 

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

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

980 

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

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

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

983 
not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 [] 
33192  984 

985 
(* term > bool *) 

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

987 
 is_ground_term (Const _) = true 

988 
 is_ground_term _ = false 

989 

990 
(* term > word > word *) 

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

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

993 
 hashw_term _ = 0w0 

994 
(* term > int *) 

995 
val hash_term = Word.toInt o hashw_term 

996 

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

998 
fun special_bounds ts = 

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

1000 

1001 
(* indexname * typ > term > term *) 

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

1003 

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

1006 
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

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

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

1011 
 is_funky_typedef _ _ = false 

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

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

1015 
 is_arity_type_axiom _ = false 

1016 
(* theory > bool > term > bool *) 

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

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

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

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

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

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

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

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

1028 
using "typedef_info". *) 

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

1030 
fun partition_axioms_by_definitionality thy axioms def_names = 

1031 
let 

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

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

1034 
val nondefs = 

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

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

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

1038 

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

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

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

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

1044 

1045 
(* term > bool *) 

1046 
val is_plain_definition = 

1047 
let 

1048 
(* term > bool *) 

1049 
fun do_lhs t1 = 

1050 
case strip_comb t1 of 

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

1052 
andalso not (has_duplicates (op =) args) 

1053 
 _ => false 

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

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

1056 
do_lhs t1 

1057 
 do_eq _ = false 

1058 
in do_eq end 

1059 

1060 
(* theory > term list * term list * term list *) 

1061 
fun all_axioms_of thy = 

1062 
let 

1063 
(* theory list > term list *) 

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

1065 
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

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

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

1070 
val built_in_axioms = axioms_of_thys built_in_thys 

1071 
val user_axioms = axioms_of_thys user_thys 

1072 
val (built_in_defs, built_in_nondefs) = 

1073 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

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

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

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

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

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

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

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

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

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

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

1087 
(* bool > styp > int option *) 

1088 
fun arity_of_built_in_const fast_descrs (s, T) = 

1089 
if s = @{const_name If} then 

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

1091 
else case AList.lookup (op =) 

1092 
(built_in_consts 

1093 
> fast_descrs ? append built_in_descr_consts) s of 

1094 
SOME n => SOME n 

1095 
 NONE => 

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

1097 
SOME n => SOME n 

1098 
 NONE => 

1099 
if is_fun_type T andalso is_set_type (domain_type T) then 

1100 
AList.lookup (op =) built_in_set_consts s 

1101 
else 

1102 
NONE 

1103 
(* bool > styp > bool *) 

1104 
val is_built_in_const = is_some oo arity_of_built_in_const 

1105 

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

1107 
simplification rules (equational specifications). *) 

1108 
(* term > term *) 

1109 
fun term_under_def t = 

1110 
case t of 

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

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

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

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

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

1116 
 t1 $ _ => term_under_def t1 

1117 
 _ => t 

1118 

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

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

1121 
be matched in the face of overloading. *) 

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

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

1124 
if is_built_in_const fast_descrs x then 

1125 
[] 

1126 
else 

1127 
these (Symtab.lookup table s) 

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

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

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

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

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

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

1135 
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

1136 
 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

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

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

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

1142 
(t1, t2) 

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

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

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

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

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

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

1150 
NONE 

1151 
else 

1152 
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

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

1156 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1157 

1158 
(* term > fixpoint_kind *) 

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

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

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

1162 
 fixpoint_kind_of_rhs _ = NoFp 

1163 

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

1165 
fun is_mutually_inductive_pred_def thy table t = 

1166 
let 

1167 
(* term > bool *) 

1168 
fun is_good_arg (Bound _) = true 

1169 
 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

1170 
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

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

1174 
case t > strip_abs_body > strip_comb of 

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

1176 
(case def_of_const thy table x of 

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

1178 
 NONE => false) 

1179 
 _ => false 

1180 
end 

1181 
(* theory > const_table > term > term *) 

1182 
fun unfold_mutually_inductive_preds thy table = 

1183 
map_aterms (fn t as Const x => 

1184 
(case def_of_const thy table x of 

1185 
SOME t' => 

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

1187 
if is_mutually_inductive_pred_def thy table t' then t' 

1188 
else t 

1189 
end 

1190 
 NONE => t) 

1191 
 t => t) 

1192 

1193 
(* term > string * term *) 

1194 
fun pair_for_prop t = 

1195 
case term_under_def t of 

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

1197 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1201 
fun table_for get ctxt = 

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

1203 

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

1205 
fun case_const_names thy = 

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

1207 
if is_basic_datatype dtype_s then 

1208 
I 

1209 
else 

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

1211 
> the > #3 > length)) 

1212 
(Datatype.get_all thy) [] @ 

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

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

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

1216 
fun const_def_table ctxt ts = 

1217 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

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

1219 
(map pair_for_prop ts) 

1220 
(* term list > const_table *) 

1221 
fun const_nondef_table ts = 

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

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

1224 
(* Proof.context > const_table *) 

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

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

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

1228 
fun inductive_intro_table ctxt def_table = 

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

1230 
def_table o prop_of) 

1231 
o Nitpick_Intros.get) ctxt 

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

1233 
fun ground_theorem_table thy = 

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

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

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

1237 

1238 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1246 

1247 
(* theory > (string * string) list *) 

1248 
fun ersatz_table thy = 

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

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

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

1252 
fun add_simps simp_table s eqs = 

1253 
Unsynchronized.change simp_table 

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

1255 

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

1257 
the first (preorder) match. *) 

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

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

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

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

1263 
if s = s' then 

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

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

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

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

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

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

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

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

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

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

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

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

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

1278 
 aux _ ys = ys 

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

1280 

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

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

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

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

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

1286 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

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

1288 
if is_univ_typedef thy abs_T then 

1289 
[] 

1290 
else case typedef_info thy abs_s of 

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

1292 
...} => 

1293 
let 

1294 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

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

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

1297 
val set_t' = 

1298 
prop_of_Rep > HOLogic.dest_Trueprop 

1299 
> Refute.specialize_type thy (dest_Const rep_t) 

1300 
> HOLogic.dest_mem > snd 

1301 
in 

1302 
[HOLogic.all_const abs_T 

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

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

1305 
> map HOLogic.mk_Trueprop 

1306 
end 

1307 
 NONE => [] 

1308 
end 

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

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

1310 
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

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

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

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

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

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

1316 
end 
33192  1317 

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

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

1320 
let val arg_Ts = binder_types T in 

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

1322 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1323 
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

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

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

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

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

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

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

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

1335 
in 

1336 
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

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

1340 

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

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

1342 
fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t = 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33578
diff
changeset

1343 
let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in 
33192  1344 
case no_of_record_field thy s rec_T of 
1345 
~1 => (case rec_T of 

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