src/HOL/Tools/Nitpick/nitpick_kodkod.ML
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41047 9f1d3fcef1ca
parent 41045 2a41709f34c1
child 41049 0edd245892ed
permissions -rw-r--r--
simplified special handling of set products
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33892
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_kodkod.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
Kodkod problem generator part of Kodkod.
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_KODKOD =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34982
diff changeset
    10
  type hol_context = Nitpick_HOL.hol_context
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    11
  type datatype_spec = Nitpick_Scope.datatype_spec
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    12
  type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    13
  type nut = Nitpick_Nut.nut
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    15
  structure NameTable : TABLE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
  val univ_card :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
    int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    19
  val check_bits : int -> Kodkod.formula -> unit
38182
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
    20
  val check_arity : string -> int -> int -> unit
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    21
  val kk_tuple : bool -> int -> int list -> Kodkod.tuple
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    22
  val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    23
  val sequential_int_bounds : int -> Kodkod.int_bound list
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
    24
  val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    25
  val bounds_and_axioms_for_built_in_rels_in_formulas :
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
    26
    bool -> int -> int -> int -> int -> Kodkod.formula list
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    27
    -> Kodkod.bound list * Kodkod.formula list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
  val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
  val bound_for_sel_rel :
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    30
    Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    31
  val merge_bounds : Kodkod.bound list -> Kodkod.bound list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
  val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    33
  val declarative_axioms_for_datatypes :
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    34
    hol_context -> bool -> int -> int -> int Typtab.table -> kodkod_constrs
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    35
    -> nut NameTable.table -> datatype_spec list -> Kodkod.formula list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    36
  val kodkod_formula_from_nut :
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
    37
    int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    38
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    39
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    40
structure Nitpick_Kodkod : NITPICK_KODKOD =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    41
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    43
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    44
open Nitpick_HOL
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    45
open Nitpick_Scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    46
open Nitpick_Peephole
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    47
open Nitpick_Rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
    48
open Nitpick_Nut
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    50
structure KK = Kodkod
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    51
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
    52
fun pull x xs = x :: filter_out (curry (op =) x) xs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    53
38196
51a1bfef9de2 renamed internal function
blanchet
parents: 38195
diff changeset
    54
fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
51a1bfef9de2 renamed internal function
blanchet
parents: 38195
diff changeset
    55
                         : datatype_spec) = true
51a1bfef9de2 renamed internal function
blanchet
parents: 38195
diff changeset
    56
  | is_datatype_acyclic _ = false
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    57
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    58
fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    59
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
fun univ_card nat_card int_card main_j0 bounds formula =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    61
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    62
    fun rel_expr_func r k =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    63
      Int.max (k, case r of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    64
                    KK.Atom j => j + 1
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    65
                  | KK.AtomSeq (k', j0) => j0 + k'
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    66
                  | _ => 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    67
    fun tuple_func t k =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
      case t of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    69
        KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    70
      | _ => k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    71
    fun tuple_set_func ts k =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    72
      Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    73
    val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    74
                  int_expr_func = K I}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    75
    val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func}
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    76
    val card = fold (KK.fold_bound expr_F tuple_F) bounds 1
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    77
               |> KK.fold_formula expr_F formula
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    78
  in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    79
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    80
fun check_bits bits formula =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    81
  let
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    82
    fun int_expr_func (KK.Num k) () =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    83
        if is_twos_complement_representable bits k then
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    84
          ()
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    85
        else
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    86
          raise TOO_SMALL ("Nitpick_Kodkod.check_bits",
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    87
                           "\"bits\" value " ^ string_of_int bits ^
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    88
                           " too small for problem")
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    89
      | int_expr_func _ () = ()
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    90
    val expr_F = {formula_func = K I, rel_expr_func = K I,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    91
                  int_expr_func = int_expr_func}
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    92
  in KK.fold_formula expr_F formula () end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
38182
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
    94
fun check_arity guilty_party univ_card n =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    95
  if n > KK.max_arity univ_card then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
    96
    raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
38182
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
    97
                     "arity " ^ string_of_int n ^
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
    98
                     (if guilty_party = "" then
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
    99
                        ""
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
   100
                      else
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
   101
                        " of Kodkod relation associated with " ^
41045
2a41709f34c1 use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
blanchet
parents: 39898
diff changeset
   102
                        quote (original_name guilty_party)) ^
38182
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
   103
                     " too large for universe of cardinality " ^
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
   104
                     string_of_int univ_card)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   105
  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
    ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   107
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   108
fun kk_tuple debug univ_card js =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
  if debug then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   110
    KK.Tuple js
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   111
  else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   112
    KK.TupleIndex (length js,
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   113
                   fold (fn j => fn accum => accum * univ_card + j) js 0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   114
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   115
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   118
val single_atom = KK.TupleSet o single o KK.Tuple o single
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   119
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   120
fun pow_of_two_int_bounds bits j0 =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   121
  let
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   122
    fun aux 0  _ _ = []
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
   123
      | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   124
      | aux iter pow_of_two j =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   125
        (SOME pow_of_two, [single_atom j]) ::
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   126
        aux (iter - 1) (2 * pow_of_two) (j + 1)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   127
  in aux (bits + 1) 1 j0 end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   128
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   129
fun built_in_rels_in_formulas formulas =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   130
  let
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   131
    fun rel_expr_func (KK.Rel (x as (_, j))) =
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   132
        (j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   133
         x <> signed_bit_word_sel_rel)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   134
        ? insert (op =) x
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   135
      | rel_expr_func _ = I
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   136
    val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
                  int_expr_func = K I}
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   138
  in fold (KK.fold_formula expr_F) formulas [] end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   139
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
val max_table_size = 65536
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
fun check_table_size k =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
  if k > max_table_size then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   144
    raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   145
                     "precomputed table too large (" ^ string_of_int k ^ ")")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   146
  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   147
    ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   148
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   149
fun tabulate_func1 debug univ_card (k, j0) f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   150
  (check_table_size k;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   151
   map_filter (fn j1 => let val j2 = f j1 in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   152
                          if j2 >= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   153
                            SOME (kk_tuple debug univ_card [j1 + j0, j2 + j0])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   154
                          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   155
                            NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   156
                        end) (index_seq 0 k))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   157
fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   158
  (check_table_size (k * k);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   159
   map_filter (fn j => let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   160
                         val j1 = j div k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
                         val j2 = j - j1 * k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   162
                         val j3 = f (j1, j2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   163
                       in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   164
                         if j3 >= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   165
                           SOME (kk_tuple debug univ_card
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   166
                                          [j1 + j0, j2 + j0, j3 + res_j0])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   167
                         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   168
                           NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   169
                       end) (index_seq 0 (k * k)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   170
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
  (check_table_size (k * k);
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
   map_filter (fn j => let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   173
                         val j1 = j div k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
                         val j2 = j - j1 * k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   175
                         val (j3, j4) = f (j1, j2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   176
                       in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   177
                         if j3 >= 0 andalso j4 >= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
                           SOME (kk_tuple debug univ_card
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
                                          [j1 + j0, j2 + j0, j3 + res_j0,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
                                           j4 + res_j0])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
                         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   182
                           NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   183
                       end) (index_seq 0 (k * k)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   184
fun tabulate_nat_op2 debug univ_card (k, j0) f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   185
  tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   186
fun tabulate_int_op2 debug univ_card (k, j0) f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   187
  tabulate_op2 debug univ_card (k, j0) j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   188
               (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   189
fun tabulate_int_op2_2 debug univ_card (k, j0) f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   190
  tabulate_op2_2 debug univ_card (k, j0) j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   191
                 (pairself (atom_for_int (k, 0)) o f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   192
                  o pairself (int_for_atom (k, 0)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   193
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
fun isa_div (m, n) = m div n handle General.Div => 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   195
fun isa_mod (m, n) = m mod n handle General.Div => m
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   196
fun isa_gcd (m, 0) = m
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   197
  | isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   198
fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
val isa_zgcd = isa_gcd o pairself abs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   200
fun isa_norm_frac (m, n) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
  if n < 0 then isa_norm_frac (~m, ~n)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   202
  else if m = 0 orelse n = 0 then (0, 1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   203
  else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   204
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   205
fun tabulate_built_in_rel debug univ_card nat_card int_card j0
38124
6538e25cf5dd started implementation of custom sym break
blanchet
parents: 38121
diff changeset
   206
                          (x as (n, _)) =
38182
747f8077b09a more helpful message
blanchet
parents: 38164
diff changeset
   207
  (check_arity "" univ_card n;
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   208
   if x = not3_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   209
     ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   210
   else if x = suc_rel then
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   211
     ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   212
                            (Integer.add 1))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   213
   else if x = nat_add_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   214
     ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   215
   else if x = int_add_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   216
     ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   217
   else if x = nat_subtract_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   218
     ("nat_subtract",
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33631
diff changeset
   219
      tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   220
   else if x = int_subtract_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
     ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   222
   else if x = nat_multiply_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
     ("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   224
   else if x = int_multiply_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   225
     ("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   226
   else if x = nat_divide_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
     ("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   228
   else if x = int_divide_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   229
     ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   230
   else if x = nat_less_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   231
     ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35312
diff changeset
   232
                                   (int_from_bool o op <))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   233
   else if x = int_less_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   234
     ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35312
diff changeset
   235
                                   (int_from_bool o op <))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   236
   else if x = gcd_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   237
     ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   238
   else if x = lcm_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
     ("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   240
   else if x = norm_frac_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   241
     ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
                                      isa_norm_frac)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   243
   else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   244
     raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   246
fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   247
                           (x as (n, j)) =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   248
  if n = 2 andalso j <= suc_rels_base then
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   249
    let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   250
      ([(x, "suc")],
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   251
       if tabulate then
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   252
         [KK.TupleSet (tabulate_func1 debug univ_card (k - 1, j0)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   253
                       (Integer.add 1))]
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   254
       else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   255
         [KK.TupleSet [], tuple_set_from_atom_schema [y, y]])
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   256
    end
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   257
  else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   258
    let
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   259
      val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   260
                                             main_j0 x
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   261
    in ([(x, nick)], [KK.TupleSet ts]) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   262
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   263
fun axiom_for_built_in_rel (x as (n, j)) =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   264
  if n = 2 andalso j <= suc_rels_base then
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   265
    let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
38160
d04aceff43cf fix minor bug in sym breaking
blanchet
parents: 38127
diff changeset
   266
      if tabulate then
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   267
        NONE
38160
d04aceff43cf fix minor bug in sym breaking
blanchet
parents: 38127
diff changeset
   268
      else if k < 2 then
d04aceff43cf fix minor bug in sym breaking
blanchet
parents: 38127
diff changeset
   269
        SOME (KK.No (KK.Rel x))
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   270
      else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   271
        SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   272
    end
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   273
  else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   274
    NONE
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   275
fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   276
                                                    int_card main_j0 formulas =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   277
  let val rels = built_in_rels_in_formulas formulas in
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   278
    (map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0)
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   279
         rels,
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   280
     map_filter axiom_for_built_in_rel rels)
39316
b6c4385ab400 change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents: 38212
diff changeset
   281
  end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   282
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   283
fun bound_comment ctxt debug nick T R =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   284
  short_name nick ^
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
   285
  (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
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
   286
  " : " ^ string_for_rep R
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   287
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   288
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   289
    ([(x, bound_comment ctxt debug nick T R)],
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
     if nick = @{const_name bisim_iterator_max} then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   291
       case R of
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   292
         Atom (k, j0) => [single_atom (k - 1 + j0)]
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   293
       | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   294
     else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   295
       [KK.TupleSet [], upper_bound_for_rep R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   296
  | bound_for_plain_rel _ _ u =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   297
    raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   298
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   299
fun bound_for_sel_rel ctxt debug dtypes
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
   300
        (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
   301
                  R as Func (Atom (_, j0), R2), nick)) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   302
    let
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   303
      val {delta, epsilon, exclusive, explicit_max, ...} =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   304
        constr_spec dtypes (original_name nick, T1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   305
    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   306
      ([(x, bound_comment ctxt debug nick T R)],
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   307
       if explicit_max = 0 then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   308
         [KK.TupleSet []]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
       else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   310
         let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
           if R2 = Formula Neut then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   312
             [ts] |> not exclusive ? cons (KK.TupleSet [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   313
           else
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   314
             [KK.TupleSet [],
35178
29a0e3be0be1 minor fixes to Nitpick
blanchet
parents: 35177
diff changeset
   315
              if T1 = T2 andalso epsilon > delta andalso
38196
51a1bfef9de2 renamed internal function
blanchet
parents: 38195
diff changeset
   316
                 is_datatype_acyclic (the (datatype_spec dtypes T1)) then
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   317
                index_seq delta (epsilon - delta)
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   318
                |> map (fn j =>
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   319
                           KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   320
                                            KK.TupleAtomSeq (j, j0)))
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   321
                |> foldl1 KK.TupleUnion
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   322
              else
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
   323
                KK.TupleProduct (ts, upper_bound_for_rep R2)]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   324
         end)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   325
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   326
  | bound_for_sel_rel _ _ _ u =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   327
    raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   329
fun merge_bounds bs =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   330
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   331
    fun arity (zs, _) = fst (fst (hd zs))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   332
    fun add_bound ds b [] = List.revAppend (ds, [b])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   333
      | add_bound ds b (c :: cs) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   334
        if arity b = arity c andalso snd b = snd c then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   335
          List.revAppend (ds, (fst c @ fst b, snd c) :: cs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   336
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   337
          add_bound (c :: ds) b cs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   338
  in fold (add_bound []) bs [] end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   339
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   340
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   341
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   342
val singleton_from_combination = foldl1 KK.Product o map KK.Atom
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   343
fun all_singletons_for_rep R =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   344
  if is_lone_rep R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   345
    all_combinations_for_rep R |> map singleton_from_combination
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   346
  else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   347
    raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   348
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   349
fun unpack_products (KK.Product (r1, r2)) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   350
    unpack_products r1 @ unpack_products r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   351
  | unpack_products r = [r]
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   352
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   353
  | unpack_joins r = [r]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   354
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   355
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   356
fun full_rel_for_rep R =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   357
  case atom_schema_of_rep R of
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   358
    [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   359
  | schema => foldl1 KK.Product (map KK.AtomSeq schema)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   360
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   361
fun decls_for_atom_schema j0 schema =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   362
  map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   363
       (index_seq j0 (length schema)) schema
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
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   366
                     R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   367
  let val body_R = body_rep R in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   368
    if is_lone_rep body_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   369
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   370
        val binder_schema = atom_schema_of_reps (binder_reps R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   371
        val body_schema = atom_schema_of_rep body_R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   372
        val one = is_one_rep body_R
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   373
        val opt_x = case r of KK.Rel x => SOME x | _ => NONE
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   374
      in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
   375
        if opt_x <> NONE andalso length binder_schema = 1 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
   376
           length body_schema = 1 then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   377
          (if one then KK.Function else KK.Functional)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   378
              (the opt_x, KK.AtomSeq (hd binder_schema),
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   379
               KK.AtomSeq (hd body_schema))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   380
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   381
          let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   382
            val decls = decls_for_atom_schema ~1 binder_schema
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   383
            val vars = unary_var_seq ~1 (length binder_schema)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   384
            val kk_xone = if one then kk_one else kk_lone
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   385
          in kk_all decls (kk_xone (fold kk_join vars r)) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   386
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   387
    else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   388
      KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   389
  end
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   390
fun kk_n_ary_function kk R (r as KK.Rel x) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   391
    if not (is_opt_rep R) then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   392
      if x = suc_rel then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   393
        KK.False
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   394
      else if x = nat_add_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   395
        formula_for_bool (card_of_rep (body_rep R) = 1)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   396
      else if x = nat_multiply_rel then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   397
        formula_for_bool (card_of_rep (body_rep R) <= 2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   398
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   399
        d_n_ary_function kk R r
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   400
    else if x = nat_subtract_rel then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   401
      KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   402
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
      d_n_ary_function kk R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   404
  | kk_n_ary_function kk R r = d_n_ary_function kk R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   405
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   406
fun kk_disjoint_sets _ [] = KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   407
  | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   408
                     (r :: rs) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   409
    fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   410
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   411
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   412
  if inline_rel_expr r then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   413
    f r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   414
  else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   415
    let val x = (KK.arity_of_rel_expr r, j) in
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   416
      kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   417
    end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   418
val single_rel_rel_let = basic_rel_rel_let 0
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   419
fun double_rel_rel_let kk f r1 r2 =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   420
  single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
35386
45a4e19d3ebd more work on the new monotonicity stuff in Nitpick
blanchet
parents: 35385
diff changeset
   421
fun triple_rel_rel_let kk f r1 r2 r3 =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   422
  double_rel_rel_let kk
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   423
      (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   424
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   425
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   426
  kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   427
fun rel_expr_from_formula kk R f =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   428
  case unopt_rep R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   429
    Atom (2, j0) => atom_from_formula kk j0 f
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   430
  | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   431
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   432
fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   433
                          num_chunks r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   434
  List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   435
                                                    chunk_arity)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   436
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
fun kk_n_fold_join
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
        (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   439
        res_R r1 r2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   440
  case arity_of_rep R1 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
    1 => kk_join r1 r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
  | arity1 =>
38164
346df80a0924 optimize generated Kodkod formula
blanchet
parents: 38160
diff changeset
   443
    let val unpacked_rs1 = unpack_products r1 in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   444
      if one andalso length unpacked_rs1 = arity1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   445
        fold kk_join unpacked_rs1 r2
38164
346df80a0924 optimize generated Kodkod formula
blanchet
parents: 38160
diff changeset
   446
      else if one andalso inline_rel_expr r1 then
346df80a0924 optimize generated Kodkod formula
blanchet
parents: 38160
diff changeset
   447
        fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   448
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   449
        kk_project_seq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   450
            (kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   451
            arity1 (arity_of_rep res_R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   452
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   453
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   454
fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   455
  if rs1 = rs2 then r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   456
  else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   457
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   458
val lone_rep_fallback_max_card = 4096
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   459
val some_j0 = 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   460
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   461
fun lone_rep_fallback kk new_R old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
  if old_R = new_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   463
    r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   464
  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   465
    let val card = card_of_rep old_R in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
   466
      if is_lone_rep old_R andalso is_lone_rep new_R andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
   467
         card = card_of_rep new_R then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   468
        if card >= lone_rep_fallback_max_card then
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   469
          raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   470
                           "too high cardinality (" ^ string_of_int card ^ ")")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   471
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   472
          kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   473
                         (all_singletons_for_rep new_R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
      else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   475
        raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
    end
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   477
and atom_from_rel_expr kk x old_R r =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
  case old_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
    Func (R1, R2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   481
      val dom_card = card_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   482
      val R2' = case R2 of Atom _ => R2 | _ => Atom (card_of_rep R2, some_j0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   483
    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   484
      atom_from_rel_expr kk x (Vect (dom_card, R2'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   485
                         (vect_from_rel_expr kk dom_card R2' old_R r)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   486
    end
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   487
  | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   488
  | _ => lone_rep_fallback kk (Atom x) old_R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   489
and struct_from_rel_expr kk Rs old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   490
  case old_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   491
    Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   492
  | Struct Rs' =>
38190
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   493
    if Rs' = Rs then
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   494
      r
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   495
    else if map card_of_rep Rs' = map card_of_rep Rs then
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   496
      let
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   497
        val old_arities = map arity_of_rep Rs'
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   498
        val old_offsets = offset_list old_arities
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   499
        val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   500
      in
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   501
        fold1 (#kk_product kk)
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   502
              (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   503
      end
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   504
    else
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
   505
      lone_rep_fallback kk (Struct Rs) old_R r
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   506
  | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   507
and vect_from_rel_expr kk k R old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   508
  case old_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   509
    Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
  | Vect (k', R') =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   511
    if k = k' andalso R = R' then r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
    else lone_rep_fallback kk (Vect (k, R)) old_R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
  | Func (R1, Formula Neut) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   514
    if k = card_of_rep R1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
      fold1 (#kk_product kk)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
            (map (fn arg_r =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   517
                     rel_expr_from_formula kk R (#kk_subset kk arg_r r))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
                 (all_singletons_for_rep R1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   519
    else
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   520
      raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   521
  | Func (R1, R2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
    fold1 (#kk_product kk)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
          (map (fn arg_r =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   524
                   rel_expr_from_rel_expr kk R R2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   525
                                         (kk_n_fold_join kk true R1 R2 arg_r r))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   526
               (all_singletons_for_rep R1))
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   527
  | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   530
      val dom_card = card_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
      val R2' = case R2 of Atom _ => R2 | _ => Atom (card_of_rep R2, some_j0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
      func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
                                (vect_from_rel_expr kk dom_card R2' (Atom x) r)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
  | func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
    (case old_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   538
       Vect (k, Atom (2, j0)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
       let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
         val args_rs = all_singletons_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
         val vals_rs = unpack_vect_in_chunks kk 1 k r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
         fun empty_or_singleton_set_for arg_r val_r =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   543
           #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   544
       in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
         fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   546
       end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
     | Func (R1', Formula Neut) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   548
       if R1 = R1' then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   549
         r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   550
       else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
         let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
           val schema = atom_schema_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   553
           val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
                    |> rel_expr_from_rel_expr kk R1' R1
33582
bdf98e327f0b fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents: 33571
diff changeset
   555
           val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
         in
33582
bdf98e327f0b fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents: 33571
diff changeset
   557
           #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   558
         end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   559
     | Func (R1', Atom (2, j0)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
       func_from_no_opt_rel_expr kk R1 (Formula Neut)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   561
           (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1)))
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   562
     | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
                       [old_R, Func (R1, Formula Neut)]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   564
  | func_from_no_opt_rel_expr kk R1 R2 old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   565
    case old_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   566
      Vect (k, R) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   567
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
        val args_rs = all_singletons_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   569
        val vals_rs = unpack_vect_in_chunks kk (arity_of_rep R) k r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   570
                      |> map (rel_expr_from_rel_expr kk R2 R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   571
      in fold1 (#kk_union kk) (map2 (#kk_product kk) args_rs vals_rs) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   572
    | Func (R1', Formula Neut) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   573
      (case R2 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   574
         Atom (x as (2, j0)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   575
         let val schema = atom_schema_of_rep R1 in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   576
           if length schema = 1 then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   577
             #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   578
                                             (KK.Atom j0))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   579
                             (#kk_product kk r (KK.Atom (j0 + 1)))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   580
           else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   581
             let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   582
               val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   583
                        |> rel_expr_from_rel_expr kk R1' R1
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   584
               val r2 = KK.Var (1, ~(length schema) - 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
               val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
             in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
               #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x]))
33582
bdf98e327f0b fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents: 33571
diff changeset
   588
                                 (#kk_subset kk r2 r3)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   589
             end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   590
           end
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   591
         | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   592
                           [old_R, Func (R1, R2)]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   593
    | Func (R1', R2') =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   594
      if R1 = R1' andalso R2 = R2' then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   595
        r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   596
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   597
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   598
          val dom_schema = atom_schema_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   599
          val ran_schema = atom_schema_of_rep R2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   600
          val dom_prod = fold1 (#kk_product kk)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   601
                               (unary_var_seq ~1 (length dom_schema))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
                         |> rel_expr_from_rel_expr kk R1' R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
          val ran_prod = fold1 (#kk_product kk)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
                               (unary_var_seq (~(length dom_schema) - 1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
                                              (length ran_schema))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   606
                         |> rel_expr_from_rel_expr kk R2' R2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   607
          val app = kk_n_fold_join kk true R1' R2' dom_prod r
33582
bdf98e327f0b fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents: 33571
diff changeset
   608
          val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   609
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   610
          #kk_comprehension kk (decls_for_atom_schema ~1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   611
                                                      (dom_schema @ ran_schema))
33582
bdf98e327f0b fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents: 33571
diff changeset
   612
                               (kk_xeq ran_prod app)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   613
        end
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   614
    | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
                      [old_R, Func (R1, R2)])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   616
and rel_expr_from_rel_expr kk new_R old_R r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   617
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
    val unopt_old_R = unopt_rep old_R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
    val unopt_new_R = unopt_rep new_R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   621
    if unopt_old_R <> old_R andalso unopt_new_R = new_R then
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   622
      raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   623
    else if unopt_new_R = unopt_old_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   624
      r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   625
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   626
      (case unopt_new_R of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   627
         Atom x => atom_from_rel_expr kk x
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   628
       | Struct Rs => struct_from_rel_expr kk Rs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   629
       | Vect (k, R') => vect_from_rel_expr kk k R'
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   630
       | Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   631
       | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   632
                         [old_R, new_R]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   633
          unopt_old_R r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   634
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   636
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   637
fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   638
  kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   639
                       unsigned_bit_word_sel_rel
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   640
                     else
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   641
                       signed_bit_word_sel_rel))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   642
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   643
fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   644
                        : kodkod_constrs) T R i =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   645
  kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   646
                   (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   647
                              (KK.Bits i))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   648
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   649
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   650
    kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   651
                      (KK.Rel x)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
  | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
                                    (FreeRel (x, _, R, _)) =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   654
    if is_one_rep R then kk_one (KK.Rel x)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   655
    else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   656
    else KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
  | declarative_axiom_for_plain_rel _ u =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   658
    raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   659
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   660
fun const_triple rel_table (x as (s, T)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   661
  case the_name rel_table (ConstName (s, T, Any)) of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   662
    FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
   663
  | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   664
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   665
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   666
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   667
fun nfa_transitions_for_sel hol_ctxt binarize
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   668
                            ({kk_project, ...} : kodkod_constrs) rel_table
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   669
                            (dtypes : datatype_spec list) constr_x n =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   670
  let
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   671
    val x as (_, T) =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   672
      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   673
    val (r, R, arity) = const_triple rel_table x
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   674
    val type_schema = type_schema_of_rep T R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   675
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   676
    map_filter (fn (j, T) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   677
                   if forall (not_equal T o #typ) dtypes then NONE
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   678
                   else SOME ((x, kk_project r (map KK.Num [0, j])), T))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   679
               (index_seq 1 (arity - 1) ~~ tl type_schema)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
  end
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   681
fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   682
                               (x as (_, T)) =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   683
  maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   684
       (index_seq 0 (num_sels_for_constr_type T))
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   685
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   686
  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   687
  | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   688
  | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   689
                           {typ, constrs, ...} =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   690
    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   691
                                                dtypes o #const) constrs)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   692
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   693
val empty_rel = KK.Product (KK.None, KK.None)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   694
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   695
fun direct_path_rel_exprs nfa start_T final_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   696
  case AList.lookup (op =) nfa final_T of
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   697
    SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   698
  | NONE => []
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   699
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   700
                      final_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   701
    fold kk_union (direct_path_rel_exprs nfa start_T final_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   702
         (if start_T = final_T then KK.Iden else empty_rel)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   703
  | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   704
    kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   705
             (knot_path_rel_expr kk nfa Ts start_T T final_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   706
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   707
                       start_T knot_T final_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   708
  kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   709
                   (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   710
          (any_path_rel_expr kk nfa Ts start_T knot_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   711
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   712
    fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   713
  | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   714
                       start_T =
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   715
    if start_T = T then
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   716
      kk_closure (loop_path_rel_expr kk nfa Ts start_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   717
    else
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   718
      kk_union (loop_path_rel_expr kk nfa Ts start_T)
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35078
diff changeset
   719
               (knot_path_rel_expr kk nfa Ts start_T T start_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   720
39898
blanchet
parents: 39456
diff changeset
   721
fun add_nfa_to_graph [] = I
blanchet
parents: 39456
diff changeset
   722
  | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
blanchet
parents: 39456
diff changeset
   723
  | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
blanchet
parents: 39456
diff changeset
   724
    add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
blanchet
parents: 39456
diff changeset
   725
    Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   726
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   727
fun strongly_connected_sub_nfas nfa =
39898
blanchet
parents: 39456
diff changeset
   728
  add_nfa_to_graph nfa Typ_Graph.empty
blanchet
parents: 39456
diff changeset
   729
  |> Typ_Graph.strong_conn
blanchet
parents: 39456
diff changeset
   730
  |> map (fn keys => filter (member (op =) keys o fst) nfa)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   731
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   732
fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   733
                                  start_T =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   734
  kk_no (kk_intersect
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   735
             (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   736
             KK.Iden)
38195
a8cef06e0480 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents: 38194
diff changeset
   737
(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
a8cef06e0480 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents: 38194
diff changeset
   738
   the first equation. *)
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   739
fun acyclicity_axioms_for_datatypes _ [_] = []
38195
a8cef06e0480 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents: 38194
diff changeset
   740
  | acyclicity_axioms_for_datatypes kk nfas =
a8cef06e0480 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents: 38194
diff changeset
   741
    maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   742
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   743
fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   744
  kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   745
fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   746
  kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   747
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   748
fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   749
  (delta, (epsilon, (num_binder_types T, s)))
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   750
val constr_ord =
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   751
  prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   752
  o pairself constr_quadruple
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   753
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   754
fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   755
                   {card = card2, self_rec = self_rec2, constrs = constr2, ...})
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   756
                  : datatype_spec * datatype_spec) =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   757
  prod_ord int_ord (prod_ord bool_ord int_ord)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   758
           ((card1, (self_rec1, length constr1)),
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   759
            (card2, (self_rec2, length constr2)))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   760
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   761
(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   762
   break cycles; otherwise, we may end up with two incompatible symmetry
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   763
   breaking orders, leading to spurious models. *)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   764
fun should_tabulate_suc_for_type dtypes T =
38127
9f9f696fc4e8 tweak datatype sym break code
blanchet
parents: 38126
diff changeset
   765
  is_asymmetric_nondatatype T orelse
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   766
  case datatype_spec dtypes T of
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   767
    SOME {self_rec, ...} => self_rec
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   768
  | NONE => false
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   769
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   770
fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   771
                       dtypes sel_quadruples =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   772
  case sel_quadruples of
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   773
    [] => KK.True
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   774
  | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   775
    let val z = (x, should_tabulate_suc_for_type dtypes T) in
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   776
      if null sel_quadruples' then
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   777
        gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   778
      else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   779
        kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   780
                          (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   781
               (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   782
                                      (kk_join (KK.Var (1, 0)) r))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   783
                           (lex_order_rel_expr kk dtypes sel_quadruples'))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   784
    end
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   785
    (* Skip constructors components that aren't atoms, since we cannot compare
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   786
       these easily. *)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   787
  | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   788
38193
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   789
fun is_nil_like_constr_type dtypes T =
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   790
  case datatype_spec dtypes T of
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   791
    SOME {constrs, ...} =>
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   792
    (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   793
       [{const = (_, T'), ...}] => T = T'
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   794
     | _ => false)
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   795
  | NONE => false
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   796
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   797
fun sym_break_axioms_for_constr_pair hol_ctxt binarize
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   798
       (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   799
               kk_join, ...}) rel_table nfas dtypes
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   800
       (constr_ord,
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   801
        ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
39345
062c10ff848c remove unreferenced identifiers
blanchet
parents: 39316
diff changeset
   802
         {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
38191
deaef70a8c05 make SML/NJ happy
blanchet
parents: 38190
diff changeset
   803
        : constr_spec * constr_spec) =
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   804
  let
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   805
    val dataT = body_type T1
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   806
    val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   807
    val rec_Ts = nfa |> map fst
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   808
    fun rec_and_nonrec_sels (x as (_, T)) =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   809
      index_seq 0 (num_sels_for_constr_type T)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   810
      |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   811
      |> List.partition (member (op =) rec_Ts o range_type o snd)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   812
    val sel_xs1 = rec_and_nonrec_sels const1 |> op @
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   813
  in
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   814
    if constr_ord = EQUAL andalso null sel_xs1 then
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   815
      []
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   816
    else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   817
      let
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   818
        val z =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   819
          (case #2 (const_triple rel_table (discr_for_constr const1)) of
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   820
             Func (Atom x, Formula _) => x
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   821
           | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   822
                             [R]), should_tabulate_suc_for_type dtypes dataT)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   823
        val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   824
        val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   825
        fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   826
        (* If the two constructors are the same, we drop the first selector
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   827
           because that one is always checked by the lexicographic order.
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   828
           We sometimes also filter out direct subterms, because those are
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   829
           already handled by the acyclicity breaking in the bound
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   830
           declarations. *)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   831
        fun filter_out_sels no_direct sel_xs =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   832
          apsnd (filter_out
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   833
                     (fn ((x, _), T) =>
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   834
                         (constr_ord = EQUAL andalso x = hd sel_xs) orelse
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   835
                         (T = dataT andalso
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   836
                          (no_direct orelse not (member (op =) sel_xs x)))))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   837
        fun subterms_r no_direct sel_xs j =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   838
          loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   839
                           (filter_out (curry (op =) dataT) (map fst nfa)) dataT
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   840
          |> kk_join (KK.Var (1, j))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   841
      in
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   842
        [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   843
                 KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   844
             (kk_implies
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   845
                 (if delta2 >= epsilon1 then KK.True
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   846
                  else if delta1 >= epsilon2 - 1 then KK.False
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   847
                  else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   848
                 (kk_or
38193
44d635ce6da4 improve datatype symmetry breaking;
blanchet
parents: 38191
diff changeset
   849
                      (if is_nil_like_constr_type dtypes T1 then
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   850
                         KK.True
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   851
                       else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   852
                         kk_some (kk_intersect (subterms_r false sel_xs2 1)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   853
                                               (all_ge kk z (KK.Var (1, 0)))))
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   854
                      (case constr_ord of
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   855
                         EQUAL =>
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   856
                         kk_and
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   857
                             (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
38197
4374005e02f9 remove buggy and needless condition
blanchet
parents: 38196
diff changeset
   858
                             (kk_all [KK.DeclOne ((1, 2),
4374005e02f9 remove buggy and needless condition
blanchet
parents: 38196
diff changeset
   859
                                                  subterms_r true sel_xs1 0)]
4374005e02f9 remove buggy and needless condition
blanchet
parents: 38196
diff changeset
   860
                                     (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   861
                       | LESS =>
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   862
                         kk_all [KK.DeclOne ((1, 2),
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   863
                                 subterms_r false sel_xs1 0)]
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   864
                                (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   865
                       | GREATER => KK.False)))]
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   866
      end
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   867
  end
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   868
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   869
fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   870
                                  ({constrs, ...} : datatype_spec) =
38194
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   871
  let
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   872
    val constrs = sort constr_ord constrs
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   873
    val constr_pairs = all_distinct_unordered_pairs_of constrs
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   874
  in
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   875
    map (pair EQUAL) (constrs ~~ constrs) @
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   876
    map (pair LESS) constr_pairs @
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   877
    map (pair GREATER) (map swap constr_pairs)
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   878
    |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   879
                                              nfas dtypes)
a9877c14550f avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents: 38193
diff changeset
   880
  end
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   881
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   882
val min_sym_break_card = 7
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   883
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   884
fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   885
                                   rel_table nfas dtypes =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   886
  if datatype_sym_break = 0 then
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   887
    []
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   888
  else
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   889
    maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   890
                                        dtypes)
38196
51a1bfef9de2 renamed internal function
blanchet
parents: 38195
diff changeset
   891
         (dtypes |> filter is_datatype_acyclic
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   892
                 |> filter (fn {constrs = [_], ...} => false
38127
9f9f696fc4e8 tweak datatype sym break code
blanchet
parents: 38126
diff changeset
   893
                             | {card, constrs, ...} =>
9f9f696fc4e8 tweak datatype sym break code
blanchet
parents: 38126
diff changeset
   894
                               card >= min_sym_break_card andalso
9f9f696fc4e8 tweak datatype sym break code
blanchet
parents: 38126
diff changeset
   895
                               forall (forall (not o is_higher_order_type)
9f9f696fc4e8 tweak datatype sym break code
blanchet
parents: 38126
diff changeset
   896
                                       o binder_types o snd o #const) constrs)
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   897
                 |> (fn dtypes' =>
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   898
                        dtypes'
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   899
                        |> length dtypes' > datatype_sym_break
38212
a7e92239922f improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents: 38197
diff changeset
   900
                           ? (sort (datatype_ord o swap)
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   901
                              #> take datatype_sym_break)))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   902
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   903
fun sel_axiom_for_sel hol_ctxt binarize j0
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   904
        (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   905
        rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   906
        n =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   907
  let
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   908
    val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   909
    val (r, R, _) = const_triple rel_table x
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   910
    val R2 = dest_Func R |> snd
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   911
    val z = (epsilon - delta, delta + j0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   912
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   913
    if exclusive then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   914
      kk_n_ary_function kk (Func (Atom z, R2)) r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
    else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   916
      let val r' = kk_join (KK.Var (1, 0)) r in
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   917
        kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   918
               (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   919
                              (kk_n_ary_function kk R2 r') (kk_no r'))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   920
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   921
  end
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   922
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   923
        (constr as {const, delta, epsilon, explicit_max, ...}) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   924
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   925
    val honors_explicit_max =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   926
      explicit_max < 0 orelse epsilon - delta <= explicit_max
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   927
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   928
    if explicit_max = 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   929
      [formula_for_bool honors_explicit_max]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   930
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   931
      let
35178
29a0e3be0be1 minor fixes to Nitpick
blanchet
parents: 35177
diff changeset
   932
        val dom_r = discr_rel_expr rel_table const
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   933
        val max_axiom =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   934
          if honors_explicit_max then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   935
            KK.True
38121
a9d96531c2ee gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents: 37476
diff changeset
   936
          else if bits = 0 orelse
a9d96531c2ee gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents: 37476
diff changeset
   937
               is_twos_complement_representable bits (epsilon - delta) then
35178
29a0e3be0be1 minor fixes to Nitpick
blanchet
parents: 35177
diff changeset
   938
            KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   939
          else
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   940
            raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   941
                             "\"bits\" value " ^ string_of_int bits ^
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   942
                             " too small for \"max\"")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   943
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   944
        max_axiom ::
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   945
        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   946
            (index_seq 0 (num_sels_for_constr_type (snd const)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   947
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   948
  end
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   949
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   950
                            ({constrs, ...} : datatype_spec) =
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   951
  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   952
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   953
fun uniqueness_axiom_for_constr hol_ctxt binarize
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   954
        ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   955
         : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   956
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   957
    fun conjunct_for_sel r =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   958
      kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   959
    val num_sels = num_sels_for_constr_type (snd const)
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   960
    val triples =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   961
      map (const_triple rel_table
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   962
           o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   963
          (~1 upto num_sels - 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   964
    val set_r = triples |> hd |> #1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   965
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   966
    if num_sels = 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   967
      kk_lone set_r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   968
    else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   969
      kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   970
             (kk_implies
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   971
                  (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   972
                  (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   973
  end
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   974
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   975
                                   ({constrs, ...} : datatype_spec) =
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   976
  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   977
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   978
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   979
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   980
                                  rel_table
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   981
                                  ({card, constrs, ...} : datatype_spec) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   982
  if forall #exclusive constrs then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   983
    [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   984
  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   985
    let val rs = map (discr_rel_expr rel_table o #const) constrs in
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   986
      [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   987
       kk_disjoint_sets kk rs]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   988
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   989
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   990
fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   991
  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   992
                              (dtype as {typ, ...}) =
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33232
diff changeset
   993
    let val j0 = offset_of_type ofs typ in
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   994
      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35185
diff changeset
   995
      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33232
diff changeset
   996
      partition_axioms_for_datatype j0 kk rel_table dtype
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33232
diff changeset
   997
    end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   998
38126
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
   999
fun declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break bits
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1000
                                     ofs kk rel_table dtypes =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1001
  let
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1002
    val nfas =
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1003
      dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1004
                                                   rel_table dtypes)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1005
             |> strongly_connected_sub_nfas
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1006
  in
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1007
    acyclicity_axioms_for_datatypes kk nfas @
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1008
    sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1009
                                   rel_table nfas dtypes @
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1010
    maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1011
         dtypes
8031d099379a added manual symmetry breaking for datatypes
blanchet
parents: 38124
diff changeset
  1012
  end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1013
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
  1014
fun kodkod_formula_from_nut ofs
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1015
        (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
  1016
                kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
39456
blanchet
parents: 39360
diff changeset
  1017
                kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union,
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
  1018
                kk_difference, kk_intersect, kk_product, kk_join, kk_closure,
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
  1019
                kk_comprehension, kk_project, kk_project_seq, kk_not3,
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
  1020
                kk_nat_less, kk_int_less, ...}) u =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1021
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1022
    val main_j0 = offset_of_type ofs bool_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1023
    val bool_j0 = main_j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1024
    val bool_atom_R = Atom (2, main_j0)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1025
    val false_atom = KK.Atom bool_j0
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1026
    val true_atom = KK.Atom (bool_j0 + 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1027
    fun formula_from_opt_atom polar j0 r =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1028
      case polar of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1029
        Neg => kk_not (kk_rel_eq r (KK.Atom j0))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1030
      | _ => kk_rel_eq r (KK.Atom (j0 + 1))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1031
    val formula_from_atom = formula_from_opt_atom Pos
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1032
    val unpack_formulas =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1033
      map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1034
    fun kk_vect_set_bool_op connective k r1 r2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1035
      fold1 kk_and (map2 connective (unpack_formulas k r1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1036
                         (unpack_formulas k r2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1037
    fun to_f u =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1038
      case rep_of u of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1039
        Formula polar =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1040
        (case u of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1041
           Cst (False, _, _) => KK.False
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1042
         | Cst (True, _, _) => KK.True
33854
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1043
         | Op1 (Not, _, _, u1) =>
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1044
           kk_not (to_f_with_polarity (flip_polarity polar) u1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1045
         | Op1 (Finite, _, _, u1) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1046
           let val opt1 = is_opt_rep (rep_of u1) in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1047
             case polar of
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1048
               Neut =>
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1049
               if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1050
               else KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1051
             | Pos => formula_for_bool (not opt1)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1052
             | Neg => KK.True
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1053
           end
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1054
         | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1055
         | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
33854
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1056
         | Op2 (All, _, _, u1, u2) =>
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1057
           kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1058
         | Op2 (Exist, _, _, u1, u2) =>
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1059
           kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2)
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1060
         | Op2 (Or, _, _, u1, u2) =>
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1061
           kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1062
         | Op2 (And, _, _, u1, u2) =>
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1063
           kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1064
         | Op2 (Less, T, Formula polar, u1, u2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1065
           formula_from_opt_atom polar bool_j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1066
               (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1067
         | Op2 (Subset, _, _, u1, u2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1068
           let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1069
             val dom_T = domain_type (type_of u1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1070
             val R1 = rep_of u1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1071
             val R2 = rep_of u2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1072
             val (dom_R, ran_R) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1073
               case min_rep R1 R2 of
38190
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
  1074
                 Func Rp => Rp
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1075
               | R => (Atom (card_of_domain_from_rep 2 R,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1076
                             offset_of_type ofs dom_T),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1077
                       if is_opt_rep R then Opt bool_atom_R else Formula Neut)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1078
             val set_R = Func (dom_R, ran_R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1079
           in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1080
             if not (is_opt_rep ran_R) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1081
               to_set_bool_op kk_implies kk_subset u1 u2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1082
             else if polar = Neut then
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1083
               raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1084
             else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1085
               let
33886
cde73f8dbe4e fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents: 33863
diff changeset
  1086
                 (* FIXME: merge with similar code below *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1087
                 fun set_to_r widen u =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1088
                   if widen then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1089
                     kk_difference (full_rel_for_rep dom_R)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1090
                                   (kk_join (to_rep set_R u) false_atom)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1091
                   else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1092
                     kk_join (to_rep set_R u) true_atom
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1093
                 val widen1 = (polar = Pos andalso is_opt_rep R1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1094
                 val widen2 = (polar = Neg andalso is_opt_rep R2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1095
               in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1096
           end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1097
         | Op2 (DefEq, _, _, u1, u2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1098
           (case min_rep (rep_of u1) (rep_of u2) of
38190
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
  1099
              Formula polar =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1100
              kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1101
            | min_R =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1102
              let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1103
                fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1104
                  | args (Tuple (_, _, us)) = us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1105
                  | args _ = []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1106
                val opt_arg_us = filter (is_opt_rep o rep_of) (args u1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1107
              in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1108
                if null opt_arg_us orelse not (is_Opt min_R) orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1109
                   is_eval_name u1 then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1110
                  fold (kk_or o (kk_no o to_r)) opt_arg_us
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1111
                       (kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1112
                else
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
  1113
                  kk_subset (to_rep min_R u1) (to_rep min_R u2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1114
              end)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
  1115
         | Op2 (Eq, _, _, u1, u2) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1116
           (case min_rep (rep_of u1) (rep_of u2) of
38190
b02e204b613a get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents: 38182
diff changeset
  1117
              Formula polar =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1118
              kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1119
            | min_R =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1120
              if is_opt_rep min_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1121
                if polar = Neut then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1122
                  (* continuation of hackish optimization *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1123
                  kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1124
                else if is_Cst Unrep u1 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1125
                  to_could_be_unrep (polar = Neg) u2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1126
                else if is_Cst Unrep u2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1127
                  to_could_be_unrep (polar = Neg) u1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1128
                else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1129
                  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1130
                    val r1 = to_rep min_R u1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1131
                    val r2 = to_rep min_R u2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1132
                    val both_opt = forall (is_opt_rep o rep_of) [u1, u2]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1133
                  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1134
                    (if polar = Pos then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1135
                       if not both_opt then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1136
                         kk_rel_eq r1 r2
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1137
                       else if is_lone_rep min_R andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1138
                               arity_of_rep min_R = 1 then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1139
                         kk_some (kk_intersect r1 r2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1140
                       else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1141
                         raise SAME ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1142
                     else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1143
                       if is_lone_rep min_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1144
                         if arity_of_rep min_R = 1 then
35072
d79308423aea optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents: 35070
diff changeset
  1145
                           kk_lone (kk_union r1 r2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1146
                         else if not both_opt then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1147
                           (r1, r2) |> is_opt_rep (rep_of u2) ? swap
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
  1148
                                    |-> kk_subset
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1149
                         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1150
                           raise SAME ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1151
                       else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1152
                         raise SAME ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1153
                    handle SAME () =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1154
                           formula_from_opt_atom polar bool_j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1155
                               (to_guard [u1, u2] bool_atom_R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1156
                                         (rel_expr_from_formula kk bool_atom_R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1157
                                                            (kk_rel_eq r1 r2)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1158
                  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1159
              else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1160
                let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1161
                  val r1 = to_rep min_R u1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1162
                  val r2 = to_rep min_R 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
                  if is_one_rep min_R then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1165
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1166
                      val rs1 = unpack_products r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1167
                      val rs2 = unpack_products r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1168
                    in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1169
                      if length rs1 = length rs2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1170
                         map KK.arity_of_rel_expr rs1
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34288
diff changeset
  1171
                         = map KK.arity_of_rel_expr rs2 then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1172
                        fold1 kk_and (map2 kk_subset rs1 rs2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1173
                      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1174
                        kk_subset r1 r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1175
                    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1176
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1177
                    kk_rel_eq r1 r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1178
                end)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1179
         | Op2 (Apply, T, _, u1, u2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1180
           (case (polar, rep_of u1) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1181
              (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1182
            | _ =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1183
              to_f_with_polarity polar
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1184
                 (Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1185
         | Op3 (Let, _, _, u1, u2, u3) =>
33854
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1186
           kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1187
         | Op3 (If, _, _, u1, u2, u3) =>
33854
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1188
           kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
26a4cb3a7eae fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents: 33744
diff changeset
  1189
                         (to_f_with_polarity polar u3)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1190
         | FormulaReg (j, _, _) => KK.FormulaReg j
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1191
         | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1192
      | Atom (2, j0) => formula_from_atom j0 (to_r u)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1193
      | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1194
    and to_f_with_polarity polar u =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1195
      case rep_of u of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1196
        Formula _ => to_f u
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1197
      | Atom (2, j0) => formula_from_atom j0 (to_r u)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1198
      | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1199
      | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1200
    and to_r u =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1201
      case u of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1202
        Cst (False, _, Atom _) => false_atom
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1203
      | Cst (True, _, Atom _) => true_atom
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
  1204
      | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1205
        if R1 = R2 andalso arity_of_rep R1 = 1 then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1206
          kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1207
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1208
          let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1209
            val schema1 = atom_schema_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1210
            val schema2 = atom_schema_of_rep R2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1211
            val arity1 = length schema1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1212
            val arity2 = length schema2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1213
            val r1 = fold1 kk_product (unary_var_seq 0 arity1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1214
            val r2 = fold1 kk_product (unary_var_seq arity1 arity2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1215
            val min_R = min_rep R1 R2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1216
          in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1217
            kk_comprehension
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1218
                (decls_for_atom_schema 0 (schema1 @ schema2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1219
                (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1220
                           (rel_expr_from_rel_expr kk min_R R2 r2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1221
          end
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
  1222
      | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
  1223
      | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1224
        to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1225
      | Cst (Num j, T, R) =>
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1226
        if is_word_type T then
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1227
          atom_from_int_expr kk T R (KK.Num j)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1228
        else if T = int_T then
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1229
          case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1230
            ~1 => if is_opt_rep R then KK.None
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33192
diff changeset
  1231
                  else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1232
          | j' => KK.Atom j'
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1233
        else
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1234
          if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T)
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1235
          else if is_opt_rep R then KK.None
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1236
          else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1237
      | Cst (Unknown, _, R) => empty_rel_for_rep R
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1238
      | Cst (Unrep, _, R) => empty_rel_for_rep R
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1239
      | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) =>
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1240
        to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1241
      | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1242
        kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
  1243
      | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
  1244
      | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
  1245
      | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
  1246
      | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
  1247
        to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
35665
ff2bf50505ab added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents: 35407
diff changeset
  1248
      | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
  1249
        to_bit_word_binary_op T R