author  blanchet 
Tue, 23 Feb 2010 11:05:32 +0100  
changeset 35311  8f9a66fc9f80 
parent 35309  997aa3a3e4bb 
child 35332  22442ab3e7a3 
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 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

68 
val unarize_and_unbox_type : typ > typ 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

69 
val unarize_unbox_and_uniterize_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 
33192  151 
val card_of_type : (typ * int) list > typ > int 
152 
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

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

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

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

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

157 
val is_funky_typedef : theory > typ > bool 
33192  158 
val all_axioms_of : theory > 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

159 
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

160 
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

161 
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

162 
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

163 
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

164 
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

165 
theory > (typ option * bool) list > (string * int) list 
33192  166 
val const_def_table : Proof.context > term list > const_table 
167 
val const_nondef_table : term list > const_table 

168 
val const_simp_table : Proof.context > const_table 

169 
val const_psimp_table : Proof.context > const_table 

170 
val inductive_intro_table : Proof.context > const_table > const_table 

171 
val ground_theorem_table : theory > term list Inttab.table 

172 
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

173 
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

174 
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

175 
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

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

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

180 
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

181 
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

182 
val is_equational_fun : hol_context > styp > bool 
33192  183 
val is_constr_pattern_lhs : theory > term > bool 
184 
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

185 
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

186 
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

187 
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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
val ground_types_in_terms : hol_context > bool > term list > typ list 
33192  194 
val format_type : int list > int list > typ > typ 
195 
val format_term_type : 

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

197 
val user_friendly_const : 

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

198 
hol_context > string * string > (term option * int list) list 
33192  199 
> styp > term * typ 
200 
val assign_operator_for_const : styp > string 

201 
end; 

202 

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

203 
structure Nitpick_HOL : NITPICK_HOL = 
33192  204 
struct 
205 

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

206 
open Nitpick_Util 
33192  207 

208 
type const_table = term list Symtab.table 

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

210 
type unrolled = styp * styp 

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

212 

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

213 
type hol_context = { 
33192  214 
thy: theory, 
215 
ctxt: Proof.context, 

216 
max_bisim_depth: int, 

217 
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

218 
stds: (typ option * bool) list, 
33192  219 
wfs: (styp option * bool option) list, 
220 
user_axioms: bool option, 

221 
debug: bool, 

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

222 
binary_ints: bool option, 
33192  223 
destroy_constrs: bool, 
224 
specialize: bool, 

225 
skolemize: bool, 

226 
star_linear_preds: bool, 

227 
uncurry: bool, 

228 
fast_descrs: bool, 

229 
tac_timeout: Time.time option, 

230 
evals: term list, 

231 
case_names: (string * int) list, 

232 
def_table: const_table, 

233 
nondef_table: const_table, 

234 
user_nondefs: term list, 

235 
simp_table: const_table Unsynchronized.ref, 

236 
psimp_table: const_table, 

237 
intro_table: const_table, 

238 
ground_thm_table: term list Inttab.table, 

239 
ersatz_table: (string * string) list, 

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

241 
special_funs: special_fun list Unsynchronized.ref, 

242 
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

243 
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

244 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  245 

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

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

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

248 
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

249 

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

250 
structure Data = Theory_Data( 
33192  251 
type T = {frac_types: (string * (string * string) list) list, 
252 
codatatypes: (string * (string * styp list)) list} 

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

254 
val extend = I 

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

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

258 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  259 

260 
val name_sep = "$" 

261 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

262 
val sel_prefix = nitpick_prefix ^ "sel" 

263 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

264 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

265 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

266 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

267 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

268 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

269 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

270 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

271 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

35311  272 
val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep 
33192  273 
val skolem_prefix = nitpick_prefix ^ "sk" 
274 
val special_prefix = nitpick_prefix ^ "sp" 

275 
val uncurry_prefix = nitpick_prefix ^ "unc" 

276 
val eval_prefix = nitpick_prefix ^ "eval" 

277 
val iter_var_prefix = "i" 

278 
val arg_var_prefix = "x" 

279 

280 
(* int > string *) 

281 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

35311  282 
(* Proof.context > typ > string *) 
283 
fun quot_normal_name_for_type ctxt T = 

284 
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) 

33192  285 

286 
(* string > string * string *) 

287 
val strip_first_name_sep = 

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

289 
#> pairself Substring.string 

290 
(* string > string *) 

291 
fun original_name s = 

292 
if String.isPrefix nitpick_prefix s then 

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

294 
else 

295 
s 

296 
val after_name_sep = snd o strip_first_name_sep 

297 

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

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

301 
 s_conj (t1, t2) = 

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

303 
else HOLogic.mk_conj (t1, t2) 

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

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

306 
 s_disj (t1, t2) = 

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

308 
else HOLogic.mk_disj (t1, t2) 

309 

310 
(* term > term > term list *) 

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

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

313 
 strip_connective _ t = [t] 

314 
(* term > term list * term *) 

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

315 
fun strip_any_connective (t as (t0 $ _ $ _)) = 
34998  316 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 
317 
(strip_connective t0 t, t0) 

318 
else 

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

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

321 
(* term > term list *) 

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

322 
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

323 
val disjuncts_of = strip_connective @{const "op "} 
34998  324 

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

326 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  327 
well. *) 
328 
val built_in_consts = 

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

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

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

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

333 
(@{const_name Trueprop}, 1), 

334 
(@{const_name Not}, 1), 

335 
(@{const_name False}, 0), 

336 
(@{const_name True}, 0), 

337 
(@{const_name All}, 1), 

338 
(@{const_name Ex}, 1), 

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

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

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

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

343 
(@{const_name If}, 3), 

344 
(@{const_name Let}, 2), 

345 
(@{const_name Unity}, 0), 

346 
(@{const_name Pair}, 2), 

347 
(@{const_name fst}, 1), 

348 
(@{const_name snd}, 1), 

349 
(@{const_name Id}, 0), 

350 
(@{const_name insert}, 2), 

351 
(@{const_name converse}, 1), 

352 
(@{const_name trancl}, 1), 

353 
(@{const_name rel_comp}, 2), 

354 
(@{const_name image}, 2), 

355 
(@{const_name finite}, 1), 

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

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

357 
(@{const_name is_unknown}, 1), 
33192  358 
(@{const_name Tha}, 1), 
359 
(@{const_name Frac}, 0), 

360 
(@{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

361 
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

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

363 
(@{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

364 
(@{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

365 
(@{const_name nat_lcm}, 0)] 
33192  366 
val built_in_descr_consts = 
367 
[(@{const_name The}, 1), 

368 
(@{const_name Eps}, 1)] 

369 
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

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

371 
((@{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

372 
((@{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

373 
((@{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

374 
((@{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

375 
((@{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

376 
((@{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

377 
((@{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

378 
((@{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

379 
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

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

381 
((@{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

382 
((@{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

383 
((@{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

384 
((@{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

385 
((@{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

386 
((@{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

387 
((@{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

388 
((@{const_name of_nat}, nat_T > int_T), 0)] 
33192  389 
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

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

391 
(@{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

392 
(@{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

393 
(@{const_name ord_class.less_eq}, 2)] 
33192  394 

395 
(* typ > typ *) 

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

396 
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

397 
 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

398 
 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

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

400 
fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

401 
unarize_and_unbox_type (Type ("fun", Ts)) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

402 
 unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

404 
 unarize_and_unbox_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

405 
 unarize_and_unbox_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

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

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

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

409 
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

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

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

412 
val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

413 

33192  414 
(* Proof.context > typ > string *) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

415 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type 
33192  416 

417 
(* string > string > string *) 

418 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

419 
(* string > string *) 

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

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

423 
(* string > string *) 

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

424 
fun short_name s = 
33192  425 
case space_explode name_sep s of 
426 
[_] => 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

427 
 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

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

429 
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

430 
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

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

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

434 
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

435 
#> map_types shorten_names_in_type 
33192  436 

437 
(* theory > typ * typ > bool *) 

438 
fun type_match thy (T1, T2) = 

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

440 
handle Type.TYPE_MATCH => false 

441 
(* theory > styp * styp > bool *) 

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

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

444 
(* theory > term * term > bool *) 

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

446 
 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

447 
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

448 
 term_match _ (t1, t2) = t1 aconv t2 
33192  449 

450 
(* typ > bool *) 

451 
fun is_TFree (TFree _) = true 

452 
 is_TFree _ = false 

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

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

455 
 is_higher_order_type _ = false 

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

457 
 is_fun_type _ = false 

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

459 
 is_set_type _ = false 

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

461 
 is_pair_type _ = false 

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

463 
 is_lfp_iterator_type _ = false 

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

465 
 is_gfp_iterator_type _ = false 

466 
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

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

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

469 
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

470 
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

471 
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

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

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

474 
val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type 
33192  475 
val is_record_type = not o null o Record.dest_recTs 
476 
(* theory > typ > bool *) 

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

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

478 
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s))) 
33192  479 
 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

480 
fun is_number_type thy = is_integer_like_type orf is_frac_type thy 
33192  481 

482 
(* bool > styp > typ *) 

483 
fun iterator_type_for_const gfp (s, T) = 

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

485 
binder_types T) 

486 
(* typ > styp *) 

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

488 
 const_for_iterator_type T = 

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

489 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  490 

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

491 
(* int > typ > typ list * typ *) 
33192  492 
fun strip_n_binders 0 T = ([], T) 
493 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

494 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

497 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  498 
(* typ > typ *) 
499 
val nth_range_type = snd oo strip_n_binders 

500 

501 
(* typ > int *) 

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

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

504 
 num_factors_in_type _ = 1 

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

506 
 num_binder_types _ = 0 

507 
(* typ > typ list *) 

508 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

509 
fun maybe_curried_binder_types T = 

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

511 

512 
(* typ > term list > term *) 

513 
fun mk_flat_tuple _ [t] = t 

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

515 
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

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

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

520 

521 
(* int > typ > typ list *) 

522 
fun dest_n_tuple_type 1 T = [T] 

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

524 
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

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

526 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  527 

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

528 
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

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

530 
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

531 
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

532 

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

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

534 
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

535 
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

536 
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

537 
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

538 
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

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

540 
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

541 
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

542 
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

543 
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

544 
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

545 
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

546 
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

547 
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

548 
 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

549 

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

551 
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

552 
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

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

554 
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

555 

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

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

557 
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

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

559 
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

560 
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

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

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

563 

33192  564 
(* theory > typ > typ > typ > typ *) 
565 
fun instantiate_type thy T1 T1' T2 = 

566 
Same.commit (Envir.subst_type_same 

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

569 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
35311  570 
fun varify_and_instantiate_type thy T1 T1' T2 = 
571 
instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) 

33192  572 

573 
(* theory > typ > typ > styp *) 

574 
fun repair_constr_type thy body_T' T = 

35311  575 
varify_and_instantiate_type thy (body_type T) body_T' T 
33192  576 

577 
(* string > (string * string) list > theory > theory *) 

578 
fun register_frac_type frac_s ersaetze thy = 

579 
let 

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

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

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

585 

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

587 
fun register_codatatype co_T case_name constr_xs thy = 

588 
let 

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

589 
val {frac_types, codatatypes} = Data.get thy 
33192  590 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
591 
val (co_s, co_Ts) = dest_Type co_T 

592 
val _ = 

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

593 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) 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

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

595 
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

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

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

598 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  599 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
600 
codatatypes 

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

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

604 

605 
(* theory > typ > bool *) 

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

606 
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

607 
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

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

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

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

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

614 
is_typedef thy s andalso 

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

615 
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

616 
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

617 
is_integer_like_type T) 
33192  618 
 is_pure_typedef _ _ = false 
619 
fun is_univ_typedef thy (Type (s, _)) = 

620 
(case typedef_info thy s of 

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

622 
(case set_def of 

623 
SOME thm => 

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

625 
 NONE => 

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

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

627 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top} 
33192  628 
 NONE => false) 
629 
 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

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

631 
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

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

633 
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

634 
 is_datatype _ _ _ = false 
33192  635 

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

637 
fun all_record_fields thy T = 

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

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

640 
end 

641 
handle TYPE _ => [] 

642 
(* styp > bool *) 

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

643 
fun is_record_constr (s, T) = 
33192  644 
String.isSuffix Record.extN s andalso 
645 
let val dataT = body_type T in 

646 
is_record_type dataT andalso 

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

648 
end 

649 
(* theory > typ > int *) 

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

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

652 
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

653 
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

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

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

657 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  658 
 is_record_get _ _ = false 
659 
fun is_record_update thy (s, T) = 

660 
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

661 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  662 
(all_record_fields thy (body_type T)) 
663 
handle TYPE _ => false 

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

665 
(case typedef_info thy s' of 

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

667 
 NONE => false) 

668 
 is_abs_fun _ _ = false 

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

670 
(case typedef_info thy s' of 

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

672 
 NONE => false) 

673 
 is_rep_fun _ _ = false 

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

674 
(* Proof.context > styp > bool *) 
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

675 
fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

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

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

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

679 
fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) = 
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35283
diff
changeset

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

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

682 
 is_quot_rep_fun _ _ = false 
33192  683 

684 
(* theory > styp > styp *) 

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

686 
(case typedef_info thy s' of 

687 
SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1])) 

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

688 
 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

689 
 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

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

691 
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

692 
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

693 
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

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

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

696 
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

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

698 
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

699 
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

700 
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

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

702 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  703 

704 
(* theory > styp > bool *) 

705 
fun is_coconstr thy (s, T) = 

706 
let 

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

707 
val {codatatypes, ...} = Data.get thy 
33192  708 
val co_T = body_type T 
709 
val co_s = dest_Type co_T > fst 

710 
in 

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

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

713 
end 

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

715 
fun is_constr_like thy (s, T) = 

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

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

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

718 
@{const_name Suc_Rep}] s orelse 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

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

720 
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

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

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

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

725 
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

726 
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

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

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

729 
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

730 
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

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

732 
not (is_stale_constr thy x) 
33192  733 
(* string > bool *) 
734 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

735 
val is_sel_like_and_no_discr = 

736 
String.isPrefix sel_prefix 

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

738 

739 
(* boxability > boxability *) 

740 
fun in_fun_lhs_for InConstr = InSel 

741 
 in_fun_lhs_for _ = InFunLHS 

742 
fun in_fun_rhs_for InConstr = InConstr 

743 
 in_fun_rhs_for InSel = InSel 

744 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

745 
 in_fun_rhs_for _ = InFunRHS1 

746 

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

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

748 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  749 
case T of 
750 
Type ("fun", _) => 

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

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

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

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

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

756 
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

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

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

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

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

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

765 
and box_type hol_ctxt boxy T = 
33192  766 
case T of 
767 
Type (z as ("fun", [T1, T2])) => 

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

768 
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

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

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

773 
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

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

776 
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

777 
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

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

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

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

782 
else InPair)) Ts) 
33192  783 
 _ => T 
784 

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

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

786 
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

787 
 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

788 
 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

789 
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

790 
 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

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

792 
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

793 

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

796 

797 
(* typ > int *) 

798 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

799 
(* string > int > string *) 

800 
fun nth_sel_name_for_constr_name s n = 

801 
if s = @{const_name Pair} then 

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

803 
else 

804 
sel_prefix_for n ^ s 

805 
(* styp > int > styp *) 

806 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

807 
 nth_sel_for_constr (s, T) n = 

808 
(nth_sel_name_for_constr_name s n, 

809 
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

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

811 
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

812 
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

813 
oo nth_sel_for_constr 
33192  814 

815 
(* string > int *) 

816 
fun sel_no_from_name s = 

817 
if String.isPrefix discr_prefix s then 

818 
~1 

819 
else if String.isPrefix sel_prefix s then 

820 
s > unprefix sel_prefix > Int.fromString > the 

821 
else if s = @{const_name snd} then 

822 
1 

823 
else 

824 
0 

825 

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

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

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

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

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

830 
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

831 
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

832 
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

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

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

835 
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

836 
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

837 
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

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

839 
 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

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

841 

33192  842 
(* typ list > term > int > term *) 
843 
fun eta_expand _ t 0 = t 

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

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

846 
 eta_expand Ts t n = 

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

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

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

850 

851 
(* term > term *) 

852 
fun extensionalize t = 

853 
case t of 

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

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

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

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

858 
end 

859 
 _ => t 

860 

861 
(* typ > term list > term *) 

862 
fun distinctness_formula T = 

863 
all_distinct_unordered_pairs_of 

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

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

866 

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

868 
fun zero_const T = Const (@{const_name zero_class.zero}, T) 
33192  869 
fun suc_const T = Const (@{const_name Suc}, T > T) 
870 

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

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

872 
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

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

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

875 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

897 
SOME {abs_type, rep_type, Abs_name, ...} => 
35311  898 
[(Abs_name, 
899 
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

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

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

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

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

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

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

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

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

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

909 
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

910 
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

911 
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

912 
 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

913 
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

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

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

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

917 
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

918 
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

919 
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

920 
(* hol_context > typ > int *) 
33192  921 
val num_datatype_constrs = length oo datatype_constrs 
922 

923 
(* string > string *) 

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

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

926 
 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

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

928 
fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') = 
33192  929 
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

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

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

932 
s 
33192  933 
> the > pair s 
934 
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

935 

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

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

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

940 
Abs (Name.uu, dataT, 

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

942 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  943 
Const (discr_for_constr x) 
944 
else 

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

946 
end 

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

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

948 
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

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

950 
Const x' => 
33192  951 
if x = x' then @{const True} 
952 
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

953 
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

954 
 _ => betapply (discr_term_for_constr hol_ctxt x, t) 
33192  955 

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

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

957 
fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n = 
33192  958 
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

959 
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

960 
@{term "%n::nat. n  1"} 
33192  961 
else if is_pair_type dataT then 
962 
Const (nth_sel_for_constr x n) 

963 
else 

964 
let 

965 
(* int > typ > int * term *) 

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

967 
let 

968 
val (m, t1) = aux m T1 

969 
val (m, t2) = aux m T2 

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

971 
 aux m T = 

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

973 
$ Bound 0) 

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

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

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

977 
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

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

979 
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

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

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

982 
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

983 
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

984 
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

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

986 
handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) 
33192  987 

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

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

989 
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

990 
 construct_value thy stds (x as (s, _)) args = 
33192  991 
let val args = map Envir.eta_contract args in 
992 
case hd args of 

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

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

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

995 
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

996 
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

997 
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

998 
(index_seq 0 (length args) ~~ args) then 
33192  999 
t 
1000 
else 

1001 
list_comb (Const x, args) 

1002 
 _ => list_comb (Const x, args) 

1003 
end 

1004 

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

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

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

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

1009 
card_of_type assigns T1 * card_of_type assigns T2 
33192  1010 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
1011 
 card_of_type _ @{typ prop} = 2 

1012 
 card_of_type _ @{typ bool} = 2 

1013 
 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

1014 
 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

1015 
case AList.lookup (op =) assigns T of 
33192  1016 
SOME k => k 
1017 
 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

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

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

1022 
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

1023 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  1024 
in 
1025 
if k1 = max orelse k2 = max then max 

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

1027 
end 

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

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

1030 
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

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

1033 
 bounded_card_of_type max default_card assigns T = 
33192  1034 
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

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

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

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

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

1041 
fun bounded_exact_card_of_type hol_ctxt max default_card assigns T = 
33192  1042 
let 
1043 
(* typ list > typ > int *) 

1044 
fun aux avoid T = 

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

1045 
(if member (op =) avoid T then 
33192  1046 
0 
1047 
else case T of 

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

1049 
let 

1050 
val k1 = aux avoid T1 

1051 
val k2 = aux avoid T2 

1052 
in 

1053 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1056 
end 

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

1058 
let 

1059 
val k1 = aux avoid T1 

1060 
val k2 = aux avoid T2 

1061 
in 

1062 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1065 
end 

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

1067 
 @{typ prop} => 2 

1068 
 @{typ bool} => 2 

1069 
 @{typ unit} => 1 

1070 
 Type _ => 

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

1071 
(case datatype_constrs hol_ctxt T of 
34126  1072 
[] => if is_integer_type T orelse is_bit_type T then 0 
1073 
else raise SAME () 

33192  1074 
 constrs => 
1075 
let 

1076 
val constr_cards = 

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

1077 
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

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

1080 
if exists (curry (op =) 0) constr_cards then 0 
33192  1081 
else Integer.sum constr_cards 
1082 
end) 

1083 
 _ => raise SAME ()) 

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

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

1085 
AList.lookup (op =) assigns T > the_default default_card 
33192  1086 
in Int.min (max, aux [] T) end 
1087 

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

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

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

1090 
not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 [] 
33192  1091 

1092 
(* term > bool *) 

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

1094 
 is_ground_term (Const _) = true 

1095 
 is_ground_term _ = false 

1096 

1097 
(* term > word > word *) 

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

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

1100 
 hashw_term _ = 0w0 

1101 
(* term > int *) 

1102 
val hash_term = Word.toInt o hashw_term 

1103 

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

1105 
fun special_bounds ts = 

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

1107 

1108 
(* indexname * typ > term > term *) 

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

1110 

33571  1111 
(* theory > string > bool *) 
1112 
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

1113 
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

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

1115 
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

1116 
(* theory > typ > bool *) 
33571  1117 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 
1118 
 is_funky_typedef _ _ = false 

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

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

1122 
 is_arity_type_axiom _ = false 

1123 
(* theory > bool > term > bool *) 

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

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

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

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

1128 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1129 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1130 
 is_typedef_axiom _ _ _ = false 
1131 

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

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

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

1135 
using "typedef_info". *) 

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

1137 
fun partition_axioms_by_definitionality thy axioms def_names = 

1138 
let 

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

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

1141 
val nondefs = 

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

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

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

1145 

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

1146 
(* Ideally we would check against "Complex_Main", not "Refute", but any theory 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1147 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1148 
commands. *) 
1149 
(* theory > bool *) 

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

1151 

1152 
(* term > bool *) 

35283
7ae51d5ea05d
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
blanchet
parents:
35280
diff
changeset

1153 
val is_trivial_definition = 
7ae51d5ea05d
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
blanchet
parents:
35280
diff
changeset

1154 
the_default false o try (op aconv o Logic.dest_equals) 
33192  1155 
val is_plain_definition = 
1156 
let 

1157 
(* term > bool *) 

1158 
fun do_lhs t1 = 

1159 
case strip_comb t1 of 

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

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

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

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

1165 
do_lhs t1 

1166 
 do_eq _ = false 

1167 
in do_eq end 

1168 

1169 
(* theory > term list * term list * term list *) 

1170 
fun all_axioms_of thy = 

1171 
let 

1172 
(* theory list > term list *) 

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

1174 
val specs = Defs.all_specifications_of (Theory.defs_of thy) 

33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33699
diff
changeset

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

1176 
> OrdList.make fast_string_ord 
33192  1177 
val thys = thy :: Theory.ancestors_of thy 
1178 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1179 
val built_in_axioms = axioms_of_thys built_in_thys 

1180 
val user_axioms = axioms_of_thys user_thys 

1181 
val (built_in_defs, built_in_nondefs) = 

1182 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1183 
> filter (is_typedef_axiom thy false) 
33192  1184 
val (user_defs, user_nondefs) = 
1185 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

1191 
> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) 
35283
7ae51d5ea05d
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
blanchet
parents:
35280
diff
changeset

1192 
> map (prop_of o snd) 
7ae51d5ea05d
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
blanchet
parents:
35280
diff
changeset

1193 
> filter_out is_trivial_definition 
7ae51d5ea05d
filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
blanchet
parents:
35280
diff
changeset

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

1195 
user_defs @ built_in_defs 
33192  1196 
in (defs, built_in_nondefs, user_nondefs) end 
1197 

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

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

1199 
fun arity_of_built_in_const thy stds fast_descrs (s, T) = 
33192  1200 
if s = @{const_name If} then 
1201 
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3 

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

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

1203 
let val std_nats = is_standard_datatype thy stds nat_T in 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1204 
case AList.lookup (op =) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1205 
(built_in_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

1206 
> std_nats ? append 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

1207 
> fast_descrs ? append built_in_descr_consts) 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

1208 
SOME n => SOME 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

1209 
 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

1210 
case AList.lookup (op =) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1211 
(built_in_typed_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

1212 
> std_nats ? append 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

1213 
(s, unarize_type 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

1214 
SOME n => SOME 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

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

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

1217 
@{const_name zero_class.zero} => 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1218 
if is_iterator_type T then SOME 0 else NONE 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1219 
 @{const_name Suc} => 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1220 
if is_iterator_type (domain_type T) then SOME 0 else NONE 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1221 
 _ => if is_fun_type T andalso is_set_type (domain_type T) then 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1222 
AList.lookup (op =) built_in_set_consts s 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

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

1224 
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

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

1226 
(* theory > (typ option * bool) list > bool > 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

1227 
val is_built_in_const = is_some oooo arity_of_built_in_const 
33192  1228 

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

1230 
simplification rules (equational specifications). *) 

1231 
(* term > term *) 

1232 
fun term_under_def t = 

1233 
case t of 

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

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

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

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

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

1239 
 t1 $ _ => term_under_def t1 

1240 
 _ => t 

1241 

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

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

1244 
be matched in the face of overloading. *) 

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

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

1246 
> term 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

1247 
fun def_props_for_const thy stds fast_descrs table (x as (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

1248 
if is_built_in_const thy stds fast_descrs x then 
33192  1249 
[] 
1250 
else 

1251 
these (Symtab.lookup table s) 

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

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

1253 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1254 

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

1255 
(* term > term option *) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1256 
fun normalized_rhs_of t = 
33192  1257 
let 
33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

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

1259 
fun aux (v as Var _) (SOME t) = SOME (lambda v t) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1260 
 aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t) 
33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1261 
 aux _ _ = NONE 
33192  1262 
val (lhs, rhs) = 
