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