author  blanchet 
Wed, 20 Jan 2010 10:38:06 +0100  
changeset 34936  c4f04bee79f3 
parent 34288  cf455b5880e1 
child 34982  7b8c366e34a2 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_nut.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Copyright 2008, 2009 

4 

5 
Nitpick underlying terms (nuts). 

6 
*) 

7 

8 
signature NITPICK_NUT = 

9 
sig 

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

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

11 
type extended_context = Nitpick_HOL.extended_context 
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 
Unity  

18 
False  

19 
True  

20 
Iden  

21 
Num of int  

22 
Unknown  

23 
Unrep  

24 
Suc  

25 
Add  

26 
Subtract  

27 
Multiply  

28 
Divide  

29 
Gcd  

30 
Lcm  

31 
Fracs  

32 
NormFrac  

33 
NatToInt  

34 
IntToNat 

35 

36 
datatype op1 = 

37 
Not  

38 
Finite  

39 
Converse  

40 
Closure  

41 
SingletonSet  

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

42 
IsUnknown  
33192  43 
Tha  
44 
First  

45 
Second  

46 
Cast 

47 

48 
datatype op2 = 

49 
All  

50 
Exist  

51 
Or  

52 
And  

53 
Less  

54 
Subset  

55 
DefEq  

56 
Eq  

57 
The  

58 
Eps  

59 
Triad  

60 
Union  

61 
SetDifference  

62 
Intersect  

63 
Composition  

64 
Product  

65 
Image  

66 
Apply  

67 
Lambda 

68 

69 
datatype op3 = 

70 
Let  

71 
If 

72 

73 
datatype nut = 

74 
Cst of cst * typ * rep  

75 
Op1 of op1 * typ * rep * nut  

76 
Op2 of op2 * typ * rep * nut * nut  

77 
Op3 of op3 * typ * rep * nut * nut * nut  

78 
Tuple of typ * rep * nut list  

79 
Construct of nut list * typ * rep * nut list  

80 
BoundName of int * typ * rep * string  

81 
FreeName of string * typ * rep  

82 
ConstName of string * typ * rep  

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

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

85 
RelReg of int * typ * rep  

86 
FormulaReg of int * typ * rep 

87 

88 
structure NameTable : TABLE 

89 

90 
exception NUT of string * nut list 

91 

92 
val string_for_nut : Proof.context > nut > string 

93 
val inline_nut : nut > bool 

94 
val type_of : nut > typ 

95 
val rep_of : nut > rep 

96 
val nickname_of : nut > string 

97 
val is_skolem_name : nut > bool 

98 
val is_eval_name : nut > bool 

33631  99 
val is_FreeName : nut > bool 
33192  100 
val is_Cst : cst > nut > bool 
101 
val fold_nut : (nut > 'a > 'a) > nut > 'a > 'a 

102 
val map_nut : (nut > nut) > nut > nut 

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

104 
val add_free_and_const_names : 

105 
nut > nut list * nut list > nut list * nut list 

106 
val name_ord : (nut * nut) > order 

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

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

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

109 
val nut_from_term : extended_context > op2 > term > nut 
33192  110 
val choose_reps_for_free_vars : 
111 
scope > nut list > rep NameTable.table > nut list * rep NameTable.table 

112 
val choose_reps_for_consts : 

113 
scope > bool > nut list > rep NameTable.table 

114 
> nut list * rep NameTable.table 

115 
val choose_reps_for_all_sels : 

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

117 
val choose_reps_in_nut : 

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

119 
val rename_free_vars : 

120 
nut list > name_pool > nut NameTable.table 

121 
> nut list * name_pool * nut NameTable.table 

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

123 
end; 

124 

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

125 
structure Nitpick_Nut : NITPICK_NUT = 
33192  126 
struct 
127 

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

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

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

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

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

132 
open Nitpick_Rep 
33192  133 

34126  134 
structure KK = Kodkod 
135 

33192  136 
datatype cst = 
137 
Unity  

138 
False  

139 
True  

140 
Iden  

141 
Num of int  

142 
Unknown  

143 
Unrep  

144 
Suc  

145 
Add  

146 
Subtract  

147 
Multiply  

148 
Divide  

149 
Gcd  

150 
Lcm  

151 
Fracs  

152 
NormFrac  

153 
NatToInt  

154 
IntToNat 

155 

156 
datatype op1 = 

157 
Not  

158 
Finite  

159 
Converse  

160 
Closure  

161 
SingletonSet  

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

162 
IsUnknown  
33192  163 
Tha  
164 
First  

165 
Second  

166 
Cast 

167 

168 
datatype op2 = 

169 
All  

170 
Exist  

171 
Or  

172 
And  

173 
Less  

174 
Subset  

175 
DefEq  

176 
Eq  

177 
The  

178 
Eps  

179 
Triad  

180 
Union  

181 
SetDifference  

182 
Intersect  

183 
Composition  

184 
Product  

185 
Image  

186 
Apply  

187 
Lambda 

188 

189 
datatype op3 = 

190 
Let  

191 
If 

192 

193 
datatype nut = 

194 
Cst of cst * typ * rep  

195 
Op1 of op1 * typ * rep * nut  

196 
Op2 of op2 * typ * rep * nut * nut  

197 
Op3 of op3 * typ * rep * nut * nut * nut  

198 
Tuple of typ * rep * nut list  

199 
Construct of nut list * typ * rep * nut list  

200 
BoundName of int * typ * rep * string  

201 
FreeName of string * typ * rep  

202 
ConstName of string * typ * rep  

34126  203 
BoundRel of KK.n_ary_index * typ * rep * string  
204 
FreeRel of KK.n_ary_index * typ * rep * string  

33192  205 
RelReg of int * typ * rep  
206 
FormulaReg of int * typ * rep 

207 

208 
exception NUT of string * nut list 

209 

210 
(* cst > string *) 

211 
fun string_for_cst Unity = "Unity" 

212 
 string_for_cst False = "False" 

213 
 string_for_cst True = "True" 

214 
 string_for_cst Iden = "Iden" 

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

216 
 string_for_cst Unknown = "Unknown" 

217 
 string_for_cst Unrep = "Unrep" 

218 
 string_for_cst Suc = "Suc" 

219 
 string_for_cst Add = "Add" 

220 
 string_for_cst Subtract = "Subtract" 

221 
 string_for_cst Multiply = "Multiply" 

222 
 string_for_cst Divide = "Divide" 

223 
 string_for_cst Gcd = "Gcd" 

224 
 string_for_cst Lcm = "Lcm" 

225 
 string_for_cst Fracs = "Fracs" 

226 
 string_for_cst NormFrac = "NormFrac" 

227 
 string_for_cst NatToInt = "NatToInt" 

228 
 string_for_cst IntToNat = "IntToNat" 

229 

230 
(* op1 > string *) 

231 
fun string_for_op1 Not = "Not" 

232 
 string_for_op1 Finite = "Finite" 

233 
 string_for_op1 Converse = "Converse" 

234 
 string_for_op1 Closure = "Closure" 

235 
 string_for_op1 SingletonSet = "SingletonSet" 

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

236 
 string_for_op1 IsUnknown = "IsUnknown" 
33192  237 
 string_for_op1 Tha = "Tha" 
238 
 string_for_op1 First = "First" 

239 
 string_for_op1 Second = "Second" 

240 
 string_for_op1 Cast = "Cast" 

241 

242 
(* op2 > string *) 

243 
fun string_for_op2 All = "All" 

244 
 string_for_op2 Exist = "Exist" 

245 
 string_for_op2 Or = "Or" 

246 
 string_for_op2 And = "And" 

247 
 string_for_op2 Less = "Less" 

248 
 string_for_op2 Subset = "Subset" 

249 
 string_for_op2 DefEq = "DefEq" 

250 
 string_for_op2 Eq = "Eq" 

251 
 string_for_op2 The = "The" 

252 
 string_for_op2 Eps = "Eps" 

253 
 string_for_op2 Triad = "Triad" 

254 
 string_for_op2 Union = "Union" 

255 
 string_for_op2 SetDifference = "SetDifference" 

256 
 string_for_op2 Intersect = "Intersect" 

257 
 string_for_op2 Composition = "Composition" 

258 
 string_for_op2 Product = "Product" 

259 
 string_for_op2 Image = "Image" 

260 
 string_for_op2 Apply = "Apply" 

261 
 string_for_op2 Lambda = "Lambda" 

262 

263 
(* op3 > string *) 

264 
fun string_for_op3 Let = "Let" 

265 
 string_for_op3 If = "If" 

266 

267 
(* int > Proof.context > nut > string *) 

268 
fun basic_string_for_nut indent ctxt u = 

269 
let 

270 
(* nut > string *) 

271 
val sub = basic_string_for_nut (indent + 1) ctxt 

272 
in 

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

274 
"(" ^ 

275 
(case u of 

276 
Cst (c, T, R) => 

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

278 
string_for_rep R 

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

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

281 
string_for_rep R ^ " " ^ sub u1 

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

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

284 
string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 

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

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

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

288 
 Tuple (T, R, us) => 

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

290 
implode (map sub us) 

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

292 
"Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^ 

293 
" " ^ string_for_rep R ^ " " ^ implode (map sub us) 

294 
 BoundName (j, T, R, nick) => 

295 
"BoundName " ^ signed_string_of_int j ^ " " ^ 

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

297 
 FreeName (s, T, R) => 

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

299 
string_for_rep R 

300 
 ConstName (s, T, R) => 

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

302 
string_for_rep R 

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

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

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

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

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

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

309 
 RelReg (j, T, R) => 

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

311 
" " ^ string_for_rep R 

312 
 FormulaReg (j, T, R) => 

313 
"FormulaReg " ^ signed_string_of_int j ^ " " ^ 

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

315 
")" 

316 
end 

317 
(* Proof.context > nut > string *) 

318 
val string_for_nut = basic_string_for_nut 0 

319 

320 
(* nut > bool *) 

321 
fun inline_nut (Op1 _) = false 

322 
 inline_nut (Op2 _) = false 

323 
 inline_nut (Op3 _) = false 

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

325 
 inline_nut _ = true 

326 

327 
(* nut > typ *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

341 

342 
(* nut > rep *) 

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

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

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

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

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

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

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

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

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

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

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

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

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

356 

357 
(* nut > string *) 

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

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

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

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

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

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

363 
 nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u]) 
33192  364 

365 
(* nut > bool *) 

366 
fun is_skolem_name u = 

367 
space_explode name_sep (nickname_of u) 

368 
> exists (String.isPrefix skolem_prefix) 

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

369 
handle NUT ("Nitpick_Nut.nickname_of", _) => false 
33192  370 
fun is_eval_name u = 
371 
String.isPrefix eval_prefix (nickname_of u) 

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

372 
handle NUT ("Nitpick_Nut.nickname_of", _) => false 
33631  373 
fun is_FreeName (FreeName _) = true 
374 
 is_FreeName _ = false 

33192  375 
(* cst > nut > bool *) 
376 
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst') 

377 
 is_Cst _ _ = false 

378 

379 
(* (nut > 'a > 'a) > nut > 'a > 'a *) 

380 
fun fold_nut f u = 

381 
case u of 

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

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

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

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

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

387 
 _ => f u 

388 
(* (nut > nut) > nut > nut *) 

389 
fun map_nut f u = 

390 
case u of 

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

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

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

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

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

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

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

398 
 _ => f u 

399 

400 
(* nut * nut > order *) 

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

402 
int_ord (j1, j2) 

403 
 name_ord (BoundName _, _) = LESS 

404 
 name_ord (_, BoundName _) = GREATER 

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

406 
(case fast_string_ord (s1, s2) of 

407 
EQUAL => TermOrd.typ_ord (T1, T2) 

408 
 ord => ord) 

409 
 name_ord (FreeName _, _) = LESS 

410 
 name_ord (_, FreeName _) = GREATER 

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

412 
(case fast_string_ord (s1, s2) of 

413 
EQUAL => TermOrd.typ_ord (T1, T2) 

414 
 ord => ord) 

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

415 
 name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2]) 
33192  416 

417 
(* nut > nut > int *) 

418 
fun num_occs_in_nut needle_u stack_u = 

419 
fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0 

420 
(* nut > nut > bool *) 

421 
val is_subterm_of = not_equal 0 oo num_occs_in_nut 

422 

423 
(* nut > nut > nut > nut *) 

424 
fun substitute_in_nut needle_u needle_u' = 

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

426 

427 
(* nut > nut list * nut list > nut list * nut list *) 

428 
val add_free_and_const_names = 

429 
fold_nut (fn u => case u of 

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

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

432 
 _ => I) 

433 

434 
(* nut > rep > nut *) 

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

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

437 
 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

438 
 modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u]) 
33192  439 

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

441 

442 
(* 'a NameTable.table > nut > 'a *) 

443 
fun the_name table name = 

444 
case NameTable.lookup table name of 

445 
SOME u => u 

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

446 
 NONE => raise NUT ("Nitpick_Nut.the_name", [name]) 
34126  447 
(* nut NameTable.table > nut > KK.n_ary_index *) 
33192  448 
fun the_rel table name = 
449 
case the_name table name of 

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

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

451 
 u => raise NUT ("Nitpick_Nut.the_rel", [u]) 
33192  452 

453 
(* typ * term > typ * term *) 

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

455 
 mk_fst (T, t) = 

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

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

458 
end 

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

460 
(domain_type (range_type T), t2) 

461 
 mk_snd (T, t) = 

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

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

464 
end 

465 
(* typ * term > (typ * term) list *) 

466 
fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z] 

467 
 factorize z = [z] 

468 

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

469 
(* extended_context > op2 > term > nut *) 
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

470 
fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq = 
33192  471 
let 
472 
(* string list > typ list > term > nut *) 

473 
fun aux eq ss Ts t = 

474 
let 

475 
(* term > nut *) 

476 
val sub = aux Eq ss Ts 

477 
val sub' = aux eq ss Ts 

478 
(* string > typ > term > nut *) 

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

480 
(* typ > term > term > nut *) 

481 
fun sub_equals T t1 t2 = 

482 
let 

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

484 
val n = length binder_Ts 

485 
in 

486 
if eq = Eq andalso n > 0 then 

487 
let 

488 
val t1 = incr_boundvars n t1 

489 
val t2 = incr_boundvars n t2 

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

491 
val equation = Const (@{const_name "op ="}, 

492 
body_T > body_T > bool_T) 

493 
$ betapplys (t1, xs) $ betapplys (t2, xs) 

494 
val t = 

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

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

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

498 
binder_Ts (equation, n) > fst 

499 
in sub' t end 

500 
else 

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

502 
end 

503 
(* op2 > string > typ > term > nut *) 

504 
fun do_quantifier quant s T t1 = 

505 
let 

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

507 
val body_u = sub_abs s T t1 

508 
in 

509 
if is_subterm_of bound_u body_u then 

510 
Op2 (quant, bool_T, Any, bound_u, body_u) 

511 
else 

512 
body_u 

513 
end 

514 
(* term > term list > nut *) 

515 
fun do_apply t0 ts = 

516 
let 

517 
val (ts', t2) = split_last ts 

518 
val t1 = list_comb (t0, ts') 

519 
val T1 = fastype_of1 (Ts, t1) 

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

521 
in 

522 
case strip_comb t of 

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

524 
do_quantifier All s T t1 

525 
 (t0 as Const (@{const_name all}, T), [t1]) => 

526 
sub' (t0 $ eta_expand Ts t1 1) 

527 
 (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2 

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

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

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

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

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

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

534 
(case sub t1 of 

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

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

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

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

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

540 
do_quantifier All s T t1 

541 
 (t0 as Const (@{const_name All}, T), [t1]) => 

542 
sub' (t0 $ eta_expand Ts t1 1) 

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

544 
do_quantifier Exist s T t1 

545 
 (t0 as Const (@{const_name Ex}, T), [t1]) => 

546 
sub' (t0 $ eta_expand Ts t1 1) 

547 
 (t0 as Const (@{const_name The}, T), [t1]) => 

548 
if fast_descrs then 

549 
Op2 (The, range_type T, Any, sub t1, 

550 
sub (Const (@{const_name undefined_fast_The}, range_type T))) 

551 
else 

552 
do_apply t0 [t1] 

553 
 (t0 as Const (@{const_name Eps}, T), [t1]) => 

554 
if fast_descrs then 

555 
Op2 (Eps, range_type T, Any, sub t1, 

556 
sub (Const (@{const_name undefined_fast_Eps}, range_type T))) 

557 
else 

558 
do_apply t0 [t1] 

559 
 (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2 

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

561 
Op2 (And, bool_T, Any, sub' t1, sub' t2) 

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

563 
Op2 (Or, bool_T, Any, sub t1, sub t2) 

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

565 
Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2) 

566 
 (Const (@{const_name If}, T), [t1, t2, t3]) => 

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

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

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

570 
sub t1, sub_abs s T' t2) 

571 
 (t0 as Const (@{const_name Let}, T), [t1, t2]) => 

572 
sub (t0 $ t1 $ eta_expand Ts t2 1) 

573 
 (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any) 

574 
 (Const (@{const_name Pair}, T), [t1, t2]) => 

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

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

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

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

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

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

581 
 (Const (@{const_name insert}, T), [t1, t2]) => 

582 
(case t2 of 

583 
Abs (_, _, @{const False}) => 

584 
Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1) 

585 
 _ => 

586 
Op2 (Union, nth_range_type 2 T, Any, 

587 
Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1), sub t2)) 

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

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

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

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

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

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

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

595 
Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2') 

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

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

598 
 (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any) 

599 
 (Const (@{const_name finite}, T), [t1]) => 

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

600 
(if is_finite_type ext_ctxt (domain_type T) then 
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

601 
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

602 
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

603 
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

604 
 _ => Op1 (Finite, bool_T, Any, sub t1)) 
33192  605 
 (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any) 
606 
 (Const (@{const_name zero_nat_inst.zero_nat}, T), []) => 

607 
Cst (Num 0, T, Any) 

608 
 (Const (@{const_name one_nat_inst.one_nat}, T), []) => 

609 
Cst (Num 1, T, Any) 

610 
 (Const (@{const_name plus_nat_inst.plus_nat}, T), []) => 

611 
Cst (Add, T, Any) 

612 
 (Const (@{const_name minus_nat_inst.minus_nat}, T), []) => 

613 
Cst (Subtract, T, Any) 

614 
 (Const (@{const_name times_nat_inst.times_nat}, T), []) => 

615 
Cst (Multiply, T, Any) 

616 
 (Const (@{const_name div_nat_inst.div_nat}, T), []) => 

617 
Cst (Divide, T, Any) 

618 
 (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) => 

619 
Op2 (Less, bool_T, Any, sub t1, sub t2) 

620 
 (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) => 

621 
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) 

622 
 (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any) 

623 
 (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any) 

624 
 (Const (@{const_name zero_int_inst.zero_int}, T), []) => 

625 
Cst (Num 0, T, Any) 

626 
 (Const (@{const_name one_int_inst.one_int}, T), []) => 

627 
Cst (Num 1, T, Any) 

628 
 (Const (@{const_name plus_int_inst.plus_int}, T), []) => 

629 
Cst (Add, T, Any) 

630 
 (Const (@{const_name minus_int_inst.minus_int}, T), []) => 

631 
Cst (Subtract, T, Any) 

632 
 (Const (@{const_name times_int_inst.times_int}, T), []) => 

633 
Cst (Multiply, T, Any) 

634 
 (Const (@{const_name div_int_inst.div_int}, T), []) => 

635 
Cst (Divide, T, Any) 

636 
 (Const (@{const_name uminus_int_inst.uminus_int}, T), []) => 

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

637 
let val num_T = domain_type T in 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

638 
Op2 (Apply, num_T > num_T, Any, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

639 
Cst (Subtract, num_T > num_T > num_T, Any), 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

640 
Cst (Num 0, num_T, Any)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

641 
end 
33192  642 
 (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) => 
643 
Op2 (Less, bool_T, Any, sub t1, sub t2) 

644 
 (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) => 

645 
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1)) 

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

646 
 (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

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

648 
Op1 (IsUnknown, bool_T, Any, sub t1) 
33192  649 
 (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) => 
650 
Op1 (Tha, T2, Any, sub t1) 

651 
 (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any) 

652 
 (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any) 

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

654 
Cst (NatToInt, T, Any) 

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

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

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

657 
Cst (NatToInt, T, Any) 
33192  658 
 (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T), 
659 
[t1, t2]) => 

660 
Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2) 

661 
 (Const (@{const_name upper_semilattice_fun_inst.sup_fun}, T), 

662 
[t1, t2]) => 

663 
Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2) 

664 
 (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) => 

665 
Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2) 

666 
 (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) => 

667 
Op2 (Subset, bool_T, Any, sub t1, sub t2) 

668 
 (t0 as Const (x as (s, T)), ts) => 

669 
if is_constr thy x then 

670 
case num_binder_types T  length ts of 

671 
0 => Construct (map ((fn (s, T) => ConstName (s, T, Any)) 

672 
o nth_sel_for_constr x) 

673 
(~1 upto num_sels_for_constr_type T  1), 

674 
body_type T, Any, 

675 
ts > map (`(curry fastype_of1 Ts)) 

676 
> maps factorize > map (sub o snd)) 

677 
 k => sub (eta_expand Ts t k) 

678 
else if String.isPrefix numeral_prefix s then 

679 
Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any) 

680 
else 

681 
(case arity_of_built_in_const fast_descrs x of 

682 
SOME n => 

683 
(case n  length ts of 

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

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

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

688 
else do_apply t0 ts) 

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

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

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

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

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

696 
 (t0, ts) => do_apply t0 ts 

697 
end 

698 
in aux eq [] [] end 

699 

700 
(* scope > typ > rep *) 

701 
fun rep_for_abs_fun scope T = 

702 
let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in 

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

704 
end 

705 

706 
(* scope > nut > nut list * rep NameTable.table 

707 
> nut list * rep NameTable.table *) 

708 
fun choose_rep_for_free_var scope v (vs, table) = 

709 
let 

710 
val R = best_non_opt_set_rep_for_type scope (type_of v) 

711 
val v = modify_name_rep v R 

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

713 
(* scope > bool > nut > nut list * rep NameTable.table 

714 
> nut list * rep NameTable.table *) 

715 
fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes, 

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

716 
ofs, ...}) all_exact v (vs, table) = 
33192  717 
let 
718 
val x as (s, T) = (nickname_of v, type_of v) 

719 
val R = (if is_abs_fun thy x then 

720 
rep_for_abs_fun 

721 
else if is_rep_fun thy x then 

722 
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

723 
else if all_exact orelse is_skolem_name v orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

724 
member (op =) [@{const_name undefined_fast_The}, 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

725 
@{const_name undefined_fast_Eps}, 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

726 
@{const_name bisim}, 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

727 
@{const_name bisim_iterator_max}] 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

728 
(original_name s) then 
33192  729 
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

730 
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

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

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

733 
(original_name s) then 
33192  734 
best_set_rep_for_type 
735 
else 

736 
best_opt_set_rep_for_type) scope T 

737 
val v = modify_name_rep v R 

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

739 

740 
(* scope > nut list > rep NameTable.table > nut list * rep NameTable.table *) 

741 
fun choose_reps_for_free_vars scope vs table = 

742 
fold (choose_rep_for_free_var scope) vs ([], table) 

743 
(* scope > bool > nut list > rep NameTable.table 

744 
> nut list * rep NameTable.table *) 

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

745 
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

746 
fold (choose_rep_for_const scope all_exact) vs ([], table) 
33192  747 

748 
(* scope > styp > int > nut list * rep NameTable.table 

749 
> nut list * rep NameTable.table *) 

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

750 
fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n 
33192  751 
(vs, table) = 
752 
let 

753 
val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n 

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

754 
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

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

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

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

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

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

762 
(* scope > styp > nut list * rep NameTable.table 

763 
> nut list * rep NameTable.table *) 

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

765 
fold_rev (choose_rep_for_nth_sel_for_constr scope x) 

766 
(~1 upto num_sels_for_constr_type T  1) 

767 
(* scope > dtype_spec > nut list * rep NameTable.table 

768 
> nut list * rep NameTable.table *) 

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

769 
fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

770 
 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

771 
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs 
33192  772 
(* scope > rep NameTable.table > nut list * rep NameTable.table *) 
773 
fun choose_reps_for_all_sels (scope as {datatypes, ...}) = 

774 
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair [] 

775 

776 
(* scope > nut > rep NameTable.table > rep NameTable.table *) 

777 
fun choose_rep_for_bound_var scope v table = 

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

779 
NameTable.update (v, R) table 

780 
end 

781 

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

783 
threevalued logic, it would evaluate to a unrepresentable value ("unrep") 

33631  784 
according to the HOL semantics. For example, "Suc n" is constructive if "n" 
785 
is representable or "Unrep", because unknown implies unrep. *) 

33192  786 
(* nut > bool *) 
787 
fun is_constructive u = 

788 
is_Cst Unrep u orelse 

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

790 
case u of 

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

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

792 
 Cst (cst, T, _) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

793 
cst = Suc orelse (body_type T = nat_T andalso cst = Add) 
33192  794 
 Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2] 
795 
 Op3 (If, _, _, u1, u2, u3) => 

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

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

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

799 
 _ => false 

800 

801 
(* nut > nut *) 

802 
fun optimize_unit u = 

803 
if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u 

804 
(* typ > rep > nut *) 

805 
fun unknown_boolean T R = 

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

806 
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

807 
T, R) 
33192  808 

809 
(* op1 > typ > rep > nut > nut *) 

810 
fun s_op1 oper T R u1 = 

811 
((if oper = Not then 

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

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

814 
else raise SAME () 

815 
else 

816 
raise SAME ()) 

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

818 
> optimize_unit 

819 
(* op2 > typ > rep > nut > nut > nut *) 

820 
fun s_op2 oper T R u1 u2 = 

821 
((case oper of 

822 
Or => 

823 
if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R) 

824 
else if is_Cst False u1 then u2 

825 
else if is_Cst False u2 then u1 

826 
else raise SAME () 

827 
 And => 

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

829 
else if is_Cst True u1 then u2 

830 
else if is_Cst True u2 then u1 

831 
else raise SAME () 

832 
 Eq => 

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

834 
(true, true) => unknown_boolean T R 

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

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

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

838 
 Triad => 

839 
if is_Cst True u1 then u1 

840 
else if is_Cst False u2 then u2 

841 
else raise SAME () 

842 
 Apply => 

843 
if is_Cst Unrep u1 then 

844 
Cst (Unrep, T, R) 

845 
else if is_Cst Unrep u2 then 

846 
if is_constructive u1 then 

847 
Cst (Unrep, T, R) 

33631  848 
else if is_boolean_type T then 
849 
if is_FreeName u1 then Cst (False, T, Formula Neut) 

850 
else unknown_boolean T R 

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

853 
Cst (Unrep, T, R) 

854 
 _ => raise SAME () 

855 
else 

856 
raise SAME () 

857 
 _ => raise SAME ()) 

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

859 
> optimize_unit 

860 
(* op3 > typ > rep > nut > nut > nut > nut *) 

861 
fun s_op3 oper T R u1 u2 u3 = 

862 
((case oper of 

863 
Let => 

864 
if inline_nut u2 orelse num_occs_in_nut u1 u3 < 2 then 

865 
substitute_in_nut u1 u2 u3 

866 
else 

867 
raise SAME () 

868 
 _ => raise SAME ()) 

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

870 
> optimize_unit 

871 
(* typ > rep > nut list > nut *) 

872 
fun s_tuple T R us = 

873 
(if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)) 

874 
> optimize_unit 

875 

876 
(* theory > nut > nut *) 

877 
fun optimize_nut u = 

878 
case u of 

879 
Op1 (oper, T, R, u1) => s_op1 oper T R (optimize_nut u1) 

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

881 
s_op2 oper T R (optimize_nut u1) (optimize_nut u2) 

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

883 
s_op3 oper T R (optimize_nut u1) (optimize_nut u2) (optimize_nut u3) 

884 
 Tuple (T, R, us) => s_tuple T R (map optimize_nut us) 

885 
 Construct (us', T, R, us) => Construct (us', T, R, map optimize_nut us) 

886 
 _ => optimize_unit u 

887 

888 
(* (nut > 'a) > nut > 'a list *) 

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

890 
 untuple f u = if rep_of u = Unit then [] else [f u] 

891 

892 
(* scope > bool > rep NameTable.table > bool > nut > nut *) 

893 
fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, 

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

894 
bits, datatypes, ofs, ...}) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

895 
liberal table def = 
33192  896 
let 
897 
val bool_atom_R = Atom (2, offset_of_type ofs bool_T) 

898 
(* polarity > bool > rep *) 

899 
fun bool_rep polar opt = 

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

901 
(* nut > nut > nut *) 

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

903 
(* (polarity > nut) > nut *) 

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

905 
(* rep NameTable.table > bool > polarity > nut > nut > nut *) 

906 
fun unrepify_nut_in_nut table def polar needle_u = 

907 
let val needle_T = type_of needle_u in 

908 
substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown 

909 
else Unrep, needle_T, Any)) 

910 
#> aux table def polar 

911 
end 

912 
(* rep NameTable.table > bool > polarity > nut > nut *) 

913 
and aux table def polar u = 

914 
let 

915 
(* bool > polarity > nut > nut *) 

916 
val gsub = aux table 

917 
(* nut > nut *) 

918 
val sub = gsub false Neut 

919 
in 

920 
case u of 

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

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

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

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

924 
if is_word_type T then 
34126  925 
Cst (if is_twos_complement_representable bits j then Num j 
926 
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

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

928 
(case spec_of_type scope T of 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

929 
(1, j0) => if j = 0 then Cst (Unity, T, Unit) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

930 
else Cst (Unrep, T, Opt (Atom (1, j0))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

931 
 (k, j0) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

933 
val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

934 
else j < k) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

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

936 
if ok then Cst (Num j, T, Atom (k, j0)) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

937 
else Cst (Unrep, T, Opt (Atom (k, j0))) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

938 
end) 
33192  939 
 Cst (Suc, T as Type ("fun", [T1, _]), _) => 
940 
let val R = Atom (spec_of_type scope T1) in 

941 
Cst (Suc, T, Func (R, Opt R)) 

942 
end 

943 
 Cst (Fracs, T, _) => 

944 
Cst (Fracs, T, best_non_opt_set_rep_for_type scope T) 

945 
 Cst (NormFrac, T, _) => 

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

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

948 
end 

949 
 Cst (cst, T, _) => 

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

950 
if cst = Unknown orelse cst = Unrep then 
33192  951 
case (is_boolean_type T, polar) of 
952 
(true, Pos) => Cst (False, T, Formula Pos) 

953 
 (true, Neg) => Cst (True, T, Formula Neg) 

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

955 
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

956 
cst then 
33192  957 
let 
958 
val T1 = domain_type T 

959 
val R1 = Atom (spec_of_type scope T1) 

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

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

961 
(cst = Subtract orelse cst = Divide orelse cst = Gcd) 
33192  962 
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

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

965 
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

966 
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

967 
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

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

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

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

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

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

974 
Atom (ran_card, ran_j0) > not total ? Opt)) 
33192  975 
end 
976 
else 

977 
Cst (cst, T, best_set_rep_for_type scope T) 

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

979 
(case gsub def (flip_polarity polar) u1 of 

980 
Op2 (Triad, T, R, u11, u12) => 

981 
triad (s_op1 Not T (Formula Pos) u12) 

982 
(s_op1 Not T (Formula Neg) u11) 

983 
 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

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

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

986 
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

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

988 
end 
33192  989 
 Op1 (oper, T, _, u1) => 
990 
let 

991 
val u1 = sub u1 

992 
val R1 = rep_of u1 

993 
val R = case oper of 

994 
Finite => bool_rep polar (is_opt_rep R1) 

995 
 _ => (if is_opt_rep R1 then best_opt_set_rep_for_type 

996 
else best_non_opt_set_rep_for_type) scope T 

997 
in s_op1 oper T R u1 end 

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

999 
let 

1000 
val u1 = sub u1 

1001 
val u2 = sub u2 

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

1003 
in s_op2 Less T R u1 u2 end 

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

1005 
let 

1006 
val u1 = sub u1 

1007 
val u2 = sub u2 

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

1009 
val R = bool_rep polar opt 

1010 
in 

1011 
if is_opt_rep R then 

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

1013 
else if opt andalso polar = Pos andalso 

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

1014 
not (is_concrete_type datatypes (type_of u1)) then 
33192  1015 
Cst (False, T, Formula Pos) 
1016 
else 

1017 
s_op2 Subset T R u1 u2 

1018 
end 

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

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

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

1022 
let 

1023 
val u1' = sub u1 

1024 
val u2' = sub u2 

1025 
(* unit > nut *) 

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

1027 
(* unit > nut *) 

1028 
fun opt_opt_case () = 

1029 
if polar = Neut then 

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

1031 
else 

1032 
non_opt_case () 

1033 
(* nut > nut *) 

1034 
fun hybrid_case u = 

1035 
(* hackish optimization *) 

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

1037 
else opt_opt_case () 

1038 
in 

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

1039 
if liberal orelse polar = Neg orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1040 
is_concrete_type datatypes (type_of u1) then 
33192  1041 
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of 
1042 
(true, true) => opt_opt_case () 

1043 
 (true, false) => hybrid_case u1' 

1044 
 (false, true) => hybrid_case u2' 

1045 
 (false, false) => non_opt_case () 

1046 
else 

1047 
Cst (False, T, Formula Pos) 

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

1049 
end 

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

1051 
let 

1052 
val u1' = sub u1 

1053 
val u2' = sub u2 

1054 
in 

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

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

1057 
if R21 = R11 andalso is_lone_rep R12 then 

1058 
let 

1059 
val R = 

1060 
best_non_opt_set_rep_for_type scope T 

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

1062 
in s_op2 Image T R u1' u2' end 

1063 
else 

1064 
raise SAME () 

1065 
 _ => raise SAME ()) 

1066 
handle SAME () => 

1067 
let 

1068 
val T1 = type_of u1 

1069 
val dom_T = domain_type T1 

1070 
val ran_T = range_type T1 

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

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

1073 
in 

1074 
Op2 (Lambda, T, Any, y_u, 

1075 
Op2 (Exist, bool_T, Any, x_u, 

1076 
Op2 (And, bool_T, Any, 

1077 
case u2 of 

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

33571  1079 
if num_occs_in_nut u21 u22 = 0 then 
33192  1080 
u22 
1081 
else 

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

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

33571  1084 

33192  1085 
Op2 (Eq, bool_T, Any, y_u, 
1086 
Op2 (Apply, ran_T, Any, u1, x_u))))) 

1087 
> sub 

1088 
end 

1089 
end 

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

1091 
let 

1092 
val u1 = sub u1 

1093 
val u2 = sub u2 

1094 
val T1 = type_of u1 

1095 
val R1 = rep_of u1 

1096 
val R2 = rep_of u2 

1097 
val opt = 

1098 
case (u1, is_opt_rep R2) of 

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

1100 
 _ => exists is_opt_rep [R1, R2] 

1101 
val ran_R = 

1102 
if is_boolean_type T then 

1103 
bool_rep polar opt 

1104 
else 

1105 
smart_range_rep ofs T1 (fn () => card_of_type card_assigns T) 

1106 
(unopt_rep R1) 

1107 
> opt ? opt_rep ofs T 

1108 
in s_op2 Apply T ran_R u1 u2 end 

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

1110 
(case best_set_rep_for_type scope T of 

1111 
Unit => Cst (Unity, T, Unit) 

1112 
 R as Func (R1, _) => 

1113 
let 

1114 
val table' = NameTable.update (u1, R1) table 

1115 
val u1' = aux table' false Neut u1 

1116 
val u2' = aux table' false Neut u2 

1117 
val R = 

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

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

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

1120 
not (is_Cst False (unrepify_nut_in_nut table false Neut 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

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

1122 
> optimize_nut))) then 
33192  1123 
opt_rep ofs T R 
1124 
else 

1125 
unopt_rep R 

1126 
in s_op2 Lambda T R u1' u2' end 

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

1127 
 R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u])) 
33192  1128 
 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

1129 
if oper = All orelse oper = Exist then 
33192  1130 
let 
1131 
val table' = fold (choose_rep_for_bound_var scope) (untuple I u1) 

1132 
table 

1133 
val u1' = aux table' def polar u1 

1134 
val u2' = aux table' def polar u2 

1135 
in 

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

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

1138 
else 

1139 
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

1140 
if def orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1141 
(liberal andalso (polar = Pos) = (oper = All)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1142 
is_complete_type datatypes (type_of u1) then 
33192  1143 
quant_u 
1144 
else 

1145 
let 

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

1147 
val unrepified_u = unrepify_nut_in_nut table def polar 

1148 
u1 u2 

1149 
in 

1150 
s_op2 connective T 

1151 
(min_rep (rep_of quant_u) (rep_of unrepified_u)) 

1152 
quant_u unrepified_u 

1153 
end 

1154 
end 

1155 
end 

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

1156 
else if oper = Or orelse oper = And then 
33192  1157 
let 
1158 
val u1' = gsub def polar u1 

1159 
val u2' = gsub def polar u2 

1160 
in 

1161 
(if polar = Neut then 

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

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

1164 
 (true, false) => 

1165 
s_op2 oper T (Opt bool_atom_R) 

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

1167 
 (false, true) => 

1168 
s_op2 oper T (Opt bool_atom_R) 

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

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

1171 
else 

1172 
raise SAME ()) 

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

1174 
end 

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

1175 
else if oper = The orelse oper = Eps then 
33192  1176 
let 
1177 
val u1' = sub u1 

1178 
val opt1 = is_opt_rep (rep_of u1') 

33744
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33631
diff
changeset

1179 
val opt = (oper = Eps orelse opt1) 
33192  1180 
val unopt_R = best_one_rep_for_type scope T > optable_rep ofs T 
33744
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33631
diff
changeset

1181 
val R = if is_boolean_type T then bool_rep polar opt 
e82531ebf5f3
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
blanchet
parents:
33631
diff
changeset

1182 
else unopt_R > opt ? opt_rep ofs T 
33192  1183 
val u = Op2 (oper, T, R, u1', sub u2) 
1184 
in 

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

1185 
if is_complete_type datatypes T orelse not opt1 then 
33192  1186 
u 
1187 
else 

1188 
let 

1189 
val x_u = BoundName (~1, T, unopt_R, "descr.x") 

1190 
val R = R > opt_rep ofs T 

1191 
in 

1192 
Op3 (If, T, R, 

1193 
Op2 (Exist, bool_T, Formula Pos, x_u, 

1194 
s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1) 

1195 
x_u), u, Cst (Unknown, T, R)) 

1196 
end 

1197 
end 

1198 
else 

1199 
let 

1200 
val u1 = sub u1 

1201 
val u2 = sub u2 

1202 
val R = 

1203 
best_non_opt_set_rep_for_type scope T 

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

1205 
in s_op2 oper T R u1 u2 end 

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

1207 
let 

1208 
val u2 = sub u2 

1209 
val R2 = rep_of u2 

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

1211 
val u1 = modify_name_rep u1 R2 

1212 
val u3 = aux table' false polar u3 

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

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

1215 
let 

1216 
val u1 = sub u1 

1217 
val u2 = gsub def polar u2 

1218 
val u3 = gsub def polar u3 

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

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

1221 
in s_op3 If T R u1 u2 u3 end 

1222 
 Tuple (T, _, us) => 

1223 
let 

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

1225 
val us = map sub us 

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

1226 
val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs 
33192  1227 
val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R 
1228 
in s_tuple T R' us end 

1229 
 Construct (us', T, _, us) => 

1230 
let 

1231 
val us = map sub us 

1232 
val Rs = map rep_of us 

1233 
val R = best_one_rep_for_type scope T 

1234 
val {total, ...} = 

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

1236 
val opt = exists is_opt_rep Rs orelse not total 

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

1238 
 _ => 

1239 
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

1240 
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

1241 
not (is_opt_rep (rep_of u)) then 
33192  1242 
u 
1243 
else 

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

1245 
end 

1246 
end 

1247 
> optimize_unit 

1248 
in aux table def Pos end 

1249 

34126  1250 
(* int > KK.n_ary_index list > KK.n_ary_index list 
1251 
> int * KK.n_ary_index list *) 

33192  1252 
fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys) 
1253 
 fresh_n_ary_index n ((m, j) :: xs) ys = 

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

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

1256 
(* int > name_pool > int * name_pool *) 

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

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

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

1260 
rel_reg = rel_reg}) 

1261 
end 

1262 
(* int > name_pool > int * name_pool *) 

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

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

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

1266 
rel_reg = rel_reg}) 

1267 
end 

1268 
(* int > name_pool > int * name_pool *) 

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

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

1271 
rel_reg = rel_reg}) 

1272 
(* int > name_pool > int * name_pool *) 

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

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

1275 
rel_reg = rel_reg + 1}) 

1276 

1277 
(* nut > nut list * name_pool * nut NameTable.table 

1278 
> nut list * name_pool * nut NameTable.table *) 

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

1280 
let 

1281 
val is_formula = (rep_of v = Formula Neut) 

1282 
val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg 

1283 
val (j, pool) = fresh pool 

1284 
val constr = if is_formula then FormulaReg else RelReg 

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

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

1287 

1288 
(* typ > rep > nut list > nut *) 

1289 
fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us = 

1290 
let val arity1 = arity_of_rep R1 in 

1291 
Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)), 

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

1293 
end 

1294 
 shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us = 

1295 
Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us)) 

1296 
 shape_tuple T R [u] = 

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

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

1299 
 shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us) 
33192  1300 

1301 
(* bool > nut > nut list * name_pool * nut NameTable.table 

1302 
> nut list * name_pool * nut NameTable.table *) 

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

1304 
let 

1305 
val T = type_of v 

1306 
val R = rep_of v 

1307 
val arity = arity_of_rep R 

1308 
val nick = nickname_of v 

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

1310 
else (BoundRel, fresh_var) 

1311 
in 

1312 
if not rename_free andalso arity > 1 then 

1313 
let 

1314 
val atom_schema = atom_schema_of_rep R 

1315 
val type_schema = type_schema_of_rep T R 

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

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

1318 
(j :: js, pool) 

1319 
end) 

1320 
([], pool) 

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

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

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

1324 
(rev js) atom_schema type_schema 

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

1326 
else 

1327 
let 

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

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

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

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

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

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

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

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

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

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

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

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

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

1342 
end 

1343 

1344 
(* nut list > name_pool > nut NameTable.table 

1345 
> nut list * name_pool * nut NameTable.table *) 

1346 
fun rename_free_vars vs pool table = 

1347 
let 

1348 
val vs = filter (not_equal Unit o rep_of) vs 

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

1350 
in (rev vs, pool, table) end 

1351 

1352 
(* name_pool > nut NameTable.table > nut > nut *) 

1353 
fun rename_vars_in_nut pool table u = 

1354 
case u of 

1355 
Cst _ => u 

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

1357 
 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

1358 
if oper = All orelse oper = Exist orelse oper = Lambda then 
33192  1359 
let 
1360 
val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1) 

1361 
([], pool, table) 

1362 
in 

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

1364 
rename_vars_in_nut pool table u2) 

1365 
end 

1366 
else 

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

1368 
rename_vars_in_nut pool table u2) 

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

1370 
if rep_of u2 = Unit orelse inline_nut u2 then 

1371 
let 

1372 
val u2 = rename_vars_in_nut pool table u2 

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

1374 
in rename_vars_in_nut pool table u3 end 
