tune parentheses and indentation
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 4100401f33bf79596
parent 41003 7e2a7bd55a00
child 41005 60d931de0709
tune parentheses and indentation
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -1061,42 +1061,41 @@
     1.4              Plus => do_term t accum
     1.5            | Minus => consider_general_equals mdata false x t1 t2 accum
     1.6        in
     1.7 -        (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
     1.8 -                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
     1.9 -                             " : o\<^sup>" ^ string_for_sign sn ^ "?");
    1.10 -         case t of
    1.11 -           Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    1.12 -           do_quantifier x s1 T1 t1
    1.13 -         | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    1.14 -         | @{const Trueprop} $ t1 =>
    1.15 -           let val (m1, accum) = do_formula sn t1 accum in
    1.16 -             (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    1.17 -                    m1), accum)
    1.18 -           end
    1.19 -         | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    1.20 -           do_quantifier x s1 T1 t1
    1.21 -         | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
    1.22 -           (case sn of
    1.23 -              Plus => do_quantifier x0 s1 T1 t1'
    1.24 -            | Minus =>
    1.25 -              (* FIXME: Move elsewhere *)
    1.26 -              do_term (@{const Not}
    1.27 -                       $ (HOLogic.eq_const (domain_type T0) $ t1
    1.28 -                          $ Abs (Name.uu, T1, @{const False}))) accum)
    1.29 -         | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.30 -           do_equals x t1 t2
    1.31 -         | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.32 -           do_formula sn (betapply (t2, t1)) accum
    1.33 -         | @{const Pure.conjunction} $ t1 $ t2 =>
    1.34 -           do_connect meta_conj_triple false t1 t2 accum
    1.35 -         | @{const "==>"} $ t1 $ t2 =>
    1.36 -           do_connect meta_imp_triple true t1 t2 accum
    1.37 -         | @{const Not} $ t1 =>
    1.38 -           do_connect imp_triple true t1 @{const False} accum
    1.39 -         | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
    1.40 -         | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
    1.41 -         | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
    1.42 -         | _ => do_term t accum)
    1.43 +        trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
    1.44 +                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
    1.45 +                            " : o\<^sup>" ^ string_for_sign sn ^ "?");
    1.46 +        case t of
    1.47 +          Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    1.48 +          do_quantifier x s1 T1 t1
    1.49 +        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    1.50 +        | @{const Trueprop} $ t1 =>
    1.51 +          let val (m1, accum) = do_formula sn t1 accum in
    1.52 +            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
    1.53 +             accum)
    1.54 +          end
    1.55 +        | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    1.56 +          do_quantifier x s1 T1 t1
    1.57 +        | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
    1.58 +          (case sn of
    1.59 +             Plus => do_quantifier x0 s1 T1 t1'
    1.60 +           | Minus =>
    1.61 +             (* FIXME: Move elsewhere *)
    1.62 +             do_term (@{const Not}
    1.63 +                      $ (HOLogic.eq_const (domain_type T0) $ t1
    1.64 +                         $ Abs (Name.uu, T1, @{const False}))) accum)
    1.65 +        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_equals x t1 t2
    1.66 +        | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.67 +          do_formula sn (betapply (t2, t1)) accum
    1.68 +        | @{const Pure.conjunction} $ t1 $ t2 =>
    1.69 +          do_connect meta_conj_triple false t1 t2 accum
    1.70 +        | @{const "==>"} $ t1 $ t2 =>
    1.71 +          do_connect meta_imp_triple true t1 t2 accum
    1.72 +        | @{const Not} $ t1 =>
    1.73 +          do_connect imp_triple true t1 @{const False} accum
    1.74 +        | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
    1.75 +        | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
    1.76 +        | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
    1.77 +        | _ => do_term t accum
    1.78        end
    1.79        |> tap (fn (m, (gamma, _)) =>
    1.80                   trace_msg (fn () => string_for_mcontext ctxt t gamma ^