author  blanchet 
Tue, 09 Mar 2010 09:25:23 +0100  
changeset 35665  ff2bf50505ab 
parent 35625  9c818cab0dd0 
child 35671  ed2c3830d881 
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 
35311  57 
val quot_normal_prefix : string 
33192  58 
val skolem_prefix : string 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

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

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

34998  63 
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

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

65 
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

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

67 
val disjuncts_of : term > term list 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

68 
val unarize_unbox_etc_type : typ > typ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

69 
val uniterize_unarize_unbox_etc_type : typ > typ 
33192  70 
val string_for_type : Proof.context > typ > string 
71 
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

72 
val shortest_name : string > string 
33192  73 
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

74 
val shorten_names_in_term : term > term 
33192  75 
val type_match : theory > typ * typ > bool 
76 
val const_match : theory > styp * styp > bool 

77 
val term_match : theory > term * term > bool 

78 
val is_TFree : typ > bool 

79 
val is_higher_order_type : typ > bool 

80 
val is_fun_type : typ > bool 

81 
val is_set_type : typ > bool 

82 
val is_pair_type : typ > bool 

83 
val is_lfp_iterator_type : typ > bool 

84 
val is_gfp_iterator_type : typ > bool 

85 
val is_fp_iterator_type : typ > bool 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

86 
val is_iterator_type : typ > bool 
33192  87 
val is_boolean_type : typ > bool 
88 
val is_integer_type : typ > bool 

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

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

90 
val is_word_type : typ > bool 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

91 
val is_integer_like_type : typ > bool 
33192  92 
val is_record_type : typ > bool 
93 
val is_number_type : theory > typ > bool 

94 
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

95 
val strip_n_binders : int > typ > typ list * typ 
33192  96 
val nth_range_type : int > typ > typ 
97 
val num_factors_in_type : typ > int 

98 
val num_binder_types : typ > int 

99 
val curried_binder_types : typ > typ list 

100 
val mk_flat_tuple : typ > term list > term 

101 
val dest_n_tuple : int > term > term list 

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

102 
val is_real_datatype : theory > string > bool 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

103 
val is_standard_datatype : theory > (typ option * bool) list > typ > bool 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

104 
val is_quot_type : theory > typ > bool 
33192  105 
val is_codatatype : theory > typ > bool 
106 
val is_pure_typedef : theory > typ > bool 

107 
val is_univ_typedef : theory > typ > bool 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

108 
val is_datatype : theory > (typ option * bool) list > typ > bool 
33192  109 
val is_record_constr : styp > bool 
110 
val is_record_get : theory > styp > bool 

111 
val is_record_update : theory > styp > bool 

112 
val is_abs_fun : theory > styp > bool 

113 
val is_rep_fun : theory > styp > bool 

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

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

115 
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

116 
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

117 
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

118 
val is_stale_constr : theory > styp > bool 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

119 
val is_constr : theory > (typ option * bool) list > styp > bool 
33192  120 
val is_sel : string > bool 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

121 
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

122 
val box_type : hol_context > boxability > typ > typ 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

123 
val binarize_nat_and_int_in_type : typ > typ 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

124 
val binarize_nat_and_int_in_term : term > term 
33192  125 
val discr_for_constr : styp > styp 
126 
val num_sels_for_constr_type : typ > int 

127 
val nth_sel_name_for_constr_name : string > int > string 

128 
val nth_sel_for_constr : styp > int > styp 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

129 
val binarized_and_boxed_nth_sel_for_constr : 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

130 
hol_context > bool > styp > int > styp 
33192  131 
val sel_no_from_name : string > int 
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

132 
val close_form : term > term 
33192  133 
val eta_expand : typ list > term > int > term 
134 
val extensionalize : term > term 

135 
val distinctness_formula : typ > term list > term 

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

137 
val unregister_frac_type : string > theory > theory 

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

139 
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

140 
val datatype_constrs : hol_context > typ > styp list 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

141 
val binarized_and_boxed_datatype_constrs : 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

143 
val num_datatype_constrs : hol_context > typ > int 
33192  144 
val constr_name_for_sel_like : string > string 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

146 
val discriminate_value : hol_context > styp > term > term 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

147 
val select_nth_constr_arg : 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

148 
theory > (typ option * bool) list > styp > term > int > typ > term 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

149 
val construct_value : 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

150 
theory > (typ option * bool) list > styp > term list > term 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

151 
val coerce_term : hol_context > typ list > typ > typ > term > term 
33192  152 
val card_of_type : (typ * int) list > typ > int 
153 
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

154 
val bounded_exact_card_of_type : 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

156 
val is_finite_type : hol_context > typ > bool 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

158 
val special_bounds : term list > (indexname * typ) list 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

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

160 
val is_funky_typedef : theory > typ > bool 
35335  161 
val all_axioms_of : 
162 
theory > (term * term) list > term list * term list * term list 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

163 
val arity_of_built_in_const : 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

164 
theory > (typ option * bool) list > bool > styp > int option 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

165 
val is_built_in_const : 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

167 
val term_under_def : term > term 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

168 
val case_const_names : 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

169 
theory > (typ option * bool) list > (string * int) list 
35335  170 
val const_def_table : 
171 
Proof.context > (term * term) list > term list > const_table 

33192  172 
val const_nondef_table : term list > const_table 
35335  173 
val const_simp_table : Proof.context > (term * term) list > const_table 
174 
val const_psimp_table : Proof.context > (term * term) list > const_table 

175 
val inductive_intro_table : 

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

33192  177 
val ground_theorem_table : theory > term list Inttab.table 
178 
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

179 
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

180 
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

181 
val optimized_typedef_axioms : theory > string * typ list > term list 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

182 
val optimized_quot_type_axioms : 
35311  183 
Proof.context > (typ option * bool) list > string * typ list > term list 
33192  184 
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

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

186 
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

187 
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

188 
val is_equational_fun : hol_context > styp > bool 
33192  189 
val is_constr_pattern_lhs : theory > term > bool 
190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

196 
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

197 
val merge_type_vars_in_terms : term list > term list 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

198 
val ground_types_in_type : hol_context > bool > typ > typ list 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

199 
val ground_types_in_terms : hol_context > bool > term list > typ list 
33192  200 
val format_type : int list > int list > typ > typ 
201 
val format_term_type : 

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

203 
val user_friendly_const : 

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

204 
hol_context > string * string > (term option * int list) list 
33192  205 
> styp > term * typ 
206 
val assign_operator_for_const : styp > string 

207 
end; 

208 

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

209 
structure Nitpick_HOL : NITPICK_HOL = 
33192  210 
struct 
211 

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

212 
open Nitpick_Util 
33192  213 

214 
type const_table = term list Symtab.table 

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

216 
type unrolled = styp * styp 

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

218 

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

219 
type hol_context = { 
33192  220 
thy: theory, 
221 
ctxt: Proof.context, 

222 
max_bisim_depth: int, 

223 
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

224 
stds: (typ option * bool) list, 
33192  225 
wfs: (styp option * bool option) list, 
226 
user_axioms: bool option, 

227 
debug: bool, 

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

228 
binary_ints: bool option, 
33192  229 
destroy_constrs: bool, 
230 
specialize: bool, 

231 
skolemize: bool, 

232 
star_linear_preds: bool, 

233 
uncurry: bool, 

234 
fast_descrs: bool, 

235 
tac_timeout: Time.time option, 

236 
evals: term list, 

237 
case_names: (string * int) list, 

238 
def_table: const_table, 

239 
nondef_table: const_table, 

240 
user_nondefs: term list, 

241 
simp_table: const_table Unsynchronized.ref, 

242 
psimp_table: const_table, 

243 
intro_table: const_table, 

244 
ground_thm_table: term list Inttab.table, 

245 
ersatz_table: (string * string) list, 

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

247 
special_funs: special_fun list Unsynchronized.ref, 

248 
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

249 
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

250 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  251 

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

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

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

254 
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

255 

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

256 
structure Data = Theory_Data( 
33192  257 
type T = {frac_types: (string * (string * string) list) list, 
258 
codatatypes: (string * (string * styp list)) list} 

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

260 
val extend = I 

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

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

264 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  265 

266 
val name_sep = "$" 

267 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

268 
val sel_prefix = nitpick_prefix ^ "sel" 

269 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

270 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

271 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

272 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

273 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

274 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

275 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

276 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

277 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

35311  278 
val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep 
33192  279 
val skolem_prefix = nitpick_prefix ^ "sk" 
280 
val special_prefix = nitpick_prefix ^ "sp" 

281 
val uncurry_prefix = nitpick_prefix ^ "unc" 

282 
val eval_prefix = nitpick_prefix ^ "eval" 

283 
val iter_var_prefix = "i" 

284 
val arg_var_prefix = "x" 

285 

286 
(* int > string *) 

287 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

35311  288 
(* Proof.context > typ > string *) 
289 
fun quot_normal_name_for_type ctxt T = 

290 
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) 

33192  291 

292 
(* string > string * string *) 

293 
val strip_first_name_sep = 

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

295 
#> pairself Substring.string 

296 
(* string > string *) 

297 
fun original_name s = 

298 
if String.isPrefix nitpick_prefix s then 

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

300 
else 

301 
s 

302 
val after_name_sep = snd o strip_first_name_sep 

303 

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

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

307 
 s_conj (t1, t2) = 

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

309 
else HOLogic.mk_conj (t1, t2) 

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

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

312 
 s_disj (t1, t2) = 

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

314 
else HOLogic.mk_disj (t1, t2) 

315 

316 
(* term > term > term list *) 

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

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

319 
 strip_connective _ t = [t] 

320 
(* term > term list * term *) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

321 
fun strip_any_connective (t as (t0 $ _ $ _)) = 
34998  322 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 
323 
(strip_connective t0 t, t0) 

324 
else 

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

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

327 
(* term > term list *) 

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

328 
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

329 
val disjuncts_of = strip_connective @{const "op "} 
34998  330 

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

332 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  333 
well. *) 
334 
val built_in_consts = 

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

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

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

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

339 
(@{const_name Trueprop}, 1), 

340 
(@{const_name Not}, 1), 

341 
(@{const_name False}, 0), 

342 
(@{const_name True}, 0), 

343 
(@{const_name All}, 1), 

344 
(@{const_name Ex}, 1), 

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

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

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

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

349 
(@{const_name If}, 3), 

350 
(@{const_name Let}, 2), 

351 
(@{const_name Unity}, 0), 

352 
(@{const_name Pair}, 2), 

353 
(@{const_name fst}, 1), 

354 
(@{const_name snd}, 1), 

355 
(@{const_name Id}, 0), 

356 
(@{const_name insert}, 2), 

357 
(@{const_name converse}, 1), 

358 
(@{const_name trancl}, 1), 

359 
(@{const_name rel_comp}, 2), 

360 
(@{const_name image}, 2), 

361 
(@{const_name finite}, 1), 

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

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

363 
(@{const_name is_unknown}, 1), 
33192  364 
(@{const_name Tha}, 1), 
365 
(@{const_name Frac}, 0), 

366 
(@{const_name norm_frac}, 0)] 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

367 
val built_in_nat_consts = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

368 
[(@{const_name Suc}, 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

369 
(@{const_name nat}, 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

370 
(@{const_name nat_gcd}, 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

371 
(@{const_name nat_lcm}, 0)] 
33192  372 
val built_in_descr_consts = 
373 
[(@{const_name The}, 1), 

374 
(@{const_name Eps}, 1)] 

375 
val built_in_typed_consts = 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

376 
[((@{const_name zero_class.zero}, int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

377 
((@{const_name one_class.one}, int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

378 
((@{const_name plus_class.plus}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

379 
((@{const_name minus_class.minus}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

380 
((@{const_name times_class.times}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

381 
((@{const_name div_class.div}, int_T > int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

382 
((@{const_name uminus_class.uminus}, int_T > int_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

383 
((@{const_name ord_class.less}, int_T > int_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

384 
((@{const_name ord_class.less_eq}, int_T > int_T > bool_T), 2)] 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

385 
val built_in_typed_nat_consts = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

386 
[((@{const_name zero_class.zero}, nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

387 
((@{const_name one_class.one}, nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

388 
((@{const_name plus_class.plus}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

389 
((@{const_name minus_class.minus}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

390 
((@{const_name times_class.times}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

391 
((@{const_name div_class.div}, nat_T > nat_T > nat_T), 0), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

392 
((@{const_name ord_class.less}, nat_T > nat_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

393 
((@{const_name ord_class.less_eq}, nat_T > nat_T > bool_T), 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

394 
((@{const_name of_nat}, nat_T > int_T), 0)] 
33192  395 
val built_in_set_consts = 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

396 
[(@{const_name semilattice_inf_class.inf}, 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

397 
(@{const_name semilattice_sup_class.sup}, 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

398 
(@{const_name minus_class.minus}, 2), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

399 
(@{const_name ord_class.less_eq}, 2)] 
33192  400 

401 
(* typ > typ *) 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

402 
fun unarize_type @{typ "unsigned_bit word"} = nat_T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

403 
 unarize_type @{typ "signed_bit word"} = int_T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

404 
 unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

405 
 unarize_type T = T 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

406 
fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

407 
unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

408 
 unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

409 
unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

410 
 unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

411 
Type (@{type_name "*"}, map unarize_unbox_etc_type Ts) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

412 
 unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

413 
 unarize_unbox_etc_type @{typ "signed_bit word"} = int_T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

414 
 unarize_unbox_etc_type (Type (s, Ts as _ :: _)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

415 
Type (s, map unarize_unbox_etc_type Ts) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

416 
 unarize_unbox_etc_type T = T 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

417 
fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

418 
 uniterize_type @{typ bisim_iterator} = nat_T 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

419 
 uniterize_type T = T 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

420 
val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

421 

33192  422 
(* Proof.context > typ > string *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

423 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type 
33192  424 

425 
(* string > string > string *) 

426 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

427 
(* string > string *) 

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

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

431 
(* string > string *) 

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

432 
fun short_name s = 
33192  433 
case space_explode name_sep s of 
434 
[_] => 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

435 
 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

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

437 
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

438 
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

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

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

442 
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

443 
#> map_types shorten_names_in_type 
33192  444 

445 
(* theory > typ * typ > bool *) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

446 
fun strict_type_match thy (T1, T2) = 
33192  447 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 
448 
handle Type.TYPE_MATCH => false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

449 
fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type 
33192  450 
(* theory > styp * styp > bool *) 
451 
fun const_match thy ((s1, T1), (s2, T2)) = 

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

453 
(* theory > term * term > bool *) 

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

455 
 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

456 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

457 
 term_match _ (t1, t2) = t1 aconv t2 
33192  458 

459 
(* typ > bool *) 

460 
fun is_TFree (TFree _) = true 

461 
 is_TFree _ = false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

462 
fun is_higher_order_type (Type (@{type_name fun}, _)) = true 
33192  463 
 is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts 
464 
 is_higher_order_type _ = false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

465 
fun is_fun_type (Type (@{type_name fun}, _)) = true 
33192  466 
 is_fun_type _ = false 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

467 
fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true 
33192  468 
 is_set_type _ = false 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

469 
fun is_pair_type (Type (@{type_name "*"}, _)) = true 
33192  470 
 is_pair_type _ = false 
471 
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s 

472 
 is_lfp_iterator_type _ = false 

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

474 
 is_gfp_iterator_type _ = false 

475 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

476 
fun is_iterator_type T = 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

477 
(T = @{typ bisim_iterator} orelse is_fp_iterator_type T) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

478 
fun is_boolean_type T = (T = prop_T orelse T = bool_T) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

479 
fun is_integer_type T = (T = nat_T orelse T = int_T) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

480 
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

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

482 
 is_word_type _ = false 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

483 
val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type 
33192  484 
val is_record_type = not o null o Record.dest_recTs 
485 
(* theory > typ > bool *) 

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

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

487 
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) 
33192  488 
 is_frac_type _ _ = false 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

489 
fun is_number_type thy = is_integer_like_type orf is_frac_type thy 
33192  490 

491 
(* bool > styp > typ *) 

492 
fun iterator_type_for_const gfp (s, T) = 

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

494 
binder_types T) 

495 
(* typ > styp *) 

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

497 
 const_for_iterator_type T = 

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

498 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  499 

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

500 
(* int > typ > typ list * typ *) 
33192  501 
fun strip_n_binders 0 T = ([], T) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

502 
 strip_n_binders n (Type (@{type_name fun}, [T1, T2])) = 
33192  503 
strip_n_binders (n  1) T2 >> cons T1 
504 
 strip_n_binders n (Type (@{type_name fun_box}, Ts)) = 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

505 
strip_n_binders n (Type (@{type_name fun}, Ts)) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

506 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  507 
(* typ > typ *) 
508 
val nth_range_type = snd oo strip_n_binders 

509 

510 
(* typ > int *) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

511 
fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) = 
33192  512 
fold (Integer.add o num_factors_in_type) [T1, T2] 0 
513 
 num_factors_in_type _ = 1 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

514 
fun num_binder_types (Type (@{type_name fun}, [_, T2])) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

515 
1 + num_binder_types T2 
33192  516 
 num_binder_types _ = 0 
517 
(* typ > typ list *) 

518 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

519 
fun maybe_curried_binder_types T = 

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

521 

522 
(* typ > term list > term *) 

523 
fun mk_flat_tuple _ [t] = t 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

524 
 mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) = 
33192  525 
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

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

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

530 

531 
(* int > typ > typ list *) 

532 
fun dest_n_tuple_type 1 T = [T] 

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

534 
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

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

536 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  537 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

538 
type typedef_info = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

539 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

540 
set_def: thm option, prop_of_Rep: thm, set_name: string, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

541 
Abs_inverse: thm option, Rep_inverse: thm option} 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

542 

2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

543 
(* theory > string > typedef_info *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

544 
fun typedef_info thy s = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

545 
if is_frac_type thy (Type (s, [])) then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

546 
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

547 
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

548 
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"} 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

549 
> Logic.varify, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

550 
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE} 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

551 
else case Typedef.get_info thy s of 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

552 
SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

553 
Rep_inverse, ...} => 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

554 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

555 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

556 
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

557 
Rep_inverse = SOME Rep_inverse} 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

558 
 NONE => NONE 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

559 

2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

560 
(* theory > string > bool *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

561 
val is_typedef = is_some oo typedef_info 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

562 
val is_real_datatype = is_some oo Datatype.get_info 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

563 
(* theory > (typ option * bool) list > typ > bool *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

564 
fun is_standard_datatype thy = the oo triple_lookup (type_match thy) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

565 

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

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

567 
e.g., by adding a field to "Datatype_Aux.info". *) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

568 
(* theory > (typ option * bool) list > string > bool *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

569 
fun is_basic_datatype thy stds s = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

570 
member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit}, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

571 
@{type_name int}, "Code_Numeral.code_numeral"] s orelse 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

572 
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

573 

33192  574 
(* theory > typ > typ > typ > typ *) 
575 
fun instantiate_type thy T1 T1' T2 = 

576 
Same.commit (Envir.subst_type_same 

35311  577 
(Sign.typ_match thy (T1, T1') Vartab.empty)) T2 
33192  578 
handle Type.TYPE_MATCH => 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

579 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
35311  580 
fun varify_and_instantiate_type thy T1 T1' T2 = 
581 
instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) 

33192  582 

583 
(* theory > typ > typ > styp *) 

584 
fun repair_constr_type thy body_T' T = 

35311  585 
varify_and_instantiate_type thy (body_type T) body_T' T 
33192  586 

587 
(* string > (string * string) list > theory > theory *) 

588 
fun register_frac_type frac_s ersaetze thy = 

589 
let 

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

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

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

595 

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

597 
fun register_codatatype co_T case_name constr_xs thy = 

598 
let 

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

599 
val {frac_types, codatatypes} = Data.get thy 
33192  600 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
601 
val (co_s, co_Ts) = dest_Type co_T 

602 
val _ = 

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

603 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

604 
co_s <> @{type_name fun} andalso 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

605 
not (is_basic_datatype thy [(NONE, true)] co_s) then 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

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

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

608 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  609 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
610 
codatatypes 

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

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

614 

615 
(* theory > typ > bool *) 

35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

616 
fun is_quot_type thy (Type (s, _)) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

617 
is_some (Quotient_Info.quotdata_lookup_raw thy s) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

618 
 is_quot_type _ _ = false 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

619 
fun is_codatatype thy (Type (s, _)) = 
33583
b5e0909cd5ea
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet
diff
changeset

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

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

624 
is_typedef thy s andalso 

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

625 
not (is_real_datatype thy s orelse is_quot_type thy T orelse 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

626 
is_codatatype thy T orelse is_record_type T orelse 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

627 
is_integer_like_type T) 
33192  628 
 is_pure_typedef _ _ = false 
629 
fun is_univ_typedef thy (Type (s, _)) = 

630 
(case typedef_info thy s of 

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

35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

632 
let 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

633 
val t_opt = 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

634 
case set_def of 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

635 
SOME thm => try (snd o Logic.dest_equals o prop_of) thm 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

636 
 NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

637 
prop_of_Rep 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

638 
in 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

639 
case t_opt of 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

640 
SOME (Const (@{const_name top}, _)) => true 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

641 
(* "Multiset.multiset" *) 
35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

642 
 SOME (Const (@{const_name Collect}, _) 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

643 
$ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

644 
(* "FinFun.finfun" *) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

645 
 SOME (Const (@{const_name Collect}, _) $ Abs (_, _, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

646 
Const (@{const_name Ex}, _) $ Abs (_, _, 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

647 
Const (@{const_name finite}, _) $ _))) => true 
35332
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

648 
 _ => false 
22442ab3e7a3
optimized multisets in Nitpick by fishing "finite"
blanchet
parents:
35311
diff
changeset

649 
end 
33192  650 
 NONE => false) 
651 
 is_univ_typedef _ _ = false 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

652 
(* theory > (typ option * bool) list > typ > bool *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

654 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

655 
is_quot_type thy T) andalso not (is_basic_datatype thy stds s) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

656 
 is_datatype _ _ _ = false 
33192  657 

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

659 
fun all_record_fields thy T = 

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

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

662 
end 

663 
handle TYPE _ => [] 

664 
(* styp > bool *) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

665 
fun is_record_constr (s, T) = 
33192  666 
String.isSuffix Record.extN s andalso 
667 
let val dataT = body_type T in 

668 
is_record_type dataT andalso 

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

670 
end 

671 
(* theory > typ > int *) 

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

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

674 
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

675 
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

676 
(Record.get_extT_fields thy T1 > single > op @) 
33192  677 
(* theory > styp > bool *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

678 
fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) = 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

679 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  680 
 is_record_get _ _ = false 
681 
fun is_record_update thy (s, T) = 

682 
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

683 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  684 
(all_record_fields thy (body_type T)) 
685 
handle TYPE _ => false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

686 
fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) = 
33192  687 
(case typedef_info thy s' of 
688 
SOME {Abs_name, ...} => s = Abs_name 

689 
 NONE => false) 

690 
 is_abs_fun _ _ = false 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

691 
fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) = 
33192  692 
(case typedef_info thy s' of 
693 
SOME {Rep_name, ...} => s = Rep_name 

694 
 NONE => false) 

695 
 is_rep_fun _ _ = false 

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

696 
(* Proof.context > styp > bool *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

697 
fun is_quot_abs_fun ctxt 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

698 
(x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) = 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

699 
(try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s' 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

700 
= SOME (Const x)) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

701 
 is_quot_abs_fun _ _ = false 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

702 
fun is_quot_rep_fun ctxt 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

703 
(x as (_, Type (@{type_name fun}, [Type (s', _), _]))) = 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

704 
(try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s' 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

705 
= SOME (Const x)) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

706 
 is_quot_rep_fun _ _ = false 
33192  707 

708 
(* theory > styp > styp *) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

709 
fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun}, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

710 
[T1 as Type (s', _), T2]))) = 
33192  711 
(case typedef_info thy s' of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

712 
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1])) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

713 
 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

714 
 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

715 
(* theory > typ > typ *) 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

716 
fun rep_type_for_quot_type thy (T as Type (s, _)) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

717 
let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

718 
instantiate_type thy qtyp T rtyp 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

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

720 
(* theory > typ > term *) 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

721 
fun equiv_relation_for_quot_type thy (Type (s, Ts)) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

722 
let 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

723 
val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

724 
val Ts' = qtyp > dest_Type > snd 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

725 
in subst_atomic_types (Ts' ~~ Ts) equiv_rel end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

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

727 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  728 

729 
(* theory > styp > bool *) 

730 
fun is_coconstr thy (s, T) = 

731 
let 

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

732 
val {codatatypes, ...} = Data.get thy 
33192  733 
val co_T = body_type T 
734 
val co_s = dest_Type co_T > fst 

735 
in 

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

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

738 
end 

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

740 
fun is_constr_like thy (s, T) = 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

741 
member (op =) [@{const_name FinFun}, @{const_name FunBox}, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

742 
@{const_name PairBox}, @{const_name Quot}, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

743 
@{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

745 
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

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

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

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

750 
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

751 
not (is_coconstr thy x) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

752 
(* theory > (typ option * bool) list > styp > bool *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

754 
is_constr_like thy x andalso 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

755 
not (is_basic_datatype thy stds 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

756 
(fst (dest_Type (unarize_type (body_type T))))) andalso 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

757 
not (is_stale_constr thy x) 
33192  758 
(* string > bool *) 
759 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

760 
val is_sel_like_and_no_discr = 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

761 
String.isPrefix sel_prefix orf 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

762 
(member (op =) [@{const_name fst}, @{const_name snd}]) 
33192  763 

764 
(* boxability > boxability *) 

765 
fun in_fun_lhs_for InConstr = InSel 

766 
 in_fun_lhs_for _ = InFunLHS 

767 
fun in_fun_rhs_for InConstr = InConstr 

768 
 in_fun_rhs_for InSel = InSel 

769 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

770 
 in_fun_rhs_for _ = InFunRHS1 

771 

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

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

773 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  774 
case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

775 
Type (@{type_name fun}, _) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

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

777 
not (is_boolean_type (body_type T)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

778 
 Type (@{type_name "*"}, Ts) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

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

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

781 
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

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

784 
(* hol_context > boxability > string * typ list > string *) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

785 
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z = 
33192  786 
case triple_lookup (type_match thy) boxes (Type z) of 
787 
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

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

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

790 
and box_type hol_ctxt boxy T = 
33192  791 
case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

792 
Type (z as (@{type_name fun}, [T1, T2])) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

793 
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

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

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

798 
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

799 
> box_type hol_ctxt (in_fun_rhs_for boxy) T2 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

800 
 Type (z as (@{type_name "*"}, 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

801 
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

802 
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

803 
Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts) 
33192  804 
else 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

805 
Type (@{type_name "*"}, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

806 
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

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

808 
else InPair)) Ts) 
33192  809 
 _ => T 
810 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

811 
(* typ > typ *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

812 
fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"} 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

813 
 binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"} 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

814 
 binarize_nat_and_int_in_type (Type (s, Ts)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

815 
Type (s, map binarize_nat_and_int_in_type Ts) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

816 
 binarize_nat_and_int_in_type T = T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

817 
(* term > term *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

818 
val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

819 

33192  820 
(* styp > styp *) 
821 
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T > bool_T) 

822 

823 
(* typ > int *) 

824 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

825 
(* string > int > string *) 

826 
fun nth_sel_name_for_constr_name s n = 

827 
if s = @{const_name Pair} then 

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

829 
else 

830 
sel_prefix_for n ^ s 

831 
(* styp > int > styp *) 

832 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

833 
 nth_sel_for_constr (s, T) n = 

834 
(nth_sel_name_for_constr_name s n, 

835 
body_type T > nth (maybe_curried_binder_types T) n) 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

836 
(* hol_context > bool > styp > int > styp *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

837 
fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

838 
apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

839 
oo nth_sel_for_constr 
33192  840 

841 
(* string > int *) 

842 
fun sel_no_from_name s = 

843 
if String.isPrefix discr_prefix s then 

844 
~1 

845 
else if String.isPrefix sel_prefix s then 

846 
s > unprefix sel_prefix > Int.fromString > the 

847 
else if s = @{const_name snd} then 

848 
1 

849 
else 

850 
0 

851 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

852 
(* term > term *) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

853 
val close_form = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

854 
let 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

855 
(* (indexname * typ) list > (indexname * typ) list > term > term *) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

856 
fun close_up zs zs' = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

857 
fold (fn (z as ((s, _), T)) => fn t' => 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

858 
Term.all T $ Abs (s, T, abstract_over (Var z, t'))) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

859 
(take (length zs'  length zs) zs') 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

860 
(* (indexname * typ) list > term > term *) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

861 
fun aux zs (@{const "==>"} $ t1 $ t2) = 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

862 
let val zs' = Term.add_vars t1 zs in 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

863 
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2)) 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

864 
end 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

865 
 aux zs t = close_up zs (Term.add_vars t zs) t 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

866 
in aux [] end 
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35075
diff
changeset

867 

33192  868 
(* typ list > term > int > term *) 
869 
fun eta_expand _ t 0 = t 

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

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

872 
 eta_expand Ts t n = 

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

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

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

876 

877 
(* term > term *) 

878 
fun extensionalize t = 

879 
case t of 

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

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

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

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

884 
end 

885 
 _ => t 

886 

887 
(* typ > term list > term *) 

888 
fun distinctness_formula T = 

889 
all_distinct_unordered_pairs_of 

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

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

892 

893 
(* typ > term *) 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

894 
fun zero_const T = Const (@{const_name zero_class.zero}, T) 
33192  895 
fun suc_const T = Const (@{const_name Suc}, T > T) 
896 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

897 
(* hol_context > typ > styp list *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

898 
fun uncached_datatype_constrs ({thy, stds, ...} : hol_context) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

901 
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

902 
 _ => 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

921 
[(@{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

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

923 
SOME {abs_type, rep_type, Abs_name, ...} => 
35311  924 
[(Abs_name, 
925 
varify_and_instantiate_type thy abs_type T rep_type > T)] 

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

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

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

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

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

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

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

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

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

934 
(* hol_context > typ > styp list *) 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

935 
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

936 
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

937 
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

938 
 NONE => 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

939 
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

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

941 
end 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

942 
(* hol_context > bool > typ > styp list *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

943 
fun binarized_and_boxed_datatype_constrs hol_ctxt binarize = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

944 
map (apsnd ((binarize ? binarize_nat_and_int_in_type) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

946 
(* hol_context > typ > int *) 
33192  947 
val num_datatype_constrs = length oo datatype_constrs 
948 

949 
(* string > string *) 

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

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

952 
 constr_name_for_sel_like s' = original_name s' 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

953 
(* hol_context > bool > styp > styp *) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

954 
fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') = 
33192  955 
let val s = constr_name_for_sel_like s' in 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

956 
AList.lookup (op =) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

957 
(binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T')) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

958 
s 
33192  959 
> the > pair s 
960 
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

961 

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

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

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

966 
Abs (Name.uu, dataT, 

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

968 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  969 
Const (discr_for_constr x) 
970 
else 

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

972 
end 

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

973 
(* hol_context > styp > term > term *) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

974 
fun discriminate_value (hol_ctxt as {thy, ...}) x t = 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

975 
case head_of t of 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

976 
Const x' => 
33192  977 
if x = x' then @{const True} 
978 
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

979 
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

980 
 _ => betapply (discr_term_for_constr hol_ctxt x, t) 
33192  981 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

982 
(* theory > (typ option * bool) list > styp > term > term *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

983 
fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n = 
33192  984 
let val (arg_Ts, dataT) = strip_type T in 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

985 
if dataT = nat_T andalso is_standard_datatype thy stds nat_T then 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

986 
@{term "%n::nat. n  1"} 
33192  987 
else if is_pair_type dataT then 
988 
Const (nth_sel_for_constr x n) 

989 
else 

990 
let 

991 
(* int > typ > int * term *) 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

992 
fun aux m (Type (@{type_name "*"}, [T1, T2])) = 
33192  993 
let 
994 
val (m, t1) = aux m T1 

995 
val (m, t2) = aux m T2 

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

997 
 aux m T = 

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

999 
$ Bound 0) 

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

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

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

1003 
end 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1004 
(* theory > (typ option * bool) list > styp > term > int > typ > term *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1005 
fun select_nth_constr_arg thy stds x t n res_T = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1006 
(case strip_comb t of 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1007 
(Const x', args) => 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1008 
if x = x' then nth args n 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1009 
else if is_constr_like thy x' then Const (@{const_name unknown}, res_T) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1010 
else raise SAME () 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1011 
 _ => raise SAME()) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1012 
handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) 
33192  1013 

35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1014 
(* theory > (typ option * bool) list > styp > term list > term *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1015 
fun construct_value _ _ x [] = Const x 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1016 
 construct_value thy stds (x as (s, _)) args = 
33192  1017 
let val args = map Envir.eta_contract args in 
1018 
case hd args of 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

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

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

1021 
constr_name_for_sel_like s' = s andalso 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1022 
forall (fn (n, t') => 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1023 
select_nth_constr_arg thy stds x t n dummyT = t') 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1024 
(index_seq 0 (length args) ~~ args) then 
33192  1025 
t 
1026 
else 

1027 
list_comb (Const x, args) 

1028 
 _ => list_comb (Const x, args) 

1029 
end 

1030 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1031 
(* hol_context > typ > term > term *) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1032 
fun constr_expand (hol_ctxt as {thy, stds, ...}) T t = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1033 
(case head_of t of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1034 
Const x => if is_constr_like thy x then t else raise SAME () 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1035 
 _ => raise SAME ()) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1036 
handle SAME () => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1037 
let 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1038 
val x' as (_, T') = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1039 
if is_pair_type T then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1040 
let val (T1, T2) = HOLogic.dest_prodT T in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1041 
(@{const_name Pair}, T1 > T2 > T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1042 
end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1043 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1044 
datatype_constrs hol_ctxt T > hd 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1045 
val arg_Ts = binder_types T' 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1046 
in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1047 
list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1048 
(index_seq 0 (length arg_Ts)) arg_Ts) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1049 
end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1050 

ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1051 
(* (term > term) > int > term > term *) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1052 
fun coerce_bound_no f j t = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1053 
case t of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1054 
t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1055 
 Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1056 
 Bound j' => if j' = j then f t else t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1057 
 _ => t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1058 
(* hol_context > typ > typ > term > term *) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1059 
fun coerce_bound_0_in_term hol_ctxt new_T old_T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1060 
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1061 
(* hol_context > typ list > typ > typ > term > term *) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1062 
and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1063 
if old_T = new_T then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1064 
t 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1065 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1066 
case (new_T, old_T) of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1067 
(Type (new_s, new_Ts as [new_T1, new_T2]), 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1068 
Type (@{type_name fun}, [old_T1, old_T2])) => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1069 
(case eta_expand Ts t 1 of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1070 
Abs (s, _, t') => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1071 
Abs (s, new_T1, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1072 
t' > coerce_bound_0_in_term hol_ctxt new_T1 old_T1 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1073 
> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1074 
> Envir.eta_contract 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1075 
> new_s <> @{type_name fun} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1076 
? construct_value thy stds 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1077 
(if new_s = @{type_name fin_fun} then @{const_name FinFun} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1078 
else @{const_name FunBox}, 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1079 
Type (@{type_name fun}, new_Ts) > new_T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1080 
o single 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1081 
 t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1082 
 (Type (new_s, new_Ts as [new_T1, new_T2]), 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1083 
Type (old_s, old_Ts as [old_T1, old_T2])) => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1084 
if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1085 
old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1086 
case constr_expand hol_ctxt old_T t of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1087 
Const (old_s, _) $ t1 => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1088 
if new_s = @{type_name fun} then 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1089 
coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1090 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1091 
construct_value thy stds 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1092 
(old_s, Type (@{type_name fun}, new_Ts) > new_T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1093 
[coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1094 
(Type (@{type_name fun}, old_Ts)) t1] 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1095 
 Const _ $ t1 $ t2 => 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1096 
construct_value thy stds 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1097 
(if new_s = @{type_name "*"} then @{const_name Pair} 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1098 
else @{const_name PairBox}, new_Ts > new_T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1099 
(map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2] 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1100 
[t1, t2]) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1101 
 t' => raise TERM ("Nitpick_HOL.coerce_term", [t']) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1102 
else 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1103 
raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1104 
 _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t]) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1105 

33192  1106 
(* (typ * int) list > typ > int *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

1108 
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

1110 
card_of_type assigns T1 * card_of_type assigns T2 
33192  1111 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
1112 
 card_of_type _ @{typ prop} = 2 

1113 
 card_of_type _ @{typ bool} = 2 

1114 
 card_of_type _ @{typ unit} = 1 

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

1115 
 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

1116 
case AList.lookup (op =) assigns T of 
33192  1117 
SOME k => k 
1118 
 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

1119 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
33192  1120 
(* int > (typ * int) list > typ > int *) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1121 
fun bounded_card_of_type max default_card assigns 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1122 
(Type (@{type_name fun}, [T1, T2])) = 
33192  1123 
let 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

1124 
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

1125 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  1126 
in 
1127 
if k1 = max orelse k2 = max then max 

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

1129 
end 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1130 
 bounded_card_of_type max default_card assigns 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1131 
(Type (@{type_name "*"}, [T1, T2])) = 
33192  1132 
let 
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

1133 
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

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

1136 
 bounded_card_of_type max default_card assigns T = 
33192  1137 
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

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

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

1141 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
33192  1142 
default_card) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1143 
(* hol_context > typ list > int > (typ * int) list > typ > int *) 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1144 
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1145 
assigns T = 
33192  1146 
let 
1147 
(* typ list > typ > int *) 

1148 
fun aux avoid T = 

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

1149 
(if member (op =) avoid T then 
33192  1150 
0 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1151 
else if member (op =) finitizable_dataTs T then 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1152 
raise SAME () 
33192  1153 
else case T of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1154 
Type (@{type_name fun}, [T1, T2]) => 
33192  1155 
let 
1156 
val k1 = aux avoid T1 

1157 
val k2 = aux avoid T2 

1158 
in 

1159 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1162 
end 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1163 
 Type (@{type_name "*"}, [T1, T2]) => 
33192  1164 
let 
1165 
val k1 = aux avoid T1 

1166 
val k2 = aux avoid T2 

1167 
in 

1168 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1171 
end 

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

1173 
 @{typ prop} => 2 

1174 
 @{typ bool} => 2 

1175 
 @{typ unit} => 1 

1176 
 Type _ => 

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

1177 
(case datatype_constrs hol_ctxt T of 
34126  1178 
[] => if is_integer_type T orelse is_bit_type T then 0 
1179 
else raise SAME () 

33192  1180 
 constrs => 
1181 
let 

1182 
val constr_cards = 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1183 
map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

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

1186 
if exists (curry (op =) 0) constr_cards then 0 
33192  1187 
else Integer.sum constr_cards 
1188 
end) 

1189 
 _ => raise SAME ()) 

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

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

1191 
AList.lookup (op =) assigns T > the_default default_card 
33192  1192 
in Int.min (max, aux [] T) end 
1193 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1194 
val small_type_max_card = 5 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1195 

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

1196 
(* hol_context > typ > bool *) 
35384  1197 
fun is_finite_type hol_ctxt T = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1198 
bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1199 
(* hol_context > typ > bool *) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1200 
fun is_small_finite_type hol_ctxt T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1201 
let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1202 
n > 0 andalso n <= small_type_max_card 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

1203 
end 
33192  1204 

1205 
(* term > bool *) 

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

1207 
 is_ground_term (Const _) = true 

1208 
 is_ground_term _ = false 

1209 

1210 
(* term > word > word *) 

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

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

1213 
 hashw_term _ = 0w0 

1214 
(* term > int *) 

1215 
val hash_term = Word.toInt o hashw_term 

1216 

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

1218 
fun special_bounds ts = 

35408  1219 
fold Term.add_vars ts [] > sort (Term_Ord.fast_indexname_ord o pairself fst) 
33192  1220 

1221 
(* indexname * typ > term > term *) 

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

1223 

33571  1224 
(* theory > string > bool *) 
1225 
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

1226 
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

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

1228 
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

1229 
(* theory > typ > bool *) 
33571  1230 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 
1231 
 is_funky_typedef _ _ = false 

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

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

1235 
 is_arity_type_axiom _ = false 

1236 
(* theory > bool > term > bool *) 

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

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

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

1239 
 is_typedef_axiom thy boring 
33192  1240 
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove 