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