src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35280 54ab4921f826
parent 35220 2bcdae5f4fdb
child 35385 29f81babefd7
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 22 10:28:49 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 22 11:57:33 2010 +0100
     1.3 @@ -74,12 +74,12 @@
     1.4    |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
     1.5       ? prefix "\<^isub>,"
     1.6  (* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
     1.7 -fun nth_atom_name pool prefix (T as Type (s, _)) j k =
     1.8 +fun nth_atom_name pool prefix (Type (s, _)) j k =
     1.9      let val s' = shortest_name s in
    1.10        prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
    1.11        nth_atom_suffix pool s j k
    1.12      end
    1.13 -  | nth_atom_name pool prefix (T as TFree (s, _)) j k =
    1.14 +  | nth_atom_name pool prefix (TFree (s, _)) j k =
    1.15      prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
    1.16    | nth_atom_name _ _ T _ _ =
    1.17      raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
    1.18 @@ -113,20 +113,23 @@
    1.19  fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
    1.20      unarize_and_unbox_term t1
    1.21    | unarize_and_unbox_term (Const (@{const_name PairBox},
    1.22 -                                   Type ("fun", [T1, Type ("fun", [T2, T3])]))
    1.23 +                                   Type ("fun", [T1, Type ("fun", [T2, _])]))
    1.24                              $ t1 $ t2) =
    1.25 -    let val Ts = map unarize_and_unbox_type [T1, T2] in
    1.26 +    let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
    1.27        Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
    1.28        $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    1.29      end
    1.30 -  | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
    1.31 +  | unarize_and_unbox_term (Const (s, T)) =
    1.32 +    Const (s, unarize_unbox_and_uniterize_type T)
    1.33    | unarize_and_unbox_term (t1 $ t2) =
    1.34      unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
    1.35 -  | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
    1.36 -  | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
    1.37 +  | unarize_and_unbox_term (Free (s, T)) =
    1.38 +    Free (s, unarize_unbox_and_uniterize_type T)
    1.39 +  | unarize_and_unbox_term (Var (x, T)) =
    1.40 +    Var (x, unarize_unbox_and_uniterize_type T)
    1.41    | unarize_and_unbox_term (Bound j) = Bound j
    1.42    | unarize_and_unbox_term (Abs (s, T, t')) =
    1.43 -    Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
    1.44 +    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
    1.45  
    1.46  (* typ -> typ -> (typ * typ) * (typ * typ) *)
    1.47  fun factor_out_types (T1 as Type ("*", [T11, T12]))
    1.48 @@ -260,12 +263,12 @@
    1.49    | mk_tuple _ (t :: _) = t
    1.50    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.51  
    1.52 -(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
    1.53 -   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    1.54 -   -> typ -> rep -> int list list -> term *)
    1.55 -fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
    1.56 -        ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
    1.57 -          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
    1.58 +(* bool -> atom_pool -> (string * string) * (string * string) -> scope
    1.59 +   -> nut list -> nut list -> nut list -> nut NameTable.table
    1.60 +   -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
    1.61 +fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
    1.62 +        ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
    1.63 +          ofs, ...} : scope) sel_names rel_table bounds =
    1.64    let
    1.65      val for_auto = (maybe_name = "")
    1.66      (* int list list -> int *)
    1.67 @@ -357,11 +360,11 @@
    1.68        ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
    1.69                   |> make_plain_fun maybe_opt T1 T2
    1.70                   |> unarize_and_unbox_term
    1.71 -                 |> typecast_fun (unarize_and_unbox_type T')
    1.72 -                                 (unarize_and_unbox_type T1)
    1.73 -                                 (unarize_and_unbox_type T2)
    1.74 +                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
    1.75 +                                 (unarize_unbox_and_uniterize_type T1)
    1.76 +                                 (unarize_unbox_and_uniterize_type T2)
    1.77      (* (typ * int) list -> typ -> typ -> int -> term *)
    1.78 -    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
    1.79 +    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
    1.80          let
    1.81            val k1 = card_of_type card_assigns T1
    1.82            val k2 = card_of_type card_assigns T2
    1.83 @@ -525,7 +528,7 @@
    1.84                       map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
    1.85                            [[js1], [js2]])
    1.86          end
    1.87 -      | term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] =
    1.88 +      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
    1.89          term_for_vect seen k R' T1 T2 T' js
    1.90        | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
    1.91                       jss =
    1.92 @@ -548,7 +551,7 @@
    1.93          in make_fun true T1 T2 T' ts1 ts2 end
    1.94        | term_for_rep seen T T' (Opt R) jss =
    1.95          if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
    1.96 -      | term_for_rep seen T _ R jss =
    1.97 +      | term_for_rep _ T _ R jss =
    1.98          raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
    1.99                     Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
   1.100                     string_of_int (length jss))
   1.101 @@ -559,11 +562,11 @@
   1.102  fun term_for_name pool scope sel_names rel_table bounds name =
   1.103    let val T = type_of name in
   1.104      tuple_list_for_name rel_table bounds name
   1.105 -    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
   1.106 -                        bounds T T (rep_of name)
   1.107 +    |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
   1.108 +                        rel_table bounds T T (rep_of name)
   1.109    end
   1.110  
   1.111 -(* Proof.context -> (string * string * string * string) * Proof.context *)
   1.112 +(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
   1.113  fun add_wacky_syntax ctxt =
   1.114    let
   1.115      (* term -> string *)
   1.116 @@ -572,17 +575,17 @@
   1.117      val (maybe_t, thy) =
   1.118        Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
   1.119                            Mixfix (maybe_mixfix, [1000], 1000)) thy
   1.120 +    val (abs_t, thy) =
   1.121 +      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
   1.122 +                          Mixfix (abs_mixfix, [40], 40)) thy
   1.123      val (base_t, thy) =
   1.124        Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
   1.125                            Mixfix (base_mixfix, [1000], 1000)) thy
   1.126      val (step_t, thy) =
   1.127        Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
   1.128                            Mixfix (step_mixfix, [1000], 1000)) thy
   1.129 -    val (abs_t, thy) =
   1.130 -      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
   1.131 -                          Mixfix (abs_mixfix, [40], 40)) thy
   1.132    in
   1.133 -    ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
   1.134 +    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
   1.135       ProofContext.transfer_syntax thy ctxt)
   1.136    end
   1.137  
   1.138 @@ -613,18 +616,18 @@
   1.139    -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
   1.140    -> Pretty.T * bool *)
   1.141  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
   1.142 -        ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
   1.143 -                       user_axioms, debug, binary_ints, destroy_constrs,
   1.144 -                       specialize, skolemize, star_linear_preds, uncurry,
   1.145 -                       fast_descrs, tac_timeout, evals, case_names, def_table,
   1.146 -                       nondef_table, user_nondefs, simp_table, psimp_table,
   1.147 -                       intro_table, ground_thm_table, ersatz_table, skolems,
   1.148 -                       special_funs, unrolled_preds, wf_cache, constr_cache},
   1.149 +        ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
   1.150 +                      debug, binary_ints, destroy_constrs, specialize,
   1.151 +                      skolemize, star_linear_preds, uncurry, fast_descrs,
   1.152 +                      tac_timeout, evals, case_names, def_table, nondef_table,
   1.153 +                      user_nondefs, simp_table, psimp_table, intro_table,
   1.154 +                      ground_thm_table, ersatz_table, skolems, special_funs,
   1.155 +                      unrolled_preds, wf_cache, constr_cache},
   1.156           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
   1.157          formats all_frees free_names sel_names nonsel_names rel_table bounds =
   1.158    let
   1.159      val pool = Unsynchronized.ref []
   1.160 -    val (wacky_names as (_, base_name, step_name, _), ctxt) =
   1.161 +    val (wacky_names as (_, base_step_names), ctxt) =
   1.162        add_wacky_syntax ctxt
   1.163      val hol_ctxt =
   1.164        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
   1.165 @@ -679,13 +682,12 @@
   1.166          val (oper, (t1, T'), T) =
   1.167            case name of
   1.168              FreeName (s, T, _) =>
   1.169 -            let val t = Free (s, unarize_and_unbox_type T) in
   1.170 +            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
   1.171                ("=", (t, format_term_type thy def_table formats t), T)
   1.172              end
   1.173            | ConstName (s, T, _) =>
   1.174              (assign_operator_for_const (s, T),
   1.175 -             user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
   1.176 -             T)
   1.177 +             user_friendly_const hol_ctxt base_step_names formats (s, T), T)
   1.178            | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
   1.179                              \pretty_for_assign", [name])
   1.180          val t2 = if rep_of name = Any then
   1.181 @@ -701,7 +703,8 @@
   1.182      (* dtype_spec -> Pretty.T *)
   1.183      fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
   1.184        Pretty.block (Pretty.breaks
   1.185 -          [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
   1.186 +          [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
   1.187 +           Pretty.str "=",
   1.188             Pretty.enum "," "{" "}"
   1.189                 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
   1.190                  (if complete then [] else [Pretty.str unrep]))])
   1.191 @@ -746,7 +749,8 @@
   1.192      val free_names =
   1.193        map (fn x as (s, T) =>
   1.194                case filter (curry (op =) x
   1.195 -                       o pairf nickname_of (unarize_and_unbox_type o type_of))
   1.196 +                       o pairf nickname_of
   1.197 +                               (unarize_unbox_and_uniterize_type o type_of))
   1.198                         free_names of
   1.199                  [name] => name
   1.200                | [] => FreeName (s, T, Any)
   1.201 @@ -767,7 +771,7 @@
   1.202  
   1.203  (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
   1.204     -> KK.raw_bound list -> term -> bool option *)
   1.205 -fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
   1.206 +fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
   1.207                                 card_assigns, ...})
   1.208                      auto_timeout free_names sel_names rel_table bounds prop =
   1.209    let