author  blanchet 
Wed, 02 Mar 2011 14:50:16 +0100  
changeset 41871  394eef237bd1 
parent 41803  ef13e3b7cbaf 
child 41875  e3cd0dce9b1a 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_model.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:
34974
diff
changeset

3 
Copyright 2009, 2010 
33192  4 

5 
Model reconstruction for Nitpick. 

6 
*) 

7 

8 
signature NITPICK_MODEL = 

9 
sig 

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

10 
type styp = Nitpick_Util.styp 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

11 
type scope = Nitpick_Scope.scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

12 
type rep = Nitpick_Rep.rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

13 
type nut = Nitpick_Nut.nut 
33192  14 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

15 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

16 
{show_datatypes: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

17 
show_consts: bool} 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

18 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

19 
type term_postprocessor = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

20 
Proof.context > string > (typ > term list) > typ > term > term 
33192  21 

22 
structure NameTable : TABLE 

23 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

24 
val irrelevant : string 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

25 
val unknown : string 
37261  26 
val unrep : unit > string 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

27 
val register_term_postprocessor : 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

28 
typ > term_postprocessor > morphism > Context.generic > Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

29 
val register_term_postprocessor_global : 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

30 
typ > term_postprocessor > theory > theory 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

31 
val unregister_term_postprocessor : 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

32 
typ > morphism > Context.generic > Context.generic 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

33 
val unregister_term_postprocessor_global : typ > theory > theory 
33192  34 
val tuple_list_for_name : 
35 
nut NameTable.table > Kodkod.raw_bound list > nut > int list list 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

36 
val dest_plain_fun : term > bool * (term list * term list) 
33192  37 
val reconstruct_hol_model : 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

38 
params > scope > (term option * int list) list 
38170  39 
> (typ option * string list) list > styp list > styp list > nut list 
40 
> nut list > nut list > nut NameTable.table > Kodkod.raw_bound list 

33192  41 
> Pretty.T * bool 
42 
val prove_hol_model : 

43 
scope > Time.time option > nut list > nut list > nut NameTable.table 

44 
> Kodkod.raw_bound list > term > bool option 

45 
end; 

46 

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

47 
structure Nitpick_Model : NITPICK_MODEL = 
33192  48 
struct 
49 

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

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

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

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

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

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

55 
open Nitpick_Nut 
33192  56 

34126  57 
structure KK = Kodkod 
58 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

59 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

60 
{show_datatypes: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

61 
show_consts: bool} 
33192  62 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

63 
type term_postprocessor = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

64 
Proof.context > string > (typ > term list) > typ > term > term 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

65 

41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

66 
structure Data = Generic_Data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

67 
( 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

68 
type T = (typ * term_postprocessor) list 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

69 
val empty = [] 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

70 
val extend = I 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

71 
fun merge data = AList.merge (op =) (K true) data 
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41052
diff
changeset

72 
) 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

73 

37261  74 
fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s' 
75 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

76 
val irrelevant = "_" 
33192  77 
val unknown = "?" 
37261  78 
val unrep = xsym "\<dots>" "..." 
79 
val maybe_mixfix = xsym "_\<^sup>?" "_?" 

80 
val base_mixfix = xsym "_\<^bsub>base\<^esub>" "_.base" 

81 
val step_mixfix = xsym "_\<^bsub>step\<^esub>" "_.step" 

82 
val abs_mixfix = xsym "\<guillemotleft>_\<guillemotright>" "\"_\"" 

35718  83 
val arg_var_prefix = "x" 
37261  84 
val cyclic_co_val_name = xsym "\<omega>" "w" 
85 
val cyclic_const_prefix = xsym "\<xi>" "X" 

86 
fun cyclic_type_name () = nitpick_prefix ^ cyclic_const_prefix () 

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

87 
val opt_flag = nitpick_prefix ^ "opt" 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

88 
val non_opt_flag = nitpick_prefix ^ "non_opt" 
33192  89 

35076
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
35075
diff
changeset

90 
type atom_pool = ((string * int) * int list) list 
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
35075
diff
changeset

91 

35718  92 
fun add_wacky_syntax ctxt = 
93 
let 

94 
val name_of = fst o dest_Const 

95 
val thy = ProofContext.theory_of ctxt > Context.reject_draft 

96 
val (maybe_t, thy) = 

97 
Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), 

37261  98 
Mixfix (maybe_mixfix (), [1000], 1000)) thy 
35718  99 
val (abs_t, thy) = 
100 
Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), 

37261  101 
Mixfix (abs_mixfix (), [40], 40)) thy 
35718  102 
val (base_t, thy) = 
103 
Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), 

37261  104 
Mixfix (base_mixfix (), [1000], 1000)) thy 
35718  105 
val (step_t, thy) = 
106 
Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), 

37261  107 
Mixfix (step_mixfix (), [1000], 1000)) thy 
35718  108 
in 
109 
(pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), 

110 
ProofContext.transfer_syntax thy ctxt) 

111 
end 

112 

113 
(** Term reconstruction **) 

114 

37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

115 
fun nth_atom_number pool T j = 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

116 
case AList.lookup (op =) (!pool) T of 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

117 
SOME js => 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

118 
(case find_index (curry (op =) j) js of 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

119 
~1 => (Unsynchronized.change pool (cons (T, j :: js)); 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

120 
length js + 1) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

121 
 n => length js  n) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

122 
 NONE => (Unsynchronized.change pool (cons (T, [j])); 1) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

123 
fun atom_suffix s = 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

124 
nat_subscript 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40132
diff
changeset

125 
#> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s))) (* FIXME Symbol.explode (?) *) 
33884
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

126 
? prefix "\<^isub>," 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

127 
fun nth_atom_name thy atomss pool prefix T j = 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

128 
let 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

129 
val ss = these (triple_lookup (type_match thy) atomss T) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

130 
val m = nth_atom_number pool T j 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

131 
in 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

132 
if m <= length ss then 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

133 
nth ss (m  1) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

134 
else case T of 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

135 
Type (s, _) => 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

136 
let val s' = shortest_name s in 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

137 
prefix ^ 
41039
405a9f41ad6b
show strings as "s_1" etc. rather than "l_1" etc.
blanchet
parents:
40627
diff
changeset

138 
(if T = @{typ string} then "s" 
405a9f41ad6b
show strings as "s_1" etc. rather than "l_1" etc.
blanchet
parents:
40627
diff
changeset

139 
else if String.isPrefix "\\" s' then s' 
405a9f41ad6b
show strings as "s_1" etc. rather than "l_1" etc.
blanchet
parents:
40627
diff
changeset

140 
else substring (s', 0, 1)) ^ atom_suffix s m 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

141 
end 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

142 
 TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

143 
 _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], []) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

144 
end 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

145 
fun nth_atom thy atomss pool for_auto T j = 
33192  146 
if for_auto then 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

147 
Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix)) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

148 
T j, T) 
33192  149 
else 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

150 
Const (nth_atom_name thy atomss pool "" T j, T) 
33192  151 

35177  152 
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) = 
34126  153 
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) 
154 
 extract_real_number t = real (snd (HOLogic.dest_number t)) 

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

155 
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) 
34126  156 
 nice_term_ord tp = Real.compare (pairself extract_real_number tp) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

157 
handle TERM ("dest_number", _) => 
34126  158 
case tp of 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

159 
(t11 $ t12, t21 $ t22) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

160 
(case nice_term_ord (t11, t21) of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

161 
EQUAL => nice_term_ord (t12, t22) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

162 
 ord => ord) 
35408  163 
 _ => Term_Ord.fast_term_ord tp 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

164 

38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

165 
fun register_term_postprocessor_generic T postproc = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

166 
Data.map (cons (T, postproc)) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

167 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

168 
fun register_term_postprocessor T postproc (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

169 
register_term_postprocessor_generic T postproc 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

170 
val register_term_postprocessor_global = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

171 
Context.theory_map oo register_term_postprocessor_generic 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

172 

a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

173 
fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T) 
38284
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

174 
(* TODO: Consider morphism. *) 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

175 
fun unregister_term_postprocessor T (_ : morphism) = 
9f98107ad8b4
use "declaration" instead of "setup" to register Nitpick extensions
blanchet
parents:
38240
diff
changeset

176 
unregister_term_postprocessor_generic T 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

177 
val unregister_term_postprocessor_global = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

178 
Context.theory_map o unregister_term_postprocessor_generic 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

179 

33192  180 
fun tuple_list_for_name rel_table bounds name = 
181 
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] 

182 

41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41039
diff
changeset

183 
fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

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

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

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

188 
$ t1 $ t2) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

189 
let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

190 
Const (@{const_name Pair}, Ts > Type (@{type_name prod}, Ts)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

191 
$ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 
33192  192 
end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

193 
 unarize_unbox_etc_term (Const (s, T)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

194 
Const (s, uniterize_unarize_unbox_etc_type T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

195 
 unarize_unbox_etc_term (t1 $ t2) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

196 
unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

197 
 unarize_unbox_etc_term (Free (s, T)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

198 
Free (s, uniterize_unarize_unbox_etc_type T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

199 
 unarize_unbox_etc_term (Var (x, T)) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

200 
Var (x, uniterize_unarize_unbox_etc_type T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

201 
 unarize_unbox_etc_term (Bound j) = Bound j 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

203 
Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t') 
33192  204 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

205 
fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12])) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

206 
(T2 as Type (@{type_name prod}, [T21, T22])) = 
33192  207 
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in 
208 
if n1 = n2 then 

209 
let 

210 
val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 

211 
in 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

212 
((Type (@{type_name prod}, [T11, T11']), opt_T12'), 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

213 
(Type (@{type_name prod}, [T21, T21']), opt_T22')) 
33192  214 
end 
215 
else if n1 < n2 then 

216 
case factor_out_types T1 T21 of 

217 
(p1, (T21', NONE)) => (p1, (T21', SOME T22)) 

218 
 (p1, (T21', SOME T22')) => 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

219 
(p1, (T21', SOME (Type (@{type_name prod}, [T22', T22])))) 
33192  220 
else 
221 
swap (factor_out_types T2 T1) 

222 
end 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

223 
 factor_out_types (Type (@{type_name prod}, [T11, T12])) T2 = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

224 
((T11, SOME T12), (T2, NONE)) 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

225 
 factor_out_types T1 (Type (@{type_name prod}, [T21, T22])) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

226 
((T1, NONE), (T21, SOME T22)) 
33192  227 
 factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) 
228 

229 
fun make_plain_fun maybe_opt T1 T2 = 

230 
let 

231 
fun aux T1 T2 [] = 

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

232 
Const (if maybe_opt then opt_flag else non_opt_flag, T1 > T2) 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

233 
 aux T1 T2 ((t1, t2) :: tps) = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

234 
Const (@{const_name fun_upd}, (T1 > T2) > T1 > T2 > T1 > T2) 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

235 
$ aux T1 T2 tps $ t1 $ t2 
33192  236 
in aux T1 T2 o rev 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:
34974
diff
changeset

237 
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag) 
33192  238 
 is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) = 
239 
is_plain_fun t0 

240 
 is_plain_fun _ = false 

241 
val dest_plain_fun = 

242 
let 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

243 
fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], [])) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

244 
 aux (Const (s, _)) = (s <> non_opt_flag, ([], [])) 
33192  245 
 aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

246 
let val (maybe_opt, (ts1, ts2)) = aux t0 in 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

247 
(maybe_opt, (t1 :: ts1, t2 :: ts2)) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

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

249 
 aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) 
33192  250 
in apsnd (pairself rev) o aux end 
251 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

252 
fun break_in_two T T1 T2 t = 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

253 
let 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

254 
val ps = HOLogic.flat_tupleT_paths T 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

255 
val cut = length (HOLogic.strip_tupleT T1) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

256 
val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

257 
val (ts1, ts2) = t > HOLogic.strip_ptuple ps > chop cut 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

258 
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

259 
fun pair_up (Type (@{type_name prod}, [T1', T2'])) 
33192  260 
(t1 as Const (@{const_name Pair}, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

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

263 
$ t11 $ t12) t2 = 
33192  264 
if T1 = T1' then HOLogic.mk_prod (t1, t2) 
265 
else HOLogic.mk_prod (t11, pair_up T2' t12 t2) 

266 
 pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2) 

267 
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3 

268 

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

269 
fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t = 
33192  270 
let 
33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

271 
fun do_curry T1 T1a T1b T2 t = 
33192  272 
let 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

273 
val (maybe_opt, tsp) = dest_plain_fun t 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

274 
val tps = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

275 
tsp >> map (break_in_two T1 T1a T1b) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

276 
> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2)))) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

277 
> AList.coalesce (op =) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

278 
> map (apsnd (make_plain_fun maybe_opt T1b T2)) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

279 
in make_plain_fun maybe_opt T1a (T1b > T2) tps end 
33192  280 
and do_uncurry T1 T2 t = 
281 
let 

282 
val (maybe_opt, tsp) = dest_plain_fun t 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

283 
val tps = 
33192  284 
tsp > op ~~ 
285 
> maps (fn (t1, t2) => 

286 
multi_pair_up T1 t1 (snd (dest_plain_fun t2))) 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

287 
in make_plain_fun maybe_opt T1 T2 tps end 
33192  288 
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' > T2') 
289 
 do_arrow T1' T2' T1 T2 

290 
(Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = 

291 
Const (@{const_name fun_upd}, 

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

292 
(T1' > T2') > T1' > T2' > T1' > T2') 
33192  293 
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 
294 
 do_arrow _ _ _ _ t = 

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

295 
raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) 
33192  296 
and do_fun T1' T2' T1 T2 t = 
297 
case factor_out_types T1' T1 of 

298 
((_, NONE), (_, NONE)) => t > do_arrow T1' T2' T1 T2 

299 
 ((_, NONE), (T1a, SOME T1b)) => 

33565
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

300 
t > do_curry T1 T1a T1b T2 > do_arrow T1' T2' T1a (T1b > T2) 
33192  301 
 ((T1a', SOME T1b'), (_, NONE)) => 
302 
t > do_arrow T1a' (T1b' > T2') T1 T2 > do_uncurry T1' T2' 

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

303 
 _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

304 
and do_term (Type (@{type_name fun}, [T1', T2'])) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

305 
(Type (@{type_name fun}, [T1, T2])) t = 
33192  306 
do_fun T1' T2' T1 T2 t 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

307 
 do_term (T' as Type (@{type_name prod}, Ts' as [T1', T2'])) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

308 
(Type (@{type_name prod}, [T1, T2])) 
33192  309 
(Const (@{const_name Pair}, _) $ t1 $ t2) = 
310 
Const (@{const_name Pair}, Ts' > T') 

311 
$ do_term T1' T1 t1 $ do_term T2' T2 t2 

312 
 do_term T' T t = 

313 
if T = T' then t 

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

314 
else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], []) 
33192  315 
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end 
34998  316 
 typecast_fun T' _ _ _ = 
317 
raise TYPE ("Nitpick_Model.typecast_fun", [T'], []) 

33192  318 

319 
fun truth_const_sort_key @{const True} = "0" 

320 
 truth_const_sort_key @{const False} = "2" 

321 
 truth_const_sort_key _ = "1" 

322 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

323 
fun mk_tuple (Type (@{type_name prod}, [T1, T2])) ts = 
33192  324 
HOLogic.mk_prod (mk_tuple T1 ts, 
325 
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) 

326 
 mk_tuple _ (t :: _) = t 

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

327 
 mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) 
33192  328 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

329 
fun varified_type_match ctxt (candid_T, pat_T) = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

330 
let val thy = ProofContext.theory_of ctxt in 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

331 
strict_type_match thy (candid_T, varify_type ctxt pat_T) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

332 
end 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

333 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

334 
fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope) 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

335 
atomss sel_names rel_table bounds card T = 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

336 
let 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

337 
val card = if card = 0 then card_of_type card_assigns T else card 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

338 
fun nth_value_of_type n = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

339 
let 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

340 
fun term unfold = 
37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

341 
reconstruct_term true unfold pool wacky_names scope atomss sel_names 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

342 
rel_table bounds T T (Atom (card, 0)) [[n]] 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

343 
in 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

344 
case term false of 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

345 
t as Const (s, _) => 
37261  346 
if String.isPrefix (cyclic_const_prefix ()) s then 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

347 
HOLogic.mk_eq (t, term true) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

348 
else 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

349 
t 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

350 
 t => t 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

351 
end 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

352 
in index_seq 0 card > map nth_value_of_type > sort nice_term_ord end 
37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

353 
and reconstruct_term maybe_opt unfold pool 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

354 
(wacky_names as ((maybe_name, abs_name), _)) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37170
diff
changeset

355 
(scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

356 
bits, datatypes, ofs, ...}) 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

357 
atomss sel_names rel_table bounds = 
33192  358 
let 
359 
val for_auto = (maybe_name = "") 

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

360 
fun value_of_bits jss = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

362 
val j0 = offset_of_type ofs @{typ unsigned_bit} 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

363 
val js = map (Integer.add (~ j0) o the_single) jss 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

365 
fold (fn j => Integer.add (reasonable_power 2 j > j = bits ? op ~)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

367 
end 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

368 
val all_values = 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

369 
all_values_of_type pool wacky_names scope atomss sel_names rel_table 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

370 
bounds 0 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

371 
fun postprocess_term (Type (@{type_name fun}, _)) = I 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

372 
 postprocess_term T = 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

373 
case Data.get (Context.Proof ctxt) of 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

374 
[] => I 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

375 
 postprocs => 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

376 
case AList.lookup (varified_type_match ctxt) postprocs T of 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

377 
SOME postproc => postproc ctxt maybe_name all_values T 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38209
diff
changeset

378 
 NONE => I 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

379 
fun postprocess_subterms Ts (t1 $ t2) = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

380 
let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

381 
postprocess_term (fastype_of1 (Ts, t)) t 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

382 
end 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

383 
 postprocess_subterms Ts (Abs (s, T, t')) = 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

384 
Abs (s, T, postprocess_subterms (T :: Ts) t') 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

385 
 postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t 
35388
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

386 
fun make_set maybe_opt T1 T2 tps = 
33192  387 
let 
35402  388 
val empty_const = Const (@{const_abbrev Set.empty}, T1 > T2) 
33192  389 
val insert_const = Const (@{const_name insert}, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

390 
T1 > (T1 > T2) > T1 > T2) 
33192  391 
fun aux [] = 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset

392 
if maybe_opt andalso not (is_complete_type datatypes false T1) then 
37261  393 
insert_const $ Const (unrep (), T1) $ empty_const 
33192  394 
else 
395 
empty_const 

396 
 aux ((t1, t2) :: zs) = 

35388
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

397 
aux zs 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

398 
> t2 <> @{const False} 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

399 
? curry (op $) 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

400 
(insert_const 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

401 
$ (t1 > t2 <> @{const True} 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

402 
? curry (op $) 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

403 
(Const (maybe_name, T1 > T1)))) 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

404 
in 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

405 
if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False}) 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

406 
tps then 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

407 
Const (unknown, T1 > T2) 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

408 
else 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

409 
aux tps 
42d39948cace
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents:
35385
diff
changeset

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

411 
fun make_map maybe_opt T1 T2 T2' = 
33192  412 
let 
413 
val update_const = Const (@{const_name fun_upd}, 

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

414 
(T1 > T2) > T1 > T2 > T1 > T2) 
35402  415 
fun aux' [] = Const (@{const_abbrev Map.empty}, T1 > T2) 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

416 
 aux' ((t1, t2) :: tps) = 
33192  417 
(case t2 of 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

418 
Const (@{const_name None}, _) => aux' tps 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

419 
 _ => update_const $ aux' tps $ t1 $ t2) 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

420 
fun aux tps = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

421 
if maybe_opt andalso not (is_complete_type datatypes false T1) then 
37261  422 
update_const $ aux' tps $ Const (unrep (), T1) 
33192  423 
$ (Const (@{const_name Some}, T2' > T2) $ Const (unknown, T2')) 
424 
else 

35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

425 
aux' tps 
33192  426 
in aux 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:
34974
diff
changeset

427 
fun polish_funs Ts t = 
33192  428 
(case fastype_of1 (Ts, t) of 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

429 
Type (@{type_name fun}, [T1, T2]) => 
33192  430 
if is_plain_fun t then 
431 
case T2 of 

432 
@{typ bool} => 

433 
let 

434 
val (maybe_opt, ts_pair) = 

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

435 
dest_plain_fun t > pairself (map (polish_funs Ts)) 
33192  436 
in 
437 
make_set maybe_opt T1 T2 

438 
(sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair)) 

439 
end 

440 
 Type (@{type_name option}, [T2']) => 

441 
let 

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

442 
val (maybe_opt, ts_pair) = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

443 
dest_plain_fun t > pairself (map (polish_funs Ts)) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

444 
in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end 
33192  445 
 _ => raise SAME () 
446 
else 

447 
raise SAME () 

448 
 _ => raise SAME ()) 

449 
handle SAME () => 

450 
case t 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:
34974
diff
changeset

451 
(t1 as Const (@{const_name fun_upd}, _) $ t11 $ _) 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

452 
$ (t2 as Const (s, _)) => 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

453 
if s = unknown then polish_funs Ts t11 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

454 
else polish_funs Ts t1 $ polish_funs Ts t2 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

455 
 t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

456 
 Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t') 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

457 
 Const (s, Type (@{type_name fun}, [T1, T2])) => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

458 
if s = opt_flag orelse s = non_opt_flag then 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

459 
Abs ("x", T1, 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

460 
Const (if is_complete_type datatypes false T1 then 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

461 
irrelevant 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

462 
else 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

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

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

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

466 
 t => t 
33192  467 
fun make_fun maybe_opt T1 T2 T' ts1 ts2 = 
34126  468 
ts1 ~~ ts2 > sort (nice_term_ord o pairself fst) 
34998  469 
> make_plain_fun maybe_opt T1 T2 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

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

471 
> typecast_fun (uniterize_unarize_unbox_etc_type T') 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

472 
(uniterize_unarize_unbox_etc_type T1) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

473 
(uniterize_unarize_unbox_etc_type T2) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

474 
fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ = 
33192  475 
let 
476 
val k1 = card_of_type card_assigns T1 

477 
val k2 = card_of_type card_assigns T2 

478 
in 

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

479 
term_for_rep true seen T T' (Vect (k1, Atom (k2, 0))) 
33192  480 
[nth_combination (replicate k1 (k2, 0)) j] 
481 
handle General.Subscript => 

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

482 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", 
33192  483 
signed_string_of_int j ^ " for " ^ 
484 
string_for_rep (Vect (k1, Atom (k2, 0)))) 

485 
end 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

486 
 term_for_atom seen (Type (@{type_name prod}, [T1, T2])) _ j k = 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

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

488 
val k1 = card_of_type card_assigns T1 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

489 
val k2 = k div k1 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

490 
in 
33192  491 
list_comb (HOLogic.pair_const T1 T2, 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

492 
map3 (fn T => term_for_atom seen T T) [T1, T2] 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

493 
[j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *) 
33192  494 
end 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

495 
 term_for_atom seen @{typ prop} _ j k = 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

496 
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k) 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

497 
 term_for_atom _ @{typ bool} _ j _ = 
33192  498 
if j = 0 then @{const False} else @{const True} 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

499 
 term_for_atom seen T _ j k = 
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

500 
if T = nat_T andalso is_standard_datatype thy stds nat_T then 
33192  501 
HOLogic.mk_number nat_T j 
502 
else if T = int_T then 

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

503 
HOLogic.mk_number int_T (int_for_atom (k, 0) j) 
33192  504 
else if is_fp_iterator_type T then 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

505 
HOLogic.mk_number nat_T (k  j  1) 
33192  506 
else if T = @{typ bisim_iterator} then 
507 
HOLogic.mk_number nat_T j 

508 
else case datatype_spec datatypes T of 

37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

509 
NONE => nth_atom thy atomss pool for_auto T j 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

510 
 SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j 
35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

511 
 SOME {co, standard, constrs, ...} => 
33192  512 
let 
513 
fun tuples_for_const (s, T) = 

514 
tuple_list_for_name rel_table bounds (ConstName (s, T, Any)) 

35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

515 
fun cyclic_atom () = 
37261  516 
nth_atom thy atomss pool for_auto (Type (cyclic_type_name (), [])) 
517 
j 

37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

518 
fun cyclic_var () = 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

519 
Var ((nth_atom_name thy atomss pool "" T j, 0), T) 
33192  520 
val discr_jsss = map (tuples_for_const o discr_for_constr o #const) 
521 
constrs 

522 
val real_j = j + offset_of_type ofs T 

523 
val constr_x as (constr_s, constr_T) = 

524 
get_first (fn (jss, {const, ...}) => 

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

525 
if member (op =) jss [real_j] then SOME const 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

526 
else NONE) 
33192  527 
(discr_jsss ~~ constrs) > the 
528 
val arg_Ts = curried_binder_types constr_T 

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

529 
val sel_xs = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35188
diff
changeset

530 
map (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:
35188
diff
changeset

531 
constr_x) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35188
diff
changeset

532 
(index_seq 0 (length arg_Ts)) 
33192  533 
val sel_Rs = 
534 
map (fn x => get_first 

535 
(fn ConstName (s', T', R) => 

536 
if (s', T') = x then SOME R else NONE 

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

537 
 u => raise NUT ("Nitpick_Model.reconstruct_\ 
33192  538 
\term.term_for_atom", [u])) 
539 
sel_names > the) sel_xs 

540 
val arg_Rs = map (snd o dest_Func) sel_Rs 

541 
val sel_jsss = map tuples_for_const sel_xs 

542 
val arg_jsss = 

543 
map (map_filter (fn js => if hd js = real_j then SOME (tl js) 

544 
else NONE)) sel_jsss 

545 
val uncur_arg_Ts = binder_types constr_T 

35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

546 
val maybe_cyclic = co orelse not standard 
33192  547 
in 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

548 
if maybe_cyclic andalso not (null seen) andalso 
35188
8c70a34931b1
improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents:
35180
diff
changeset

549 
member (op =) (seen > unfold ? (fst o split_last)) (T, j) then 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

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

551 
else if constr_s = @{const_name Word} then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

552 
HOLogic.mk_number 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

553 
(if T = @{typ "unsigned_bit word"} then nat_T else int_T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

554 
(value_of_bits (the_single arg_jsss)) 
33192  555 
else 
556 
let 

35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

557 
val seen = seen > maybe_cyclic ? cons (T, j) 
33192  558 
val ts = 
559 
if length arg_Ts = 0 then 

560 
[] 

561 
else 

41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41039
diff
changeset

562 
map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs 
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41039
diff
changeset

563 
arg_jsss 
33192  564 
> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) 
565 
> dest_n_tuple (length uncur_arg_Ts) 

566 
val t = 

567 
if constr_s = @{const_name Abs_Frac} then 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

568 
case ts of 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

569 
[Const (@{const_name Pair}, _) $ t1 $ t2] => 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

570 
frac_from_term_pair (body_type T) t1 t2 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

571 
 _ => raise TERM ("Nitpick_Model.reconstruct_term.\ 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35665
diff
changeset

572 
\term_for_atom (Abs_Frac)", ts) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

573 
else if not for_auto andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37170
diff
changeset

574 
(is_abs_fun ctxt constr_x orelse 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

575 
constr_s = @{const_name Quot}) then 
33192  576 
Const (abs_name, constr_T) $ the_single ts 
577 
else 

578 
list_comb (Const constr_x, ts) 

579 
in 

35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

580 
if maybe_cyclic then 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

581 
let val var = cyclic_var () in 
35188
8c70a34931b1
improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents:
35180
diff
changeset

582 
if unfold andalso not standard andalso 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

583 
length seen = 1 andalso 
37261  584 
exists_subterm 
585 
(fn Const (s, _) => 

586 
String.isPrefix (cyclic_const_prefix ()) s 

587 
 t' => t' = var) t then 

35188
8c70a34931b1
improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents:
35180
diff
changeset

588 
subst_atomic [(var, cyclic_atom ())] t 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

589 
else if exists_subterm (curry (op =) var) t then 
35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

590 
if co then 
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

591 
Const (@{const_name The}, (T > bool_T) > T) 
37261  592 
$ Abs (cyclic_co_val_name (), T, 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38284
diff
changeset

593 
Const (@{const_name HOL.eq}, T > T > bool_T) 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

594 
$ Bound 0 $ abstract_over (var, t)) 
35179
4b198af5beb5
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents:
35177
diff
changeset

595 
else 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

596 
cyclic_atom () 
33192  597 
else 
598 
t 

599 
end 

600 
else 

601 
t 

602 
end 

603 
end 

604 
and term_for_vect seen k R T1 T2 T' js = 

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

605 
make_fun true T1 T2 T' 
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

606 
(map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

607 
(map (term_for_rep true seen T2 T2 R o single) 
33192  608 
(batch_list (arity_of_rep R) js)) 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

609 
and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] = 
35075
888802be2019
handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents:
35070
diff
changeset

610 
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j  j0) k 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

611 
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38189
diff
changeset

612 
 term_for_rep _ seen (Type (@{type_name prod}, [T1, T2])) _ 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

613 
(Struct [R1, R2]) [js] = 
33192  614 
let 
615 
val arity1 = arity_of_rep R1 

616 
val (js1, js2) = chop arity1 js 

617 
in 

618 
list_comb (HOLogic.pair_const T1 T2, 

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

619 
map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2] 
33192  620 
[[js1], [js2]]) 
621 
end 

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

622 
 term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T' 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

623 
(Vect (k, R')) [js] = 
33192  624 
term_for_vect seen k R' T1 T2 T' js 
37170
38ba15040455
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
blanchet
parents:
36607
diff
changeset

625 
 term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

626 
(Func (R1, Formula Neut)) jss = 
33192  627 
let 
628 
val jss1 = all_combinations_for_rep R1 

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

629 
val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1 
33192  630 
val ts2 = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

631 
map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0)) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset

632 
[[int_from_bool (member (op =) jss js)]]) 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

633 
jss1 
37170
38ba15040455
Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
blanchet
parents:
36607
diff
changeset

634 
in make_fun maybe_opt T1 T2 T' ts1 ts2 end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

635 
 term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T' 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

636 
(Func (R1, R2)) jss = 
33192  637 
let 
638 
val arity1 = arity_of_rep R1 

639 
val jss1 = all_combinations_for_rep R1 

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

640 
val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1 
33192  641 
val grouped_jss2 = AList.group (op =) (map (chop arity1) jss) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

642 
val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default [] 
33192  643 
o AList.lookup (op =) grouped_jss2) jss1 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

644 
in make_fun maybe_opt T1 T2 T' ts1 ts2 end 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

645 
 term_for_rep _ seen T T' (Opt R) jss = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

646 
if null jss then Const (unknown, T) 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

647 
else term_for_rep true seen T T' R jss 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

648 
 term_for_rep _ _ T _ R jss = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

649 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

650 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ 
33192  651 
string_of_int (length jss)) 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

652 
in 
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

653 
postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term 
37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

654 
oooo term_for_rep maybe_opt [] 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

655 
end 
33192  656 

35718  657 
(** Constant postprocessing **) 
658 

659 
fun dest_n_tuple_type 1 T = [T] 

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

661 
T1 :: dest_n_tuple_type (n  1) T2 

662 
 dest_n_tuple_type _ T = 

663 
raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], []) 

664 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

665 
fun const_format thy def_tables (x as (s, T)) = 
35718  666 
if String.isPrefix unrolled_prefix s then 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

667 
const_format thy def_tables (original_name s, range_type T) 
35718  668 
else if String.isPrefix skolem_prefix s then 
669 
let 

670 
val k = unprefix skolem_prefix s 

671 
> strip_first_name_sep > fst > space_explode "@" 

672 
> hd > Int.fromString > the 

673 
in [k, num_binder_types T  k] end 

674 
else if original_name s <> s then 

675 
[num_binder_types T] 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

676 
else case def_of_const thy def_tables x of 
35718  677 
SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then 
678 
let val k = length (strip_abs_vars t') in 

679 
[k, num_binder_types T  k] 

680 
end 

681 
else 

682 
[num_binder_types T] 

683 
 NONE => [num_binder_types T] 

684 
fun intersect_formats _ [] = [] 

685 
 intersect_formats [] _ = [] 

686 
 intersect_formats ks1 ks2 = 

687 
let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in 

688 
intersect_formats (ks1' @ (if k1 > k2 then [k1  k2] else [])) 

689 
(ks2' @ (if k2 > k1 then [k2  k1] else [])) @ 

690 
[Int.min (k1, k2)] 

691 
end 

692 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

693 
fun lookup_format thy def_tables formats t = 
35718  694 
case AList.lookup (fn (SOME x, SOME y) => 
695 
(term_match thy) (x, y)  _ => false) 

696 
formats (SOME t) of 

697 
SOME format => format 

698 
 NONE => let val format = the (AList.lookup (op =) formats NONE) in 

699 
case t of 

700 
Const x => intersect_formats format 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

701 
(const_format thy def_tables x) 
35718  702 
 _ => format 
703 
end 

704 

705 
fun format_type default_format format T = 

706 
let 

707 
val T = uniterize_unarize_unbox_etc_type T 

708 
val format = format > filter (curry (op <) 0) 

709 
in 

710 
if forall (curry (op =) 1) format then 

711 
T 

712 
else 

713 
let 

714 
val (binder_Ts, body_T) = strip_type T 

715 
val batched = 

716 
binder_Ts 

717 
> map (format_type default_format default_format) 

718 
> rev > chunk_list_unevenly (rev format) 

719 
> map (HOLogic.mk_tupleT o rev) 

720 
in List.foldl (op >) body_T batched end 

721 
end 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

722 
fun format_term_type thy def_tables formats t = 
35718  723 
format_type (the (AList.lookup (op =) formats NONE)) 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

724 
(lookup_format thy def_tables formats t) (fastype_of t) 
35718  725 

726 
fun repair_special_format js m format = 

727 
m  1 downto 0 > chunk_list_unevenly (rev format) 

728 
> map (rev o filter_out (member (op =) js)) 

729 
> filter_out null > map length > rev 

730 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

731 
fun user_friendly_const ({thy, evals, def_tables, skolems, special_funs, ...} 
35718  732 
: hol_context) (base_name, step_name) formats = 
733 
let 

734 
val default_format = the (AList.lookup (op =) formats NONE) 

735 
fun do_const (x as (s, T)) = 

736 
(if String.isPrefix special_prefix s then 

737 
let 

738 
val do_term = map_aterms (fn Const x => fst (do_const x)  t' => t') 

739 
val (x' as (_, T'), js, ts) = 

740 
AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T) 

741 
> the_single 

742 
val max_j = List.last js 

743 
val Ts = List.take (binder_types T', max_j + 1) 

744 
val missing_js = filter_out (member (op =) js) (0 upto max_j) 

745 
val missing_Ts = filter_indices missing_js Ts 

746 
fun nth_missing_var n = 

747 
((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n) 

748 
val missing_vars = map nth_missing_var (0 upto length missing_js  1) 

749 
val vars = special_bounds ts @ missing_vars 

750 
val ts' = 

751 
map (fn j => 

752 
case AList.lookup (op =) (js ~~ ts) j of 

753 
SOME t => do_term t 

754 
 NONE => 

755 
Var (nth missing_vars 

756 
(find_index (curry (op =) j) missing_js))) 

757 
(0 upto max_j) 

758 
val t = do_const x' > fst 

759 
val format = 

760 
case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2) 

761 
 _ => false) formats (SOME t) of 

762 
SOME format => 

763 
repair_special_format js (num_binder_types T') format 

764 
 NONE => 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

765 
const_format thy def_tables x' 
35718  766 
> repair_special_format js (num_binder_types T') 
767 
> intersect_formats default_format 

768 
in 

769 
(list_comb (t, ts') > fold_rev abs_var vars, 

770 
format_type default_format format T) 

771 
end 

772 
else if String.isPrefix uncurry_prefix s then 

773 
let 

774 
val (ss, s') = unprefix uncurry_prefix s 

775 
> strip_first_name_sep >> space_explode "@" 

776 
in 

777 
if String.isPrefix step_prefix s' then 

778 
do_const (s', T) 

779 
else 

780 
let 

781 
val k = the (Int.fromString (hd ss)) 

782 
val j = the (Int.fromString (List.last ss)) 

783 
val (before_Ts, (tuple_T, rest_T)) = 

784 
strip_n_binders j T > (strip_n_binders 1 #>> hd) 

785 
val T' = before_Ts > dest_n_tuple_type k tuple_T > rest_T 

786 
in do_const (s', T') end 

787 
end 

788 
else if String.isPrefix unrolled_prefix s then 

789 
let val t = Const (original_name s, range_type T) in 

790 
(lambda (Free (iter_var_prefix, nat_T)) t, 

791 
format_type default_format 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

792 
(lookup_format thy def_tables formats t) T) 
35718  793 
end 
794 
else if String.isPrefix base_prefix s then 

795 
(Const (base_name, T > T) $ Const (unprefix base_prefix s, T), 

796 
format_type default_format default_format T) 

797 
else if String.isPrefix step_prefix s then 

798 
(Const (step_name, T > T) $ Const (unprefix step_prefix s, T), 

799 
format_type default_format default_format T) 

800 
else if String.isPrefix quot_normal_prefix s then 

38207
792b78e355e7
added support for "Abs_" and "Rep_" functions on quotient types
blanchet
parents:
38190
diff
changeset

801 
let val t = Const (nitpick_prefix ^ "quotient normal form", T) in 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

802 
(t, format_term_type thy def_tables formats t) 
35718  803 
end 
804 
else if String.isPrefix skolem_prefix s then 

805 
let 

806 
val ss = the (AList.lookup (op =) (!skolems) s) 

807 
val (Ts, Ts') = chop (length ss) (binder_types T) 

808 
val frees = map Free (ss ~~ Ts) 

809 
val s' = original_name s 

810 
in 

811 
(fold lambda frees (Const (s', Ts' > T)), 

812 
format_type default_format 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

813 
(lookup_format thy def_tables formats (Const x)) T) 
35718  814 
end 
815 
else if String.isPrefix eval_prefix s then 

816 
let 

817 
val t = nth evals (the (Int.fromString (unprefix eval_prefix s))) 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

818 
in (t, format_term_type thy def_tables formats t) end 
35718  819 
else 
820 
let val t = Const (original_name s, T) in 

41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

821 
(t, format_term_type thy def_tables formats t) 
35718  822 
end) 
823 
>> map_types uniterize_unarize_unbox_etc_type 

824 
>> shorten_names_in_term >> Term.map_abs_vars shortest_name 

825 
in do_const end 

826 

827 
fun assign_operator_for_const (s, T) = 

828 
if String.isPrefix ubfp_prefix s then 

37261  829 
if is_fun_type T then xsym "\<subseteq>" "<=" () 
830 
else xsym "\<le>" "<=" () 

35718  831 
else if String.isPrefix lbfp_prefix s then 
37261  832 
if is_fun_type T then xsym "\<supseteq>" ">=" () 
833 
else xsym "\<ge>" ">=" () 

35718  834 
else if original_name s <> s then 
835 
assign_operator_for_const (strip_first_name_sep s > snd, T) 

836 
else 

837 
"=" 

838 

839 
(** Model reconstruction **) 

840 

33192  841 
fun unfold_outer_the_binders (t as Const (@{const_name The}, _) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38284
diff
changeset

842 
$ Abs (s, T, Const (@{const_name HOL.eq}, _) 
33192  843 
$ Bound 0 $ t')) = 
844 
betapply (Abs (s, T, t'), t) > unfold_outer_the_binders 

845 
 unfold_outer_the_binders t = t 

846 
fun bisimilar_values _ 0 _ = true 

847 
 bisimilar_values coTs max_depth (t1, t2) = 

848 
let val T = fastype_of t1 in 

849 
if exists_subtype (member (op =) coTs) T then 

850 
let 

851 
val ((head1, args1), (head2, args2)) = 

852 
pairself (strip_comb o unfold_outer_the_binders) (t1, t2) 

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

853 
val max_depth = max_depth  (if member (op =) coTs T then 1 else 0) 
33192  854 
in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

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

856 
forall (bisimilar_values coTs max_depth) (args1 ~~ args2) 
33192  857 
end 
858 
else 

859 
t1 = t2 

860 
end 

861 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

862 
fun reconstruct_hol_model {show_datatypes, show_consts} 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

863 
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms, 
38209  864 
debug, whacks, binary_ints, destroy_constrs, specialize, 
41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

865 
star_linear_preds, total_consts, preconstrs, tac_timeout, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

866 
evals, case_names, def_tables, nondef_table, user_nondefs, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41791
diff
changeset

867 
simp_table, psimp_table, choice_spec_table, intro_table, 
36388  868 
ground_thm_table, ersatz_table, skolems, special_funs, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41791
diff
changeset

869 
unrolled_preds, wf_cache, constr_cache}, binarize, 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41791
diff
changeset

870 
card_assigns, bits, bisim_depth, datatypes, ofs} : scope) 
38170  871 
formats atomss real_frees pseudo_frees free_names sel_names nonsel_names 
872 
rel_table bounds = 

33192  873 
let 
35180
c57dba973391
more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents:
35179
diff
changeset

874 
val pool = Unsynchronized.ref [] 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

875 
val (wacky_names as (_, base_step_names), ctxt) = 
33192  876 
add_wacky_syntax ctxt 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

877 
val hol_ctxt = 
33192  878 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

879 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
38209  880 
whacks = whacks, binary_ints = binary_ints, 
881 
destroy_constrs = destroy_constrs, specialize = specialize, 

41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

882 
star_linear_preds = star_linear_preds, total_consts = total_consts, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

883 
preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

884 
case_names = case_names, def_tables = def_tables, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

885 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

886 
simp_table = simp_table, psimp_table = psimp_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

887 
choice_spec_table = choice_spec_table, intro_table = intro_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

888 
ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

889 
skolems = skolems, special_funs = special_funs, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

890 
unrolled_preds = unrolled_preds, wf_cache = wf_cache, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41803
diff
changeset

891 
constr_cache = constr_cache} 
36388  892 
val scope = 
893 
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns, 

894 
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} 

37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

895 
fun term_for_rep maybe_opt unfold = 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

896 
reconstruct_term maybe_opt unfold pool wacky_names scope atomss 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

897 
sel_names rel_table bounds 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

898 
val all_values = 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

899 
all_values_of_type pool wacky_names scope atomss sel_names rel_table 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

900 
bounds 
38126  901 
fun is_codatatype_wellformed (cos : datatype_spec list) 
902 
({typ, card, ...} : datatype_spec) = 

33192  903 
let 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

904 
val ts = all_values card typ 
33192  905 
val max_depth = Integer.sum (map #card cos) 
906 
in 

907 
forall (not o bisimilar_values (map #typ cos) max_depth) 

908 
(all_distinct_unordered_pairs_of ts) 

909 
end 

910 
fun pretty_for_assign name = 

911 
let 

912 
val (oper, (t1, T'), T) = 

913 
case name of 

914 
FreeName (s, T, _) => 

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

915 
let val t = Free (s, uniterize_unarize_unbox_etc_type T) in 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41472
diff
changeset

916 
("=", (t, format_term_type thy def_tables formats t), T) 
33192  917 
end 
918 
 ConstName (s, T, _) => 

919 
(assign_operator_for_const (s, T), 

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

920 
user_friendly_const hol_ctxt base_step_names formats (s, T), T) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

921 
 _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\ 
33192  922 
\pretty_for_assign", [name]) 
923 
val t2 = if rep_of name = Any then 

924 
Const (@{const_name undefined}, T') 

925 
else 

926 
tuple_list_for_name rel_table bounds name 

37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

927 
> term_for_rep (not (is_fully_representable_set name)) false 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

928 
T T' (rep_of name) 
33192  929 
in 
930 
Pretty.block (Pretty.breaks 

39118
12f3788be67b
turned show_all_types into proper configuration option;
wenzelm
parents:
38864
diff
changeset

931 
[Syntax.pretty_term (set_show_all_types ctxt) t1, 
33192  932 
Pretty.str oper, Syntax.pretty_term ctxt t2]) 
933 
end 

38126  934 
fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) = 
33192  935 
Pretty.block (Pretty.breaks 
38189  936 
(pretty_for_type ctxt typ :: 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

937 
(case typ of 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41039
diff
changeset

938 
Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"] 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

939 
 Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"] 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

940 
 _ => []) @ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

941 
[Pretty.str "=", 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

942 
Pretty.enum "," "{" "}" 
35712
77aa29bf14ee
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
blanchet
parents:
35711
diff
changeset

943 
(map (Syntax.pretty_term ctxt) (all_values card typ) @ 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset

944 
(if fun_from_pair complete false then [] 
37261  945 
else [Pretty.str (unrep ())]))])) 
33192  946 
fun integer_datatype T = 
947 
[{typ = T, card = card_of_type card_assigns T, co = false, 

38126  948 
standard = true, self_rec = true, complete = (false, false), 
949 
concrete = (true, true), deep = true, constrs = []}] 

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

950 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] 
33192  951 
val (codatatypes, datatypes) = 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34974
diff
changeset

952 
datatypes > filter #deep > List.partition #co 
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

953 
> append (integer_datatype int_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

954 
> is_standard_datatype thy stds nat_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

955 
? append (integer_datatype nat_T)) 
33192  956 
val block_of_datatypes = 
957 
if show_datatypes andalso not (null datatypes) then 

958 
[Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":") 

959 
(map pretty_for_datatype datatypes)] 

960 
else 

961 
[] 

962 
val block_of_codatatypes = 

963 
if show_datatypes andalso not (null codatatypes) then 

964 
[Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":") 

965 
(map pretty_for_datatype codatatypes)] 

966 
else 

967 
[] 

968 
fun block_of_names show title names = 

969 
if show andalso not (null names) then 

970 
Pretty.str (title ^ plural_s_for_list names ^ ":") 

971 
:: map (Pretty.indent indent_size o pretty_for_assign) 

972 
(sort_wrt (original_name o nickname_of) names) 

973 
else 

974 
[] 

38170  975 
fun free_name_for_term keep_all (x as (s, T)) = 
976 
case filter (curry (op =) x 

977 
o pairf nickname_of (uniterize_unarize_unbox_etc_type 

978 
o type_of)) free_names of 

979 
[name] => SOME name 

980 
 [] => if keep_all then SOME (FreeName (s, T, Any)) else NONE 

981 
 _ => raise TERM ("Nitpick_Model.reconstruct_hol_model.\ 

982 
\free_name_for_term", [Const x]) 

33192  983 
val (skolem_names, nonskolem_nonsel_names) = 
984 
List.partition is_skolem_name nonsel_names 

985 
val (eval_names, noneval_nonskolem_nonsel_names) = 

986 
List.partition (String.isPrefix eval_prefix o nickname_of) 

987 
nonskolem_nonsel_names 

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

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

989 
@{const_name bisim_iterator_max}] 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

990 
o nickname_of) 
38170  991 
> append (map_filter (free_name_for_term false) pseudo_frees) 
992 
val real_free_names = map_filter (free_name_for_term true) real_frees 

993 
val chunks = block_of_names true "Free variable" real_free_names @ 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

994 
block_of_names true "Skolem constant" skolem_names @ 
33192  995 
block_of_names true "Evaluated term" eval_names @ 
996 
block_of_datatypes @ block_of_codatatypes @ 

997 
block_of_names show_consts "Constant" 

998 
noneval_nonskolem_nonsel_names 

999 
in 

1000 
(Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"] 

1001 
else chunks), 

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

1002 
bisim_depth >= 0 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34126
diff
changeset

1003 
forall (is_codatatype_wellformed codatatypes) codatatypes) 
33192  1004 
end 
1005 

37262
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1006 
fun term_for_name pool scope atomss sel_names rel_table bounds name = 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1007 
let val T = type_of name in 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1008 
tuple_list_for_name rel_table bounds name 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1009 
> reconstruct_term (not (is_fully_representable_set name)) false pool 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1010 
(("", ""), ("", "")) scope atomss sel_names rel_table 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1011 
bounds T T (rep_of name) 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1012 
end 
c0fe8fa35771
don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
blanchet
parents:
37261
diff
changeset

1013 

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

1014 
fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...}, 
34998  1015 
card_assigns, ...}) 
33192  1016 
auto_timeout free_names sel_names rel_table bounds prop = 
1017 
let 

35076
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
35075
diff
changeset

1018 
val pool = Unsynchronized.ref [] 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

1019 
val atomss = [(NONE, [])] 
33192  1020 
fun free_type_assm (T, k) = 
1021 
let 

37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

1022 
fun atom j = nth_atom thy atomss pool true T j 
33192  1023 
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j 
1024 
val eqs = map equation_for_atom (index_seq 0 k) 

1025 
val compreh_assm = 

1026 
Const (@{const_name All}, (T > bool_T) > bool_T) 

1027 
$ Abs ("x", T, foldl1 HOLogic.mk_disj eqs) 

1028 
val distinct_assm = distinctness_formula T (map atom (index_seq 0 k)) 

34998  1029 
in s_conj (compreh_assm, distinct_assm) end 
33192  1030 
fun free_name_assm name = 
1031 
HOLogic.mk_eq (Free (nickname_of name, type_of name), 

37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

1032 
term_for_name pool scope atomss sel_names rel_table bounds 
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset

1033 
name) 
33192  1034 
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) 
1035 
val model_assms = map free_name_assm free_names 

34998  1036 
val assm = foldr1 s_conj (freeT_assms @ model_assms) 
33192  1037 
fun try_out negate = 
1038 
let 

1039 
val concl = (negate ? curry (op $) @{const Not}) 

35625  1040 
(Object_Logic.atomize_term thy prop) 
34998  1041 
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl)) 
33192  1042 
> map_types (map_type_tfree 
34998  1043 
(fn (s, []) => TFree (s, HOLogic.typeS) 
1044 
 x => TFree x)) 

1045 
val _ = if debug then 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39360
diff
changeset

1046 
Output.urgent_message ((if negate then "Genuineness" else "Spuriousness") ^ 
34998  1047 
" goal: " ^ Syntax.string_of_term ctxt prop ^ ".") 
1048 
else 

1049 
() 

1050 
val goal = prop > cterm_of thy > Goal.init 

33192  1051 
in 
1052 
(goal > SINGLE (DETERM_TIMEOUT auto_timeout 

1053 
(auto_tac (clasimpset_of ctxt))) 

1054 
> the > Goal.finish ctxt; true) 

1055 
handle THM _ => false 

1056 
 TimeLimit.TimeOut => false 

1057 
end 

1058 
in 

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

1059 
if try_out false then SOME true 
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

1060 
else if try_out true then SOME false 
33192  1061 
else NONE 
1062 
end 

1063 

1064 
end; 