src/HOL/Tools/Nitpick/nitpick_model.ML
author blanchet
Fri, 05 Feb 2010 12:04:54 +0100
changeset 35075 888802be2019
parent 35070 96136eb6218f
child 35076 cc19e2aef17e
permissions -rw-r--r--
handle Nitpick's nonstandard model enumeration in a cleaner way; and renumber the atoms so that we get more often a_1 and a_2 and less often a_{n-1} and a_{n-2} in counterexamples
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>"
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
    56
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
    57
val non_opt_flag = nitpick_prefix ^ "non_opt"
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    58
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    59
(* string -> int -> int -> string *)
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    60
fun nth_atom_suffix s j k =
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    61
  nat_subscript (k - j)
33884
a0c43f185fef generate clearer atom names in Nitpick for types that end with a digit;
blanchet
parents: 33705
diff changeset
    62
  |> (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
    63
     ? prefix "\<^isub>,"
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    64
(* string -> typ -> int -> int -> string *)
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    65
fun nth_atom_name prefix (T as 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
    66
    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
    67
      prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    68
      nth_atom_suffix 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
    69
    end
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    70
  | nth_atom_name prefix (T as TFree (s, _)) j k =
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    71
    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    72
  | nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    73
(* bool -> typ -> int -> int -> term *)
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    74
fun nth_atom for_auto T j k =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    75
  if for_auto then
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    76
    Free (nth_atom_name (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
    77
  else
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
    78
    Const (nth_atom_name "" T j k, T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    79
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    80
(* term -> real *)
34974
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34936
diff changeset
    81
fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    82
    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
    83
  | 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
    84
(* term * term -> order *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    85
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
    86
  | 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
    87
    handle TERM ("dest_number", _) =>
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    88
           case tp of
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    89
             (t11 $ t12, t21 $ t22) =>
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    90
             (case nice_term_ord (t11, t21) of
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    91
                EQUAL => nice_term_ord (t12, t22)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    92
              | ord => ord)
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    93
           | _ => TermOrd.fast_term_ord tp
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
    94
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
    95
(* 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
    96
fun tuple_list_for_name rel_table bounds name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    97
  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
    98
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
    99
(* term -> term *)
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   100
fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   101
    unbit_and_unbox_term t1
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   102
  | unbit_and_unbox_term (Const (@{const_name PairBox},
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   103
                          Type ("fun", [T1, Type ("fun", [T2, T3])]))
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   104
                          $ t1 $ t2) =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   105
    let val Ts = map unbit_and_unbox_type [T1, T2] in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   106
      Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   107
      $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   108
    end
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   109
  | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   110
  | unbit_and_unbox_term (t1 $ t2) =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   111
    unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   112
  | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   113
  | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   114
  | unbit_and_unbox_term (Bound j) = Bound j
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   115
  | unbit_and_unbox_term (Abs (s, T, t')) =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   116
    Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   117
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   118
(* typ -> typ -> (typ * typ) * (typ * typ) *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   119
fun factor_out_types (T1 as Type ("*", [T11, T12]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   120
                     (T2 as Type ("*", [T21, T22])) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   121
    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
   122
      if n1 = n2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   123
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   124
          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
   125
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   126
          ((Type ("*", [T11, T11']), opt_T12'),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   127
           (Type ("*", [T21, T21']), opt_T22'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   128
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   129
      else if n1 < n2 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   130
        case factor_out_types T1 T21 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   131
          (p1, (T21', NONE)) => (p1, (T21', SOME T22))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   132
        | (p1, (T21', SOME T22')) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   133
          (p1, (T21', SOME (Type ("*", [T22', T22]))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   134
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   135
        swap (factor_out_types T2 T1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   136
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   137
  | 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
   138
  | 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
   139
  | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   140
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   141
(* bool -> typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   142
fun make_plain_fun maybe_opt T1 T2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   143
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   144
    (* typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   145
    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
   146
        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
   147
      | aux T1 T2 ((t1, t2) :: ps) =
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   148
        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
   149
        $ aux T1 T2 ps $ t1 $ t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   150
  in aux T1 T2 o rev end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   151
(* 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
   152
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
   153
  | is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   154
    is_plain_fun t0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   155
  | is_plain_fun _ = false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   156
(* term -> bool * (term list * term list) *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   157
val dest_plain_fun =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   158
  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
   159
    (* 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
   160
    fun aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   161
      | aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   162
        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
   163
      | 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
   164
  in apsnd (pairself rev) o aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   165
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   166
(* 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
   167
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
   168
  let
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   169
    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
   170
    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
   171
    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
   172
    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
   173
  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
   174
(* typ -> term -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   175
fun pair_up (Type ("*", [T1', T2']))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   176
            (t1 as Const (@{const_name Pair},
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   177
                          Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   178
            t2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   179
    if T1 = T1' then HOLogic.mk_prod (t1, t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   180
    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
   181
  | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   182
(* typ -> term -> term list * term list -> (term * term) list*)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   183
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
   184
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   185
(* typ -> typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   186
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
   187
    let
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   188
      (* 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
   189
      fun do_curry T1 T1a T1b T2 t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   190
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   191
          val (maybe_opt, ps) = dest_plain_fun t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   192
          val ps =
33565
5fad8e36dfb1 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet
parents: 33558
diff changeset
   193
            ps |>> map (break_in_two T1 T1a T1b)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   194
               |> 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
   195
               |> AList.coalesce (op =)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   196
               |> map (apsnd (make_plain_fun maybe_opt T1b T2))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   197
        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
   198
      (* typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   199
      and do_uncurry T1 T2 t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   200
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   201
          val (maybe_opt, tsp) = dest_plain_fun t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   202
          val ps =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   203
            tsp |> op ~~
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   204
                |> maps (fn (t1, t2) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   205
                            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
   206
        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
   207
      (* typ -> typ -> typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   208
      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
   209
        | do_arrow T1' T2' T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   210
                   (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   211
          Const (@{const_name fun_upd},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   212
                 (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   213
          $ 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
   214
        | do_arrow _ _ _ _ t =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   215
          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
   216
      and do_fun T1' T2' T1 T2 t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   217
        case factor_out_types T1' T1 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   218
          ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   219
        | ((_, 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
   220
          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
   221
        | ((T1a', SOME T1b'), (_, NONE)) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   222
          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
   223
        | _ => 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
   224
      (* typ -> typ -> term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   225
      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
   226
          do_fun T1' T2' T1 T2 t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   227
        | 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
   228
                  (Const (@{const_name Pair}, _) $ t1 $ t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   229
          Const (@{const_name Pair}, Ts' ---> T')
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   230
          $ 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
   231
        | do_term T' T t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   232
          if T = T' then t
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   233
          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
   234
    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
   235
  | typecast_fun T' _ _ _ =
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   236
    raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   237
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   238
(* term -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   239
fun truth_const_sort_key @{const True} = "0"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   240
  | truth_const_sort_key @{const False} = "2"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   241
  | truth_const_sort_key _ = "1"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   242
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   243
(* typ -> term list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   244
fun mk_tuple (Type ("*", [T1, T2])) ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   245
    HOLogic.mk_prod (mk_tuple T1 ts,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   246
        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
   247
  | mk_tuple _ (t :: _) = t
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   248
  | 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
   249
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   250
(* string * string * string * string -> scope -> nut list -> nut list
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   251
   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   252
   -> int list list -> term *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   253
fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   254
        ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   255
         : scope) sel_names rel_table bounds =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   256
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   257
    val for_auto = (maybe_name = "")
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   258
    (* int list list -> int *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   259
    fun value_of_bits jss =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   260
      let
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   261
        val j0 = offset_of_type ofs @{typ unsigned_bit}
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   262
        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
   263
      in
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   264
        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
   265
             js 0
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   266
      end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   267
    (* bool -> typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   268
    fun make_set maybe_opt T1 T2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   269
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   270
        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
   271
        val insert_const = Const (@{const_name insert},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   272
                                  T1 --> (T1 --> T2) --> T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   273
        (* (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   274
        fun aux [] =
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   275
            if maybe_opt andalso not (is_complete_type datatypes T1) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   276
              insert_const $ Const (unrep, T1) $ empty_const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   277
            else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   278
              empty_const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   279
          | aux ((t1, t2) :: zs) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   280
            aux zs |> t2 <> @{const False}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   281
                      ? curry (op $) (insert_const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   282
                                      $ (t1 |> t2 <> @{const True}
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   283
                                               ? curry (op $)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   284
                                                       (Const (maybe_name,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   285
                                                               T1 --> T1))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   286
      in aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   287
    (* typ -> typ -> typ -> (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   288
    fun make_map T1 T2 T2' =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   289
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   290
        val update_const = Const (@{const_name fun_upd},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   291
                                  (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   292
        (* (term * term) list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   293
        fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   294
          | aux' ((t1, t2) :: ps) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   295
            (case t2 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   296
               Const (@{const_name None}, _) => aux' ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   297
             | _ => update_const $ aux' ps $ t1 $ t2)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   298
        fun aux ps =
34123
c4988215a691 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents: 34121
diff changeset
   299
          if not (is_complete_type datatypes T1) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   300
            update_const $ aux' ps $ Const (unrep, T1)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   301
            $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   302
          else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   303
            aux' ps
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   304
      in aux end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   305
    (* 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
   306
    fun polish_funs Ts t =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   307
      (case fastype_of1 (Ts, t) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   308
         Type ("fun", [T1, T2]) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   309
         if is_plain_fun t then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   310
           case T2 of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   311
             @{typ bool} =>
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 (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
   314
                 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
   315
             in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   316
               make_set maybe_opt T1 T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   317
                        (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
   318
             end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   319
           | Type (@{type_name option}, [T2']) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   320
             let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   321
               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
   322
                             |> pairself (map (polish_funs Ts))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   323
             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
   324
           | _ => raise SAME ()
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
           raise SAME ()
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   327
       | _ => raise SAME ())
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   328
      handle SAME () =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   329
             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
   330
               (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
   331
               $ (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
   332
               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
   333
               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
   334
             | 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
   335
             | 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
   336
             | 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
   337
               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
   338
                 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
   339
               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
   340
                 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
   341
             | t => t
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   342
    (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   343
    fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   344
      ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   345
                 |> make_plain_fun maybe_opt T1 T2
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   346
                 |> unbit_and_unbox_term
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   347
                 |> typecast_fun (unbit_and_unbox_type T')
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   348
                                 (unbit_and_unbox_type T1)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   349
                                 (unbit_and_unbox_type T2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   350
    (* (typ * int) list -> typ -> typ -> int -> term *)
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   351
    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   352
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   353
          val k1 = card_of_type card_assigns T1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   354
          val k2 = card_of_type card_assigns T2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   355
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   356
          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
   357
                       [nth_combination (replicate k1 (k2, 0)) j]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   358
          handle General.Subscript =>
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   359
                 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
   360
                            signed_string_of_int j ^ " for " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   361
                            string_for_rep (Vect (k1, Atom (k2, 0))))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   362
        end
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   363
      | 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
   364
        let
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   365
          val k1 = card_of_type card_assigns T1
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   366
          val k2 = k div k1
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   367
        in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   368
          list_comb (HOLogic.pair_const T1 T2,
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   369
                     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
   370
                          [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
   371
        end
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   372
      | term_for_atom seen @{typ prop} _ j k =
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   373
        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
   374
      | term_for_atom _ @{typ bool} _ j _ =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   375
        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
   376
      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   377
      | term_for_atom seen T _ j k =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   378
        if T = nat_T then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   379
          HOLogic.mk_number nat_T j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   380
        else if T = int_T then
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   381
          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
   382
        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
   383
          HOLogic.mk_number nat_T (k - j - 1)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   384
        else if T = @{typ bisim_iterator} then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   385
          HOLogic.mk_number nat_T j
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   386
        else case datatype_spec datatypes T of
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   387
          NONE => nth_atom for_auto T j k
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   388
        | SOME {deep = false, ...} => nth_atom for_auto T j k
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33232
diff changeset
   389
        | SOME {co, constrs, ...} =>
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   390
          let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   391
            (* styp -> int list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   392
            fun tuples_for_const (s, T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   393
              tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   394
            (* unit -> indexname * typ *)
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   395
            fun var () = ((nth_atom_name "" T j k, 0), T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   396
            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
   397
                                 constrs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   398
            val real_j = j + offset_of_type ofs T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   399
            val constr_x as (constr_s, constr_T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   400
              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
   401
                            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
   402
                            else NONE)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   403
                        (discr_jsss ~~ constrs) |> the
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   404
            val arg_Ts = curried_binder_types constr_T
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   405
            val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   406
                             (index_seq 0 (length arg_Ts))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   407
            val sel_Rs =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   408
              map (fn x => get_first
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   409
                               (fn ConstName (s', T', R) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   410
                                   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
   411
                                 | u => raise NUT ("Nitpick_Model.reconstruct_\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   412
                                                   \term.term_for_atom", [u]))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   413
                               sel_names |> the) sel_xs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   414
            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
   415
            val sel_jsss = map tuples_for_const sel_xs
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   416
            val arg_jsss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   417
              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
   418
                                        else NONE)) sel_jsss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   419
            val uncur_arg_Ts = binder_types constr_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   420
          in
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   421
            if co andalso member (op =) seen (T, j) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   422
              Var (var ())
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   423
            else if constr_s = @{const_name Word} then
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   424
              HOLogic.mk_number
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   425
                  (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
   426
                  (value_of_bits (the_single arg_jsss))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   427
            else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   428
              let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   429
                val seen = seen |> co ? cons (T, j)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   430
                val ts =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   431
                  if length arg_Ts = 0 then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   432
                    []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   433
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   434
                    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
   435
                         arg_jsss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   436
                    |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   437
                    |> dest_n_tuple (length uncur_arg_Ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   438
                val t =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   439
                  if constr_s = @{const_name Abs_Frac} then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   440
                    let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   441
                      val num_T = body_type T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   442
                      (* int -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   443
                      val mk_num = HOLogic.mk_number num_T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   444
                    in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   445
                      case ts of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   446
                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   447
                        (case snd (HOLogic.dest_number t1) of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   448
                           0 => mk_num 0
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   449
                         | n1 => case HOLogic.dest_number t2 |> snd of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   450
                                   1 => mk_num n1
34974
18b41bba42b5 new theory Algebras.thy for generic algebraic structures
haftmann
parents: 34936
diff changeset
   451
                                 | n2 => Const (@{const_name Algebras.divide},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   452
                                                num_T --> num_T --> num_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   453
                                         $ 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
   454
                      | _ => 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
   455
                                         \term_for_atom (Abs_Frac)", ts)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   456
                    end
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   457
                  else if not for_auto andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   458
                          (is_abs_fun thy constr_x orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   459
                           constr_s = @{const_name Quot}) then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   460
                    Const (abs_name, constr_T) $ the_single ts
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
   461
                  else if not for_auto andalso
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
   462
                          constr_s = @{const_name NonStd} 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
   463
                    Const (fst (dest_Const (the_single ts)), T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   464
                  else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   465
                    list_comb (Const constr_x, ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   466
              in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   467
                if co then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   468
                  let val var = var () in
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   469
                    if exists_subterm (curry (op =) (Var var)) t then
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   470
                      Const (@{const_name The}, (T --> bool_T) --> T)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   471
                      $ Abs ("\<omega>", T,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   472
                             Const (@{const_name "op ="}, T --> T --> bool_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   473
                             $ Bound 0 $ abstract_over (Var var, t))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   474
                    else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   475
                      t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   476
                  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   477
                else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   478
                  t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   479
              end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   480
          end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   481
    (* (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
   482
       -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   483
    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
   484
      make_fun true T1 T2 T'
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   485
               (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
   486
               (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
   487
                    (batch_list (arity_of_rep R) js))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   488
    (* (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
   489
    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
   490
      | 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
   491
        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
   492
        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
   493
      | 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
   494
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   495
          val arity1 = arity_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   496
          val (js1, js2) = chop arity1 js
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   497
        in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   498
          list_comb (HOLogic.pair_const T1 T2,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   499
                     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
   500
                          [[js1], [js2]])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   501
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   502
      | term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   503
        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
   504
      | 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
   505
                     jss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   506
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   507
          val jss1 = all_combinations_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   508
          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
   509
          val ts2 =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   510
            map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   511
                                       [[int_for_bool (member (op =) jss js)]])
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   512
                jss1
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   513
        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
   514
      | 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
   515
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   516
          val arity1 = arity_of_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   517
          val jss1 = all_combinations_for_rep R1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   518
          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
   519
          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
   520
          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
   521
                         o AList.lookup (op =) grouped_jss2) jss1
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   522
        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
   523
      | term_for_rep seen T T' (Opt R) jss =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   524
        if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   525
      | term_for_rep seen T _ R jss =
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   526
        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
   527
                   Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   528
                   string_of_int (length jss))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   529
  in
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   530
    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   531
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   532
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34124
diff changeset
   533
(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   534
   -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   535
fun term_for_name scope sel_names rel_table bounds name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   536
  let val T = type_of name in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   537
    tuple_list_for_name rel_table bounds name
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   538
    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   539
                        (rep_of name)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   540
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   541
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
   542
(* Proof.context -> (string * string * string * string) * Proof.context *)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   543
fun add_wacky_syntax ctxt =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   544
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   545
    (* term -> string *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   546
    val name_of = fst o dest_Const
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   547
    val thy = ProofContext.theory_of ctxt |> Context.reject_draft
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   548
    val (maybe_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   549
      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   550
                          Mixfix (maybe_mixfix, [1000], 1000)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   551
    val (base_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   552
      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   553
                          Mixfix (base_mixfix, [1000], 1000)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   554
    val (step_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   555
      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   556
                          Mixfix (step_mixfix, [1000], 1000)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   557
    val (abs_t, thy) =
33202
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   558
      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
0183ab3ca7b4 make Nitpick compile again
blanchet
parents: 33192
diff changeset
   559
                          Mixfix (abs_mixfix, [40], 40)) thy
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   560
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   561
    ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   562
     ProofContext.transfer_syntax thy ctxt)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   563
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   564
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   565
(* term -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   566
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
   567
                                   $ Abs (s, T, Const (@{const_name "op ="}, _)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   568
                                                $ Bound 0 $ t')) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   569
    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
   570
  | unfold_outer_the_binders t = t
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   571
(* typ list -> int -> term * term -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   572
fun bisimilar_values _ 0 _ = true
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   573
  | bisimilar_values coTs max_depth (t1, t2) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   574
    let val T = fastype_of t1 in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   575
      if exists_subtype (member (op =) coTs) T then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   576
        let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   577
          val ((head1, args1), (head2, args2)) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   578
            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
   579
          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
   580
        in
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   581
          head1 = head2 andalso
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   582
          forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   583
        end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   584
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   585
        t1 = t2
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   586
    end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   587
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   588
(* 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
   589
  -> 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
   590
  -> Pretty.T * bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   591
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   592
        ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
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
   593
                       user_axioms, debug, binary_ints, destroy_constrs,
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
   594
                       specialize, skolemize, star_linear_preds, uncurry,
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
   595
                       fast_descrs, tac_timeout, evals, case_names, def_table,
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
   596
                       nondef_table, user_nondefs, simp_table, psimp_table,
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
   597
                       intro_table, ground_thm_table, ersatz_table, skolems,
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
   598
                       special_funs, unrolled_preds, wf_cache, constr_cache},
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   599
         card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   600
        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
   601
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   602
    val (wacky_names as (_, base_name, step_name, _), ctxt) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   603
      add_wacky_syntax ctxt
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   604
    val hol_ctxt =
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   605
      {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
   606
       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
   607
       binary_ints = binary_ints, destroy_constrs = destroy_constrs,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   608
       specialize = specialize, skolemize = skolemize,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   609
       star_linear_preds = star_linear_preds, uncurry = uncurry,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   610
       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
   611
       case_names = case_names, def_table = def_table,
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   612
       nondef_table = nondef_table, user_nondefs = user_nondefs,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   613
       simp_table = simp_table, psimp_table = psimp_table,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   614
       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
   615
       ersatz_table = ersatz_table, skolems = skolems,
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   616
       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
   617
       wf_cache = wf_cache, constr_cache = constr_cache}
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   618
    val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   619
                 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   620
                 ofs = ofs}
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   621
    (* typ -> typ -> rep -> int list list -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   622
    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   623
                                        bounds
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   624
    (* nat -> typ -> nat -> typ *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   625
    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   626
    (* nat -> typ -> typ list *)
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   627
    fun all_values_of_type card T =
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   628
      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
   629
    (* dtype_spec list -> dtype_spec -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   630
    fun is_codatatype_wellformed (cos : dtype_spec list)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   631
                                 ({typ, card, ...} : dtype_spec) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   632
      let
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   633
        val ts = all_values_of_type card typ
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   634
        val max_depth = Integer.sum (map #card cos)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   635
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   636
        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
   637
               (all_distinct_unordered_pairs_of ts)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   638
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   639
    (* string -> Pretty.T *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   640
    fun pretty_for_assign name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   641
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   642
        val (oper, (t1, T'), T) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   643
          case name of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   644
            FreeName (s, T, _) =>
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   645
            let val t = Free (s, unbit_and_unbox_type T) in
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   646
              ("=", (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
   647
            end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   648
          | ConstName (s, T, _) =>
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   649
            (assign_operator_for_const (s, T),
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   650
             user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   651
             T)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   652
          | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   653
                            \pretty_for_assign", [name])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   654
        val t2 = if rep_of name = Any then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   655
                   Const (@{const_name undefined}, T')
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   656
                 else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   657
                   tuple_list_for_name rel_table bounds name
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   658
                   |> term_for_rep T T' (rep_of name)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   659
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   660
        Pretty.block (Pretty.breaks
33571
3655e51f9958 minor cleanup in Nitpick
blanchet
parents: 33565
diff changeset
   661
            [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
   662
             Pretty.str oper, Syntax.pretty_term ctxt t2])
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   663
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   664
    (* 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
   665
    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
   666
      Pretty.block (Pretty.breaks
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   667
          [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   668
           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
   669
               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
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
   670
                (if complete then [] else [Pretty.str unrep]))])
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   671
    (* typ -> dtype_spec list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   672
    fun integer_datatype T =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   673
      [{typ = T, card = card_of_type card_assigns T, co = false,
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
   674
        complete = false, concrete = true, deep = true, constrs = []}]
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   675
      handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   676
    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
   677
      datatypes |> filter #deep |> List.partition #co
33558
a2db56854b83 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents: 33232
diff changeset
   678
                ||> append (integer_datatype nat_T @ integer_datatype int_T)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   679
    val block_of_datatypes =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   680
      if show_datatypes andalso not (null datatypes) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   681
        [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   682
                         (map pretty_for_datatype datatypes)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   683
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   684
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   685
    val block_of_codatatypes =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   686
      if show_datatypes andalso not (null codatatypes) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   687
        [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   688
                         (map pretty_for_datatype codatatypes)]
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   689
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   690
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   691
    (* bool -> string -> nut list -> Pretty.T list *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   692
    fun block_of_names show title names =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   693
      if show andalso not (null names) then
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   694
        Pretty.str (title ^ plural_s_for_list names ^ ":")
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   695
        :: map (Pretty.indent indent_size o pretty_for_assign)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   696
               (sort_wrt (original_name o nickname_of) names)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   697
      else
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   698
        []
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   699
    val (skolem_names, nonskolem_nonsel_names) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   700
      List.partition is_skolem_name nonsel_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   701
    val (eval_names, noneval_nonskolem_nonsel_names) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   702
      List.partition (String.isPrefix eval_prefix o nickname_of)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   703
                     nonskolem_nonsel_names
34121
5e831d805118 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents: 33982
diff changeset
   704
      ||> 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
   705
                      o nickname_of)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   706
    val free_names =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   707
      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
   708
              case filter (curry (op =) x
34124
c4628a1dcf75 added support for binary nat/int representation to Nitpick
blanchet
parents: 34123
diff changeset
   709
                           o pairf nickname_of (unbit_and_unbox_type o type_of))
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   710
                          free_names of
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   711
                [name] => name
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   712
              | [] => FreeName (s, T, Any)
33232
f93390060bbe internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents: 33202
diff changeset
   713
              | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   714
                                 [Const x])) all_frees
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   715
    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
   716
                 block_of_names show_skolems "Skolem constant" skolem_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   717
                 block_of_names true "Evaluated term" eval_names @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   718
                 block_of_datatypes @ block_of_codatatypes @
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   719
                 block_of_names show_consts "Constant"
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   720
                                noneval_nonskolem_nonsel_names
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   721
  in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   722
    (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
   723
                    else chunks),
34936
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   724
     bisim_depth >= 0 orelse
c4f04bee79f3 some work on Nitpick's support for quotient types;
blanchet
parents: 34126
diff changeset
   725
     forall (is_codatatype_wellformed codatatypes) codatatypes)
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   726
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   727
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   728
(* 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
   729
   -> KK.raw_bound list -> term -> bool option *)
35070
96136eb6218f split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents: 34998
diff changeset
   730
fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   731
                               card_assigns, ...})
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   732
                    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
   733
  let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   734
    (* typ * int -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   735
    fun free_type_assm (T, k) =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   736
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   737
        (* int -> term *)
35075
888802be2019 handle Nitpick's nonstandard model enumeration in a cleaner way;
blanchet
parents: 35070
diff changeset
   738
        fun atom j = nth_atom true T j k
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   739
        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
   740
        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
   741
        val compreh_assm =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   742
          Const (@{const_name All}, (T --> bool_T) --> bool_T)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   743
              $ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   744
        val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   745
      in s_conj (compreh_assm, distinct_assm) end
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   746
    (* nut -> term *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   747
    fun free_name_assm name =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   748
      HOLogic.mk_eq (Free (nickname_of name, type_of name),
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   749
                     term_for_name scope sel_names rel_table bounds name)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   750
    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
   751
    val model_assms = map free_name_assm free_names
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   752
    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
   753
    (* bool -> bool *)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   754
    fun try_out negate =
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   755
      let
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   756
        val concl = (negate ? curry (op $) @{const Not})
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   757
                    (ObjectLogic.atomize_term thy prop)
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   758
        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
   759
                   |> map_types (map_type_tfree
34998
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   760
                                     (fn (s, []) => TFree (s, HOLogic.typeS)
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   761
                                       | x => TFree x))
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   762
       val _ = if debug then
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   763
                 priority ((if negate then "Genuineness" else "Spuriousness") ^
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   764
                           " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   765
               else
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   766
                 ()
5e492a862b34 four changes to Nitpick:
blanchet
parents: 34982
diff changeset
   767
        val goal = prop |> cterm_of thy |> Goal.init
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   768
      in
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   769
        (goal |> SINGLE (DETERM_TIMEOUT auto_timeout
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   770
                                        (auto_tac (clasimpset_of ctxt)))
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   771
              |> the |> Goal.finish ctxt; true)
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   772
        handle THM _ => false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   773
             | TimeLimit.TimeOut => false
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   774
      end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   775
  in
33705
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   776
    if try_out false then SOME true
947184dc75c9 removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents: 33580
diff changeset
   777
    else if try_out true then SOME false
33192
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   778
    else NONE
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   779
  end
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   780
08a39a957ed7 added Nitpick's theory and ML files to Isabelle/HOL;
blanchet
parents:
diff changeset
   781
end;