author  blanchet 
Thu, 25 Feb 2010 16:33:39 +0100  
changeset 35385  29f81babefd7 
parent 35384  88dbcfe75c45 
child 35386  45a4e19d3ebd 
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 : 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

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

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 
35335  158 
val all_axioms_of : 
159 
theory > (term * term) list > term list * term list * term list 

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

160 
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

161 
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

162 
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

163 
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

164 
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

165 
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

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

33192  169 
val const_nondef_table : term list > const_table 
35335  170 
val const_simp_table : Proof.context > (term * term) list > const_table 
171 
val const_psimp_table : Proof.context > (term * term) list > const_table 

172 
val inductive_intro_table : 

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

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

176 
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

177 
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

178 
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

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

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

183 
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

184 
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

185 
val is_equational_fun : hol_context > styp > bool 
33192  186 
val is_constr_pattern_lhs : theory > term > bool 
187 
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

188 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

196 
val ground_types_in_terms : hol_context > bool > term list > typ list 
33192  197 
val format_type : int list > int list > typ > typ 
198 
val format_term_type : 

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

200 
val user_friendly_const : 

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

201 
hol_context > string * string > (term option * int list) list 
33192  202 
> styp > term * typ 
203 
val assign_operator_for_const : styp > string 

204 
end; 

205 

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

206 
structure Nitpick_HOL : NITPICK_HOL = 
33192  207 
struct 
208 

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

209 
open Nitpick_Util 
33192  210 

211 
type const_table = term list Symtab.table 

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

213 
type unrolled = styp * styp 

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

215 

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

216 
type hol_context = { 
33192  217 
thy: theory, 
218 
ctxt: Proof.context, 

219 
max_bisim_depth: int, 

220 
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

221 
stds: (typ option * bool) list, 
33192  222 
wfs: (styp option * bool option) list, 
223 
user_axioms: bool option, 

224 
debug: bool, 

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

225 
binary_ints: bool option, 
33192  226 
destroy_constrs: bool, 
227 
specialize: bool, 

228 
skolemize: bool, 

229 
star_linear_preds: bool, 

230 
uncurry: bool, 

231 
fast_descrs: bool, 

232 
tac_timeout: Time.time option, 

233 
evals: term list, 

234 
case_names: (string * int) list, 

235 
def_table: const_table, 

236 
nondef_table: const_table, 

237 
user_nondefs: term list, 

238 
simp_table: const_table Unsynchronized.ref, 

239 
psimp_table: const_table, 

240 
intro_table: const_table, 

241 
ground_thm_table: term list Inttab.table, 

242 
ersatz_table: (string * string) list, 

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

244 
special_funs: special_fun list Unsynchronized.ref, 

245 
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

246 
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

247 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  248 

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

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

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

251 
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

252 

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

253 
structure Data = Theory_Data( 
33192  254 
type T = {frac_types: (string * (string * string) list) list, 
255 
codatatypes: (string * (string * styp list)) list} 

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

257 
val extend = I 

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

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

261 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  262 

263 
val name_sep = "$" 

264 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

265 
val sel_prefix = nitpick_prefix ^ "sel" 

266 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

267 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

268 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

269 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

270 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

271 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

272 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

273 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

274 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

35311  275 
val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep 
33192  276 
val skolem_prefix = nitpick_prefix ^ "sk" 
277 
val special_prefix = nitpick_prefix ^ "sp" 

278 
val uncurry_prefix = nitpick_prefix ^ "unc" 

279 
val eval_prefix = nitpick_prefix ^ "eval" 

280 
val iter_var_prefix = "i" 

281 
val arg_var_prefix = "x" 

282 

283 
(* int > string *) 

284 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

35311  285 
(* Proof.context > typ > string *) 
286 
fun quot_normal_name_for_type ctxt T = 

287 
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T) 

33192  288 

289 
(* string > string * string *) 

290 
val strip_first_name_sep = 

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

292 
#> pairself Substring.string 

293 
(* string > string *) 

294 
fun original_name s = 

295 
if String.isPrefix nitpick_prefix s then 

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

297 
else 

298 
s 

299 
val after_name_sep = snd o strip_first_name_sep 

300 

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

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

304 
 s_conj (t1, t2) = 

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

306 
else HOLogic.mk_conj (t1, t2) 

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

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

309 
 s_disj (t1, t2) = 

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

311 
else HOLogic.mk_disj (t1, t2) 

312 

313 
(* term > term > term list *) 

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

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

316 
 strip_connective _ t = [t] 

317 
(* term > term list * term *) 

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

318 
fun strip_any_connective (t as (t0 $ _ $ _)) = 
34998  319 
if t0 = @{const "op &"} orelse t0 = @{const "op "} then 
320 
(strip_connective t0 t, t0) 

321 
else 

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

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

324 
(* term > term list *) 

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

325 
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

326 
val disjuncts_of = strip_connective @{const "op "} 
34998  327 

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

329 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  330 
well. *) 
331 
val built_in_consts = 

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

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

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

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

336 
(@{const_name Trueprop}, 1), 

337 
(@{const_name Not}, 1), 

338 
(@{const_name False}, 0), 

339 
(@{const_name True}, 0), 

340 
(@{const_name All}, 1), 

341 
(@{const_name Ex}, 1), 

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

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

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

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

346 
(@{const_name If}, 3), 

347 
(@{const_name Let}, 2), 

348 
(@{const_name Unity}, 0), 

349 
(@{const_name Pair}, 2), 

350 
(@{const_name fst}, 1), 

351 
(@{const_name snd}, 1), 

352 
(@{const_name Id}, 0), 

353 
(@{const_name insert}, 2), 

354 
(@{const_name converse}, 1), 

355 
(@{const_name trancl}, 1), 

356 
(@{const_name rel_comp}, 2), 

357 
(@{const_name image}, 2), 

358 
(@{const_name finite}, 1), 

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

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

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

363 
(@{const_name norm_frac}, 0)] 

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

364 
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

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

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

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

368 
(@{const_name nat_lcm}, 0)] 
33192  369 
val built_in_descr_consts = 
370 
[(@{const_name The}, 1), 

371 
(@{const_name Eps}, 1)] 

372 
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

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

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

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

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

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

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

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

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

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

382 
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

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

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

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

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

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

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

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

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

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

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

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

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

396 
(@{const_name ord_class.less_eq}, 2)] 
33192  397 

398 
(* typ > typ *) 

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

399 
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

400 
 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

401 
 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

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

403 
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

404 
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

405 
 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

406 
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

407 
 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

408 
 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

409 
 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

410 
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

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

412 
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

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

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

415 
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

416 

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

418 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type 
33192  419 

420 
(* string > string > string *) 

421 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

422 
(* string > string *) 

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

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

426 
(* string > string *) 

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

427 
fun short_name s = 
33192  428 
case space_explode name_sep s of 
429 
[_] => 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

430 
 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

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

432 
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

433 
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

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

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

437 
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

438 
#> map_types shorten_names_in_type 
33192  439 

440 
(* theory > typ * typ > bool *) 

441 
fun type_match thy (T1, T2) = 

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

443 
handle Type.TYPE_MATCH => false 

444 
(* theory > styp * styp > bool *) 

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

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

447 
(* theory > term * term > bool *) 

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

449 
 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

450 
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

451 
 term_match _ (t1, t2) = t1 aconv t2 
33192  452 

453 
(* typ > bool *) 

454 
fun is_TFree (TFree _) = true 

455 
 is_TFree _ = false 

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

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

458 
 is_higher_order_type _ = false 

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

460 
 is_fun_type _ = false 

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

462 
 is_set_type _ = false 

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

464 
 is_pair_type _ = false 

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

466 
 is_lfp_iterator_type _ = false 

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

468 
 is_gfp_iterator_type _ = false 

469 
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

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

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

472 
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

473 
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

474 
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

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

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

477 
val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type 
33192  478 
val is_record_type = not o null o Record.dest_recTs 
479 
(* theory > typ > bool *) 

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

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

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

483 
fun is_number_type thy = is_integer_like_type orf is_frac_type thy 
33192  484 

485 
(* bool > styp > typ *) 

486 
fun iterator_type_for_const gfp (s, T) = 

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

488 
binder_types T) 

489 
(* typ > styp *) 

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

491 
 const_for_iterator_type T = 

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

492 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  493 

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

494 
(* int > typ > typ list * typ *) 
33192  495 
fun strip_n_binders 0 T = ([], T) 
496 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

497 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

500 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  501 
(* typ > typ *) 
502 
val nth_range_type = snd oo strip_n_binders 

503 

504 
(* typ > int *) 

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

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

507 
 num_factors_in_type _ = 1 

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

509 
 num_binder_types _ = 0 

510 
(* typ > typ list *) 

511 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

512 
fun maybe_curried_binder_types T = 

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

514 

515 
(* typ > term list > term *) 

516 
fun mk_flat_tuple _ [t] = t 

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

518 
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

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

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

523 

524 
(* int > typ > typ list *) 

525 
fun dest_n_tuple_type 1 T = [T] 

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

527 
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

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

529 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  530 

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

531 
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

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

533 
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

534 
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

535 

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

537 
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

538 
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

539 
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

540 
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

541 
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

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

543 
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

544 
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

545 
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

546 
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

547 
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

548 
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

549 
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

550 
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

551 
 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

552 

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

554 
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

555 
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

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

557 
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

558 

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

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

560 
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

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

562 
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

563 
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

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

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

566 

33192  567 
(* theory > typ > typ > typ > typ *) 
568 
fun instantiate_type thy T1 T1' T2 = 

569 
Same.commit (Envir.subst_type_same 

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

572 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
35311  573 
fun varify_and_instantiate_type thy T1 T1' T2 = 
574 
instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2) 

33192  575 

576 
(* theory > typ > typ > styp *) 

577 
fun repair_constr_type thy body_T' T = 

35311  578 
varify_and_instantiate_type thy (body_type T) body_T' T 
33192  579 

580 
(* string > (string * string) list > theory > theory *) 

581 
fun register_frac_type frac_s ersaetze thy = 

582 
let 

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

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

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

588 

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

590 
fun register_codatatype co_T case_name constr_xs thy = 

591 
let 

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

592 
val {frac_types, codatatypes} = Data.get thy 
33192  593 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
594 
val (co_s, co_Ts) = dest_Type co_T 

595 
val _ = 

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

596 
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

597 
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

598 
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

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

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

601 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  602 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
603 
codatatypes 

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

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

607 

608 
(* theory > typ > bool *) 

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

609 
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

610 
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

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

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

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

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

617 
is_typedef thy s andalso 

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

618 
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

619 
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

620 
is_integer_like_type T) 
33192  621 
 is_pure_typedef _ _ = false 
622 
fun is_univ_typedef thy (Type (s, _)) = 

623 
(case typedef_info thy s of 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

637 
end 
33192  638 
 NONE => false) 
639 
 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

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

641 
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

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

643 
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

644 
 is_datatype _ _ _ = false 
33192  645 

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

647 
fun all_record_fields thy T = 

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

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

650 
end 

651 
handle TYPE _ => [] 

652 
(* styp > bool *) 

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

653 
fun is_record_constr (s, T) = 
33192  654 
String.isSuffix Record.extN s andalso 
655 
let val dataT = body_type T in 

656 
is_record_type dataT andalso 

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

658 
end 

659 
(* theory > typ > int *) 

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

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

662 
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

663 
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

664 
(Record.get_extT_fields thy T1 > single > op @) 
33192  665 
(* theory > styp > bool *) 
666 
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

667 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  668 
 is_record_get _ _ = false 
669 
fun is_record_update thy (s, T) = 

670 
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

671 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  672 
(all_record_fields thy (body_type T)) 
673 
handle TYPE _ => false 

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

675 
(case typedef_info thy s' of 

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

677 
 NONE => false) 

678 
 is_abs_fun _ _ = false 

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

680 
(case typedef_info thy s' of 

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

682 
 NONE => false) 

683 
 is_rep_fun _ _ = false 

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

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

685 
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

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

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

688 
 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

689 
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

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

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

692 
 is_quot_rep_fun _ _ = false 
33192  693 

694 
(* theory > styp > styp *) 

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

696 
(case typedef_info thy s' of 

697 
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

698 
 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

699 
 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

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

701 
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

702 
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

703 
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

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

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

706 
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

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

708 
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

709 
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

710 
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

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

712 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  713 

714 
(* theory > styp > bool *) 

715 
fun is_coconstr thy (s, T) = 

716 
let 

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

717 
val {codatatypes, ...} = Data.get thy 
33192  718 
val co_T = body_type T 
719 
val co_s = dest_Type co_T > fst 

720 
in 

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

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

723 
end 

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

725 
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

726 
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

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

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

729 
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

730 
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

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

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

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

735 
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

736 
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

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

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

739 
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

740 
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

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

742 
not (is_stale_constr thy x) 
33192  743 
(* string > bool *) 
744 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

745 
val is_sel_like_and_no_discr = 

746 
String.isPrefix sel_prefix 

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

748 

749 
(* boxability > boxability *) 

750 
fun in_fun_lhs_for InConstr = InSel 

751 
 in_fun_lhs_for _ = InFunLHS 

752 
fun in_fun_rhs_for InConstr = InConstr 

753 
 in_fun_rhs_for InSel = InSel 

754 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

755 
 in_fun_rhs_for _ = InFunRHS1 

756 

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

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

758 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  759 
case T of 
760 
Type ("fun", _) => 

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

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

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

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

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

766 
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

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

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

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

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

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

775 
and box_type hol_ctxt boxy T = 
33192  776 
case T of 
777 
Type (z as ("fun", [T1, T2])) => 

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

778 
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

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

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

783 
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

784 
> box_type hol_ctxt (in_fun_rhs_for boxy) T2 
33192  785 
 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

786 
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

787 
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

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

790 
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

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

792 
else InPair)) Ts) 
33192  793 
 _ => T 
794 

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

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

796 
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

797 
 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

798 
 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

799 
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

800 
 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

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

802 
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

803 

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

806 

807 
(* typ > int *) 

808 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

809 
(* string > int > string *) 

810 
fun nth_sel_name_for_constr_name s n = 

811 
if s = @{const_name Pair} then 

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

813 
else 

814 
sel_prefix_for n ^ s 

815 
(* styp > int > styp *) 

816 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

817 
 nth_sel_for_constr (s, T) n = 

818 
(nth_sel_name_for_constr_name s n, 

819 
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

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

821 
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

822 
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

823 
oo nth_sel_for_constr 
33192  824 

825 
(* string > int *) 

826 
fun sel_no_from_name s = 

827 
if String.isPrefix discr_prefix s then 

828 
~1 

829 
else if String.isPrefix sel_prefix s then 

830 
s > unprefix sel_prefix > Int.fromString > the 

831 
else if s = @{const_name snd} then 

832 
1 

833 
else 

834 
0 

835 

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

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

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

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

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

840 
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

841 
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

842 
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

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

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

845 
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

846 
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

847 
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

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

849 
 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

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

851 

33192  852 
(* typ list > term > int > term *) 
853 
fun eta_expand _ t 0 = t 

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

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

856 
 eta_expand Ts t n = 

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

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

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

860 

861 
(* term > term *) 

862 
fun extensionalize t = 

863 
case t of 

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

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

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

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

868 
end 

869 
 _ => t 

870 

871 
(* typ > term list > term *) 

872 
fun distinctness_formula T = 

873 
all_distinct_unordered_pairs_of 

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

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

876 

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

878 
fun zero_const T = Const (@{const_name zero_class.zero}, T) 
33192  879 
fun suc_const T = Const (@{const_name Suc}, T > T) 
880 

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

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

882 
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

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

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

885 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

907 
SOME {abs_type, rep_type, Abs_name, ...} => 
35311  908 
[(Abs_name, 
909 
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

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

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

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

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

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

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

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

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

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

919 
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

920 
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

921 
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

922 
 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

923 
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

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

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

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

927 
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

928 
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

929 
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

930 
(* hol_context > typ > int *) 
33192  931 
val num_datatype_constrs = length oo datatype_constrs 
932 

933 
(* string > string *) 

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

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

936 
 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

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

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

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

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

942 
s 
33192  943 
> the > pair s 
944 
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

945 

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

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

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

950 
Abs (Name.uu, dataT, 

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

952 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  953 
Const (discr_for_constr x) 
954 
else 

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

956 
end 

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

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

958 
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

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

960 
Const x' => 
33192  961 
if x = x' then @{const True} 
962 
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

963 
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

964 
 _ => betapply (discr_term_for_constr hol_ctxt x, t) 
33192  965 

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

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

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

969 
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

970 
@{term "%n::nat. n  1"} 
33192  971 
else if is_pair_type dataT then 
972 
Const (nth_sel_for_constr x n) 

973 
else 

974 
let 

975 
(* int > typ > int * term *) 

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

977 
let 

978 
val (m, t1) = aux m T1 

979 
val (m, t2) = aux m T2 

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

981 
 aux m T = 

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

983 
$ Bound 0) 

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

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

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

987 
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

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

989 
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

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

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

992 
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

993 
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

994 
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

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

996 
handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) 
33192  997 

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

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

999 
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

1000 
 construct_value thy stds (x as (s, _)) args = 
33192  1001 
let val args = map Envir.eta_contract args in 
1002 
case hd args of 

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

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

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

1005 
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

1006 
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

1007 
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

1008 
(index_seq 0 (length args) ~~ args) then 
33192  1009 
t 
1010 
else 

1011 
list_comb (Const x, args) 

1012 
 _ => list_comb (Const x, args) 

1013 
end 

1014 

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

1016 
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

1017 
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

1018 
 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

1019 
card_of_type assigns T1 * card_of_type assigns T2 
33192  1020 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
1021 
 card_of_type _ @{typ prop} = 2 

1022 
 card_of_type _ @{typ bool} = 2 

1023 
 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

1024 
 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

1025 
case AList.lookup (op =) assigns T of 
33192  1026 
SOME k => k 
1027 
 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

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

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

1032 
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

1033 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  1034 
in 
1035 
if k1 = max orelse k2 = max then max 

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

1037 
end 

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

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

1040 
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

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

1043 
 bounded_card_of_type max default_card assigns T = 
33192  1044 
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

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

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

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

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

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

1052 
assigns T = 
33192  1053 
let 
1054 
(* typ list > typ > int *) 

1055 
fun aux avoid T = 

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

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

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

1059 
raise SAME () 
33192  1060 
else case T of 
1061 
Type ("fun", [T1, T2]) => 

1062 
let 

1063 
val k1 = aux avoid T1 

1064 
val k2 = aux avoid T2 

1065 
in 

1066 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1069 
end 

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

1071 
let 

1072 
val k1 = aux avoid T1 

1073 
val k2 = aux avoid T2 

1074 
in 

1075 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1078 
end 

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

1080 
 @{typ prop} => 2 

1081 
 @{typ bool} => 2 

1082 
 @{typ unit} => 1 

1083 
 Type _ => 

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

1084 
(case datatype_constrs hol_ctxt T of 
34126  1085 
[] => if is_integer_type T orelse is_bit_type T then 0 
1086 
else raise SAME () 

33192  1087 
 constrs => 
1088 
let 

1089 
val constr_cards = 

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

1090 
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

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

1093 
if exists (curry (op =) 0) constr_cards then 0 
33192  1094 
else Integer.sum constr_cards 
1095 
end) 

1096 
 _ => raise SAME ()) 

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

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

1098 
AList.lookup (op =) assigns T > the_default default_card 
33192  1099 
in Int.min (max, aux [] T) end 
1100 

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

1101 
(* hol_context > typ > bool *) 
35384  1102 
fun is_finite_type hol_ctxt T = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

1103 
bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0 
33192  1104 

1105 
(* term > bool *) 

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

1107 
 is_ground_term (Const _) = true 

1108 
 is_ground_term _ = false 

1109 

1110 
(* term > word > word *) 

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

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

1113 
 hashw_term _ = 0w0 

1114 
(* term > int *) 

1115 
val hash_term = Word.toInt o hashw_term 

1116 

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

1118 
fun special_bounds ts = 

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

1120 

1121 
(* indexname * typ > term > term *) 

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

1123 

33571  1124 
(* theory > string > bool *) 
1125 
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

1126 
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

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

1128 
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

1129 
(* theory > typ > bool *) 
33571  1130 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 
1131 
 is_funky_typedef _ _ = false 

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

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

1135 
 is_arity_type_axiom _ = false 

1136 
(* theory > bool > term > bool *) 

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

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

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

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

1141 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1142 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1143 
 is_typedef_axiom _ _ _ = false 
1144 

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

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

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

1148 
using "typedef_info". *) 

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

1150 
fun partition_axioms_by_definitionality thy axioms def_names = 

1151 
let 

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

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

1154 
val nondefs = 

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

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

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

1158 

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

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

1160 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1161 
commands. *) 
1162 
(* theory > bool *) 

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

1164 

1165 
(* term > bool *) 

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

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

1167 
the_default false o try (op aconv o Logic.dest_equals) 
33192  1168 
val is_plain_definition = 
1169 
let 

1170 
(* term > bool *) 

1171 
fun do_lhs t1 = 

1172 
case strip_comb t1 of 

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

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

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

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

1178 
do_lhs t1 

1179 
 do_eq _ = false 

1180 
in do_eq end 

1181 

35335  1182 
(* theory > (term * term) list > term list * term list * term list *) 
1183 
fun all_axioms_of thy subst = 

33192  1184 
let 
1185 
(* theory list > term list *) 

35335  1186 
val axioms_of_thys = 
1187 
maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of)) 

33192  1188 
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

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

1190 
> OrdList.make fast_string_ord 
33192  1191 
val thys = thy :: Theory.ancestors_of thy 
1192 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1193 
val built_in_axioms = axioms_of_thys built_in_thys 

1194 
val user_axioms = axioms_of_thys user_thys 

1195 
val (built_in_defs, built_in_nondefs) = 

1196 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1197 
> filter (is_typedef_axiom thy false) 
33192  1198 
val (user_defs, user_nondefs) = 
1199 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

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

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

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

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

1209 
user_defs @ built_in_defs 
33192  1210 
in (defs, built_in_nondefs, user_nondefs) end 
1211 

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

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

1213 
fun arity_of_built_in_const thy stds fast_descrs (s, T) = 
33192  1214 
if s = @{const_name If} then 
1215 
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

1216 
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

1217 
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

1218 
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

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

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

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

1222 
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

1223 
 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

1224 
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

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

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

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

1228 
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

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

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

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

1232 
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

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

1234 
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

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

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

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

1238 
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

1239 
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

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

1241 
val is_built_in_const = is_some oooo arity_of_built_in_const 
33192  1242 

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

1244 
simplification rules (equational specifications). *) 

1245 
(* term > term *) 

1246 
fun term_under_def t = 

1247 
case t of 

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

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

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

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

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

1253 
 t1 $ _ => term_under_def t1 

1254 
 _ => t 

1255 

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

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

1258 
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

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

1260 
> term list *) 