src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 61331 2007ea8615a2
parent 61324 d4ec7594f558
child 61333 24b5e7579fdd
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 05 23:03:50 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Oct 06 09:27:31 2015 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  
     1.5    val irrelevant : string
     1.6    val unknown : string
     1.7 -  val unrep : unit -> string
     1.8    val register_term_postprocessor :
     1.9      typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
    1.10    val register_term_postprocessor_global :
    1.11 @@ -73,7 +72,7 @@
    1.12  
    1.13  val irrelevant = "_"
    1.14  val unknown = "?"
    1.15 -val unrep = xsym "\<dots>" "..."
    1.16 +val unrep_mixfix = xsym "\<dots>" "..."
    1.17  val maybe_mixfix = xsym "_\<^sup>?" "_?"
    1.18  val base_mixfix = xsym "_\<^bsub>base\<^esub>" "_.base"
    1.19  val step_mixfix = xsym "_\<^bsub>step\<^esub>" "_.step"
    1.20 @@ -91,20 +90,28 @@
    1.21    let
    1.22      val name_of = fst o dest_Const
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24 -    val (maybe_t, thy) =
    1.25 -      Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.26 -                          Mixfix (maybe_mixfix (), [1000], 1000)) thy
    1.27 -    val (abs_t, thy) =
    1.28 -      Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    1.29 -                          Mixfix (abs_mixfix (), [40], 40)) thy
    1.30 -    val (base_t, thy) =
    1.31 -      Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    1.32 -                          Mixfix (base_mixfix (), [1000], 1000)) thy
    1.33 -    val (step_t, thy) =
    1.34 -      Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    1.35 -                          Mixfix (step_mixfix (), [1000], 1000)) thy
    1.36 +    val (unrep_s, thy) = thy
    1.37 +      |> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}),
    1.38 +        Mixfix (unrep_mixfix (), [], 1000))
    1.39 +      |>> name_of
    1.40 +    val (maybe_s, thy) = thy
    1.41 +      |> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.42 +        Mixfix (maybe_mixfix (), [1000], 1000))
    1.43 +      |>> name_of
    1.44 +    val (abs_s, thy) = thy
    1.45 +      |> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    1.46 +        Mixfix (abs_mixfix (), [40], 40))
    1.47 +      |>> name_of
    1.48 +    val (base_s, thy) = thy
    1.49 +      |> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    1.50 +        Mixfix (base_mixfix (), [1000], 1000))
    1.51 +      |>> name_of
    1.52 +    val (step_s, thy) = thy
    1.53 +      |> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    1.54 +        Mixfix (step_mixfix (), [1000], 1000))
    1.55 +      |>> name_of
    1.56    in
    1.57 -    (apply2 (apply2 name_of) ((maybe_t, abs_t), (base_t, step_t)),
    1.58 +    (((unrep_s, maybe_s, abs_s), (base_s, step_s)),
    1.59       Proof_Context.transfer thy ctxt)
    1.60    end
    1.61  
    1.62 @@ -362,7 +369,7 @@
    1.63        end
    1.64    in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
    1.65  and reconstruct_term maybe_opt unfold pool
    1.66 -        (wacky_names as ((maybe_name, abs_name), _))
    1.67 +        (wacky_names as ((unrep_name, maybe_name, abs_name), _))
    1.68          (scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
    1.69                     data_types, ofs, ...})
    1.70          atomss sel_names rel_table bounds =
    1.71 @@ -401,7 +408,7 @@
    1.72          val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
    1.73          fun aux [] =
    1.74              if maybe_opt andalso not (is_complete_type data_types false T) then
    1.75 -              insert_const $ Const (unrep (), T) $ empty_const
    1.76 +              insert_const $ Const (unrep_name, T) $ empty_const
    1.77              else
    1.78                empty_const
    1.79            | aux ((t1, t2) :: zs) =
    1.80 @@ -430,7 +437,7 @@
    1.81               | _ => update_const $ aux' tps $ t1 $ t2)
    1.82          fun aux tps =
    1.83            if maybe_opt andalso not (is_complete_type data_types false T1) then
    1.84 -            update_const $ aux' tps $ Const (unrep (), T1)
    1.85 +            update_const $ aux' tps $ Const (unrep_name, T1)
    1.86              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    1.87            else
    1.88              aux' tps
    1.89 @@ -979,7 +986,7 @@
    1.90              Pretty.enum "," "{" "}"
    1.91                  (map (pretty_term_auto_global ctxt) (all_values card typ) @
    1.92                   (if fun_from_pair complete false then []
    1.93 -                  else [Pretty.str (unrep ())]))]))
    1.94 +                  else [Pretty.str (unrep_mixfix ())]))]))
    1.95      fun integer_data_type T =
    1.96        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.97          self_rec = true, complete = (false, false), concrete = (true, true),