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