1 (* Title: HOL/Tools/Nitpick/nitpick_nut.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 Nitpick underlying terms (nuts).
8 signature NITPICK_NUT =
10 type hol_context = Nitpick_HOL.hol_context
11 type scope = Nitpick_Scope.scope
12 type name_pool = Nitpick_Peephole.name_pool
13 type rep = Nitpick_Rep.rep
73 Cst of cst * typ * rep |
74 Op1 of op1 * typ * rep * nut |
75 Op2 of op2 * typ * rep * nut * nut |
76 Op3 of op3 * typ * rep * nut * nut * nut |
77 Tuple of typ * rep * nut list |
78 Construct of nut list * typ * rep * nut list |
79 BoundName of int * typ * rep * string |
80 FreeName of string * typ * rep |
81 ConstName of string * typ * rep |
82 BoundRel of Kodkod.n_ary_index * typ * rep * string |
83 FreeRel of Kodkod.n_ary_index * typ * rep * string |
84 RelReg of int * typ * rep |
85 FormulaReg of int * typ * rep
87 structure NameTable : TABLE
89 exception NUT of string * nut list
91 val string_for_nut : Proof.context -> nut -> string
92 val inline_nut : nut -> bool
93 val type_of : nut -> typ
94 val rep_of : nut -> rep
95 val nickname_of : nut -> string
96 val is_skolem_name : nut -> bool
97 val is_eval_name : nut -> bool
98 val is_Cst : cst -> nut -> bool
99 val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
100 val map_nut : (nut -> nut) -> nut -> nut
101 val untuple : (nut -> 'a) -> nut -> 'a list
102 val add_free_and_const_names :
103 nut -> nut list * nut list -> nut list * nut list
104 val name_ord : (nut * nut) -> order
105 val the_name : 'a NameTable.table -> nut -> 'a
106 val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
107 val nut_from_term : hol_context -> op2 -> term -> nut
108 val choose_reps_for_free_vars :
109 scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
110 val choose_reps_for_consts :
111 scope -> bool -> nut list -> rep NameTable.table
112 -> nut list * rep NameTable.table
113 val choose_reps_for_all_sels :
114 scope -> rep NameTable.table -> nut list * rep NameTable.table
115 val choose_reps_in_nut :
116 scope -> bool -> rep NameTable.table -> bool -> nut -> nut
117 val rename_free_vars :
118 nut list -> name_pool -> nut NameTable.table
119 -> nut list * name_pool * nut NameTable.table
120 val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut
123 structure Nitpick_Nut : NITPICK_NUT =
129 open Nitpick_Peephole
132 structure KK = Kodkod
192 Cst of cst * typ * rep |
193 Op1 of op1 * typ * rep * nut |
194 Op2 of op2 * typ * rep * nut * nut |
195 Op3 of op3 * typ * rep * nut * nut * nut |
196 Tuple of typ * rep * nut list |
197 Construct of nut list * typ * rep * nut list |
198 BoundName of int * typ * rep * string |
199 FreeName of string * typ * rep |
200 ConstName of string * typ * rep |
201 BoundRel of KK.n_ary_index * typ * rep * string |
202 FreeRel of KK.n_ary_index * typ * rep * string |
203 RelReg of int * typ * rep |
204 FormulaReg of int * typ * rep
206 exception NUT of string * nut list
209 fun string_for_cst Unity = "Unity"
210 | string_for_cst False = "False"
211 | string_for_cst True = "True"
212 | string_for_cst Iden = "Iden"
213 | string_for_cst (Num j) = "Num " ^ signed_string_of_int j
214 | string_for_cst Unknown = "Unknown"
215 | string_for_cst Unrep = "Unrep"
216 | string_for_cst Suc = "Suc"
217 | string_for_cst Add = "Add"
218 | string_for_cst Subtract = "Subtract"
219 | string_for_cst Multiply = "Multiply"
220 | string_for_cst Divide = "Divide"
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"
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 IsUnknown = "IsUnknown"
235 | string_for_op1 Tha = "Tha"
236 | string_for_op1 First = "First"
237 | string_for_op1 Second = "Second"
238 | string_for_op1 Cast = "Cast"
241 fun string_for_op2 All = "All"
242 | string_for_op2 Exist = "Exist"
243 | string_for_op2 Or = "Or"
244 | string_for_op2 And = "And"
245 | string_for_op2 Less = "Less"
246 | string_for_op2 Subset = "Subset"
247 | string_for_op2 DefEq = "DefEq"
248 | string_for_op2 Eq = "Eq"
249 | string_for_op2 The = "The"
250 | string_for_op2 Eps = "Eps"
251 | string_for_op2 Triad = "Triad"
252 | string_for_op2 Union = "Union"
253 | string_for_op2 SetDifference = "SetDifference"
254 | string_for_op2 Intersect = "Intersect"
255 | string_for_op2 Composition = "Composition"
256 | string_for_op2 Product = "Product"
257 | string_for_op2 Image = "Image"
258 | string_for_op2 Apply = "Apply"
259 | string_for_op2 Lambda = "Lambda"
262 fun string_for_op3 Let = "Let"
263 | string_for_op3 If = "If"
265 (* int -> Proof.context -> nut -> string *)
266 fun basic_string_for_nut indent ctxt u =
269 val sub = basic_string_for_nut (indent + 1) ctxt
271 (if indent = 0 then "" else "\n" ^ implode (replicate (2 * indent) " ")) ^
275 "Cst " ^ string_for_cst c ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
277 | Op1 (oper, T, R, u1) =>
278 "Op1 " ^ string_for_op1 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
279 string_for_rep R ^ " " ^ sub u1
280 | Op2 (oper, T, R, u1, u2) =>
281 "Op2 " ^ string_for_op2 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
282 string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2
283 | Op3 (oper, T, R, u1, u2, u3) =>
284 "Op3 " ^ string_for_op3 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
285 string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 ^ " " ^ sub u3
286 | Tuple (T, R, us) =>
287 "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
289 | Construct (us', T, R, us) =>
290 "Construct " ^ implode (map sub us') ^ " " ^
291 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
293 | BoundName (j, T, R, nick) =>
294 "BoundName " ^ signed_string_of_int j ^ " " ^
295 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
296 | FreeName (s, T, R) =>
297 "FreeName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
299 | ConstName (s, T, R) =>
300 "ConstName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
302 | BoundRel ((n, j), T, R, nick) =>
303 "BoundRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
304 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
305 | FreeRel ((n, j), T, R, nick) =>
306 "FreeRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
307 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
308 | RelReg (j, T, R) =>
309 "RelReg " ^ signed_string_of_int j ^ " " ^ Syntax.string_of_typ ctxt T ^
310 " " ^ string_for_rep R
311 | FormulaReg (j, T, R) =>
312 "FormulaReg " ^ signed_string_of_int j ^ " " ^
313 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R) ^
316 (* Proof.context -> nut -> string *)
317 val string_for_nut = basic_string_for_nut 0
320 fun inline_nut (Op1 _) = false
321 | inline_nut (Op2 _) = false
322 | inline_nut (Op3 _) = false
323 | inline_nut (Tuple (_, _, us)) = forall inline_nut us
324 | inline_nut _ = true
327 fun type_of (Cst (_, T, _)) = T
328 | type_of (Op1 (_, T, _, _)) = T
329 | type_of (Op2 (_, T, _, _, _)) = T
330 | type_of (Op3 (_, T, _, _, _, _)) = T
331 | type_of (Tuple (T, _, _)) = T
332 | type_of (Construct (_, T, _, _)) = T
333 | type_of (BoundName (_, T, _, _)) = T
334 | type_of (FreeName (_, T, _)) = T
335 | type_of (ConstName (_, T, _)) = T
336 | type_of (BoundRel (_, T, _, _)) = T
337 | type_of (FreeRel (_, T, _, _)) = T
338 | type_of (RelReg (_, T, _)) = T
339 | type_of (FormulaReg (_, T, _)) = T
342 fun rep_of (Cst (_, _, R)) = R
343 | rep_of (Op1 (_, _, R, _)) = R
344 | rep_of (Op2 (_, _, R, _, _)) = R
345 | rep_of (Op3 (_, _, R, _, _, _)) = R
346 | rep_of (Tuple (_, R, _)) = R
347 | rep_of (Construct (_, _, R, _)) = R
348 | rep_of (BoundName (_, _, R, _)) = R
349 | rep_of (FreeName (_, _, R)) = R
350 | rep_of (ConstName (_, _, R)) = R
351 | rep_of (BoundRel (_, _, R, _)) = R
352 | rep_of (FreeRel (_, _, R, _)) = R
353 | rep_of (RelReg (_, _, R)) = R
354 | rep_of (FormulaReg (_, _, R)) = R
357 fun nickname_of (BoundName (_, _, _, nick)) = nick
358 | nickname_of (FreeName (s, _, _)) = s
359 | nickname_of (ConstName (s, _, _)) = s
360 | nickname_of (BoundRel (_, _, _, nick)) = nick
361 | nickname_of (FreeRel (_, _, _, nick)) = nick
362 | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
365 fun is_skolem_name u =
366 space_explode name_sep (nickname_of u)
367 |> exists (String.isPrefix skolem_prefix)
368 handle NUT ("Nitpick_Nut.nickname_of", _) => false
370 String.isPrefix eval_prefix (nickname_of u)
371 handle NUT ("Nitpick_Nut.nickname_of", _) => false
372 (* cst -> nut -> bool *)
373 fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
376 (* (nut -> 'a -> 'a) -> nut -> 'a -> 'a *)
379 Op1 (_, _, _, u1) => fold_nut f u1
380 | Op2 (_, _, _, u1, u2) => fold_nut f u1 #> fold_nut f u2
381 | Op3 (_, _, _, u1, u2, u3) => fold_nut f u1 #> fold_nut f u2 #> fold_nut f u3
382 | Tuple (_, _, us) => fold (fold_nut f) us
383 | Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
385 (* (nut -> nut) -> nut -> nut *)
388 Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
389 | Op2 (oper, T, R, u1, u2) => Op2 (oper, T, R, map_nut f u1, map_nut f u2)
390 | Op3 (oper, T, R, u1, u2, u3) =>
391 Op3 (oper, T, R, map_nut f u1, map_nut f u2, map_nut f u3)
392 | Tuple (T, R, us) => Tuple (T, R, map (map_nut f) us)
393 | Construct (us', T, R, us) =>
394 Construct (map (map_nut f) us', T, R, map (map_nut f) us)
397 (* nut * nut -> order *)
398 fun name_ord (BoundName (j1, _, _, _), BoundName (j2, _, _, _)) =
400 | name_ord (BoundName _, _) = LESS
401 | name_ord (_, BoundName _) = GREATER
402 | name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) =
403 (case fast_string_ord (s1, s2) of
404 EQUAL => Term_Ord.typ_ord (T1, T2)
406 | name_ord (FreeName _, _) = LESS
407 | name_ord (_, FreeName _) = GREATER
408 | name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) =
409 (case fast_string_ord (s1, s2) of
410 EQUAL => Term_Ord.typ_ord (T1, T2)
412 | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
414 (* nut -> nut -> int *)
415 fun num_occs_in_nut needle_u stack_u =
416 fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0
417 (* nut -> nut -> bool *)
418 val is_subterm_of = not_equal 0 oo num_occs_in_nut
420 (* nut -> nut -> nut -> nut *)
421 fun substitute_in_nut needle_u needle_u' =
422 map_nut (fn u => if u = needle_u then needle_u' else u)
424 (* nut -> nut list * nut list -> nut list * nut list *)
425 val add_free_and_const_names =
426 fold_nut (fn u => case u of
427 FreeName _ => apfst (insert (op =) u)
428 | ConstName _ => apsnd (insert (op =) u)
431 (* nut -> rep -> nut *)
432 fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
433 | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
434 | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
435 | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u])
437 structure NameTable = Table(type key = nut val ord = name_ord)
439 (* 'a NameTable.table -> nut -> 'a *)
440 fun the_name table name =
441 case NameTable.lookup table name of
443 | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
444 (* nut NameTable.table -> nut -> KK.n_ary_index *)
445 fun the_rel table name =
446 case the_name table name of
447 FreeRel (x, _, _, _) => x
448 | u => raise NUT ("Nitpick_Nut.the_rel", [u])
450 (* typ * term -> typ * term *)
451 fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
453 let val res_T = fst (HOLogic.dest_prodT T) in
454 (res_T, Const (@{const_name fst}, T --> res_T) $ t)
456 fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) =
457 (domain_type (range_type T), t2)
459 let val res_T = snd (HOLogic.dest_prodT T) in
460 (res_T, Const (@{const_name snd}, T --> res_T) $ t)
462 (* typ * term -> (typ * term) list *)
463 fun factorize (z as (Type (@{type_name "*"}, _), _)) =
464 maps factorize [mk_fst z, mk_snd z]
467 (* hol_context -> op2 -> term -> nut *)
468 fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
470 (* string list -> typ list -> term -> nut *)
474 val sub = aux Eq ss Ts
475 val sub' = aux eq ss Ts
476 (* string -> typ -> term -> nut *)
477 fun sub_abs s T = aux eq (s :: ss) (T :: Ts)
478 (* typ -> term -> term -> nut *)
479 fun sub_equals T t1 t2 =
481 val (binder_Ts, body_T) = strip_type (domain_type T)
482 val n = length binder_Ts
484 if eq = Eq andalso n > 0 then
486 val t1 = incr_boundvars n t1
487 val t2 = incr_boundvars n t2
488 val xs = map Bound (n - 1 downto 0)
489 val equation = Const (@{const_name "op ="},
490 body_T --> body_T --> bool_T)
491 $ betapplys (t1, xs) $ betapplys (t2, xs)
493 fold_rev (fn T => fn (t, j) =>
494 (Const (@{const_name All}, T --> bool_T)
495 $ Abs ("x" ^ nat_subscript j, T, t), j - 1))
496 binder_Ts (equation, n) |> fst
499 Op2 (eq, bool_T, Any, aux Eq ss Ts t1, aux Eq ss Ts t2)
501 (* op2 -> string -> typ -> term -> nut *)
502 fun do_quantifier quant s T t1 =
504 val bound_u = BoundName (length Ts, T, Any, s)
505 val body_u = sub_abs s T t1
507 if is_subterm_of bound_u body_u then
508 Op2 (quant, bool_T, Any, bound_u, body_u)
512 (* term -> term list -> nut *)
515 val (ts', t2) = split_last ts
516 val t1 = list_comb (t0, ts')
517 val T1 = fastype_of1 (Ts, t1)
518 in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
519 (* styp -> term list -> term *)
520 fun construct (x as (_, T)) ts =
521 case num_binder_types T - length ts of
522 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
523 o nth_sel_for_constr x)
524 (~1 upto num_sels_for_constr_type T - 1),
526 ts |> map (`(curry fastype_of1 Ts))
527 |> maps factorize |> map (sub o snd))
528 | k => sub (eta_expand Ts t k)
531 (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
532 do_quantifier All s T t1
533 | (t0 as Const (@{const_name all}, _), [t1]) =>
534 sub' (t0 $ eta_expand Ts t1 1)
535 | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
536 | (Const (@{const_name "==>"}, _), [t1, t2]) =>
537 Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
538 | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
539 Op2 (And, prop_T, Any, sub' t1, sub' t2)
540 | (Const (@{const_name Trueprop}, _), [t1]) => sub' t1
541 | (Const (@{const_name Not}, _), [t1]) =>
543 Op1 (Not, _, _, u11) => u11
544 | u1 => Op1 (Not, bool_T, Any, u1))
545 | (Const (@{const_name False}, T), []) => Cst (False, T, Any)
546 | (Const (@{const_name True}, T), []) => Cst (True, T, Any)
547 | (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
548 do_quantifier All s T t1
549 | (t0 as Const (@{const_name All}, _), [t1]) =>
550 sub' (t0 $ eta_expand Ts t1 1)
551 | (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
552 do_quantifier Exist s T t1
553 | (t0 as Const (@{const_name Ex}, _), [t1]) =>
554 sub' (t0 $ eta_expand Ts t1 1)
555 | (t0 as Const (@{const_name The}, T), [t1]) =>
557 Op2 (The, range_type T, Any, sub t1,
558 sub (Const (@{const_name undefined_fast_The}, range_type T)))
561 | (t0 as Const (@{const_name Eps}, T), [t1]) =>
563 Op2 (Eps, range_type T, Any, sub t1,
564 sub (Const (@{const_name undefined_fast_Eps}, range_type T)))
567 | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
568 | (Const (@{const_name "op &"}, _), [t1, t2]) =>
569 Op2 (And, bool_T, Any, sub' t1, sub' t2)
570 | (Const (@{const_name "op |"}, _), [t1, t2]) =>
571 Op2 (Or, bool_T, Any, sub t1, sub t2)
572 | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
573 Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
574 | (Const (@{const_name If}, T), [t1, t2, t3]) =>
575 Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
576 | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
577 Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
578 sub t1, sub_abs s T' t2)
579 | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
580 sub (t0 $ t1 $ eta_expand Ts t2 1)
581 | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
582 | (Const (@{const_name Pair}, T), [t1, t2]) =>
583 Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
584 | (Const (@{const_name fst}, T), [t1]) =>
585 Op1 (First, range_type T, Any, sub t1)
586 | (Const (@{const_name snd}, T), [t1]) =>
587 Op1 (Second, range_type T, Any, sub t1)
588 | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
589 | (Const (@{const_name insert}, T), [t1, t2]) =>
591 Abs (_, _, @{const False}) =>
592 Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1)
594 Op2 (Union, nth_range_type 2 T, Any,
595 Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1), sub t2))
596 | (Const (@{const_name converse}, T), [t1]) =>
597 Op1 (Converse, range_type T, Any, sub t1)
598 | (Const (@{const_name trancl}, T), [t1]) =>
599 Op1 (Closure, range_type T, Any, sub t1)
600 | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
601 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
602 | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
603 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
604 | (Const (@{const_name image}, T), [t1, t2]) =>
605 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
606 | (Const (x as (s as @{const_name Suc}, T)), []) =>
607 if is_built_in_const thy stds false x then Cst (Suc, T, Any)
608 else if is_constr thy stds x then construct x []
609 else ConstName (s, T, Any)
610 | (Const (@{const_name finite}, T), [t1]) =>
611 (if is_finite_type hol_ctxt (domain_type T) then
612 Cst (True, bool_T, Any)
614 Const (@{const_name top}, _) => Cst (False, bool_T, Any)
615 | _ => Op1 (Finite, bool_T, Any, sub t1))
616 | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
617 | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
618 if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
619 else if is_constr thy stds x then construct x []
620 else ConstName (s, T, Any)
621 | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
622 if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
623 else ConstName (s, T, Any)
624 | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
625 if is_built_in_const thy stds false x then Cst (Add, T, Any)
626 else ConstName (s, T, Any)
627 | (Const (@{const_name minus_class.minus},
628 Type (@{type_name fun},
629 [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
631 Op2 (SetDifference, T1, Any, sub t1, sub t2)
632 | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
633 if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
634 else ConstName (s, T, Any)
635 | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
636 if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
637 else ConstName (s, T, Any)
638 | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
639 if is_built_in_const thy stds false x then Cst (Divide, T, Any)
640 else ConstName (s, T, Any)
641 | (t0 as Const (x as (@{const_name ord_class.less}, _)),
643 if is_built_in_const thy stds false x then
644 Op2 (Less, bool_T, Any, sub t1, sub t2)
647 | (Const (@{const_name ord_class.less_eq},
648 Type (@{type_name fun},
649 [Type (@{type_name fun}, [_, @{typ bool}]), _])),
651 Op2 (Subset, bool_T, Any, sub t1, sub t2)
652 (* FIXME: find out if this case is necessary *)
653 | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
655 if is_built_in_const thy stds false x then
656 Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
659 | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
660 | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
661 | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
662 if is_built_in_const thy stds false x then
663 let val num_T = domain_type T in
664 Op2 (Apply, num_T --> num_T, Any,
665 Cst (Subtract, num_T --> num_T --> num_T, Any),
666 Cst (Num 0, num_T, Any))
669 ConstName (s, T, Any)
670 | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
671 | (Const (@{const_name is_unknown}, _), [t1]) =>
672 Op1 (IsUnknown, bool_T, Any, sub t1)
673 | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
674 Op1 (Tha, T2, Any, sub t1)
675 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
676 | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
677 | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
678 Cst (NatToInt, T, Any)
679 | (Const (@{const_name of_nat},
680 T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
681 Cst (NatToInt, T, Any)
682 | (Const (@{const_name semilattice_inf_class.inf},
683 Type (@{type_name fun},
684 [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
686 Op2 (Intersect, T1, Any, sub t1, sub t2)
687 | (Const (@{const_name semilattice_sup_class.sup},
688 Type (@{type_name fun},
689 [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
691 Op2 (Union, T1, Any, sub t1, sub t2)
692 | (t0 as Const (x as (s, T)), ts) =>
693 if is_constr thy stds x then
695 else if String.isPrefix numeral_prefix s then
696 Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
698 (case arity_of_built_in_const thy stds fast_descrs x of
700 (case n - length ts of
701 0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
702 | k => if k > 0 then sub (eta_expand Ts t k)
704 | NONE => if null ts then ConstName (s, T, Any)
706 | (Free (s, T), []) => FreeName (s, T, Any)
707 | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
709 BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
710 | (Abs (s, T, t1), []) =>
711 Op2 (Lambda, T --> fastype_of1 (T :: Ts, t1), Any,
712 BoundName (length Ts, T, Any, s), sub_abs s T t1)
713 | (t0, ts) => do_apply t0 ts
717 (* scope -> typ -> rep *)
718 fun rep_for_abs_fun scope T =
719 let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
720 Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
723 (* scope -> nut -> nut list * rep NameTable.table
724 -> nut list * rep NameTable.table *)
725 fun choose_rep_for_free_var scope v (vs, table) =
727 val R = best_non_opt_set_rep_for_type scope (type_of v)
728 val v = modify_name_rep v R
729 in (v :: vs, NameTable.update (v, R) table) end
730 (* scope -> bool -> nut -> nut list * rep NameTable.table
731 -> nut list * rep NameTable.table *)
732 fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
735 val x as (s, T) = (nickname_of v, type_of v)
736 val R = (if is_abs_fun thy x then
738 else if is_rep_fun thy x then
739 Func oo best_non_opt_symmetric_reps_for_fun_type
740 else if all_exact orelse is_skolem_name v orelse
741 member (op =) [@{const_name undefined_fast_The},
742 @{const_name undefined_fast_Eps},
744 @{const_name bisim_iterator_max}]
745 (original_name s) then
746 best_non_opt_set_rep_for_type
747 else if member (op =) [@{const_name set}, @{const_name distinct},
748 @{const_name ord_class.less},
749 @{const_name ord_class.less_eq}]
750 (original_name s) then
751 best_set_rep_for_type
753 best_opt_set_rep_for_type) scope T
754 val v = modify_name_rep v R
755 in (v :: vs, NameTable.update (v, R) table) end
757 (* scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
758 fun choose_reps_for_free_vars scope vs table =
759 fold (choose_rep_for_free_var scope) vs ([], table)
760 (* scope -> bool -> nut list -> rep NameTable.table
761 -> nut list * rep NameTable.table *)
762 fun choose_reps_for_consts scope all_exact vs table =
763 fold (choose_rep_for_const scope all_exact) vs ([], table)
765 (* scope -> styp -> int -> nut list * rep NameTable.table
766 -> nut list * rep NameTable.table *)
767 fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
768 (x as (_, T)) n (vs, table) =
770 val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
771 val R' = if n = ~1 orelse is_word_type (body_type T) orelse
772 (is_fun_type (range_type T') andalso
773 is_boolean_type (body_type T')) then
774 best_non_opt_set_rep_for_type scope T'
776 best_opt_set_rep_for_type scope T' |> unopt_rep
777 val v = ConstName (s', T', R')
778 in (v :: vs, NameTable.update (v, R') table) end
779 (* scope -> styp -> nut list * rep NameTable.table
780 -> nut list * rep NameTable.table *)
781 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
782 fold_rev (choose_rep_for_nth_sel_for_constr scope x)
783 (~1 upto num_sels_for_constr_type T - 1)
784 (* scope -> dtype_spec -> nut list * rep NameTable.table
785 -> nut list * rep NameTable.table *)
786 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
787 | choose_rep_for_sels_of_datatype scope {constrs, ...} =
788 fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
789 (* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
790 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
791 fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
793 (* scope -> nut -> rep NameTable.table -> rep NameTable.table *)
794 fun choose_rep_for_bound_var scope v table =
795 let val R = best_one_rep_for_type scope (type_of v) in
796 NameTable.update (v, R) table
799 (* A nut is said to be constructive if whenever it evaluates to unknown in our
800 three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
801 according to the HOL semantics. For example, "Suc n" is constructive if "n"
802 is representable or "Unrep", because unknown implies "Unrep". *)
804 fun is_constructive u =
805 is_Cst Unrep u orelse
806 (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
808 Cst (Num _, _, _) => true
810 cst = Suc orelse (body_type T = nat_T andalso cst = Add)
811 | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
812 | Op3 (If, _, _, u1, u2, u3) =>
813 not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
814 | Tuple (_, _, us) => forall is_constructive us
815 | Construct (_, _, _, us) => forall is_constructive us
819 fun optimize_unit u =
820 if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
821 (* typ -> rep -> nut *)
822 fun unknown_boolean T R =
823 Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
826 fun is_fully_representable_set u =
827 not (is_opt_rep (rep_of u)) andalso
830 | Op1 (SingletonSet, _, _, _) => true
831 | Op2 (oper, _, _, u1, u2) =>
832 member (op =) [Union, SetDifference, Intersect] oper andalso
833 forall is_fully_representable_set [u1, u2]
836 (* op1 -> typ -> rep -> nut -> nut *)
837 fun s_op1 oper T R u1 =
839 if is_Cst True u1 then Cst (False, T, R)
840 else if is_Cst False u1 then Cst (True, T, R)
844 handle SAME () => Op1 (oper, T, R, u1))
846 (* op2 -> typ -> rep -> nut -> nut -> nut *)
847 fun s_op2 oper T R u1 u2 =
850 if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R)
851 else if is_Cst False u1 then u2
852 else if is_Cst False u2 then u1
855 if exists (is_Cst False) [u1, u2] then Cst (False, T, unopt_rep R)
856 else if is_Cst True u1 then u2
857 else if is_Cst True u2 then u1
860 (case pairself (is_Cst Unrep) (u1, u2) of
861 (true, true) => unknown_boolean T R
862 | (false, false) => raise SAME ()
863 | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()
864 else Cst (False, T, Formula Neut))
866 if is_Cst True u1 then u1
867 else if is_Cst False u2 then u2
870 if is_Cst Unrep u1 then
872 else if is_Cst Unrep u2 then
873 if is_constructive u1 then
875 else if is_boolean_type T then
876 if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
877 else unknown_boolean T R
879 Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
884 | _ => raise SAME ())
885 handle SAME () => Op2 (oper, T, R, u1, u2))
887 (* op3 -> typ -> rep -> nut -> nut -> nut -> nut *)
888 fun s_op3 oper T R u1 u2 u3 =
891 if inline_nut u2 orelse num_occs_in_nut u1 u3 < 2 then
892 substitute_in_nut u1 u2 u3
895 | _ => raise SAME ())
896 handle SAME () => Op3 (oper, T, R, u1, u2, u3))
898 (* typ -> rep -> nut list -> nut *)
900 (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us))
903 (* theory -> nut -> nut *)
906 Op1 (oper, T, R, u1) => s_op1 oper T R (optimize_nut u1)
907 | Op2 (oper, T, R, u1, u2) =>
908 s_op2 oper T R (optimize_nut u1) (optimize_nut u2)
909 | Op3 (oper, T, R, u1, u2, u3) =>
910 s_op3 oper T R (optimize_nut u1) (optimize_nut u2) (optimize_nut u3)
911 | Tuple (T, R, us) => s_tuple T R (map optimize_nut us)
912 | Construct (us', T, R, us) => Construct (us', T, R, map optimize_nut us)
913 | _ => optimize_unit u
915 (* (nut -> 'a) -> nut -> 'a list *)
916 fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
917 | untuple f u = if rep_of u = Unit then [] else [f u]
919 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
920 fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
923 val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
924 (* polarity -> bool -> rep *)
925 fun bool_rep polar opt =
926 if polar = Neut andalso opt then Opt bool_atom_R else Formula polar
927 (* nut -> nut -> nut *)
928 fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2
929 (* (polarity -> nut) -> nut *)
930 fun triad_fn f = triad (f Pos) (f Neg)
931 (* rep NameTable.table -> bool -> polarity -> nut -> nut -> nut *)
932 fun unrepify_nut_in_nut table def polar needle_u =
933 let val needle_T = type_of needle_u in
934 substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown
935 else Unrep, needle_T, Any))
936 #> aux table def polar
938 (* rep NameTable.table -> bool -> polarity -> nut -> nut *)
939 and aux table def polar u =
941 (* bool -> polarity -> nut -> nut *)
944 val sub = gsub false Neut
947 Cst (False, T, _) => Cst (False, T, Formula Neut)
948 | Cst (True, T, _) => Cst (True, T, Formula Neut)
949 | Cst (Num j, T, _) =>
950 if is_word_type T then
951 Cst (if is_twos_complement_representable bits j then Num j
952 else Unrep, T, best_opt_set_rep_for_type scope T)
954 (case spec_of_type scope T of
955 (1, j0) => if j = 0 then Cst (Unity, T, Unit)
956 else Cst (Unrep, T, Opt (Atom (1, j0)))
959 val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
962 if ok then Cst (Num j, T, Atom (k, j0))
963 else Cst (Unrep, T, Opt (Atom (k, j0)))
965 | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
966 let val R = Atom (spec_of_type scope T1) in
967 Cst (Suc, T, Func (R, Opt R))
969 | Cst (Fracs, T, _) =>
970 Cst (Fracs, T, best_non_opt_set_rep_for_type scope T)
971 | Cst (NormFrac, T, _) =>
972 let val R1 = Atom (spec_of_type scope (domain_type T)) in
973 Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
976 if cst = Unknown orelse cst = Unrep then
977 case (is_boolean_type T, polar) of
978 (true, Pos) => Cst (False, T, Formula Pos)
979 | (true, Neg) => Cst (True, T, Formula Neg)
980 | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
981 else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
984 val T1 = domain_type T
985 val R1 = Atom (spec_of_type scope T1)
986 val total = T1 = nat_T andalso
987 (cst = Subtract orelse cst = Divide orelse cst = Gcd)
988 in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
989 else if cst = NatToInt orelse cst = IntToNat then
991 val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
992 val (ran_card, ran_j0) = spec_of_type scope (range_type T)
993 val total = not (is_word_type (domain_type T)) andalso
994 (if cst = NatToInt then
995 max_int_for_card ran_card >= dom_card + 1
997 max_int_for_card dom_card < ran_card)
999 Cst (cst, T, Func (Atom (dom_card, dom_j0),
1000 Atom (ran_card, ran_j0) |> not total ? Opt))
1003 Cst (cst, T, best_set_rep_for_type scope T)
1004 | Op1 (Not, T, _, u1) =>
1005 (case gsub def (flip_polarity polar) u1 of
1006 Op2 (Triad, T, _, u11, u12) =>
1007 triad (s_op1 Not T (Formula Pos) u12)
1008 (s_op1 Not T (Formula Neg) u11)
1009 | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
1010 | Op1 (IsUnknown, T, _, u1) =>
1011 let val u1 = sub u1 in
1012 if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
1013 else Cst (False, T, Formula Neut)
1015 | Op1 (oper, T, _, u1) =>
1019 val R = case oper of
1020 Finite => bool_rep polar (is_opt_rep R1)
1021 | _ => (if is_opt_rep R1 then best_opt_set_rep_for_type
1022 else best_non_opt_set_rep_for_type) scope T
1023 in s_op1 oper T R u1 end
1024 | Op2 (Less, T, _, u1, u2) =>
1028 val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
1029 in s_op2 Less T R u1 u2 end
1030 | Op2 (Subset, T, _, u1, u2) =>
1034 val opt = exists (is_opt_rep o rep_of) [u1, u2]
1035 val R = bool_rep polar opt
1037 if is_opt_rep R then
1038 triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
1039 else if opt andalso polar = Pos andalso
1040 not (is_concrete_type datatypes true (type_of u1)) then
1041 Cst (False, T, Formula Pos)
1043 s_op2 Subset T R u1 u2
1045 | Op2 (DefEq, T, _, u1, u2) =>
1046 s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
1047 | Op2 (Eq, T, _, u1, u2) =>
1052 fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2'
1054 fun opt_opt_case () =
1055 if polar = Neut then
1056 triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2')
1061 (* hackish optimization *)
1062 if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
1063 else opt_opt_case ()
1065 if unsound orelse polar = Neg orelse
1066 is_concrete_type datatypes true (type_of u1) then
1067 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
1068 (true, true) => opt_opt_case ()
1069 | (true, false) => hybrid_case u1'
1070 | (false, true) => hybrid_case u2'
1071 | (false, false) => non_opt_case ()
1073 Cst (False, T, Formula Pos)
1074 |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
1076 | Op2 (Image, T, _, u1, u2) =>
1081 (case (rep_of u1', rep_of u2') of
1082 (Func (R11, R12), Func (R21, Formula Neut)) =>
1083 if R21 = R11 andalso is_lone_rep R12 then
1086 best_non_opt_set_rep_for_type scope T
1087 |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
1088 in s_op2 Image T R u1' u2' end
1091 | _ => raise SAME ())
1095 val dom_T = domain_type T1
1096 val ran_T = range_type T1
1097 val x_u = BoundName (~1, dom_T, Any, "image.x")
1098 val y_u = BoundName (~2, ran_T, Any, "image.y")
1100 Op2 (Lambda, T, Any, y_u,
1101 Op2 (Exist, bool_T, Any, x_u,
1102 Op2 (And, bool_T, Any,
1104 Op2 (Lambda, _, _, u21, u22) =>
1105 if num_occs_in_nut u21 u22 = 0 then
1108 Op2 (Apply, bool_T, Any, u2, x_u)
1109 | _ => Op2 (Apply, bool_T, Any, u2, x_u),
1111 Op2 (Eq, bool_T, Any, y_u,
1112 Op2 (Apply, ran_T, Any, u1, x_u)))))
1116 | Op2 (Apply, T, _, u1, u2) =>
1124 case (u1, is_opt_rep R2) of
1125 (ConstName (@{const_name set}, _, _), false) => false
1126 | _ => exists is_opt_rep [R1, R2]
1128 if is_boolean_type T then
1131 smart_range_rep ofs T1 (fn () => card_of_type card_assigns T)
1133 |> opt ? opt_rep ofs T
1134 in s_op2 Apply T ran_R u1 u2 end
1135 | Op2 (Lambda, T, _, u1, u2) =>
1136 (case best_set_rep_for_type scope T of
1137 Unit => Cst (Unity, T, Unit)
1138 | R as Func (R1, _) =>
1140 val table' = NameTable.update (u1, R1) table
1141 val u1' = aux table' false Neut u1
1142 val u2' = aux table' false Neut u2
1144 if is_opt_rep (rep_of u2') orelse
1145 (range_type T = bool_T andalso
1146 not (is_Cst False (unrepify_nut_in_nut table false Neut
1148 |> optimize_nut))) then
1152 in s_op2 Lambda T R u1' u2' end
1153 | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
1154 | Op2 (oper, T, _, u1, u2) =>
1155 if oper = All orelse oper = Exist then
1157 val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
1159 val u1' = aux table' def polar u1
1160 val u2' = aux table' def polar u2
1162 if polar = Neut andalso is_opt_rep (rep_of u2') then
1163 triad_fn (fn polar => gsub def polar u)
1165 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
1167 (unsound andalso (polar = Pos) = (oper = All)) orelse
1168 is_complete_type datatypes true (type_of u1) then
1172 val connective = if oper = All then And else Or
1173 val unrepified_u = unrepify_nut_in_nut table def polar
1177 (min_rep (rep_of quant_u) (rep_of unrepified_u))
1178 quant_u unrepified_u
1182 else if oper = Or orelse oper = And then
1184 val u1' = gsub def polar u1
1185 val u2' = gsub def polar u2
1187 (if polar = Neut then
1188 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
1189 (true, true) => triad_fn (fn polar => gsub def polar u)
1191 s_op2 oper T (Opt bool_atom_R)
1192 (triad_fn (fn polar => gsub def polar u1)) u2'
1194 s_op2 oper T (Opt bool_atom_R)
1195 u1' (triad_fn (fn polar => gsub def polar u2))
1196 | (false, false) => raise SAME ()
1199 handle SAME () => s_op2 oper T (Formula polar) u1' u2'
1201 else if oper = The orelse oper = Eps then
1204 val opt1 = is_opt_rep (rep_of u1')
1205 val opt = (oper = Eps orelse opt1)
1206 val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
1207 val R = if is_boolean_type T then bool_rep polar opt
1208 else unopt_R |> opt ? opt_rep ofs T
1209 val u = Op2 (oper, T, R, u1', sub u2)
1211 if is_complete_type datatypes true T orelse not opt1 then
1215 val x_u = BoundName (~1, T, unopt_R, "descr.x")
1216 val R = R |> opt_rep ofs T
1219 Op2 (Exist, bool_T, Formula Pos, x_u,
1220 s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1)
1221 x_u), u, Cst (Unknown, T, R))
1229 best_non_opt_set_rep_for_type scope T
1230 |> exists (is_opt_rep o rep_of) [u1, u2] ? opt_rep ofs T
1231 in s_op2 oper T R u1 u2 end
1232 | Op3 (Let, T, _, u1, u2, u3) =>
1236 val table' = NameTable.update (u1, R2) table
1237 val u1 = modify_name_rep u1 R2
1238 val u3 = aux table' false polar u3
1239 in s_op3 Let T (rep_of u3) u1 u2 u3 end
1240 | Op3 (If, T, _, u1, u2, u3) =>
1243 val u2 = gsub def polar u2
1244 val u3 = gsub def polar u3
1245 val min_R = min_rep (rep_of u2) (rep_of u3)
1246 val R = min_R |> is_opt_rep (rep_of u1) ? opt_rep ofs T
1247 in s_op3 If T R u1 u2 u3 end
1248 | Tuple (T, _, us) =>
1250 val Rs = map (best_one_rep_for_type scope o type_of) us
1252 val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
1253 val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
1254 in s_tuple T R' us end
1255 | Construct (us', T, _, us) =>
1258 val Rs = map rep_of us
1259 val R = best_one_rep_for_type scope T
1261 constr_spec datatypes (original_name (nickname_of (hd us')), T)
1262 val opt = exists is_opt_rep Rs orelse not total
1263 in Construct (map sub us', T, R |> opt ? Opt, us) end
1265 let val u = modify_name_rep u (the_name table u) in
1266 if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
1267 not (is_opt_rep (rep_of u)) then
1270 s_op1 Cast (type_of u) (Formula polar) u
1274 in aux table def Pos end
1276 (* int -> KK.n_ary_index list -> KK.n_ary_index list
1277 -> int * KK.n_ary_index list *)
1278 fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
1279 | fresh_n_ary_index n ((m, j) :: xs) ys =
1280 if m = n then (j, ys @ ((m, j + 1) :: xs))
1281 else fresh_n_ary_index n xs ((m, j) :: ys)
1282 (* int -> name_pool -> int * name_pool *)
1283 fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
1284 let val (j, rels') = fresh_n_ary_index n rels [] in
1285 (j, {rels = rels', vars = vars, formula_reg = formula_reg,
1288 (* int -> name_pool -> int * name_pool *)
1289 fun fresh_var n {rels, vars, formula_reg, rel_reg} =
1290 let val (j, vars') = fresh_n_ary_index n vars [] in
1291 (j, {rels = rels, vars = vars', formula_reg = formula_reg,
1294 (* int -> name_pool -> int * name_pool *)
1295 fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
1296 (formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
1298 (* int -> name_pool -> int * name_pool *)
1299 fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
1300 (rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
1301 rel_reg = rel_reg + 1})
1303 (* nut -> nut list * name_pool * nut NameTable.table
1304 -> nut list * name_pool * nut NameTable.table *)
1305 fun rename_plain_var v (ws, pool, table) =
1307 val is_formula = (rep_of v = Formula Neut)
1308 val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg
1309 val (j, pool) = fresh pool
1310 val constr = if is_formula then FormulaReg else RelReg
1311 val w = constr (j, type_of v, rep_of v)
1312 in (w :: ws, pool, NameTable.update (v, w) table) end
1314 (* typ -> rep -> nut list -> nut *)
1315 fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
1317 let val arity1 = arity_of_rep R1 in
1318 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
1319 shape_tuple T2 R2 (List.drop (us, arity1))])
1321 | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
1322 Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
1323 | shape_tuple T _ [u] =
1324 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
1325 | shape_tuple T Unit [] = Cst (Unity, T, Unit)
1326 | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
1328 (* bool -> nut -> nut list * name_pool * nut NameTable.table
1329 -> nut list * name_pool * nut NameTable.table *)
1330 fun rename_n_ary_var rename_free v (ws, pool, table) =
1334 val arity = arity_of_rep R
1335 val nick = nickname_of v
1336 val (constr, fresh) = if rename_free then (FreeRel, fresh_rel)
1337 else (BoundRel, fresh_var)
1339 if not rename_free andalso arity > 1 then
1341 val atom_schema = atom_schema_of_rep R
1342 val type_schema = type_schema_of_rep T R
1343 val (js, pool) = funpow arity (fn (js, pool) =>
1344 let val (j, pool) = fresh 1 pool in
1348 val ws' = map3 (fn j => fn x => fn T =>
1349 constr ((1, j), T, Atom x,
1350 nick ^ " [" ^ string_of_int j ^ "]"))
1351 (rev js) atom_schema type_schema
1352 in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
1358 if is_sel_like_and_no_discr nick then
1359 case domain_type T of
1360 @{typ "unsigned_bit word"} =>
1361 (snd unsigned_bit_word_sel_rel, pool)
1362 | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
1363 | _ => fresh arity pool
1366 | _ => fresh arity pool
1367 val w = constr ((arity, j), T, R, nick)
1368 in (w :: ws, pool, NameTable.update (v, w) table) end
1371 (* nut list -> name_pool -> nut NameTable.table
1372 -> nut list * name_pool * nut NameTable.table *)
1373 fun rename_free_vars vs pool table =
1375 val vs = filter (not_equal Unit o rep_of) vs
1376 val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
1377 in (rev vs, pool, table) end
1379 (* name_pool -> nut NameTable.table -> nut -> nut *)
1380 fun rename_vars_in_nut pool table u =
1383 | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
1384 | Op2 (oper, T, R, u1, u2) =>
1385 if oper = All orelse oper = Exist orelse oper = Lambda then
1387 val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
1390 Op2 (oper, T, R, rename_vars_in_nut pool table u1,
1391 rename_vars_in_nut pool table u2)
1394 Op2 (oper, T, R, rename_vars_in_nut pool table u1,
1395 rename_vars_in_nut pool table u2)
1396 | Op3 (Let, T, R, u1, u2, u3) =>
1397 if rep_of u2 = Unit orelse inline_nut u2 then
1399 val u2 = rename_vars_in_nut pool table u2
1400 val table = NameTable.update (u1, u2) table
1401 in rename_vars_in_nut pool table u3 end
1404 val bs = untuple I u1
1405 val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
1407 Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
1408 rename_vars_in_nut pool table u2,
1409 rename_vars_in_nut pool table' u3)
1411 | Op3 (oper, T, R, u1, u2, u3) =>
1412 Op3 (oper, T, R, rename_vars_in_nut pool table u1,
1413 rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3)
1414 | Tuple (T, R, us) => Tuple (T, R, map (rename_vars_in_nut pool table) us)
1415 | Construct (us', T, R, us) =>
1416 Construct (map (rename_vars_in_nut pool table) us', T, R,
1417 map (rename_vars_in_nut pool table) us)
1418 | _ => the_name table u