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 styp = Nitpick_Util.styp
11 type hol_context = Nitpick_HOL.hol_context
12 type scope = Nitpick_Scope.scope
13 type name_pool = Nitpick_Peephole.name_pool
14 type rep = Nitpick_Rep.rep
70 Cst of cst * typ * rep |
71 Op1 of op1 * typ * rep * nut |
72 Op2 of op2 * typ * rep * nut * nut |
73 Op3 of op3 * typ * rep * nut * nut * nut |
74 Tuple of typ * rep * nut list |
75 Construct of nut list * typ * rep * nut list |
76 BoundName of int * typ * rep * string |
77 FreeName of string * typ * rep |
78 ConstName of string * typ * rep |
79 BoundRel of Kodkod.n_ary_index * typ * rep * string |
80 FreeRel of Kodkod.n_ary_index * typ * rep * string |
81 RelReg of int * typ * rep |
82 FormulaReg of int * typ * rep
84 structure NameTable : TABLE
86 exception NUT of string * nut list
88 val string_for_nut : Proof.context -> nut -> string
89 val inline_nut : nut -> bool
90 val type_of : nut -> typ
91 val rep_of : nut -> rep
92 val nickname_of : nut -> string
93 val is_skolem_name : nut -> bool
94 val is_eval_name : nut -> bool
95 val is_Cst : cst -> nut -> bool
96 val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
97 val map_nut : (nut -> nut) -> nut -> nut
98 val untuple : (nut -> 'a) -> nut -> 'a list
99 val add_free_and_const_names :
100 nut -> nut list * nut list -> nut list * nut list
101 val name_ord : (nut * nut) -> order
102 val the_name : 'a NameTable.table -> nut -> 'a
103 val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
104 val nut_from_term : hol_context -> op2 -> term -> nut
105 val is_fully_representable_set : nut -> bool
106 val choose_reps_for_free_vars :
107 scope -> styp list -> nut list -> rep NameTable.table
108 -> nut list * rep NameTable.table
109 val choose_reps_for_consts :
110 scope -> bool -> nut list -> rep NameTable.table
111 -> nut list * rep NameTable.table
112 val choose_reps_for_all_sels :
113 scope -> rep NameTable.table -> nut list * rep NameTable.table
114 val choose_reps_in_nut :
115 scope -> bool -> rep NameTable.table -> bool -> nut -> nut
116 val rename_free_vars :
117 nut list -> name_pool -> nut NameTable.table
118 -> nut list * name_pool * nut NameTable.table
119 val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut
122 structure Nitpick_Nut : NITPICK_NUT =
128 open Nitpick_Peephole
131 structure KK = Kodkod
187 Cst of cst * typ * rep |
188 Op1 of op1 * typ * rep * nut |
189 Op2 of op2 * typ * rep * nut * nut |
190 Op3 of op3 * typ * rep * nut * nut * nut |
191 Tuple of typ * rep * nut list |
192 Construct of nut list * typ * rep * nut list |
193 BoundName of int * typ * rep * string |
194 FreeName of string * typ * rep |
195 ConstName of string * typ * rep |
196 BoundRel of KK.n_ary_index * typ * rep * string |
197 FreeRel of KK.n_ary_index * typ * rep * string |
198 RelReg of int * typ * rep |
199 FormulaReg of int * typ * rep
201 exception NUT of string * nut list
203 fun string_for_cst False = "False"
204 | string_for_cst True = "True"
205 | string_for_cst Iden = "Iden"
206 | string_for_cst (Num j) = "Num " ^ signed_string_of_int j
207 | string_for_cst Unknown = "Unknown"
208 | string_for_cst Unrep = "Unrep"
209 | string_for_cst Suc = "Suc"
210 | string_for_cst Add = "Add"
211 | string_for_cst Subtract = "Subtract"
212 | string_for_cst Multiply = "Multiply"
213 | string_for_cst Divide = "Divide"
214 | string_for_cst Gcd = "Gcd"
215 | string_for_cst Lcm = "Lcm"
216 | string_for_cst Fracs = "Fracs"
217 | string_for_cst NormFrac = "NormFrac"
218 | string_for_cst NatToInt = "NatToInt"
219 | string_for_cst IntToNat = "IntToNat"
221 fun string_for_op1 Not = "Not"
222 | string_for_op1 Finite = "Finite"
223 | string_for_op1 Converse = "Converse"
224 | string_for_op1 Closure = "Closure"
225 | string_for_op1 SingletonSet = "SingletonSet"
226 | string_for_op1 IsUnknown = "IsUnknown"
227 | string_for_op1 SafeThe = "SafeThe"
228 | string_for_op1 First = "First"
229 | string_for_op1 Second = "Second"
230 | string_for_op1 Cast = "Cast"
232 fun string_for_op2 All = "All"
233 | string_for_op2 Exist = "Exist"
234 | string_for_op2 Or = "Or"
235 | string_for_op2 And = "And"
236 | string_for_op2 Less = "Less"
237 | string_for_op2 Subset = "Subset"
238 | string_for_op2 DefEq = "DefEq"
239 | string_for_op2 Eq = "Eq"
240 | string_for_op2 The = "The"
241 | string_for_op2 Eps = "Eps"
242 | string_for_op2 Triad = "Triad"
243 | string_for_op2 Composition = "Composition"
244 | string_for_op2 Product = "Product"
245 | string_for_op2 Image = "Image"
246 | string_for_op2 Apply = "Apply"
247 | string_for_op2 Lambda = "Lambda"
249 fun string_for_op3 Let = "Let"
250 | string_for_op3 If = "If"
252 fun basic_string_for_nut indent ctxt u =
254 val sub = basic_string_for_nut (indent + 1) ctxt
256 (if indent = 0 then "" else "\n" ^ implode (replicate (2 * indent) " ")) ^
260 "Cst " ^ string_for_cst c ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
262 | Op1 (oper, T, R, u1) =>
263 "Op1 " ^ string_for_op1 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
264 string_for_rep R ^ " " ^ sub u1
265 | Op2 (oper, T, R, u1, u2) =>
266 "Op2 " ^ string_for_op2 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
267 string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2
268 | Op3 (oper, T, R, u1, u2, u3) =>
269 "Op3 " ^ string_for_op3 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
270 string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 ^ " " ^ sub u3
271 | Tuple (T, R, us) =>
272 "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
274 | Construct (us', T, R, us) =>
275 "Construct " ^ implode (map sub us') ^ " " ^
276 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
278 | BoundName (j, T, R, nick) =>
279 "BoundName " ^ signed_string_of_int j ^ " " ^
280 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
281 | FreeName (s, T, R) =>
282 "FreeName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
284 | ConstName (s, T, R) =>
285 "ConstName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
287 | BoundRel ((n, j), T, R, nick) =>
288 "BoundRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
289 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
290 | FreeRel ((n, j), T, R, nick) =>
291 "FreeRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
292 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
293 | RelReg (j, T, R) =>
294 "RelReg " ^ signed_string_of_int j ^ " " ^ Syntax.string_of_typ ctxt T ^
295 " " ^ string_for_rep R
296 | FormulaReg (j, T, R) =>
297 "FormulaReg " ^ signed_string_of_int j ^ " " ^
298 Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R) ^
301 val string_for_nut = basic_string_for_nut 0
303 fun inline_nut (Op1 _) = false
304 | inline_nut (Op2 _) = false
305 | inline_nut (Op3 _) = false
306 | inline_nut (Tuple (_, _, us)) = forall inline_nut us
307 | inline_nut _ = true
309 fun type_of (Cst (_, T, _)) = T
310 | type_of (Op1 (_, T, _, _)) = T
311 | type_of (Op2 (_, T, _, _, _)) = T
312 | type_of (Op3 (_, T, _, _, _, _)) = T
313 | type_of (Tuple (T, _, _)) = T
314 | type_of (Construct (_, T, _, _)) = T
315 | type_of (BoundName (_, T, _, _)) = T
316 | type_of (FreeName (_, T, _)) = T
317 | type_of (ConstName (_, T, _)) = T
318 | type_of (BoundRel (_, T, _, _)) = T
319 | type_of (FreeRel (_, T, _, _)) = T
320 | type_of (RelReg (_, T, _)) = T
321 | type_of (FormulaReg (_, T, _)) = T
323 fun rep_of (Cst (_, _, R)) = R
324 | rep_of (Op1 (_, _, R, _)) = R
325 | rep_of (Op2 (_, _, R, _, _)) = R
326 | rep_of (Op3 (_, _, R, _, _, _)) = R
327 | rep_of (Tuple (_, R, _)) = R
328 | rep_of (Construct (_, _, R, _)) = R
329 | rep_of (BoundName (_, _, R, _)) = R
330 | rep_of (FreeName (_, _, R)) = R
331 | rep_of (ConstName (_, _, R)) = R
332 | rep_of (BoundRel (_, _, R, _)) = R
333 | rep_of (FreeRel (_, _, R, _)) = R
334 | rep_of (RelReg (_, _, R)) = R
335 | rep_of (FormulaReg (_, _, R)) = R
337 fun nickname_of (BoundName (_, _, _, nick)) = nick
338 | nickname_of (FreeName (s, _, _)) = s
339 | nickname_of (ConstName (s, _, _)) = s
340 | nickname_of (BoundRel (_, _, _, nick)) = nick
341 | nickname_of (FreeRel (_, _, _, nick)) = nick
342 | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
344 fun is_skolem_name u =
345 space_explode name_sep (nickname_of u)
346 |> exists (String.isPrefix skolem_prefix)
347 handle NUT ("Nitpick_Nut.nickname_of", _) => false
349 String.isPrefix eval_prefix (nickname_of u)
350 handle NUT ("Nitpick_Nut.nickname_of", _) => false
351 fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
356 Op1 (_, _, _, u1) => fold_nut f u1
357 | Op2 (_, _, _, u1, u2) => fold_nut f u1 #> fold_nut f u2
358 | Op3 (_, _, _, u1, u2, u3) => fold_nut f u1 #> fold_nut f u2 #> fold_nut f u3
359 | Tuple (_, _, us) => fold (fold_nut f) us
360 | Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
364 Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
365 | Op2 (oper, T, R, u1, u2) => Op2 (oper, T, R, map_nut f u1, map_nut f u2)
366 | Op3 (oper, T, R, u1, u2, u3) =>
367 Op3 (oper, T, R, map_nut f u1, map_nut f u2, map_nut f u3)
368 | Tuple (T, R, us) => Tuple (T, R, map (map_nut f) us)
369 | Construct (us', T, R, us) =>
370 Construct (map (map_nut f) us', T, R, map (map_nut f) us)
373 fun name_ord (BoundName (j1, _, _, _), BoundName (j2, _, _, _)) =
375 | name_ord (BoundName _, _) = LESS
376 | name_ord (_, BoundName _) = GREATER
377 | name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) =
378 (case fast_string_ord (s1, s2) of
379 EQUAL => Term_Ord.typ_ord (T1, T2)
381 | name_ord (FreeName _, _) = LESS
382 | name_ord (_, FreeName _) = GREATER
383 | name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) =
384 (case fast_string_ord (s1, s2) of
385 EQUAL => Term_Ord.typ_ord (T1, T2)
387 | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
389 fun num_occurrences_in_nut needle_u stack_u =
390 fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0
391 val is_subnut_of = not_equal 0 oo num_occurrences_in_nut
393 fun substitute_in_nut needle_u needle_u' =
394 map_nut (fn u => if u = needle_u then needle_u' else u)
396 val add_free_and_const_names =
397 fold_nut (fn u => case u of
398 FreeName _ => apfst (insert (op =) u)
399 | ConstName _ => apsnd (insert (op =) u)
402 fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
403 | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
404 | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
405 | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u])
407 structure NameTable = Table(type key = nut val ord = name_ord)
409 fun the_name table name =
410 case NameTable.lookup table name of
412 | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
413 fun the_rel table name =
414 case the_name table name of
415 FreeRel (x, _, _, _) => x
416 | u => raise NUT ("Nitpick_Nut.the_rel", [u])
418 fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
420 let val res_T = fst (HOLogic.dest_prodT T) in
421 (res_T, Const (@{const_name fst}, T --> res_T) $ t)
423 fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) =
424 (domain_type (range_type T), t2)
426 let val res_T = snd (HOLogic.dest_prodT T) in
427 (res_T, Const (@{const_name snd}, T --> res_T) $ t)
429 fun factorize (z as (Type (@{type_name prod}, _), _)) =
430 maps factorize [mk_fst z, mk_snd z]
433 fun nut_from_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, ...}) eq =
437 val sub = aux Eq ss Ts
438 val sub' = aux eq ss Ts
439 fun sub_abs s T = aux eq (s :: ss) (T :: Ts)
440 fun sub_equals T t1 t2 =
442 val (binder_Ts, body_T) = strip_type (domain_type T)
443 val n = length binder_Ts
445 if eq = Eq andalso n > 0 then
447 val t1 = incr_boundvars n t1
448 val t2 = incr_boundvars n t2
449 val xs = map Bound (n - 1 downto 0)
450 val equation = Const (@{const_name "op ="},
451 body_T --> body_T --> bool_T)
452 $ betapplys (t1, xs) $ betapplys (t2, xs)
454 fold_rev (fn T => fn (t, j) =>
455 (Const (@{const_name All}, T --> bool_T)
456 $ Abs ("x" ^ nat_subscript j, T, t), j - 1))
457 binder_Ts (equation, n) |> fst
460 Op2 (eq, bool_T, Any, aux Eq ss Ts t1, aux Eq ss Ts t2)
462 fun do_quantifier quant s T t1 =
464 val bound_u = BoundName (length Ts, T, Any, s)
465 val body_u = sub_abs s T t1
466 in Op2 (quant, bool_T, Any, bound_u, body_u) end
469 val (ts', t2) = split_last ts
470 val t1 = list_comb (t0, ts')
471 val T1 = fastype_of1 (Ts, t1)
472 in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
473 fun do_description_operator oper undef_s (x as (_, T)) t1 =
475 Op2 (oper, range_type T, Any, sub t1,
476 sub (Const (undef_s, range_type T)))
478 do_apply (Const x) [t1]
479 fun do_construct (x as (_, T)) ts =
480 case num_binder_types T - length ts of
481 0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
482 o nth_sel_for_constr x)
483 (~1 upto num_sels_for_constr_type T - 1),
485 ts |> map (`(curry fastype_of1 Ts))
486 |> maps factorize |> map (sub o snd))
487 | k => sub (eta_expand Ts t k)
490 (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
491 do_quantifier All s T t1
492 | (t0 as Const (@{const_name all}, _), [t1]) =>
493 sub' (t0 $ eta_expand Ts t1 1)
494 | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
495 | (Const (@{const_name "==>"}, _), [t1, t2]) =>
496 Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
497 | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
498 Op2 (And, prop_T, Any, sub' t1, sub' t2)
499 | (Const (@{const_name Trueprop}, _), [t1]) => sub' t1
500 | (Const (@{const_name Not}, _), [t1]) =>
502 Op1 (Not, _, _, u11) => u11
503 | u1 => Op1 (Not, bool_T, Any, u1))
504 | (Const (@{const_name False}, T), []) => Cst (False, T, Any)
505 | (Const (@{const_name True}, T), []) => Cst (True, T, Any)
506 | (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
507 do_quantifier All s T t1
508 | (t0 as Const (@{const_name All}, _), [t1]) =>
509 sub' (t0 $ eta_expand Ts t1 1)
510 | (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
511 do_quantifier Exist s T t1
512 | (t0 as Const (@{const_name Ex}, _), [t1]) =>
513 sub' (t0 $ eta_expand Ts t1 1)
514 | (Const (x as (@{const_name The}, _)), [t1]) =>
515 do_description_operator The @{const_name undefined_fast_The} x t1
516 | (Const (x as (@{const_name Eps}, _)), [t1]) =>
517 do_description_operator Eps @{const_name undefined_fast_Eps} x t1
518 | (Const (@{const_name "op ="}, T), [t1]) =>
519 Op1 (SingletonSet, range_type T, Any, sub t1)
520 | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
521 | (Const (@{const_name "op &"}, _), [t1, t2]) =>
522 Op2 (And, bool_T, Any, sub' t1, sub' t2)
523 | (Const (@{const_name "op |"}, _), [t1, t2]) =>
524 Op2 (Or, bool_T, Any, sub t1, sub t2)
525 | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
526 Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
527 | (Const (@{const_name If}, T), [t1, t2, t3]) =>
528 Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
529 | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
530 Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
531 sub t1, sub_abs s T' t2)
532 | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
533 sub (t0 $ t1 $ eta_expand Ts t2 1)
534 | (Const (@{const_name Pair}, T), [t1, t2]) =>
535 Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
536 | (Const (@{const_name fst}, T), [t1]) =>
537 Op1 (First, range_type T, Any, sub t1)
538 | (Const (@{const_name snd}, T), [t1]) =>
539 Op1 (Second, range_type T, Any, sub t1)
540 | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
541 | (Const (@{const_name converse}, T), [t1]) =>
542 Op1 (Converse, range_type T, Any, sub t1)
543 | (Const (@{const_name trancl}, T), [t1]) =>
544 Op1 (Closure, range_type T, Any, sub t1)
545 | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
546 Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
547 | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
548 Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
549 | (Const (@{const_name image}, T), [t1, t2]) =>
550 Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
551 | (Const (x as (s as @{const_name Suc}, T)), []) =>
552 if is_built_in_const thy stds false x then Cst (Suc, T, Any)
553 else if is_constr ctxt stds x then do_construct x []
554 else ConstName (s, T, Any)
555 | (Const (@{const_name finite}, T), [t1]) =>
556 (if is_finite_type hol_ctxt (domain_type T) then
557 Cst (True, bool_T, Any)
559 Const (@{const_name top}, _) => Cst (False, bool_T, Any)
560 | _ => Op1 (Finite, bool_T, Any, sub t1))
561 | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
562 | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
563 if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
564 else if is_constr ctxt stds x then do_construct x []
565 else ConstName (s, T, Any)
566 | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
567 if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
568 else ConstName (s, T, Any)
569 | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
570 if is_built_in_const thy stds false x then Cst (Add, T, Any)
571 else ConstName (s, T, Any)
572 | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
573 if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
574 else ConstName (s, T, Any)
575 | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
576 if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
577 else ConstName (s, T, Any)
578 | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
579 if is_built_in_const thy stds false x then Cst (Divide, T, Any)
580 else ConstName (s, T, Any)
581 | (t0 as Const (x as (@{const_name ord_class.less}, _)),
583 if is_built_in_const thy stds false x then
584 Op2 (Less, bool_T, Any, sub t1, sub t2)
587 | (Const (@{const_name ord_class.less_eq},
588 Type (@{type_name fun},
589 [Type (@{type_name fun}, [_, @{typ bool}]), _])),
591 Op2 (Subset, bool_T, Any, sub t1, sub t2)
592 (* FIXME: find out if this case is necessary *)
593 | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
595 if is_built_in_const thy stds false x then
596 Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
599 | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
600 | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
601 | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
602 if is_built_in_const thy stds false x then
603 let val num_T = domain_type T in
604 Op2 (Apply, num_T --> num_T, Any,
605 Cst (Subtract, num_T --> num_T --> num_T, Any),
606 Cst (Num 0, num_T, Any))
609 ConstName (s, T, Any)
610 | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
611 | (Const (@{const_name is_unknown}, _), [t1]) =>
612 Op1 (IsUnknown, bool_T, Any, sub t1)
613 | (Const (@{const_name safe_The},
614 Type (@{type_name fun}, [_, T2])), [t1]) =>
615 Op1 (SafeThe, T2, Any, sub t1)
616 | (Const (x as (@{const_name safe_Eps}, _)), [t1]) =>
617 do_description_operator Eps @{const_name undefined_fast_Eps} x t1
618 | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
619 | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
620 | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
621 Cst (NatToInt, T, Any)
622 | (Const (@{const_name of_nat},
623 T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
624 Cst (NatToInt, T, Any)
625 | (t0 as Const (x as (s, T)), ts) =>
626 if is_constr ctxt stds x then
628 else if String.isPrefix numeral_prefix s then
629 Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
631 (case arity_of_built_in_const thy stds fast_descrs x of
633 (case n - length ts of
634 0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
635 | k => if k > 0 then sub (eta_expand Ts t k)
637 | NONE => if null ts then ConstName (s, T, Any)
639 | (Free (s, T), []) => FreeName (s, T, Any)
640 | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
642 BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
643 | (Abs (s, T, t1), []) =>
644 Op2 (Lambda, T --> fastype_of1 (T :: Ts, t1), Any,
645 BoundName (length Ts, T, Any, s), sub_abs s T t1)
646 | (t0, ts) => do_apply t0 ts
650 fun is_fully_representable_set u =
651 not (is_opt_rep (rep_of u)) andalso
654 | Op1 (SingletonSet, _, _, _) => true
655 | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
656 | Op2 (oper, _, _, u1, u2) =>
659 ConstName (s, _, _) =>
660 is_sel_like_and_no_discr s orelse s = @{const_name set}
664 | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
667 fun rep_for_abs_fun scope T =
668 let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
669 Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
672 fun choose_rep_for_free_var scope pseudo_frees v (vs, table) =
674 val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then
675 best_opt_set_rep_for_type
677 best_non_opt_set_rep_for_type) scope (type_of v)
678 val v = modify_name_rep v R
679 in (v :: vs, NameTable.update (v, R) table) end
680 fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
683 val x as (s, T) = (nickname_of v, type_of v)
684 val R = (if is_abs_fun ctxt x then
686 else if is_rep_fun ctxt x then
687 Func oo best_non_opt_symmetric_reps_for_fun_type
688 else if all_exact orelse is_skolem_name v orelse
689 member (op =) [@{const_name undefined_fast_The},
690 @{const_name undefined_fast_Eps},
692 @{const_name bisim_iterator_max}]
693 (original_name s) then
694 best_non_opt_set_rep_for_type
695 else if member (op =) [@{const_name set}, @{const_name distinct},
696 @{const_name ord_class.less},
697 @{const_name ord_class.less_eq}]
698 (original_name s) then
699 best_set_rep_for_type
701 best_opt_set_rep_for_type) scope T
702 val v = modify_name_rep v R
703 in (v :: vs, NameTable.update (v, R) table) end
705 fun choose_reps_for_free_vars scope pseudo_frees vs table =
706 fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
707 fun choose_reps_for_consts scope all_exact vs table =
708 fold (choose_rep_for_const scope all_exact) vs ([], table)
710 fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
711 (x as (_, T)) n (vs, table) =
713 val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
714 val R' = if n = ~1 orelse is_word_type (body_type T) orelse
715 (is_fun_type (range_type T') andalso
716 is_boolean_type (body_type T')) then
717 best_non_opt_set_rep_for_type scope T'
719 best_opt_set_rep_for_type scope T' |> unopt_rep
720 val v = ConstName (s', T', R')
721 in (v :: vs, NameTable.update (v, R') table) end
722 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
723 fold_rev (choose_rep_for_nth_sel_for_constr scope x)
724 (~1 upto num_sels_for_constr_type T - 1)
725 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
726 | choose_rep_for_sels_of_datatype scope {constrs, ...} =
727 fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
728 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
729 fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
731 fun choose_rep_for_bound_var scope v table =
732 let val R = best_one_rep_for_type scope (type_of v) in
733 NameTable.update (v, R) table
736 (* A nut is said to be constructive if whenever it evaluates to unknown in our
737 three-valued logic, it would evaluate to an unrepresentable value ("Unrep")
738 according to the HOL semantics. For example, "Suc n" is constructive if "n"
739 is representable or "Unrep", because unknown implies "Unrep". *)
740 fun is_constructive u =
741 is_Cst Unrep u orelse
742 (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
744 Cst (Num _, _, _) => true
745 | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
746 | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
747 | Op3 (If, _, _, u1, u2, u3) =>
748 not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
749 | Tuple (_, _, us) => forall is_constructive us
750 | Construct (_, _, _, us) => forall is_constructive us
753 fun unknown_boolean T R =
754 Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
757 fun s_op1 oper T R u1 =
759 if is_Cst True u1 then Cst (False, T, R)
760 else if is_Cst False u1 then Cst (True, T, R)
764 handle SAME () => Op1 (oper, T, R, u1))
765 fun s_op2 oper T R u1 u2 =
767 All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
768 | Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2
770 if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R)
771 else if is_Cst False u1 then u2
772 else if is_Cst False u2 then u1
775 if exists (is_Cst False) [u1, u2] then Cst (False, T, unopt_rep R)
776 else if is_Cst True u1 then u2
777 else if is_Cst True u2 then u1
780 (case pairself (is_Cst Unrep) (u1, u2) of
781 (true, true) => unknown_boolean T R
782 | (false, false) => raise SAME ()
783 | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()
784 else Cst (False, T, Formula Neut))
786 if is_Cst True u1 then u1
787 else if is_Cst False u2 then u2
790 if is_Cst Unrep u1 then
792 else if is_Cst Unrep u2 then
793 if is_boolean_type T then
794 if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
795 else unknown_boolean T R
796 else if is_constructive u1 then
799 Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
804 | _ => raise SAME ())
805 handle SAME () => Op2 (oper, T, R, u1, u2))
806 fun s_op3 oper T R u1 u2 u3 =
809 if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then
810 substitute_in_nut u1 u2 u3
813 | _ => raise SAME ())
814 handle SAME () => Op3 (oper, T, R, u1, u2, u3))
816 if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
818 fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
819 | untuple f u = [f u]
821 fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
824 val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
825 fun bool_rep polar opt =
826 if polar = Neut andalso opt then Opt bool_atom_R else Formula polar
827 fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2
828 fun triad_fn f = triad (f Pos) (f Neg)
829 fun unrepify_nut_in_nut table def polar needle_u =
830 let val needle_T = type_of needle_u in
831 substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown
832 else Unrep, needle_T, Any))
833 #> aux table def polar
835 and aux table def polar u =
838 val sub = gsub false Neut
841 Cst (False, T, _) => Cst (False, T, Formula Neut)
842 | Cst (True, T, _) => Cst (True, T, Formula Neut)
843 | Cst (Num j, T, _) =>
844 if is_word_type T then
845 Cst (if is_twos_complement_representable bits j then Num j
846 else Unrep, T, best_opt_set_rep_for_type scope T)
849 val (k, j0) = spec_of_type scope T
850 val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
853 if ok then Cst (Num j, T, Atom (k, j0))
854 else Cst (Unrep, T, Opt (Atom (k, j0)))
856 | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
857 let val R = Atom (spec_of_type scope T1) in
858 Cst (Suc, T, Func (R, Opt R))
860 | Cst (Fracs, T, _) =>
861 Cst (Fracs, T, best_non_opt_set_rep_for_type scope T)
862 | Cst (NormFrac, T, _) =>
863 let val R1 = Atom (spec_of_type scope (domain_type T)) in
864 Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
867 if cst = Unknown orelse cst = Unrep then
868 case (is_boolean_type T, polar |> unsound ? flip_polarity) of
869 (true, Pos) => Cst (False, T, Formula Pos)
870 | (true, Neg) => Cst (True, T, Formula Neg)
871 | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
872 else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
875 val T1 = domain_type T
876 val R1 = Atom (spec_of_type scope T1)
877 val total = T1 = nat_T andalso
878 (cst = Subtract orelse cst = Divide orelse cst = Gcd)
879 in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
880 else if cst = NatToInt orelse cst = IntToNat then
882 val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
883 val (ran_card, ran_j0) = spec_of_type scope (range_type T)
884 val total = not (is_word_type (domain_type T)) andalso
885 (if cst = NatToInt then
886 max_int_for_card ran_card >= dom_card + 1
888 max_int_for_card dom_card < ran_card)
890 Cst (cst, T, Func (Atom (dom_card, dom_j0),
891 Atom (ran_card, ran_j0) |> not total ? Opt))
894 Cst (cst, T, best_set_rep_for_type scope T)
895 | Op1 (Not, T, _, u1) =>
896 (case gsub def (flip_polarity polar) u1 of
897 Op2 (Triad, T, _, u11, u12) =>
898 triad (s_op1 Not T (Formula Pos) u12)
899 (s_op1 Not T (Formula Neg) u11)
900 | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
901 | Op1 (IsUnknown, T, _, u1) =>
902 let val u1 = sub u1 in
903 if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
904 else Cst (False, T, Formula Neut)
906 | Op1 (oper, T, _, u1) =>
911 Finite => bool_rep polar (is_opt_rep R1)
912 | _ => (if is_opt_rep R1 then best_opt_set_rep_for_type
913 else best_non_opt_set_rep_for_type) scope T
914 in s_op1 oper T R u1 end
915 | Op2 (Less, T, _, u1, u2) =>
919 val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
920 in s_op2 Less T R u1 u2 end
921 | Op2 (Subset, T, _, u1, u2) =>
925 val opt = exists (is_opt_rep o rep_of) [u1, u2]
926 val R = bool_rep polar opt
929 triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
930 else if not opt orelse unsound orelse polar = Neg orelse
931 is_concrete_type datatypes true (type_of u1) then
932 s_op2 Subset T R u1 u2
934 Cst (False, T, Formula Pos)
936 | Op2 (DefEq, T, _, u1, u2) =>
937 s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
938 | Op2 (Eq, T, _, u1, u2) =>
942 fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2'
943 fun opt_opt_case () =
945 triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2')
949 (* hackish optimization *)
950 if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
953 if unsound orelse polar = Neg orelse
954 is_concrete_type datatypes true (type_of u1) then
955 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
956 (true, true) => opt_opt_case ()
957 | (true, false) => hybrid_case u1'
958 | (false, true) => hybrid_case u2'
959 | (false, false) => non_opt_case ()
961 Cst (False, T, Formula Pos)
962 |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
964 | Op2 (Image, T, _, u1, u2) =>
969 (case (rep_of u1', rep_of u2') of
970 (Func (R11, R12), Func (R21, Formula Neut)) =>
971 if R21 = R11 andalso is_lone_rep R12 then
974 best_non_opt_set_rep_for_type scope T
975 |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
976 in s_op2 Image T R u1' u2' end
979 | _ => raise SAME ())
983 val dom_T = domain_type T1
984 val ran_T = range_type T1
985 val x_u = BoundName (~1, dom_T, Any, "image.x")
986 val y_u = BoundName (~2, ran_T, Any, "image.y")
988 Op2 (Lambda, T, Any, y_u,
989 Op2 (Exist, bool_T, Any, x_u,
990 Op2 (And, bool_T, Any,
992 Op2 (Lambda, _, _, u21, u22) =>
993 if num_occurrences_in_nut u21 u22 = 0 then
996 Op2 (Apply, bool_T, Any, u2, x_u)
997 | _ => Op2 (Apply, bool_T, Any, u2, x_u),
999 Op2 (Eq, bool_T, Any, y_u,
1000 Op2 (Apply, ran_T, Any, u1, x_u)))))
1004 | Op2 (Apply, T, _, u1, u2) =>
1012 case (u1, is_opt_rep R2) of
1013 (ConstName (@{const_name set}, _, _), false) => false
1014 | _ => exists is_opt_rep [R1, R2]
1016 if is_boolean_type T then
1019 lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T)
1021 |> opt ? opt_rep ofs T
1022 in s_op2 Apply T ran_R u1 u2 end
1023 | Op2 (Lambda, T, _, u1, u2) =>
1024 (case best_set_rep_for_type scope T of
1025 R as Func (R1, _) =>
1027 val table' = NameTable.update (u1, R1) table
1028 val u1' = aux table' false Neut u1
1029 val u2' = aux table' false Neut u2
1031 if is_opt_rep (rep_of u2') orelse
1032 (range_type T = bool_T andalso
1033 not (is_Cst False (unrepify_nut_in_nut table false Neut
1038 in s_op2 Lambda T R u1' u2' end
1039 | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u]))
1040 | Op2 (oper, T, _, u1, u2) =>
1041 if oper = All orelse oper = Exist then
1043 val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
1045 val u1' = aux table' def polar u1
1046 val u2' = aux table' def polar u2
1048 if polar = Neut andalso is_opt_rep (rep_of u2') then
1049 triad_fn (fn polar => gsub def polar u)
1051 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
1053 (unsound andalso (polar = Pos) = (oper = All)) orelse
1054 is_complete_type datatypes true (type_of u1) then
1058 val connective = if oper = All then And else Or
1059 val unrepified_u = unrepify_nut_in_nut table def polar
1063 (min_rep (rep_of quant_u) (rep_of unrepified_u))
1064 quant_u unrepified_u
1068 else if oper = Or orelse oper = And then
1070 val u1' = gsub def polar u1
1071 val u2' = gsub def polar u2
1073 (if polar = Neut then
1074 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
1075 (true, true) => triad_fn (fn polar => gsub def polar u)
1077 s_op2 oper T (Opt bool_atom_R)
1078 (triad_fn (fn polar => gsub def polar u1)) u2'
1080 s_op2 oper T (Opt bool_atom_R)
1081 u1' (triad_fn (fn polar => gsub def polar u2))
1082 | (false, false) => raise SAME ()
1085 handle SAME () => s_op2 oper T (Formula polar) u1' u2'
1087 else if oper = The orelse oper = Eps then
1090 val opt1 = is_opt_rep (rep_of u1')
1091 val opt = (oper = Eps orelse opt1)
1092 val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
1093 val R = if is_boolean_type T then bool_rep polar opt
1094 else unopt_R |> opt ? opt_rep ofs T
1095 val u = Op2 (oper, T, R, u1', sub u2)
1097 if is_complete_type datatypes true T orelse not opt1 then
1101 val x_u = BoundName (~1, T, unopt_R, "descr.x")
1102 val R = R |> opt_rep ofs T
1105 Op2 (Exist, bool_T, Formula Pos, x_u,
1106 s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1)
1107 x_u), u, Cst (Unknown, T, R))
1115 best_non_opt_set_rep_for_type scope T
1116 |> exists (is_opt_rep o rep_of) [u1, u2] ? opt_rep ofs T
1117 in s_op2 oper T R u1 u2 end
1118 | Op3 (Let, T, _, u1, u2, u3) =>
1122 val table' = NameTable.update (u1, R2) table
1123 val u1 = modify_name_rep u1 R2
1124 val u3 = aux table' false polar u3
1125 in s_op3 Let T (rep_of u3) u1 u2 u3 end
1126 | Op3 (If, T, _, u1, u2, u3) =>
1129 val u2 = gsub def polar u2
1130 val u3 = gsub def polar u3
1131 val min_R = min_rep (rep_of u2) (rep_of u3)
1132 val R = min_R |> is_opt_rep (rep_of u1) ? opt_rep ofs T
1133 in s_op3 If T R u1 u2 u3 end
1134 | Tuple (T, _, us) =>
1136 val Rs = map (best_one_rep_for_type scope o type_of) us
1139 |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T
1140 in s_tuple T R' us end
1141 | Construct (us', T, _, us) =>
1144 val Rs = map rep_of us
1145 val R = best_one_rep_for_type scope T
1147 constr_spec datatypes (original_name (nickname_of (hd us')), T)
1148 val opt = exists is_opt_rep Rs orelse not total
1149 in Construct (map sub us', T, R |> opt ? Opt, us) end
1151 let val u = modify_name_rep u (the_name table u) in
1152 if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
1153 not (is_opt_rep (rep_of u)) then
1156 s_op1 Cast (type_of u) (Formula polar) u
1159 in aux table def Pos end
1161 fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
1162 | fresh_n_ary_index n ((m, j) :: xs) ys =
1163 if m = n then (j, ys @ ((m, j + 1) :: xs))
1164 else fresh_n_ary_index n xs ((m, j) :: ys)
1165 fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
1166 let val (j, rels') = fresh_n_ary_index n rels [] in
1167 (j, {rels = rels', vars = vars, formula_reg = formula_reg,
1170 fun fresh_var n {rels, vars, formula_reg, rel_reg} =
1171 let val (j, vars') = fresh_n_ary_index n vars [] in
1172 (j, {rels = rels, vars = vars', formula_reg = formula_reg,
1175 fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
1176 (formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
1178 fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
1179 (rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
1180 rel_reg = rel_reg + 1})
1182 fun rename_plain_var v (ws, pool, table) =
1184 val is_formula = (rep_of v = Formula Neut)
1185 val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg
1186 val (j, pool) = fresh pool
1187 val constr = if is_formula then FormulaReg else RelReg
1188 val w = constr (j, type_of v, rep_of v)
1189 in (w :: ws, pool, NameTable.update (v, w) table) end
1191 fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2])
1193 let val arity1 = arity_of_rep R1 in
1194 Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
1195 shape_tuple T2 R2 (List.drop (us, arity1))])
1197 | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
1198 Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
1199 | shape_tuple T _ [u] =
1200 if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
1201 | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
1203 fun rename_n_ary_var rename_free v (ws, pool, table) =
1207 val arity = arity_of_rep R
1208 val nick = nickname_of v
1209 val (constr, fresh) = if rename_free then (FreeRel, fresh_rel)
1210 else (BoundRel, fresh_var)
1212 if not rename_free andalso arity > 1 then
1214 val atom_schema = atom_schema_of_rep R
1215 val type_schema = type_schema_of_rep T R
1216 val (js, pool) = funpow arity (fn (js, pool) =>
1217 let val (j, pool) = fresh 1 pool in
1221 val ws' = map3 (fn j => fn x => fn T =>
1222 constr ((1, j), T, Atom x,
1223 nick ^ " [" ^ string_of_int j ^ "]"))
1224 (rev js) atom_schema type_schema
1225 in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
1231 if is_sel_like_and_no_discr nick then
1232 case domain_type T of
1233 @{typ "unsigned_bit word"} =>
1234 (snd unsigned_bit_word_sel_rel, pool)
1235 | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
1236 | _ => fresh arity pool
1239 | _ => fresh arity pool
1240 val w = constr ((arity, j), T, R, nick)
1241 in (w :: ws, pool, NameTable.update (v, w) table) end
1244 fun rename_free_vars vs pool table =
1246 val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
1247 in (rev vs, pool, table) end
1249 fun rename_vars_in_nut pool table u =
1252 | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
1253 | Op2 (oper, T, R, u1, u2) =>
1254 if oper = All orelse oper = Exist orelse oper = Lambda then
1256 val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
1259 Op2 (oper, T, R, rename_vars_in_nut pool table u1,
1260 rename_vars_in_nut pool table u2)
1263 Op2 (oper, T, R, rename_vars_in_nut pool table u1,
1264 rename_vars_in_nut pool table u2)
1265 | Op3 (Let, T, R, u1, u2, u3) =>
1266 if inline_nut u2 then
1268 val u2 = rename_vars_in_nut pool table u2
1269 val table = NameTable.update (u1, u2) table
1270 in rename_vars_in_nut pool table u3 end
1273 val bs = untuple I u1
1274 val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
1276 Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
1277 rename_vars_in_nut pool table u2,
1278 rename_vars_in_nut pool table' u3)
1280 | Op3 (oper, T, R, u1, u2, u3) =>
1281 Op3 (oper, T, R, rename_vars_in_nut pool table u1,
1282 rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3)
1283 | Tuple (T, R, us) => Tuple (T, R, map (rename_vars_in_nut pool table) us)
1284 | Construct (us', T, R, us) =>
1285 Construct (map (rename_vars_in_nut pool table) us', T, R,
1286 map (rename_vars_in_nut pool table) us)
1287 | _ => the_name table u