src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41000 4bbff1684465
parent 40999 69d0d445c46a
child 41001 11715564e2ad
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:30:57 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:05 2010 +0100
     1.3 @@ -457,37 +457,37 @@
     1.4    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
     1.5    | do_notin_mtype_fv Plus [asg] MAlpha (SOME clauses) =
     1.6      clauses |> add_assign_literal asg
     1.7 -  | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) =
     1.8 -    SOME (insert (op =) clause clauses)
     1.9 -  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset =
    1.10 -    cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus clause M1
    1.11 +  | do_notin_mtype_fv Plus unless MAlpha (SOME clauses) =
    1.12 +    SOME (insert (op =) unless clauses)
    1.13 +  | do_notin_mtype_fv sn unless (MFun (M1, A a, M2)) cset =
    1.14 +    cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus unless M1
    1.15               else I)
    1.16 -         |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus clause M1
    1.17 +         |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus unless M1
    1.18               else I)
    1.19 -         |> do_notin_mtype_fv sn clause M2
    1.20 -  | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset =
    1.21 -    cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME clause) of
    1.22 +         |> do_notin_mtype_fv sn unless M2
    1.23 +  | do_notin_mtype_fv Plus unless (MFun (M1, V x, M2)) cset =
    1.24 +    cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME unless) of
    1.25                 NONE => I
    1.26 -             | SOME clause' => do_notin_mtype_fv Plus clause' M1)
    1.27 -         |> do_notin_mtype_fv Minus clause M1
    1.28 -         |> do_notin_mtype_fv Plus clause M2
    1.29 -  | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset =
    1.30 +             | SOME unless' => do_notin_mtype_fv Plus unless' M1)
    1.31 +         |> do_notin_mtype_fv Minus unless M1
    1.32 +         |> do_notin_mtype_fv Plus unless M2
    1.33 +  | do_notin_mtype_fv Minus unless (MFun (M1, V x, M2)) cset =
    1.34      cset |> (case fold (fn a => add_assign_disjunct (x, (Plus, a))) [Fls, Tru]
    1.35 -                       (SOME clause) of
    1.36 +                       (SOME unless) of
    1.37                 NONE => I
    1.38 -             | SOME clause' => do_notin_mtype_fv Plus clause' M1)
    1.39 -         |> do_notin_mtype_fv Minus clause M2
    1.40 -  | do_notin_mtype_fv sn clause (MPair (M1, M2)) cset =
    1.41 -    cset |> fold (do_notin_mtype_fv sn clause) [M1, M2]
    1.42 -  | do_notin_mtype_fv sn clause (MType (_, Ms)) cset =
    1.43 -    cset |> fold (do_notin_mtype_fv sn clause) Ms
    1.44 +             | SOME unless' => do_notin_mtype_fv Plus unless' M1)
    1.45 +         |> do_notin_mtype_fv Minus unless M2
    1.46 +  | do_notin_mtype_fv sn unless (MPair (M1, M2)) cset =
    1.47 +    cset |> fold (do_notin_mtype_fv sn unless) [M1, M2]
    1.48 +  | do_notin_mtype_fv sn unless (MType (_, Ms)) cset =
    1.49 +    cset |> fold (do_notin_mtype_fv sn unless) Ms
    1.50   | do_notin_mtype_fv _ _ M _ =
    1.51     raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
    1.52  
    1.53 -fun add_notin_mtype_fv sn M (comps, clauses) =
    1.54 +fun add_notin_mtype_fv sn unless M (comps, clauses) =
    1.55    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
    1.56                         (case sn of Minus => "concrete" | Plus => "complete"));
    1.57 -   case SOME clauses |> do_notin_mtype_fv sn [] M of
    1.58 +   case SOME clauses |> do_notin_mtype_fv sn unless M of
    1.59       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.60     | SOME clauses => (comps, clauses))
    1.61  
    1.62 @@ -695,8 +695,8 @@
    1.63      | V x => add_annotation_clause_from_quasi_clause rest accum
    1.64               |> Option.map (cons (x, (sign_for_comp_op cmp, a)))
    1.65  
    1.66 -fun assign_clause_from_quasi_clause clause =
    1.67 -  add_annotation_clause_from_quasi_clause clause (SOME [])
    1.68 +fun assign_clause_from_quasi_clause unless =
    1.69 +  add_annotation_clause_from_quasi_clause unless (SOME [])
    1.70  
    1.71  fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 =
    1.72    (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^
    1.73 @@ -767,7 +767,7 @@
    1.74          val body_M = mtype_for (body_type T)
    1.75        in
    1.76          (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
    1.77 -         (gamma, cset |> add_mtype_is_complete abs_M))
    1.78 +         (gamma, cset |> add_mtype_is_complete [] abs_M))
    1.79        end
    1.80      fun do_equals T (gamma, cset) =
    1.81        let
    1.82 @@ -775,7 +775,7 @@
    1.83          val aa = V (Unsynchronized.inc max_fresh)
    1.84        in
    1.85          (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))),
    1.86 -         (gamma, cset |> add_mtype_is_concrete M
    1.87 +         (gamma, cset |> add_mtype_is_concrete [] M
    1.88                        |> add_annotation_atom_comp Leq [] (A Fls) aa))
    1.89        end
    1.90      fun do_robust_set_operation T (gamma, cset) =
    1.91 @@ -797,7 +797,7 @@
    1.92              else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2)
    1.93            | custom_mtype_for T = mtype_for T
    1.94        in
    1.95 -        (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
    1.96 +        (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete [] set_M))
    1.97        end
    1.98      fun do_pair_constr T accum =
    1.99        case mtype_for (nth_range_type 2 T) of
   1.100 @@ -1067,89 +1067,89 @@
   1.101            accum)
   1.102    end
   1.103  
   1.104 -fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
   1.105 +fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,
   1.106 +                                        ...}) =
   1.107    let
   1.108      val mtype_for = fresh_mtype_for_type mdata false
   1.109      val do_term = consider_term mdata
   1.110      fun do_formula sn t (accum as (gamma, _)) =
   1.111 -        let
   1.112 -          fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   1.113 -            let
   1.114 -              val abs_M = mtype_for abs_T
   1.115 -              val a = Gen (* FIXME: strengthen *)
   1.116 -              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   1.117 -              val (body_m, accum) =
   1.118 -                accum ||> side_cond ? add_mtype_is_complete abs_M
   1.119 -                      |>> push_bound (A a) abs_T abs_M |> do_formula sn body_t
   1.120 -              val body_M = mtype_of_mterm body_m
   1.121 -            in
   1.122 -              (MApp (MRaw (Const quant_x,
   1.123 -                           MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
   1.124 -                     MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   1.125 -               accum |>> pop_bound)
   1.126 -            end
   1.127 -          fun do_equals x t1 t2 =
   1.128 -            case sn of
   1.129 -              Plus => do_term t accum
   1.130 -            | Minus => consider_general_equals mdata false x t1 t2 accum
   1.131 -        in
   1.132 -          (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   1.133 -                               " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   1.134 -                               " : o\<^sup>" ^ string_for_sign sn ^ "?");
   1.135 -           case t of
   1.136 -             Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   1.137 -             do_quantifier x s1 T1 t1
   1.138 -           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
   1.139 -           | @{const Trueprop} $ t1 =>
   1.140 -             let val (m1, accum) = do_formula sn t1 accum in
   1.141 -               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
   1.142 -                      m1), accum)
   1.143 -             end
   1.144 -           | @{const Not} $ t1 =>
   1.145 -             let val (m1, accum) = do_formula (negate_sign sn) t1 accum in
   1.146 -               (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
   1.147 +      let
   1.148 +        fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   1.149 +          let
   1.150 +            val abs_M = mtype_for abs_T
   1.151 +            val x = Unsynchronized.inc max_fresh
   1.152 +            val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   1.153 +            val (body_m, accum) =
   1.154 +              accum ||> side_cond
   1.155 +                        ? add_mtype_is_complete [(x, (Minus, Fls))] abs_M
   1.156 +                    |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
   1.157 +            val body_M = mtype_of_mterm body_m
   1.158 +          in
   1.159 +            (MApp (MRaw (Const quant_x,
   1.160 +                         MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
   1.161 +                   MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   1.162 +             accum |>> pop_bound)
   1.163 +          end
   1.164 +        fun do_equals x t1 t2 =
   1.165 +          case sn of
   1.166 +            Plus => do_term t accum
   1.167 +          | Minus => consider_general_equals mdata false x t1 t2 accum
   1.168 +      in
   1.169 +        (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   1.170 +                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   1.171 +                             " : o\<^sup>" ^ string_for_sign sn ^ "?");
   1.172 +         case t of
   1.173 +           Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   1.174 +           do_quantifier x s1 T1 t1
   1.175 +         | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
   1.176 +         | @{const Trueprop} $ t1 =>
   1.177 +           let val (m1, accum) = do_formula sn t1 accum in
   1.178 +             (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
   1.179 +                    m1), accum)
   1.180 +           end
   1.181 +         | @{const Not} $ t1 =>
   1.182 +           let val (m1, accum) = do_formula (negate_sign sn) t1 accum in
   1.183 +             (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
   1.184 +              accum)
   1.185 +           end
   1.186 +         | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   1.187 +           do_quantifier x s1 T1 t1
   1.188 +         | Const (x0 as (@{const_name Ex}, T0))
   1.189 +           $ (t1 as Abs (s1, T1, t1')) =>
   1.190 +           (case sn of
   1.191 +              Plus => do_quantifier x0 s1 T1 t1'
   1.192 +            | Minus =>
   1.193 +              (* FIXME: Move elsewhere *)
   1.194 +              do_term (@{const Not}
   1.195 +                       $ (HOLogic.eq_const (domain_type T0) $ t1
   1.196 +                          $ Abs (Name.uu, T1, @{const False}))) accum)
   1.197 +         | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   1.198 +           do_equals x t1 t2
   1.199 +         | Const (@{const_name Let}, _) $ t1 $ t2 =>
   1.200 +           do_formula sn (betapply (t2, t1)) accum
   1.201 +         | (t0 as Const (s0, _)) $ t1 $ t2 =>
   1.202 +           if s0 = @{const_name "==>"} orelse
   1.203 +              s0 = @{const_name Pure.conjunction} orelse
   1.204 +              s0 = @{const_name conj} orelse s0 = @{const_name disj} orelse
   1.205 +              s0 = @{const_name implies} then
   1.206 +             let
   1.207 +               val impl = (s0 = @{const_name "==>"} orelse
   1.208 +                           s0 = @{const_name implies})
   1.209 +               val (m1, accum) = do_formula (sn |> impl ? negate_sign) t1 accum
   1.210 +               val (m2, accum) = do_formula sn t2 accum
   1.211 +             in
   1.212 +               (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.213                  accum)
   1.214               end
   1.215 -           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   1.216 -             do_quantifier x s1 T1 t1
   1.217 -           | Const (x0 as (@{const_name Ex}, T0))
   1.218 -             $ (t1 as Abs (s1, T1, t1')) =>
   1.219 -             (case sn of
   1.220 -                Plus => do_quantifier x0 s1 T1 t1'
   1.221 -              | Minus =>
   1.222 -                (* FIXME: Move elsewhere *)
   1.223 -                do_term (@{const Not}
   1.224 -                         $ (HOLogic.eq_const (domain_type T0) $ t1
   1.225 -                            $ Abs (Name.uu, T1, @{const False}))) accum)
   1.226 -           | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   1.227 -             do_equals x t1 t2
   1.228 -           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   1.229 -             do_formula sn (betapply (t2, t1)) accum
   1.230 -           | (t0 as Const (s0, _)) $ t1 $ t2 =>
   1.231 -             if s0 = @{const_name "==>"} orelse
   1.232 -                s0 = @{const_name Pure.conjunction} orelse
   1.233 -                s0 = @{const_name conj} orelse
   1.234 -                s0 = @{const_name disj} orelse
   1.235 -                s0 = @{const_name implies} then
   1.236 -               let
   1.237 -                 val impl = (s0 = @{const_name "==>"} orelse
   1.238 -                             s0 = @{const_name implies})
   1.239 -                 val (m1, accum) =
   1.240 -                   do_formula (sn |> impl ? negate_sign) t1 accum
   1.241 -                 val (m2, accum) = do_formula sn t2 accum
   1.242 -               in
   1.243 -                 (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   1.244 -                  accum)
   1.245 -               end
   1.246 -             else
   1.247 -               do_term t accum
   1.248 -           | _ => do_term t accum)
   1.249 -        end
   1.250 -        |> tap (fn (m, (gamma, _)) =>
   1.251 -                   trace_msg (fn () => string_for_mcontext ctxt t gamma ^
   1.252 -                                       " \<turnstile> " ^
   1.253 -                                       string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.254 -                                       string_for_sign sn))
   1.255 +           else
   1.256 +             do_term t accum
   1.257 +         | _ => do_term t accum)
   1.258 +      end
   1.259 +      |> tap (fn (m, (gamma, _)) =>
   1.260 +                 trace_msg (fn () => string_for_mcontext ctxt t gamma ^
   1.261 +                                     " \<turnstile> " ^
   1.262 +                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.263 +                                     string_for_sign sn))
   1.264    in do_formula end
   1.265  
   1.266  (* The harmless axiom optimization below is somewhat too aggressive in the face