author  blanchet 
Thu, 29 Oct 2009 15:24:52 +0100  
changeset 33571  3655e51f9958 
parent 33565  5fad8e36dfb1 
child 33580  45c33e97cb86 
permissions  rwrr 
33192  1 
(* Title: HOL/Nitpick/Tools/nitpick_model.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Copyright 2009 

4 

5 
Model reconstruction for Nitpick. 

6 
*) 

7 

8 
signature NITPICK_MODEL = 

9 
sig 

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

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

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

12 
type nut = Nitpick_Nut.nut 
33192  13 

14 
type params = { 

15 
show_skolems: bool, 

16 
show_datatypes: bool, 

17 
show_consts: bool} 

18 

19 
structure NameTable : TABLE 

20 

21 
val tuple_list_for_name : 

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

23 
val reconstruct_hol_model : 

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

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

26 
> Pretty.T * bool 

27 
val prove_hol_model : 

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

29 
> Kodkod.raw_bound list > term > bool option 

30 
end; 

31 

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

32 
structure Nitpick_Model : NITPICK_MODEL = 
33192  33 
struct 
34 

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

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

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

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

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

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

40 
open Nitpick_Nut 
33192  41 

42 
type params = { 

43 
show_skolems: bool, 

44 
show_datatypes: bool, 

45 
show_consts: bool} 

46 

47 
val unknown = "?" 

48 
val unrep = "\<dots>" 

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

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

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

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

53 
val non_opt_name = nitpick_prefix ^ "non_opt" 

54 

55 
(* string > typ > int > string *) 

56 
fun atom_name prefix (T as Type (s, _)) j = 

57 
prefix ^ substring (short_name s, 0, 1) ^ nat_subscript (j + 1) 

58 
 atom_name prefix (T as TFree (s, _)) j = 

59 
prefix ^ perhaps (try (unprefix "'")) s ^ nat_subscript (j + 1) 

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

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

63 
if for_auto then 

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

65 
else 

66 
Const (atom_name "" T j, T) 

67 

68 
(* nut NameTable.table > Kodkod.raw_bound list > nut > int list list *) 

69 
fun tuple_list_for_name rel_table bounds name = 

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

71 

72 
(* term > term *) 

73 
fun unbox_term (Const (@{const_name FunBox}, _) $ t1) = unbox_term t1 

74 
 unbox_term (Const (@{const_name PairBox}, 

75 
Type ("fun", [T1, Type ("fun", [T2, T3])])) $ t1 $ t2) = 

76 
let val Ts = map unbox_type [T1, T2] in 

77 
Const (@{const_name Pair}, Ts > Type ("*", Ts)) 

78 
$ unbox_term t1 $ unbox_term t2 

79 
end 

80 
 unbox_term (Const (s, T)) = Const (s, unbox_type T) 

81 
 unbox_term (t1 $ t2) = unbox_term t1 $ unbox_term t2 

82 
 unbox_term (Free (s, T)) = Free (s, unbox_type T) 

83 
 unbox_term (Var (x, T)) = Var (x, unbox_type T) 

84 
 unbox_term (Bound j) = Bound j 

85 
 unbox_term (Abs (s, T, t')) = Abs (s, unbox_type T, unbox_term t') 

86 

87 
(* typ > typ > (typ * typ) * (typ * typ) *) 

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

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

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

91 
if n1 = n2 then 

92 
let 

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

94 
in 

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

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

97 
end 

98 
else if n1 < n2 then 

99 
case factor_out_types T1 T21 of 

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

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

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

103 
else 

104 
swap (factor_out_types T2 T1) 

105 
end 

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

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

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

109 

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

111 
fun make_plain_fun maybe_opt T1 T2 = 

112 
let 

113 
(* typ > typ > (term * term) list > term *) 

114 
fun aux T1 T2 [] = 

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

116 
else non_opt_name, T1 > T2) 

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

118 
Const (@{const_name fun_upd}, [T1 > T2, T1, T2] > T1 > T2) 

119 
$ aux T1 T2 ps $ t1 $ t2 

120 
in aux T1 T2 o rev end 

121 
(* term > bool *) 

122 
fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name] 

123 
 is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) = 

124 
is_plain_fun t0 

125 
 is_plain_fun _ = false 

126 
(* term > bool * (term list * term list) *) 

127 
val dest_plain_fun = 

128 
let 

129 
(* term > term list * term list *) 

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

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

132 
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

133 
 aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) 
33192  134 
in apsnd (pairself rev) o aux end 
135 

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

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

137 
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

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

139 
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

140 
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

141 
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

142 
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

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

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

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

148 
t2 = 

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

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

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

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

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

154 

155 
(* typ > typ > typ > term > term *) 

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

157 
let 

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

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

159 
fun do_curry T1 T1a T1b T2 t = 
33192  160 
let 
161 
val (maybe_opt, ps) = dest_plain_fun t 

162 
val ps = 

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

163 
ps >> map (break_in_two T1 T1a T1b) 
33192  164 
> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2)))) 
165 
> AList.coalesce (op =) 

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

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

168 
(* typ > typ > term > term *) 

169 
and do_uncurry T1 T2 t = 

170 
let 

171 
val (maybe_opt, tsp) = dest_plain_fun t 

172 
val ps = 

173 
tsp > op ~~ 

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

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

176 
in make_plain_fun maybe_opt T1 T2 ps end 

177 
(* typ > typ > typ > typ > term > term *) 

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

179 
 do_arrow T1' T2' T1 T2 

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

181 
Const (@{const_name fun_upd}, 

182 
[T1' > T2', T1', T2'] > T1' > T2') 

183 
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2 

184 
 do_arrow _ _ _ _ t = 

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

185 
raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t]) 
33192  186 
and do_fun T1' T2' T1 T2 t = 
187 
case factor_out_types T1' T1 of 

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

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

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

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

196 
do_fun T1' T2' T1 T2 t 

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

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

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

200 
$ do_term T1' T1 t1 $ do_term T2' T2 t2 

201 
 do_term T' T t = 

202 
if T = T' then t 

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

203 
else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], []) 
33192  204 
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

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

207 
(* term > string *) 

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

209 
 truth_const_sort_key @{const False} = "2" 

210 
 truth_const_sort_key _ = "1" 

211 

212 
(* typ > term list > term *) 

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

214 
HOLogic.mk_prod (mk_tuple T1 ts, 

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

216 
 mk_tuple _ (t :: _) = t 

217 

218 
(* string * string * string * string > scope > nut list > nut list 

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

220 
> rep > int list list > term *) 

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

222 
({ext_ctxt as {thy, ctxt, ...}, card_assigns, datatypes, ofs, ...} 

223 
: scope) sel_names rel_table bounds = 

224 
let 

225 
val for_auto = (maybe_name = "") 

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

227 
fun make_set maybe_opt T1 T2 = 

228 
let 

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

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

231 
[T1, T1 > T2] > T1 > T2) 

232 
(* (term * term) list > term *) 

233 
fun aux [] = 

234 
if maybe_opt andalso not (is_precise_type datatypes T1) then 

235 
insert_const $ Const (unrep, T1) $ empty_const 

236 
else 

237 
empty_const 

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

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

240 
? curry (op $) (insert_const 

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

242 
? curry (op $) 

243 
(Const (maybe_name, 

244 
T1 > T1)))) 

245 
in aux end 

246 
(* typ > typ > typ > (term * term) list > term *) 

247 
fun make_map T1 T2 T2' = 

248 
let 

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

250 
[T1 > T2, T1, T2] > T1 > T2) 

251 
(* (term * term) list > term *) 

252 
fun aux' [] = Const (@{const_name Map.empty}, T1 > T2) 

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

254 
(case t2 of 

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

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

257 
fun aux ps = 

258 
if not (is_precise_type datatypes T1) then 

259 
update_const $ aux' ps $ Const (unrep, T1) 

260 
$ (Const (@{const_name Some}, T2' > T2) $ Const (unknown, T2')) 

261 
else 

262 
aux' ps 

263 
in aux end 

264 
(* typ list > term > term *) 

265 
fun setify_mapify_funs Ts t = 

266 
(case fastype_of1 (Ts, t) of 

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

268 
if is_plain_fun t then 

269 
case T2 of 

270 
@{typ bool} => 

271 
let 

272 
val (maybe_opt, ts_pair) = 

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

274 
in 

275 
make_set maybe_opt T1 T2 

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

277 
end 

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

279 
let 

280 
val ts_pair = snd (dest_plain_fun t) 

281 
> pairself (map (setify_mapify_funs Ts)) 

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

283 
 _ => raise SAME () 

284 
else 

285 
raise SAME () 

286 
 _ => raise SAME ()) 

287 
handle SAME () => 

288 
case t of 

289 
t1 $ t2 => setify_mapify_funs Ts t1 $ setify_mapify_funs Ts t2 

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

291 
 _ => t 

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

293 
fun make_fun maybe_opt T1 T2 T' ts1 ts2 = 

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

295 
> make_plain_fun (maybe_opt andalso not for_auto) T1 T2 

296 
> unbox_term 

297 
> typecast_fun (unbox_type T') (unbox_type T1) (unbox_type T2) 

298 
(* (typ * int) list > typ > typ > int > term *) 

299 
fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j = 

300 
let 

301 
val k1 = card_of_type card_assigns T1 

302 
val k2 = card_of_type card_assigns T2 

303 
in 

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

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

306 
handle General.Subscript => 

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

307 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom", 
33192  308 
signed_string_of_int j ^ " for " ^ 
309 
string_for_rep (Vect (k1, Atom (k2, 0)))) 

310 
end 

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

312 
let val k1 = card_of_type card_assigns T1 in 

313 
list_comb (HOLogic.pair_const T1 T2, 

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

315 
[j div k1, j mod k1]) 

316 
end 

317 
 term_for_atom seen @{typ prop} _ j = 

318 
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j) 

319 
 term_for_atom _ @{typ bool} _ j = 

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

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

322 
 term_for_atom seen T _ j = 

323 
if T = nat_T then 

324 
HOLogic.mk_number nat_T j 

325 
else if T = int_T then 

326 
HOLogic.mk_number int_T 

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

328 
else if is_fp_iterator_type T then 

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

330 
else if T = @{typ bisim_iterator} then 

331 
HOLogic.mk_number nat_T j 

332 
else case datatype_spec datatypes T of 

333 
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

334 
 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

335 
 SOME {co, constrs, ...} => 
33192  336 
let 
337 
(* styp > int list *) 

338 
fun tuples_for_const (s, T) = 

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

340 
(* unit > indexname * typ *) 

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

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

343 
constrs 

344 
val real_j = j + offset_of_type ofs T 

345 
val constr_x as (constr_s, constr_T) = 

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

347 
if [real_j] mem jss then SOME const else NONE) 

348 
(discr_jsss ~~ constrs) > the 

349 
val arg_Ts = curried_binder_types constr_T 

350 
val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x) 

351 
(index_seq 0 (length arg_Ts)) 

352 
val sel_Rs = 

353 
map (fn x => get_first 

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

355 
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

356 
 u => raise NUT ("Nitpick_Model.reconstruct_\ 
33192  357 
\term.term_for_atom", [u])) 
358 
sel_names > the) sel_xs 

359 
val arg_Rs = map (snd o dest_Func) sel_Rs 

360 
val sel_jsss = map tuples_for_const sel_xs 

361 
val arg_jsss = 

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

363 
else NONE)) sel_jsss 

364 
val uncur_arg_Ts = binder_types constr_T 

365 
in 

366 
if co andalso (T, j) mem seen then 

367 
Var (var ()) 

368 
else 

369 
let 

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

371 
val ts = 

372 
if length arg_Ts = 0 then 

373 
[] 

374 
else 

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

376 
arg_jsss 

377 
> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) 

378 
> dest_n_tuple (length uncur_arg_Ts) 

379 
val t = 

380 
if constr_s = @{const_name Abs_Frac} then 

381 
let 

382 
val num_T = body_type T 

383 
(* int > term *) 

384 
val mk_num = HOLogic.mk_number num_T 

385 
in 

386 
case ts of 

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

388 
(case snd (HOLogic.dest_number t1) of 

389 
0 => mk_num 0 

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

391 
1 => mk_num n1 

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

393 
[num_T, num_T] > num_T) 

394 
$ mk_num n1 $ mk_num n2) 

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

395 
 _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\ 
33192  396 
\for_atom (Abs_Frac)", ts) 
397 
end 

398 
else if not for_auto andalso is_abs_fun thy constr_x then 

399 
Const (abs_name, constr_T) $ the_single ts 

400 
else 

401 
list_comb (Const constr_x, ts) 

402 
in 

403 
if co then 

404 
let val var = var () in 

405 
if exists_subterm (equal (Var var)) t then 

406 
Const (@{const_name The}, (T > bool_T) > T) 

407 
$ Abs ("\<omega>", T, 

408 
Const (@{const_name "op ="}, [T, T] > bool_T) 

409 
$ Bound 0 $ abstract_over (Var var, t)) 

410 
else 

411 
t 

412 
end 

413 
else 

414 
t 

415 
end 

416 
end 

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

418 
> term *) 

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

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

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

422 
(batch_list (arity_of_rep R) js)) 

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

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

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

426 
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

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

430 
val arity1 = arity_of_rep R1 

431 
val (js1, js2) = chop arity1 js 

432 
in 

433 
list_comb (HOLogic.pair_const T1 T2, 

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

435 
[[js1], [js2]]) 

436 
end 

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

438 
term_for_vect seen k R' T1 T2 T' js 

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

440 
jss = 

441 
let 

442 
val jss1 = all_combinations_for_rep R1 

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

444 
val ts2 = 

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

446 
[[int_for_bool (js mem jss)]]) jss1 

447 
in make_fun false T1 T2 T' ts1 ts2 end 

448 
 term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = 

449 
let 

450 
val arity1 = arity_of_rep R1 

451 
val jss1 = all_combinations_for_rep R1 

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

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

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

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

456 
in make_fun true T1 T2 T' ts1 ts2 end 

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

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

459 
 term_for_rep seen T _ R jss = 

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

460 
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep", 
33192  461 
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^ 
462 
string_of_int (length jss)) 

463 
in 

464 
(not for_auto ? setify_mapify_funs []) o unbox_term oooo term_for_rep [] 

465 
end 

466 

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

468 
> term *) 

469 
fun term_for_name scope sel_names rel_table bounds name = 

470 
let val T = type_of name in 

471 
tuple_list_for_name rel_table bounds name 

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

473 
(rep_of name) 

474 
end 

475 

476 
(* Proof.context 

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

478 
fun add_wacky_syntax ctxt = 

479 
let 

480 
(* term > string *) 

481 
val name_of = fst o dest_Const 

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

483 
val (maybe_t, thy) = 

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

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

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

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

33192  495 
in 
496 
((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t), 

497 
ProofContext.transfer_syntax thy ctxt) 

498 
end 

499 

500 
(* term > term *) 

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

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

503 
$ Bound 0 $ t')) = 

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

505 
 unfold_outer_the_binders t = t 

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

507 
fun bisimilar_values _ 0 _ = true 

508 
 bisimilar_values coTs max_depth (t1, t2) = 

509 
let val T = fastype_of t1 in 

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

511 
let 

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

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

514 
val max_depth = max_depth  (if T mem coTs then 1 else 0) 

515 
in 

516 
head1 = head2 

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

518 
end 

519 
else 

520 
t1 = t2 

521 
end 

522 

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

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

525 
> Pretty.T * bool *) 

526 
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} 

527 
({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, user_axioms, debug, 

528 
wfs, destroy_constrs, specialize, skolemize, 

529 
star_linear_preds, uncurry, fast_descrs, tac_timeout, 

530 
evals, case_names, def_table, nondef_table, user_nondefs, 

531 
simp_table, psimp_table, intro_table, ground_thm_table, 

532 
ersatz_table, skolems, special_funs, unrolled_preds, 

533 
wf_cache}, 

534 
card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees 

535 
free_names sel_names nonsel_names rel_table bounds = 

536 
let 

537 
val (wacky_names as (_, base_name, step_name, _), ctxt) = 

538 
add_wacky_syntax ctxt 

539 
val ext_ctxt = 

540 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 

541 
wfs = wfs, user_axioms = user_axioms, debug = debug, 

542 
destroy_constrs = destroy_constrs, specialize = specialize, 

543 
skolemize = skolemize, star_linear_preds = star_linear_preds, 

544 
uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout, 

545 
evals = evals, case_names = case_names, def_table = def_table, 

546 
nondef_table = nondef_table, user_nondefs = user_nondefs, 

547 
simp_table = simp_table, psimp_table = psimp_table, 

548 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

549 
ersatz_table = ersatz_table, skolems = skolems, 

550 
special_funs = special_funs, unrolled_preds = unrolled_preds, 

551 
wf_cache = wf_cache} 

552 
val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns, 

553 
bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs} 

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

555 
val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table 

556 
bounds 

557 
(* typ > typ > typ *) 

558 
fun nth_value_of_type T card n = term_for_rep T T (Atom (card, 0)) [[n]] 

559 
(* dtype_spec list > dtype_spec > bool *) 

560 
fun is_codatatype_wellformed (cos : dtype_spec list) 

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

562 
let 

563 
val ts = map (nth_value_of_type typ card) (index_seq 0 card) 

564 
val max_depth = Integer.sum (map #card cos) 

565 
in 

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

567 
(all_distinct_unordered_pairs_of ts) 

568 
end 

569 
(* string > Pretty.T *) 

570 
fun pretty_for_assign name = 

571 
let 

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

573 
case name of 

574 
FreeName (s, T, _) => 

575 
let val t = Free (s, unbox_type T) in 

576 
("=", (t, format_term_type thy def_table formats t), T) 

577 
end 

578 
 ConstName (s, T, _) => 

579 
(assign_operator_for_const (s, T), 

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

581 
T) 

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

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

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

586 
else 

587 
tuple_list_for_name rel_table bounds name 

588 
> term_for_rep T T' (rep_of name) 

589 
in 

590 
Pretty.block (Pretty.breaks 

33571  591 
[setmp_show_all_types (Syntax.pretty_term ctxt) t1, 
33192  592 
Pretty.str oper, Syntax.pretty_term ctxt t2]) 
593 
end 

594 
(* dtype_spec > Pretty.T *) 

595 
fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) = 

596 
Pretty.block (Pretty.breaks 

597 
[Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=", 

598 
Pretty.enum "," "{" "}" 

599 
(map (Syntax.pretty_term ctxt o nth_value_of_type typ card) 

600 
(index_seq 0 card) @ 

601 
(if precise then [] else [Pretty.str unrep]))]) 

602 
(* typ > dtype_spec list *) 

603 
fun integer_datatype T = 

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

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

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

606 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] 
33192  607 
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

608 
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

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

610 
> append (integer_datatype nat_T @ integer_datatype int_T) 
33192  611 
val block_of_datatypes = 
612 
if show_datatypes andalso not (null datatypes) then 

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

614 
(map pretty_for_datatype datatypes)] 

615 
else 

616 
[] 

617 
val block_of_codatatypes = 

618 
if show_datatypes andalso not (null codatatypes) then 

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

620 
(map pretty_for_datatype codatatypes)] 

621 
else 

622 
[] 

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

624 
fun block_of_names show title names = 

625 
if show andalso not (null names) then 

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

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

628 
(sort_wrt (original_name o nickname_of) names) 

629 
else 

630 
[] 

631 
val (skolem_names, nonskolem_nonsel_names) = 

632 
List.partition is_skolem_name nonsel_names 

633 
val (eval_names, noneval_nonskolem_nonsel_names) = 

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

635 
nonskolem_nonsel_names 

636 
> filter_out (equal @{const_name bisim_iterator_max} o nickname_of) 

637 
val free_names = 

638 
map (fn x as (s, T) => 

639 
case filter (equal x o nickname_of pairf (unbox_type o type_of)) 

640 
free_names of 

641 
[name] => name 

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

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

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

646 
block_of_names show_skolems "Skolem constant" skolem_names @ 

647 
block_of_names true "Evaluated term" eval_names @ 

648 
block_of_datatypes @ block_of_codatatypes @ 

649 
block_of_names show_consts "Constant" 

650 
noneval_nonskolem_nonsel_names 

651 
in 

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

653 
else chunks), 

654 
bisim_depth >= 0 

655 
orelse forall (is_codatatype_wellformed codatatypes) codatatypes) 

656 
end 

657 

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

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

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

661 
auto_timeout free_names sel_names rel_table bounds prop = 

662 
let 

663 
(* typ * int > term *) 

664 
fun free_type_assm (T, k) = 

665 
let 

666 
(* int > term *) 

667 
val atom = atom true T 

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

669 
val eqs = map equation_for_atom (index_seq 0 k) 

670 
val compreh_assm = 

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

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

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

674 
in HOLogic.mk_conj (compreh_assm, distinct_assm) end 

675 
(* nut > term *) 

676 
fun free_name_assm name = 

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

678 
term_for_name scope sel_names rel_table bounds name) 

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

680 
val model_assms = map free_name_assm free_names 

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

682 
(freeT_assms @ model_assms) 

683 
(* bool > bool *) 

684 
fun try_out negate = 

685 
let 

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

687 
(ObjectLogic.atomize_term thy prop) 

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

689 
> map_types (map_type_tfree 

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

691 
 x => TFree x)) 

692 
> cterm_of thy > Goal.init 

693 
in 

694 
(goal > SINGLE (DETERM_TIMEOUT auto_timeout 

695 
(auto_tac (clasimpset_of ctxt))) 

696 
> the > Goal.finish ctxt; true) 

697 
handle THM _ => false 

698 
 TimeLimit.TimeOut => false 

699 
end 

700 
in 

701 
if silence try_out false then SOME true 

702 
else if silence try_out true then SOME false 

703 
else NONE 

704 
end 

705 

706 
end; 