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