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