src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35075 888802be2019
parent 35070 96136eb6218f
child 35076 cc19e2aef17e
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 11:24:53 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 05 12:04:54 2010 +0100
     1.3 @@ -56,26 +56,26 @@
     1.4  val opt_flag = nitpick_prefix ^ "opt"
     1.5  val non_opt_flag = nitpick_prefix ^ "non_opt"
     1.6  
     1.7 -(* string -> int -> string *)
     1.8 -fun atom_suffix s j =
     1.9 -  nat_subscript (j + 1)
    1.10 +(* string -> int -> int -> string *)
    1.11 +fun nth_atom_suffix s j k =
    1.12 +  nat_subscript (k - j)
    1.13    |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
    1.14       ? prefix "\<^isub>,"
    1.15 -(* string -> typ -> int -> string *)
    1.16 -fun atom_name prefix (T as Type (s, _)) j =
    1.17 +(* string -> typ -> int -> int -> string *)
    1.18 +fun nth_atom_name prefix (T as Type (s, _)) j k =
    1.19      let val s' = shortest_name s in
    1.20        prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    1.21 -      atom_suffix s j
    1.22 +      nth_atom_suffix s j k
    1.23      end
    1.24 -  | atom_name prefix (T as TFree (s, _)) j =
    1.25 -    prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
    1.26 -  | atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
    1.27 -(* bool -> typ -> int -> term *)
    1.28 -fun atom for_auto T j =
    1.29 +  | nth_atom_name prefix (T as TFree (s, _)) j k =
    1.30 +    prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix s j k
    1.31 +  | nth_atom_name _ T _ _ = raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
    1.32 +(* bool -> typ -> int -> int -> term *)
    1.33 +fun nth_atom for_auto T j k =
    1.34    if for_auto then
    1.35 -    Free (atom_name (hd (space_explode "." nitpick_prefix)) T j, T)
    1.36 +    Free (nth_atom_name (hd (space_explode "." nitpick_prefix)) T j k, T)
    1.37    else
    1.38 -    Const (atom_name "" T j, T)
    1.39 +    Const (nth_atom_name "" T j k, T)
    1.40  
    1.41  (* term -> real *)
    1.42  fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
    1.43 @@ -348,7 +348,7 @@
    1.44                                   (unbit_and_unbox_type T1)
    1.45                                   (unbit_and_unbox_type T2)
    1.46      (* (typ * int) list -> typ -> typ -> int -> term *)
    1.47 -    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
    1.48 +    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
    1.49          let
    1.50            val k1 = card_of_type card_assigns T1
    1.51            val k2 = card_of_type card_assigns T2
    1.52 @@ -360,37 +360,39 @@
    1.53                              signed_string_of_int j ^ " for " ^
    1.54                              string_for_rep (Vect (k1, Atom (k2, 0))))
    1.55          end
    1.56 -      | term_for_atom seen (Type ("*", [T1, T2])) _ j =
    1.57 -        let val k1 = card_of_type card_assigns T1 in
    1.58 +      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
    1.59 +        let
    1.60 +          val k1 = card_of_type card_assigns T1
    1.61 +          val k2 = k div k1
    1.62 +        in
    1.63            list_comb (HOLogic.pair_const T1 T2,
    1.64 -                     map2 (fn T => term_for_atom seen T T) [T1, T2]
    1.65 -                          [j div k1, j mod k1])
    1.66 +                     map3 (fn T => term_for_atom seen T T) [T1, T2]
    1.67 +                          [j div k2, j mod k2] [k1, k2]) (* ### k2 or k1? FIXME *)
    1.68          end
    1.69 -      | term_for_atom seen @{typ prop} _ j =
    1.70 -        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j)
    1.71 -      | term_for_atom _ @{typ bool} _ j =
    1.72 +      | term_for_atom seen @{typ prop} _ j k =
    1.73 +        HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
    1.74 +      | term_for_atom _ @{typ bool} _ j _ =
    1.75          if j = 0 then @{const False} else @{const True}
    1.76 -      | term_for_atom _ @{typ unit} _ _ = @{const Unity}
    1.77 -      | term_for_atom seen T _ j =
    1.78 +      | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
    1.79 +      | term_for_atom seen T _ j k =
    1.80          if T = nat_T then
    1.81            HOLogic.mk_number nat_T j
    1.82          else if T = int_T then
    1.83 -          HOLogic.mk_number int_T
    1.84 -              (int_for_atom (card_of_type card_assigns int_T, 0) j)
    1.85 +          HOLogic.mk_number int_T (int_for_atom (k, 0) j)
    1.86          else if is_fp_iterator_type T then
    1.87 -          HOLogic.mk_number nat_T (card_of_type card_assigns T - j - 1)
    1.88 +          HOLogic.mk_number nat_T (k - j - 1)
    1.89          else if T = @{typ bisim_iterator} then
    1.90            HOLogic.mk_number nat_T j
    1.91          else case datatype_spec datatypes T of
    1.92 -          NONE => atom for_auto T j
    1.93 -        | SOME {deep = false, ...} => atom for_auto T j
    1.94 +          NONE => nth_atom for_auto T j k
    1.95 +        | SOME {deep = false, ...} => nth_atom for_auto T j k
    1.96          | SOME {co, constrs, ...} =>
    1.97            let
    1.98              (* styp -> int list *)
    1.99              fun tuples_for_const (s, T) =
   1.100                tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
   1.101              (* unit -> indexname * typ *)
   1.102 -            fun var () = ((atom_name "" T j, 0), T)
   1.103 +            fun var () = ((nth_atom_name "" T j k, 0), T)
   1.104              val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
   1.105                                   constrs
   1.106              val real_j = j + offset_of_type ofs T
   1.107 @@ -479,13 +481,14 @@
   1.108      (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
   1.109         -> term *)
   1.110      and term_for_vect seen k R T1 T2 T' js =
   1.111 -      make_fun true T1 T2 T' (map (term_for_atom seen T1 T1) (index_seq 0 k))
   1.112 +      make_fun true T1 T2 T'
   1.113 +               (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
   1.114                 (map (term_for_rep seen T2 T2 R o single)
   1.115                      (batch_list (arity_of_rep R) js))
   1.116      (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
   1.117 -    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0
   1.118 +    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
   1.119        | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
   1.120 -        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0)
   1.121 +        if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
   1.122          else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
   1.123        | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
   1.124          let
   1.125 @@ -732,7 +735,7 @@
   1.126      fun free_type_assm (T, k) =
   1.127        let
   1.128          (* int -> term *)
   1.129 -        val atom = atom true T
   1.130 +        fun atom j = nth_atom true T j k
   1.131          fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
   1.132          val eqs = map equation_for_atom (index_seq 0 k)
   1.133          val compreh_assm =