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