handle Nitpick's nonstandard model enumeration in a cleaner way;
authorblanchet
Fri Feb 05 12:04:54 2010 +0100 (2010-02-05)
changeset 35075888802be2019
parent 35074 a88642066448
child 35076 cc19e2aef17e
handle Nitpick's nonstandard model enumeration in a cleaner way;
and renumber the atoms so that we get more often a_1 and a_2
and less often a_{n-1} and a_{n-2} in counterexamples
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 05 11:24:53 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 05 12:04:54 2010 +0100
     1.3 @@ -339,7 +339,7 @@
     1.4      fun is_type_always_monotonic T =
     1.5        (is_datatype thy T andalso not (is_quot_type thy T) andalso
     1.6         (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
     1.7 -      is_number_type thy T orelse is_bit_type T orelse T = @{typ \<xi>}
     1.8 +      is_number_type thy T orelse is_bit_type T
     1.9      fun is_type_monotonic T =
    1.10        unique_scope orelse
    1.11        case triple_lookup (type_match thy) monos T of
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 05 11:24:53 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 05 12:04:54 2010 +0100
     2.3 @@ -940,6 +940,10 @@
     2.4        | _ => list_comb (Const x, args)
     2.5      end
     2.6  
     2.7 +(* The higher this number is, the more nonstandard models can be generated. It's
     2.8 +   not important enough to be a user option, though. *)
     2.9 +val xi_card = 8
    2.10 +
    2.11  (* (typ * int) list -> typ -> int *)
    2.12  fun card_of_type assigns (Type ("fun", [T1, T2])) =
    2.13      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
    2.14 @@ -949,6 +953,7 @@
    2.15    | card_of_type _ @{typ prop} = 2
    2.16    | card_of_type _ @{typ bool} = 2
    2.17    | card_of_type _ @{typ unit} = 1
    2.18 +  | card_of_type _ @{typ \<xi>} = xi_card
    2.19    | card_of_type assigns T =
    2.20      case AList.lookup (op =) assigns T of
    2.21        SOME k => k
    2.22 @@ -1005,6 +1010,7 @@
    2.23         | @{typ prop} => 2
    2.24         | @{typ bool} => 2
    2.25         | @{typ unit} => 1
    2.26 +       | @{typ \<xi>} => xi_card
    2.27         | Type _ =>
    2.28           (case datatype_constrs hol_ctxt T of
    2.29              [] => if is_integer_type T orelse is_bit_type T then 0
    2.30 @@ -2009,7 +2015,8 @@
    2.31    | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
    2.32    | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
    2.33    | Type (_, Ts) =>
    2.34 -    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
    2.35 +    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
    2.36 +                      @{typ \<xi>} :: accum) T then
    2.37        accum
    2.38      else
    2.39        T :: accum
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 11:24:53 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 12:04:54 2010 +0100
     3.3 @@ -56,26 +56,26 @@
     3.4  val opt_flag = nitpick_prefix ^ "opt"
     3.5  val non_opt_flag = nitpick_prefix ^ "non_opt"
     3.6  
     3.7 -(* string -> int -> string *)
     3.8 -fun atom_suffix s j =
     3.9 -  nat_subscript (j + 1)
    3.10 +(* string -> int -> int -> string *)
    3.11 +fun nth_atom_suffix s j k =
    3.12 +  nat_subscript (k - j)
    3.13    |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    3.14       ? prefix "\<^isub>,"
    3.15 -(* string -> typ -> int -> string *)
    3.16 -fun atom_name prefix (T as Type (s, _)) j =
    3.17 +(* string -> typ -> int -> int -> string *)
    3.18 +fun nth_atom_name prefix (T as Type (s, _)) j k =
    3.19      let val s' = shortest_name s in
    3.20        prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    3.21 -      atom_suffix s j
    3.22 +      nth_atom_suffix s j k
    3.23      end
    3.24 -  | atom_name prefix (T as TFree (s, _)) j =
    3.25 -    prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    3.26 -  | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    3.27 -(* bool -> typ -> int -> term *)
    3.28 -fun atom for_auto T j =
    3.29 +  | nth_atom_name prefix (T as TFree (s, _)) j k =
    3.30 +    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k
    3.31 +  | nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
    3.32 +(* bool -> typ -> int -> int -> term *)
    3.33 +fun nth_atom for_auto T j k =
    3.34    if for_auto then
    3.35 -    Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T)
    3.36 +    Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T)
    3.37    else
    3.38 -    Const (atom_name "" T j, T)
    3.39 +    Const (nth_atom_name "" T j k, T)
    3.40  
    3.41  (* term -> real *)
    3.42  fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
    3.43 @@ -348,7 +348,7 @@
    3.44                                   (unbit_and_unbox_type T1)
    3.45                                   (unbit_and_unbox_type T2)
    3.46      (* (typ * int) list -> typ -> typ -> int -> term *)
    3.47 -    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
    3.48 +    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
    3.49          let
    3.50            val k1 = card_of_type card_assigns T1
    3.51            val k2 = card_of_type card_assigns T2
    3.52 @@ -360,37 +360,39 @@
    3.53                              signed_string_of_int j ^ " for " ^
    3.54                              string_for_rep (Vect (k1, Atom (k2, 0))))
    3.55          end
    3.56 -      | term_for_atom seen (Type ("*", [T1, T2])) _ j =
    3.57 -        let val k1 = card_of_type card_assigns T1 in
    3.58 +      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
    3.59 +        let
    3.60 +          val k1 = card_of_type card_assigns T1
    3.61 +          val k2 = k div k1
    3.62 +        in
    3.63            list_comb (HOLogic.pair_const T1 T2,
    3.64 -                     map2 (fn T => term_for_atom seen T T) [T1, T2]
    3.65 -                          [j div k1, j mod k1])
    3.66 +                     map3 (fn T => term_for_atom seen T T) [T1, T2]
    3.67 +                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
    3.68          end
    3.69 -      | term_for_atom seen @{typ prop} _ j =
    3.70 -        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j)
    3.71 -      | term_for_atom _ @{typ bool} _ j =
    3.72 +      | term_for_atom seen @{typ prop} _ j k =
    3.73 +        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
    3.74 +      | term_for_atom _ @{typ bool} _ j _ =
    3.75          if j = 0 then @{const False} else @{const True}
    3.76 -      | term_for_atom _ @{typ unit} _ _ = @{const Unity}
    3.77 -      | term_for_atom seen T _ j =
    3.78 +      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
    3.79 +      | term_for_atom seen T _ j k =
    3.80          if T = nat_T then
    3.81            HOLogic.mk_number nat_T j
    3.82          else if T = int_T then
    3.83 -          HOLogic.mk_number int_T
    3.84 -              (int_for_atom (card_of_type card_assigns int_T, 0) j)
    3.85 +          HOLogic.mk_number int_T (int_for_atom (k, 0) j)
    3.86          else if is_fp_iterator_type T then
    3.87 -          HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
    3.88 +          HOLogic.mk_number nat_T (k - j - 1)
    3.89          else if T = @{typ bisim_iterator} then
    3.90            HOLogic.mk_number nat_T j
    3.91          else case datatype_spec datatypes T of
    3.92 -          NONE => atom for_auto T j
    3.93 -        | SOME {deep = false, ...} => atom for_auto T j
    3.94 +          NONE => nth_atom for_auto T j k
    3.95 +        | SOME {deep = false, ...} => nth_atom for_auto T j k
    3.96          | SOME {co, constrs, ...} =>
    3.97            let
    3.98              (* styp -> int list *)
    3.99              fun tuples_for_const (s, T) =
   3.100                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
   3.101              (* unit -> indexname * typ *)
   3.102 -            fun var () = ((atom_name "" T j, 0), T)
   3.103 +            fun var () = ((nth_atom_name "" T j k, 0), T)
   3.104              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
   3.105                                   constrs
   3.106              val real_j = j + offset_of_type ofs T
   3.107 @@ -479,13 +481,14 @@
   3.108      (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
   3.109         -> term *)
   3.110      and term_for_vect seen k R T1 T2 T' js =
   3.111 -      make_fun true T1 T2 T' (map (term_for_atom seen T1 T1) (index_seq 0 k))
   3.112 +      make_fun true T1 T2 T'
   3.113 +               (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
   3.114                 (map (term_for_rep seen T2 T2 R o single)
   3.115                      (batch_list (arity_of_rep R) js))
   3.116      (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
   3.117 -    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
   3.118 +    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
   3.119        | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
   3.120 -        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
   3.121 +        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   3.122          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   3.123        | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
   3.124          let
   3.125 @@ -732,7 +735,7 @@
   3.126      fun free_type_assm (T, k) =
   3.127        let
   3.128          (* int -> term *)
   3.129 -        val atom = atom true T
   3.130 +        fun atom j = nth_atom true T j k
   3.131          fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
   3.132          val eqs = map equation_for_atom (index_seq 0 k)
   3.133          val compreh_assm =
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 05 11:24:53 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 05 12:04:54 2010 +0100
     4.3 @@ -134,7 +134,7 @@
     4.4  fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
     4.5                                  bits, bisim_depth, datatypes, ...} : scope) =
     4.6    let
     4.7 -    val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
     4.8 +    val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
     4.9                       @{typ bisim_iterator}]
    4.10      val (iter_assigns, card_assigns) =
    4.11        card_assigns |> filter_out (member (op =) boring_Ts o fst)