src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 37704 c6161bee8486
parent 37678 0040bafffdef
child 38179 7207321df8af
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jul 03 00:49:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jul 03 00:50:35 2010 +0200
     1.3 @@ -628,7 +628,9 @@
     1.4        end
     1.5      and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
     1.6                               cset)) =
     1.7 -        (case t of
     1.8 +        (print_g (fn () => "  \<Gamma> \<turnstile> " ^
     1.9 +                           Syntax.string_of_term ctxt t ^ " : _?");
    1.10 +         case t of
    1.11             Const (x as (s, T)) =>
    1.12             (case AList.lookup (op =) consts x of
    1.13                SOME M => (M, accum)
    1.14 @@ -846,48 +848,54 @@
    1.15                Plus => do_term t accum
    1.16              | Minus => consider_general_equals mdata false x t1 t2 accum
    1.17          in
    1.18 -          case t of
    1.19 -            Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    1.20 -            do_quantifier x s1 T1 t1
    1.21 -          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    1.22 -          | @{const Trueprop} $ t1 =>
    1.23 -            let val (m1, accum) = do_formula sn t1 accum in
    1.24 -              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    1.25 -                     m1), accum)
    1.26 -            end
    1.27 -          | @{const Not} $ t1 =>
    1.28 -            let val (m1, accum) = do_formula (negate sn) t1 accum in
    1.29 -              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
    1.30 -               accum)
    1.31 -            end
    1.32 -          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    1.33 -            do_quantifier x s1 T1 t1
    1.34 -          | Const (x0 as (s0 as @{const_name Ex}, T0))
    1.35 -            $ (t1 as Abs (s1, T1, t1')) =>
    1.36 -            (case sn of
    1.37 -               Plus => do_quantifier x0 s1 T1 t1'
    1.38 -             | Minus =>
    1.39 -               (* FIXME: Move elsewhere *)
    1.40 -               do_term (@{const Not}
    1.41 -                        $ (HOLogic.eq_const (domain_type T0) $ t1
    1.42 -                           $ Abs (Name.uu, T1, @{const False}))) accum)
    1.43 -          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.44 -            do_equals x t1 t2
    1.45 -          | (t0 as Const (s0, _)) $ t1 $ t2 =>
    1.46 -            if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
    1.47 -               s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
    1.48 -              let
    1.49 -                val impl = (s0 = @{const_name "==>"} orelse
    1.50 -                           s0 = @{const_name "op -->"})
    1.51 -                val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
    1.52 -                val (m2, accum) = do_formula sn t2 accum
    1.53 -              in
    1.54 -                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
    1.55 -                 accum)
    1.56 -              end 
    1.57 -            else
    1.58 -              do_term t accum
    1.59 -          | _ => do_term t accum
    1.60 +          (print_g (fn () => "  \<Gamma> \<turnstile> " ^
    1.61 +                           Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
    1.62 +                           string_for_sign sn ^ "?");
    1.63 +           case t of
    1.64 +             Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    1.65 +             do_quantifier x s1 T1 t1
    1.66 +           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
    1.67 +           | @{const Trueprop} $ t1 =>
    1.68 +             let val (m1, accum) = do_formula sn t1 accum in
    1.69 +               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    1.70 +                      m1), accum)
    1.71 +             end
    1.72 +           | @{const Not} $ t1 =>
    1.73 +             let val (m1, accum) = do_formula (negate sn) t1 accum in
    1.74 +               (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
    1.75 +                accum)
    1.76 +             end
    1.77 +           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
    1.78 +             do_quantifier x s1 T1 t1
    1.79 +           | Const (x0 as (s0 as @{const_name Ex}, T0))
    1.80 +             $ (t1 as Abs (s1, T1, t1')) =>
    1.81 +             (case sn of
    1.82 +                Plus => do_quantifier x0 s1 T1 t1'
    1.83 +              | Minus =>
    1.84 +                (* FIXME: Move elsewhere *)
    1.85 +                do_term (@{const Not}
    1.86 +                         $ (HOLogic.eq_const (domain_type T0) $ t1
    1.87 +                            $ Abs (Name.uu, T1, @{const False}))) accum)
    1.88 +           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
    1.89 +             do_equals x t1 t2
    1.90 +           | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.91 +             do_formula sn (betapply (t2, t1)) accum
    1.92 +           | (t0 as Const (s0, _)) $ t1 $ t2 =>
    1.93 +             if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
    1.94 +                s0 = @{const_name "op |"} orelse
    1.95 +                s0 = @{const_name "op -->"} then
    1.96 +               let
    1.97 +                 val impl = (s0 = @{const_name "==>"} orelse
    1.98 +                             s0 = @{const_name "op -->"})
    1.99 +                 val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
   1.100 +                 val (m2, accum) = do_formula sn t2 accum
   1.101 +               in
   1.102 +                 (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.103 +                  accum)
   1.104 +               end 
   1.105 +             else
   1.106 +               do_term t accum
   1.107 +           | _ => do_term t accum)
   1.108          end
   1.109          |> tap (fn (m, _) =>
   1.110                     print_g (fn () => "\<Gamma> \<turnstile> " ^