33192

1 
(* Title: HOL/Nitpick/Tools/nitpick_nut.ML


2 
Author: Jasmin Blanchette, TU Muenchen


3 
Copyright 2008, 2009


4 


5 
Nitpick underlying terms (nuts).


6 
*)


7 


8 
signature NITPICK_NUT =


9 
sig


10 
type special_fun = NitpickHOL.special_fun


11 
type extended_context = NitpickHOL.extended_context


12 
type scope = NitpickScope.scope


13 
type name_pool = NitpickPeephole.name_pool


14 
type rep = NitpickRep.rep


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 
Modulo 


30 
Gcd 


31 
Lcm 


32 
Fracs 


33 
NormFrac 


34 
NatToInt 


35 
IntToNat


36 


37 
datatype op1 =


38 
Not 


39 
Finite 


40 
Converse 


41 
Closure 


42 
SingletonSet 


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


99 
val is_Cst : cst > nut > bool


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


101 
val map_nut : (nut > nut) > nut > nut


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


103 
val add_free_and_const_names :


104 
nut > nut list * nut list > nut list * nut list


105 
val name_ord : (nut * nut) > order


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


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


108 
val nut_from_term : theory > bool > special_fun list > op2 > term > nut


109 
val choose_reps_for_free_vars :


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


111 
val choose_reps_for_consts :


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


113 
> nut list * rep NameTable.table


114 
val choose_reps_for_all_sels :


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


116 
val choose_reps_in_nut :


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


118 
val rename_free_vars :


119 
nut list > name_pool > nut NameTable.table


120 
> nut list * name_pool * nut NameTable.table


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


122 
end;


123 


124 
structure NitpickNut : NITPICK_NUT =


125 
struct


126 


127 
open NitpickUtil


128 
open NitpickHOL


129 
open NitpickScope


130 
open NitpickPeephole


131 
open NitpickRep


132 


133 
datatype cst =


134 
Unity 


135 
False 


136 
True 


137 
Iden 


138 
Num of int 


139 
Unknown 


140 
Unrep 


141 
Suc 


142 
Add 


143 
Subtract 


144 
Multiply 


145 
Divide 


146 
Modulo 


147 
Gcd 


148 
Lcm 


149 
Fracs 


150 
NormFrac 


151 
NatToInt 


152 
IntToNat


153 


154 
datatype op1 =


155 
Not 


156 
Finite 


157 
Converse 


158 
Closure 


159 
SingletonSet 


160 
Tha 


161 
First 


162 
Second 


163 
Cast


164 


165 
datatype op2 =


166 
All 


167 
Exist 


168 
Or 


169 
And 


170 
Less 


171 
Subset 


172 
DefEq 


173 
Eq 


174 
The 


175 
Eps 


176 
Triad 


177 
Union 


178 
SetDifference 


179 
Intersect 


180 
Composition 


181 
Product 


182 
Image 


183 
Apply 


184 
Lambda


185 


186 
datatype op3 =


187 
Let 


188 
If


189 


190 
datatype nut =


191 
Cst of cst * typ * rep 


192 
Op1 of op1 * typ * rep * nut 


193 
Op2 of op2 * typ * rep * nut * nut 


194 
Op3 of op3 * typ * rep * nut * nut * nut 


195 
Tuple of typ * rep * nut list 


196 
Construct of nut list * typ * rep * nut list 


197 
BoundName of int * typ * rep * string 


198 
FreeName of string * typ * rep 


199 
ConstName of string * typ * rep 


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


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


202 
RelReg of int * typ * rep 


203 
FormulaReg of int * typ * rep


204 


205 
exception NUT of string * nut list


206 


207 
(* cst > string *)


208 
fun string_for_cst Unity = "Unity"


209 
 string_for_cst False = "False"


210 
 string_for_cst True = "True"


211 
 string_for_cst Iden = "Iden"


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


213 
 string_for_cst Unknown = "Unknown"


214 
 string_for_cst Unrep = "Unrep"


215 
 string_for_cst Suc = "Suc"


216 
 string_for_cst Add = "Add"


217 
 string_for_cst Subtract = "Subtract"


218 
 string_for_cst Multiply = "Multiply"


219 
 string_for_cst Divide = "Divide"


220 
 string_for_cst Modulo = "Modulo"


221 
 string_for_cst Gcd = "Gcd"


222 
 string_for_cst Lcm = "Lcm"


223 
 string_for_cst Fracs = "Fracs"


224 
 string_for_cst NormFrac = "NormFrac"


225 
 string_for_cst NatToInt = "NatToInt"


226 
 string_for_cst IntToNat = "IntToNat"


227 


228 
(* op1 > string *)


229 
fun string_for_op1 Not = "Not"


230 
 string_for_op1 Finite = "Finite"


231 
 string_for_op1 Converse = "Converse"


232 
 string_for_op1 Closure = "Closure"


233 
 string_for_op1 SingletonSet = "SingletonSet"


234 
 string_for_op1 Tha = "Tha"


235 
 string_for_op1 First = "First"


236 
 string_for_op1 Second = "Second"


237 
 string_for_op1 Cast = "Cast"


238 


239 
(* op2 > string *)


240 
fun string_for_op2 All = "All"


241 
 string_for_op2 Exist = "Exist"


242 
 string_for_op2 Or = "Or"


243 
 string_for_op2 And = "And"


244 
 string_for_op2 Less = "Less"


245 
 string_for_op2 Subset = "Subset"


246 
 string_for_op2 DefEq = "DefEq"


247 
 string_for_op2 Eq = "Eq"


248 
 string_for_op2 The = "The"


249 
 string_for_op2 Eps = "Eps"


250 
 string_for_op2 Triad = "Triad"


251 
 string_for_op2 Union = "Union"


252 
 string_for_op2 SetDifference = "SetDifference"


253 
 string_for_op2 Intersect = "Intersect"


254 
 string_for_op2 Composition = "Composition"


255 
 string_for_op2 Product = "Product"


256 
 string_for_op2 Image = "Image"


257 
 string_for_op2 Apply = "Apply"


258 
 string_for_op2 Lambda = "Lambda"


259 


260 
(* op3 > string *)


261 
fun string_for_op3 Let = "Let"


262 
 string_for_op3 If = "If"


263 


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


265 
fun basic_string_for_nut indent ctxt u =


266 
let


267 
(* nut > string *)


268 
val sub = basic_string_for_nut (indent + 1) ctxt


269 
in


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


271 
"(" ^


272 
(case u of


273 
Cst (c, T, R) =>


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


275 
string_for_rep R


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


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


278 
string_for_rep R ^ " " ^ sub u1


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


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


281 
string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2


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


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


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


285 
 Tuple (T, R, us) =>


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


287 
implode (map sub us)


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


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


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


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


292 
"BoundName " ^ signed_string_of_int j ^ " " ^


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


294 
 FreeName (s, T, R) =>


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


296 
string_for_rep R


297 
 ConstName (s, T, R) =>


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


299 
string_for_rep R


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


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


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


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


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


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


306 
 RelReg (j, T, R) =>


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


308 
" " ^ string_for_rep R


309 
 FormulaReg (j, T, R) =>


310 
"FormulaReg " ^ signed_string_of_int j ^ " " ^


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


312 
")"


313 
end


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


315 
val string_for_nut = basic_string_for_nut 0


316 


317 
(* nut > bool *)


318 
fun inline_nut (Op1 _) = false


319 
 inline_nut (Op2 _) = false


320 
 inline_nut (Op3 _) = false


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


322 
 inline_nut _ = true


323 


324 
(* nut > typ *)


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


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


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


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


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


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


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


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


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


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


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


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


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


338 


339 
(* nut > rep *)


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


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


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


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


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


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


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


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


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


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


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


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


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


353 


354 
(* nut > string *)


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


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


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


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


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


360 
 nickname_of u = raise NUT ("NitpickNut.nickname_of", [u])


361 


362 
(* nut > bool *)


363 
fun is_skolem_name u =


364 
space_explode name_sep (nickname_of u)


365 
> exists (String.isPrefix skolem_prefix)


366 
handle NUT ("NitpickNut.nickname_of", _) => false


367 
fun is_eval_name u =


368 
String.isPrefix eval_prefix (nickname_of u)


369 
handle NUT ("NitpickNut.nickname_of", _) => false


370 
(* cst > nut > bool *)


371 
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')


372 
 is_Cst _ _ = false


373 


374 
(* (nut > 'a > 'a) > nut > 'a > 'a *)


375 
fun fold_nut f u =


376 
case u of


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


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


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


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


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


382 
 _ => f u


383 
(* (nut > nut) > nut > nut *)


384 
fun map_nut f u =


385 
case u of


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


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


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


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


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


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


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


393 
 _ => f u


394 


395 
(* nut * nut > order *)


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


397 
int_ord (j1, j2)


398 
 name_ord (BoundName _, _) = LESS


399 
 name_ord (_, BoundName _) = GREATER


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


401 
(case fast_string_ord (s1, s2) of


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


403 
 ord => ord)


404 
 name_ord (FreeName _, _) = LESS


405 
 name_ord (_, FreeName _) = GREATER


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


407 
(case fast_string_ord (s1, s2) of


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


409 
 ord => ord)


410 
 name_ord (u1, u2) = raise NUT ("NitpickNut.name_ord", [u1, u2])


411 


412 
(* nut > nut > int *)


413 
fun num_occs_in_nut needle_u stack_u =


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


415 
(* nut > nut > bool *)


416 
val is_subterm_of = not_equal 0 oo num_occs_in_nut


417 


418 
(* nut > nut > nut > nut *)


419 
fun substitute_in_nut needle_u needle_u' =


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


421 


422 
(* nut > nut list * nut list > nut list * nut list *)


423 
val add_free_and_const_names =


424 
fold_nut (fn u => case u of


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


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


427 
 _ => I)


428 


429 
(* nut > rep > nut *)


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


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


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


433 
 modify_name_rep u _ = raise NUT ("NitpickNut.modify_name_rep", [u])


434 


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


436 


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


438 
fun the_name table name =


439 
case NameTable.lookup table name of


440 
SOME u => u


441 
 NONE => raise NUT ("NitpickNut.the_name", [name])


442 
(* nut NameTable.table > nut > Kodkod.n_ary_index *)


443 
fun the_rel table name =


444 
case the_name table name of


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


446 
 u => raise NUT ("NitpickNut.the_rel", [u])


447 


448 
(* typ * term > typ * term *)


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


450 
 mk_fst (T, t) =


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


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


453 
end


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


455 
(domain_type (range_type T), t2)


456 
 mk_snd (T, t) =


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


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


459 
end


460 
(* typ * term > (typ * term) list *)


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


462 
 factorize z = [z]


463 


464 
(* theory > bool > special_fun list > op2 > term > nut *)


465 
fun nut_from_term thy fast_descrs special_funs eq =


466 
let


467 
(* string list > typ list > term > nut *)


468 
fun aux eq ss Ts t =


469 
let


470 
(* term > nut *)


471 
val sub = aux Eq ss Ts


472 
val sub' = aux eq ss Ts


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


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


475 
(* typ > term > term > nut *)


476 
fun sub_equals T t1 t2 =


477 
let


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


479 
val n = length binder_Ts


480 
in


481 
if eq = Eq andalso n > 0 then


482 
let


483 
val t1 = incr_boundvars n t1


484 
val t2 = incr_boundvars n t2


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


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


487 
body_T > body_T > bool_T)


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


489 
val t =


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


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


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


493 
binder_Ts (equation, n) > fst


494 
in sub' t end


495 
else


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


497 
end


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


499 
fun do_quantifier quant s T t1 =


500 
let


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


502 
val body_u = sub_abs s T t1


503 
in


504 
if is_subterm_of bound_u body_u then


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


506 
else


507 
body_u


508 
end


509 
(* term > term list > nut *)


510 
fun do_apply t0 ts =


511 
let


512 
val (ts', t2) = split_last ts


513 
val t1 = list_comb (t0, ts')


514 
val T1 = fastype_of1 (Ts, t1)


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


516 
in


517 
case strip_comb t of


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


519 
do_quantifier All s T t1


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


521 
sub' (t0 $ eta_expand Ts t1 1)


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


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


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


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


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


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


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


529 
(case sub t1 of


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


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


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


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


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


535 
do_quantifier All s T t1


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


537 
sub' (t0 $ eta_expand Ts t1 1)


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


539 
do_quantifier Exist s T t1


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


541 
sub' (t0 $ eta_expand Ts t1 1)


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


543 
if fast_descrs then


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


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


546 
else


547 
do_apply t0 [t1]


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


549 
if fast_descrs then


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


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


552 
else


553 
do_apply t0 [t1]


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


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


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


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


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


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


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


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


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


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


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


565 
sub t1, sub_abs s T' t2)


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


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


568 
 (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)


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


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


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


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


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


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


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


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


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


578 
(case t2 of


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


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


581 
 _ =>


582 
Op2 (Union, nth_range_type 2 T, Any,


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


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


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


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


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


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


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


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


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


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


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


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


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


596 
Op1 (Finite, bool_T, Any, sub t1)


597 
 (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)


598 
 (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>


599 
Cst (Num 0, T, Any)


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


601 
Cst (Num 1, T, Any)


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


603 
Cst (Add, T, Any)


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


605 
Cst (Subtract, T, Any)


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


607 
Cst (Multiply, T, Any)


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


609 
Cst (Divide, T, Any)


610 
 (Const (@{const_name div_nat_inst.mod_nat}, T), []) =>


611 
Cst (Modulo, T, Any)


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


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


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


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


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


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


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


619 
Cst (Num 0, T, Any)


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


621 
Cst (Num 1, T, Any)


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


623 
Cst (Add, T, Any)


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


625 
Cst (Subtract, T, Any)


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


627 
Cst (Multiply, T, Any)


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


629 
Cst (Divide, T, Any)


630 
 (Const (@{const_name div_int_inst.mod_int}, T), []) =>


631 
Cst (Modulo, T, Any)


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


633 
Op2 (Apply, int_T > int_T, Any,


634 
Cst (Subtract, [int_T, int_T] > int_T, Any),


635 
Cst (Num 0, int_T, Any))


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


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


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


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


640 
 (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>


641 
Op1 (Tha, T2, Any, sub t1)


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


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


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


645 
Cst (NatToInt, T, Any)


646 
 (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T),


647 
[t1, t2]) =>


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


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


650 
[t1, t2]) =>


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


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


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


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


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


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


657 
if is_constr thy x then


658 
case num_binder_types T  length ts of


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


660 
o nth_sel_for_constr x)


661 
(~1 upto num_sels_for_constr_type T  1),


662 
body_type T, Any,


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


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


665 
 k => sub (eta_expand Ts t k)


666 
else if String.isPrefix numeral_prefix s then


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


668 
else


669 
(case arity_of_built_in_const fast_descrs x of


670 
SOME n =>


671 
(case n  length ts of


672 
0 => raise TERM ("NitpickNut.nut_from_term.aux", [t])


673 
 k => if k > 0 then sub (eta_expand Ts t k)


674 
else do_apply t0 ts)


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


676 
else do_apply t0 ts)


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


678 
 (Var _, []) => raise TERM ("NitpickNut.nut_from_term", [t])


679 
 (Bound j, []) =>


680 
BoundName (length Ts  j  1, nth Ts j, Any, nth ss j)


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


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


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


684 
 (t0, ts) => do_apply t0 ts


685 
end


686 
in aux eq [] [] end


687 


688 
(* scope > typ > rep *)


689 
fun rep_for_abs_fun scope T =


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


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


692 
end


693 


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


695 
> nut list * rep NameTable.table *)


696 
fun choose_rep_for_free_var scope v (vs, table) =


697 
let


698 
val R = best_non_opt_set_rep_for_type scope (type_of v)


699 
val v = modify_name_rep v R


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


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


702 
> nut list * rep NameTable.table *)


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


704 
ofs, ...}) all_precise v (vs, table) =


705 
let


706 
val x as (s, T) = (nickname_of v, type_of v)


707 
val R = (if is_abs_fun thy x then


708 
rep_for_abs_fun


709 
else if is_rep_fun thy x then


710 
Func oo best_non_opt_symmetric_reps_for_fun_type


711 
else if all_precise orelse is_skolem_name v


712 
orelse s mem [@{const_name undefined_fast_The},


713 
@{const_name undefined_fast_Eps},


714 
@{const_name bisim}] then


715 
best_non_opt_set_rep_for_type


716 
else if original_name s


717 
mem [@{const_name set}, @{const_name distinct},


718 
@{const_name ord_class.less},


719 
@{const_name ord_class.less_eq},


720 
@{const_name bisim_iterator_max}] then


721 
best_set_rep_for_type


722 
else


723 
best_opt_set_rep_for_type) scope T


724 
val v = modify_name_rep v R


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


726 


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


728 
fun choose_reps_for_free_vars scope vs table =


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


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


731 
> nut list * rep NameTable.table *)


732 
fun choose_reps_for_consts scope all_precise vs table =


733 
fold (choose_rep_for_const scope all_precise) vs ([], table)


734 


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


736 
> nut list * rep NameTable.table *)


737 
fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) x n


738 
(vs, table) =


739 
let


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


741 
val R' = if n = ~1 then best_non_opt_set_rep_for_type scope T'


742 
else best_opt_set_rep_for_type scope T' > unopt_rep


743 
val v = ConstName (s', T', R')


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


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


746 
> nut list * rep NameTable.table *)


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


748 
fold_rev (choose_rep_for_nth_sel_for_constr scope x)


749 
(~1 upto num_sels_for_constr_type T  1)


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


751 
> nut list * rep NameTable.table *)


752 
fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) =


753 
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs


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


755 
fun choose_reps_for_all_sels (scope as {datatypes, ...}) =


756 
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []


757 


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


759 
fun choose_rep_for_bound_var scope v table =


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


761 
NameTable.update (v, R) table


762 
end


763 


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


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


766 
according to the HOL semantics. For example, "Suc n" is


767 
constructive if "n" is representable or "Unrep", because unknown implies


768 
unrep. *)


769 
(* nut > bool *)


770 
fun is_constructive u =


771 
is_Cst Unrep u orelse


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


773 
case u of


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


775 
 Cst (cst, T, _) => cst = Suc orelse (body_type T = nat_T andalso cst = Add)


776 
 Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]


777 
 Op3 (If, _, _, u1, u2, u3) =>


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


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


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


781 
 _ => false


782 


783 
(* nut > nut *)


784 
fun optimize_unit u =


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


786 
(* typ > rep > nut *)


787 
fun unknown_boolean T R =


788 
Cst (case R of


789 
Formula Pos => False


790 
 Formula Neg => True


791 
 _ => Unknown, T, R)


792 


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


794 
fun s_op1 oper T R u1 =


795 
((if oper = Not then


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


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


798 
else raise SAME ()


799 
else


800 
raise SAME ())


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


802 
> optimize_unit


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


804 
fun s_op2 oper T R u1 u2 =


805 
((case oper of


806 
Or =>


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


808 
else if is_Cst False u1 then u2


809 
else if is_Cst False u2 then u1


810 
else raise SAME ()


811 
 And =>


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


813 
else if is_Cst True u1 then u2


814 
else if is_Cst True u2 then u1


815 
else raise SAME ()


816 
 Eq =>


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


818 
(true, true) => unknown_boolean T R


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


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


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


822 
 Triad =>


823 
if is_Cst True u1 then u1


824 
else if is_Cst False u2 then u2


825 
else raise SAME ()


826 
 Apply =>


827 
if is_Cst Unrep u1 then


828 
Cst (Unrep, T, R)


829 
else if is_Cst Unrep u2 then


830 
if is_constructive u1 then


831 
Cst (Unrep, T, R)


832 
else if is_boolean_type T andalso not (is_opt_rep (rep_of u1)) then


833 
(* Selectors are an unfortunate exception to the rule that non"Opt"


834 
predicates return "False" for unrepresentable domain values. *)


835 
case u1 of


836 
ConstName (s, _, _) => if is_sel s then unknown_boolean T R


837 
else Cst (False, T, Formula Neut)


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


839 
else case u1 of


840 
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>


841 
Cst (Unrep, T, R)


842 
 _ => raise SAME ()


843 
else


844 
raise SAME ()


845 
 _ => raise SAME ())


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


847 
> optimize_unit


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


849 
fun s_op3 oper T R u1 u2 u3 =


850 
((case oper of


851 
Let =>


852 
if inline_nut u2 orelse num_occs_in_nut u1 u3 < 2 then


853 
substitute_in_nut u1 u2 u3


854 
else


855 
raise SAME ()


856 
 _ => raise SAME ())


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


858 
> optimize_unit


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


860 
fun s_tuple T R us =


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


862 
> optimize_unit


863 


864 
(* theory > nut > nut *)


865 
fun optimize_nut u =


866 
case u of


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


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


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


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


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


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


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


874 
 _ => optimize_unit u


875 


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


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


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


879 


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


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


882 
datatypes, ofs, ...}) liberal table def =


883 
let


884 
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)


885 
(* polarity > bool > rep *)


886 
fun bool_rep polar opt =


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


888 
(* nut > nut > nut *)


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


890 
(* (polarity > nut) > nut *)


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


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


893 
fun unrepify_nut_in_nut table def polar needle_u =


894 
let val needle_T = type_of needle_u in


895 
substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown


896 
else Unrep, needle_T, Any))


897 
#> aux table def polar


898 
end


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


900 
and aux table def polar u =


901 
let


902 
(* bool > polarity > nut > nut *)


903 
val gsub = aux table


904 
(* nut > nut *)


905 
val sub = gsub false Neut


906 
in


907 
case u of


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


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


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


911 
(case spec_of_type scope T of


912 
(1, j0) => if j = 0 then Cst (Unity, T, Unit)


913 
else Cst (Unrep, T, Opt (Atom (1, j0)))


914 
 (k, j0) =>


915 
let


916 
val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1


917 
else j < k)


918 
in


919 
if ok then Cst (Num j, T, Atom (k, j0))


920 
else Cst (Unrep, T, Opt (Atom (k, j0)))


921 
end)


922 
 Cst (Suc, T as Type ("fun", [T1, _]), _) =>


923 
let val R = Atom (spec_of_type scope T1) in


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


925 
end


926 
 Cst (Fracs, T, _) =>


927 
Cst (Fracs, T, best_non_opt_set_rep_for_type scope T)


928 
 Cst (NormFrac, T, _) =>


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


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


931 
end


932 
 Cst (cst, T, _) =>


933 
if cst mem [Unknown, Unrep] then


934 
case (is_boolean_type T, polar) of


935 
(true, Pos) => Cst (False, T, Formula Pos)


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


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


938 
else if cst mem [Add, Subtract, Multiply, Divide, Modulo, Gcd,


939 
Lcm] then


940 
let


941 
val T1 = domain_type T


942 
val R1 = Atom (spec_of_type scope T1)


943 
val total =


944 
T1 = nat_T andalso cst mem [Subtract, Divide, Modulo, Gcd]


945 
in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end


946 
else if cst mem [NatToInt, IntToNat] then


947 
let


948 
val (nat_card, nat_j0) = spec_of_type scope nat_T


949 
val (int_card, int_j0) = spec_of_type scope int_T


950 
in


951 
if cst = NatToInt then


952 
let val total = (max_int_for_card int_card >= nat_card + 1) in


953 
Cst (cst, T,


954 
Func (Atom (nat_card, nat_j0),


955 
(not total ? Opt) (Atom (int_card, int_j0))))


956 
end


957 
else


958 
let val total = (max_int_for_card int_card < nat_card) in


959 
Cst (cst, T, Func (Atom (int_card, int_j0),


960 
Atom (nat_card, nat_j0)) > not total ? Opt)


961 
end


962 
end


963 
else


964 
Cst (cst, T, best_set_rep_for_type scope T)


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


966 
(case gsub def (flip_polarity polar) u1 of


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


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


969 
(s_op1 Not T (Formula Neg) u11)


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


971 
 Op1 (oper, T, _, u1) =>


972 
let


973 
val u1 = sub u1


974 
val R1 = rep_of u1


975 
val R = case oper of


976 
Finite => bool_rep polar (is_opt_rep R1)


977 
 _ => (if is_opt_rep R1 then best_opt_set_rep_for_type


978 
else best_non_opt_set_rep_for_type) scope T


979 
in s_op1 oper T R u1 end


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


981 
let


982 
val u1 = sub u1


983 
val u2 = sub u2


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


985 
in s_op2 Less T R u1 u2 end


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


987 
let


988 
val u1 = sub u1


989 
val u2 = sub u2


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


991 
val R = bool_rep polar opt


992 
in


993 
if is_opt_rep R then


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


995 
else if opt andalso polar = Pos andalso


996 
not (is_fully_comparable_type datatypes (type_of u1)) then


997 
Cst (False, T, Formula Pos)


998 
else


999 
s_op2 Subset T R u1 u2


1000 
end


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


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


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


1004 
let


1005 
val u1' = sub u1


1006 
val u2' = sub u2


1007 
(* unit > nut *)


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


1009 
(* unit > nut *)


1010 
fun opt_opt_case () =


1011 
if polar = Neut then


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


1013 
else


1014 
non_opt_case ()


1015 
(* nut > nut *)


1016 
fun hybrid_case u =


1017 
(* hackish optimization *)


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


1019 
else opt_opt_case ()


1020 
in


1021 
if liberal orelse polar = Neg


1022 
orelse is_fully_comparable_type datatypes (type_of u1) then


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


1024 
(true, true) => opt_opt_case ()


1025 
 (true, false) => hybrid_case u1'


1026 
 (false, true) => hybrid_case u2'


1027 
 (false, false) => non_opt_case ()


1028 
else


1029 
Cst (False, T, Formula Pos)


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


1031 
end


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


1033 
let


1034 
val u1' = sub u1


1035 
val u2' = sub u2


1036 
in


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


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


1039 
if R21 = R11 andalso is_lone_rep R12 then


1040 
let


1041 
val R =


1042 
best_non_opt_set_rep_for_type scope T


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


1044 
in s_op2 Image T R u1' u2' end


1045 
else


1046 
raise SAME ()


1047 
 _ => raise SAME ())


1048 
handle SAME () =>


1049 
let


1050 
val T1 = type_of u1


1051 
val dom_T = domain_type T1


1052 
val ran_T = range_type T1


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


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


1055 
in


1056 
Op2 (Lambda, T, Any, y_u,


1057 
Op2 (Exist, bool_T, Any, x_u,


1058 
Op2 (And, bool_T, Any,


1059 
case u2 of


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


1061 
if num_occs_in_nut u21 u22 = 0 then (* FIXME: move to s_op2 *)


1062 
u22


1063 
else


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


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


1066 
Op2 (Eq, bool_T, Any, y_u,


1067 
Op2 (Apply, ran_T, Any, u1, x_u)))))


1068 
> sub


1069 
end


1070 
end


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


1072 
let


1073 
val u1 = sub u1


1074 
val u2 = sub u2


1075 
val T1 = type_of u1


1076 
val R1 = rep_of u1


1077 
val R2 = rep_of u2


1078 
val opt =


1079 
case (u1, is_opt_rep R2) of


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


1081 
 _ => exists is_opt_rep [R1, R2]


1082 
val ran_R =


1083 
if is_boolean_type T then


1084 
bool_rep polar opt


1085 
else


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


1087 
(unopt_rep R1)


1088 
> opt ? opt_rep ofs T


1089 
in s_op2 Apply T ran_R u1 u2 end


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


1091 
(case best_set_rep_for_type scope T of


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


1093 
 R as Func (R1, _) =>


1094 
let


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


1096 
val u1' = aux table' false Neut u1


1097 
val u2' = aux table' false Neut u2


1098 
val R =


1099 
if is_opt_rep (rep_of u2')


1100 
orelse (range_type T = bool_T andalso


1101 
not (is_Cst False


1102 
(unrepify_nut_in_nut table false Neut


1103 
u1 u2


1104 
> optimize_nut))) then


1105 
opt_rep ofs T R


1106 
else


1107 
unopt_rep R


1108 
in s_op2 Lambda T R u1' u2' end


1109 
 R => raise NUT ("NitpickNut.aux.choose_reps_in_nut", [u]))


1110 
 Op2 (oper, T, _, u1, u2) =>


1111 
if oper mem [All, Exist] then


1112 
let


1113 
val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)


1114 
table


1115 
val u1' = aux table' def polar u1


1116 
val u2' = aux table' def polar u2


1117 
in


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


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


1120 
else


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


1122 
if def


1123 
orelse (liberal andalso (polar = Pos) = (oper = All))


1124 
orelse is_precise_type datatypes (type_of u1) then


1125 
quant_u


1126 
else


1127 
let


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


1129 
val unrepified_u = unrepify_nut_in_nut table def polar


1130 
u1 u2


1131 
in


1132 
s_op2 connective T


1133 
(min_rep (rep_of quant_u) (rep_of unrepified_u))


1134 
quant_u unrepified_u


1135 
end


1136 
end


1137 
end


1138 
else if oper mem [Or, And] then


1139 
let


1140 
val u1' = gsub def polar u1


1141 
val u2' = gsub def polar u2


1142 
in


1143 
(if polar = Neut then


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


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


1146 
 (true, false) =>


1147 
s_op2 oper T (Opt bool_atom_R)


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


1149 
 (false, true) =>


1150 
s_op2 oper T (Opt bool_atom_R)


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


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


1153 
else


1154 
raise SAME ())


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


1156 
end


1157 
else if oper mem [The, Eps] then


1158 
let


1159 
val u1' = sub u1


1160 
val opt1 = is_opt_rep (rep_of u1')


1161 
val unopt_R = best_one_rep_for_type scope T > optable_rep ofs T


1162 
val R = unopt_R > (oper = Eps orelse opt1) ? opt_rep ofs T


1163 
val u = Op2 (oper, T, R, u1', sub u2)


1164 
in


1165 
if is_precise_type datatypes T orelse not opt1 then


1166 
u


1167 
else


1168 
let


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


1170 
val R = R > opt_rep ofs T


1171 
in


1172 
Op3 (If, T, R,


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


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


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


1176 
end


1177 
end


1178 
else


1179 
let


1180 
val u1 = sub u1


1181 
val u2 = sub u2


1182 
val R =


1183 
best_non_opt_set_rep_for_type scope T


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


1185 
in s_op2 oper T R u1 u2 end


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


1187 
let


1188 
val u2 = sub u2


1189 
val R2 = rep_of u2


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


1191 
val u1 = modify_name_rep u1 R2


1192 
val u3 = aux table' false polar u3


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


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


1195 
let


1196 
val u1 = sub u1


1197 
val u2 = gsub def polar u2


1198 
val u3 = gsub def polar u3


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


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


1201 
in s_op3 If T R u1 u2 u3 end


1202 
 Tuple (T, _, us) =>


1203 
let


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


1205 
val us = map sub us


1206 
val R = if forall (equal Unit) Rs then Unit else Struct Rs


1207 
val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R


1208 
in s_tuple T R' us end


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


1210 
let


1211 
val us = map sub us


1212 
val Rs = map rep_of us


1213 
val R = best_one_rep_for_type scope T


1214 
val {total, ...} =


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


1216 
val opt = exists is_opt_rep Rs orelse not total


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


1218 
 _ =>


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


1220 
if polar = Neut orelse not (is_boolean_type (type_of u))


1221 
orelse not (is_opt_rep (rep_of u)) then


1222 
u


1223 
else


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


1225 
end


1226 
end


1227 
> optimize_unit


1228 
in aux table def Pos end


1229 


1230 
(* int > Kodkod.n_ary_index list > Kodkod.n_ary_index list


1231 
> int * Kodkod.n_ary_index list *)


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


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


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


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


1236 
(* int > name_pool > int * name_pool *)


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


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


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


1240 
rel_reg = rel_reg})


1241 
end


1242 
(* int > name_pool > int * name_pool *)


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


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


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


1246 
rel_reg = rel_reg})


1247 
end


1248 
(* int > name_pool > int * name_pool *)


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


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


1251 
rel_reg = rel_reg})


1252 
(* int > name_pool > int * name_pool *)


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


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


1255 
rel_reg = rel_reg + 1})


1256 


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


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


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


1260 
let


1261 
val is_formula = (rep_of v = Formula Neut)


1262 
val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg


1263 
val (j, pool) = fresh pool


1264 
val constr = if is_formula then FormulaReg else RelReg


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


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


1267 


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


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


1270 
let val arity1 = arity_of_rep R1 in


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


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


1273 
end


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


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


1276 
 shape_tuple T R [u] =


1277 
if type_of u = T then u else raise NUT ("NitpickNut.shape_tuple", [u])


1278 
 shape_tuple T Unit [] = Cst (Unity, T, Unit)


1279 
 shape_tuple _ _ us = raise NUT ("NitpickNut.shape_tuple", us)


1280 


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


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


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


1284 
let


1285 
val T = type_of v


1286 
val R = rep_of v


1287 
val arity = arity_of_rep R


1288 
val nick = nickname_of v


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


1290 
else (BoundRel, fresh_var)


1291 
in


1292 
if not rename_free andalso arity > 1 then


1293 
let


1294 
val atom_schema = atom_schema_of_rep R


1295 
val type_schema = type_schema_of_rep T R


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


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


1298 
(j :: js, pool)


1299 
end)


1300 
([], pool)


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


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


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


1304 
(rev js) atom_schema type_schema


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


1306 
else


1307 
let


1308 
val (j, pool) = fresh arity pool


1309 
val w = constr ((arity, j), T, R, nick)


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


1311 
end


1312 


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


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


1315 
fun rename_free_vars vs pool table =


1316 
let


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


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


1319 
in (rev vs, pool, table) end


1320 


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


1322 
fun rename_vars_in_nut pool table u =


1323 
case u of


1324 
Cst _ => u


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


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


1327 
if oper mem [All, Exist, Lambda] then


1328 
let


1329 
val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)


1330 
([], pool, table)


1331 
in


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


1333 
rename_vars_in_nut pool table u2)


1334 
end


1335 
else


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


1337 
rename_vars_in_nut pool table u2)


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


1339 
if rep_of u2 = Unit orelse inline_nut u2 then


1340 
let


1341 
val u2 = rename_vars_in_nut pool table u2


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


1343 
in rename_vars_in_nut pool table u3 end


1344 
else


1345 
let


1346 
val bs = untuple I u1


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


1348 
val u11 = rename_vars_in_nut pool table' u1


1349 
in


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


1351 
rename_vars_in_nut pool table u2,


1352 
rename_vars_in_nut pool table' u3)


1353 
end


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


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


1356 
rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3)


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


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


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


1360 
map (rename_vars_in_nut pool table) us)


1361 
 _ => the_name table u


1362 


1363 
end;
