src/HOL/Tools/Nitpick/nitpick_nut.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 61324 d4ec7594f558
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_nut.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Nitpick underlying terms (nuts).
     6 *)
     7 
     8 signature NITPICK_NUT =
     9 sig
    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
    14 
    15   datatype cst =
    16     False |
    17     True |
    18     Iden |
    19     Num of int |
    20     Unknown |
    21     Unrep |
    22     Suc |
    23     Add |
    24     Subtract |
    25     Multiply |
    26     Divide |
    27     Gcd |
    28     Lcm |
    29     Fracs |
    30     NormFrac |
    31     NatToInt |
    32     IntToNat
    33 
    34   datatype op1 =
    35     Not |
    36     Finite |
    37     Converse |
    38     Closure |
    39     SingletonSet |
    40     IsUnknown |
    41     SafeThe |
    42     First |
    43     Second |
    44     Cast
    45 
    46   datatype op2 =
    47     All |
    48     Exist |
    49     Or |
    50     And |
    51     Less |
    52     DefEq |
    53     Eq |
    54     Triad |
    55     Composition |
    56     Apply |
    57     Lambda
    58 
    59   datatype op3 =
    60     Let |
    61     If
    62 
    63   datatype nut =
    64     Cst of cst * typ * rep |
    65     Op1 of op1 * typ * rep * nut |
    66     Op2 of op2 * typ * rep * nut * nut |
    67     Op3 of op3 * typ * rep * nut * nut * nut |
    68     Tuple of typ * rep * nut list |
    69     Construct of nut list * typ * rep * nut list |
    70     BoundName of int * typ * rep * string |
    71     FreeName of string * typ * rep |
    72     ConstName of string * typ * rep |
    73     BoundRel of Kodkod.n_ary_index * typ * rep * string |
    74     FreeRel of Kodkod.n_ary_index * typ * rep * string |
    75     RelReg of int * typ * rep |
    76     FormulaReg of int * typ * rep
    77 
    78   structure NameTable : TABLE
    79 
    80   exception NUT of string * nut list
    81 
    82   val string_for_nut : Proof.context -> nut -> string
    83   val inline_nut : nut -> bool
    84   val type_of : nut -> typ
    85   val rep_of : nut -> rep
    86   val nickname_of : nut -> string
    87   val is_skolem_name : nut -> bool
    88   val is_eval_name : nut -> bool
    89   val is_Cst : cst -> nut -> bool
    90   val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
    91   val map_nut : (nut -> nut) -> nut -> nut
    92   val untuple : (nut -> 'a) -> nut -> 'a list
    93   val add_free_and_const_names :
    94     nut -> nut list * nut list -> nut list * nut list
    95   val name_ord : (nut * nut) -> order
    96   val the_name : 'a NameTable.table -> nut -> 'a
    97   val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
    98   val nut_from_term : hol_context -> op2 -> term -> nut
    99   val is_fully_representable_set : nut -> bool
   100   val choose_reps_for_free_vars :
   101     scope -> (string * typ) list -> nut list -> rep NameTable.table
   102     -> nut list * rep NameTable.table
   103   val choose_reps_for_consts :
   104     scope -> bool -> nut list -> rep NameTable.table
   105     -> nut list * rep NameTable.table
   106   val choose_reps_for_all_sels :
   107     scope -> rep NameTable.table -> nut list * rep NameTable.table
   108   val choose_reps_in_nut :
   109     scope -> bool -> rep NameTable.table -> bool -> nut -> nut
   110   val rename_free_vars :
   111     nut list -> name_pool -> nut NameTable.table
   112     -> nut list * name_pool * nut NameTable.table
   113   val rename_vars_in_nut : name_pool -> nut NameTable.table -> nut -> nut
   114 end;
   115 
   116 structure Nitpick_Nut : NITPICK_NUT =
   117 struct
   118 
   119 open Nitpick_Util
   120 open Nitpick_HOL
   121 open Nitpick_Scope
   122 open Nitpick_Peephole
   123 open Nitpick_Rep
   124 
   125 structure KK = Kodkod
   126 
   127 datatype cst =
   128   False |
   129   True |
   130   Iden |
   131   Num of int |
   132   Unknown |
   133   Unrep |
   134   Suc |
   135   Add |
   136   Subtract |
   137   Multiply |
   138   Divide |
   139   Gcd |
   140   Lcm |
   141   Fracs |
   142   NormFrac |
   143   NatToInt |
   144   IntToNat
   145 
   146 datatype op1 =
   147   Not |
   148   Finite |
   149   Converse |
   150   Closure |
   151   SingletonSet |
   152   IsUnknown |
   153   SafeThe |
   154   First |
   155   Second |
   156   Cast
   157 
   158 datatype op2 =
   159   All |
   160   Exist |
   161   Or |
   162   And |
   163   Less |
   164   DefEq |
   165   Eq |
   166   Triad |
   167   Composition |
   168   Apply |
   169   Lambda
   170 
   171 datatype op3 =
   172   Let |
   173   If
   174 
   175 datatype nut =
   176   Cst of cst * typ * rep |
   177   Op1 of op1 * typ * rep * nut |
   178   Op2 of op2 * typ * rep * nut * nut |
   179   Op3 of op3 * typ * rep * nut * nut * nut |
   180   Tuple of typ * rep * nut list |
   181   Construct of nut list * typ * rep * nut list |
   182   BoundName of int * typ * rep * string |
   183   FreeName of string * typ * rep |
   184   ConstName of string * typ * rep |
   185   BoundRel of KK.n_ary_index * typ * rep * string |
   186   FreeRel of KK.n_ary_index * typ * rep * string |
   187   RelReg of int * typ * rep |
   188   FormulaReg of int * typ * rep
   189 
   190 exception NUT of string * nut list
   191 
   192 fun string_for_cst False = "False"
   193   | string_for_cst True = "True"
   194   | string_for_cst Iden = "Iden"
   195   | string_for_cst (Num j) = "Num " ^ signed_string_of_int j
   196   | string_for_cst Unknown = "Unknown"
   197   | string_for_cst Unrep = "Unrep"
   198   | string_for_cst Suc = "Suc"
   199   | string_for_cst Add = "Add"
   200   | string_for_cst Subtract = "Subtract"
   201   | string_for_cst Multiply = "Multiply"
   202   | string_for_cst Divide = "Divide"
   203   | string_for_cst Gcd = "Gcd"
   204   | string_for_cst Lcm = "Lcm"
   205   | string_for_cst Fracs = "Fracs"
   206   | string_for_cst NormFrac = "NormFrac"
   207   | string_for_cst NatToInt = "NatToInt"
   208   | string_for_cst IntToNat = "IntToNat"
   209 
   210 fun string_for_op1 Not = "Not"
   211   | string_for_op1 Finite = "Finite"
   212   | string_for_op1 Converse = "Converse"
   213   | string_for_op1 Closure = "Closure"
   214   | string_for_op1 SingletonSet = "SingletonSet"
   215   | string_for_op1 IsUnknown = "IsUnknown"
   216   | string_for_op1 SafeThe = "SafeThe"
   217   | string_for_op1 First = "First"
   218   | string_for_op1 Second = "Second"
   219   | string_for_op1 Cast = "Cast"
   220 
   221 fun string_for_op2 All = "All"
   222   | string_for_op2 Exist = "Exist"
   223   | string_for_op2 Or = "Or"
   224   | string_for_op2 And = "And"
   225   | string_for_op2 Less = "Less"
   226   | string_for_op2 DefEq = "DefEq"
   227   | string_for_op2 Eq = "Eq"
   228   | string_for_op2 Triad = "Triad"
   229   | string_for_op2 Composition = "Composition"
   230   | string_for_op2 Apply = "Apply"
   231   | string_for_op2 Lambda = "Lambda"
   232 
   233 fun string_for_op3 Let = "Let"
   234   | string_for_op3 If = "If"
   235 
   236 fun basic_string_for_nut indent ctxt u =
   237   let
   238     val sub = basic_string_for_nut (indent + 1) ctxt
   239   in
   240     (if indent = 0 then "" else "\n" ^ implode (replicate (2 * indent) " ")) ^
   241     "(" ^
   242     (case u of
   243        Cst (c, T, R) =>
   244        "Cst " ^ string_for_cst c ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   245        string_for_rep R
   246      | Op1 (oper, T, R, u1) =>
   247        "Op1 " ^ string_for_op1 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   248        string_for_rep R ^ " " ^ sub u1
   249      | Op2 (oper, T, R, u1, u2) =>
   250        "Op2 " ^ string_for_op2 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   251        string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2
   252      | Op3 (oper, T, R, u1, u2, u3) =>
   253        "Op3 " ^ string_for_op3 oper ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   254        string_for_rep R ^ " " ^ sub u1 ^ " " ^ sub u2 ^ " " ^ sub u3
   255      | Tuple (T, R, us) =>
   256        "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
   257        implode (map sub us)
   258      | Construct (us', T, R, us) =>
   259        "Construct " ^ implode (map sub us') ^ " " ^
   260        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
   261        implode (map sub us)
   262      | BoundName (j, T, R, nick) =>
   263        "BoundName " ^ signed_string_of_int j ^ " " ^
   264        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
   265      | FreeName (s, T, R) =>
   266        "FreeName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   267        string_for_rep R
   268      | ConstName (s, T, R) =>
   269        "ConstName " ^ s ^ " " ^ Syntax.string_of_typ ctxt T ^ " " ^
   270        string_for_rep R
   271      | BoundRel ((n, j), T, R, nick) =>
   272        "BoundRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
   273        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
   274      | FreeRel ((n, j), T, R, nick) =>
   275        "FreeRel " ^ string_of_int n ^ "." ^ signed_string_of_int j ^ " " ^
   276        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
   277      | RelReg (j, T, R) =>
   278        "RelReg " ^ signed_string_of_int j ^ " " ^ Syntax.string_of_typ ctxt T ^
   279        " " ^ string_for_rep R
   280      | FormulaReg (j, T, R) =>
   281        "FormulaReg " ^ signed_string_of_int j ^ " " ^
   282        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R) ^
   283     ")"
   284   end
   285 val string_for_nut = basic_string_for_nut 0
   286 
   287 fun inline_nut (Op1 _) = false
   288   | inline_nut (Op2 _) = false
   289   | inline_nut (Op3 _) = false
   290   | inline_nut (Tuple (_, _, us)) = forall inline_nut us
   291   | inline_nut _ = true
   292 
   293 fun type_of (Cst (_, T, _)) = T
   294   | type_of (Op1 (_, T, _, _)) = T
   295   | type_of (Op2 (_, T, _, _, _)) = T
   296   | type_of (Op3 (_, T, _, _, _, _)) = T
   297   | type_of (Tuple (T, _, _)) = T
   298   | type_of (Construct (_, T, _, _)) = T
   299   | type_of (BoundName (_, T, _, _)) = T
   300   | type_of (FreeName (_, T, _)) = T
   301   | type_of (ConstName (_, T, _)) = T
   302   | type_of (BoundRel (_, T, _, _)) = T
   303   | type_of (FreeRel (_, T, _, _)) = T
   304   | type_of (RelReg (_, T, _)) = T
   305   | type_of (FormulaReg (_, T, _)) = T
   306 
   307 fun rep_of (Cst (_, _, R)) = R
   308   | rep_of (Op1 (_, _, R, _)) = R
   309   | rep_of (Op2 (_, _, R, _, _)) = R
   310   | rep_of (Op3 (_, _, R, _, _, _)) = R
   311   | rep_of (Tuple (_, R, _)) = R
   312   | rep_of (Construct (_, _, R, _)) = R
   313   | rep_of (BoundName (_, _, R, _)) = R
   314   | rep_of (FreeName (_, _, R)) = R
   315   | rep_of (ConstName (_, _, R)) = R
   316   | rep_of (BoundRel (_, _, R, _)) = R
   317   | rep_of (FreeRel (_, _, R, _)) = R
   318   | rep_of (RelReg (_, _, R)) = R
   319   | rep_of (FormulaReg (_, _, R)) = R
   320 
   321 fun nickname_of (BoundName (_, _, _, nick)) = nick
   322   | nickname_of (FreeName (s, _, _)) = s
   323   | nickname_of (ConstName (s, _, _)) = s
   324   | nickname_of (BoundRel (_, _, _, nick)) = nick
   325   | nickname_of (FreeRel (_, _, _, nick)) = nick
   326   | nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
   327 
   328 fun is_skolem_name u =
   329   space_explode name_sep (nickname_of u)
   330   |> exists (String.isPrefix skolem_prefix)
   331   handle NUT ("Nitpick_Nut.nickname_of", _) => false
   332 
   333 fun is_eval_name u =
   334   String.isPrefix eval_prefix (nickname_of u)
   335   handle NUT ("Nitpick_Nut.nickname_of", _) => false
   336 
   337 fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
   338   | is_Cst _ _ = false
   339 
   340 fun fold_nut f u =
   341   case u of
   342     Op1 (_, _, _, u1) => fold_nut f u1
   343   | Op2 (_, _, _, u1, u2) => fold_nut f u1 #> fold_nut f u2
   344   | Op3 (_, _, _, u1, u2, u3) => fold_nut f u1 #> fold_nut f u2 #> fold_nut f u3
   345   | Tuple (_, _, us) => fold (fold_nut f) us
   346   | Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
   347   | _ => f u
   348 
   349 fun map_nut f u =
   350   case u of
   351     Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
   352   | Op2 (oper, T, R, u1, u2) => Op2 (oper, T, R, map_nut f u1, map_nut f u2)
   353   | Op3 (oper, T, R, u1, u2, u3) =>
   354     Op3 (oper, T, R, map_nut f u1, map_nut f u2, map_nut f u3)
   355   | Tuple (T, R, us) => Tuple (T, R, map (map_nut f) us)
   356   | Construct (us', T, R, us) =>
   357     Construct (map (map_nut f) us', T, R, map (map_nut f) us)
   358   | _ => f u
   359 
   360 fun name_ord (BoundName (j1, _, _, _), BoundName (j2, _, _, _)) =
   361     int_ord (j1, j2)
   362   | name_ord (BoundName _, _) = LESS
   363   | name_ord (_, BoundName _) = GREATER
   364   | name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) =
   365     (case fast_string_ord (s1, s2) of
   366        EQUAL => Term_Ord.typ_ord (T1, T2)
   367      | ord => ord)
   368   | name_ord (FreeName _, _) = LESS
   369   | name_ord (_, FreeName _) = GREATER
   370   | name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) =
   371     (case fast_string_ord (s1, s2) of
   372        EQUAL => Term_Ord.typ_ord (T1, T2)
   373      | ord => ord)
   374   | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
   375 
   376 fun num_occurrences_in_nut needle_u stack_u =
   377   fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0
   378 val is_subnut_of = not_equal 0 oo num_occurrences_in_nut
   379 
   380 fun substitute_in_nut needle_u needle_u' =
   381   map_nut (fn u => if u = needle_u then needle_u' else u)
   382 
   383 val add_free_and_const_names =
   384   fold_nut (fn u => case u of
   385                       FreeName _ => apfst (insert (op =) u)
   386                     | ConstName _ => apsnd (insert (op =) u)
   387                     | _ => I)
   388 
   389 fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
   390   | modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
   391   | modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
   392   | modify_name_rep u _ = raise NUT ("Nitpick_Nut.modify_name_rep", [u])
   393 
   394 structure NameTable = Table(type key = nut val ord = name_ord)
   395 
   396 fun the_name table name =
   397   case NameTable.lookup table name of
   398     SOME u => u
   399   | NONE => raise NUT ("Nitpick_Nut.the_name", [name])
   400 
   401 fun the_rel table name =
   402   case the_name table name of
   403     FreeRel (x, _, _, _) => x
   404   | u => raise NUT ("Nitpick_Nut.the_rel", [u])
   405 
   406 fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
   407   | mk_fst (T, t) =
   408     let val res_T = fst (HOLogic.dest_prodT T) in
   409       (res_T, Const (@{const_name fst}, T --> res_T) $ t)
   410     end
   411 
   412 fun mk_snd (_, Const (@{const_name Pair}, T) $ _ $ t2) =
   413     (domain_type (range_type T), t2)
   414   | mk_snd (T, t) =
   415     let val res_T = snd (HOLogic.dest_prodT T) in
   416       (res_T, Const (@{const_name snd}, T --> res_T) $ t)
   417     end
   418 
   419 fun factorize (z as (Type (@{type_name prod}, _), _)) =
   420     maps factorize [mk_fst z, mk_snd z]
   421   | factorize z = [z]
   422 
   423 fun nut_from_term (hol_ctxt as {ctxt, ...}) eq =
   424   let
   425     fun aux eq ss Ts t =
   426       let
   427         val sub = aux Eq ss Ts
   428         val sub' = aux eq ss Ts
   429         fun sub_abs s T = aux eq (s :: ss) (T :: Ts)
   430         fun sub_equals T t1 t2 =
   431           let
   432             val (binder_Ts, body_T) = strip_type (domain_type T)
   433             val n = length binder_Ts
   434           in
   435             if eq = Eq andalso n > 0 then
   436               let
   437                 val t1 = incr_boundvars n t1
   438                 val t2 = incr_boundvars n t2
   439                 val xs = map Bound (n - 1 downto 0)
   440                 val equation = Const (@{const_name HOL.eq},
   441                                       body_T --> body_T --> bool_T)
   442                                    $ betapplys (t1, xs) $ betapplys (t2, xs)
   443                 val t =
   444                   fold_rev (fn T => fn (t, j) =>
   445                                (Const (@{const_name All}, T --> bool_T)
   446                                 $ Abs ("x" ^ nat_subscript j, T, t), j - 1))
   447                            binder_Ts (equation, n) |> fst
   448               in sub' t end
   449             else
   450               Op2 (eq, bool_T, Any, aux Eq ss Ts t1, aux Eq ss Ts t2)
   451           end
   452         fun do_quantifier quant s T t1 =
   453           let
   454             val bound_u = BoundName (length Ts, T, Any, s)
   455             val body_u = sub_abs s T t1
   456           in Op2 (quant, bool_T, Any, bound_u, body_u) end
   457         fun do_apply t0 ts =
   458           let
   459             val (ts', t2) = split_last ts
   460             val t1 = list_comb (t0, ts')
   461             val T1 = fastype_of1 (Ts, t1)
   462           in Op2 (Apply, pseudo_range_type T1, Any, sub t1, sub t2) end
   463         fun do_construct (x as (_, T)) ts =
   464           case num_binder_types T - length ts of
   465             0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
   466                                   o nth_sel_for_constr x)
   467                                 (~1 upto num_sels_for_constr_type T - 1),
   468                             body_type T, Any,
   469                             ts |> map (`(curry fastype_of1 Ts))
   470                                |> maps factorize |> map (sub o snd))
   471           | k => sub (eta_expand Ts t k)
   472       in
   473         case strip_comb t of
   474           (Const (@{const_name Pure.all}, _), [Abs (s, T, t1)]) =>
   475           do_quantifier All s T t1
   476         | (t0 as Const (@{const_name Pure.all}, _), [t1]) =>
   477           sub' (t0 $ eta_expand Ts t1 1)
   478         | (Const (@{const_name Pure.eq}, T), [t1, t2]) => sub_equals T t1 t2
   479         | (Const (@{const_name Pure.imp}, _), [t1, t2]) =>
   480           Op2 (Or, prop_T, Any, Op1 (Not, prop_T, Any, sub t1), sub' t2)
   481         | (Const (@{const_name Pure.conjunction}, _), [t1, t2]) =>
   482           Op2 (And, prop_T, Any, sub' t1, sub' t2)
   483         | (Const (@{const_name Trueprop}, _), [t1]) => sub' t1
   484         | (Const (@{const_name Not}, _), [t1]) =>
   485           (case sub t1 of
   486              Op1 (Not, _, _, u11) => u11
   487            | u1 => Op1 (Not, bool_T, Any, u1))
   488         | (Const (@{const_name False}, T), []) => Cst (False, T, Any)
   489         | (Const (@{const_name True}, T), []) => Cst (True, T, Any)
   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 Ex}, _), [Abs (s, T, t1)]) =>
   495           do_quantifier Exist s T t1
   496         | (t0 as Const (@{const_name Ex}, _), [t1]) =>
   497           sub' (t0 $ eta_expand Ts t1 1)
   498         | (Const (@{const_name HOL.eq}, T), [t1]) =>
   499           Op1 (SingletonSet, range_type T, Any, sub t1)
   500         | (Const (@{const_name HOL.eq}, T), [t1, t2]) => sub_equals T t1 t2
   501         | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
   502           Op2 (And, bool_T, Any, sub' t1, sub' t2)
   503         | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
   504           Op2 (Or, bool_T, Any, sub t1, sub t2)
   505         | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
   506           Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
   507         | (Const (@{const_name If}, T), [t1, t2, t3]) =>
   508           Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
   509         | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
   510           Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
   511                sub t1, sub_abs s T' t2)
   512         | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
   513           sub (t0 $ t1 $ eta_expand Ts t2 1)
   514         | (Const (@{const_name Pair}, T), [t1, t2]) =>
   515           Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
   516         | (Const (@{const_name fst}, T), [t1]) =>
   517           Op1 (First, range_type T, Any, sub t1)
   518         | (Const (@{const_name snd}, T), [t1]) =>
   519           Op1 (Second, range_type T, Any, sub t1)
   520         | (Const (@{const_name Set.member}, _), [t1, t2]) => do_apply t2 [t1]
   521         | (Const (@{const_name Collect}, _), [t1]) => sub t1
   522         | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
   523         | (Const (@{const_name converse}, T), [t1]) =>
   524           Op1 (Converse, range_type T, Any, sub t1)
   525         | (Const (@{const_name trancl}, T), [t1]) =>
   526           Op1 (Closure, range_type T, Any, sub t1)
   527         | (Const (@{const_name relcomp}, T), [t1, t2]) =>
   528           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   529         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   530           if is_built_in_const x then Cst (Suc, T, Any)
   531           else if is_constr ctxt x then do_construct x []
   532           else ConstName (s, T, Any)
   533         | (Const (@{const_name finite}, T), [t1]) =>
   534           (if is_finite_type hol_ctxt (domain_type T) then
   535              Cst (True, bool_T, Any)
   536            else case t1 of
   537              Const (@{const_name top}, _) => Cst (False, bool_T, Any)
   538            | _ => Op1 (Finite, bool_T, Any, sub t1))
   539         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
   540         | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
   541           if is_built_in_const x then Cst (Num 0, T, Any)
   542           else if is_constr ctxt x then do_construct x []
   543           else ConstName (s, T, Any)
   544         | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
   545           if is_built_in_const x then Cst (Num 1, T, Any)
   546           else ConstName (s, T, Any)
   547         | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
   548           if is_built_in_const x then Cst (Add, T, Any)
   549           else ConstName (s, T, Any)
   550         | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
   551           if is_built_in_const x then Cst (Subtract, T, Any)
   552           else ConstName (s, T, Any)
   553         | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
   554           if is_built_in_const x then Cst (Multiply, T, Any)
   555           else ConstName (s, T, Any)
   556         | (Const (x as (s as @{const_name Rings.divide}, T)), []) =>
   557           if is_built_in_const x then Cst (Divide, T, Any)
   558           else ConstName (s, T, Any)
   559         | (t0 as Const (x as (@{const_name ord_class.less}, _)),
   560            ts as [t1, t2]) =>
   561           if is_built_in_const x then
   562             Op2 (Less, bool_T, Any, sub t1, sub t2)
   563           else
   564             do_apply t0 ts
   565         | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
   566            ts as [t1, t2]) =>
   567           if is_built_in_const x then
   568             (* FIXME: find out if this case is necessary *)
   569             Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
   570           else
   571             do_apply t0 ts
   572         | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
   573         | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
   574         | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
   575           if is_built_in_const x then
   576             let val num_T = domain_type T in
   577               Op2 (Apply, num_T --> num_T, Any,
   578                    Cst (Subtract, num_T --> num_T --> num_T, Any),
   579                    Cst (Num 0, num_T, Any))
   580             end
   581           else
   582             ConstName (s, T, Any)
   583         | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
   584         | (Const (@{const_name is_unknown}, _), [t1]) =>
   585           Op1 (IsUnknown, bool_T, Any, sub t1)
   586         | (Const (@{const_name safe_The},
   587                   Type (@{type_name fun}, [_, T2])), [t1]) =>
   588           Op1 (SafeThe, T2, Any, sub t1)
   589         | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
   590         | (Const (@{const_name norm_frac}, T), []) =>
   591           Cst (NormFrac, T, Any)
   592         | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
   593           Cst (NatToInt, T, Any)
   594         | (Const (@{const_name of_nat},
   595                   T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
   596           Cst (NatToInt, T, Any)
   597         | (t0 as Const (x as (s, T)), ts) =>
   598           if is_constr ctxt x then
   599             do_construct x ts
   600           else if String.isPrefix numeral_prefix s then
   601             Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   602           else
   603             (case arity_of_built_in_const x of
   604                SOME n =>
   605                (case n - length ts of
   606                   0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
   607                 | k => if k > 0 then sub (eta_expand Ts t k)
   608                        else do_apply t0 ts)
   609              | NONE => if null ts then ConstName (s, T, Any)
   610                        else do_apply t0 ts)
   611         | (Free (s, T), []) => FreeName (s, T, Any)
   612         | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
   613         | (Bound j, []) =>
   614           BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
   615         | (Abs (s, T, t1), []) =>
   616           Op2 (Lambda, T --> fastype_of1 (T :: Ts, t1), Any,
   617                BoundName (length Ts, T, Any, s), sub_abs s T t1)
   618         | (t0, ts) => do_apply t0 ts
   619       end
   620   in aux eq [] [] end
   621 
   622 fun is_fully_representable_set u =
   623   not (is_opt_rep (rep_of u)) andalso
   624   case u of
   625     FreeName _ => true
   626   | Op1 (SingletonSet, _, _, _) => true
   627   | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
   628   | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
   629   | Op2 (oper, _, _, u1, _) =>
   630     if oper = Apply then
   631       case u1 of
   632         ConstName (s, _, _) =>
   633         is_sel_like_and_no_discr s orelse s = @{const_name set}
   634       | _ => false
   635     else
   636       false
   637   | _ => false
   638 
   639 fun rep_for_abs_fun scope T =
   640   let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
   641     Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
   642   end
   643 
   644 fun choose_rep_for_free_var scope pseudo_frees v (vs, table) =
   645   let
   646     val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then
   647                best_opt_set_rep_for_type
   648              else
   649                best_non_opt_set_rep_for_type) scope (type_of v)
   650     val v = modify_name_rep v R
   651   in (v :: vs, NameTable.update (v, R) table) end
   652 
   653 fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
   654                          (vs, table) =
   655   let
   656     val x as (s, T) = (nickname_of v, type_of v)
   657     val R = (if is_abs_fun ctxt x then
   658                rep_for_abs_fun
   659              else if is_rep_fun ctxt x then
   660                Func oo best_non_opt_symmetric_reps_for_fun_type
   661              else if total_consts orelse is_skolem_name v orelse
   662                      member (op =) [@{const_name bisim},
   663                                     @{const_name bisim_iterator_max}]
   664                             (original_name s) then
   665                best_non_opt_set_rep_for_type
   666              else if member (op =) [@{const_name set}, @{const_name distinct},
   667                                     @{const_name ord_class.less},
   668                                     @{const_name ord_class.less_eq}]
   669                             (original_name s) then
   670                best_set_rep_for_type
   671              else
   672                best_opt_set_rep_for_type) scope T
   673     val v = modify_name_rep v R
   674   in (v :: vs, NameTable.update (v, R) table) end
   675 
   676 fun choose_reps_for_free_vars scope pseudo_frees vs table =
   677   fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
   678 
   679 fun choose_reps_for_consts scope total_consts vs table =
   680   fold (choose_rep_for_const scope total_consts) vs ([], table)
   681 
   682 fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
   683                                       (x as (_, T)) n (vs, table) =
   684   let
   685     val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
   686     val R' = if n = ~1 orelse is_word_type (body_type T) orelse
   687                 (is_fun_type (range_type T') andalso
   688                  is_boolean_type (body_type T')) orelse
   689                 (is_set_type (body_type T')) then
   690                best_non_opt_set_rep_for_type scope T'
   691              else
   692                best_opt_set_rep_for_type scope T' |> unopt_rep
   693     val v = ConstName (s', T', R')
   694   in (v :: vs, NameTable.update (v, R') table) end
   695 
   696 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   697   fold_rev (choose_rep_for_nth_sel_for_constr scope x)
   698            (~1 upto num_sels_for_constr_type T - 1)
   699 
   700 fun choose_rep_for_sels_of_data_type _ ({deep = false, ...} : data_type_spec) = I
   701   | choose_rep_for_sels_of_data_type scope {constrs, ...} =
   702     fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   703 
   704 fun choose_reps_for_all_sels (scope as {data_types, ...}) =
   705   fold (choose_rep_for_sels_of_data_type scope) data_types o pair []
   706 
   707 val min_univ_card = 2
   708 
   709 fun choose_rep_for_bound_var scope v =
   710   let
   711     val R = best_one_rep_for_type scope (type_of v)
   712     val arity = arity_of_rep R
   713   in
   714     if arity > KK.max_arity min_univ_card then
   715       raise TOO_LARGE ("Nitpick_Nut.choose_rep_for_bound_var",
   716                        "arity " ^ string_of_int arity ^ " of bound variable \
   717                        \too large")
   718     else
   719       NameTable.update (v, R)
   720   end
   721 
   722 (* A nut is said to be constructive if whenever it evaluates to unknown in our
   723    three-valued logic, it would evaluate to an unrepresentable value ("Unrep")
   724    according to the HOL semantics. For example, "Suc n" is constructive if "n"
   725    is representable or "Unrep", because unknown implies "Unrep". *)
   726 fun is_constructive u =
   727   is_Cst Unrep u orelse
   728   (not (is_fun_or_set_type (type_of u)) andalso
   729    not (is_opt_rep (rep_of u))) orelse
   730   case u of
   731     Cst (Num _, _, _) => true
   732   | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
   733   | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
   734   | Op3 (If, _, _, u1, u2, u3) =>
   735     not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
   736   | Tuple (_, _, us) => forall is_constructive us
   737   | Construct (_, _, _, us) => forall is_constructive us
   738   | _ => false
   739 
   740 fun unknown_boolean T R =
   741   Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
   742        T, R)
   743 
   744 fun s_op1 oper T R u1 =
   745   ((if oper = Not then
   746       if is_Cst True u1 then Cst (False, T, R)
   747       else if is_Cst False u1 then Cst (True, T, R)
   748       else raise SAME ()
   749     else
   750       raise SAME ())
   751    handle SAME () => Op1 (oper, T, R, u1))
   752 
   753 fun s_op2 oper T R u1 u2 =
   754   ((case oper of
   755       All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
   756     | Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2
   757     | Or =>
   758       if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R)
   759       else if is_Cst False u1 then u2
   760       else if is_Cst False u2 then u1
   761       else raise SAME ()
   762     | And =>
   763       if exists (is_Cst False) [u1, u2] then Cst (False, T, unopt_rep R)
   764       else if is_Cst True u1 then u2
   765       else if is_Cst True u2 then u1
   766       else raise SAME ()
   767     | Eq =>
   768       (case apply2 (is_Cst Unrep) (u1, u2) of
   769          (true, true) => unknown_boolean T R
   770        | (false, false) => raise SAME ()
   771        | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()
   772               else Cst (False, T, Formula Neut))
   773     | Triad =>
   774       if is_Cst True u1 then u1
   775       else if is_Cst False u2 then u2
   776       else raise SAME ()
   777     | Apply =>
   778       if is_Cst Unrep u1 then
   779         Cst (Unrep, T, R)
   780       else if is_Cst Unrep u2 then
   781         if is_boolean_type T then
   782           if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
   783           else unknown_boolean T R
   784         else if is_constructive u1 then
   785           Cst (Unrep, T, R)
   786         else case u1 of
   787           Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
   788           Cst (Unrep, T, R)
   789         | _ => raise SAME ()
   790       else
   791         raise SAME ()
   792     | _ => raise SAME ())
   793    handle SAME () => Op2 (oper, T, R, u1, u2))
   794 
   795 fun s_op3 oper T R u1 u2 u3 =
   796   ((case oper of
   797       Let =>
   798       if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then
   799         substitute_in_nut u1 u2 u3
   800       else
   801         raise SAME ()
   802     | _ => raise SAME ())
   803    handle SAME () => Op3 (oper, T, R, u1, u2, u3))
   804 
   805 fun s_tuple T R us =
   806   if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
   807 
   808 fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
   809   | untuple f u = [f u]
   810 
   811 fun choose_reps_in_nut (scope as {card_assigns, bits, data_types, ofs, ...})
   812                        unsound table def =
   813   let
   814     val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
   815     fun bool_rep polar opt =
   816       if polar = Neut andalso opt then Opt bool_atom_R else Formula polar
   817     fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2
   818     fun triad_fn f = triad (f Pos) (f Neg)
   819     fun unrepify_nut_in_nut table def polar needle_u =
   820       let val needle_T = type_of needle_u in
   821         substitute_in_nut needle_u
   822             (Cst (if is_fun_or_set_type needle_T then Unknown
   823                   else Unrep, needle_T, Any))
   824         #> aux table def polar
   825       end
   826     and aux table def polar u =
   827       let
   828         val gsub = aux table
   829         val sub = gsub false Neut
   830       in
   831         case u of
   832           Cst (False, T, _) => Cst (False, T, Formula Neut)
   833         | Cst (True, T, _) => Cst (True, T, Formula Neut)
   834         | Cst (Num j, T, _) =>
   835           if is_word_type T then
   836             Cst (if is_twos_complement_representable bits j then Num j
   837                  else Unrep, T, best_opt_set_rep_for_type scope T)
   838           else
   839              let
   840                val (k, j0) = spec_of_type scope T
   841                val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
   842                          else j < k)
   843              in
   844                if ok then Cst (Num j, T, Atom (k, j0))
   845                else Cst (Unrep, T, Opt (Atom (k, j0)))
   846              end
   847         | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
   848           let val R = Atom (spec_of_type scope T1) in
   849             Cst (Suc, T, Func (R, Opt R))
   850           end
   851         | Cst (Fracs, T, _) =>
   852           Cst (Fracs, T, best_non_opt_set_rep_for_type scope T)
   853         | Cst (NormFrac, T, _) =>
   854           let val R1 = Atom (spec_of_type scope (domain_type T)) in
   855             Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
   856           end
   857         | Cst (cst, T, _) =>
   858           if cst = Unknown orelse cst = Unrep then
   859             case (is_boolean_type T, polar |> unsound ? flip_polarity) of
   860               (true, Pos) => Cst (False, T, Formula Pos)
   861             | (true, Neg) => Cst (True, T, Formula Neg)
   862             | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
   863           else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
   864                          cst then
   865             let
   866               val T1 = domain_type T
   867               val R1 = Atom (spec_of_type scope T1)
   868               val total = T1 = nat_T andalso
   869                           (cst = Subtract orelse cst = Divide orelse cst = Gcd)
   870             in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
   871           else if cst = NatToInt orelse cst = IntToNat then
   872             let
   873               val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
   874               val (ran_card, ran_j0) = spec_of_type scope (range_type T)
   875               val total = not (is_word_type (domain_type T)) andalso
   876                           (if cst = NatToInt then
   877                              max_int_for_card ran_card >= dom_card + 1
   878                            else
   879                              max_int_for_card dom_card < ran_card)
   880             in
   881               Cst (cst, T, Func (Atom (dom_card, dom_j0),
   882                                  Atom (ran_card, ran_j0) |> not total ? Opt))
   883             end
   884           else
   885             Cst (cst, T, best_set_rep_for_type scope T)
   886         | Op1 (Not, T, _, u1) =>
   887           (case gsub def (flip_polarity polar) u1 of
   888              Op2 (Triad, T, _, u11, u12) =>
   889              triad (s_op1 Not T (Formula Pos) u12)
   890                    (s_op1 Not T (Formula Neg) u11)
   891            | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
   892         | Op1 (IsUnknown, T, _, u1) =>
   893           let val u1 = sub u1 in
   894             if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
   895             else Cst (False, T, Formula Neut)
   896           end
   897         | Op1 (oper, T, _, u1) =>
   898           let
   899             val u1 = sub u1
   900             val R1 = rep_of u1
   901             val R = case oper of
   902                       Finite => bool_rep polar (is_opt_rep R1)
   903                     | _ => (if is_opt_rep R1 then best_opt_set_rep_for_type
   904                             else best_non_opt_set_rep_for_type) scope T
   905           in s_op1 oper T R u1 end
   906         | Op2 (Less, T, _, u1, u2) =>
   907           let
   908             val u1 = sub u1
   909             val u2 = sub u2
   910             val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
   911           in s_op2 Less T R u1 u2 end
   912         | Op2 (DefEq, T, _, u1, u2) =>
   913           s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
   914         | Op2 (Eq, T, _, u1, u2) =>
   915           let
   916             val u1' = sub u1
   917             val u2' = sub u2
   918             fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2'
   919             fun opt_opt_case () =
   920               if polar = Neut then
   921                 triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2')
   922               else
   923                 non_opt_case ()
   924             fun hybrid_case u =
   925               (* hackish optimization *)
   926               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
   927               else opt_opt_case ()
   928           in
   929             if unsound orelse polar = Neg orelse
   930                is_concrete_type data_types true (type_of u1) then
   931               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
   932                 (true, true) => opt_opt_case ()
   933               | (true, false) => hybrid_case u1'
   934               | (false, true) => hybrid_case u2'
   935               | (false, false) => non_opt_case ()
   936             else
   937               Cst (False, T, Formula Pos)
   938               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
   939           end
   940         | Op2 (Apply, T, _, u1, u2) =>
   941           let
   942             val u1 = sub u1
   943             val u2 = sub u2
   944             val T1 = type_of u1
   945             val R1 = rep_of u1
   946             val R2 = rep_of u2
   947             val opt =
   948               case (u1, is_opt_rep R2) of
   949                 (ConstName (@{const_name set}, _, _), false) => false
   950               | _ => exists is_opt_rep [R1, R2]
   951             val ran_R =
   952               if is_boolean_type T then
   953                 bool_rep polar opt
   954               else
   955                 lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T)
   956                                (unopt_rep R1)
   957                 |> opt ? opt_rep ofs T
   958           in s_op2 Apply T ran_R u1 u2 end
   959         | Op2 (Lambda, T, _, u1, u2) =>
   960           (case best_set_rep_for_type scope T of
   961              R as Func (R1, _) =>
   962              let
   963                val table' = NameTable.update (u1, R1) table
   964                val u1' = aux table' false Neut u1
   965                val u2' = aux table' false Neut u2
   966                val R =
   967                  if is_opt_rep (rep_of u2') then opt_rep ofs T R
   968                  else unopt_rep R
   969              in s_op2 Lambda T R u1' u2' end
   970            | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u]))
   971         | Op2 (oper, T, _, u1, u2) =>
   972           if oper = All orelse oper = Exist then
   973             let
   974               val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
   975                                 table
   976               val u1' = aux table' def polar u1
   977               val u2' = aux table' def polar u2
   978             in
   979               if polar = Neut andalso is_opt_rep (rep_of u2') then
   980                 triad_fn (fn polar => gsub def polar u)
   981               else
   982                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
   983                   if def orelse
   984                      (unsound andalso (polar = Pos) = (oper = All)) orelse
   985                      is_complete_type data_types true (type_of u1) then
   986                     quant_u
   987                   else
   988                     let
   989                       val connective = if oper = All then And else Or
   990                       val unrepified_u = unrepify_nut_in_nut table def polar
   991                                                              u1 u2
   992                     in
   993                       s_op2 connective T
   994                             (min_rep (rep_of quant_u) (rep_of unrepified_u))
   995                             quant_u unrepified_u
   996                     end
   997                 end
   998             end
   999           else if oper = Or orelse oper = And then
  1000             let
  1001               val u1' = gsub def polar u1
  1002               val u2' = gsub def polar u2
  1003             in
  1004               (if polar = Neut then
  1005                  case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
  1006                    (true, true) => triad_fn (fn polar => gsub def polar u)
  1007                  | (true, false) =>
  1008                    s_op2 oper T (Opt bool_atom_R)
  1009                          (triad_fn (fn polar => gsub def polar u1)) u2'
  1010                  | (false, true) =>
  1011                    s_op2 oper T (Opt bool_atom_R)
  1012                          u1' (triad_fn (fn polar => gsub def polar u2))
  1013                  | (false, false) => raise SAME ()
  1014                else
  1015                  raise SAME ())
  1016               handle SAME () => s_op2 oper T (Formula polar) u1' u2'
  1017             end
  1018           else
  1019             let
  1020               val u1 = sub u1
  1021               val u2 = sub u2
  1022               val R =
  1023                 best_non_opt_set_rep_for_type scope T
  1024                 |> exists (is_opt_rep o rep_of) [u1, u2] ? opt_rep ofs T
  1025             in s_op2 oper T R u1 u2 end
  1026         | Op3 (Let, T, _, u1, u2, u3) =>
  1027           let
  1028             val u2 = sub u2
  1029             val R2 = rep_of u2
  1030             val table' = NameTable.update (u1, R2) table
  1031             val u1 = modify_name_rep u1 R2
  1032             val u3 = aux table' false polar u3
  1033           in s_op3 Let T (rep_of u3) u1 u2 u3 end
  1034         | Op3 (If, T, _, u1, u2, u3) =>
  1035           let
  1036             val u1 = sub u1
  1037             val u2 = gsub def polar u2
  1038             val u3 = gsub def polar u3
  1039             val min_R = min_rep (rep_of u2) (rep_of u3)
  1040             val R = min_R |> is_opt_rep (rep_of u1) ? opt_rep ofs T
  1041           in s_op3 If T R u1 u2 u3 end
  1042         | Tuple (T, _, us) =>
  1043           let
  1044             val Rs = map (best_one_rep_for_type scope o type_of) us
  1045             val us = map sub us
  1046             val R' = Struct Rs
  1047                      |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T
  1048           in s_tuple T R' us end
  1049         | Construct (us', T, _, us) =>
  1050           let
  1051             val us = map sub us
  1052             val Rs = map rep_of us
  1053             val R = best_one_rep_for_type scope T
  1054             val {total, ...} =
  1055               constr_spec data_types (original_name (nickname_of (hd us')), T)
  1056             val opt = exists is_opt_rep Rs orelse not total
  1057           in Construct (map sub us', T, R |> opt ? Opt, us) end
  1058         | _ =>
  1059           let val u = modify_name_rep u (the_name table u) in
  1060             if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
  1061                not (is_opt_rep (rep_of u)) then
  1062               u
  1063             else
  1064               s_op1 Cast (type_of u) (Formula polar) u
  1065           end
  1066       end
  1067   in aux table def Pos end
  1068 
  1069 fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
  1070   | fresh_n_ary_index n ((m, j) :: xs) ys =
  1071     if m = n then (j, ys @ ((m, j + 1) :: xs))
  1072     else fresh_n_ary_index n xs ((m, j) :: ys)
  1073 
  1074 fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
  1075   let val (j, rels') = fresh_n_ary_index n rels [] in
  1076     (j, {rels = rels', vars = vars, formula_reg = formula_reg,
  1077          rel_reg = rel_reg})
  1078   end
  1079 
  1080 fun fresh_var n {rels, vars, formula_reg, rel_reg} =
  1081   let val (j, vars') = fresh_n_ary_index n vars [] in
  1082     (j, {rels = rels, vars = vars', formula_reg = formula_reg,
  1083          rel_reg = rel_reg})
  1084   end
  1085 
  1086 fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
  1087   (formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
  1088                  rel_reg = rel_reg})
  1089 
  1090 fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
  1091   (rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
  1092              rel_reg = rel_reg + 1})
  1093 
  1094 fun rename_plain_var v (ws, pool, table) =
  1095   let
  1096     val is_formula = (rep_of v = Formula Neut)
  1097     val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg
  1098     val (j, pool) = fresh pool
  1099     val constr = if is_formula then FormulaReg else RelReg
  1100     val w = constr (j, type_of v, rep_of v)
  1101   in (w :: ws, pool, NameTable.update (v, w) table) end
  1102 
  1103 fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2])
  1104                 us =
  1105     let val arity1 = arity_of_rep R1 in
  1106       Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
  1107                     shape_tuple T2 R2 (List.drop (us, arity1))])
  1108     end
  1109   | shape_tuple T (R as Vect (k, R')) us =
  1110     Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
  1111                      (chunk_list (length us div k) us))
  1112   | shape_tuple T _ [u] =
  1113     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
  1114   | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
  1115 
  1116 fun rename_n_ary_var rename_free v (ws, pool, table) =
  1117   let
  1118     val T = type_of v
  1119     val R = rep_of v
  1120     val arity = arity_of_rep R
  1121     val nick = nickname_of v
  1122     val (constr, fresh) = if rename_free then (FreeRel, fresh_rel)
  1123                           else (BoundRel, fresh_var)
  1124   in
  1125     if not rename_free andalso arity > 1 then
  1126       let
  1127         val atom_schema = atom_schema_of_rep R
  1128         val type_schema = type_schema_of_rep T R
  1129         val (js, pool) = funpow arity (fn (js, pool) =>
  1130                                           let val (j, pool) = fresh 1 pool in
  1131                                             (j :: js, pool)
  1132                                           end)
  1133                                 ([], pool)
  1134         val ws' = @{map 3} (fn j => fn x => fn T =>
  1135                            constr ((1, j), T, Atom x,
  1136                                    nick ^ " [" ^ string_of_int j ^ "]"))
  1137                        (rev js) atom_schema type_schema
  1138       in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
  1139     else
  1140       let
  1141         val (j, pool) =
  1142           case v of
  1143             ConstName _ =>
  1144             if is_sel_like_and_no_discr nick then
  1145               case domain_type T of
  1146                 @{typ "unsigned_bit word"} =>
  1147                 (snd unsigned_bit_word_sel_rel, pool)
  1148               | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
  1149               | _ => fresh arity pool
  1150             else
  1151               fresh arity pool
  1152           | _ => fresh arity pool
  1153         val w = constr ((arity, j), T, R, nick)
  1154       in (w :: ws, pool, NameTable.update (v, w) table) end
  1155   end
  1156 
  1157 fun rename_free_vars vs pool table =
  1158   let
  1159     val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
  1160   in (rev vs, pool, table) end
  1161 
  1162 fun rename_vars_in_nut pool table u =
  1163   case u of
  1164     Cst _ => u
  1165   | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
  1166   | Op2 (oper, T, R, u1, u2) =>
  1167     if oper = All orelse oper = Exist orelse oper = Lambda then
  1168       let
  1169         val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
  1170                                     ([], pool, table)
  1171       in
  1172         Op2 (oper, T, R, rename_vars_in_nut pool table u1,
  1173              rename_vars_in_nut pool table u2)
  1174       end
  1175     else
  1176       Op2 (oper, T, R, rename_vars_in_nut pool table u1,
  1177            rename_vars_in_nut pool table u2)
  1178   | Op3 (Let, T, R, u1, u2, u3) =>
  1179     if inline_nut u2 then
  1180       let
  1181         val u2 = rename_vars_in_nut pool table u2
  1182         val table = NameTable.update (u1, u2) table
  1183       in rename_vars_in_nut pool table u3 end
  1184     else
  1185       let
  1186         val bs = untuple I u1
  1187         val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
  1188       in
  1189         Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
  1190              rename_vars_in_nut pool table u2,
  1191              rename_vars_in_nut pool table' u3)
  1192       end
  1193   | Op3 (oper, T, R, u1, u2, u3) =>
  1194     Op3 (oper, T, R, rename_vars_in_nut pool table u1,
  1195          rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3)
  1196   | Tuple (T, R, us) => Tuple (T, R, map (rename_vars_in_nut pool table) us)
  1197   | Construct (us', T, R, us) =>
  1198     Construct (map (rename_vars_in_nut pool table) us', T, R,
  1199                map (rename_vars_in_nut pool table) us)
  1200   | _ => the_name table u
  1201 
  1202 end;