rationalized output (a bit)
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03)
changeset 46086096697aec8a7
parent 46085 447cda88adfe
child 46087 680edc162249
rationalized output (a bit)
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -235,20 +235,19 @@
     1.4           show_skolems, show_consts, evals, formats, atomss, max_potential,
     1.5           max_genuine, check_potential, check_genuine, batch_size, ...} = params
     1.6      val state_ref = Unsynchronized.ref state
     1.7 -    val pprint =
     1.8 +    fun pprint print =
     1.9        if mode = Auto_Try then
    1.10          Unsynchronized.change state_ref o Proof.goal_message o K
    1.11          o Pretty.chunks o cons (Pretty.str "") o single
    1.12          o Pretty.mark Isabelle_Markup.hilite
    1.13        else
    1.14 -        (fn s => (Output.urgent_message s; if debug then tracing s else ()))
    1.15 -        o Pretty.string_of
    1.16 -    fun pprint_n f = () |> mode = Normal ? pprint o f
    1.17 -    fun pprint_v f = () |> verbose ? pprint o f
    1.18 -    fun pprint_d f = () |> debug ? pprint o f
    1.19 -    val print = pprint o curry Pretty.blk 0 o pstrs
    1.20 +        print o Pretty.string_of
    1.21 +    fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
    1.22 +    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
    1.23 +    fun pprint_d f = () |> debug ? pprint tracing o f
    1.24 +    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
    1.25  (*
    1.26 -    val print_g = pprint o Pretty.str
    1.27 +    val print_g = pprint tracing o Pretty.str
    1.28  *)
    1.29      val print_n = pprint_n o K o plazy
    1.30      val print_v = pprint_v o K o plazy
    1.31 @@ -323,7 +322,7 @@
    1.32        got_all_mono_user_axioms andalso no_poly_user_axioms
    1.33  
    1.34      fun print_wf (x, (gfp, wf)) =
    1.35 -      pprint (Pretty.blk (0,
    1.36 +      pprint_n (fn () => Pretty.blk (0,
    1.37            pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
    1.38            @ Syntax.pretty_term ctxt (Const x) ::
    1.39            pstrs (if wf then
    1.40 @@ -672,7 +671,7 @@
    1.41            codatatypes_ok
    1.42          fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
    1.43        in
    1.44 -        (pprint (Pretty.chunks
    1.45 +        (pprint_n (fn () => Pretty.chunks
    1.46               [Pretty.blk (0,
    1.47                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.48                            "Nitpick found a" ^
    1.49 @@ -881,7 +880,7 @@
    1.50            if null scopes then
    1.51              print_n (K "The scope specification is inconsistent.")
    1.52            else if verbose then
    1.53 -            pprint (Pretty.chunks
    1.54 +            pprint_n (fn () => Pretty.chunks
    1.55                  [Pretty.blk (0,
    1.56                       pstrs ((if n > 1 then
    1.57                                 "Batch " ^ string_of_int (j + 1) ^ " of " ^
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     2.3 @@ -1815,12 +1815,17 @@
     2.4  
     2.5  (** Axiom extraction/generation **)
     2.6  
     2.7 -fun extensional_equal j (Type (@{type_name fun}, [dom_T, ran_T])) t1 t2 =
     2.8 -    let val var_t = Var (("x", j), dom_T) in
     2.9 +fun extensional_equal j T t1 t2 =
    2.10 +  if is_fun_type T orelse is_set_like_type T then
    2.11 +    let
    2.12 +      val dom_T = pseudo_domain_type T
    2.13 +      val ran_T = pseudo_range_type T
    2.14 +      val var_t = Var (("x", j), dom_T)
    2.15 +    in
    2.16        extensional_equal (j + 1) ran_T (betapply (t1, var_t))
    2.17                          (betapply (t2, var_t))
    2.18      end
    2.19 -  | extensional_equal _ T t1 t2 =
    2.20 +  else
    2.21      Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
    2.22  
    2.23  fun equationalize_term ctxt tag t =
    2.24 @@ -1837,7 +1842,7 @@
    2.25            @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
    2.26          | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
    2.27            @{const Trueprop} $ extensional_equal j T t1 t2
    2.28 -        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^
    2.29 +        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
    2.30                           quote (Syntax.string_of_term ctxt t) ^ ".");
    2.31                  raise SAME ()))
    2.32      |> SOME
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:18 2012 +0100
     3.3 @@ -786,7 +786,7 @@
     3.4                 (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
     3.5           | Op2 (Subset, _, _, u1, u2) =>
     3.6             let
     3.7 -             val dom_T = elem_type (type_of u1)
     3.8 +             val dom_T = pseudo_domain_type (type_of u1)
     3.9               val R1 = rep_of u1
    3.10               val R2 = rep_of u2
    3.11               val (dom_R, ran_R) =
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:18 2012 +0100
     4.3 @@ -1110,8 +1110,9 @@
     4.4        Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
     4.5                      shape_tuple T2 R2 (List.drop (us, arity1))])
     4.6      end
     4.7 -  | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
     4.8 -    Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
     4.9 +  | shape_tuple T (R as Vect (k, R')) us =
    4.10 +    Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
    4.11 +                     (batch_list (length us div k) us))
    4.12    | shape_tuple T _ [u] =
    4.13      if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
    4.14    | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)