support 3 monotonicity calculi in one and fix soundness bug
authorblanchet
Mon Dec 06 13:18:25 2010 +0100 (2010-12-06)
changeset 4099352ee2a187cdb
parent 40992 8cacefe9851c
child 40994 3bdb8df0daf0
support 3 monotonicity calculi in one and fix soundness bug
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -347,7 +347,7 @@
     1.4         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
     1.5        is_number_type ctxt T orelse is_bit_type T
     1.6      fun is_type_actually_monotonic T =
     1.7 -      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     1.8 +      formulas_monotonic hol_ctxt binarize 3 T (nondef_ts, def_ts)
     1.9      fun is_type_kind_of_monotonic T =
    1.10        case triple_lookup (type_match thy) monos T of
    1.11          SOME (SOME false) => false
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     2.3 @@ -11,9 +11,9 @@
     2.4  
     2.5    val trace : bool Unsynchronized.ref
     2.6    val formulas_monotonic :
     2.7 -    hol_context -> bool -> typ -> term list * term list -> bool
     2.8 +    hol_context -> bool -> int -> typ -> term list * term list -> bool
     2.9    val finitize_funs :
    2.10 -    hol_context -> bool -> (typ option * bool option) list -> typ
    2.11 +    hol_context -> bool -> (typ option * bool option) list -> int -> typ
    2.12      -> term list * term list -> term list * term list
    2.13  end;
    2.14  
    2.15 @@ -373,32 +373,41 @@
    2.16  fun add_assign_disjunct _ NONE = NONE
    2.17    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
    2.18  
    2.19 -fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    2.20 +fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    2.21      (case (aa1, aa2) of
    2.22         (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    2.23       | (V x1, A a2) =>
    2.24         SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
    2.25       | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
    2.26 -     | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum)
    2.27 -  | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    2.28 +     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
    2.29 +  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    2.30      (case (aa1, aa2) of
    2.31         (_, A Gen) => SOME accum
    2.32       | (A Gen, A _) => NONE
    2.33       | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    2.34       | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
    2.35 -  | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    2.36 +  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    2.37      SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
    2.38  
    2.39 +fun add_annotation_atom_comp cmp xs aa1 aa2
    2.40 +                             ((asgs, comps, clauses) : constraint_set) =
    2.41 +  (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
    2.42 +                       string_for_comp_op cmp ^ " " ^
    2.43 +                       string_for_annotation_atom aa2);
    2.44 +   case do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) of
    2.45 +     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    2.46 +   | SOME (asgs, comps) => (asgs, comps, clauses))
    2.47 +
    2.48  fun do_mtype_comp _ _ _ _ NONE = NONE
    2.49    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
    2.50    | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    2.51                    (SOME accum) =
    2.52 -     accum |> add_annotation_atom_comp Eq xs aa1 aa2
    2.53 +     accum |> do_annotation_atom_comp Eq xs aa1 aa2
    2.54             |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
    2.55    | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    2.56                    (SOME accum) =
    2.57      (if exists_alpha_sub_mtype M11 then
    2.58 -       accum |> add_annotation_atom_comp Leq xs aa1 aa2
    2.59 +       accum |> do_annotation_atom_comp Leq xs aa1 aa2
    2.60               |> do_mtype_comp Leq xs M21 M11
    2.61               |> (case aa2 of
    2.62                     A Gen => I
    2.63 @@ -435,12 +444,12 @@
    2.64      SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
    2.65    | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
    2.66      SOME (asgs, insert (op =) clause clauses)
    2.67 -  | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum =
    2.68 -    accum |> (if aa <> Gen andalso sn = Plus then
    2.69 +  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) accum =
    2.70 +    accum |> (if a <> Gen andalso sn = Plus then
    2.71                  do_notin_mtype_fv Plus clause M1
    2.72                else
    2.73                  I)
    2.74 -          |> (if aa = Gen orelse sn = Plus then
    2.75 +          |> (if a = Gen orelse sn = Plus then
    2.76                  do_notin_mtype_fv Minus clause M1
    2.77                else
    2.78                  I)
    2.79 @@ -452,7 +461,7 @@
    2.80            |> do_notin_mtype_fv Minus clause M1
    2.81            |> do_notin_mtype_fv Plus clause M2
    2.82    | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
    2.83 -    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru]
    2.84 +    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
    2.85                          (SOME clause) of
    2.86                  NONE => I
    2.87                | SOME clause' => do_notin_mtype_fv Plus clause' M1)
    2.88 @@ -474,15 +483,15 @@
    2.89  val add_mtype_is_concrete = add_notin_mtype_fv Minus
    2.90  val add_mtype_is_complete = add_notin_mtype_fv Plus
    2.91  
    2.92 -fun fst_var n = 2 * n
    2.93 -fun snd_var n = 2 * n + 1
    2.94 -
    2.95  val bool_table =
    2.96    [(Gen, (false, false)),
    2.97     (New, (false, true)),
    2.98     (Fls, (true, false)),
    2.99     (Tru, (true, true))]
   2.100  
   2.101 +fun fst_var n = 2 * n
   2.102 +fun snd_var n = 2 * n + 1
   2.103 +
   2.104  val bools_from_annotation = AList.lookup (op =) bool_table #> the
   2.105  val annotation_from_bools = AList.find (op =) bool_table #> the_single
   2.106  
   2.107 @@ -514,10 +523,14 @@
   2.108      PL.SOr (prop_for_exists_var_assign xs Gen,
   2.109              prop_for_comp (aa1, aa2, cmp, []))
   2.110  
   2.111 -fun fix_bool_options (NONE, NONE) = (false, false)
   2.112 -  | fix_bool_options (NONE, SOME b) = (b, b)
   2.113 -  | fix_bool_options (SOME b, NONE) = (b, b)
   2.114 -  | fix_bool_options (SOME b1, SOME b2) = (b1, b2)
   2.115 +(* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
   2.116 +   the M1, M2, and M3 calculi from Blanchette & Krauss 2011. *)
   2.117 +fun variable_domain calculus =
   2.118 +  [Gen] @ (if calculus > 1 then [Fls] else [])
   2.119 +  @ (if calculus > 2 then [New, Tru] else [])
   2.120 +
   2.121 +fun prop_for_variable_domain calculus x =
   2.122 +  PL.exists (map (curry prop_for_assign x) (variable_domain calculus))
   2.123  
   2.124  fun extract_assigns max_var assigns asgs =
   2.125    fold (fn x => fn accum =>
   2.126 @@ -525,7 +538,8 @@
   2.127               accum
   2.128             else case (fst_var x, snd_var x) |> pairself assigns of
   2.129               (NONE, NONE) => accum
   2.130 -           | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
   2.131 +           | bp => (x, annotation_from_bools (pairself (the_default false) bp))
   2.132 +                   :: accum)
   2.133         (max_var downto 1) asgs
   2.134  
   2.135  fun print_problem asgs comps clauses =
   2.136 @@ -543,14 +557,20 @@
   2.137                               string_for_vars ", " xs)
   2.138         |> space_implode "\n"))
   2.139  
   2.140 -fun solve max_var (asgs, comps, clauses) =
   2.141 +fun solve calculus max_var (asgs, comps, clauses) =
   2.142    let
   2.143      fun do_assigns assigns =
   2.144        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
   2.145      val _ = print_problem asgs comps clauses
   2.146 -    val prop = PL.all (map prop_for_assign asgs @
   2.147 -                       map prop_for_comp comps @
   2.148 -                       map prop_for_assign_clause clauses)
   2.149 +    val prop =
   2.150 +      map prop_for_assign asgs @
   2.151 +      map prop_for_comp comps @
   2.152 +      map prop_for_assign_clause clauses @
   2.153 +      (if calculus < 3 then
   2.154 +         map (prop_for_variable_domain calculus) (1 upto max_var)
   2.155 +       else
   2.156 +         [])
   2.157 +      |> PL.all
   2.158    in
   2.159      if PL.eval (K false) prop then
   2.160        do_assigns (K (SOME false))
   2.161 @@ -581,11 +601,14 @@
   2.162  val initial_gamma =
   2.163    {bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}
   2.164  
   2.165 -fun push_bound T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   2.166 +fun push_bound aa T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   2.167    {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
   2.168 -   bound_frame = bound_frame, frees = frees, consts = consts}
   2.169 +   bound_frame = (length bound_Ts, aa) :: bound_frame, frees = frees,
   2.170 +   consts = consts}
   2.171  fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   2.172 -  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, bound_frame = bound_frame,
   2.173 +  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
   2.174 +   bound_frame = bound_frame
   2.175 +                 |> filter_out (fn (depth, _) => depth = length bound_Ts - 1),
   2.176     frees = frees, consts = consts}
   2.177    handle List.Empty => initial_gamma (* FIXME: needed? *)
   2.178  
   2.179 @@ -648,17 +671,18 @@
   2.180      fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
   2.181        let
   2.182          val abs_M = mtype_for abs_T
   2.183 +        val aa = V (Unsynchronized.inc max_fresh)
   2.184          val (bound_m, accum) =
   2.185 -          accum |>> push_bound abs_T abs_M |> do_term bound_t
   2.186 +          accum |>> push_bound aa abs_T abs_M |> do_term bound_t
   2.187          val expected_bound_M = plus_set_mtype_for_dom abs_M
   2.188          val (body_m, accum) =
   2.189            accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
   2.190                  |> do_term body_t ||> apfst pop_bound
   2.191          val bound_M = mtype_of_mterm bound_m
   2.192 -        val (M1, aa, _) = dest_MFun bound_M
   2.193 +        val (M1, aa', _) = dest_MFun bound_M
   2.194        in
   2.195 -        (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
   2.196 -               MAbs (abs_s, abs_T, M1, aa,
   2.197 +        (MApp (MRaw (t0, MFun (bound_M, aa, bool_M)),
   2.198 +               MAbs (abs_s, abs_T, M1, aa',
   2.199                       MApp (MApp (MRaw (connective_t,
   2.200                                         mtype_for (fastype_of connective_t)),
   2.201                                   MApp (bound_m, MRaw (Bound 0, M1))),
   2.202 @@ -666,13 +690,21 @@
   2.203        end
   2.204      and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
   2.205                               cset)) =
   2.206 -        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   2.207 -                             Syntax.string_of_term ctxt t ^ " : _?");
   2.208 -         case t of
   2.209 -           Const (x as (s, T)) =>
   2.210 -           (case AList.lookup (op =) consts x of
   2.211 -              SOME M => (M, accum)
   2.212 -            | NONE =>
   2.213 +      (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   2.214 +                           Syntax.string_of_term ctxt t ^ " : _?");
   2.215 +       case t of
   2.216 +         Const (x as (s, T)) =>
   2.217 +         (case AList.lookup (op =) consts x of
   2.218 +            SOME M => (M, accum)
   2.219 +          | NONE =>
   2.220 +            case s of
   2.221 +              @{const_name False} =>
   2.222 +              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Fls))
   2.223 +                                      (map snd bound_frame))
   2.224 +            | @{const_name True} =>
   2.225 +              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Tru))
   2.226 +                                      (map snd bound_frame))
   2.227 +            | _ =>
   2.228                if not (could_exist_alpha_subtype alpha_T T) then
   2.229                  (mtype_for T, accum)
   2.230                else case s of
   2.231 @@ -742,8 +774,8 @@
   2.232                      MFun (mtype_for (domain_type T), V x, bool_M)
   2.233                    val a_set_T = domain_type T
   2.234                    val a_M = mtype_for (domain_type a_set_T)
   2.235 -                  val b_set_M = mtype_for_set (range_type (domain_type
   2.236 -                                                               (range_type T)))
   2.237 +                  val b_set_M =
   2.238 +                    mtype_for_set (range_type (domain_type (range_type T)))
   2.239                    val a_set_M = mtype_for_set a_set_T
   2.240                    val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
   2.241                    val ab_set_M = mtype_for_set (nth_range_type 2 T)
   2.242 @@ -788,9 +820,8 @@
   2.243                SOME t' =>
   2.244                let
   2.245                  val M = mtype_for T
   2.246 -                val aa = V (Unsynchronized.inc max_fresh)
   2.247 -                val (m', accum) = do_term t' (accum |>> push_bound T M)
   2.248 -              in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end
   2.249 +                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
   2.250 +              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
   2.251              | NONE =>
   2.252                ((case t' of
   2.253                    t1' $ Bound 0 =>
   2.254 @@ -808,13 +839,17 @@
   2.255                 handle SAME () =>
   2.256                        let
   2.257                          val M = mtype_for T
   2.258 -                        val (m', accum) = do_term t' (accum |>> push_bound T M)
   2.259 -                      in (MAbs (s, T, M, A Gen, m'), accum |>> pop_bound) end))
   2.260 +                        val aa = V (Unsynchronized.inc max_fresh)
   2.261 +                        val (m', accum) =
   2.262 +                          do_term t' (accum |>> push_bound aa T M)
   2.263 +                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   2.264           | (t0 as Const (@{const_name All}, _))
   2.265 -           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
   2.266 +           $ Abs (s', T', (t10 as @{const HOL.implies})
   2.267 +                          $ (t11 $ Bound 0) $ t12) =>
   2.268             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   2.269           | (t0 as Const (@{const_name Ex}, _))
   2.270 -           $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
   2.271 +           $ Abs (s', T', (t10 as @{const HOL.conj})
   2.272 +                          $ (t11 $ Bound 0) $ t12) =>
   2.273             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   2.274           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   2.275             do_term (betapply (t2, t1)) accum
   2.276 @@ -865,10 +900,11 @@
   2.277            fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   2.278              let
   2.279                val abs_M = mtype_for abs_T
   2.280 +              val a = Gen (* FIXME: strengthen *)
   2.281                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   2.282                val (body_m, accum) =
   2.283                  accum ||> side_cond ? add_mtype_is_complete abs_M
   2.284 -                      |>> push_bound abs_T abs_M |> do_formula sn body_t
   2.285 +                      |>> push_bound (A a) abs_T abs_M |> do_formula sn body_t
   2.286                val body_M = mtype_of_mterm body_m
   2.287              in
   2.288                (MApp (MRaw (Const quant_x,
   2.289 @@ -969,7 +1005,7 @@
   2.290          let
   2.291            val abs_M = mtype_for abs_T
   2.292            val (body_m, accum) =
   2.293 -            accum |>> push_bound abs_T abs_M |> do_formula body_t
   2.294 +            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
   2.295            val body_M = mtype_of_mterm body_m
   2.296          in
   2.297            (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
   2.298 @@ -1027,7 +1063,7 @@
   2.299  fun amass f t (ms, accum) =
   2.300    let val (m, accum) = f t accum in (m :: ms, accum) end
   2.301  
   2.302 -fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   2.303 +fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize calculus alpha_T
   2.304            (nondef_ts, def_ts) =
   2.305    let
   2.306      val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   2.307 @@ -1043,7 +1079,7 @@
   2.308      val (def_ms, (gamma, cset)) =
   2.309        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   2.310    in
   2.311 -    case solve (!max_fresh) cset of
   2.312 +    case solve calculus (!max_fresh) cset of
   2.313        SOME asgs => (print_mtype_context ctxt asgs gamma;
   2.314                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   2.315      | _ => NONE
   2.316 @@ -1055,14 +1091,15 @@
   2.317         | MTERM (loc, ms) =>
   2.318           raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
   2.319  
   2.320 -val formulas_monotonic = is_some oooo infer "Monotonicity" false
   2.321 +fun formulas_monotonic hol_ctxt =
   2.322 +  is_some oooo infer "Monotonicity" false hol_ctxt
   2.323  
   2.324  fun fin_fun_constr T1 T2 =
   2.325    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
   2.326  
   2.327 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
   2.328 -                  binarize finitizes alpha_T tsp =
   2.329 -  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   2.330 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
   2.331 +                  finitizes calculus alpha_T tsp =
   2.332 +  case infer "Finiteness" true hol_ctxt binarize calculus alpha_T tsp of
   2.333      SOME (asgs, msp, constr_mtypes) =>
   2.334      if forall (curry (op =) Gen o snd) asgs then
   2.335        tsp
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:18:25 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:18:25 2010 +0100
     3.3 @@ -1261,7 +1261,7 @@
     3.4                                        triple_lookup (type_match thy) monos T
     3.5                                        = SOME (SOME false))
     3.6      in
     3.7 -      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
     3.8 +      fold (finitize_funs hol_ctxt binarize finitizes 3) Ts (nondef_ts, def_ts)
     3.9      end
    3.10  
    3.11  (** Preprocessor entry point **)