src/HOL/Tools/Nitpick/nitpick_model.ML
author blanchet
Fri, 26 Feb 2010 18:38:23 +0100
changeset 35388 42d39948cace
parent 35385 29f81babefd7
child 35402 115a5a95710a
permissions -rw-r--r--
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33982
1ae222745c4a fixed paths in Nitpick's ML file headers
blanchet
parents: 33884
diff changeset
     1
(*  Title:      HOL/Tools/Nitpick/nitpick_model.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: 34974
diff changeset
     3
    Copyright   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
Model reconstruction for Nitpick.
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     6
*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     7
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     8
signature NITPICK_MODEL =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
     9
sig
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
    10
  type styp = Nitpick_Util.styp
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    11
  type scope = Nitpick_Scope.scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    12
  type rep = Nitpick_Rep.rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    13
  type nut = Nitpick_Nut.nut
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    14
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    15
  type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    16
    show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    17
    show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    18
    show_consts: bool}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    19
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    20
  structure NameTable : TABLE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    21
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    22
  val tuple_list_for_name :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    23
    nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    24
  val reconstruct_hol_model :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    25
    params -> scope -> (term option * int list) list -> styp list -> nut list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    26
    -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    27
    -> Pretty.T * bool
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    28
  val prove_hol_model :
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    29
    scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    30
    -> Kodkod.raw_bound list -> term -> bool option
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    31
end;
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    32
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    33
structure Nitpick_Model : NITPICK_MODEL =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    34
struct
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    35
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    36
open Nitpick_Util
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    37
open Nitpick_HOL
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    38
open Nitpick_Scope
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    39
open Nitpick_Peephole
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    40
open Nitpick_Rep
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
    41
open Nitpick_Nut
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    42
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    43
structure KK = Kodkod
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    44
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    45
type params = {
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    46
  show_skolems: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    47
  show_datatypes: bool,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    48
  show_consts: bool}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    49
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    50
val unknown = "?"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    51
val unrep = "\<dots>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    52
val maybe_mixfix = "_\<^sup>?"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    53
val base_mixfix = "_\<^bsub>base\<^esub>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    54
val step_mixfix = "_\<^bsub>step\<^esub>"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    55
val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
    56
val cyclic_co_val_name = "\<omega>"
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
    57
val cyclic_const_prefix = "\<xi>"
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
    58
val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
    59
val opt_flag = nitpick_prefix ^ "opt"
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
    60
val non_opt_flag = nitpick_prefix ^ "non_opt"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    61
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    62
type atom_pool = ((string * int) * int list) list
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    63
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    64
(* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    65
fun nth_atom_suffix pool s j k =
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    66
  (case AList.lookup (op =) (!pool) (s, k) of
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    67
     SOME js =>
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    68
     (case find_index (curry (op =) j) js of
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    69
        ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    70
               length js + 1)
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    71
      | n => length js - n)
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    72
   | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    73
  |> nat_subscript
33884
a0c43f185fef generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents: 33705
diff changeset
    74
  |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
a0c43f185fef generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents: 33705
diff changeset
    75
     ? prefix "\<^isub>,"
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    76
(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
    77
fun nth_atom_name pool prefix (Type (s, _)) j k =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
    78
    let val s' = shortest_name s in
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
    79
      prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    80
      nth_atom_suffix pool s j k
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
    81
    end
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
    82
  | nth_atom_name pool prefix (TFree (s, _)) j k =
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    83
    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    84
  | nth_atom_name _ _ T _ _ =
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    85
    raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    86
(* atom_pool Unsynchronized.ref -> bool -> typ -> int -> int -> term *)
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    87
fun nth_atom pool for_auto T j k =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    88
  if for_auto then
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    89
    Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    90
  else
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
    91
    Const (nth_atom_name pool "" T j k, T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    92
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    93
(* term -> real *)
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35086
diff changeset
    94
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    95
    real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    96
  | extract_real_number t = real (snd (HOLogic.dest_number t))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    97
(* term * term -> order *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    98
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    99
  | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   100
    handle TERM ("dest_number", _) =>
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   101
           case tp of
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   102
             (t11 $ t12, t21 $ t22) =>
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   103
             (case nice_term_ord (t11, t21) of
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   104
                EQUAL => nice_term_ord (t12, t22)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   105
              | ord => ord)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   106
           | _ => TermOrd.fast_term_ord tp
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   107
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   108
(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   109
fun tuple_list_for_name rel_table bounds name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   110
  the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   111
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   112
(* term -> term *)
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   113
fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   114
    unarize_and_unbox_term t1
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   115
  | unarize_and_unbox_term (Const (@{const_name PairBox},
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   116
                                   Type ("fun", [T1, Type ("fun", [T2, _])]))
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   117
                            $ t1 $ t2) =
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   118
    let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
      Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   120
      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
    end
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   122
  | unarize_and_unbox_term (Const (s, T)) =
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   123
    Const (s, unarize_unbox_and_uniterize_type T)
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   124
  | unarize_and_unbox_term (t1 $ t2) =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   125
    unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   126
  | unarize_and_unbox_term (Free (s, T)) =
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   127
    Free (s, unarize_unbox_and_uniterize_type T)
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   128
  | unarize_and_unbox_term (Var (x, T)) =
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   129
    Var (x, unarize_unbox_and_uniterize_type T)
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   130
  | unarize_and_unbox_term (Bound j) = Bound j
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   131
  | unarize_and_unbox_term (Abs (s, T, t')) =
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   132
    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   134
(* typ -> typ -> (typ * typ) * (typ * typ) *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   135
fun factor_out_types (T1 as Type ("*", [T11, T12]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   136
                     (T2 as Type ("*", [T21, T22])) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
    let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   138
      if n1 = n2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   139
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
          val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
          ((Type ("*", [T11, T11']), opt_T12'),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
           (Type ("*", [T21, T21']), opt_T22'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   144
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
      else if n1 < n2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   146
        case factor_out_types T1 T21 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   147
          (p1, (T21', NONE)) => (p1, (T21', SOME T22))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   148
        | (p1, (T21', SOME T22')) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   149
          (p1, (T21', SOME (Type ("*", [T22', T22]))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   150
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   151
        swap (factor_out_types T2 T1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   152
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   153
  | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   154
  | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   155
  | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
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
(* bool -> typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   158
fun make_plain_fun maybe_opt T1 T2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   159
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   160
    (* typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
    fun aux T1 T2 [] =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   162
        Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   163
      | aux T1 T2 ((t1, t2) :: ps) =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   164
        Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   165
        $ aux T1 T2 ps $ t1 $ t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   166
  in aux T1 T2 o rev end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   167
(* term -> bool *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   168
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   169
  | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   170
    is_plain_fun t0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   171
  | is_plain_fun _ = false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   172
(* term -> bool * (term list * term list) *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   173
val dest_plain_fun =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   174
  let
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   175
    (* term -> bool * (term list * term list) *)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   176
    fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   177
      | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
        let val (s, (ts1, ts2)) = aux t0 in (s, (t1 :: ts1, t2 :: ts2)) end
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   179
      | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
  in apsnd (pairself rev) o aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   181
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   182
(* typ -> typ -> typ -> term -> term * term *)
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   183
fun break_in_two T T1 T2 t =
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   184
  let
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   185
    val ps = HOLogic.flat_tupleT_paths T
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   186
    val cut = length (HOLogic.strip_tupleT T1)
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   187
    val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   188
    val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   189
  in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   190
(* typ -> term -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   191
fun pair_up (Type ("*", [T1', T2']))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   192
            (t1 as Const (@{const_name Pair},
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   193
                          Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
            t2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   195
    if T1 = T1' then HOLogic.mk_prod (t1, t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   196
    else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   197
  | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   198
(* typ -> term -> term list * term list -> (term * term) list*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   200
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
(* typ -> typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   202
fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   203
    let
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   204
      (* typ -> typ -> typ -> typ -> term -> term *)
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   205
      fun do_curry T1 T1a T1b T2 t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   206
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   207
          val (maybe_opt, ps) = dest_plain_fun t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   208
          val ps =
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   209
            ps |>> map (break_in_two T1 T1a T1b)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   210
               |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   211
               |> AList.coalesce (op =)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   212
               |> map (apsnd (make_plain_fun maybe_opt T1b T2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   213
        in make_plain_fun maybe_opt T1a (T1b --> T2) ps end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   214
      (* typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   215
      and do_uncurry T1 T2 t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   216
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   217
          val (maybe_opt, tsp) = dest_plain_fun t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   218
          val ps =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   219
            tsp |> op ~~
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   220
                |> maps (fn (t1, t2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   221
                            multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
        in make_plain_fun maybe_opt T1 T2 ps end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   223
      (* typ -> typ -> typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   224
      and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   225
        | do_arrow T1' T2' T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   226
                   (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
          Const (@{const_name fun_upd},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   228
                 (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   229
          $ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   230
        | do_arrow _ _ _ _ t =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   231
          raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   232
      and do_fun T1' T2' T1 T2 t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   233
        case factor_out_types T1' T1 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   234
          ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   235
        | ((_, NONE), (T1a, SOME T1b)) =>
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   236
          t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   237
        | ((T1a', SOME T1b'), (_, NONE)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   238
          t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   239
        | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   240
      (* typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   241
      and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
          do_fun T1' T2' T1 T2 t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   243
        | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   244
                  (Const (@{const_name Pair}, _) $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
          Const (@{const_name Pair}, Ts' ---> T')
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   246
          $ do_term T1' T1 t1 $ do_term T2' T2 t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   247
        | do_term T' T t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   248
          if T = T' then t
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   249
          else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   250
    in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   251
  | typecast_fun T' _ _ _ =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   252
    raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   253
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   254
(* term -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   255
fun truth_const_sort_key @{const True} = "0"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   256
  | truth_const_sort_key @{const False} = "2"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   257
  | truth_const_sort_key _ = "1"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   258
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   259
(* typ -> term list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   260
fun mk_tuple (Type ("*", [T1, T2])) ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   261
    HOLogic.mk_prod (mk_tuple T1 ts,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   262
        mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   263
  | mk_tuple _ (t :: _) = t
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   264
  | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   265
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   266
(* bool -> atom_pool -> (string * string) * (string * string) -> scope
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   267
   -> nut list -> nut list -> nut list -> nut NameTable.table
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   268
   -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   269
fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   270
        ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   271
          ofs, ...} : scope) sel_names rel_table bounds =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   272
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   273
    val for_auto = (maybe_name = "")
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   274
    (* int list list -> int *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   275
    fun value_of_bits jss =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   276
      let
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   277
        val j0 = offset_of_type ofs @{typ unsigned_bit}
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   278
        val js = map (Integer.add (~ j0) o the_single) jss
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   279
      in
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   280
        fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   281
             js 0
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   282
      end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   283
    (* bool -> typ -> typ -> (term * term) list -> term *)
35388
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   284
    fun make_set maybe_opt T1 T2 tps =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   285
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
        val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   287
        val insert_const = Const (@{const_name insert},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   288
                                  T1 --> (T1 --> T2) --> T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   289
        (* (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
        fun aux [] =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   291
            if maybe_opt andalso not (is_complete_type datatypes false T1) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   292
              insert_const $ Const (unrep, T1) $ empty_const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   293
            else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   294
              empty_const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   295
          | aux ((t1, t2) :: zs) =
35388
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   296
            aux zs
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   297
            |> t2 <> @{const False}
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   298
               ? curry (op $)
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   299
                       (insert_const
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   300
                        $ (t1 |> t2 <> @{const True}
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   301
                                 ? curry (op $)
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   302
                                         (Const (maybe_name, T1 --> T1))))
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   303
      in
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   304
        if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   305
                  tps then
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   306
          Const (unknown, T1 --> T2)
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   307
        else
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   308
          aux tps
42d39948cace use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
blanchet
parents: 35385
diff changeset
   309
      end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   310
    (* typ -> typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
    fun make_map T1 T2 T2' =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   312
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   313
        val update_const = Const (@{const_name fun_upd},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   314
                                  (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   315
        (* (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   316
        fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   317
          | aux' ((t1, t2) :: ps) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   318
            (case t2 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   319
               Const (@{const_name None}, _) => aux' ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   320
             | _ => update_const $ aux' ps $ t1 $ t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   321
        fun aux ps =
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   322
          if not (is_complete_type datatypes false T1) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   323
            update_const $ aux' ps $ Const (unrep, T1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   324
            $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   325
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   326
            aux' ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   327
      in aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
    (* typ list -> term -> term *)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   329
    fun polish_funs Ts t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   330
      (case fastype_of1 (Ts, t) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   331
         Type ("fun", [T1, T2]) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   332
         if is_plain_fun t then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   333
           case T2 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   334
             @{typ bool} =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   335
             let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   336
               val (maybe_opt, ts_pair) =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   337
                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   338
             in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   339
               make_set maybe_opt T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   340
                        (sort_wrt (truth_const_sort_key o snd) (op ~~ ts_pair))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   341
             end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   342
           | Type (@{type_name option}, [T2']) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   343
             let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   344
               val ts_pair = snd (dest_plain_fun t)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   345
                             |> pairself (map (polish_funs Ts))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   346
             in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   347
           | _ => raise SAME ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   348
         else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   349
           raise SAME ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   350
       | _ => raise SAME ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   351
      handle SAME () =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   352
             case t of
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   353
               (t1 as Const (@{const_name fun_upd}, _) $ t11 $ _)
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   354
               $ (t2 as Const (s, _)) =>
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   355
               if s = unknown then polish_funs Ts t11
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   356
               else polish_funs Ts t1 $ polish_funs Ts t2
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   357
             | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   358
             | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   359
             | Const (s, Type ("fun", [T1, T2])) =>
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   360
               if s = opt_flag orelse s = non_opt_flag then
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   361
                 Abs ("x", T1, Const (unknown, T2))
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   362
               else
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   363
                 t
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   364
             | t => t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   365
    (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   366
    fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   367
      ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   368
                 |> make_plain_fun maybe_opt T1 T2
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   369
                 |> unarize_and_unbox_term
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   370
                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   371
                                 (unarize_unbox_and_uniterize_type T1)
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   372
                                 (unarize_unbox_and_uniterize_type T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   373
    (* (typ * int) list -> typ -> typ -> int -> term *)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   374
    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   375
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   376
          val k1 = card_of_type card_assigns T1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   377
          val k2 = card_of_type card_assigns T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   378
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   379
          term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   380
                       [nth_combination (replicate k1 (k2, 0)) j]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   381
          handle General.Subscript =>
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   382
                 raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   383
                            signed_string_of_int j ^ " for " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   384
                            string_for_rep (Vect (k1, Atom (k2, 0))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   385
        end
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   386
      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   387
        let
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   388
          val k1 = card_of_type card_assigns T1
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   389
          val k2 = k div k1
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   390
        in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   391
          list_comb (HOLogic.pair_const T1 T2,
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   392
                     map3 (fn T => term_for_atom seen T T) [T1, T2]
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   393
                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   394
        end
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   395
      | term_for_atom seen @{typ prop} _ j k =
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   396
        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   397
      | term_for_atom _ @{typ bool} _ j _ =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   398
        if j = 0 then @{const False} else @{const True}
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   399
      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   400
      | term_for_atom seen T _ j k =
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   401
        if T = nat_T andalso is_standard_datatype thy stds nat_T then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   402
          HOLogic.mk_number nat_T j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
        else if T = int_T then
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   404
          HOLogic.mk_number int_T (int_for_atom (k, 0) j)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   405
        else if is_fp_iterator_type T then
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   406
          HOLogic.mk_number nat_T (k - j - 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   407
        else if T = @{typ bisim_iterator} then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   408
          HOLogic.mk_number nat_T j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   409
        else case datatype_spec datatypes T of
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
   410
          NONE => nth_atom pool for_auto T j k
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
   411
        | SOME {deep = false, ...} => nth_atom pool for_auto T j k
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   412
        | SOME {co, standard, constrs, ...} =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   413
          let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   414
            (* styp -> int list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   415
            fun tuples_for_const (s, T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   416
              tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   417
            (* unit -> term *)
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   418
            fun cyclic_atom () =
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   419
              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   420
            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   421
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   422
            val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   423
                                 constrs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   424
            val real_j = j + offset_of_type ofs T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   425
            val constr_x as (constr_s, constr_T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   426
              get_first (fn (jss, {const, ...}) =>
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   427
                            if member (op =) jss [real_j] then SOME const
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   428
                            else NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   429
                        (discr_jsss ~~ constrs) |> the
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   430
            val arg_Ts = curried_binder_types constr_T
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   431
            val sel_xs =
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   432
              map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   433
                                                          constr_x)
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   434
                  (index_seq 0 (length arg_Ts))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   435
            val sel_Rs =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   436
              map (fn x => get_first
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
                               (fn ConstName (s', T', R) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
                                   if (s', T') = x then SOME R else NONE
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   439
                                 | u => raise NUT ("Nitpick_Model.reconstruct_\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   440
                                                   \term.term_for_atom", [u]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
                               sel_names |> the) sel_xs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
            val arg_Rs = map (snd o dest_Func) sel_Rs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   443
            val sel_jsss = map tuples_for_const sel_xs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   444
            val arg_jsss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   445
              map (map_filter (fn js => if hd js = real_j then SOME (tl js)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   446
                                        else NONE)) sel_jsss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
            val uncur_arg_Ts = binder_types constr_T
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   448
            val maybe_cyclic = co orelse not standard
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   449
          in
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   450
            if maybe_cyclic andalso not (null seen) andalso
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   451
               member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   452
              cyclic_var ()
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   453
            else if constr_s = @{const_name Word} then
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   454
              HOLogic.mk_number
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   455
                  (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   456
                  (value_of_bits (the_single arg_jsss))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   457
            else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   458
              let
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   459
                val seen = seen |> maybe_cyclic ? cons (T, j)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   460
                val ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   461
                  if length arg_Ts = 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   462
                    []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   463
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   464
                    map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   465
                         arg_jsss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   466
                    |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   467
                    |> dest_n_tuple (length uncur_arg_Ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   468
                val t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   469
                  if constr_s = @{const_name Abs_Frac} then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   470
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   471
                      val num_T = body_type T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   472
                      (* int -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   473
                      val mk_num = HOLogic.mk_number num_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
                    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   475
                      case ts of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   477
                        (case snd (HOLogic.dest_number t1) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
                           0 => mk_num 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
                         | n1 => case HOLogic.dest_number t2 |> snd of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
                                   1 => mk_num n1
35177
168041f24f80 various cosmetic changes to Nitpick
blanchet
parents: 35086
diff changeset
   481
                                 | n2 => Const (@{const_name divide},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   482
                                                num_T --> num_T --> num_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   483
                                         $ mk_num n1 $ mk_num n2)
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   484
                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   485
                                         \term_for_atom (Abs_Frac)", ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   486
                    end
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   487
                  else if not for_auto andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   488
                          (is_abs_fun thy constr_x orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   489
                           constr_s = @{const_name Quot}) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   490
                    Const (abs_name, constr_T) $ the_single ts
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   491
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   492
                    list_comb (Const constr_x, ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   493
              in
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   494
                if maybe_cyclic then
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   495
                  let val var = cyclic_var () in
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   496
                    if unfold andalso not standard andalso
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   497
                       length seen = 1 andalso
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   498
                       exists_subterm (fn Const (s, _) =>
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   499
                                          String.isPrefix cyclic_const_prefix s
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   500
                                        | t' => t' = var) t then
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   501
                      subst_atomic [(var, cyclic_atom ())] t
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   502
                    else if exists_subterm (curry (op =) var) t then
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   503
                      if co then
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   504
                        Const (@{const_name The}, (T --> bool_T) --> T)
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   505
                        $ Abs (cyclic_co_val_name, T,
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   506
                               Const (@{const_name "op ="}, T --> T --> bool_T)
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   507
                               $ Bound 0 $ abstract_over (var, t))
35179
4b198af5beb5 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
blanchet
parents: 35177
diff changeset
   508
                      else
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   509
                        cyclic_atom ()
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
                    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   511
                      t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   512
                  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
                else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   514
                  t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   515
              end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
          end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   517
    (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
       -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   519
    and term_for_vect seen k R T1 T2 T' js =
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   520
      make_fun true T1 T2 T'
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   521
               (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
               (map (term_for_rep seen T2 T2 R o single)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   523
                    (batch_list (arity_of_rep R) js))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   524
    (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   525
    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   526
      | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   527
        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   528
        else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
      | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   530
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
          val arity1 = arity_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
          val (js1, js2) = chop arity1 js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   533
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
          list_comb (HOLogic.pair_const T1 T2,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
                     map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
                          [[js1], [js2]])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
        end
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   538
      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
        term_for_vect seen k R' T1 T2 T' js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
                     jss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   542
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   543
          val jss1 = all_combinations_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   544
          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
          val ts2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   546
            map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   547
                                       [[int_from_bool (member (op =) jss js)]])
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   548
                jss1
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   549
        in make_fun false T1 T2 T' ts1 ts2 end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   550
      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   552
          val arity1 = arity_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   553
          val jss1 = all_combinations_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   555
          val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   556
          val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
                         o AList.lookup (op =) grouped_jss2) jss1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   558
        in make_fun true T1 T2 T' ts1 ts2 end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   559
      | term_for_rep seen T T' (Opt R) jss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
        if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   561
      | term_for_rep _ T _ R jss =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   562
        raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
                   Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   564
                   string_of_int (length jss))
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   565
  in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   566
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   567
(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   568
   -> nut -> term *)
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   569
fun term_for_name pool scope sel_names rel_table bounds name =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   570
  let val T = type_of name in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   571
    tuple_list_for_name rel_table bounds name
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   572
    |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   573
                        rel_table bounds T T (rep_of name)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   574
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   575
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   576
(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   577
fun add_wacky_syntax ctxt =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   578
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   579
    (* term -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   580
    val name_of = fst o dest_Const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   581
    val thy = ProofContext.theory_of ctxt |> Context.reject_draft
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   582
    val (maybe_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   583
      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   584
                          Mixfix (maybe_mixfix, [1000], 1000)) thy
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   585
    val (abs_t, thy) =
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   586
      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   587
                          Mixfix (abs_mixfix, [40], 40)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   588
    val (base_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   589
      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   590
                          Mixfix (base_mixfix, [1000], 1000)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   591
    val (step_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   592
      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   593
                          Mixfix (step_mixfix, [1000], 1000)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   594
  in
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   595
    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   596
     ProofContext.transfer_syntax thy ctxt)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   597
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   598
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   599
(* term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   600
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   601
                                   $ Abs (s, T, Const (@{const_name "op ="}, _)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
                                                $ Bound 0 $ t')) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
    betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   604
  | unfold_outer_the_binders t = t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
(* typ list -> int -> term * term -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   606
fun bisimilar_values _ 0 _ = true
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   607
  | bisimilar_values coTs max_depth (t1, t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   608
    let val T = fastype_of t1 in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   609
      if exists_subtype (member (op =) coTs) T then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   610
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   611
          val ((head1, args1), (head2, args2)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   612
            pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   613
          val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   614
        in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   615
          head1 = head2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   616
          forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   617
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   618
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   619
        t1 = t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   620
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   621
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
(* params -> scope -> (term option * int list) list -> styp list -> nut list
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   623
  -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   624
  -> Pretty.T * bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   625
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   626
        ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   627
                      debug, binary_ints, destroy_constrs, specialize,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   628
                      skolemize, star_linear_preds, uncurry, fast_descrs,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   629
                      tac_timeout, evals, case_names, def_table, nondef_table,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   630
                      user_nondefs, simp_table, psimp_table, intro_table,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   631
                      ground_thm_table, ersatz_table, skolems, special_funs,
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   632
                      unrolled_preds, wf_cache, constr_cache},
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   633
         binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   634
        formats all_frees free_names sel_names nonsel_names rel_table bounds =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
  let
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   636
    val pool = Unsynchronized.ref []
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   637
    val (wacky_names as (_, base_step_names), ctxt) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   638
      add_wacky_syntax ctxt
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   639
    val hol_ctxt =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   640
      {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   641
       stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   642
       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   643
       specialize = specialize, skolemize = skolemize,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   644
       star_linear_preds = star_linear_preds, uncurry = uncurry,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   645
       fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   646
       case_names = case_names, def_table = def_table,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   647
       nondef_table = nondef_table, user_nondefs = user_nondefs,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   648
       simp_table = simp_table, psimp_table = psimp_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   649
       intro_table = intro_table, ground_thm_table = ground_thm_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   650
       ersatz_table = ersatz_table, skolems = skolems,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
       special_funs = special_funs, unrolled_preds = unrolled_preds,
33580
45c33e97cb86 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents: 33571
diff changeset
   652
       wf_cache = wf_cache, constr_cache = constr_cache}
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   653
    val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   654
                 card_assigns = card_assigns, bits = bits,
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   655
                 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   656
    (* bool -> typ -> typ -> rep -> int list list -> term *)
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   657
    fun term_for_rep unfold =
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   658
      reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   659
    (* nat -> typ -> nat -> term *)
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   660
    fun nth_value_of_type card T n =
35188
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   661
      let
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   662
        (* bool -> term *)
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   663
        fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   664
      in
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   665
        case aux false of
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   666
          t as Const (s, _) =>
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   667
          if String.isPrefix cyclic_const_prefix s then
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   668
            HOLogic.mk_eq (t, aux true)
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   669
          else
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   670
            t
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   671
        | t => t
8c70a34931b1 improve Nitpick's "Datatypes" rendering for elements containing cycles
blanchet
parents: 35180
diff changeset
   672
      end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   673
    (* nat -> typ -> typ list *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   674
    fun all_values_of_type card T =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   675
      index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   676
    (* dtype_spec list -> dtype_spec -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   677
    fun is_codatatype_wellformed (cos : dtype_spec list)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   678
                                 ({typ, card, ...} : dtype_spec) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   679
      let
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   680
        val ts = all_values_of_type card typ
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   681
        val max_depth = Integer.sum (map #card cos)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   682
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   683
        forall (not o bisimilar_values (map #typ cos) max_depth)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   684
               (all_distinct_unordered_pairs_of ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   685
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   686
    (* string -> Pretty.T *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   687
    fun pretty_for_assign name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   688
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   689
        val (oper, (t1, T'), T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   690
          case name of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   691
            FreeName (s, T, _) =>
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   692
            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   693
              ("=", (t, format_term_type thy def_table formats t), T)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   694
            end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   695
          | ConstName (s, T, _) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   696
            (assign_operator_for_const (s, T),
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   697
             user_friendly_const hol_ctxt base_step_names formats (s, T), T)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   698
          | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   699
                            \pretty_for_assign", [name])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   700
        val t2 = if rep_of name = Any then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   701
                   Const (@{const_name undefined}, T')
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   702
                 else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   703
                   tuple_list_for_name rel_table bounds name
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   704
                   |> term_for_rep false T T' (rep_of name)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   705
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   706
        Pretty.block (Pretty.breaks
33571
3655e51f9958 minor cleanup in Nitpick
blanchet
parents: 33565
diff changeset
   707
            [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   708
             Pretty.str oper, Syntax.pretty_term ctxt t2])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   709
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   710
    (* dtype_spec -> Pretty.T *)
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   711
    fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   712
      Pretty.block (Pretty.breaks
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   713
          [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   714
           Pretty.str "=",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   715
           Pretty.enum "," "{" "}"
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   716
               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   717
                (if fun_from_pair complete false then []
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   718
                 else [Pretty.str unrep]))])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   719
    (* typ -> dtype_spec list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   720
    fun integer_datatype T =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
      [{typ = T, card = card_of_type card_assigns T, co = false,
35385
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   722
        standard = true, complete = (false, false), concrete = (true, true),
29f81babefd7 improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents: 35280
diff changeset
   723
        deep = true, constrs = []}]
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   724
      handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   725
    val (codatatypes, datatypes) =
34982
7b8c366e34a2 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents: 34974
diff changeset
   726
      datatypes |> filter #deep |> List.partition #co
35220
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   727
                ||> append (integer_datatype int_T
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   728
                            |> is_standard_datatype thy stds nat_T
2bcdae5f4fdb added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents: 35190
diff changeset
   729
                               ? append (integer_datatype nat_T))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   730
    val block_of_datatypes =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   731
      if show_datatypes andalso not (null datatypes) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   732
        [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   733
                         (map pretty_for_datatype datatypes)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   735
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   736
    val block_of_codatatypes =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
      if show_datatypes andalso not (null codatatypes) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   738
        [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   739
                         (map pretty_for_datatype codatatypes)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   740
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   741
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   742
    (* bool -> string -> nut list -> Pretty.T list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   743
    fun block_of_names show title names =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   744
      if show andalso not (null names) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   745
        Pretty.str (title ^ plural_s_for_list names ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   746
        :: map (Pretty.indent indent_size o pretty_for_assign)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   747
               (sort_wrt (original_name o nickname_of) names)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   748
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   749
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   750
    val (skolem_names, nonskolem_nonsel_names) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   751
      List.partition is_skolem_name nonsel_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   752
    val (eval_names, noneval_nonskolem_nonsel_names) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   753
      List.partition (String.isPrefix eval_prefix o nickname_of)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   754
                     nonskolem_nonsel_names
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   755
      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   756
                      o nickname_of)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
    val free_names =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   758
      map (fn x as (s, T) =>
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   759
              case filter (curry (op =) x
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   760
                       o pairf nickname_of
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   761
                               (unarize_unbox_and_uniterize_type o type_of))
35190
ce653cc27a94 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents: 35188
diff changeset
   762
                       free_names of
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   763
                [name] => name
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   764
              | [] => FreeName (s, T, Any)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   765
              | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   766
                                 [Const x])) all_frees
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   767
    val chunks = block_of_names true "Free variable" free_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   768
                 block_of_names show_skolems "Skolem constant" skolem_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   769
                 block_of_names true "Evaluated term" eval_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   770
                 block_of_datatypes @ block_of_codatatypes @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   771
                 block_of_names show_consts "Constant"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   772
                                noneval_nonskolem_nonsel_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   773
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   774
    (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   775
                    else chunks),
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   776
     bisim_depth >= 0 orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   777
     forall (is_codatatype_wellformed codatatypes) codatatypes)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   779
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   780
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   781
   -> KK.raw_bound list -> term -> bool option *)
35280
54ab4921f826 fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents: 35220
diff changeset
   782
fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   783
                               card_assigns, ...})
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   784
                    auto_timeout free_names sel_names rel_table bounds prop =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   785
  let
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
   786
    val pool = Unsynchronized.ref []
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   787
    (* typ * int -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   788
    fun free_type_assm (T, k) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   789
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   790
        (* int -> term *)
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35075
diff changeset
   791
        fun atom j = nth_atom pool true T j k
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   792
        fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   793
        val eqs = map equation_for_atom (index_seq 0 k)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   794
        val compreh_assm =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   795
          Const (@{const_name All}, (T --> bool_T) --> bool_T)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   796
              $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   797
        val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   798
      in s_conj (compreh_assm, distinct_assm) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   799
    (* nut -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   800
    fun free_name_assm name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   801
      HOLogic.mk_eq (Free (nickname_of name, type_of name),
35180
c57dba973391 more work on Nitpick's support for nonstandard models + fix in model reconstruction
blanchet
parents: 35179
diff changeset
   802
                     term_for_name pool scope sel_names rel_table bounds name)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   803
    val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   804
    val model_assms = map free_name_assm free_names
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   805
    val assm = foldr1 s_conj (freeT_assms @ model_assms)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   806
    (* bool -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   807
    fun try_out negate =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   808
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   809
        val concl = (negate ? curry (op $) @{const Not})
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   810
                    (ObjectLogic.atomize_term thy prop)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   811
        val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   812
                   |> map_types (map_type_tfree
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   813
                                     (fn (s, []) => TFree (s, HOLogic.typeS)
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   814
                                       | x => TFree x))
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   815
       val _ = if debug then
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   816
                 priority ((if negate then "Genuineness" else "Spuriousness") ^
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   817
                           " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   818
               else
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   819
                 ()
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   820
        val goal = prop |> cterm_of thy |> Goal.init
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   821
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   822
        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   823
                                        (auto_tac (clasimpset_of ctxt)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   824
              |> the |> Goal.finish ctxt; true)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   825
        handle THM _ => false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   826
             | TimeLimit.TimeOut => false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   827
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   828
  in
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   829
    if try_out false then SOME true
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   830
    else if try_out true then SOME false
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   831
    else NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   832
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   833
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   834
end;