src/HOL/Tools/Nitpick/nitpick_nut.ML
author griff
Tue Apr 03 17:26:30 2012 +0900 (2012-04-03)
changeset 47433 07f4bf913230
parent 46115 ecab67f5a5c2
child 47753 792634c6679e
permissions -rw-r--r--
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
     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 {thy, ctxt, stds, ...}) 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 thy stds x then Cst (Suc, T, Any)
   529           else if is_constr ctxt stds 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 thy stds x then Cst (Num 0, T, Any)
   540           else if is_constr ctxt stds 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 thy stds 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 thy stds 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 thy stds 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 thy stds 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 thy stds 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 thy stds 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 thy stds x then
   568             (* FIXME: find out if this case is necessary *)
   569             Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
   570           else
   571             do_apply t0 ts
   572         | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
   573         | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
   574         | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
   575           if is_built_in_const thy stds x then
   576             let val num_T = domain_type T in
   577               Op2 (Apply, num_T --> num_T, Any,
   578                    Cst (Subtract, num_T --> num_T --> num_T, Any),
   579                    Cst (Num 0, num_T, Any))
   580             end
   581           else
   582             ConstName (s, T, Any)
   583         | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
   584         | (Const (@{const_name is_unknown}, _), [t1]) =>
   585           Op1 (IsUnknown, bool_T, Any, sub t1)
   586         | (Const (@{const_name safe_The},
   587                   Type (@{type_name fun}, [_, T2])), [t1]) =>
   588           Op1 (SafeThe, T2, Any, sub t1)
   589         | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
   590         | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
   591         | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
   592           Cst (NatToInt, T, Any)
   593         | (Const (@{const_name of_nat},
   594                   T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
   595           Cst (NatToInt, T, Any)
   596         | (t0 as Const (x as (s, T)), ts) =>
   597           if is_constr ctxt stds x then
   598             do_construct x ts
   599           else if String.isPrefix numeral_prefix s then
   600             Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
   601           else
   602             (case arity_of_built_in_const thy stds x of
   603                SOME n =>
   604                (case n - length ts of
   605                   0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
   606                 | k => if k > 0 then sub (eta_expand Ts t k)
   607                        else do_apply t0 ts)
   608              | NONE => if null ts then ConstName (s, T, Any)
   609                        else do_apply t0 ts)
   610         | (Free (s, T), []) => FreeName (s, T, Any)
   611         | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
   612         | (Bound j, []) =>
   613           BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
   614         | (Abs (s, T, t1), []) =>
   615           Op2 (Lambda, T --> fastype_of1 (T :: Ts, t1), Any,
   616                BoundName (length Ts, T, Any, s), sub_abs s T t1)
   617         | (t0, ts) => do_apply t0 ts
   618       end
   619   in aux eq [] [] end
   620 
   621 fun is_fully_representable_set u =
   622   not (is_opt_rep (rep_of u)) andalso
   623   case u of
   624     FreeName _ => true
   625   | Op1 (SingletonSet, _, _, _) => true
   626   | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
   627   | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
   628   | Op2 (oper, _, _, u1, _) =>
   629     if oper = Apply then
   630       case u1 of
   631         ConstName (s, _, _) =>
   632         is_sel_like_and_no_discr s orelse s = @{const_name set}
   633       | _ => false
   634     else
   635       false
   636   | _ => false
   637 
   638 fun rep_for_abs_fun scope T =
   639   let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
   640     Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
   641   end
   642 
   643 fun choose_rep_for_free_var scope pseudo_frees v (vs, table) =
   644   let
   645     val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then
   646                best_opt_set_rep_for_type
   647              else
   648                best_non_opt_set_rep_for_type) scope (type_of v)
   649     val v = modify_name_rep v R
   650   in (v :: vs, NameTable.update (v, R) table) end
   651 fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) total_consts v
   652                          (vs, table) =
   653   let
   654     val x as (s, T) = (nickname_of v, type_of v)
   655     val R = (if is_abs_fun ctxt x then
   656                rep_for_abs_fun
   657              else if is_rep_fun ctxt x then
   658                Func oo best_non_opt_symmetric_reps_for_fun_type
   659              else if total_consts orelse is_skolem_name v orelse
   660                      member (op =) [@{const_name bisim},
   661                                     @{const_name bisim_iterator_max}]
   662                             (original_name s) then
   663                best_non_opt_set_rep_for_type
   664              else if member (op =) [@{const_name set}, @{const_name distinct},
   665                                     @{const_name ord_class.less},
   666                                     @{const_name ord_class.less_eq}]
   667                             (original_name s) then
   668                best_set_rep_for_type
   669              else
   670                best_opt_set_rep_for_type) scope T
   671     val v = modify_name_rep v R
   672   in (v :: vs, NameTable.update (v, R) table) end
   673 
   674 fun choose_reps_for_free_vars scope pseudo_frees vs table =
   675   fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
   676 fun choose_reps_for_consts scope total_consts vs table =
   677   fold (choose_rep_for_const scope total_consts) vs ([], table)
   678 
   679 fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
   680                                       (x as (_, T)) n (vs, table) =
   681   let
   682     val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
   683     val R' = if n = ~1 orelse is_word_type (body_type T) orelse
   684                 (is_fun_type (range_type T') andalso
   685                  is_boolean_type (body_type T')) orelse
   686                 (is_set_type (body_type T')) then
   687                best_non_opt_set_rep_for_type scope T'
   688              else
   689                best_opt_set_rep_for_type scope T' |> unopt_rep
   690     val v = ConstName (s', T', R')
   691   in (v :: vs, NameTable.update (v, R') table) end
   692 fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
   693   fold_rev (choose_rep_for_nth_sel_for_constr scope x)
   694            (~1 upto num_sels_for_constr_type T - 1)
   695 fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
   696   | choose_rep_for_sels_of_datatype scope {constrs, ...} =
   697     fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
   698 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   699   fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
   700 
   701 val min_univ_card = 2
   702 
   703 fun choose_rep_for_bound_var scope v =
   704   let
   705     val R = best_one_rep_for_type scope (type_of v)
   706     val arity = arity_of_rep R
   707   in
   708     if arity > KK.max_arity min_univ_card then
   709       raise TOO_LARGE ("Nitpick_Nut.choose_rep_for_bound_var",
   710                        "arity " ^ string_of_int arity ^ " of bound variable \
   711                        \too large")
   712     else
   713       NameTable.update (v, R)
   714   end
   715 
   716 (* A nut is said to be constructive if whenever it evaluates to unknown in our
   717    three-valued logic, it would evaluate to an unrepresentable value ("Unrep")
   718    according to the HOL semantics. For example, "Suc n" is constructive if "n"
   719    is representable or "Unrep", because unknown implies "Unrep". *)
   720 fun is_constructive u =
   721   is_Cst Unrep u orelse
   722   (not (is_fun_or_set_type (type_of u)) andalso
   723    not (is_opt_rep (rep_of u))) orelse
   724   case u of
   725     Cst (Num _, _, _) => true
   726   | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
   727   | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
   728   | Op3 (If, _, _, u1, u2, u3) =>
   729     not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
   730   | Tuple (_, _, us) => forall is_constructive us
   731   | Construct (_, _, _, us) => forall is_constructive us
   732   | _ => false
   733 
   734 fun unknown_boolean T R =
   735   Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
   736        T, R)
   737 
   738 fun s_op1 oper T R u1 =
   739   ((if oper = Not then
   740       if is_Cst True u1 then Cst (False, T, R)
   741       else if is_Cst False u1 then Cst (True, T, R)
   742       else raise SAME ()
   743     else
   744       raise SAME ())
   745    handle SAME () => Op1 (oper, T, R, u1))
   746 fun s_op2 oper T R u1 u2 =
   747   ((case oper of
   748       All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
   749     | Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2
   750     | Or =>
   751       if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R)
   752       else if is_Cst False u1 then u2
   753       else if is_Cst False u2 then u1
   754       else raise SAME ()
   755     | And =>
   756       if exists (is_Cst False) [u1, u2] then Cst (False, T, unopt_rep R)
   757       else if is_Cst True u1 then u2
   758       else if is_Cst True u2 then u1
   759       else raise SAME ()
   760     | Eq =>
   761       (case pairself (is_Cst Unrep) (u1, u2) of
   762          (true, true) => unknown_boolean T R
   763        | (false, false) => raise SAME ()
   764        | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()
   765               else Cst (False, T, Formula Neut))
   766     | Triad =>
   767       if is_Cst True u1 then u1
   768       else if is_Cst False u2 then u2
   769       else raise SAME ()
   770     | Apply =>
   771       if is_Cst Unrep u1 then
   772         Cst (Unrep, T, R)
   773       else if is_Cst Unrep u2 then
   774         if is_boolean_type T then
   775           if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
   776           else unknown_boolean T R
   777         else if is_constructive u1 then
   778           Cst (Unrep, T, R)
   779         else case u1 of
   780           Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
   781           Cst (Unrep, T, R)
   782         | _ => raise SAME ()
   783       else
   784         raise SAME ()
   785     | _ => raise SAME ())
   786    handle SAME () => Op2 (oper, T, R, u1, u2))
   787 fun s_op3 oper T R u1 u2 u3 =
   788   ((case oper of
   789       Let =>
   790       if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then
   791         substitute_in_nut u1 u2 u3
   792       else
   793         raise SAME ()
   794     | _ => raise SAME ())
   795    handle SAME () => Op3 (oper, T, R, u1, u2, u3))
   796 fun s_tuple T R us =
   797   if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)
   798 
   799 fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
   800   | untuple f u = [f u]
   801 
   802 fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
   803                        unsound table def =
   804   let
   805     val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
   806     fun bool_rep polar opt =
   807       if polar = Neut andalso opt then Opt bool_atom_R else Formula polar
   808     fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2
   809     fun triad_fn f = triad (f Pos) (f Neg)
   810     fun unrepify_nut_in_nut table def polar needle_u =
   811       let val needle_T = type_of needle_u in
   812         substitute_in_nut needle_u
   813             (Cst (if is_fun_or_set_type needle_T then Unknown
   814                   else Unrep, needle_T, Any))
   815         #> aux table def polar
   816       end
   817     and aux table def polar u =
   818       let
   819         val gsub = aux table
   820         val sub = gsub false Neut
   821       in
   822         case u of
   823           Cst (False, T, _) => Cst (False, T, Formula Neut)
   824         | Cst (True, T, _) => Cst (True, T, Formula Neut)
   825         | Cst (Num j, T, _) =>
   826           if is_word_type T then
   827             Cst (if is_twos_complement_representable bits j then Num j
   828                  else Unrep, T, best_opt_set_rep_for_type scope T)
   829           else
   830              let
   831                val (k, j0) = spec_of_type scope T
   832                val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
   833                          else j < k)
   834              in
   835                if ok then Cst (Num j, T, Atom (k, j0))
   836                else Cst (Unrep, T, Opt (Atom (k, j0)))
   837              end
   838         | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
   839           let val R = Atom (spec_of_type scope T1) in
   840             Cst (Suc, T, Func (R, Opt R))
   841           end
   842         | Cst (Fracs, T, _) =>
   843           Cst (Fracs, T, best_non_opt_set_rep_for_type scope T)
   844         | Cst (NormFrac, T, _) =>
   845           let val R1 = Atom (spec_of_type scope (domain_type T)) in
   846             Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
   847           end
   848         | Cst (cst, T, _) =>
   849           if cst = Unknown orelse cst = Unrep then
   850             case (is_boolean_type T, polar |> unsound ? flip_polarity) of
   851               (true, Pos) => Cst (False, T, Formula Pos)
   852             | (true, Neg) => Cst (True, T, Formula Neg)
   853             | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
   854           else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
   855                          cst then
   856             let
   857               val T1 = domain_type T
   858               val R1 = Atom (spec_of_type scope T1)
   859               val total = T1 = nat_T andalso
   860                           (cst = Subtract orelse cst = Divide orelse cst = Gcd)
   861             in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
   862           else if cst = NatToInt orelse cst = IntToNat then
   863             let
   864               val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
   865               val (ran_card, ran_j0) = spec_of_type scope (range_type T)
   866               val total = not (is_word_type (domain_type T)) andalso
   867                           (if cst = NatToInt then
   868                              max_int_for_card ran_card >= dom_card + 1
   869                            else
   870                              max_int_for_card dom_card < ran_card)
   871             in
   872               Cst (cst, T, Func (Atom (dom_card, dom_j0),
   873                                  Atom (ran_card, ran_j0) |> not total ? Opt))
   874             end
   875           else
   876             Cst (cst, T, best_set_rep_for_type scope T)
   877         | Op1 (Not, T, _, u1) =>
   878           (case gsub def (flip_polarity polar) u1 of
   879              Op2 (Triad, T, _, u11, u12) =>
   880              triad (s_op1 Not T (Formula Pos) u12)
   881                    (s_op1 Not T (Formula Neg) u11)
   882            | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
   883         | Op1 (IsUnknown, T, _, u1) =>
   884           let val u1 = sub u1 in
   885             if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
   886             else Cst (False, T, Formula Neut)
   887           end
   888         | Op1 (oper, T, _, u1) =>
   889           let
   890             val u1 = sub u1
   891             val R1 = rep_of u1
   892             val R = case oper of
   893                       Finite => bool_rep polar (is_opt_rep R1)
   894                     | _ => (if is_opt_rep R1 then best_opt_set_rep_for_type
   895                             else best_non_opt_set_rep_for_type) scope T
   896           in s_op1 oper T R u1 end
   897         | Op2 (Less, T, _, u1, u2) =>
   898           let
   899             val u1 = sub u1
   900             val u2 = sub u2
   901             val R = bool_rep polar (exists (is_opt_rep o rep_of) [u1, u2])
   902           in s_op2 Less T R u1 u2 end
   903         | Op2 (Subset, T, _, u1, u2) =>
   904           let
   905             val u1 = sub u1
   906             val u2 = sub u2
   907             val opt = exists (is_opt_rep o rep_of) [u1, u2]
   908             val R = bool_rep polar opt
   909           in
   910             if is_opt_rep R then
   911               triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
   912             else if not opt orelse unsound orelse polar = Neg orelse
   913                     is_concrete_type datatypes true (type_of u1) then
   914               s_op2 Subset T R u1 u2
   915             else
   916               Cst (False, T, Formula Pos)
   917           end
   918         | Op2 (DefEq, T, _, u1, u2) =>
   919           s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)
   920         | Op2 (Eq, T, _, u1, u2) =>
   921           let
   922             val u1' = sub u1
   923             val u2' = sub u2
   924             fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2'
   925             fun opt_opt_case () =
   926               if polar = Neut then
   927                 triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2')
   928               else
   929                 non_opt_case ()
   930             fun hybrid_case u =
   931               (* hackish optimization *)
   932               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
   933               else opt_opt_case ()
   934           in
   935             if unsound orelse polar = Neg orelse
   936                is_concrete_type datatypes true (type_of u1) then
   937               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
   938                 (true, true) => opt_opt_case ()
   939               | (true, false) => hybrid_case u1'
   940               | (false, true) => hybrid_case u2'
   941               | (false, false) => non_opt_case ()
   942             else
   943               Cst (False, T, Formula Pos)
   944               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
   945           end
   946         | Op2 (Apply, T, _, u1, u2) =>
   947           let
   948             val u1 = sub u1
   949             val u2 = sub u2
   950             val T1 = type_of u1
   951             val R1 = rep_of u1
   952             val R2 = rep_of u2
   953             val opt =
   954               case (u1, is_opt_rep R2) of
   955                 (ConstName (@{const_name set}, _, _), false) => false
   956               | _ => exists is_opt_rep [R1, R2]
   957             val ran_R =
   958               if is_boolean_type T then
   959                 bool_rep polar opt
   960               else
   961                 lazy_range_rep ofs T1 (fn () => card_of_type card_assigns T)
   962                                (unopt_rep R1)
   963                 |> opt ? opt_rep ofs T
   964           in s_op2 Apply T ran_R u1 u2 end
   965         | Op2 (Lambda, T, _, u1, u2) =>
   966           (case best_set_rep_for_type scope T of
   967              R as Func (R1, _) =>
   968              let
   969                val table' = NameTable.update (u1, R1) table
   970                val u1' = aux table' false Neut u1
   971                val u2' = aux table' false Neut u2
   972                val R =
   973                  if is_opt_rep (rep_of u2') orelse
   974                     (pseudo_range_type T = bool_T andalso
   975                      not (is_Cst False (unrepify_nut_in_nut table false Neut
   976                                                             u1 u2))) then
   977                    opt_rep ofs T R
   978                  else
   979                    unopt_rep R
   980              in s_op2 Lambda T R u1' u2' end
   981            | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u]))
   982         | Op2 (oper, T, _, u1, u2) =>
   983           if oper = All orelse oper = Exist then
   984             let
   985               val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
   986                                 table
   987               val u1' = aux table' def polar u1
   988               val u2' = aux table' def polar u2
   989             in
   990               if polar = Neut andalso is_opt_rep (rep_of u2') then
   991                 triad_fn (fn polar => gsub def polar u)
   992               else
   993                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
   994                   if def orelse
   995                      (unsound andalso (polar = Pos) = (oper = All)) orelse
   996                      is_complete_type datatypes true (type_of u1) then
   997                     quant_u
   998                   else
   999                     let
  1000                       val connective = if oper = All then And else Or
  1001                       val unrepified_u = unrepify_nut_in_nut table def polar
  1002                                                              u1 u2
  1003                     in
  1004                       s_op2 connective T
  1005                             (min_rep (rep_of quant_u) (rep_of unrepified_u))
  1006                             quant_u unrepified_u
  1007                     end
  1008                 end
  1009             end
  1010           else if oper = Or orelse oper = And then
  1011             let
  1012               val u1' = gsub def polar u1
  1013               val u2' = gsub def polar u2
  1014             in
  1015               (if polar = Neut then
  1016                  case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
  1017                    (true, true) => triad_fn (fn polar => gsub def polar u)
  1018                  | (true, false) =>
  1019                    s_op2 oper T (Opt bool_atom_R)
  1020                          (triad_fn (fn polar => gsub def polar u1)) u2'
  1021                  | (false, true) =>
  1022                    s_op2 oper T (Opt bool_atom_R)
  1023                          u1' (triad_fn (fn polar => gsub def polar u2))
  1024                  | (false, false) => raise SAME ()
  1025                else
  1026                  raise SAME ())
  1027               handle SAME () => s_op2 oper T (Formula polar) u1' u2'
  1028             end
  1029           else
  1030             let
  1031               val u1 = sub u1
  1032               val u2 = sub u2
  1033               val R =
  1034                 best_non_opt_set_rep_for_type scope T
  1035                 |> exists (is_opt_rep o rep_of) [u1, u2] ? opt_rep ofs T
  1036             in s_op2 oper T R u1 u2 end
  1037         | Op3 (Let, T, _, u1, u2, u3) =>
  1038           let
  1039             val u2 = sub u2
  1040             val R2 = rep_of u2
  1041             val table' = NameTable.update (u1, R2) table
  1042             val u1 = modify_name_rep u1 R2
  1043             val u3 = aux table' false polar u3
  1044           in s_op3 Let T (rep_of u3) u1 u2 u3 end
  1045         | Op3 (If, T, _, u1, u2, u3) =>
  1046           let
  1047             val u1 = sub u1
  1048             val u2 = gsub def polar u2
  1049             val u3 = gsub def polar u3
  1050             val min_R = min_rep (rep_of u2) (rep_of u3)
  1051             val R = min_R |> is_opt_rep (rep_of u1) ? opt_rep ofs T
  1052           in s_op3 If T R u1 u2 u3 end
  1053         | Tuple (T, _, us) =>
  1054           let
  1055             val Rs = map (best_one_rep_for_type scope o type_of) us
  1056             val us = map sub us
  1057             val R' = Struct Rs
  1058                      |> exists (is_opt_rep o rep_of) us ? opt_rep ofs T
  1059           in s_tuple T R' us end
  1060         | Construct (us', T, _, us) =>
  1061           let
  1062             val us = map sub us
  1063             val Rs = map rep_of us
  1064             val R = best_one_rep_for_type scope T
  1065             val {total, ...} =
  1066               constr_spec datatypes (original_name (nickname_of (hd us')), T)
  1067             val opt = exists is_opt_rep Rs orelse not total
  1068           in Construct (map sub us', T, R |> opt ? Opt, us) end
  1069         | _ =>
  1070           let val u = modify_name_rep u (the_name table u) in
  1071             if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
  1072                not (is_opt_rep (rep_of u)) then
  1073               u
  1074             else
  1075               s_op1 Cast (type_of u) (Formula polar) u
  1076           end
  1077       end
  1078   in aux table def Pos end
  1079 
  1080 fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
  1081   | fresh_n_ary_index n ((m, j) :: xs) ys =
  1082     if m = n then (j, ys @ ((m, j + 1) :: xs))
  1083     else fresh_n_ary_index n xs ((m, j) :: ys)
  1084 fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
  1085   let val (j, rels') = fresh_n_ary_index n rels [] in
  1086     (j, {rels = rels', vars = vars, formula_reg = formula_reg,
  1087          rel_reg = rel_reg})
  1088   end
  1089 fun fresh_var n {rels, vars, formula_reg, rel_reg} =
  1090   let val (j, vars') = fresh_n_ary_index n vars [] in
  1091     (j, {rels = rels, vars = vars', formula_reg = formula_reg,
  1092          rel_reg = rel_reg})
  1093   end
  1094 fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
  1095   (formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
  1096                  rel_reg = rel_reg})
  1097 fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
  1098   (rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
  1099              rel_reg = rel_reg + 1})
  1100 
  1101 fun rename_plain_var v (ws, pool, table) =
  1102   let
  1103     val is_formula = (rep_of v = Formula Neut)
  1104     val fresh = if is_formula then fresh_formula_reg else fresh_rel_reg
  1105     val (j, pool) = fresh pool
  1106     val constr = if is_formula then FormulaReg else RelReg
  1107     val w = constr (j, type_of v, rep_of v)
  1108   in (w :: ws, pool, NameTable.update (v, w) table) end
  1109 
  1110 fun shape_tuple (T as Type (@{type_name prod}, [T1, T2])) (R as Struct [R1, R2])
  1111                 us =
  1112     let val arity1 = arity_of_rep R1 in
  1113       Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
  1114                     shape_tuple T2 R2 (List.drop (us, arity1))])
  1115     end
  1116   | shape_tuple T (R as Vect (k, R')) us =
  1117     Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
  1118                      (batch_list (length us div k) us))
  1119   | shape_tuple T _ [u] =
  1120     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
  1121   | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
  1122 
  1123 fun rename_n_ary_var rename_free v (ws, pool, table) =
  1124   let
  1125     val T = type_of v
  1126     val R = rep_of v
  1127     val arity = arity_of_rep R
  1128     val nick = nickname_of v
  1129     val (constr, fresh) = if rename_free then (FreeRel, fresh_rel)
  1130                           else (BoundRel, fresh_var)
  1131   in
  1132     if not rename_free andalso arity > 1 then
  1133       let
  1134         val atom_schema = atom_schema_of_rep R
  1135         val type_schema = type_schema_of_rep T R
  1136         val (js, pool) = funpow arity (fn (js, pool) =>
  1137                                           let val (j, pool) = fresh 1 pool in
  1138                                             (j :: js, pool)
  1139                                           end)
  1140                                 ([], pool)
  1141         val ws' = map3 (fn j => fn x => fn T =>
  1142                            constr ((1, j), T, Atom x,
  1143                                    nick ^ " [" ^ string_of_int j ^ "]"))
  1144                        (rev js) atom_schema type_schema
  1145       in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
  1146     else
  1147       let
  1148         val (j, pool) =
  1149           case v of
  1150             ConstName _ =>
  1151             if is_sel_like_and_no_discr nick then
  1152               case domain_type T of
  1153                 @{typ "unsigned_bit word"} =>
  1154                 (snd unsigned_bit_word_sel_rel, pool)
  1155               | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
  1156               | _ => fresh arity pool
  1157             else
  1158               fresh arity pool
  1159           | _ => fresh arity pool
  1160         val w = constr ((arity, j), T, R, nick)
  1161       in (w :: ws, pool, NameTable.update (v, w) table) end
  1162   end
  1163 
  1164 fun rename_free_vars vs pool table =
  1165   let
  1166     val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
  1167   in (rev vs, pool, table) end
  1168 
  1169 fun rename_vars_in_nut pool table u =
  1170   case u of
  1171     Cst _ => u
  1172   | Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
  1173   | Op2 (oper, T, R, u1, u2) =>
  1174     if oper = All orelse oper = Exist orelse oper = Lambda then
  1175       let
  1176         val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
  1177                                     ([], pool, table)
  1178       in
  1179         Op2 (oper, T, R, rename_vars_in_nut pool table u1,
  1180              rename_vars_in_nut pool table u2)
  1181       end
  1182     else
  1183       Op2 (oper, T, R, rename_vars_in_nut pool table u1,
  1184            rename_vars_in_nut pool table u2)
  1185   | Op3 (Let, T, R, u1, u2, u3) =>
  1186     if inline_nut u2 then
  1187       let
  1188         val u2 = rename_vars_in_nut pool table u2
  1189         val table = NameTable.update (u1, u2) table
  1190       in rename_vars_in_nut pool table u3 end
  1191     else
  1192       let
  1193         val bs = untuple I u1
  1194         val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
  1195       in
  1196         Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
  1197              rename_vars_in_nut pool table u2,
  1198              rename_vars_in_nut pool table' u3)
  1199       end
  1200   | Op3 (oper, T, R, u1, u2, u3) =>
  1201     Op3 (oper, T, R, rename_vars_in_nut pool table u1,
  1202          rename_vars_in_nut pool table u2, rename_vars_in_nut pool table u3)
  1203   | Tuple (T, R, us) => Tuple (T, R, map (rename_vars_in_nut pool table) us)
  1204   | Construct (us', T, R, us) =>
  1205     Construct (map (rename_vars_in_nut pool table) us', T, R,
  1206                map (rename_vars_in_nut pool table) us)
  1207   | _ => the_name table u
  1208 
  1209 end;