author  blanchet 
Fri, 05 Feb 2010 12:04:54 +0100  
changeset 35075  888802be2019 
parent 35070  96136eb6218f 
child 35078  6fd1052fe463 
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 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  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 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

16 
type hol_context = { 
33192  17 
thy: theory, 
18 
ctxt: Proof.context, 

19 
max_bisim_depth: int, 

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

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

21 
stds: (typ option * bool) list, 
33192  22 
wfs: (styp option * bool option) list, 
23 
user_axioms: bool option, 

24 
debug: bool, 

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

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

28 
skolemize: bool, 

29 
star_linear_preds: bool, 

30 
uncurry: bool, 

31 
fast_descrs: bool, 

32 
tac_timeout: Time.time option, 

33 
evals: term list, 

34 
case_names: (string * int) list, 

35 
def_table: const_table, 

36 
nondef_table: const_table, 

37 
user_nondefs: term list, 

38 
simp_table: const_table Unsynchronized.ref, 

39 
psimp_table: const_table, 

40 
intro_table: const_table, 

41 
ground_thm_table: term list Inttab.table, 

42 
ersatz_table: (string * string) list, 

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

44 
special_funs: special_fun list Unsynchronized.ref, 

45 
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

46 
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

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

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

49 
datatype fixpoint_kind = Lfp  Gfp  NoFp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

50 
datatype boxability = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

51 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

52 

33192  53 
val name_sep : string 
54 
val numeral_prefix : string 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

55 
val ubfp_prefix : string 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

56 
val lbfp_prefix : string 
33192  57 
val skolem_prefix : string 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

58 
val special_prefix : string 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

59 
val uncurry_prefix : string 
33192  60 
val eval_prefix : string 
61 
val original_name : string > string 

34998  62 
val s_conj : term * term > term 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

63 
val s_disj : term * term > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

64 
val strip_any_connective : term > term list * term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

65 
val conjuncts_of : term > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

66 
val disjuncts_of : term > term list 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

67 
val unbit_and_unbox_type : typ > typ 
33192  68 
val string_for_type : Proof.context > typ > string 
69 
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

70 
val shortest_name : string > string 
33192  71 
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

72 
val shorten_names_in_term : term > term 
33192  73 
val type_match : theory > typ * typ > bool 
74 
val const_match : theory > styp * styp > bool 

75 
val term_match : theory > term * term > bool 

76 
val is_TFree : typ > bool 

77 
val is_higher_order_type : typ > bool 

78 
val is_fun_type : typ > bool 

79 
val is_set_type : typ > bool 

80 
val is_pair_type : typ > bool 

81 
val is_lfp_iterator_type : typ > bool 

82 
val is_gfp_iterator_type : typ > bool 

83 
val is_fp_iterator_type : typ > bool 

84 
val is_boolean_type : typ > bool 

85 
val is_integer_type : typ > bool 

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

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

87 
val is_word_type : typ > bool 
33192  88 
val is_record_type : typ > bool 
89 
val is_number_type : theory > typ > bool 

90 
val const_for_iterator_type : typ > styp 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

91 
val strip_n_binders : int > typ > typ list * typ 
33192  92 
val nth_range_type : int > typ > typ 
93 
val num_factors_in_type : typ > int 

94 
val num_binder_types : typ > int 

95 
val curried_binder_types : typ > typ list 

96 
val mk_flat_tuple : typ > term list > term 

97 
val dest_n_tuple : int > term > term list 

98 
val instantiate_type : theory > typ > typ > typ > typ 

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

99 
val is_real_datatype : theory > string > bool 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

100 
val is_quot_type : theory > typ > bool 
33192  101 
val is_codatatype : theory > typ > bool 
102 
val is_pure_typedef : theory > typ > bool 

103 
val is_univ_typedef : theory > typ > bool 

104 
val is_datatype : theory > typ > bool 

105 
val is_record_constr : styp > bool 

106 
val is_record_get : theory > styp > bool 

107 
val is_record_update : theory > styp > bool 

108 
val is_abs_fun : theory > styp > bool 

109 
val is_rep_fun : theory > styp > bool 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

110 
val is_quot_abs_fun : Proof.context > styp > bool 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

111 
val is_quot_rep_fun : Proof.context > styp > bool 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

112 
val mate_of_rep_fun : theory > styp > styp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

113 
val is_constr_like : theory > styp > bool 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

114 
val is_stale_constr : theory > styp > bool 
33192  115 
val is_constr : theory > styp > bool 
116 
val is_sel : string > bool 

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

117 
val is_sel_like_and_no_discr : string > bool 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

118 
val box_type : hol_context > boxability > typ > typ 
33192  119 
val discr_for_constr : styp > styp 
120 
val num_sels_for_constr_type : typ > int 

121 
val nth_sel_name_for_constr_name : string > int > string 

122 
val nth_sel_for_constr : styp > int > styp 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

123 
val boxed_nth_sel_for_constr : hol_context > styp > int > styp 
33192  124 
val sel_no_from_name : string > int 
125 
val eta_expand : typ list > term > int > term 

126 
val extensionalize : term > term 

127 
val distinctness_formula : typ > term list > term 

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

129 
val unregister_frac_type : string > theory > theory 

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

131 
val unregister_codatatype : typ > theory > theory 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

132 
val datatype_constrs : hol_context > typ > styp list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

133 
val boxed_datatype_constrs : hol_context > typ > styp list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

134 
val num_datatype_constrs : hol_context > typ > int 
33192  135 
val constr_name_for_sel_like : string > string 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

136 
val boxed_constr_for_sel : hol_context > styp > styp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

137 
val discriminate_value : hol_context > styp > term > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

138 
val select_nth_constr_arg : theory > styp > term > int > typ > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

139 
val construct_value : theory > styp > term list > term 
33192  140 
val card_of_type : (typ * int) list > typ > int 
141 
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

142 
val bounded_exact_card_of_type : 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

143 
hol_context > int > int > (typ * int) list > typ > int 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

144 
val is_finite_type : hol_context > typ > bool 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

145 
val special_bounds : term list > (indexname * typ) list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

146 
val is_funky_typedef : theory > typ > bool 
33192  147 
val all_axioms_of : theory > term list * term list * term list 
148 
val arity_of_built_in_const : bool > styp > int option 

149 
val is_built_in_const : bool > styp > bool 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

150 
val term_under_def : term > term 
33192  151 
val case_const_names : theory > (string * int) list 
152 
val const_def_table : Proof.context > term list > const_table 

153 
val const_nondef_table : term list > const_table 

154 
val const_simp_table : Proof.context > const_table 

155 
val const_psimp_table : Proof.context > const_table 

156 
val inductive_intro_table : Proof.context > const_table > const_table 

157 
val ground_theorem_table : theory > term list Inttab.table 

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

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

159 
val add_simps : const_table Unsynchronized.ref > string > term list > unit 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

160 
val inverse_axioms_for_rep_fun : theory > styp > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

161 
val optimized_typedef_axioms : theory > string * typ list > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

162 
val optimized_quot_type_axioms : theory > string * typ list > term list 
33192  163 
val def_of_const : theory > const_table > styp > term option 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

164 
val fixpoint_kind_of_const : 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

165 
theory > const_table > string * typ > fixpoint_kind 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

166 
val is_inductive_pred : hol_context > styp > bool 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

167 
val is_equational_fun : hol_context > styp > bool 
33192  168 
val is_constr_pattern_lhs : theory > term > bool 
169 
val is_constr_pattern_formula : theory > term > bool 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

170 
val unfold_defs_in_term : hol_context > term > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

171 
val codatatype_bisim_axioms : hol_context > typ > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

172 
val is_well_founded_inductive_pred : hol_context > styp > bool 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

173 
val unrolled_inductive_pred_const : hol_context > bool > styp > term 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

174 
val equational_fun_axioms : hol_context > styp > term list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

175 
val is_equational_fun_surely_complete : hol_context > styp > 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

176 
val merge_type_vars_in_terms : term list > term list 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

177 
val ground_types_in_type : hol_context > typ > typ list 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

178 
val ground_types_in_terms : hol_context > term list > typ list 
33192  179 
val format_type : int list > int list > typ > typ 
180 
val format_term_type : 

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

182 
val user_friendly_const : 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

183 
hol_context > string * string > (term option * int list) list 
33192  184 
> styp > term * typ 
185 
val assign_operator_for_const : styp > string 

186 
end; 

187 

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

188 
structure Nitpick_HOL : NITPICK_HOL = 
33192  189 
struct 
190 

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

191 
open Nitpick_Util 
33192  192 

193 
type const_table = term list Symtab.table 

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

195 
type unrolled = styp * styp 

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

197 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

198 
type hol_context = { 
33192  199 
thy: theory, 
200 
ctxt: Proof.context, 

201 
max_bisim_depth: int, 

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

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

203 
stds: (typ option * bool) list, 
33192  204 
wfs: (styp option * bool option) list, 
205 
user_axioms: bool option, 

206 
debug: bool, 

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

207 
binary_ints: bool option, 
33192  208 
destroy_constrs: bool, 
209 
specialize: bool, 

210 
skolemize: bool, 

211 
star_linear_preds: bool, 

212 
uncurry: bool, 

213 
fast_descrs: bool, 

214 
tac_timeout: Time.time option, 

215 
evals: term list, 

216 
case_names: (string * int) list, 

217 
def_table: const_table, 

218 
nondef_table: const_table, 

219 
user_nondefs: term list, 

220 
simp_table: const_table Unsynchronized.ref, 

221 
psimp_table: const_table, 

222 
intro_table: const_table, 

223 
ground_thm_table: term list Inttab.table, 

224 
ersatz_table: (string * string) list, 

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

226 
special_funs: special_fun list Unsynchronized.ref, 

227 
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

228 
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

229 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  230 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

231 
datatype fixpoint_kind = Lfp  Gfp  NoFp 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

232 
datatype boxability = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

233 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

234 

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

235 
structure Data = Theory_Data( 
33192  236 
type T = {frac_types: (string * (string * string) list) list, 
237 
codatatypes: (string * (string * styp list)) list} 

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

239 
val extend = I 

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

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

243 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  244 

245 
val name_sep = "$" 

246 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

247 
val sel_prefix = nitpick_prefix ^ "sel" 

248 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

249 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

250 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

251 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

252 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

253 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

254 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

255 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

256 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

257 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

258 
val skolem_prefix = nitpick_prefix ^ "sk" 

259 
val special_prefix = nitpick_prefix ^ "sp" 

260 
val uncurry_prefix = nitpick_prefix ^ "unc" 

261 
val eval_prefix = nitpick_prefix ^ "eval" 

262 
val iter_var_prefix = "i" 

263 
val arg_var_prefix = "x" 

264 

265 
(* int > string *) 

266 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

267 

268 
(* string > string * string *) 

269 
val strip_first_name_sep = 

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

271 
#> pairself Substring.string 

272 
(* string > string *) 

273 
fun original_name s = 

274 
if String.isPrefix nitpick_prefix s then 

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

276 
else 

277 
s 

278 
val after_name_sep = snd o strip_first_name_sep 

279 

34998  280 
(* term * term > term *) 
281 
fun s_conj (t1, @{const True}) = t1 

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

283 
 s_conj (t1, t2) = 

284 
if t1 = @{const False} orelse t2 = @{const False} then @{const False} 

285 
else HOLogic.mk_conj (t1, t2) 

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

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

288 
 s_disj (t1, t2) = 

289 
if t1 = @{const True} orelse t2 = @{const True} then @{const True} 

290 
else HOLogic.mk_disj (t1, t2) 

291 

292 
(* term > term > term list *) 

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

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

295 
 strip_connective _ t = [t] 

296 
(* term > term list * term *) 

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

298 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 

299 
(strip_connective t0 t, t0) 

300 
else 

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

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

303 
(* term > term list *) 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

304 
val conjuncts_of = strip_connective @{const "op &"} 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

305 
val disjuncts_of = strip_connective @{const "op "} 
34998  306 

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

308 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  309 
well. *) 
310 
val built_in_consts = 

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

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

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

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

315 
(@{const_name Trueprop}, 1), 

316 
(@{const_name Not}, 1), 

317 
(@{const_name False}, 0), 

318 
(@{const_name True}, 0), 

319 
(@{const_name All}, 1), 

320 
(@{const_name Ex}, 1), 

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

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

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

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

325 
(@{const_name If}, 3), 

326 
(@{const_name Let}, 2), 

327 
(@{const_name Unity}, 0), 

328 
(@{const_name Pair}, 2), 

329 
(@{const_name fst}, 1), 

330 
(@{const_name snd}, 1), 

331 
(@{const_name Id}, 0), 

332 
(@{const_name insert}, 2), 

333 
(@{const_name converse}, 1), 

334 
(@{const_name trancl}, 1), 

335 
(@{const_name rel_comp}, 2), 

336 
(@{const_name image}, 2), 

337 
(@{const_name Suc}, 0), 

338 
(@{const_name finite}, 1), 

339 
(@{const_name nat}, 0), 

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

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

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

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

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

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

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

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

348 
(@{const_name nat_gcd}, 0), 

349 
(@{const_name nat_lcm}, 0), 

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

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

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

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

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

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

33571  356 
(@{const_name uminus_int_inst.uminus_int}, 0), 
33192  357 
(@{const_name ord_int_inst.less_int}, 2), 
358 
(@{const_name ord_int_inst.less_eq_int}, 2), 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

359 
(@{const_name unknown}, 0), 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

360 
(@{const_name is_unknown}, 1), 
33192  361 
(@{const_name Tha}, 1), 
362 
(@{const_name Frac}, 0), 

363 
(@{const_name norm_frac}, 0)] 

364 
val built_in_descr_consts = 

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

366 
(@{const_name Eps}, 1)] 

367 
val built_in_typed_consts = 

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

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

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

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

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

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

375 

376 
(* typ > typ *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

393 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type 
33192  394 

395 
(* string > string > string *) 

396 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

397 
(* string > string *) 

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

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

401 
(* string > string *) 

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

402 
fun short_name s = 
33192  403 
case space_explode name_sep s of 
404 
[_] => 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

405 
 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

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

407 
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

408 
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

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

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

412 
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

413 
#> map_types shorten_names_in_type 
33192  414 

415 
(* theory > typ * typ > bool *) 

416 
fun type_match thy (T1, T2) = 

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

418 
handle Type.TYPE_MATCH => false 

419 
(* theory > styp * styp > bool *) 

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

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

422 
(* theory > term * term > bool *) 

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

424 
 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

425 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
33192  426 
 term_match thy (t1, t2) = t1 aconv t2 
427 

428 
(* typ > bool *) 

429 
fun is_TFree (TFree _) = true 

430 
 is_TFree _ = false 

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

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

433 
 is_higher_order_type _ = false 

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

435 
 is_fun_type _ = false 

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

437 
 is_set_type _ = false 

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

439 
 is_pair_type _ = false 

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

441 
 is_lfp_iterator_type _ = false 

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

443 
 is_gfp_iterator_type _ = false 

444 
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

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

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

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

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

450 
 is_word_type _ = false 
33192  451 
val is_record_type = not o null o Record.dest_recTs 
452 
(* theory > typ > bool *) 

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

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

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

457 

458 
(* bool > styp > typ *) 

459 
fun iterator_type_for_const gfp (s, T) = 

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

461 
binder_types T) 

462 
(* typ > styp *) 

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

464 
 const_for_iterator_type T = 

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

465 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  466 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

467 
(* int > typ > typ list * typ *) 
33192  468 
fun strip_n_binders 0 T = ([], T) 
469 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

470 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

473 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  474 
(* typ > typ *) 
475 
val nth_range_type = snd oo strip_n_binders 

476 

477 
(* typ > int *) 

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

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

480 
 num_factors_in_type _ = 1 

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

482 
 num_binder_types _ = 0 

483 
(* typ > typ list *) 

484 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

485 
fun maybe_curried_binder_types T = 

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

487 

488 
(* typ > term list > term *) 

489 
fun mk_flat_tuple _ [t] = t 

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

491 
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

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

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

496 

497 
(* int > typ > typ list *) 

498 
fun dest_n_tuple_type 1 T = [T] 

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

500 
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

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

502 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  503 

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

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

505 
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

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

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

508 
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

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

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

511 

33192  512 
(* theory > typ > typ > typ > typ *) 
513 
fun instantiate_type thy T1 T1' T2 = 

514 
Same.commit (Envir.subst_type_same 

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

516 
(Logic.varifyT T2) 

517 
handle Type.TYPE_MATCH => 

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

518 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  519 

520 
(* theory > typ > typ > styp *) 

521 
fun repair_constr_type thy body_T' T = 

522 
instantiate_type thy (body_type T) body_T' T 

523 

524 
(* string > (string * string) list > theory > theory *) 

525 
fun register_frac_type frac_s ersaetze thy = 

526 
let 

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

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

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

532 

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

534 
fun register_codatatype co_T case_name constr_xs thy = 

535 
let 

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

536 
val {frac_types, codatatypes} = Data.get thy 
33192  537 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
538 
val (co_s, co_Ts) = dest_Type co_T 

539 
val _ = 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

540 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

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

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

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

544 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  545 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
546 
codatatypes 

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

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

550 

551 
type typedef_info = 

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

553 
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

554 
Abs_inverse: thm option, Rep_inverse: thm option} 
33192  555 

556 
(* theory > string > typedef_info *) 

557 
fun typedef_info thy s = 

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

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

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

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

562 
> Logic.varify, 

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

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

565 
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

566 
Rep_inverse, ...} => 
33192  567 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 
568 
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

569 
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

570 
Rep_inverse = SOME Rep_inverse} 
33192  571 
 NONE => NONE 
572 

573 
(* theory > string > bool *) 

574 
val is_typedef = is_some oo typedef_info 

575 
val is_real_datatype = is_some oo Datatype.get_info 

576 
(* theory > typ > bool *) 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

577 
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

578 
 is_quot_type _ (Type ("FSet.fset", _)) = true 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

579 
 is_quot_type _ _ = false 
33192  580 
fun is_codatatype thy (T as Type (s, _)) = 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

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

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

585 
is_typedef thy s andalso 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

586 
not (is_real_datatype thy s orelse is_quot_type thy T orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

587 
is_codatatype thy T orelse is_record_type T orelse is_integer_type T) 
33192  588 
 is_pure_typedef _ _ = false 
589 
fun is_univ_typedef thy (Type (s, _)) = 

590 
(case typedef_info thy s of 

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

592 
(case set_def of 

593 
SOME thm => 

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

595 
 NONE => 

596 
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

597 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} 
33192  598 
 NONE => false) 
599 
 is_univ_typedef _ _ = false 

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

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

601 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

602 
is_quot_type thy T) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

603 
not (is_basic_datatype s) 
33192  604 
 is_datatype _ _ = false 
605 

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

607 
fun all_record_fields thy T = 

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

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

610 
end 

611 
handle TYPE _ => [] 

612 
(* styp > bool *) 

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

614 
String.isSuffix Record.extN s andalso 

615 
let val dataT = body_type T in 

616 
is_record_type dataT andalso 

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

618 
end 

619 
(* theory > typ > int *) 

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

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

622 
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

623 
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

624 
(Record.get_extT_fields thy T1 > single > op @) 
33192  625 
(* theory > styp > bool *) 
626 
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

627 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  628 
 is_record_get _ _ = false 
629 
fun is_record_update thy (s, T) = 

630 
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

631 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  632 
(all_record_fields thy (body_type T)) 
633 
handle TYPE _ => false 

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

635 
(case typedef_info thy s' of 

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

637 
 NONE => false) 

638 
 is_abs_fun _ _ = false 

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

640 
(case typedef_info thy s' of 

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

642 
 NONE => false) 

643 
 is_rep_fun _ _ = false 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

644 
(* Proof.context > styp > bool *) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

645 
fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

646 
 is_quot_abs_fun _ ("FSet.abs_fset", _) = true 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

647 
 is_quot_abs_fun _ _ = false 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

648 
fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

649 
 is_quot_rep_fun _ ("FSet.rep_fset", _) = true 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

650 
 is_quot_rep_fun _ _ = false 
33192  651 

652 
(* theory > styp > styp *) 

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

654 
(case typedef_info thy s' of 

655 
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

656 
 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

657 
 mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

658 
(* theory > typ > typ *) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

659 
fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"} 
34998  660 
 rep_type_for_quot_type _ (Type ("FSet.fset", [T])) = 
661 
Type (@{type_name list}, [T]) 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

662 
 rep_type_for_quot_type _ T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

663 
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], []) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

664 
(* theory > typ > term *) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

665 
fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

666 
Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"}) 
34998  667 
 equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) = 
668 
Const ("FSet.list_eq", 

669 
Type (@{type_name list}, [T]) > Type (@{type_name list}, [T]) 

670 
> bool_T) 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

671 
 equiv_relation_for_quot_type _ T = 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

672 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  673 

674 
(* theory > styp > bool *) 

675 
fun is_coconstr thy (s, T) = 

676 
let 

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

677 
val {codatatypes, ...} = Data.get thy 
33192  678 
val co_T = body_type T 
679 
val co_s = dest_Type co_T > fst 

680 
in 

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

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

683 
end 

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

685 
fun is_constr_like thy (s, T) = 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

686 
member (op =) [@{const_name FunBox}, @{const_name PairBox}, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

687 
@{const_name Quot}, @{const_name Zero_Rep}, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

688 
@{const_name Suc_Rep}] s orelse 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

689 
let val (x as (s, T)) = (s, unbit_and_unbox_type T) in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

690 
Refute.is_IDT_constructor thy x orelse is_record_constr x orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

691 
(is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

692 
x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

693 
is_coconstr thy x 
33192  694 
end 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

695 
fun is_stale_constr thy (x as (_, T)) = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

696 
is_codatatype thy (body_type T) andalso is_constr_like thy x andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

697 
not (is_coconstr thy x) 
33192  698 
fun is_constr thy (x as (_, T)) = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

699 
is_constr_like thy x andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

700 
not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

701 
not (is_stale_constr thy x) 
33192  702 
(* string > bool *) 
703 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

704 
val is_sel_like_and_no_discr = 

705 
String.isPrefix sel_prefix 

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

707 

708 
(* boxability > boxability *) 

709 
fun in_fun_lhs_for InConstr = InSel 

710 
 in_fun_lhs_for _ = InFunLHS 

711 
fun in_fun_rhs_for InConstr = InConstr 

712 
 in_fun_rhs_for InSel = InSel 

713 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

714 
 in_fun_rhs_for _ = InFunRHS1 

715 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

716 
(* hol_context > boxability > typ > bool *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

717 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  718 
case T of 
719 
Type ("fun", _) => 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

720 
(boxy = InPair orelse boxy = InFunLHS) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

721 
not (is_boolean_type (body_type T)) 
33192  722 
 Type ("*", Ts) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

723 
boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

724 
((boxy = InExpr orelse boxy = InFunLHS) andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

725 
exists (is_boxing_worth_it hol_ctxt InPair) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

726 
(map (box_type hol_ctxt InPair) Ts)) 
33192  727 
 _ => false 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

728 
(* hol_context > boxability > string * typ list > string *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

729 
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = 
33192  730 
case triple_lookup (type_match thy) boxes (Type z) of 
731 
SOME (SOME box_me) => box_me 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

732 
 _ => is_boxing_worth_it hol_ctxt boxy (Type z) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

733 
(* hol_context > boxability > typ > typ *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

734 
and box_type hol_ctxt boxy T = 
33192  735 
case T of 
736 
Type (z as ("fun", [T1, T2])) => 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

737 
if boxy <> InConstr andalso boxy <> InSel andalso 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

738 
should_box_type hol_ctxt boxy z then 
33192  739 
Type (@{type_name fun_box}, 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

740 
[box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2]) 
33192  741 
else 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

742 
box_type hol_ctxt (in_fun_lhs_for boxy) T1 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

743 
> box_type hol_ctxt (in_fun_rhs_for boxy) T2 
33192  744 
 Type (z as ("*", Ts)) => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

745 
if boxy <> InConstr andalso boxy <> InSel 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

746 
andalso should_box_type hol_ctxt boxy z then 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

747 
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) 
33192  748 
else 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

749 
Type ("*", map (box_type hol_ctxt 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

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

751 
else InPair)) Ts) 
33192  752 
 _ => T 
753 

754 
(* styp > styp *) 

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

756 

757 
(* typ > int *) 

758 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

759 
(* string > int > string *) 

760 
fun nth_sel_name_for_constr_name s n = 

761 
if s = @{const_name Pair} then 

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

763 
else 

764 
sel_prefix_for n ^ s 

765 
(* styp > int > styp *) 

766 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

767 
 nth_sel_for_constr (s, T) n = 

768 
(nth_sel_name_for_constr_name s n, 

769 
body_type T > nth (maybe_curried_binder_types T) n) 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

770 
(* hol_context > styp > int > styp *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

771 
fun boxed_nth_sel_for_constr hol_ctxt = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

772 
apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr 
33192  773 

774 
(* string > int *) 

775 
fun sel_no_from_name s = 

776 
if String.isPrefix discr_prefix s then 

777 
~1 

778 
else if String.isPrefix sel_prefix s then 

779 
s > unprefix sel_prefix > Int.fromString > the 

780 
else if s = @{const_name snd} then 

781 
1 

782 
else 

783 
0 

784 

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

786 
fun eta_expand _ t 0 = t 

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

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

789 
 eta_expand Ts t n = 

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

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

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

793 

794 
(* term > term *) 

795 
fun extensionalize t = 

796 
case t of 

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

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

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

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

801 
end 

802 
 _ => t 

803 

804 
(* typ > term list > term *) 

805 
fun distinctness_formula T = 

806 
all_distinct_unordered_pairs_of 

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

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

809 

810 
(* typ > term *) 

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

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

813 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

814 
(* hol_context > typ > styp list *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

815 
fun uncached_datatype_constrs ({thy, stds, ...} : hol_context) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

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

817 
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

818 
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs' 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

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

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

828 
> T)) constrs 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

829 
> (triple_lookup (type_match thy) stds T > the > not) ? 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

830 
cons (@{const_name NonStd}, @{typ \<xi>} > T) 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

838 
in [(s', T')] end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

839 
else if is_quot_type thy T then 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

840 
[(@{const_name Quot}, rep_type_for_quot_type thy T > T)] 
33581
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

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

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

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

851 
 uncached_datatype_constrs _ _ = [] 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

852 
(* hol_context > typ > styp list *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

853 
fun datatype_constrs (hol_ctxt as {constr_cache, ...}) 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

854 
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

855 
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

856 
 NONE => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

857 
let val xs = uncached_datatype_constrs hol_ctxt T in 
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

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

859 
end 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

860 
fun boxed_datatype_constrs hol_ctxt = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

861 
map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

862 
(* hol_context > typ > int *) 
33192  863 
val num_datatype_constrs = length oo datatype_constrs 
864 

865 
(* string > string *) 

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

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

868 
 constr_name_for_sel_like s' = original_name s' 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

869 
(* hol_context > styp > styp *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

870 
fun boxed_constr_for_sel hol_ctxt (s', T') = 
33192  871 
let val s = constr_name_for_sel_like s' in 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

872 
AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s 
33192  873 
> the > pair s 
874 
end 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

875 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

876 
(* hol_context > styp > term *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

877 
fun discr_term_for_constr hol_ctxt (x as (s, T)) = 
33192  878 
let val dataT = body_type T in 
879 
if s = @{const_name Suc} then 

880 
Abs (Name.uu, dataT, 

881 
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

882 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  883 
Const (discr_for_constr x) 
884 
else 

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

886 
end 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

887 
(* hol_context > styp > term > term *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

888 
fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t = 
33192  889 
case strip_comb t of 
890 
(Const x', args) => 

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

892 
else if is_constr_like thy x' then @{const False} 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

893 
else betapply (discr_term_for_constr hol_ctxt x, t) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

894 
 _ => betapply (discr_term_for_constr hol_ctxt x, t) 
33192  895 

896 
(* styp > term > term *) 

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

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

899 
if dataT = nat_T then 

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

901 
else if is_pair_type dataT then 

902 
Const (nth_sel_for_constr x n) 

903 
else 

904 
let 

905 
(* int > typ > int * term *) 

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

907 
let 

908 
val (m, t1) = aux m T1 

909 
val (m, t2) = aux m T2 

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

911 
 aux m T = 

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

913 
$ Bound 0) 

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

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

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

917 
end 

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

919 
fun select_nth_constr_arg thy x t n res_T = 

920 
case strip_comb t of 

921 
(Const x', args) => 

922 
if x = x' then nth args n 

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

924 
else betapply (nth_arg_sel_term_for_constr x n, t) 

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

926 

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

928 
fun construct_value _ x [] = Const x 

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

930 
let val args = map Envir.eta_contract args in 

931 
case hd args of 

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

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

933 
if is_sel_like_and_no_discr s' andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

934 
constr_name_for_sel_like s' = s andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

935 
forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t') 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

936 
(index_seq 0 (length args) ~~ args) then 
33192  937 
t 
938 
else 

939 
list_comb (Const x, args) 

940 
 _ => list_comb (Const x, args) 

941 
end 

942 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

943 
(* The higher this number is, the more nonstandard models can be generated. It's 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

944 
not important enough to be a user option, though. *) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

945 
val xi_card = 8 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

946 

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

948 
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

949 
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

950 
 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

951 
card_of_type assigns T1 * card_of_type assigns T2 
33192  952 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
953 
 card_of_type _ @{typ prop} = 2 

954 
 card_of_type _ @{typ bool} = 2 

955 
 card_of_type _ @{typ unit} = 1 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

956 
 card_of_type _ @{typ \<xi>} = xi_card 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

957 
 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

958 
case AList.lookup (op =) assigns T of 
33192  959 
SOME k => k 
960 
 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

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

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

965 
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

966 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  967 
in 
968 
if k1 = max orelse k2 = max then max 

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

970 
end 

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

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

973 
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

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

976 
 bounded_card_of_type max default_card assigns T = 
33192  977 
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

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

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

981 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
33192  982 
default_card) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

983 
(* hol_context > int > (typ * int) list > typ > int *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

984 
fun bounded_exact_card_of_type hol_ctxt max default_card assigns T = 
33192  985 
let 
986 
(* typ list > typ > int *) 

987 
fun aux avoid T = 

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

988 
(if member (op =) avoid T then 
33192  989 
0 
990 
else case T of 

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

992 
let 

993 
val k1 = aux avoid T1 

994 
val k2 = aux avoid T2 

995 
in 

996 
if k1 = 0 orelse k2 = 0 then 0 

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

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

999 
end 

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

1001 
let 

1002 
val k1 = aux avoid T1 

1003 
val k2 = aux avoid T2 

1004 
in 

1005 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1008 
end 

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

1010 
 @{typ prop} => 2 

1011 
 @{typ bool} => 2 

1012 
 @{typ unit} => 1 

35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

1013 
 @{typ \<xi>} => xi_card 
33192  1014 
 Type _ => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1015 
(case datatype_constrs hol_ctxt T of 
34126  1016 
[] => if is_integer_type T orelse is_bit_type T then 0 
1017 
else raise SAME () 

33192  1018 
 constrs => 
1019 
let 

1020 
val constr_cards = 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1021 
datatype_constrs hol_ctxt T 
33192  1022 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
1023 
o snd) 

1024 
in 

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

1025 
if exists (curry (op =) 0) constr_cards then 0 
33192  1026 
else Integer.sum constr_cards 
1027 
end) 

1028 
 _ => raise SAME ()) 

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

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

1030 
AList.lookup (op =) assigns T > the_default default_card 
33192  1031 
in Int.min (max, aux [] T) end 
1032 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1033 
(* hol_context > typ > bool *) 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1034 
fun is_finite_type hol_ctxt = 
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1035 
not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 [] 
33192  1036 

1037 
(* term > bool *) 

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

1039 
 is_ground_term (Const _) = true 

1040 
 is_ground_term _ = false 

1041 

1042 
(* term > word > word *) 

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

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

1045 
 hashw_term _ = 0w0 

1046 
(* term > int *) 

1047 
val hash_term = Word.toInt o hashw_term 

1048 

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

1050 
fun special_bounds ts = 

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

1052 

1053 
(* indexname * typ > term > term *) 

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

1055 

33571  1056 
(* theory > string > bool *) 
1057 
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

1058 
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"}, 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1059 
@{type_name int}] s orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1060 
is_frac_type thy (Type (s, [])) 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

1061 
(* theory > typ > bool *) 
33571  1062 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 
1063 
 is_funky_typedef _ _ = false 

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

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

1067 
 is_arity_type_axiom _ = false 

1068 
(* theory > bool > term > bool *) 

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

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

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

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

1073 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1074 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1075 
 is_typedef_axiom _ _ _ = false 
1076 

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

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

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

1080 
using "typedef_info". *) 

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

1082 
fun partition_axioms_by_definitionality thy axioms def_names = 

1083 
let 

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

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

1086 
val nondefs = 

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

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

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

1090 

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

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

1092 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1093 
commands. *) 
1094 
(* theory > bool *) 

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

1096 

1097 
(* term > bool *) 

1098 
val is_plain_definition = 

1099 
let 

1100 
(* term > bool *) 

1101 
fun do_lhs t1 = 

1102 
case strip_comb t1 of 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1103 
(Const _, args) => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1104 
forall is_Var args andalso not (has_duplicates (op =) args) 
33192  1105 
 _ => false 
1106 
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 

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

1108 
do_lhs t1 

1109 
 do_eq _ = false 

1110 
in do_eq end 

1111 

1112 
(* theory > term list * term list * term list *) 

1113 
fun all_axioms_of thy = 

1114 
let 

1115 
(* theory list > term list *) 

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

1117 
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

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

1119 
> OrdList.make fast_string_ord 
33192  1120 
val thys = thy :: Theory.ancestors_of thy 
1121 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1122 
val built_in_axioms = axioms_of_thys built_in_thys 

1123 
val user_axioms = axioms_of_thys user_thys 

1124 
val (built_in_defs, built_in_nondefs) = 

1125 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1126 
> filter (is_typedef_axiom thy false) 
33192  1127 
val (user_defs, user_nondefs) = 
1128 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

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

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

1136 
user_defs @ built_in_defs 
33192  1137 
in (defs, built_in_nondefs, user_nondefs) end 
1138 

1139 
(* bool > styp > int option *) 

1140 
fun arity_of_built_in_const fast_descrs (s, T) = 

1141 
if s = @{const_name If} then 

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

1143 
else case AList.lookup (op =) 

1144 
(built_in_consts 

1145 
> fast_descrs ? append built_in_descr_consts) s of 

1146 
SOME n => SOME n 

1147 
 NONE => 

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

1149 
SOME n => SOME n 

1150 
 NONE => 

1151 
if is_fun_type T andalso is_set_type (domain_type T) then 

1152 
AList.lookup (op =) built_in_set_consts s 

1153 
else 

1154 
NONE 

1155 
(* bool > styp > bool *) 

1156 
val is_built_in_const = is_some oo arity_of_built_in_const 

1157 

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

1159 
simplification rules (equational specifications). *) 

1160 
(* term > term *) 

1161 
fun term_under_def t = 

1162 
case t of 

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

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

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

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

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

1168 
 t1 $ _ => term_under_def t1 

1169 
 _ => t 

1170 

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

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

1173 
be matched in the face of overloading. *) 

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

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

1176 
if is_built_in_const fast_descrs x then 

1177 
[] 

1178 
else 

1179 
these (Symtab.lookup table s) 

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

1181 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1182 

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

1183 
(* theory > term > term option *) 
33192  1184 
fun normalized_rhs_of thy t = 
1185 
let 

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

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

1187 
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

1188 
 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

1189 
 aux _ _ = NONE 
33192  1190 
val (lhs, rhs) = 
1191 
case t of 

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

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

1194 
(t1, t2) 

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

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

1197 
in fold_rev aux args (SOME rhs) end 
33192  1198 

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

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

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

1202 
NONE 

1203 
else 

1204 
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

1205 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1206 
handle List.Empty => NONE 
1207 

1208 
(* term > fixpoint_kind *) 

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

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

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

1212 
 fixpoint_kind_of_rhs _ = NoFp 

1213 

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

1215 
fun is_mutually_inductive_pred_def thy table t = 

1216 
let 

1217 
(* term > bool *) 

1218 
fun is_good_arg (Bound _) = true 

1219 
 is_good_arg (Const (s, _)) = 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1220 
s = @{const_name True} orelse s = @{const_name False} orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1221 
s = @{const_name undefined} 
33192  1222 
 is_good_arg _ = false 
1223 
in 

1224 
case t > strip_abs_body > strip_comb of 

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

1226 
(case def_of_const thy table x of 

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

1228 
 NONE => false) 

1229 
 _ => false 

1230 
end 

1231 
(* theory > const_table > term > term *) 

1232 
fun unfold_mutually_inductive_preds thy table = 

1233 
map_aterms (fn t as Const x => 

1234 
(case def_of_const thy table x of 

1235 
SOME t' => 

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

1237 
if is_mutually_inductive_pred_def thy table t' then t' 

1238 
else t 

1239 
end 

1240 
 NONE => t) 

1241 
 t => t) 

1242 

1243 
(* term > string * term *) 

1244 
fun pair_for_prop t = 

1245 
case term_under_def t of 

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

1247 
 Free _ => raise NOT_SUPPORTED "local definitions" 

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

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

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

1251 
fun table_for get ctxt = 

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

1253 

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

1255 
fun case_const_names thy = 

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

1257 
if is_basic_datatype dtype_s then 

1258 
I 

1259 
else 

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

1261 
> the > #3 > length)) 

1262 
(Datatype.get_all thy) [] @ 

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

1263 
map (apsnd length o snd) (#codatatypes (Data.get thy)) 
33192  1264 

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

1266 
fun const_def_table ctxt ts = 

34126  1267 
table_for (map prop_of o Nitpick_Defs.get) ctxt 
33192  1268 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) 
1269 
(map pair_for_prop ts) 

1270 
(* term list > const_table *) 

1271 
fun const_nondef_table ts = 

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

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

1274 
(* Proof.context > const_table *) 

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

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

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

1278 
fun inductive_intro_table ctxt def_table = 

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

1280 
def_table o prop_of) 

1281 
o Nitpick_Intros.get) ctxt 

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

1283 
fun ground_theorem_table thy = 

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

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

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

1287 

1288 
val basic_ersatz_table = 

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

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

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

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

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

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

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

1296 

1297 
(* theory > (string * string) list *) 

1298 
fun ersatz_table thy = 

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

1299 
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table 
33192  1300 

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

1302 
fun add_simps simp_table s eqs = 

1303 
Unsynchronized.change simp_table 

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

1305 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1306 
(* theory > styp > term list *) 