src/HOL/Tools/Nitpick/kodkod.ML
author blanchet
Fri, 14 May 2010 15:02:38 +0200
changeset 36914 1806aa69bd62
parent 36390 eee4ee6a5cbe
child 38019 e207a64e1e0b
permissions -rw-r--r--
recognize new Kodkod error message syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33734
diff changeset
     1
(*  Title:      HOL/Tools/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
ML interface on top 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 KODKOD =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    10
  type n_ary_index = int * int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    11
  type setting = string * string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    12
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    13
  datatype tuple =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
    Tuple of int list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    15
    TupleIndex of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
    TupleReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
  datatype tuple_set =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    19
    TupleUnion of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
    TupleDifference of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    21
    TupleIntersect of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    22
    TupleProduct of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    23
    TupleProject of tuple_set * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    24
    TupleSet of tuple list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
    TupleRange of tuple * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
    TupleArea of tuple * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    27
    TupleAtomSeq of int * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
    TupleSetReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    30
  datatype tuple_assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    31
    AssignTuple of n_ary_index * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
    AssignTupleSet of n_ary_index * tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    33
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
  type bound = (n_ary_index * string) list * tuple_set list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    35
  type int_bound = int option * tuple_set list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    36
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    37
  datatype formula =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    38
    All of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    39
    Exist of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    40
    FormulaLet of expr_assign list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    41
    FormulaIf of formula * formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
    Or of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    43
    Iff of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    44
    Implies of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    45
    And of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    46
    Not of formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
    Acyclic of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
    Function of n_ary_index * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
    Functional of n_ary_index * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    50
    TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    51
    Subset of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    52
    RelEq of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    53
    IntEq of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
    LT of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    55
    LE of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    56
    No of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    57
    Lone of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    58
    One of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    59
    Some of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    60
    False |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    61
    True |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    62
    FormulaReg of int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    63
  and rel_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    64
    RelLet of expr_assign list * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    65
    RelIf of formula * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    66
    Union of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    67
    Difference of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    68
    Override of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    69
    Intersect of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    70
    Product of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    71
    IfNo of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    72
    Project of rel_expr * int_expr list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    73
    Join of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    74
    Closure of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    75
    ReflexiveClosure of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    76
    Transpose of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    77
    Comprehension of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    78
    Bits of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    79
    Int of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    80
    Iden |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    81
    Ints |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    82
    None |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    83
    Univ |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    84
    Atom of int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    85
    AtomSeq of int * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    86
    Rel of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    87
    Var of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    88
    RelReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    89
  and int_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    90
    Sum of decl list * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    91
    IntLet of expr_assign list * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    92
    IntIf of formula * int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    93
    SHL of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    94
    SHA of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    95
    SHR of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    96
    Add of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    97
    Sub of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    98
    Mult of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    99
    Div of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   100
    Mod of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   101
    Cardinality of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   102
    SetSum of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   103
    BitOr of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   104
    BitXor of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   105
    BitAnd of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
    BitNot of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   107
    Neg of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   108
    Absolute of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
    Signum of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   110
    Num of int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   111
    IntReg of int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   112
  and decl =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   113
    DeclNo of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   114
    DeclLone of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   115
    DeclOne of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   116
    DeclSome of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
    DeclSet of n_ary_index * rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   118
  and expr_assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
    AssignFormulaReg of int * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   120
    AssignRelReg of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
    AssignIntReg of int * int_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   122
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   123
  type 'a fold_expr_funcs =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   124
    {formula_func: formula -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   125
     rel_expr_func: rel_expr -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   126
     int_expr_func: int_expr -> 'a -> 'a}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   127
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   128
  val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   129
  val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   130
  val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   131
  val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   132
  val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   134
  type 'a fold_tuple_funcs =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   135
    {tuple_func: tuple -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   136
     tuple_set_func: tuple_set -> 'a -> 'a}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   138
  val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   139
  val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
  val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
  val fold_bound :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
      'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
  val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   144
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   145
  type problem =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   146
    {comment: string,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   147
     settings: setting list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   148
     univ_card: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   149
     tuple_assigns: tuple_assign list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   150
     bounds: bound list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   151
     int_bounds: int_bound list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   152
     expr_assigns: expr_assign list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   153
     formula: formula}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   154
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   155
  type raw_bound = n_ary_index * int list list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   156
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   157
  datatype outcome =
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
   158
    JavaNotInstalled |
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
   159
    KodkodiNotInstalled |
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
   160
    Normal of (int * raw_bound list) list * int list * string |
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
    TimedOut of int list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   162
    Interrupted of int list option |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   163
    Error of string * int list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   164
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   165
  exception SYNTAX of string * string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   166
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   167
  val max_arity : int -> int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   168
  val arity_of_rel_expr : rel_expr -> int
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35079
diff changeset
   169
  val is_problem_trivially_false : problem -> bool
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   170
  val problems_equivalent : problem * problem -> bool
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
  val solve_any_problem :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
    bool -> Time.time option -> int -> int -> problem list -> outcome
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   173
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   175
structure Kodkod : KODKOD =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   176
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   177
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
type n_ary_index = int * int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
type setting = string * string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   182
datatype tuple =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   183
  Tuple of int list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   184
  TupleIndex of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   185
  TupleReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   186
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   187
datatype tuple_set =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   188
  TupleUnion of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   189
  TupleDifference of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   190
  TupleIntersect of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   191
  TupleProduct of tuple_set * tuple_set |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   192
  TupleProject of tuple_set * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   193
  TupleSet of tuple list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
  TupleRange of tuple * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   195
  TupleArea of tuple * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   196
  TupleAtomSeq of int * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   197
  TupleSetReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   198
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
datatype tuple_assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   200
  AssignTuple of n_ary_index * tuple |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
  AssignTupleSet of n_ary_index * tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   202
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   203
type bound = (n_ary_index * string) list * tuple_set list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   204
type int_bound = int option * tuple_set list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   205
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   206
datatype formula =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   207
  All of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   208
  Exist of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   209
  FormulaLet of expr_assign list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   210
  FormulaIf of formula * formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   211
  Or of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   212
  Iff of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   213
  Implies of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   214
  And of formula * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   215
  Not of formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   216
  Acyclic of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   217
  Function of n_ary_index * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   218
  Functional of n_ary_index * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   219
  TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   220
  Subset of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
  RelEq of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
  IntEq of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
  LT of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   224
  LE of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   225
  No of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   226
  Lone of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
  One of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   228
  Some of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   229
  False |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   230
  True |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   231
  FormulaReg of int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   232
and rel_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   233
  RelLet of expr_assign list * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   234
  RelIf of formula * rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   235
  Union of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   236
  Difference of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   237
  Override of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   238
  Intersect of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
  Product of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   240
  IfNo of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   241
  Project of rel_expr * int_expr list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
  Join of rel_expr * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   243
  Closure of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   244
  ReflexiveClosure of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
  Transpose of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   246
  Comprehension of decl list * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   247
  Bits of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   248
  Int of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   249
  Iden |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   250
  Ints |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   251
  None |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   252
  Univ |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   253
  Atom of int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   254
  AtomSeq of int * int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   255
  Rel of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   256
  Var of n_ary_index |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   257
  RelReg of n_ary_index
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   258
and int_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   259
  Sum of decl list * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   260
  IntLet of expr_assign list * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   261
  IntIf of formula * int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   262
  SHL of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   263
  SHA of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   264
  SHR of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   265
  Add of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   266
  Sub of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   267
  Mult of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   268
  Div of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   269
  Mod of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   270
  Cardinality of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   271
  SetSum of rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   272
  BitOr of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   273
  BitXor of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   274
  BitAnd of int_expr * int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   275
  BitNot of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   276
  Neg of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   277
  Absolute of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   278
  Signum of int_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   279
  Num of int |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   280
  IntReg of int
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   281
and decl =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   282
  DeclNo of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   283
  DeclLone of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   284
  DeclOne of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   285
  DeclSome of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
  DeclSet of n_ary_index * rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   287
and expr_assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   288
  AssignFormulaReg of int * formula |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   289
  AssignRelReg of n_ary_index * rel_expr |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
  AssignIntReg of int * int_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   291
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   292
type problem =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   293
  {comment: string,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   294
   settings: setting list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   295
   univ_card: int,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   296
   tuple_assigns: tuple_assign list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   297
   bounds: bound list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   298
   int_bounds: int_bound list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   299
   expr_assigns: expr_assign list,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   300
   formula: formula}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   301
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   302
type raw_bound = n_ary_index * int list list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   303
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   304
datatype outcome =
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
   305
  JavaNotInstalled |
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
   306
  KodkodiNotInstalled |
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
   307
  Normal of (int * raw_bound list) list * int list * string |
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   308
  TimedOut of int list |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
  Interrupted of int list option |
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   310
  Error of string * int list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   312
exception SYNTAX of string * string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   313
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   314
type 'a fold_expr_funcs =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   315
  {formula_func: formula -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   316
   rel_expr_func: rel_expr -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   317
   int_expr_func: int_expr -> 'a -> 'a}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   318
35718
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   319
(** Auxiliary functions on ML representation of Kodkod problems **)
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   320
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   321
fun fold_formula (F : 'a fold_expr_funcs) formula =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   322
  case formula of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   323
    All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   324
  | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   325
  | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   326
  | FormulaIf (f, f1, f2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   327
    fold_formula F f #> fold_formula F f1 #> fold_formula F f2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
  | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   329
  | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   330
  | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   331
  | And (f1, f2) => fold_formula F f1 #> fold_formula F f2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   332
  | Not f => fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   333
  | Acyclic x => fold_rel_expr F (Rel x)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   334
  | Function (x, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   335
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   336
  | Functional (x, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   337
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   338
  | TotalOrdering (x1, x2, x3, x4) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   339
    fold_rel_expr F (Rel x1) #> fold_rel_expr F (Rel x2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   340
    #> fold_rel_expr F (Rel x3) #> fold_rel_expr F (Rel x4)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   341
  | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   342
  | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   343
  | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   344
  | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   345
  | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   346
  | No r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   347
  | Lone r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   348
  | One r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   349
  | Some r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   350
  | False => #formula_func F formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   351
  | True => #formula_func F formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   352
  | FormulaReg _ => #formula_func F formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   353
and fold_rel_expr F rel_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   354
  case rel_expr of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   355
    RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   356
  | RelIf (f, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   357
    fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   358
  | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   359
  | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   360
  | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   361
  | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   362
  | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   363
  | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   364
  | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   365
  | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   366
  | Closure r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   367
  | ReflexiveClosure r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   368
  | Transpose r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   369
  | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   370
  | Bits i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   371
  | Int i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   372
  | Iden => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   373
  | Ints => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   374
  | None => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   375
  | Univ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   376
  | Atom _ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   377
  | AtomSeq _ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   378
  | Rel _ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   379
  | Var _ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   380
  | RelReg _ => #rel_expr_func F rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   381
and fold_int_expr F int_expr =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   382
  case int_expr of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   383
    Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   384
  | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   385
  | IntIf (f, i1, i2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   386
    fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   387
  | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   388
  | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   389
  | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   390
  | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   391
  | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   392
  | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   393
  | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   394
  | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   395
  | Cardinality r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   396
  | SetSum r => fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   397
  | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   398
  | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   399
  | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   400
  | BitNot i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   401
  | Neg i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   402
  | Absolute i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
  | Signum i => fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   404
  | Num _ => #int_expr_func F int_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   405
  | IntReg _ => #int_expr_func F int_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   406
and fold_decl F decl =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   407
  case decl of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   408
    DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   409
  | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   410
  | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   411
  | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   412
  | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   413
and fold_expr_assign F assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   414
  case assign of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   415
    AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   416
  | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   417
  | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   418
36390
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   419
type 'a fold_tuple_funcs =
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   420
  {tuple_func: tuple -> 'a -> 'a,
eee4ee6a5cbe remove "show_skolems" option and change style of record declarations
blanchet
parents: 36385
diff changeset
   421
   tuple_set_func: tuple_set -> 'a -> 'a}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   422
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   423
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   424
fun fold_tuple_set F tuple_set =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   425
  case tuple_set of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   426
    TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   427
  | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   428
  | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   429
  | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   430
  | TupleProject (ts, _) => fold_tuple_set F ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   431
  | TupleSet ts => fold (fold_tuple F) ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   432
  | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   433
  | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   434
  | TupleAtomSeq _ => #tuple_set_func F tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   435
  | TupleSetReg _ => #tuple_set_func F tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   436
fun fold_tuple_assign F assign =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
  case assign of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
    AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   439
  | AssignTupleSet (x, ts) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   440
    fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
fun fold_bound expr_F tuple_F (zs, tss) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
  fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   443
  #> fold (fold_tuple_set tuple_F) tss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   444
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   445
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   446
fun max_arity univ_card = floor (Math.ln 2147483647.0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
                                 / Math.ln (Real.fromInt univ_card))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   448
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   449
  | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   450
  | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   451
  | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   452
  | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   453
  | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   454
  | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   455
  | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35187
diff changeset
   456
  | arity_of_rel_expr (Project (_, is)) = length is
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   457
  | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   458
  | arity_of_rel_expr (Closure _) = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   459
  | arity_of_rel_expr (ReflexiveClosure _) = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   460
  | arity_of_rel_expr (Transpose _) = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   461
  | arity_of_rel_expr (Comprehension (ds, _)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
    fold (curry op + o arity_of_decl) ds 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   463
  | arity_of_rel_expr (Bits _) = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   464
  | arity_of_rel_expr (Int _) = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   465
  | arity_of_rel_expr Iden = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   466
  | arity_of_rel_expr Ints = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   467
  | arity_of_rel_expr None = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   468
  | arity_of_rel_expr Univ = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   469
  | arity_of_rel_expr (Atom _) = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   470
  | arity_of_rel_expr (AtomSeq _) = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   471
  | arity_of_rel_expr (Rel (n, _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   472
  | arity_of_rel_expr (Var (n, _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   473
  | arity_of_rel_expr (RelReg (n, _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   475
and arity_of_decl (DeclNo ((n, _), _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
  | arity_of_decl (DeclLone ((n, _), _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   477
  | arity_of_decl (DeclOne ((n, _), _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
  | arity_of_decl (DeclSome ((n, _), _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
  | arity_of_decl (DeclSet ((n, _), _)) = n
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
35185
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35079
diff changeset
   481
fun is_problem_trivially_false ({formula = False, ...} : problem) = true
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35079
diff changeset
   482
  | is_problem_trivially_false _ = false
9b8f351cced6 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents: 35079
diff changeset
   483
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   484
val chop_solver = take 2 o space_explode ","
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   485
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   486
fun settings_equivalent ([], []) = true
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   487
  | settings_equivalent ((key1, value1) :: settings1,
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   488
                         (key2, value2) :: settings2) =
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   489
    key1 = key2 andalso
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   490
    (value1 = value2 orelse key1 = "delay" orelse
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   491
     (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   492
    settings_equivalent (settings1, settings2)
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   493
  | settings_equivalent _ = false
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   494
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   495
fun problems_equivalent (p1 : problem, p2 : problem) =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   496
  #univ_card p1 = #univ_card p2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   497
  #formula p1 = #formula p2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   498
  #bounds p1 = #bounds p2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   499
  #expr_assigns p1 = #expr_assigns p2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   500
  #tuple_assigns p1 = #tuple_assigns p2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   501
  #int_bounds p1 = #int_bounds p2 andalso
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   502
  settings_equivalent (#settings p1, #settings p2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   503
35718
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   504
(** Serialization of problem **)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   505
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   506
fun base_name j =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   507
  if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   508
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   509
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
  | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   511
  | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
fun atom_name j = "A" ^ base_name j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   514
fun atom_seq_name (k, 0) = "u" ^ base_name k
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
  | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
fun formula_reg_name j = "$f" ^ base_name j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   517
fun rel_reg_name j = "$e" ^ base_name j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
fun int_reg_name j = "$i" ^ base_name j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   519
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   520
fun tuple_name x = n_ary_name x "A" "P" "T"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   521
fun rel_name x = n_ary_name x "s" "r" "m"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
fun var_name x = n_ary_name x "S" "R" "M"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   524
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   525
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   526
fun inline_comment "" = ""
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   527
  | inline_comment comment =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
    " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
    " */"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   530
fun block_comment "" = ""
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
  | block_comment comment = prefix_lines "// " comment ^ "\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
  | string_for_tuple (TupleIndex x) = tuple_name x
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
  | string_for_tuple (TupleReg x) = tuple_reg_name x
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   538
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
val no_prec = 100
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
val prec_TupleUnion = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
val prec_TupleIntersect = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
val prec_TupleProduct = 3
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   543
val prec_TupleProject = 4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   544
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
fun precedence_ts (TupleUnion _) = prec_TupleUnion
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   546
  | precedence_ts (TupleDifference _) = prec_TupleUnion
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
  | precedence_ts (TupleIntersect _) = prec_TupleIntersect
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   548
  | precedence_ts (TupleProduct _) = prec_TupleProduct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   549
  | precedence_ts (TupleProject _) = prec_TupleProject
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   550
  | precedence_ts _ = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
fun string_for_tuple_set tuple_set =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   553
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
    fun sub tuple_set outer_prec =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   555
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
        val prec = precedence_ts tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
        val need_parens = (prec < outer_prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   558
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   559
        (if need_parens then "(" else "") ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
        (case tuple_set of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
           TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
         | TupleDifference (ts1, ts2) =>
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35187
diff changeset
   563
           sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35187
diff changeset
   564
         | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   565
         | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   566
         | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   567
         | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
         | TupleRange (t1, t2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   569
           "{" ^ string_for_tuple t1 ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   570
           (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   571
         | TupleArea (t1, t2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   572
           "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   573
         | TupleAtomSeq x => atom_seq_name x
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   574
         | TupleSetReg x => tuple_set_reg_name x) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   575
        (if need_parens then ")" else "")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   576
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   577
  in sub tuple_set 0 end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   578
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   579
fun string_for_tuple_assign (AssignTuple (x, t)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   580
    tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   581
  | string_for_tuple_assign (AssignTupleSet (x, ts)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   582
    tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   583
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   584
fun string_for_bound (zs, tss) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
  "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
  (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
  (if length tss = 1 then "" else "]") ^ "\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   588
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   589
fun int_string_for_bound (opt_n, tss) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   590
  (case opt_n of
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   591
     SOME n => signed_string_of_int n ^ ": "
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   592
   | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   593
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   594
val prec_All = 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   595
val prec_Or = 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   596
val prec_Iff = 3
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   597
val prec_Implies = 4
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   598
val prec_And = 5
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   599
val prec_Not = 6
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   600
val prec_Eq = 7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   601
val prec_Some = 8
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
val prec_SHL = 9
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
val prec_Add = 10
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
val prec_Mult = 11
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
val prec_Override = 12
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   606
val prec_Intersect = 13
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   607
val prec_Product = 14
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   608
val prec_IfNo = 15
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   609
val prec_Project = 17
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   610
val prec_Join = 18
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   611
val prec_BitNot = 19
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   612
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   613
fun precedence_f (All _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   614
  | precedence_f (Exist _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   615
  | precedence_f (FormulaLet _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   616
  | precedence_f (FormulaIf _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   617
  | precedence_f (Or _) = prec_Or
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
  | precedence_f (Iff _) = prec_Iff
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
  | precedence_f (Implies _) = prec_Implies
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
  | precedence_f (And _) = prec_And
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   621
  | precedence_f (Not _) = prec_Not
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
  | precedence_f (Acyclic _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   623
  | precedence_f (Function _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   624
  | precedence_f (Functional _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   625
  | precedence_f (TotalOrdering _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   626
  | precedence_f (Subset _) = prec_Eq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   627
  | precedence_f (RelEq _) = prec_Eq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   628
  | precedence_f (IntEq _) = prec_Eq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   629
  | precedence_f (LT _) = prec_Eq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   630
  | precedence_f (LE _) = prec_Eq
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   631
  | precedence_f (No _) = prec_Some
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   632
  | precedence_f (Lone _) = prec_Some
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   633
  | precedence_f (One _) = prec_Some
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   634
  | precedence_f (Some _) = prec_Some
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
  | precedence_f False = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   636
  | precedence_f True = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   637
  | precedence_f (FormulaReg _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   638
and precedence_r (RelLet _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   639
  | precedence_r (RelIf _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   640
  | precedence_r (Union _) = prec_Add
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   641
  | precedence_r (Difference _) = prec_Add
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   642
  | precedence_r (Override _) = prec_Override
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   643
  | precedence_r (Intersect _) = prec_Intersect
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   644
  | precedence_r (Product _) = prec_Product
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   645
  | precedence_r (IfNo _) = prec_IfNo
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   646
  | precedence_r (Project _) = prec_Project
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   647
  | precedence_r (Join _) = prec_Join
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   648
  | precedence_r (Closure _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   649
  | precedence_r (ReflexiveClosure _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   650
  | precedence_r (Transpose _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
  | precedence_r (Comprehension _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   652
  | precedence_r (Bits _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
  | precedence_r (Int _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   654
  | precedence_r Iden = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   655
  | precedence_r Ints = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   656
  | precedence_r None = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
  | precedence_r Univ = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   658
  | precedence_r (Atom _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   659
  | precedence_r (AtomSeq _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   660
  | precedence_r (Rel _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   661
  | precedence_r (Var _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   662
  | precedence_r (RelReg _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   663
and precedence_i (Sum _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   664
  | precedence_i (IntLet _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   665
  | precedence_i (IntIf _) = prec_All
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   666
  | precedence_i (SHL _) = prec_SHL
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   667
  | precedence_i (SHA _) = prec_SHL
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   668
  | precedence_i (SHR _) = prec_SHL
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   669
  | precedence_i (Add _) = prec_Add
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   670
  | precedence_i (Sub _) = prec_Add
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   671
  | precedence_i (Mult _) = prec_Mult
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   672
  | precedence_i (Div _) = prec_Mult
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   673
  | precedence_i (Mod _) = prec_Mult
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   674
  | precedence_i (Cardinality _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   675
  | precedence_i (SetSum _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   676
  | precedence_i (BitOr _) = prec_Intersect
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   677
  | precedence_i (BitXor _) = prec_Intersect
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   678
  | precedence_i (BitAnd _) = prec_Intersect
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   679
  | precedence_i (BitNot _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
  | precedence_i (Neg _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   681
  | precedence_i (Absolute _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   682
  | precedence_i (Signum _) = prec_BitNot
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   683
  | precedence_i (Num _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   684
  | precedence_i (IntReg _) = no_prec
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   685
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   686
fun write_problem_file out problems =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   687
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   688
    fun out_outmost_f (And (f1, f2)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   689
        (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   690
      | out_outmost_f f = out_f f prec_And
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   691
    and out_f formula outer_prec =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   692
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   693
        val prec = precedence_f formula
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   694
        val need_parens = (prec < outer_prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   695
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   696
        (if need_parens then out "(" else ());
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   697
        (case formula of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   698
           All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   699
         | Exist (ds, f) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   700
           (out "some ["; out_decls ds; out "] | "; out_f f prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   701
         | FormulaLet (bs, f) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   702
           (out "let ["; out_assigns bs; out "] | "; out_f f prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   703
         | FormulaIf (f, f1, f2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   704
           (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else ";
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   705
            out_f f2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   706
         | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   707
         | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   708
         | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   709
         | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   710
         | Not f => (out "! "; out_f f prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   711
         | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   712
         | Function (x, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   713
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one ";
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   714
            out_r r2 0; out ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   715
         | Functional (x, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   716
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   717
            out_r r2 0; out ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   718
         | TotalOrdering (x1, x2, x3, x4) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   719
           out ("TOTAL_ORDERING(" ^ rel_name x1 ^ ", " ^ rel_name x2 ^ ", "
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   720
                ^ rel_name x3 ^ ", " ^ rel_name x4 ^ ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
         | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   722
         | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   723
         | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   724
         | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   725
         | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   726
         | No r => (out "no "; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   727
         | Lone r => (out "lone "; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   728
         | One r => (out "one "; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   729
         | Some r => (out "some "; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   730
         | False => out "false"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   731
         | True => out "true"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   732
         | FormulaReg j => out (formula_reg_name j));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   733
        (if need_parens then out ")" else ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   735
    and out_r rel_expr outer_prec =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   736
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
        val prec = precedence_r rel_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   738
        val need_parens = (prec < outer_prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   739
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   740
        (if need_parens then out "(" else ());
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   741
        (case rel_expr of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   742
           RelLet (bs, r) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   743
           (out "let ["; out_assigns bs; out "] | "; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   744
         | RelIf (f, r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   745
           (out "if "; out_f f prec; out " then "; out_r r1 prec;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   746
            out " else "; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   747
         | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   748
         | Difference (r1, r2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   749
           (out_r r1 prec; out " - "; out_r r2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   750
         | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   751
         | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   752
         | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   753
         | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   754
         | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   755
         | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   756
         | Closure r => (out "^"; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
         | ReflexiveClosure r => (out "*"; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   758
         | Transpose r => (out "~"; out_r r prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   759
         | Comprehension (ds, f) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   760
           (out "{["; out_decls ds; out "] | "; out_f f 0; out "}")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   761
         | Bits i => (out "Bits["; out_i i 0; out "]")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   762
         | Int i => (out "Int["; out_i i 0; out "]")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   763
         | Iden => out "iden"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   764
         | Ints => out "ints"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   765
         | None => out "none"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   766
         | Univ => out "univ"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   767
         | Atom j => out (atom_name j)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   768
         | AtomSeq x => out (atom_seq_name x)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   769
         | Rel x => out (rel_name x)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   770
         | Var x => out (var_name x)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   771
         | RelReg (_, j) => out (rel_reg_name j));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   772
        (if need_parens then out ")" else ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   773
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   774
    and out_i int_expr outer_prec =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   775
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   776
        val prec = precedence_i int_expr
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   777
        val need_parens = (prec < outer_prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   779
        (if need_parens then out "(" else ());
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   780
        (case int_expr of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   781
           Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   782
         | IntLet (bs, i) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   783
           (out "let ["; out_assigns bs; out "] | "; out_i i prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   784
         | IntIf (f, i1, i2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   785
           (out "if "; out_f f prec; out " then "; out_i i1 prec;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   786
            out " else "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   787
         | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   788
         | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
         | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   790
         | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   791
         | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   792
         | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   793
         | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   794
         | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   795
         | Cardinality r => (out "#("; out_r r 0; out ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   796
         | SetSum r => (out "sum("; out_r r 0; out ")")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   797
         | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   798
         | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   799
         | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   800
         | BitNot i => (out "~"; out_i i prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   801
         | Neg i => (out "-"; out_i i prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   802
         | Absolute i => (out "abs "; out_i i prec)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   803
         | Signum i => (out "sgn "; out_i i prec)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34121
diff changeset
   804
         | Num k => out (signed_string_of_int k)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   805
         | IntReg j => out (int_reg_name j));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   806
        (if need_parens then out ")" else ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   807
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   808
    and out_decls [] = ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   809
      | out_decls [d] = out_decl d
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   810
      | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   811
    and out_decl (DeclNo (x, r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   812
        (out (var_name x); out " : no "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   813
      | out_decl (DeclLone (x, r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   814
        (out (var_name x); out " : lone "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   815
      | out_decl (DeclOne (x, r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   816
        (out (var_name x); out " : one "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   817
      | out_decl (DeclSome (x, r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   818
        (out (var_name x); out " : some "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   819
      | out_decl (DeclSet (x, r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   820
        (out (var_name x); out " : set "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   821
    and out_assigns [] = ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   822
      | out_assigns [b] = out_assign b
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   823
      | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   824
    and out_assign (AssignFormulaReg (j, f)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   825
        (out (formula_reg_name j); out " := "; out_f f 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   826
      | out_assign (AssignRelReg ((_, j), r)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   827
        (out (rel_reg_name j); out " := "; out_r r 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   828
      | out_assign (AssignIntReg (j, i)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   829
        (out (int_reg_name j); out " := "; out_i i 0)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   830
    and out_columns [] = ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   831
      | out_columns [i] = out_i i 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   832
      | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   833
    and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   834
                     int_bounds, expr_assigns, formula} =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   835
        (out ("\n" ^ block_comment comment ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   836
              implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   837
                            settings) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   838
              "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   839
              implode (map string_for_tuple_assign tuple_assigns) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   840
              implode (map string_for_bound bounds) ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   841
              (if int_bounds = [] then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   842
                 ""
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   843
               else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   844
                 "int_bounds: " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   845
                 commas (map int_string_for_bound int_bounds) ^ "\n"));
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   846
         map (fn b => (out_assign b; out ";")) expr_assigns;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   847
         out "solve "; out_outmost_f formula; out ";\n")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   848
  in
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
   849
    out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
36381
f4d84d84a01a reuse timestamp function
blanchet
parents: 35814
diff changeset
   850
         "// " ^ Sledgehammer_Util.timestamp () ^ "\n");
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   851
    map out_problem problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   852
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   853
35718
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   854
(** Parsing of solution **)
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   855
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   856
fun is_ident_char s =
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   857
  Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   858
  s = "_" orelse s = "'" orelse s = "$"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   859
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   860
fun strip_blanks [] = []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   861
  | strip_blanks (" " :: ss) = strip_blanks ss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   862
  | strip_blanks [s1, " "] = [s1]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   863
  | strip_blanks (s1 :: " " :: s2 :: ss) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   864
    if is_ident_char s1 andalso is_ident_char s2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   865
      s1 :: " " :: strip_blanks (s2 :: ss)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   866
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   867
      strip_blanks (s1 :: s2 :: ss)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   868
  | strip_blanks (s :: ss) = s :: strip_blanks ss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   869
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   870
fun scan_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   871
fun scan_list scan = scan_non_empty_list scan || Scan.succeed []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   872
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   873
               >> (the o Int.fromString o space_implode "")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   874
val scan_rel_name = $$ "s" |-- scan_nat >> pair 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   875
                    || $$ "r" |-- scan_nat >> pair 2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   876
                    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   877
val scan_atom = $$ "A" |-- scan_nat
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   878
val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   879
val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   880
val scan_assignment = (scan_rel_name --| $$ "=") -- scan_tuple_set
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   881
val scan_instance = Scan.this_string "relations:" |--
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   882
                    $$ "{" |-- scan_list scan_assignment --| $$ "}"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   883
35336
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   884
val parse_instance =
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   885
  fst o Scan.finite Symbol.stopper
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   886
            (Scan.error (!! (fn _ =>
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   887
                                raise SYNTAX ("Kodkod.parse_instance",
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   888
                                              "ill-formed Kodkodi output"))
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   889
                            scan_instance))
ef3eba82465f cosmetics
blanchet
parents: 35333
diff changeset
   890
  o strip_blanks o explode
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   891
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   892
val problem_marker = "*** PROBLEM "
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   893
val outcome_marker = "---OUTCOME---\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   894
val instance_marker = "---INSTANCE---\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   895
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   896
fun read_section_body marker =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   897
  Substring.string o fst o Substring.position "\n\n"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   898
  o Substring.triml (size marker)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   899
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   900
fun read_next_instance s =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   901
  let val s = Substring.position instance_marker s |> snd in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   902
    if Substring.isEmpty s then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   903
      raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   904
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   905
      read_section_body instance_marker s |> parse_instance
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   906
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   907
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   908
fun read_next_outcomes j (s, ps, js) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   909
  let val (s1, s2) = Substring.position outcome_marker s in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   910
    if Substring.isEmpty s2 orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   911
       not (Substring.isEmpty (Substring.position problem_marker s1
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34124
diff changeset
   912
                               |> snd)) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   913
      (s, ps, js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   914
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   915
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   916
        val outcome = read_section_body outcome_marker s2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   917
        val s = Substring.triml (size outcome_marker) s2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   918
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   919
        if String.isSuffix "UNSATISFIABLE" outcome then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   920
          read_next_outcomes j (s, ps, j :: js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   921
        else if String.isSuffix "SATISFIABLE" outcome then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   922
          read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   923
        else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   924
          raise SYNTAX ("Kodkod.read_next_outcomes",
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   925
                        "unknown outcome " ^ quote outcome)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   926
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   927
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   928
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   929
fun read_next_problems (s, ps, js) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   930
  let val s = Substring.position problem_marker s |> snd in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   931
    if Substring.isEmpty s then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   932
      (ps, js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   933
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   934
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   935
        val s = Substring.triml (size problem_marker) s
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   936
        val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   937
                         |> Int.fromString |> the
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   938
        val j = j_plus_1 - 1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   939
      in read_next_problems (read_next_outcomes j (s, ps, js)) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   940
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   941
  handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   942
                                        "expected number after \"PROBLEM\"")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   943
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   944
fun read_output_file path =
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
   945
  (false, read_next_problems (Substring.full (File.read path), [], [])
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
   946
          |>> rev ||> rev)
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
   947
  handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   948
35718
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   949
(** Main Kodkod entry point **)
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   950
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   951
val created_temp_dir = Unsynchronized.ref false
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   952
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   953
fun serial_string_and_temporary_dir_for_overlord overlord =
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   954
  if overlord then
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   955
    ("", getenv "ISABELLE_HOME_USER")
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   956
  else
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   957
    let
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   958
      val dir = getenv "ISABELLE_TMP"
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   959
      val _ = if !created_temp_dir then ()
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   960
              else (created_temp_dir := true; File.mkdir (Path.explode dir))
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   961
    in (serial_string (), dir) end
eee1a5e0d334 moved some Nitpick code around
blanchet
parents: 35696
diff changeset
   962
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   963
(* The fudge term below is to account for Kodkodi's slow start-up time, which
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   964
   is partly due to the JVM and partly due to the ML "bash" function. *)
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   965
val fudge_ms = 250
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   966
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   967
fun milliseconds_until_deadline deadline =
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   968
  case deadline of
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   969
    NONE => ~1
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   970
  | SOME time =>
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   971
    Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms)
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   972
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   973
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
   974
                               problems =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   975
  let
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   976
    val j = find_index (curry (op =) True o #formula) problems
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   977
    val indexed_problems = if j >= 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   978
                             [(j, nth problems j)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   979
                           else
35187
3acab6c90d4a don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents: 35185
diff changeset
   980
                             filter_out (is_problem_trivially_false o snd)
3acab6c90d4a don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents: 35185
diff changeset
   981
                                        (0 upto length problems - 1 ~~ problems)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   982
    val triv_js = filter_out (AList.defined (op =) indexed_problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   983
                             (0 upto length problems - 1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   984
    val reindex = fst o nth indexed_problems
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   985
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   986
    if null indexed_problems then
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
   987
      Normal ([], triv_js, "")
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   988
    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   989
      let
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   990
        val (serial_str, temp_dir) =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   991
          serial_string_and_temporary_dir_for_overlord overlord
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   992
        fun path_for suf =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   993
          Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   994
        val in_path = path_for "kki"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   995
        val in_buf = Unsynchronized.ref Buffer.empty
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   996
        fun out s = Unsynchronized.change in_buf (Buffer.add s)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   997
        val out_path = path_for "out"
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   998
        val err_path = path_for "err"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   999
        val _ = write_problem_file out (map snd indexed_problems)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1000
        val _ = File.write_buffer in_path (!in_buf)
33575
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1001
        fun remove_temporary_files () =
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1002
          if overlord then ()
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1003
          else List.app (K () o try File.rm) [in_path, out_path, err_path]
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1004
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1005
        let
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1006
          val ms = milliseconds_until_deadline deadline
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1007
          val outcome =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1008
            let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1009
              val code =
35011
9e55e87434ff proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
wenzelm
parents: 35010
diff changeset
  1010
                bash ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^
35079
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1011
                      "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1012
                      \JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1013
                      \$JAVA_LIBRARY_PATH\" \
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1014
                      \LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1015
                      \$LD_LIBRARY_PATH\" \
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1016
                      \\"$KODKODI\"/bin/kodkodi" ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1017
                      (if ms >= 0 then " -max-msecs " ^ string_of_int ms
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1018
                       else "") ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1019
                      (if max_solutions > 1 then " -solve-all" else "") ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1020
                      " -max-solutions " ^ string_of_int max_solutions ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1021
                      (if max_threads > 0 then
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1022
                         " -max-threads " ^ string_of_int max_threads
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1023
                       else
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1024
                         "") ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1025
                      " < " ^ File.shell_path in_path ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1026
                      " > " ^ File.shell_path out_path ^
592edca1dfb3 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
blanchet
parents: 35011 35074
diff changeset
  1027
                      " 2> " ^ File.shell_path err_path)
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1028
              val (io_error, (ps, nontriv_js)) =
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1029
                read_output_file out_path
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1030
                ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1031
              val js = triv_js @ nontriv_js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1032
              val first_error =
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1033
                (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1034
                 handle IO.Io _ => "" | OS.SysErr _ => "")
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1035
                |> perhaps (try (unsuffix "\r"))
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1036
                |> perhaps (try (unsuffix "."))
36914
1806aa69bd62 recognize new Kodkod error message syntax
blanchet
parents: 36390
diff changeset
  1037
                |> perhaps (try (unprefix "Solve error: "))
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1038
                |> perhaps (try (unprefix "Error: "))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1039
            in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1040
              if null ps then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1041
                if code = 2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1042
                  TimedOut js
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
  1043
                else if code = 0 then
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
  1044
                  Normal ([], js, first_error)
33233
f9ff11344ec4 added friendly error message when Kodkodi is not available
blanchet
parents: 33232
diff changeset
  1045
                else if first_error |> Substring.full
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
  1046
                        |> Substring.position "exec: java" |> snd
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
  1047
                        |> Substring.isEmpty |> not then
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
  1048
                  JavaNotInstalled
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
  1049
                else if first_error |> Substring.full
33233
f9ff11344ec4 added friendly error message when Kodkodi is not available
blanchet
parents: 33232
diff changeset
  1050
                        |> Substring.position "NoClassDefFoundError" |> snd
f9ff11344ec4 added friendly error message when Kodkodi is not available
blanchet
parents: 33232
diff changeset
  1051
                        |> Substring.isEmpty |> not then
35696
17ae461d6133 show nice error message in Nitpick when "java" is not available
blanchet
parents: 35695
diff changeset
  1052
                  KodkodiNotInstalled
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1053
                else if first_error <> "" then
35695
80b2c22f8f00 fixed soundness bug in Nitpick
blanchet
parents: 35336
diff changeset
  1054
                  Error (first_error, js)
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1055
                else if io_error then
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1056
                  Error ("I/O error", js)
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
  1057
                else
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1058
                  Error ("Unknown error", js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1059
              else
35333
f61de25f71f9 distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents: 35309
diff changeset
  1060
                Normal (ps, js, first_error)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1061
            end
33575
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1062
        in remove_temporary_files (); outcome end
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1063
        handle Exn.Interrupt =>
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1064
               let
35309
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1065
                 val nontriv_js =
997aa3a3e4bb catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents: 35280
diff changeset
  1066
                   read_output_file out_path |> snd |> snd |> map reindex
33575
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1067
               in
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1068
                 (remove_temporary_files ();
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1069
                  Interrupted (SOME (triv_js @ nontriv_js)))
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1070
                 handle Exn.Interrupt =>
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1071
                        (remove_temporary_files (); Interrupted NONE)
118517551c12 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents: 33233
diff changeset
  1072
               end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1073
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1074
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1075
35814
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1076
val cached_outcome =
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1077
  Synchronized.var "Kodkod.cached_outcome"
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1078
                   (NONE : ((int * problem list) * outcome) option)
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1079
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1080
fun solve_any_problem overlord deadline max_threads max_solutions problems =
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1081
  let
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1082
    fun do_solve () = uncached_solve_any_problem overlord deadline max_threads
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1083
                                                 max_solutions problems
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1084
  in
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1085
    if overlord then
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1086
      do_solve ()
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1087
    else
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1088
      case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1089
                            max1 = max2 andalso length ps1 = length ps2 andalso
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1090
                            forall problems_equivalent (ps1 ~~ ps2))
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1091
                        (the_list (Synchronized.value cached_outcome))
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1092
                        (max_solutions, problems) of
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1093
        SOME outcome => outcome
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1094
      | NONE =>
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1095
        let val outcome = do_solve () in
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1096
          (case outcome of
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1097
             Normal (ps, js, "") =>
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1098
             Synchronized.change cached_outcome
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1099
                                 (K (SOME ((max_solutions, problems), outcome)))
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1100
           | _ => ());
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1101
          outcome
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1102
        end
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1103
  end
234eaa508359 added one-entry cache around Kodkod invocation
blanchet
parents: 35718
diff changeset
  1104
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
  1105
end;