author  blanchet 
Thu, 17 Dec 2009 15:22:11 +0100  
changeset 34124  c4628a1dcf75 
parent 34123  c4988215a691 
child 34126  8a2c5d7aff51 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_model.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2009 

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 

15 
type params = { 

16 
show_skolems: bool, 

17 
show_datatypes: bool, 

18 
show_consts: bool} 

19 

20 
structure NameTable : TABLE 

21 

22 
val tuple_list_for_name : 

23 
nut NameTable.table > Kodkod.raw_bound list > nut > int list list 

24 
val reconstruct_hol_model : 

25 
params > scope > (term option * int list) list > styp list > nut list 

26 
> nut list > nut list > nut NameTable.table > Kodkod.raw_bound list 

27 
> Pretty.T * bool 

28 
val prove_hol_model : 

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

30 
> Kodkod.raw_bound list > term > bool option 

31 
end; 

32 

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

33 
structure Nitpick_Model : NITPICK_MODEL = 
33192  34 
struct 
35 

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

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

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

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

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

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

41 
open Nitpick_Nut 
33192  42 

43 
type params = { 

44 
show_skolems: bool, 

45 
show_datatypes: bool, 

46 
show_consts: bool} 

47 

48 
val unknown = "?" 

49 
val unrep = "\<dots>" 

50 
val maybe_mixfix = "_\<^sup>?" 

51 
val base_mixfix = "_\<^bsub>base\<^esub>" 

52 
val step_mixfix = "_\<^bsub>step\<^esub>" 

53 
val abs_mixfix = "\<guillemotleft>_\<guillemotright>" 

54 
val non_opt_name = nitpick_prefix ^ "non_opt" 

55 

33884
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

56 
(* string > int > string *) 
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

57 
fun atom_suffix s j = 
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

58 
nat_subscript (j + 1) 
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

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

60 
? prefix "\<^isub>," 
33192  61 
(* string > typ > int > string *) 
62 
fun atom_name prefix (T as Type (s, _)) j = 

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

63 
prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j 
33192  64 
 atom_name prefix (T as TFree (s, _)) j = 
33884
a0c43f185fef
generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents:
33705
diff
changeset

65 
prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

66 
 atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], []) 
33192  67 
(* bool > typ > int > term *) 
68 
fun atom for_auto T j = 

69 
if for_auto then 

70 
Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T) 

71 
else 

72 
Const (atom_name "" T j, T) 

73 

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

74 
(* term * term > order *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

75 
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

76 
 nice_term_ord (t1, t2) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

77 
int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

78 
handle TERM ("dest_number", _) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

79 
case (t1, t2) of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

83 
 ord => ord) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

84 
 _ => TermOrd.term_ord (t1, t2) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

85 

33192  86 
(* nut NameTable.table > Kodkod.raw_bound list > nut > int list list *) 
87 
fun tuple_list_for_name rel_table bounds name = 

88 
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] 

89 

90 
(* term > term *) 

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

91 
fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

93 
 unbit_and_unbox_term (Const (@{const_name PairBox}, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

94 
Type ("fun", [T1, Type ("fun", [T2, T3])])) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

95 
$ t1 $ t2) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

96 
let val Ts = map unbit_and_unbox_type [T1, T2] in 
33192  97 
Const (@{const_name Pair}, Ts > Type ("*", Ts)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

98 
$ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 
33192  99 
end 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

100 
 unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

101 
 unbit_and_unbox_term (t1 $ t2) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

102 
unbit_and_unbox_term t1 $ unbit_and_unbox_term t2 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

103 
 unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

104 
 unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

105 
 unbit_and_unbox_term (Bound j) = Bound j 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

106 
 unbit_and_unbox_term (Abs (s, T, t')) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

107 
Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t') 
33192  108 

109 
(* typ > typ > (typ * typ) * (typ * typ) *) 

110 
fun factor_out_types (T1 as Type ("*", [T11, T12])) 

111 
(T2 as Type ("*", [T21, T22])) = 

112 
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in 

113 
if n1 = n2 then 

114 
let 

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

116 
in 

117 
((Type ("*", [T11, T11']), opt_T12'), 

118 
(Type ("*", [T21, T21']), opt_T22')) 

119 
end 

120 
else if n1 < n2 then 

121 
case factor_out_types T1 T21 of 

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

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

124 
(p1, (T21', SOME (Type ("*", [T22', T22])))) 

125 
else 

126 
swap (factor_out_types T2 T1) 

127 
end 

128 
 factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE)) 

129 
 factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22)) 

130 
 factor_out_types T1 T2 = ((T1, NONE), (T2, NONE)) 

131 

132 
(* bool > typ > typ > (term * term) list > term *) 

133 
fun make_plain_fun maybe_opt T1 T2 = 

134 
let 

135 
(* typ > typ > (term * term) list > term *) 

136 
fun aux T1 T2 [] = 

137 
Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined} 

138 
else non_opt_name, T1 > T2) 

139 
 aux T1 T2 ((t1, t2) :: ps) = 

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

140 
Const (@{const_name fun_upd}, (T1 > T2) > T1 > T2 > T1 > T2) 
33192  141 
$ aux T1 T2 ps $ t1 $ t2 
142 
in aux T1 T2 o rev end 

143 
(* term > bool *) 

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

144 
fun is_plain_fun (Const (s, _)) = 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

145 
(s = @{const_name undefined} orelse s = non_opt_name) 
33192  146 
 is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) = 
147 
is_plain_fun t0 

148 
 is_plain_fun _ = false 

149 
(* term > bool * (term list * term list) *) 

150 
val dest_plain_fun = 

151 
let 

152 
(* term > term list * term list *) 

153 
fun aux (Const (s, _)) = (s <> non_opt_name, ([], [])) 

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

155 
let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end 

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

156 
 aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) 
33192  157 
in apsnd (pairself rev) o aux end 
158 

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

159 
(* typ > typ > typ > term > term * term *) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

160 
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

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

162 
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

163 
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

164 
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

165 
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

166 
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end 
33192  167 
(* typ > term > term > term *) 
168 
fun pair_up (Type ("*", [T1', T2'])) 

169 
(t1 as Const (@{const_name Pair}, 

170 
Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12) 

171 
t2 = 

172 
if T1 = T1' then HOLogic.mk_prod (t1, t2) 

173 
else HOLogic.mk_prod (t11, pair_up T2' t12 t2) 

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

175 
(* typ > term > term list * term list > (term * term) list*) 

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

177 

178 
(* typ > typ > typ > term > term *) 

179 
fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t = 

180 
let 

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

181 
(* typ > typ > typ > typ > term > term *) 
5fad8e36dfb1
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents:
33558
diff
changeset

182 
fun do_curry T1 T1a T1b T2 t = 
33192  183 
let 
184 
val (maybe_opt, ps) = dest_plain_fun t 

185 
val ps = 

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

186 
ps >> map (break_in_two T1 T1a T1b) 
33192  187 
> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2)))) 
188 
> AList.coalesce (op =) 

189 
> map (apsnd (make_plain_fun maybe_opt T1b T2)) 

190 
in make_plain_fun maybe_opt T1a (T1b > T2) ps end 

191 
(* typ > typ > term > term *) 

192 
and do_uncurry T1 T2 t = 

193 
let 

194 
val (maybe_opt, tsp) = dest_plain_fun t 

195 
val ps = 

196 
tsp > op ~~ 

197 
> maps (fn (t1, t2) => 

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

199 
in make_plain_fun maybe_opt T1 T2 ps end 

200 
(* typ > typ > typ > typ > term > term *) 

201 
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' > T2') 

202 
 do_arrow T1' T2' T1 T2 

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

204 
Const (@{const_name fun_upd}, 

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

205 
(T1' > T2') > T1' > T2' > T1' > T2') 
33192  206 
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 
207 
 do_arrow _ _ _ _ t = 

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

208 
raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) 
33192  209 
and do_fun T1' T2' T1 T2 t = 
210 
case factor_out_types T1' T1 of 

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

212 
 ((_, 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

213 
t > do_curry T1 T1a T1b T2 > do_arrow T1' T2' T1a (T1b > T2) 
33192  214 
 ((T1a', SOME T1b'), (_, NONE)) => 
215 
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

216 
 _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], []) 
33192  217 
(* typ > typ > term > term *) 
218 
and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t = 

219 
do_fun T1' T2' T1 T2 t 

220 
 do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2])) 

221 
(Const (@{const_name Pair}, _) $ t1 $ t2) = 

222 
Const (@{const_name Pair}, Ts' > T') 

223 
$ do_term T1' T1 t1 $ do_term T2' T2 t2 

224 
 do_term T' T t = 

225 
if T = T' then t 

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

226 
else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], []) 
33192  227 
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

228 
 typecast_fun T' _ _ _ = raise TYPE ("Nitpick_Model.typecast_fun", [T'], []) 
33192  229 

230 
(* term > string *) 

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

232 
 truth_const_sort_key @{const False} = "2" 

233 
 truth_const_sort_key _ = "1" 

234 

235 
(* typ > term list > term *) 

236 
fun mk_tuple (Type ("*", [T1, T2])) ts = 

237 
HOLogic.mk_prod (mk_tuple T1 ts, 

238 
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1)))) 

239 
 mk_tuple _ (t :: _) = t 

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

240 
 mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) 
33192  241 

242 
(* string * string * string * string > scope > nut list > nut list 

243 
> nut list > nut NameTable.table > Kodkod.raw_bound list > typ > typ 

244 
> rep > int list list > term *) 

245 
fun reconstruct_term (maybe_name, base_name, step_name, abs_name) 

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

246 
({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} 
33192  247 
: scope) sel_names rel_table bounds = 
248 
let 

249 
val for_auto = (maybe_name = "") 

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

250 
(* int list list > int *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

254 
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

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

256 
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

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

258 
end 
33192  259 
(* bool > typ > typ > (term * term) list > term *) 
260 
fun make_set maybe_opt T1 T2 = 

261 
let 

262 
val empty_const = Const (@{const_name Set.empty}, T1 > T2) 

263 
val insert_const = Const (@{const_name insert}, 

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

264 
T1 > (T1 > T2) > T1 > T2) 
33192  265 
(* (term * term) list > term *) 
266 
fun aux [] = 

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

267 
if maybe_opt andalso not (is_complete_type datatypes T1) then 
33192  268 
insert_const $ Const (unrep, T1) $ empty_const 
269 
else 

270 
empty_const 

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

272 
aux zs > t2 <> @{const False} 

273 
? curry (op $) (insert_const 

274 
$ (t1 > t2 <> @{const True} 

275 
? curry (op $) 

276 
(Const (maybe_name, 

277 
T1 > T1)))) 

278 
in aux end 

279 
(* typ > typ > typ > (term * term) list > term *) 

280 
fun make_map T1 T2 T2' = 

281 
let 

282 
val update_const = Const (@{const_name fun_upd}, 

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

283 
(T1 > T2) > T1 > T2 > T1 > T2) 
33192  284 
(* (term * term) list > term *) 
285 
fun aux' [] = Const (@{const_name Map.empty}, T1 > T2) 

286 
 aux' ((t1, t2) :: ps) = 

287 
(case t2 of 

288 
Const (@{const_name None}, _) => aux' ps 

289 
 _ => update_const $ aux' ps $ t1 $ t2) 

290 
fun aux ps = 

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

291 
if not (is_complete_type datatypes T1) then 
33192  292 
update_const $ aux' ps $ Const (unrep, T1) 
293 
$ (Const (@{const_name Some}, T2' > T2) $ Const (unknown, T2')) 

294 
else 

295 
aux' ps 

296 
in aux end 

297 
(* typ list > term > term *) 

298 
fun setify_mapify_funs Ts t = 

299 
(case fastype_of1 (Ts, t) of 

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

301 
if is_plain_fun t then 

302 
case T2 of 

303 
@{typ bool} => 

304 
let 

305 
val (maybe_opt, ts_pair) = 

306 
dest_plain_fun t > pairself (map (setify_mapify_funs Ts)) 

307 
in 

308 
make_set maybe_opt T1 T2 

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

310 
end 

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

312 
let 

313 
val ts_pair = snd (dest_plain_fun t) 

314 
> pairself (map (setify_mapify_funs Ts)) 

315 
in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end 

316 
 _ => raise SAME () 

317 
else 

318 
raise SAME () 

319 
 _ => raise SAME ()) 

320 
handle SAME () => 

321 
case t of 

322 
t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2 

323 
 Abs (s, T, t') => Abs (s, T, setify_mapify_funs (T :: Ts) t') 

324 
 _ => t 

325 
(* bool > typ > typ > typ > term list > term list > term *) 

326 
fun make_fun maybe_opt T1 T2 T' ts1 ts2 = 

327 
ts1 ~~ ts2 > T1 = @{typ bisim_iterator} ? rev 

328 
> make_plain_fun (maybe_opt andalso not for_auto) T1 T2 

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

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

330 
> typecast_fun (unbit_and_unbox_type T') 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

331 
(unbit_and_unbox_type T1) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

332 
(unbit_and_unbox_type T2) 
33192  333 
(* (typ * int) list > typ > typ > int > term *) 
334 
fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j = 

335 
let 

336 
val k1 = card_of_type card_assigns T1 

337 
val k2 = card_of_type card_assigns T2 

338 
in 

339 
term_for_rep seen T T' (Vect (k1, Atom (k2, 0))) 

340 
[nth_combination (replicate k1 (k2, 0)) j] 

341 
handle General.Subscript => 

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

342 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", 
33192  343 
signed_string_of_int j ^ " for " ^ 
344 
string_for_rep (Vect (k1, Atom (k2, 0)))) 

345 
end 

346 
 term_for_atom seen (Type ("*", [T1, T2])) _ j = 

347 
let val k1 = card_of_type card_assigns T1 in 

348 
list_comb (HOLogic.pair_const T1 T2, 

349 
map2 (fn T => term_for_atom seen T T) [T1, T2] 

350 
[j div k1, j mod k1]) 

351 
end 

352 
 term_for_atom seen @{typ prop} _ j = 

353 
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j) 

354 
 term_for_atom _ @{typ bool} _ j = 

355 
if j = 0 then @{const False} else @{const True} 

356 
 term_for_atom _ @{typ unit} _ _ = @{const Unity} 

357 
 term_for_atom seen T _ j = 

358 
if T = nat_T then 

359 
HOLogic.mk_number nat_T j 

360 
else if T = int_T then 

361 
HOLogic.mk_number int_T 

362 
(int_for_atom (card_of_type card_assigns int_T, 0) j) 

363 
else if is_fp_iterator_type T then 

364 
HOLogic.mk_number nat_T (card_of_type card_assigns T  j  1) 

365 
else if T = @{typ bisim_iterator} then 

366 
HOLogic.mk_number nat_T j 

367 
else case datatype_spec datatypes T of 

368 
NONE => atom for_auto T j 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

369 
 SOME {shallow = true, ...} => atom for_auto T j 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

370 
 SOME {co, constrs, ...} => 
33192  371 
let 
372 
(* styp > int list *) 

373 
fun tuples_for_const (s, T) = 

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

375 
(* unit > indexname * typ *) 

376 
fun var () = ((atom_name "" T j, 0), T) 

377 
val discr_jsss = map (tuples_for_const o discr_for_constr o #const) 

378 
constrs 

379 
val real_j = j + offset_of_type ofs T 

380 
val constr_x as (constr_s, constr_T) = 

381 
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

382 
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

383 
else NONE) 
33192  384 
(discr_jsss ~~ constrs) > the 
385 
val arg_Ts = curried_binder_types constr_T 

386 
val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x) 

387 
(index_seq 0 (length arg_Ts)) 

388 
val sel_Rs = 

389 
map (fn x => get_first 

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

391 
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

392 
 u => raise NUT ("Nitpick_Model.reconstruct_\ 
33192  393 
\term.term_for_atom", [u])) 
394 
sel_names > the) sel_xs 

395 
val arg_Rs = map (snd o dest_Func) sel_Rs 

396 
val sel_jsss = map tuples_for_const sel_xs 

397 
val arg_jsss = 

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

399 
else NONE)) sel_jsss 

400 
val uncur_arg_Ts = binder_types constr_T 

401 
in 

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

402 
if co andalso member (op =) seen (T, j) then 
33192  403 
Var (var ()) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

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

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

407 
(value_of_bits (the_single arg_jsss)) 
33192  408 
else 
409 
let 

410 
val seen = seen > co ? cons (T, j) 

411 
val ts = 

412 
if length arg_Ts = 0 then 

413 
[] 

414 
else 

415 
map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs 

416 
arg_jsss 

417 
> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) 

418 
> dest_n_tuple (length uncur_arg_Ts) 

419 
val t = 

420 
if constr_s = @{const_name Abs_Frac} then 

421 
let 

422 
val num_T = body_type T 

423 
(* int > term *) 

424 
val mk_num = HOLogic.mk_number num_T 

425 
in 

426 
case ts of 

427 
[Const (@{const_name Pair}, _) $ t1 $ t2] => 

428 
(case snd (HOLogic.dest_number t1) of 

429 
0 => mk_num 0 

430 
 n1 => case HOLogic.dest_number t2 > snd of 

431 
1 => mk_num n1 

432 
 n2 => Const (@{const_name HOL.divide}, 

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

433 
num_T > num_T > num_T) 
33192  434 
$ mk_num n1 $ mk_num n2) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

435 
 _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\ 
33192  436 
\for_atom (Abs_Frac)", ts) 
437 
end 

438 
else if not for_auto andalso is_abs_fun thy constr_x then 

439 
Const (abs_name, constr_T) $ the_single ts 

440 
else 

441 
list_comb (Const constr_x, ts) 

442 
in 

443 
if co then 

444 
let val var = var () in 

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

445 
if exists_subterm (curry (op =) (Var var)) t then 
33192  446 
Const (@{const_name The}, (T > bool_T) > T) 
447 
$ Abs ("\<omega>", T, 

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

448 
Const (@{const_name "op ="}, T > T > bool_T) 
33192  449 
$ Bound 0 $ abstract_over (Var var, t)) 
450 
else 

451 
t 

452 
end 

453 
else 

454 
t 

455 
end 

456 
end 

457 
(* (typ * int) list > int > rep > typ > typ > typ > int list 

458 
> term *) 

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

460 
make_fun true T1 T2 T' (map (term_for_atom seen T1 T1) (index_seq 0 k)) 

461 
(map (term_for_rep seen T2 T2 R o single) 

462 
(batch_list (arity_of_rep R) js)) 

463 
(* (typ * int) list > typ > typ > rep > int list list > term *) 

464 
and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 

465 
 term_for_rep seen T T' (R as Atom (k, j0)) [[j]] = 

466 
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j  j0) 

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

467 
else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R]) 
33192  468 
 term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] = 
469 
let 

470 
val arity1 = arity_of_rep R1 

471 
val (js1, js2) = chop arity1 js 

472 
in 

473 
list_comb (HOLogic.pair_const T1 T2, 

474 
map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2] 

475 
[[js1], [js2]]) 

476 
end 

477 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] = 

478 
term_for_vect seen k R' T1 T2 T' js 

479 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut)) 

480 
jss = 

481 
let 

482 
val jss1 = all_combinations_for_rep R1 

483 
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 

484 
val ts2 = 

485 
map (fn js => term_for_rep seen T2 T2 (Atom (2, 0)) 

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

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

487 
jss1 
33192  488 
in make_fun false T1 T2 T' ts1 ts2 end 
489 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = 

490 
let 

491 
val arity1 = arity_of_rep R1 

492 
val jss1 = all_combinations_for_rep R1 

493 
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 

494 
val grouped_jss2 = AList.group (op =) (map (chop arity1) jss) 

495 
val ts2 = map (term_for_rep seen T2 T2 R2 o the_default [] 

496 
o AList.lookup (op =) grouped_jss2) jss1 

497 
in make_fun true T1 T2 T' ts1 ts2 end 

498 
 term_for_rep seen T T' (Opt R) jss = 

499 
if null jss then Const (unknown, T) else term_for_rep seen T T' R jss 

500 
 term_for_rep seen T _ R jss = 

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

501 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", 
33192  502 
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ 
503 
string_of_int (length jss)) 

504 
in 

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

505 
(not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

506 
oooo term_for_rep [] 
33192  507 
end 
508 

509 
(* scope > nut list > nut NameTable.table > Kodkod.raw_bound list > nut 

510 
> term *) 

511 
fun term_for_name scope sel_names rel_table bounds name = 

512 
let val T = type_of name in 

513 
tuple_list_for_name rel_table bounds name 

514 
> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T 

515 
(rep_of name) 

516 
end 

517 

518 
(* Proof.context 

519 
> (string * string * string * string * string) * Proof.context *) 

520 
fun add_wacky_syntax ctxt = 

521 
let 

522 
(* term > string *) 

523 
val name_of = fst o dest_Const 

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

525 
val (maybe_t, thy) = 

33202  526 
Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), 
527 
Mixfix (maybe_mixfix, [1000], 1000)) thy 

33192  528 
val (base_t, thy) = 
33202  529 
Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), 
530 
Mixfix (base_mixfix, [1000], 1000)) thy 

33192  531 
val (step_t, thy) = 
33202  532 
Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), 
533 
Mixfix (step_mixfix, [1000], 1000)) thy 

33192  534 
val (abs_t, thy) = 
33202  535 
Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), 
536 
Mixfix (abs_mixfix, [40], 40)) thy 

33192  537 
in 
538 
((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t), 

539 
ProofContext.transfer_syntax thy ctxt) 

540 
end 

541 

542 
(* term > term *) 

543 
fun unfold_outer_the_binders (t as Const (@{const_name The}, _) 

544 
$ Abs (s, T, Const (@{const_name "op ="}, _) 

545 
$ Bound 0 $ t')) = 

546 
betapply (Abs (s, T, t'), t) > unfold_outer_the_binders 

547 
 unfold_outer_the_binders t = t 

548 
(* typ list > int > term * term > bool *) 

549 
fun bisimilar_values _ 0 _ = true 

550 
 bisimilar_values coTs max_depth (t1, t2) = 

551 
let val T = fastype_of t1 in 

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

553 
let 

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

555 
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

556 
val max_depth = max_depth  (if member (op =) coTs T then 1 else 0) 
33192  557 
in 
558 
head1 = head2 

559 
andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2) 

560 
end 

561 
else 

562 
t1 = t2 

563 
end 

564 

565 
(* params > scope > (term option * int list) list > styp list > nut list 

566 
> nut list > nut list > nut NameTable.table > Kodkod.raw_bound list 

567 
> Pretty.T * bool *) 

568 
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} 

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

569 
({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

570 
debug, binary_ints, destroy_constrs, specialize, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

571 
skolemize, star_linear_preds, uncurry, fast_descrs, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

572 
tac_timeout, evals, case_names, def_table, nondef_table, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

573 
user_nondefs, simp_table, psimp_table, intro_table, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

574 
ground_thm_table, ersatz_table, skolems, special_funs, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

575 
unrolled_preds, wf_cache, constr_cache}, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

576 
card_assigns, bits, bisim_depth, datatypes, ofs} : scope) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

577 
formats all_frees free_names sel_names nonsel_names rel_table bounds = 
33192  578 
let 
579 
val (wacky_names as (_, base_name, step_name, _), ctxt) = 

580 
add_wacky_syntax ctxt 

581 
val ext_ctxt = 

582 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 

583 
wfs = wfs, user_axioms = user_axioms, debug = debug, 

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

584 
binary_ints = binary_ints, destroy_constrs = destroy_constrs, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

585 
specialize = specialize, skolemize = skolemize, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

586 
star_linear_preds = star_linear_preds, uncurry = uncurry, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

587 
fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

588 
case_names = case_names, def_table = def_table, 
33192  589 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
590 
simp_table = simp_table, psimp_table = psimp_table, 

591 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

592 
ersatz_table = ersatz_table, skolems = skolems, 

593 
special_funs = special_funs, unrolled_preds = unrolled_preds, 

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

594 
wf_cache = wf_cache, constr_cache = constr_cache} 
33192  595 
val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

596 
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

597 
ofs = ofs} 
33192  598 
(* typ > typ > rep > int list list > term *) 
599 
val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table 

600 
bounds 

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

601 
(* nat > typ > nat > typ *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

602 
fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

603 
(* nat > typ > typ list *) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

604 
fun all_values_of_type card T = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

605 
index_seq 0 card > map (nth_value_of_type card T) > sort nice_term_ord 
33192  606 
(* dtype_spec list > dtype_spec > bool *) 
607 
fun is_codatatype_wellformed (cos : dtype_spec list) 

608 
({typ, card, ...} : dtype_spec) = 

609 
let 

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

610 
val ts = all_values_of_type card typ 
33192  611 
val max_depth = Integer.sum (map #card cos) 
612 
in 

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

614 
(all_distinct_unordered_pairs_of ts) 

615 
end 

616 
(* string > Pretty.T *) 

617 
fun pretty_for_assign name = 

618 
let 

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

620 
case name of 

621 
FreeName (s, T, _) => 

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

622 
let val t = Free (s, unbit_and_unbox_type T) in 
33192  623 
("=", (t, format_term_type thy def_table formats t), T) 
624 
end 

625 
 ConstName (s, T, _) => 

626 
(assign_operator_for_const (s, T), 

627 
user_friendly_const ext_ctxt (base_name, step_name) formats (s, T), 

628 
T) 

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

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

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

633 
else 

634 
tuple_list_for_name rel_table bounds name 

635 
> term_for_rep T T' (rep_of name) 

636 
in 

637 
Pretty.block (Pretty.breaks 

33571  638 
[setmp_show_all_types (Syntax.pretty_term ctxt) t1, 
33192  639 
Pretty.str oper, Syntax.pretty_term ctxt t2]) 
640 
end 

641 
(* dtype_spec > Pretty.T *) 

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

642 
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = 
33192  643 
Pretty.block (Pretty.breaks 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

644 
[Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=", 
33192  645 
Pretty.enum "," "{" "}" 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

646 
(map (Syntax.pretty_term ctxt) (all_values_of_type card typ) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

647 
@ (if complete then [] else [Pretty.str unrep]))]) 
33192  648 
(* typ > dtype_spec list *) 
649 
fun integer_datatype T = 

650 
[{typ = T, card = card_of_type card_assigns T, co = false, 

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

651 
complete = false, concrete = true, shallow = false, constrs = []}] 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

652 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] 
33192  653 
val (codatatypes, datatypes) = 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

654 
datatypes > filter_out #shallow 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

655 
> List.partition #co 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

656 
> append (integer_datatype nat_T @ integer_datatype int_T) 
33192  657 
val block_of_datatypes = 
658 
if show_datatypes andalso not (null datatypes) then 

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

660 
(map pretty_for_datatype datatypes)] 

661 
else 

662 
[] 

663 
val block_of_codatatypes = 

664 
if show_datatypes andalso not (null codatatypes) then 

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

666 
(map pretty_for_datatype codatatypes)] 

667 
else 

668 
[] 

669 
(* bool > string > nut list > Pretty.T list *) 

670 
fun block_of_names show title names = 

671 
if show andalso not (null names) then 

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

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

674 
(sort_wrt (original_name o nickname_of) names) 

675 
else 

676 
[] 

677 
val (skolem_names, nonskolem_nonsel_names) = 

678 
List.partition is_skolem_name nonsel_names 

679 
val (eval_names, noneval_nonskolem_nonsel_names) = 

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

681 
nonskolem_nonsel_names 

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

682 
> filter_out (curry (op =) @{const_name bisim_iterator_max} 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

683 
o nickname_of) 
33192  684 
val free_names = 
685 
map (fn x as (s, T) => 

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

686 
case filter (curry (op =) x 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

687 
o pairf nickname_of (unbit_and_unbox_type o type_of)) 
33192  688 
free_names of 
689 
[name] => name 

690 
 [] => FreeName (s, T, Any) 

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

691 
 _ => raise TERM ("Nitpick_Model.reconstruct_hol_model", 
33192  692 
[Const x])) all_frees 
693 
val chunks = block_of_names true "Free variable" free_names @ 

694 
block_of_names show_skolems "Skolem constant" skolem_names @ 

695 
block_of_names true "Evaluated term" eval_names @ 

696 
block_of_datatypes @ block_of_codatatypes @ 

697 
block_of_names show_consts "Constant" 

698 
noneval_nonskolem_nonsel_names 

699 
in 

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

701 
else chunks), 

702 
bisim_depth >= 0 

703 
orelse forall (is_codatatype_wellformed codatatypes) codatatypes) 

704 
end 

705 

706 
(* scope > Time.time option > nut list > nut list > nut NameTable.table 

707 
> Kodkod.raw_bound list > term > bool option *) 

708 
fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...}) 

709 
auto_timeout free_names sel_names rel_table bounds prop = 

710 
let 

711 
(* typ * int > term *) 

712 
fun free_type_assm (T, k) = 

713 
let 

714 
(* int > term *) 

715 
val atom = atom true T 

716 
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j 

717 
val eqs = map equation_for_atom (index_seq 0 k) 

718 
val compreh_assm = 

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

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

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

722 
in HOLogic.mk_conj (compreh_assm, distinct_assm) end 

723 
(* nut > term *) 

724 
fun free_name_assm name = 

725 
HOLogic.mk_eq (Free (nickname_of name, type_of name), 

726 
term_for_name scope sel_names rel_table bounds name) 

727 
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns) 

728 
val model_assms = map free_name_assm free_names 

729 
val assm = List.foldr HOLogic.mk_conj @{const True} 

730 
(freeT_assms @ model_assms) 

731 
(* bool > bool *) 

732 
fun try_out negate = 

733 
let 

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

735 
(ObjectLogic.atomize_term thy prop) 

736 
val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl)) 

737 
> map_types (map_type_tfree 

738 
(fn (s, []) => TFree (s, HOLogic.typeS) 

739 
 x => TFree x)) 

740 
> cterm_of thy > Goal.init 

741 
in 

742 
(goal > SINGLE (DETERM_TIMEOUT auto_timeout 

743 
(auto_tac (clasimpset_of ctxt))) 

744 
> the > Goal.finish ctxt; true) 

745 
handle THM _ => false 

746 
 TimeLimit.TimeOut => false 

747 
end 

748 
in 

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

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

750 
else if try_out true then SOME false 
33192  751 
else NONE 
752 
end 

753 

754 
end; 