author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41047  9f1d3fcef1ca 
parent 41046  f2e94005d283 
child 41049  0edd245892ed 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_nut.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Nitpick underlying terms (nuts). 

6 
*) 

7 

8 
signature NITPICK_NUT = 

9 
sig 

38170  10 
type styp = Nitpick_Util.styp 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34982
diff
changeset

11 
type hol_context = Nitpick_HOL.hol_context 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

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

13 
type name_pool = Nitpick_Peephole.name_pool 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

14 
type rep = Nitpick_Rep.rep 
33192  15 

16 
datatype cst = 

17 
False  

18 
True  

19 
Iden  

20 
Num of int  

21 
Unknown  

22 
Unrep  

23 
Suc  

24 
Add  

25 
Subtract  

26 
Multiply  

27 
Divide  

28 
Gcd  

29 
Lcm  

30 
Fracs  

31 
NormFrac  

32 
NatToInt  

33 
IntToNat 

34 

35 
datatype op1 = 

36 
Not  

37 
Finite  

38 
Converse  

39 
Closure  

40 
SingletonSet  

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

41 
IsUnknown  
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

42 
SafeThe  
33192  43 
First  
44 
Second  

45 
Cast 

46 

47 
datatype op2 = 

48 
All  

49 
Exist  

50 
Or  

51 
And  

52 
Less  

53 
Subset  

54 
DefEq  

55 
Eq  

56 
Triad  

57 
Composition  

58 
Image  

59 
Apply  

60 
Lambda 

61 

62 
datatype op3 = 

63 
Let  

64 
If 

65 

66 
datatype nut = 

67 
Cst of cst * typ * rep  

68 
Op1 of op1 * typ * rep * nut  

69 
Op2 of op2 * typ * rep * nut * nut  

70 
Op3 of op3 * typ * rep * nut * nut * nut  

71 
Tuple of typ * rep * nut list  

72 
Construct of nut list * typ * rep * nut list  

73 
BoundName of int * typ * rep * string  

74 
FreeName of string * typ * rep  

75 
ConstName of string * typ * rep  

76 
BoundRel of Kodkod.n_ary_index * typ * rep * string  

77 
FreeRel of Kodkod.n_ary_index * typ * rep * string  

78 
RelReg of int * typ * rep  

79 
FormulaReg of int * typ * rep 

80 

81 
structure NameTable : TABLE 

82 

83 
exception NUT of string * nut list 

84 

85 
val string_for_nut : Proof.context > nut > string 

86 
val inline_nut : nut > bool 

87 
val type_of : nut > typ 

88 
val rep_of : nut > rep 

89 
val nickname_of : nut > string 

90 
val is_skolem_name : nut > bool 

91 
val is_eval_name : nut > bool 

92 
val is_Cst : cst > nut > bool 

93 
val fold_nut : (nut > 'a > 'a) > nut > 'a > 'a 

94 
val map_nut : (nut > nut) > nut > nut 

95 
val untuple : (nut > 'a) > nut > 'a list 

96 
val add_free_and_const_names : 

97 
nut > nut list * nut list > nut list * nut list 

98 
val name_ord : (nut * nut) > order 

99 
val the_name : 'a NameTable.table > nut > 'a 

100 
val the_rel : nut NameTable.table > nut > Kodkod.n_ary_index 

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

101 
val nut_from_term : hol_context > op2 > term > nut 
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:
37256
diff
changeset

102 
val is_fully_representable_set : nut > bool 
33192  103 
val choose_reps_for_free_vars : 
38170  104 
scope > styp list > nut list > rep NameTable.table 
105 
> nut list * rep NameTable.table 

33192  106 
val choose_reps_for_consts : 
107 
scope > bool > nut list > rep NameTable.table 

108 
> nut list * rep NameTable.table 

109 
val choose_reps_for_all_sels : 

110 
scope > rep NameTable.table > nut list * rep NameTable.table 

111 
val choose_reps_in_nut : 

112 
scope > bool > rep NameTable.table > bool > nut > nut 

113 
val rename_free_vars : 

114 
nut list > name_pool > nut NameTable.table 

115 
> nut list * name_pool * nut NameTable.table 

116 
val rename_vars_in_nut : name_pool > nut NameTable.table > nut > nut 

117 
end; 

118 

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

119 
structure Nitpick_Nut : NITPICK_NUT = 
33192  120 
struct 
121 

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

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

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

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

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

126 
open Nitpick_Rep 
33192  127 

34126  128 
structure KK = Kodkod 
129 

33192  130 
datatype cst = 
131 
False  

132 
True  

133 
Iden  

134 
Num of int  

135 
Unknown  

136 
Unrep  

137 
Suc  

138 
Add  

139 
Subtract  

140 
Multiply  

141 
Divide  

142 
Gcd  

143 
Lcm  

144 
Fracs  

145 
NormFrac  

146 
NatToInt  

147 
IntToNat 

148 

149 
datatype op1 = 

150 
Not  

151 
Finite  

152 
Converse  

153 
Closure  

154 
SingletonSet  

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

155 
IsUnknown  
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

156 
SafeThe  
33192  157 
First  
158 
Second  

159 
Cast 

160 

161 
datatype op2 = 

162 
All  

163 
Exist  

164 
Or  

165 
And  

166 
Less  

167 
Subset  

168 
DefEq  

169 
Eq  

170 
Triad  

171 
Composition  

172 
Image  

173 
Apply  

174 
Lambda 

175 

176 
datatype op3 = 

177 
Let  

178 
If 

179 

180 
datatype nut = 

181 
Cst of cst * typ * rep  

182 
Op1 of op1 * typ * rep * nut  

183 
Op2 of op2 * typ * rep * nut * nut  

184 
Op3 of op3 * typ * rep * nut * nut * nut  

185 
Tuple of typ * rep * nut list  

186 
Construct of nut list * typ * rep * nut list  

187 
BoundName of int * typ * rep * string  

188 
FreeName of string * typ * rep  

189 
ConstName of string * typ * rep  

34126  190 
BoundRel of KK.n_ary_index * typ * rep * string  
191 
FreeRel of KK.n_ary_index * typ * rep * string  

33192  192 
RelReg of int * typ * rep  
193 
FormulaReg of int * typ * rep 

194 

195 
exception NUT of string * nut list 

196 

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

197 
fun string_for_cst False = "False" 
33192  198 
 string_for_cst True = "True" 
199 
 string_for_cst Iden = "Iden" 

200 
 string_for_cst (Num j) = "Num " ^ signed_string_of_int j 

201 
 string_for_cst Unknown = "Unknown" 

202 
 string_for_cst Unrep = "Unrep" 

203 
 string_for_cst Suc = "Suc" 

204 
 string_for_cst Add = "Add" 

205 
 string_for_cst Subtract = "Subtract" 

206 
 string_for_cst Multiply = "Multiply" 

207 
 string_for_cst Divide = "Divide" 

208 
 string_for_cst Gcd = "Gcd" 

209 
 string_for_cst Lcm = "Lcm" 

210 
 string_for_cst Fracs = "Fracs" 

211 
 string_for_cst NormFrac = "NormFrac" 

212 
 string_for_cst NatToInt = "NatToInt" 

213 
 string_for_cst IntToNat = "IntToNat" 

214 

215 
fun string_for_op1 Not = "Not" 

216 
 string_for_op1 Finite = "Finite" 

217 
 string_for_op1 Converse = "Converse" 

218 
 string_for_op1 Closure = "Closure" 

219 
 string_for_op1 SingletonSet = "SingletonSet" 

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

220 
 string_for_op1 IsUnknown = "IsUnknown" 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

221 
 string_for_op1 SafeThe = "SafeThe" 
33192  222 
 string_for_op1 First = "First" 
223 
 string_for_op1 Second = "Second" 

224 
 string_for_op1 Cast = "Cast" 

225 

226 
fun string_for_op2 All = "All" 

227 
 string_for_op2 Exist = "Exist" 

228 
 string_for_op2 Or = "Or" 

229 
 string_for_op2 And = "And" 

230 
 string_for_op2 Less = "Less" 

231 
 string_for_op2 Subset = "Subset" 

232 
 string_for_op2 DefEq = "DefEq" 

233 
 string_for_op2 Eq = "Eq" 

234 
 string_for_op2 Triad = "Triad" 

235 
 string_for_op2 Composition = "Composition" 

236 
 string_for_op2 Image = "Image" 

237 
 string_for_op2 Apply = "Apply" 

238 
 string_for_op2 Lambda = "Lambda" 

239 

240 
fun string_for_op3 Let = "Let" 

241 
 string_for_op3 If = "If" 

242 

243 
fun basic_string_for_nut indent ctxt u = 

244 
let 

245 
val sub = basic_string_for_nut (indent + 1) ctxt 

246 
in 

247 
(if indent = 0 then "" else "\n" ^ implode (replicate (2 * indent) " ")) ^ 

248 
"(" ^ 

249 
(case u of 

250 
Cst (c, T, R) => 

251 
"Cst " ^ string_for_cst c ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

252 
string_for_rep R 

253 
 Op1 (oper, T, R, u1) => 

254 
"Op1 " ^ string_for_op1 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

255 
string_for_rep R ^ " " ^ sub u1 

256 
 Op2 (oper, T, R, u1, u2) => 

257 
"Op2 " ^ string_for_op2 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

258 
string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 

259 
 Op3 (oper, T, R, u1, u2, u3) => 

260 
"Op3 " ^ string_for_op3 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

261 
string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 ^ " " ^ sub u3 

262 
 Tuple (T, R, us) => 

263 
"Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ 

264 
implode (map sub us) 

265 
 Construct (us', T, R, us) => 

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

266 
"Construct " ^ implode (map sub us') ^ " " ^ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

267 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

268 
implode (map sub us) 
33192  269 
 BoundName (j, T, R, nick) => 
270 
"BoundName " ^ signed_string_of_int j ^ " " ^ 

271 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick 

272 
 FreeName (s, T, R) => 

273 
"FreeName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

274 
string_for_rep R 

275 
 ConstName (s, T, R) => 

276 
"ConstName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^ 

277 
string_for_rep R 

278 
 BoundRel ((n, j), T, R, nick) => 

279 
"BoundRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^ 

280 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick 

281 
 FreeRel ((n, j), T, R, nick) => 

282 
"FreeRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^ 

283 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick 

284 
 RelReg (j, T, R) => 

285 
"RelReg " ^ signed_string_of_int j ^ " " ^ Syntax.string_of_typ ctxt T ^ 

286 
" " ^ string_for_rep R 

287 
 FormulaReg (j, T, R) => 

288 
"FormulaReg " ^ signed_string_of_int j ^ " " ^ 

289 
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R) ^ 

290 
")" 

291 
end 

292 
val string_for_nut = basic_string_for_nut 0 

293 

294 
fun inline_nut (Op1 _) = false 

295 
 inline_nut (Op2 _) = false 

296 
 inline_nut (Op3 _) = false 

297 
 inline_nut (Tuple (_, _, us)) = forall inline_nut us 

298 
 inline_nut _ = true 

299 

300 
fun type_of (Cst (_, T, _)) = T 

301 
 type_of (Op1 (_, T, _, _)) = T 

302 
 type_of (Op2 (_, T, _, _, _)) = T 

303 
 type_of (Op3 (_, T, _, _, _, _)) = T 

304 
 type_of (Tuple (T, _, _)) = T 

305 
 type_of (Construct (_, T, _, _)) = T 

306 
 type_of (BoundName (_, T, _, _)) = T 

307 
 type_of (FreeName (_, T, _)) = T 

308 
 type_of (ConstName (_, T, _)) = T 

309 
 type_of (BoundRel (_, T, _, _)) = T 

310 
 type_of (FreeRel (_, T, _, _)) = T 

311 
 type_of (RelReg (_, T, _)) = T 

312 
 type_of (FormulaReg (_, T, _)) = T 

313 

314 
fun rep_of (Cst (_, _, R)) = R 

315 
 rep_of (Op1 (_, _, R, _)) = R 

316 
 rep_of (Op2 (_, _, R, _, _)) = R 

317 
 rep_of (Op3 (_, _, R, _, _, _)) = R 

318 
 rep_of (Tuple (_, R, _)) = R 

319 
 rep_of (Construct (_, _, R, _)) = R 

320 
 rep_of (BoundName (_, _, R, _)) = R 

321 
 rep_of (FreeName (_, _, R)) = R 

322 
 rep_of (ConstName (_, _, R)) = R 

323 
 rep_of (BoundRel (_, _, R, _)) = R 

324 
 rep_of (FreeRel (_, _, R, _)) = R 

325 
 rep_of (RelReg (_, _, R)) = R 

326 
 rep_of (FormulaReg (_, _, R)) = R 

327 

328 
fun nickname_of (BoundName (_, _, _, nick)) = nick 

329 
 nickname_of (FreeName (s, _, _)) = s 

330 
 nickname_of (ConstName (s, _, _)) = s 

331 
 nickname_of (BoundRel (_, _, _, nick)) = nick 

332 
 nickname_of (FreeRel (_, _, _, nick)) = nick 

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

333 
 nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u]) 
33192  334 

335 
fun is_skolem_name u = 

336 
space_explode name_sep (nickname_of u) 

337 
> exists (String.isPrefix skolem_prefix) 

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

338 
handle NUT ("Nitpick_Nut.nickname_of", _) => false 
33192  339 
fun is_eval_name u = 
340 
String.isPrefix eval_prefix (nickname_of u) 

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

341 
handle NUT ("Nitpick_Nut.nickname_of", _) => false 
33192  342 
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst') 
343 
 is_Cst _ _ = false 

344 

345 
fun fold_nut f u = 

346 
case u of 

347 
Op1 (_, _, _, u1) => fold_nut f u1 

348 
 Op2 (_, _, _, u1, u2) => fold_nut f u1 #> fold_nut f u2 

349 
 Op3 (_, _, _, u1, u2, u3) => fold_nut f u1 #> fold_nut f u2 #> fold_nut f u3 

350 
 Tuple (_, _, us) => fold (fold_nut f) us 

351 
 Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us' 

352 
 _ => f u 

353 
fun map_nut f u = 

354 
case u of 

355 
Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1) 

356 
 Op2 (oper, T, R, u1, u2) => Op2 (oper, T, R, map_nut f u1, map_nut f u2) 

357 
 Op3 (oper, T, R, u1, u2, u3) => 

358 
Op3 (oper, T, R, map_nut f u1, map_nut f u2, map_nut f u3) 

359 
 Tuple (T, R, us) => Tuple (T, R, map (map_nut f) us) 

360 
 Construct (us', T, R, us) => 

361 
Construct (map (map_nut f) us', T, R, map (map_nut f) us) 

362 
 _ => f u 

363 

364 
fun name_ord (BoundName (j1, _, _, _), BoundName (j2, _, _, _)) = 

365 
int_ord (j1, j2) 

366 
 name_ord (BoundName _, _) = LESS 

367 
 name_ord (_, BoundName _) = GREATER 

368 
 name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) = 

369 
(case fast_string_ord (s1, s2) of 

35408  370 
EQUAL => Term_Ord.typ_ord (T1, T2) 
33192  371 
 ord => ord) 
372 
 name_ord (FreeName _, _) = LESS 

373 
 name_ord (_, FreeName _) = GREATER 

374 
 name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) = 

375 
(case fast_string_ord (s1, s2) of 

35408  376 
EQUAL => Term_Ord.typ_ord (T1, T2) 
33192  377 
 ord => ord) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

378 
 name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2]) 
33192  379 

36913  380 
fun num_occurrences_in_nut needle_u stack_u = 
33192  381 
fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0 
36913  382 
val is_subnut_of = not_equal 0 oo num_occurrences_in_nut 
33192  383 

384 
fun substitute_in_nut needle_u needle_u' = 

385 
map_nut (fn u => if u = needle_u then needle_u' else u) 

386 

387 
val add_free_and_const_names = 

388 
fold_nut (fn u => case u of 

389 
FreeName _ => apfst (insert (op =) u) 

390 
 ConstName _ => apsnd (insert (op =) u) 

391 
 _ => I) 

392 

393 
fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick) 

394 
 modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R) 

395 
 modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R) 

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

396 
 modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u]) 
33192  397 

398 
structure NameTable = Table(type key = nut val ord = name_ord) 

399 

400 
fun the_name table name = 

401 
case NameTable.lookup table name of 

402 
SOME u => u 

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

403 
 NONE => raise NUT ("Nitpick_Nut.the_name", [name]) 
33192  404 
fun the_rel table name = 
405 
case the_name table name of 

406 
FreeRel (x, _, _, _) => x 

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

407 
 u => raise NUT ("Nitpick_Nut.the_rel", [u]) 
33192  408 

409 
fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1) 

410 
 mk_fst (T, t) = 

411 
let val res_T = fst (HOLogic.dest_prodT T) in 

412 
(res_T, Const (@{const_name fst}, T > res_T) $ t) 

413 
end 

414 
fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) = 

415 
(domain_type (range_type T), t2) 

416 
 mk_snd (T, t) = 

417 
let val res_T = snd (HOLogic.dest_prodT T) in 

418 
(res_T, Const (@{const_name snd}, T > res_T) $ t) 

419 
end 

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

420 
fun factorize (z as (Type (@{type_name prod}, _), _)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

421 
maps factorize [mk_fst z, mk_snd z] 
33192  422 
 factorize z = [z] 
423 

39359  424 
fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq = 
33192  425 
let 
426 
fun aux eq ss Ts t = 

427 
let 

428 
val sub = aux Eq ss Ts 

429 
val sub' = aux eq ss Ts 

430 
fun sub_abs s T = aux eq (s :: ss) (T :: Ts) 

431 
fun sub_equals T t1 t2 = 

432 
let 

433 
val (binder_Ts, body_T) = strip_type (domain_type T) 

434 
val n = length binder_Ts 

435 
in 

436 
if eq = Eq andalso n > 0 then 

437 
let 

438 
val t1 = incr_boundvars n t1 

439 
val t2 = incr_boundvars n t2 

440 
val xs = map Bound (n  1 downto 0) 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

441 
val equation = Const (@{const_name HOL.eq}, 
33192  442 
body_T > body_T > bool_T) 
443 
$ betapplys (t1, xs) $ betapplys (t2, xs) 

444 
val t = 

445 
fold_rev (fn T => fn (t, j) => 

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

447 
$ Abs ("x" ^ nat_subscript j, T, t), j  1)) 

448 
binder_Ts (equation, n) > fst 

449 
in sub' t end 

450 
else 

451 
Op2 (eq, bool_T, Any, aux Eq ss Ts t1, aux Eq ss Ts t2) 

452 
end 

453 
fun do_quantifier quant s T t1 = 

454 
let 

455 
val bound_u = BoundName (length Ts, T, Any, s) 

456 
val body_u = sub_abs s T t1 

36913  457 
in Op2 (quant, bool_T, Any, bound_u, body_u) end 
33192  458 
fun do_apply t0 ts = 
459 
let 

460 
val (ts', t2) = split_last ts 

461 
val t1 = list_comb (t0, ts') 

462 
val T1 = fastype_of1 (Ts, t1) 

463 
in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

464 
fun do_construct (x as (_, T)) ts = 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

465 
case num_binder_types T  length ts of 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

466 
0 => Construct (map ((fn (s', T') => ConstName (s', T', Any)) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

467 
o nth_sel_for_constr x) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

468 
(~1 upto num_sels_for_constr_type T  1), 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

469 
body_type T, Any, 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

470 
ts > map (`(curry fastype_of1 Ts)) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

471 
> maps factorize > map (sub o snd)) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

472 
 k => sub (eta_expand Ts t k) 
33192  473 
in 
474 
case strip_comb t of 

475 
(Const (@{const_name all}, _), [Abs (s, T, t1)]) => 

476 
do_quantifier All s T t1 

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

477 
 (t0 as Const (@{const_name all}, _), [t1]) => 
33192  478 
sub' (t0 $ eta_expand Ts t1 1) 
479 
 (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2 

480 
 (Const (@{const_name "==>"}, _), [t1, t2]) => 

481 
Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2) 

482 
 (Const (@{const_name Pure.conjunction}, _), [t1, t2]) => 

483 
Op2 (And, prop_T, Any, sub' t1, sub' t2) 

484 
 (Const (@{const_name Trueprop}, _), [t1]) => sub' t1 

485 
 (Const (@{const_name Not}, _), [t1]) => 

486 
(case sub t1 of 

487 
Op1 (Not, _, _, u11) => u11 

488 
 u1 => Op1 (Not, bool_T, Any, u1)) 

489 
 (Const (@{const_name False}, T), []) => Cst (False, T, Any) 

490 
 (Const (@{const_name True}, T), []) => Cst (True, T, Any) 

491 
 (Const (@{const_name All}, _), [Abs (s, T, t1)]) => 

492 
do_quantifier All s T t1 

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

493 
 (t0 as Const (@{const_name All}, _), [t1]) => 
33192  494 
sub' (t0 $ eta_expand Ts t1 1) 
495 
 (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) => 

496 
do_quantifier Exist s T t1 

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

497 
 (t0 as Const (@{const_name Ex}, _), [t1]) => 
33192  498 
sub' (t0 $ eta_expand Ts t1 1) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

499 
 (Const (@{const_name HOL.eq}, T), [t1]) => 
37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37266
diff
changeset

500 
Op1 (SingletonSet, range_type T, Any, sub t1) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

501 
 (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

502 
 (Const (@{const_name HOL.conj}, _), [t1, t2]) => 
33192  503 
Op2 (And, bool_T, Any, sub' t1, sub' t2) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

504 
 (Const (@{const_name HOL.disj}, _), [t1, t2]) => 
33192  505 
Op2 (Or, bool_T, Any, sub t1, sub t2) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38190
diff
changeset

506 
 (Const (@{const_name HOL.implies}, _), [t1, t2]) => 
33192  507 
Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2) 
508 
 (Const (@{const_name If}, T), [t1, t2, t3]) => 

509 
Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3) 

510 
 (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) => 

511 
Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s), 

512 
sub t1, sub_abs s T' t2) 

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

513 
 (t0 as Const (@{const_name Let}, _), [t1, t2]) => 
33192  514 
sub (t0 $ t1 $ eta_expand Ts t2 1) 
515 
 (Const (@{const_name Pair}, T), [t1, t2]) => 

516 
Tuple (nth_range_type 2 T, Any, map sub [t1, t2]) 

517 
 (Const (@{const_name fst}, T), [t1]) => 

518 
Op1 (First, range_type T, Any, sub t1) 

519 
 (Const (@{const_name snd}, T), [t1]) => 

520 
Op1 (Second, range_type T, Any, sub t1) 

521 
 (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any) 

522 
 (Const (@{const_name converse}, T), [t1]) => 

523 
Op1 (Converse, range_type T, Any, sub t1) 

524 
 (Const (@{const_name trancl}, T), [t1]) => 

525 
Op1 (Closure, range_type T, Any, sub t1) 

526 
 (Const (@{const_name rel_comp}, T), [t1, t2]) => 

527 
Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2) 

528 
 (Const (@{const_name image}, T), [t1, t2]) => 

529 
Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2) 

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

530 
 (Const (x as (s as @{const_name Suc}, T)), []) => 
39359  531 
if is_built_in_const thy stds x then Cst (Suc, T, Any) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

532 
else if is_constr ctxt stds x then do_construct x [] 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

533 
else ConstName (s, T, Any) 
33192  534 
 (Const (@{const_name finite}, T), [t1]) => 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34982
diff
changeset

535 
(if is_finite_type hol_ctxt (domain_type T) then 
33877
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33853
diff
changeset

536 
Cst (True, bool_T, Any) 
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33853
diff
changeset

537 
else case t1 of 
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33853
diff
changeset

538 
Const (@{const_name top}, _) => Cst (False, bool_T, Any) 
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33853
diff
changeset

539 
 _ => Op1 (Finite, bool_T, Any, sub t1)) 
33192  540 
 (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any) 
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

541 
 (Const (x as (s as @{const_name zero_class.zero}, T)), []) => 
39359  542 
if is_built_in_const thy stds x then Cst (Num 0, T, Any) 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

543 
else if is_constr ctxt stds x then do_construct x [] 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

544 
else ConstName (s, T, Any) 
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

545 
 (Const (x as (s as @{const_name one_class.one}, T)), []) => 
39359  546 
if is_built_in_const thy stds x then Cst (Num 1, T, Any) 
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

547 
else ConstName (s, T, Any) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

548 
 (Const (x as (s as @{const_name plus_class.plus}, T)), []) => 
39359  549 
if is_built_in_const thy stds x then Cst (Add, T, Any) 
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

550 
else ConstName (s, T, Any) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

551 
 (Const (x as (s as @{const_name minus_class.minus}, T)), []) => 
39359  552 
if is_built_in_const thy stds x then Cst (Subtract, T, Any) 
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

553 
else ConstName (s, T, Any) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

554 
 (Const (x as (s as @{const_name times_class.times}, T)), []) => 
39359  555 
if is_built_in_const thy stds x then Cst (Multiply, T, Any) 
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

556 
else ConstName (s, T, Any) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

557 
 (Const (x as (s as @{const_name div_class.div}, T)), []) => 
39359  558 
if is_built_in_const thy stds x then Cst (Divide, T, Any) 
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

559 
else ConstName (s, T, Any) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

560 
 (t0 as Const (x as (@{const_name ord_class.less}, _)), 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

561 
ts as [t1, t2]) => 
39359  562 
if is_built_in_const thy stds x then 
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

563 
Op2 (Less, bool_T, Any, sub t1, sub t2) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

566 
 (Const (@{const_name ord_class.less_eq}, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

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

568 
[Type (@{type_name fun}, [_, @{typ bool}]), _])), 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

569 
[t1, t2]) => 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

570 
Op2 (Subset, bool_T, Any, sub t1, sub t2) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

571 
(* FIXME: find out if this case is necessary *) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

572 
 (t0 as Const (x as (@{const_name ord_class.less_eq}, _)), 
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

573 
ts as [t1, t2]) => 
39359  574 
if is_built_in_const thy stds x then 
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

575 
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

577 
do_apply t0 ts 
33192  578 
 (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any) 
579 
 (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any) 

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

580 
 (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) => 
39359  581 
if is_built_in_const thy stds x then 
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

582 
let val num_T = domain_type T in 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

583 
Op2 (Apply, num_T > num_T, Any, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

584 
Cst (Subtract, num_T > num_T > num_T, Any), 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

585 
Cst (Num 0, num_T, Any)) 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

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

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

588 
ConstName (s, T, Any) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

589 
 (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

590 
 (Const (@{const_name is_unknown}, _), [t1]) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

591 
Op1 (IsUnknown, bool_T, Any, sub t1) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

592 
 (Const (@{const_name safe_The}, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

593 
Type (@{type_name fun}, [_, T2])), [t1]) => 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

594 
Op1 (SafeThe, T2, Any, sub t1) 
33192  595 
 (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) 
596 
 (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) 

597 
 (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => 

598 
Cst (NatToInt, T, Any) 

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

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

600 
T as @{typ "unsigned_bit word => signed_bit word"}), []) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

601 
Cst (NatToInt, T, Any) 
33192  602 
 (t0 as Const (x as (s, T)), ts) => 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

603 
if is_constr ctxt stds x then 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

604 
do_construct x ts 
33192  605 
else if String.isPrefix numeral_prefix s then 
606 
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any) 

607 
else 

39359  608 
(case arity_of_built_in_const thy stds x of 
33192  609 
SOME n => 
610 
(case n  length ts of 

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

611 
0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t]) 
33192  612 
 k => if k > 0 then sub (eta_expand Ts t k) 
613 
else do_apply t0 ts) 

614 
 NONE => if null ts then ConstName (s, T, Any) 

615 
else do_apply t0 ts) 

616 
 (Free (s, T), []) => FreeName (s, T, Any) 

33877
e779bea3d337
fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
blanchet
parents:
33853
diff
changeset

617 
 (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t]) 
33192  618 
 (Bound j, []) => 
619 
BoundName (length Ts  j  1, nth Ts j, Any, nth ss j) 

620 
 (Abs (s, T, t1), []) => 

621 
Op2 (Lambda, T > fastype_of1 (T :: Ts, t1), Any, 

622 
BoundName (length Ts, T, Any, s), sub_abs s T t1) 

623 
 (t0, ts) => do_apply t0 ts 

624 
end 

625 
in aux eq [] [] end 

626 

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:
37256
diff
changeset

627 
fun is_fully_representable_set u = 
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:
37256
diff
changeset

628 
not (is_opt_rep (rep_of u)) andalso 
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:
37256
diff
changeset

629 
case u of 
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:
37256
diff
changeset

630 
FreeName _ => true 
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:
37256
diff
changeset

631 
 Op1 (SingletonSet, _, _, _) => true 
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:
37256
diff
changeset

632 
 Op1 (Converse, _, _, u1) => is_fully_representable_set u1 
39343  633 
 Op2 (Lambda, _, _, _, Cst (False, _, _)) => true 
634 
 Op2 (oper, _, _, u1, _) => 

37476
0681e46b4022
optimized code generated for datatype cases + more;
blanchet
parents:
37266
diff
changeset

635 
if oper = Apply then 
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:
37256
diff
changeset

636 
case u1 of 
37266
773dc74118f6
improved precision of "set" based on an example from Lukas
blanchet
parents:
37262
diff
changeset

637 
ConstName (s, _, _) => 
773dc74118f6
improved precision of "set" based on an example from Lukas
blanchet
parents:
37262
diff
changeset

638 
is_sel_like_and_no_discr s orelse s = @{const_name set} 
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:
37256
diff
changeset

639 
 _ => 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:
37256
diff
changeset

640 
else 
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:
37256
diff
changeset

641 
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:
37256
diff
changeset

642 
 _ => 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:
37256
diff
changeset

643 

33192  644 
fun rep_for_abs_fun scope T = 
645 
let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in 

646 
Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2) 

647 
end 

648 

38170  649 
fun choose_rep_for_free_var scope pseudo_frees v (vs, table) = 
33192  650 
let 
38170  651 
val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then 
652 
best_opt_set_rep_for_type 

653 
else 

654 
best_non_opt_set_rep_for_type) scope (type_of v) 

33192  655 
val v = modify_name_rep v R 
656 
in (v :: vs, NameTable.update (v, R) table) end 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

657 
fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

658 
(vs, table) = 
33192  659 
let 
660 
val x as (s, T) = (nickname_of v, type_of v) 

37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

661 
val R = (if is_abs_fun ctxt x then 
33192  662 
rep_for_abs_fun 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
36913
diff
changeset

663 
else if is_rep_fun ctxt x then 
33192  664 
Func oo best_non_opt_symmetric_reps_for_fun_type 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

665 
else if all_exact orelse is_skolem_name v orelse 
39360
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset

666 
member (op =) [@{const_name bisim}, 
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset

667 
@{const_name bisim_iterator_max}] 
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset

668 
(original_name s) then 
33192  669 
best_non_opt_set_rep_for_type 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

670 
else if member (op =) [@{const_name set}, @{const_name distinct}, 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

671 
@{const_name ord_class.less}, 
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

672 
@{const_name ord_class.less_eq}] 
39360
cdf2c3341422
eliminate more clutter related to "fast_descrs" optimization
blanchet
parents:
39359
diff
changeset

673 
(original_name s) then 
33192  674 
best_set_rep_for_type 
675 
else 

676 
best_opt_set_rep_for_type) scope T 

677 
val v = modify_name_rep v R 

678 
in (v :: vs, NameTable.update (v, R) table) end 

679 

38170  680 
fun choose_reps_for_free_vars scope pseudo_frees vs table = 
681 
fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table) 

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

682 
fun choose_reps_for_consts scope all_exact vs table = 
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

683 
fold (choose_rep_for_const scope all_exact) vs ([], table) 
33192  684 

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

685 
fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...}) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

686 
(x as (_, T)) n (vs, table) = 
33192  687 
let 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

688 
val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

689 
val R' = if n = ~1 orelse is_word_type (body_type T) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

690 
(is_fun_type (range_type T') andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

691 
is_boolean_type (body_type T')) then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

692 
best_non_opt_set_rep_for_type scope T' 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

694 
best_opt_set_rep_for_type scope T' > unopt_rep 
33192  695 
val v = ConstName (s', T', R') 
696 
in (v :: vs, NameTable.update (v, R') table) end 

697 
fun choose_rep_for_sels_for_constr scope (x as (_, T)) = 

698 
fold_rev (choose_rep_for_nth_sel_for_constr scope x) 

699 
(~1 upto num_sels_for_constr_type T  1) 

38126  700 
fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

701 
 choose_rep_for_sels_of_datatype scope {constrs, ...} = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

702 
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs 
33192  703 
fun choose_reps_for_all_sels (scope as {datatypes, ...}) = 
704 
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair [] 

705 

706 
fun choose_rep_for_bound_var scope v table = 

707 
let val R = best_one_rep_for_type scope (type_of v) in 

708 
NameTable.update (v, R) table 

709 
end 

710 

711 
(* A nut is said to be constructive if whenever it evaluates to unknown in our 

36913  712 
threevalued logic, it would evaluate to an unrepresentable value ("Unrep") 
33631  713 
according to the HOL semantics. For example, "Suc n" is constructive if "n" 
35312  714 
is representable or "Unrep", because unknown implies "Unrep". *) 
33192  715 
fun is_constructive u = 
716 
is_Cst Unrep u orelse 

717 
(not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse 

718 
case u of 

719 
Cst (Num _, _, _) => true 

38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

720 
 Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add) 
33192  721 
 Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2] 
722 
 Op3 (If, _, _, u1, u2, u3) => 

723 
not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3] 

724 
 Tuple (_, _, us) => forall is_constructive us 

725 
 Construct (_, _, _, us) => forall is_constructive us 

726 
 _ => false 

727 

728 
fun unknown_boolean T R = 

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

729 
Cst (case R of Formula Pos => False  Formula Neg => True  _ => Unknown, 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

730 
T, R) 
33192  731 

732 
fun s_op1 oper T R u1 = 

733 
((if oper = Not then 

734 
if is_Cst True u1 then Cst (False, T, R) 

735 
else if is_Cst False u1 then Cst (True, T, R) 

736 
else raise SAME () 

737 
else 

738 
raise SAME ()) 

739 
handle SAME () => Op1 (oper, T, R, u1)) 

740 
fun s_op2 oper T R u1 u2 = 

741 
((case oper of 

36913  742 
All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2 
743 
 Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2 

744 
 Or => 

33192  745 
if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R) 
746 
else if is_Cst False u1 then u2 

747 
else if is_Cst False u2 then u1 

748 
else raise SAME () 

749 
 And => 

750 
if exists (is_Cst False) [u1, u2] then Cst (False, T, unopt_rep R) 

751 
else if is_Cst True u1 then u2 

752 
else if is_Cst True u2 then u1 

753 
else raise SAME () 

754 
 Eq => 

755 
(case pairself (is_Cst Unrep) (u1, u2) of 

756 
(true, true) => unknown_boolean T R 

757 
 (false, false) => raise SAME () 

758 
 _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME () 

759 
else Cst (False, T, Formula Neut)) 

760 
 Triad => 

761 
if is_Cst True u1 then u1 

762 
else if is_Cst False u2 then u2 

763 
else raise SAME () 

764 
 Apply => 

765 
if is_Cst Unrep u1 then 

766 
Cst (Unrep, T, R) 

767 
else if is_Cst Unrep u2 then 

36913  768 
if is_boolean_type T then 
35312  769 
if is_fully_representable_set u1 then Cst (False, T, Formula Neut) 
33631  770 
else unknown_boolean T R 
36913  771 
else if is_constructive u1 then 
772 
Cst (Unrep, T, R) 

33192  773 
else case u1 of 
774 
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) => 

775 
Cst (Unrep, T, R) 

776 
 _ => raise SAME () 

777 
else 

778 
raise SAME () 

779 
 _ => raise SAME ()) 

780 
handle SAME () => Op2 (oper, T, R, u1, u2)) 

781 
fun s_op3 oper T R u1 u2 u3 = 

782 
((case oper of 

783 
Let => 

36913  784 
if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then 
33192  785 
substitute_in_nut u1 u2 u3 
786 
else 

787 
raise SAME () 

788 
 _ => raise SAME ()) 

789 
handle SAME () => Op3 (oper, T, R, u1, u2, u3)) 

790 
fun s_tuple T R us = 

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

791 
if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us) 
33192  792 

793 
fun untuple f (Tuple (_, _, us)) = maps (untuple f) us 

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

794 
 untuple f u = [f u] 
33192  795 

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

796 
fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...}) 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset

797 
unsound table def = 
33192  798 
let 
799 
val bool_atom_R = Atom (2, offset_of_type ofs bool_T) 

800 
fun bool_rep polar opt = 

801 
if polar = Neut andalso opt then Opt bool_atom_R else Formula polar 

802 
fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2 

803 
fun triad_fn f = triad (f Pos) (f Neg) 

804 
fun unrepify_nut_in_nut table def polar needle_u = 

805 
let val needle_T = type_of needle_u in 

806 
substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown 

807 
else Unrep, needle_T, Any)) 

808 
#> aux table def polar 

809 
end 

810 
and aux table def polar u = 

811 
let 

812 
val gsub = aux table 

813 
val sub = gsub false Neut 

814 
in 

815 
case u of 

816 
Cst (False, T, _) => Cst (False, T, Formula Neut) 

817 
 Cst (True, T, _) => Cst (True, T, Formula Neut) 

818 
 Cst (Num j, T, _) => 

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

819 
if is_word_type T then 
34126  820 
Cst (if is_twos_complement_representable bits j then Num j 
821 
else Unrep, T, best_opt_set_rep_for_type scope T) 

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

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

823 
let 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

824 
val (k, j0) = spec_of_type scope T 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

825 
val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

826 
else j < k) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

827 
in 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

828 
if ok then Cst (Num j, T, Atom (k, j0)) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

829 
else Cst (Unrep, T, Opt (Atom (k, j0))) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

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

831 
 Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) => 
33192  832 
let val R = Atom (spec_of_type scope T1) in 
833 
Cst (Suc, T, Func (R, Opt R)) 

834 
end 

835 
 Cst (Fracs, T, _) => 

836 
Cst (Fracs, T, best_non_opt_set_rep_for_type scope T) 

837 
 Cst (NormFrac, T, _) => 

838 
let val R1 = Atom (spec_of_type scope (domain_type T)) in 

839 
Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1])))) 

840 
end 

841 
 Cst (cst, T, _) => 

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

842 
if cst = Unknown orelse cst = Unrep then 
37483  843 
case (is_boolean_type T, polar > unsound ? flip_polarity) of 
33192  844 
(true, Pos) => Cst (False, T, Formula Pos) 
845 
 (true, Neg) => Cst (True, T, Formula Neg) 

846 
 _ => Cst (cst, T, best_opt_set_rep_for_type scope T) 

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

847 
else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm] 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

848 
cst then 
33192  849 
let 
850 
val T1 = domain_type T 

851 
val R1 = Atom (spec_of_type scope T1) 

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

852 
val total = T1 = nat_T andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

853 
(cst = Subtract orelse cst = Divide orelse cst = Gcd) 
33192  854 
in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

855 
else if cst = NatToInt orelse cst = IntToNat then 
33192  856 
let 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

857 
val (dom_card, dom_j0) = spec_of_type scope (domain_type T) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

858 
val (ran_card, ran_j0) = spec_of_type scope (range_type T) 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

859 
val total = not (is_word_type (domain_type T)) andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

860 
(if cst = NatToInt then 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

861 
max_int_for_card ran_card >= dom_card + 1 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

862 
else 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

863 
max_int_for_card dom_card < ran_card) 
33192  864 
in 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

865 
Cst (cst, T, Func (Atom (dom_card, dom_j0), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

866 
Atom (ran_card, ran_j0) > not total ? Opt)) 
33192  867 
end 
868 
else 

869 
Cst (cst, T, best_set_rep_for_type scope T) 

870 
 Op1 (Not, T, _, u1) => 

871 
(case gsub def (flip_polarity polar) u1 of 

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

872 
Op2 (Triad, T, _, u11, u12) => 
33192  873 
triad (s_op1 Not T (Formula Pos) u12) 
874 
(s_op1 Not T (Formula Neg) u11) 

875 
 u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1') 

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

876 
 Op1 (IsUnknown, T, _, u1) => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

877 
let val u1 = sub u1 in 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

878 
if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

879 
else Cst (False, T, Formula Neut) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

880 
end 
33192  881 
 Op1 (oper, T, _, u1) => 
882 
let 

883 
val u1 = sub u1 

884 
val R1 = rep_of u1 

885 
val R = case oper of 

886 
Finite => bool_rep polar (is_opt_rep R1) 

887 
 _ => (if is_opt_rep R1 then best_opt_set_rep_for_type 

888 
else best_non_opt_set_rep_for_type) scope T 

889 
in s_op1 oper T R u1 end 

890 
 Op2 (Less, T, _, u1, u2) => 

891 
let 

892 
val u1 = sub u1 

893 
val u2 = sub u2 

894 
val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2]) 

895 
in s_op2 Less T R u1 u2 end 

896 
 Op2 (Subset, T, _, u1, u2) => 

897 
let 

898 
val u1 = sub u1 

899 
val u2 = sub u2 

900 
val opt = exists (is_opt_rep o rep_of) [u1, u2] 

901 
val R = bool_rep polar opt 

902 
in 

903 
if is_opt_rep R then 

904 
triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2) 

36912
55b97cb3806e
produce more potential counterexamples for subset operator (cf. quantifiers)
blanchet
parents:
36385
diff
changeset

905 
else if not opt orelse unsound orelse polar = Neg orelse 
55b97cb3806e
produce more potential counterexamples for subset operator (cf. quantifiers)
blanchet
parents:
36385
diff
changeset

906 
is_concrete_type datatypes true (type_of u1) then 
55b97cb3806e
produce more potential counterexamples for subset operator (cf. quantifiers)
blanchet
parents:
36385
diff
changeset

907 
s_op2 Subset T R u1 u2 
55b97cb3806e
produce more potential counterexamples for subset operator (cf. quantifiers)
blanchet
parents:
36385
diff
changeset

908 
else 
33192  909 
Cst (False, T, Formula Pos) 
910 
end 

911 
 Op2 (DefEq, T, _, u1, u2) => 

912 
s_op2 DefEq T (Formula Neut) (sub u1) (sub u2) 

913 
 Op2 (Eq, T, _, u1, u2) => 

914 
let 

915 
val u1' = sub u1 

916 
val u2' = sub u2 

917 
fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2' 

918 
fun opt_opt_case () = 

919 
if polar = Neut then 

920 
triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2') 

921 
else 

922 
non_opt_case () 

923 
fun hybrid_case u = 

924 
(* hackish optimization *) 

925 
if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2' 

926 
else opt_opt_case () 

927 
in 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset

928 
if unsound orelse polar = Neg orelse 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

929 
is_concrete_type datatypes true (type_of u1) then 
33192  930 
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of 
931 
(true, true) => opt_opt_case () 

932 
 (true, false) => hybrid_case u1' 

933 
 (false, true) => hybrid_case u2' 

934 
 (false, false) => non_opt_case () 

935 
else 

936 
Cst (False, T, Formula Pos) 

937 
> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u)) 

938 
end 

939 
 Op2 (Image, T, _, u1, u2) => 

940 
let 

941 
val u1' = sub u1 

942 
val u2' = sub u2 

943 
in 

944 
(case (rep_of u1', rep_of u2') of 

945 
(Func (R11, R12), Func (R21, Formula Neut)) => 

946 
if R21 = R11 andalso is_lone_rep R12 then 

947 
let 

948 
val R = 

949 
best_non_opt_set_rep_for_type scope T 

950 
> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T 

951 
in s_op2 Image T R u1' u2' end 

952 
else 

953 
raise SAME () 

954 
 _ => raise SAME ()) 

955 
handle SAME () => 

956 
let 

957 
val T1 = type_of u1 

958 
val dom_T = domain_type T1 

959 
val ran_T = range_type T1 

960 
val x_u = BoundName (~1, dom_T, Any, "image.x") 

961 
val y_u = BoundName (~2, ran_T, Any, "image.y") 

962 
in 

963 
Op2 (Lambda, T, Any, y_u, 

964 
Op2 (Exist, bool_T, Any, x_u, 

965 
Op2 (And, bool_T, Any, 

966 
case u2 of 

967 
Op2 (Lambda, _, _, u21, u22) => 

36913  968 
if num_occurrences_in_nut u21 u22 = 0 then 
33192  969 
u22 
970 
else 

971 
Op2 (Apply, bool_T, Any, u2, x_u) 

972 
 _ => Op2 (Apply, bool_T, Any, u2, x_u), 

33571  973 

33192  974 
Op2 (Eq, bool_T, Any, y_u, 
975 
Op2 (Apply, ran_T, Any, u1, x_u))))) 

976 
> sub 

977 
end 

978 
end 

979 
 Op2 (Apply, T, _, u1, u2) => 

980 
let 

981 
val u1 = sub u1 

982 
val u2 = sub u2 

983 
val T1 = type_of u1 

984 
val R1 = rep_of u1 

985 
val R2 = rep_of u2 

986 
val opt = 

987 
case (u1, is_opt_rep R2) of 

988 
(ConstName (@{const_name set}, _, _), false) => false 

989 
 _ => exists is_opt_rep [R1, R2] 

990 
val ran_R = 

991 
if is_boolean_type T then 

992 
bool_rep polar opt 

993 
else 

36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35671
diff
changeset

994 
lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T) 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35671
diff
changeset

995 
(unopt_rep R1) 
33192  996 
> opt ? opt_rep ofs T 
997 
in s_op2 Apply T ran_R u1 u2 end 

998 
 Op2 (Lambda, T, _, u1, u2) => 

999 
(case best_set_rep_for_type scope T of 

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

1000 
R as Func (R1, _) => 
33192  1001 
let 
1002 
val table' = NameTable.update (u1, R1) table 

1003 
val u1' = aux table' false Neut u1 

1004 
val u2' = aux table' false Neut u2 

1005 
val R = 

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

1006 
if is_opt_rep (rep_of u2') orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1007 
(range_type T = bool_T andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1008 
not (is_Cst False (unrepify_nut_in_nut table false Neut 
36913  1009 
u1 u2))) then 
33192  1010 
opt_rep ofs T R 
1011 
else 

1012 
unopt_rep R 

1013 
in s_op2 Lambda T R u1' u2' end 

36913  1014 
 _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u])) 
33192  1015 
 Op2 (oper, T, _, u1, u2) => 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1016 
if oper = All orelse oper = Exist then 
33192  1017 
let 
1018 
val table' = fold (choose_rep_for_bound_var scope) (untuple I u1) 

1019 
table 

1020 
val u1' = aux table' def polar u1 

1021 
val u2' = aux table' def polar u2 

1022 
in 

1023 
if polar = Neut andalso is_opt_rep (rep_of u2') then 

1024 
triad_fn (fn polar => gsub def polar u) 

1025 
else 

1026 
let val quant_u = s_op2 oper T (Formula polar) u1' u2' in 

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

1027 
if def orelse 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset

1028 
(unsound andalso (polar = Pos) = (oper = All)) orelse 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

1029 
is_complete_type datatypes true (type_of u1) then 
33192  1030 
quant_u 
1031 
else 

1032 
let 

1033 
val connective = if oper = All then And else Or 

1034 
val unrepified_u = unrepify_nut_in_nut table def polar 

1035 
u1 u2 

1036 
in 

1037 
s_op2 connective T 

1038 
(min_rep (rep_of quant_u) (rep_of unrepified_u)) 

1039 
quant_u unrepified_u 

1040 
end 

1041 
end 

1042 
end 

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

1043 
else if oper = Or orelse oper = And then 
33192  1044 
let 
1045 
val u1' = gsub def polar u1 

1046 
val u2' = gsub def polar u2 

1047 
in 

1048 
(if polar = Neut then 

1049 
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of 

1050 
(true, true) => triad_fn (fn polar => gsub def polar u) 

1051 
 (true, false) => 

1052 
s_op2 oper T (Opt bool_atom_R) 

1053 
(triad_fn (fn polar => gsub def polar u1)) u2' 

1054 
 (false, true) => 

1055 
s_op2 oper T (Opt bool_atom_R) 

1056 
u1' (triad_fn (fn polar => gsub def polar u2)) 

1057 
 (false, false) => raise SAME () 

1058 
else 

1059 
raise SAME ()) 

1060 
handle SAME () => s_op2 oper T (Formula polar) u1' u2' 

1061 
end 

1062 
else 

1063 
let 

1064 
val u1 = sub u1 

1065 
val u2 = sub u2 

1066 
val R = 

1067 
best_non_opt_set_rep_for_type scope T 

1068 
> exists (is_opt_rep o rep_of) [u1, u2] ? opt_rep ofs T 

1069 
in s_op2 oper T R u1 u2 end 

1070 
 Op3 (Let, T, _, u1, u2, u3) => 

1071 
let 

1072 
val u2 = sub u2 

1073 
val R2 = rep_of u2 

1074 
val table' = NameTable.update (u1, R2) table 

1075 
val u1 = modify_name_rep u1 R2 

1076 
val u3 = aux table' false polar u3 

1077 
in s_op3 Let T (rep_of u3) u1 u2 u3 end 

1078 
 Op3 (If, T, _, u1, u2, u3) => 

1079 
let 

1080 
val u1 = sub u1 

1081 
val u2 = gsub def polar u2 

1082 
val u3 = gsub def polar u3 

1083 
val min_R = min_rep (rep_of u2) (rep_of u3) 

1084 
val R = min_R > is_opt_rep (rep_of u1) ? opt_rep ofs T 

1085 
in s_op3 If T R u1 u2 u3 end 

1086 
 Tuple (T, _, us) => 

1087 
let 

1088 
val Rs = map (best_one_rep_for_type scope o type_of) us 

1089 
val us = map sub us 

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

1090 
val R' = Struct Rs 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38171
diff
changeset

1091 
> exists (is_opt_rep o rep_of) us ? opt_rep ofs T 
33192  1092 
in s_tuple T R' us end 
1093 
 Construct (us', T, _, us) => 

1094 
let 

1095 
val us = map sub us 

1096 
val Rs = map rep_of us 

1097 
val R = best_one_rep_for_type scope T 

1098 
val {total, ...} = 

1099 
constr_spec datatypes (original_name (nickname_of (hd us')), T) 

1100 
val opt = exists is_opt_rep Rs orelse not total 

1101 
in Construct (map sub us', T, R > opt ? Opt, us) end 

1102 
 _ => 

1103 
let val u = modify_name_rep u (the_name table u) in 

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

1104 
if polar = Neut orelse not (is_boolean_type (type_of u)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1105 
not (is_opt_rep (rep_of u)) then 
33192  1106 
u 
1107 
else 

1108 
s_op1 Cast (type_of u) (Formula polar) u 

1109 
end 

1110 
end 

1111 
in aux table def Pos end 

1112 

1113 
fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys) 

1114 
 fresh_n_ary_index n ((m, j) :: xs) ys = 

1115 
if m = n then (j, ys @ ((m, j + 1) :: xs)) 

1116 
else fresh_n_ary_index n xs ((m, j) :: ys) 

1117 
fun fresh_rel n {rels, vars, formula_reg, rel_reg} = 

1118 
let val (j, rels') = fresh_n_ary_index n rels [] in 

1119 
(j, {rels = rels', vars = vars, formula_reg = formula_reg, 

1120 
rel_reg = rel_reg}) 

1121 
end 

1122 
fun fresh_var n {rels, vars, formula_reg, rel_reg} = 

1123 
let val (j, vars') = fresh_n_ary_index n vars [] in 

1124 
(j, {rels = rels, vars = vars', formula_reg = formula_reg, 

1125 
rel_reg = rel_reg}) 

1126 
end 

1127 
fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} = 

1128 
(formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1, 

1129 
rel_reg = rel_reg}) 

1130 
fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} = 

1131 
(rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg, 

1132 
rel_reg = rel_reg + 1}) 

1133 

1134 
fun rename_plain_var v (ws, pool, table) = 

1135 
let 

1136 
val is_formula = (rep_of v = Formula Neut) 

1137 
val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg 

1138 
val (j, pool) = fresh pool 

1139 
val constr = if is_formula then FormulaReg else RelReg 

1140 
val w = constr (j, type_of v, rep_of v) 

1141 
in (w :: ws, pool, NameTable.update (v, w) table) end 

1142 

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

1143 
fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2]) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

1144 
us = 
33192  1145 
let val arity1 = arity_of_rep R1 in 
1146 
Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), 

1147 
shape_tuple T2 R2 (List.drop (us, arity1))]) 

1148 
end 

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

1149 
 shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us = 
33192  1150 
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us)) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1151 
 shape_tuple T _ [u] = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1152 
if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u]) 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1153 
 shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) 
33192  1154 

1155 
fun rename_n_ary_var rename_free v (ws, pool, table) = 

1156 
let 

1157 
val T = type_of v 

1158 
val R = rep_of v 

1159 
val arity = arity_of_rep R 

1160 
val nick = nickname_of v 

1161 
val (constr, fresh) = if rename_free then (FreeRel, fresh_rel) 

1162 
else (BoundRel, fresh_var) 

1163 
in 

1164 
if not rename_free andalso arity > 1 then 

1165 
let 

1166 
val atom_schema = atom_schema_of_rep R 

1167 
val type_schema = type_schema_of_rep T R 

1168 
val (js, pool) = funpow arity (fn (js, pool) => 

1169 
let val (j, pool) = fresh 1 pool in 

1170 
(j :: js, pool) 

1171 
end) 

1172 
([], pool) 

1173 
val ws' = map3 (fn j => fn x => fn T => 

1174 
constr ((1, j), T, Atom x, 

1175 
nick ^ " [" ^ string_of_int j ^ "]")) 

1176 
(rev js) atom_schema type_schema 

1177 
in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end 

1178 
else 

1179 
let 

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

1180 
val (j, pool) = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1181 
case v of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1182 
ConstName _ => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1183 
if is_sel_like_and_no_discr nick then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1184 
case domain_type T of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1185 
@{typ "unsigned_bit word"} => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1186 
(snd unsigned_bit_word_sel_rel, pool) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1187 
 @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1188 
 _ => fresh arity pool 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

1190 
fresh arity pool 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

1191 
 _ => fresh arity pool 
33192  1192 
val w = constr ((arity, j), T, R, nick) 
1193 
in (w :: ws, pool, NameTable.update (v, w) table) end 

1194 
end 

1195 

1196 
fun rename_free_vars vs pool table = 

1197 
let 

1198 
val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table) 

1199 
in (rev vs, pool, table) end 

1200 

1201 
fun rename_vars_in_nut pool table u = 

1202 
case u of 

1203 
Cst _ => u 

1204 
 Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1) 

1205 
 Op2 (oper, T, R, u1, u2) => 

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

1206 
if oper = All orelse oper = Exist orelse oper = Lambda then 
33192  1207 
let 
1208 
val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1) 

1209 
([], pool, table) 

1210 
in 

1211 
Op2 (oper, T, R, rename_vars_in_nut pool table u1, 

1212 
rename_vars_in_nut pool table u2) 

1213 
end 

1214 
else 

1215 
Op2 (oper, T, R, rename_vars_in_nut pool table u1, 

1216 
rename_vars_in_nut pool table u2) 

1217 
 Op3 (Let, T, R, u1, u2, u3) => 

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

1218 
if inline_nut u2 then 
33192  1219 
let 
1220 
val u2 = rename_vars_in_nut pool table u2 

1221 
val table = NameTable.update (u1, u2) table 

1222 
in rename_vars_in_nut pool table u3 end 

1223 
else 

1224 
let 

1225 
val bs = untuple I u1 

1226 
val (_, pool, table') = fold rename_plain_var bs ([], pool, table) 

1227 
in 

1228 
Op3 (Let, T, R, rename_vars_in_nut pool table' u1, 

1229 
rename_vars_in_nut pool table u2, 

1230 
rename_vars_in_nut pool table' u3) 

1231 
end 

1232 
 Op3 (oper, T, R, u1, u2, u3) => 

1233 
Op3 (oper, T, R, rename_vars_in_nut pool table u1, 

1234 
rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3) 

1235 
 Tuple (T, R, us) => Tuple (T, R, map (rename_vars_in_nut pool table) us) 

1236 
 Construct (us', T, R, us) => 

1237 
Construct (map (rename_vars_in_nut pool table) us', T, R, 

1238 
map (rename_vars_in_nut pool table) us) 

1239 
 _ => the_name table u 

1240 

1241 
end; 