author  blanchet 
Thu, 18 Feb 2010 18:48:07 +0100  
changeset 35220  2bcdae5f4fdb 
parent 35190  ce653cc27a94 
child 35280  54ab4921f826 
permissions  rwrr 
33978
2380c1dac86e
fix soundness bug in Nitpick's "destroy_constrs" optimization
blanchet
parents:
33968
diff
changeset

1 
(* Title: HOL/Tools/Nitpick/nitpick_hol.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Auxiliary HOLrelated functions used by Nitpick. 

6 
*) 

7 

8 
signature NITPICK_HOL = 

9 
sig 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33583
diff
changeset

10 
type styp = Nitpick_Util.styp 
33192  11 
type const_table = term list Symtab.table 
12 
type special_fun = (styp * int list * term list) * styp 

13 
type unrolled = styp * styp 

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

15 

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

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

19 
max_bisim_depth: int, 

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

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

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

24 
debug: bool, 

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

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

28 
skolemize: bool, 

29 
star_linear_preds: bool, 

30 
uncurry: bool, 

31 
fast_descrs: bool, 

32 
tac_timeout: Time.time option, 

33 
evals: term list, 

34 
case_names: (string * int) list, 

35 
def_table: const_table, 

36 
nondef_table: const_table, 

37 
user_nondefs: term list, 

38 
simp_table: const_table Unsynchronized.ref, 

39 
psimp_table: const_table, 

40 
intro_table: const_table, 

41 
ground_thm_table: term list Inttab.table, 

42 
ersatz_table: (string * string) list, 

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

44 
special_funs: special_fun list Unsynchronized.ref, 

45 
unrolled_preds: unrolled list Unsynchronized.ref, 

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

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

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

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

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

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

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

52 

33192  53 
val name_sep : string 
54 
val numeral_prefix : string 

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

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

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

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

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

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

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

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

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

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

67 
val unarize_and_unbox_type : typ > typ 
33192  68 
val string_for_type : Proof.context > typ > string 
69 
val prefix_name : string > string > string 

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

70 
val shortest_name : string > string 
33192  71 
val short_name : string > string 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

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

75 
val term_match : theory > term * term > bool 

76 
val is_TFree : typ > bool 

77 
val is_higher_order_type : typ > bool 

78 
val is_fun_type : typ > bool 

79 
val is_set_type : typ > bool 

80 
val is_pair_type : typ > bool 

81 
val is_lfp_iterator_type : typ > bool 

82 
val is_gfp_iterator_type : typ > bool 

83 
val is_fp_iterator_type : typ > bool 

84 
val is_boolean_type : typ > bool 

85 
val is_integer_type : typ > bool 

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

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

87 
val is_word_type : typ > bool 
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

88 
val is_integer_like_type : typ > bool 
33192  89 
val is_record_type : typ > bool 
90 
val is_number_type : theory > typ > bool 

91 
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

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

95 
val num_binder_types : typ > int 

96 
val curried_binder_types : typ > typ list 

97 
val mk_flat_tuple : typ > term list > term 

98 
val dest_n_tuple : int > term > term list 

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

99 
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

100 
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

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

104 
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

105 
val is_datatype : theory > (typ option * bool) list > typ > bool 
33192  106 
val is_record_constr : styp > bool 
107 
val is_record_get : theory > styp > bool 

108 
val is_record_update : theory > styp > bool 

109 
val is_abs_fun : theory > styp > bool 

110 
val is_rep_fun : theory > styp > bool 

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

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

112 
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

113 
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

114 
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

115 
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

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

118 
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

119 
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

120 
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

121 
val binarize_nat_and_int_in_term : term > term 
33192  122 
val discr_for_constr : styp > styp 
123 
val num_sels_for_constr_type : typ > int 

124 
val nth_sel_name_for_constr_name : string > int > string 

125 
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

126 
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

127 
hol_context > bool > styp > int > styp 
33192  128 
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

129 
val close_form : term > term 
33192  130 
val eta_expand : typ list > term > int > term 
131 
val extensionalize : term > term 

132 
val distinctness_formula : typ > term list > term 

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

134 
val unregister_frac_type : string > theory > theory 

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

136 
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

137 
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

138 
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

139 
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

140 
val num_datatype_constrs : hol_context > typ > int 
33192  141 
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

142 
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

143 
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

144 
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

145 
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

146 
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

147 
theory > (typ option * bool) list > styp > term list > term 
33192  148 
val card_of_type : (typ * int) list > typ > int 
149 
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

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

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

152 
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

153 
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

154 
val is_funky_typedef : theory > typ > bool 
33192  155 
val all_axioms_of : theory > term list * term list * term list 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

156 
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

157 
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

158 
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

159 
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

160 
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

161 
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

162 
theory > (typ option * bool) list > (string * int) list 
33192  163 
val const_def_table : Proof.context > term list > const_table 
164 
val const_nondef_table : term list > const_table 

165 
val const_simp_table : Proof.context > const_table 

166 
val const_psimp_table : Proof.context > const_table 

167 
val inductive_intro_table : Proof.context > const_table > const_table 

168 
val ground_theorem_table : theory > term list Inttab.table 

169 
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

170 
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

171 
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

172 
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

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

174 
theory > (typ option * bool) list > string * typ list > term list 
33192  175 
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

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

177 
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

178 
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

179 
val is_equational_fun : hol_context > styp > bool 
33192  180 
val is_constr_pattern_lhs : theory > term > bool 
181 
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

182 
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

183 
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

184 
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

185 
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

186 
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

187 
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

188 
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

189 
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

190 
val ground_types_in_terms : hol_context > bool > term list > typ list 
33192  191 
val format_type : int list > int list > typ > typ 
192 
val format_term_type : 

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

194 
val user_friendly_const : 

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

195 
hol_context > string * string > (term option * int list) list 
33192  196 
> styp > term * typ 
197 
val assign_operator_for_const : styp > string 

198 
end; 

199 

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

200 
structure Nitpick_HOL : NITPICK_HOL = 
33192  201 
struct 
202 

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

203 
open Nitpick_Util 
33192  204 

205 
type const_table = term list Symtab.table 

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

207 
type unrolled = styp * styp 

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

209 

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

210 
type hol_context = { 
33192  211 
thy: theory, 
212 
ctxt: Proof.context, 

213 
max_bisim_depth: int, 

214 
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

215 
stds: (typ option * bool) list, 
33192  216 
wfs: (styp option * bool option) list, 
217 
user_axioms: bool option, 

218 
debug: bool, 

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

219 
binary_ints: bool option, 
33192  220 
destroy_constrs: bool, 
221 
specialize: bool, 

222 
skolemize: bool, 

223 
star_linear_preds: bool, 

224 
uncurry: bool, 

225 
fast_descrs: bool, 

226 
tac_timeout: Time.time option, 

227 
evals: term list, 

228 
case_names: (string * int) list, 

229 
def_table: const_table, 

230 
nondef_table: const_table, 

231 
user_nondefs: term list, 

232 
simp_table: const_table Unsynchronized.ref, 

233 
psimp_table: const_table, 

234 
intro_table: const_table, 

235 
ground_thm_table: term list Inttab.table, 

236 
ersatz_table: (string * string) list, 

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

238 
special_funs: special_fun list Unsynchronized.ref, 

239 
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

240 
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

241 
constr_cache: (typ * styp list) list Unsynchronized.ref} 
33192  242 

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

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

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

245 
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

246 

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

247 
structure Data = Theory_Data( 
33192  248 
type T = {frac_types: (string * (string * string) list) list, 
249 
codatatypes: (string * (string * styp list)) list} 

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

251 
val extend = I 

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

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

255 
codatatypes = AList.merge (op =) (K true) (cs1, cs2)}) 
33192  256 

257 
val name_sep = "$" 

258 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

259 
val sel_prefix = nitpick_prefix ^ "sel" 

260 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

261 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

262 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

263 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

264 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

265 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

266 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

267 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

268 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

269 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

270 
val skolem_prefix = nitpick_prefix ^ "sk" 

271 
val special_prefix = nitpick_prefix ^ "sp" 

272 
val uncurry_prefix = nitpick_prefix ^ "unc" 

273 
val eval_prefix = nitpick_prefix ^ "eval" 

274 
val iter_var_prefix = "i" 

275 
val arg_var_prefix = "x" 

276 

277 
(* int > string *) 

278 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

279 

280 
(* string > string * string *) 

281 
val strip_first_name_sep = 

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

283 
#> pairself Substring.string 

284 
(* string > string *) 

285 
fun original_name s = 

286 
if String.isPrefix nitpick_prefix s then 

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

288 
else 

289 
s 

290 
val after_name_sep = snd o strip_first_name_sep 

291 

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

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

295 
 s_conj (t1, t2) = 

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

297 
else HOLogic.mk_conj (t1, t2) 

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

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

300 
 s_disj (t1, t2) = 

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

302 
else HOLogic.mk_disj (t1, t2) 

303 

304 
(* term > term > term list *) 

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

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

307 
 strip_connective _ t = [t] 

308 
(* term > term list * term *) 

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

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

311 
(strip_connective t0 t, t0) 

312 
else 

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

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

315 
(* term > term list *) 

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

316 
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

317 
val disjuncts_of = strip_connective @{const "op "} 
34998  318 

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

320 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  321 
well. *) 
322 
val built_in_consts = 

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

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

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

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

327 
(@{const_name Trueprop}, 1), 

328 
(@{const_name Not}, 1), 

329 
(@{const_name False}, 0), 

330 
(@{const_name True}, 0), 

331 
(@{const_name All}, 1), 

332 
(@{const_name Ex}, 1), 

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

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

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

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

337 
(@{const_name If}, 3), 

338 
(@{const_name Let}, 2), 

339 
(@{const_name Unity}, 0), 

340 
(@{const_name Pair}, 2), 

341 
(@{const_name fst}, 1), 

342 
(@{const_name snd}, 1), 

343 
(@{const_name Id}, 0), 

344 
(@{const_name insert}, 2), 

345 
(@{const_name converse}, 1), 

346 
(@{const_name trancl}, 1), 

347 
(@{const_name rel_comp}, 2), 

348 
(@{const_name image}, 2), 

349 
(@{const_name finite}, 1), 

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

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

351 
(@{const_name is_unknown}, 1), 
33192  352 
(@{const_name Tha}, 1), 
353 
(@{const_name Frac}, 0), 

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

355 
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

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

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

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

359 
(@{const_name nat_lcm}, 0)] 
33192  360 
val built_in_descr_consts = 
361 
[(@{const_name The}, 1), 

362 
(@{const_name Eps}, 1)] 

363 
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

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

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

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

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

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

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

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

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

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

373 
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

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

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

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

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

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

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

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

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

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

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

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

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

387 
(@{const_name ord_class.less_eq}, 2)] 
33192  388 

389 
(* typ > typ *) 

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

390 
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

391 
 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

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

393 
 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

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

395 
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

396 
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

397 
 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

398 
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

399 
 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

400 
 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

401 
 unarize_and_unbox_type @{typ bisim_iterator} = nat_T 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

403 
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

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

406 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type 
33192  407 

408 
(* string > string > string *) 

409 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

410 
(* string > string *) 

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

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

414 
(* string > string *) 

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

415 
fun short_name s = 
33192  416 
case space_explode name_sep s of 
417 
[_] => 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

418 
 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

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

420 
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

421 
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

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

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

425 
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

426 
#> map_types shorten_names_in_type 
33192  427 

428 
(* theory > typ * typ > bool *) 

429 
fun type_match thy (T1, T2) = 

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

431 
handle Type.TYPE_MATCH => false 

432 
(* theory > styp * styp > bool *) 

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

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

435 
(* theory > term * term > bool *) 

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

437 
 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

438 
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2)) 
33192  439 
 term_match thy (t1, t2) = t1 aconv t2 
440 

441 
(* typ > bool *) 

442 
fun is_TFree (TFree _) = true 

443 
 is_TFree _ = false 

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

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

446 
 is_higher_order_type _ = false 

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

448 
 is_fun_type _ = false 

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

450 
 is_set_type _ = false 

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

452 
 is_pair_type _ = false 

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

454 
 is_lfp_iterator_type _ = false 

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

456 
 is_gfp_iterator_type _ = false 

457 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

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

458 
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

459 
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

460 
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

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

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

463 
fun is_integer_like_type 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

464 
is_fp_iterator_type T orelse is_integer_type T orelse is_word_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

465 
T = @{typ bisim_iterator} 
33192  466 
val is_record_type = not o null o Record.dest_recTs 
467 
(* theory > typ > bool *) 

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

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

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

471 
fun is_number_type thy = is_integer_like_type orf is_frac_type thy 
33192  472 

473 
(* bool > styp > typ *) 

474 
fun iterator_type_for_const gfp (s, T) = 

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

476 
binder_types T) 

477 
(* typ > styp *) 

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

479 
 const_for_iterator_type T = 

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

480 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  481 

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

482 
(* int > typ > typ list * typ *) 
33192  483 
fun strip_n_binders 0 T = ([], T) 
484 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

485 
strip_n_binders (n  1) T2 >> cons T1 

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

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

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

488 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  489 
(* typ > typ *) 
490 
val nth_range_type = snd oo strip_n_binders 

491 

492 
(* typ > int *) 

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

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

495 
 num_factors_in_type _ = 1 

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

497 
 num_binder_types _ = 0 

498 
(* typ > typ list *) 

499 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

500 
fun maybe_curried_binder_types T = 

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

502 

503 
(* typ > term list > term *) 

504 
fun mk_flat_tuple _ [t] = t 

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

506 
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

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

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

511 

512 
(* int > typ > typ list *) 

513 
fun dest_n_tuple_type 1 T = [T] 

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

515 
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

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

517 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  518 

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

519 
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

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

521 
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

522 
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

523 

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

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

525 
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

526 
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

527 
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

528 
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

529 
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

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

531 
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

532 
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

533 
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

534 
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

535 
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

536 
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

537 
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

538 
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

539 
 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

540 

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

542 
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

543 
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

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

545 
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

546 

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

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

548 
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

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

550 
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

551 
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

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

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

554 

33192  555 
(* theory > typ > typ > typ > typ *) 
556 
fun instantiate_type thy T1 T1' T2 = 

557 
Same.commit (Envir.subst_type_same 

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

559 
(Logic.varifyT T2) 

560 
handle Type.TYPE_MATCH => 

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

561 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  562 

563 
(* theory > typ > typ > styp *) 

564 
fun repair_constr_type thy body_T' T = 

565 
instantiate_type thy (body_type T) body_T' T 

566 

567 
(* string > (string * string) list > theory > theory *) 

568 
fun register_frac_type frac_s ersaetze thy = 

569 
let 

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

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

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

575 

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

577 
fun register_codatatype co_T case_name constr_xs thy = 

578 
let 

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

579 
val {frac_types, codatatypes} = Data.get thy 
33192  580 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 
581 
val (co_s, co_Ts) = dest_Type co_T 

582 
val _ = 

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

583 
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

584 
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

585 
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

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

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

588 
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  589 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
590 
codatatypes 

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

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

594 

595 
(* theory > typ > bool *) 

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

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

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

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

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

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

604 
is_typedef thy s andalso 

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

605 
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

606 
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

607 
is_integer_like_type T) 
33192  608 
 is_pure_typedef _ _ = false 
609 
fun is_univ_typedef thy (Type (s, _)) = 

610 
(case typedef_info thy s of 

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

612 
(case set_def of 

613 
SOME thm => 

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

615 
 NONE => 

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

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

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

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

621 
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

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

623 
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

624 
 is_datatype _ _ _ = false 
33192  625 

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

627 
fun all_record_fields thy T = 

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

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

630 
end 

631 
handle TYPE _ => [] 

632 
(* styp > bool *) 

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

634 
String.isSuffix Record.extN s andalso 

635 
let val dataT = body_type T in 

636 
is_record_type dataT andalso 

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

638 
end 

639 
(* theory > typ > int *) 

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

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

642 
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

643 
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

644 
(Record.get_extT_fields thy T1 > single > op @) 
33192  645 
(* theory > styp > bool *) 
646 
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

647 
exists (curry (op =) s o fst) (all_record_fields thy T1) 
33192  648 
 is_record_get _ _ = false 
649 
fun is_record_update thy (s, T) = 

650 
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

651 
exists (curry (op =) (unsuffix Record.updateN s) o fst) 
33192  652 
(all_record_fields thy (body_type T)) 
653 
handle TYPE _ => false 

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

655 
(case typedef_info thy s' of 

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

657 
 NONE => false) 

658 
 is_abs_fun _ _ = false 

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

660 
(case typedef_info thy s' of 

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

662 
 NONE => false) 

663 
 is_rep_fun _ _ = false 

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

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

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

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

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

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

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

670 
 is_quot_rep_fun _ _ = false 
33192  671 

672 
(* theory > styp > styp *) 

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

674 
(case typedef_info thy s' of 

675 
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

676 
 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

677 
 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

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

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

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

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

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

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

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

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

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

690 
> bool_T) 

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

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

692 
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], []) 
33192  693 

694 
(* theory > styp > bool *) 

695 
fun is_coconstr thy (s, T) = 

696 
let 

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

697 
val {codatatypes, ...} = Data.get thy 
33192  698 
val co_T = body_type T 
699 
val co_s = dest_Type co_T > fst 

700 
in 

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

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

703 
end 

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

705 
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

706 
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

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

708 
@{const_name Suc_Rep}] s orelse 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35181
diff
changeset

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

710 
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

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

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

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

715 
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

716 
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

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

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

719 
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

720 
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

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

722 
not (is_stale_constr thy x) 
33192  723 
(* string > bool *) 
724 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

725 
val is_sel_like_and_no_discr = 

726 
String.isPrefix sel_prefix 

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

728 

729 
(* boxability > boxability *) 

730 
fun in_fun_lhs_for InConstr = InSel 

731 
 in_fun_lhs_for _ = InFunLHS 

732 
fun in_fun_rhs_for InConstr = InConstr 

733 
 in_fun_rhs_for InSel = InSel 

734 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

735 
 in_fun_rhs_for _ = InFunRHS1 

736 

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

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

738 
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T = 
33192  739 
case T of 
740 
Type ("fun", _) => 

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

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

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

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

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

746 
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

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

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

750 
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = 
33192  751 
case triple_lookup (type_match thy) boxes (Type z) of 
752 
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

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

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

755 
and box_type hol_ctxt boxy T = 
33192  756 
case T of 
757 
Type (z as ("fun", [T1, T2])) => 

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

758 
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

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

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

763 
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

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

766 
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

767 
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

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

770 
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

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

772 
else InPair)) Ts) 
33192  773 
 _ => T 
774 

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

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

776 
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

777 
 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

778 
 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

779 
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

780 
 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

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

782 
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

783 

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

786 

787 
(* typ > int *) 

788 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

789 
(* string > int > string *) 

790 
fun nth_sel_name_for_constr_name s n = 

791 
if s = @{const_name Pair} then 

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

793 
else 

794 
sel_prefix_for n ^ s 

795 
(* styp > int > styp *) 

796 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

797 
 nth_sel_for_constr (s, T) n = 

798 
(nth_sel_name_for_constr_name s n, 

799 
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

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

801 
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

802 
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

803 
oo nth_sel_for_constr 
33192  804 

805 
(* string > int *) 

806 
fun sel_no_from_name s = 

807 
if String.isPrefix discr_prefix s then 

808 
~1 

809 
else if String.isPrefix sel_prefix s then 

810 
s > unprefix sel_prefix > Int.fromString > the 

811 
else if s = @{const_name snd} then 

812 
1 

813 
else 

814 
0 

815 

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

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

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

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

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

820 
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

821 
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

822 
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

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

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

825 
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

826 
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

827 
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

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

829 
 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

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

831 

33192  832 
(* typ list > term > int > term *) 
833 
fun eta_expand _ t 0 = t 

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

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

836 
 eta_expand Ts t n = 

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

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

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

840 

841 
(* term > term *) 

842 
fun extensionalize t = 

843 
case t of 

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

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

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

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

848 
end 

849 
 _ => t 

850 

851 
(* typ > term list > term *) 

852 
fun distinctness_formula T = 

853 
all_distinct_unordered_pairs_of 

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

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

856 

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

858 
fun zero_const T = Const (@{const_name zero_class.zero}, T) 
33192  859 
fun suc_const T = Const (@{const_name Suc}, T > T) 
860 

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

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

862 
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

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

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

865 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

888 
[(Abs_name, instantiate_type thy abs_type T rep_type > T)] 
e1e77265fb1d
added possibility to register datatypes as codatatypes in Nitpick;
blanchet
parents:
33580
diff
changeset

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

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

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

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

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

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

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

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

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

898 
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

899 
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

900 
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

901 
 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

902 
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

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

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

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

906 
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

907 
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

908 
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

909 
(* hol_context > typ > int *) 
33192  910 
val num_datatype_constrs = length oo datatype_constrs 
911 

912 
(* string > string *) 

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

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

915 
 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

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

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

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

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

921 
s 
33192  922 
> the > pair s 
923 
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

924 

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

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

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

929 
Abs (Name.uu, dataT, 

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

931 
else if num_datatype_constrs hol_ctxt dataT >= 2 then 
33192  932 
Const (discr_for_constr x) 
933 
else 

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

935 
end 

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

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

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

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

941 
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

942 
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

943 
 _ => betapply (discr_term_for_constr hol_ctxt x, t) 
33192  944 

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

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

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

948 
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

949 
@{term "%n::nat. n  1"} 
33192  950 
else if is_pair_type dataT then 
951 
Const (nth_sel_for_constr x n) 

952 
else 

953 
let 

954 
(* int > typ > int * term *) 

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

956 
let 

957 
val (m, t1) = aux m T1 

958 
val (m, t2) = aux m T2 

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

960 
 aux m T = 

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

962 
$ Bound 0) 

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

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

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

966 
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

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

968 
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

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

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

971 
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

972 
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

973 
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

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

975 
handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t) 
33192  976 

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

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

978 
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

979 
 construct_value thy stds (x as (s, _)) args = 
33192  980 
let val args = map Envir.eta_contract args in 
981 
case hd args of 

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

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

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

984 
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

985 
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

986 
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

987 
(index_seq 0 (length args) ~~ args) then 
33192  988 
t 
989 
else 

990 
list_comb (Const x, args) 

991 
 _ => list_comb (Const x, args) 

992 
end 

993 

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

995 
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

996 
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

997 
 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

998 
card_of_type assigns T1 * card_of_type assigns T2 
33192  999 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 
1000 
 card_of_type _ @{typ prop} = 2 

1001 
 card_of_type _ @{typ bool} = 2 

1002 
 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

1003 
 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

1004 
case AList.lookup (op =) assigns T of 
33192  1005 
SOME k => k 
1006 
 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

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

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

1011 
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

1012 
val k2 = bounded_card_of_type max default_card assigns T2 
33192  1013 
in 
1014 
if k1 = max orelse k2 = max then max 

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

1016 
end 

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

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

1019 
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

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

1022 
 bounded_card_of_type max default_card assigns T = 
33192  1023 
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

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

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

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

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

1030 
fun bounded_exact_card_of_type hol_ctxt max default_card assigns T = 
33192  1031 
let 
1032 
(* typ list > typ > int *) 

1033 
fun aux avoid T = 

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

1034 
(if member (op =) avoid T then 
33192  1035 
0 
1036 
else case T of 

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

1038 
let 

1039 
val k1 = aux avoid T1 

1040 
val k2 = aux avoid T2 

1041 
in 

1042 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1045 
end 

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

1047 
let 

1048 
val k1 = aux avoid T1 

1049 
val k2 = aux avoid T2 

1050 
in 

1051 
if k1 = 0 orelse k2 = 0 then 0 

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

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

1054 
end 

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

1056 
 @{typ prop} => 2 

1057 
 @{typ bool} => 2 

1058 
 @{typ unit} => 1 

1059 
 Type _ => 

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

1060 
(case datatype_constrs hol_ctxt T of 
34126  1061 
[] => if is_integer_type T orelse is_bit_type T then 0 
1062 
else raise SAME () 

33192  1063 
 constrs => 
1064 
let 

1065 
val constr_cards = 

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

1066 
datatype_constrs hol_ctxt T 
33192  1067 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 
1068 
o snd) 

1069 
in 

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

1070 
if exists (curry (op =) 0) constr_cards then 0 
33192  1071 
else Integer.sum constr_cards 
1072 
end) 

1073 
 _ => raise SAME ()) 

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

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

1075 
AList.lookup (op =) assigns T > the_default default_card 
33192  1076 
in Int.min (max, aux [] T) end 
1077 

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

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

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

1080 
not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 [] 
33192  1081 

1082 
(* term > bool *) 

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

1084 
 is_ground_term (Const _) = true 

1085 
 is_ground_term _ = false 

1086 

1087 
(* term > word > word *) 

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

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

1090 
 hashw_term _ = 0w0 

1091 
(* term > int *) 

1092 
val hash_term = Word.toInt o hashw_term 

1093 

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

1095 
fun special_bounds ts = 

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

1097 

1098 
(* indexname * typ > term > term *) 

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

1100 

33571  1101 
(* theory > string > bool *) 
1102 
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

1103 
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

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

1105 
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

1106 
(* theory > typ > bool *) 
33571  1107 
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s 
1108 
 is_funky_typedef _ _ = false 

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

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

1112 
 is_arity_type_axiom _ = false 

1113 
(* theory > bool > term > bool *) 

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

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

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

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

1118 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
33571  1119 
boring <> is_funky_typedef_name thy s andalso is_typedef thy s 
33192  1120 
 is_typedef_axiom _ _ _ = false 
1121 

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

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

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

1125 
using "typedef_info". *) 

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

1127 
fun partition_axioms_by_definitionality thy axioms def_names = 

1128 
let 

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

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

1131 
val nondefs = 

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

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

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

1135 

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

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

1137 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1138 
commands. *) 
1139 
(* theory > bool *) 

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

1141 

1142 
(* term > bool *) 

1143 
val is_plain_definition = 

1144 
let 

1145 
(* term > bool *) 

1146 
fun do_lhs t1 = 

1147 
case strip_comb t1 of 

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

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

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

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

1153 
do_lhs t1 

1154 
 do_eq _ = false 

1155 
in do_eq end 

1156 

1157 
(* theory > term list * term list * term list *) 

1158 
fun all_axioms_of thy = 

1159 
let 

1160 
(* theory list > term list *) 

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

1162 
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

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

1164 
> OrdList.make fast_string_ord 
33192  1165 
val thys = thy :: Theory.ancestors_of thy 
1166 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1167 
val built_in_axioms = axioms_of_thys built_in_thys 

1168 
val user_axioms = axioms_of_thys user_thys 

1169 
val (built_in_defs, built_in_nondefs) = 

1170 
partition_axioms_by_definitionality thy built_in_axioms def_names 

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

1171 
> filter (is_typedef_axiom thy false) 
33192  1172 
val (user_defs, user_nondefs) = 
1173 
partition_axioms_by_definitionality thy user_axioms def_names 

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

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

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

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

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

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

1179 
> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd) 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1180 
> map (prop_of o snd) > filter is_plain_definition) @ 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33978
diff
changeset

1181 
user_defs @ built_in_defs 
33192  1182 
in (defs, built_in_nondefs, user_nondefs) end 
1183 

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

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

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

1188 
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

1189 
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

1190 
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

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

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

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

1194 
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

1195 
 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

1196 
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

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

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

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

1200 
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

1201 
 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

1202 
if is_fun_type T andalso is_set_type (domain_type 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

1203 
AList.lookup (op =) built_in_set_consts 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

1204 
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

1205 
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

1206 
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

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

1208 
val is_built_in_const = is_some oooo arity_of_built_in_const 
33192  1209 

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

1211 
simplification rules (equational specifications). *) 

1212 
(* term > term *) 

1213 
fun term_under_def t = 

1214 
case t of 

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

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

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

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

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

1220 
 t1 $ _ => term_under_def t1 

1221 
 _ => t 

1222 

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

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

1225 
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

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

1227 
> term list *) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1228 
fun def_props_for_const thy stds fast_descrs table (x as (s, _)) = 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

1229 
if is_built_in_const thy stds fast_descrs x then 
33192  1230 
[] 
1231 
else 

1232 
these (Symtab.lookup table s) 

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

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

1234 
> filter (curry (op =) (Const x) o term_under_def) 
33192  1235 

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

1236 
(* theory > term > term option *) 
33192  1237 
fun normalized_rhs_of thy t = 
1238 
let 

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

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

1240 
fun aux (v as Var _) (SOME t) = SOME (lambda v t) 
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

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

1242 
 aux _ _ = NONE 
33192  1243 
val (lhs, rhs) = 
1244 
case t of 

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

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

1247 
(t1, t2) 

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

1248 
 _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1249 
val args = strip_comb lhs > snd 
33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1250 
in fold_rev aux args (SOME rhs) end 
33192  1251 

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

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

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

1254 
if is_built_in_const thy [(NONE, false)] false x 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

1255 
original_name s <> s then 
33192  1256 
NONE 
1257 
else 

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

1258 
x > def_props_for_const thy [(NONE, false)] false table > List.last 
33743
a58893035742
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
blanchet
parents:
33706
diff
changeset

1259 
> normalized_rhs_of thy > Option.map (prefix_abs_vars s) 
33192  1260 
handle List.Empty => NONE 
1261 

1262 
(* term > fixpoint_kind *) 

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

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

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

1266 
 fixpoint_kind_of_rhs _ = NoFp 
