src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40993 52ee2a187cdb
parent 40991 902ad76994d5
child 40994 3bdb8df0daf0
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -11,9 +11,9 @@
     1.4  
     1.5    val trace : bool Unsynchronized.ref
     1.6    val formulas_monotonic :
     1.7 -    hol_context -> bool -> typ -> term list * term list -> bool
     1.8 +    hol_context -> bool -> int -> typ -> term list * term list -> bool
     1.9    val finitize_funs :
    1.10 -    hol_context -> bool -> (typ option * bool option) list -> typ
    1.11 +    hol_context -> bool -> (typ option * bool option) list -> int -> typ
    1.12      -> term list * term list -> term list * term list
    1.13  end;
    1.14  
    1.15 @@ -373,32 +373,41 @@
    1.16  fun add_assign_disjunct _ NONE = NONE
    1.17    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
    1.18  
    1.19 -fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    1.20 +fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    1.21      (case (aa1, aa2) of
    1.22         (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.23       | (V x1, A a2) =>
    1.24         SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
    1.25       | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
    1.26 -     | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum)
    1.27 -  | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    1.28 +     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
    1.29 +  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    1.30      (case (aa1, aa2) of
    1.31         (_, A Gen) => SOME accum
    1.32       | (A Gen, A _) => NONE
    1.33       | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.34       | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
    1.35 -  | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    1.36 +  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    1.37      SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
    1.38  
    1.39 +fun add_annotation_atom_comp cmp xs aa1 aa2
    1.40 +                             ((asgs, comps, clauses) : constraint_set) =
    1.41 +  (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
    1.42 +                       string_for_comp_op cmp ^ " " ^
    1.43 +                       string_for_annotation_atom aa2);
    1.44 +   case do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) of
    1.45 +     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.46 +   | SOME (asgs, comps) => (asgs, comps, clauses))
    1.47 +
    1.48  fun do_mtype_comp _ _ _ _ NONE = NONE
    1.49    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
    1.50    | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    1.51                    (SOME accum) =
    1.52 -     accum |> add_annotation_atom_comp Eq xs aa1 aa2
    1.53 +     accum |> do_annotation_atom_comp Eq xs aa1 aa2
    1.54             |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
    1.55    | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    1.56                    (SOME accum) =
    1.57      (if exists_alpha_sub_mtype M11 then
    1.58 -       accum |> add_annotation_atom_comp Leq xs aa1 aa2
    1.59 +       accum |> do_annotation_atom_comp Leq xs aa1 aa2
    1.60               |> do_mtype_comp Leq xs M21 M11
    1.61               |> (case aa2 of
    1.62                     A Gen => I
    1.63 @@ -435,12 +444,12 @@
    1.64      SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
    1.65    | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
    1.66      SOME (asgs, insert (op =) clause clauses)
    1.67 -  | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum =
    1.68 -    accum |> (if aa <> Gen andalso sn = Plus then
    1.69 +  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) accum =
    1.70 +    accum |> (if a <> Gen andalso sn = Plus then
    1.71                  do_notin_mtype_fv Plus clause M1
    1.72                else
    1.73                  I)
    1.74 -          |> (if aa = Gen orelse sn = Plus then
    1.75 +          |> (if a = Gen orelse sn = Plus then
    1.76                  do_notin_mtype_fv Minus clause M1
    1.77                else
    1.78                  I)
    1.79 @@ -452,7 +461,7 @@
    1.80            |> do_notin_mtype_fv Minus clause M1
    1.81            |> do_notin_mtype_fv Plus clause M2
    1.82    | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
    1.83 -    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru]
    1.84 +    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
    1.85                          (SOME clause) of
    1.86                  NONE => I
    1.87                | SOME clause' => do_notin_mtype_fv Plus clause' M1)
    1.88 @@ -474,15 +483,15 @@
    1.89  val add_mtype_is_concrete = add_notin_mtype_fv Minus
    1.90  val add_mtype_is_complete = add_notin_mtype_fv Plus
    1.91  
    1.92 -fun fst_var n = 2 * n
    1.93 -fun snd_var n = 2 * n + 1
    1.94 -
    1.95  val bool_table =
    1.96    [(Gen, (false, false)),
    1.97     (New, (false, true)),
    1.98     (Fls, (true, false)),
    1.99     (Tru, (true, true))]
   1.100  
   1.101 +fun fst_var n = 2 * n
   1.102 +fun snd_var n = 2 * n + 1
   1.103 +
   1.104  val bools_from_annotation = AList.lookup (op =) bool_table #> the
   1.105  val annotation_from_bools = AList.find (op =) bool_table #> the_single
   1.106  
   1.107 @@ -514,10 +523,14 @@
   1.108      PL.SOr (prop_for_exists_var_assign xs Gen,
   1.109              prop_for_comp (aa1, aa2, cmp, []))
   1.110  
   1.111 -fun fix_bool_options (NONE, NONE) = (false, false)
   1.112 -  | fix_bool_options (NONE, SOME b) = (b, b)
   1.113 -  | fix_bool_options (SOME b, NONE) = (b, b)
   1.114 -  | fix_bool_options (SOME b1, SOME b2) = (b1, b2)
   1.115 +(* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
   1.116 +   the M1, M2, and M3 calculi from Blanchette & Krauss 2011. *)
   1.117 +fun variable_domain calculus =
   1.118 +  [Gen] @ (if calculus > 1 then [Fls] else [])
   1.119 +  @ (if calculus > 2 then [New, Tru] else [])
   1.120 +
   1.121 +fun prop_for_variable_domain calculus x =
   1.122 +  PL.exists (map (curry prop_for_assign x) (variable_domain calculus))
   1.123  
   1.124  fun extract_assigns max_var assigns asgs =
   1.125    fold (fn x => fn accum =>
   1.126 @@ -525,7 +538,8 @@
   1.127               accum
   1.128             else case (fst_var x, snd_var x) |> pairself assigns of
   1.129               (NONE, NONE) => accum
   1.130 -           | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
   1.131 +           | bp => (x, annotation_from_bools (pairself (the_default false) bp))
   1.132 +                   :: accum)
   1.133         (max_var downto 1) asgs
   1.134  
   1.135  fun print_problem asgs comps clauses =
   1.136 @@ -543,14 +557,20 @@
   1.137                               string_for_vars ", " xs)
   1.138         |> space_implode "\n"))
   1.139  
   1.140 -fun solve max_var (asgs, comps, clauses) =
   1.141 +fun solve calculus max_var (asgs, comps, clauses) =
   1.142    let
   1.143      fun do_assigns assigns =
   1.144        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
   1.145      val _ = print_problem asgs comps clauses
   1.146 -    val prop = PL.all (map prop_for_assign asgs @
   1.147 -                       map prop_for_comp comps @
   1.148 -                       map prop_for_assign_clause clauses)
   1.149 +    val prop =
   1.150 +      map prop_for_assign asgs @
   1.151 +      map prop_for_comp comps @
   1.152 +      map prop_for_assign_clause clauses @
   1.153 +      (if calculus < 3 then
   1.154 +         map (prop_for_variable_domain calculus) (1 upto max_var)
   1.155 +       else
   1.156 +         [])
   1.157 +      |> PL.all
   1.158    in
   1.159      if PL.eval (K false) prop then
   1.160        do_assigns (K (SOME false))
   1.161 @@ -581,11 +601,14 @@
   1.162  val initial_gamma =
   1.163    {bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}
   1.164  
   1.165 -fun push_bound T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   1.166 +fun push_bound aa T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   1.167    {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
   1.168 -   bound_frame = bound_frame, frees = frees, consts = consts}
   1.169 +   bound_frame = (length bound_Ts, aa) :: bound_frame, frees = frees,
   1.170 +   consts = consts}
   1.171  fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
   1.172 -  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, bound_frame = bound_frame,
   1.173 +  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
   1.174 +   bound_frame = bound_frame
   1.175 +                 |> filter_out (fn (depth, _) => depth = length bound_Ts - 1),
   1.176     frees = frees, consts = consts}
   1.177    handle List.Empty => initial_gamma (* FIXME: needed? *)
   1.178  
   1.179 @@ -648,17 +671,18 @@
   1.180      fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
   1.181        let
   1.182          val abs_M = mtype_for abs_T
   1.183 +        val aa = V (Unsynchronized.inc max_fresh)
   1.184          val (bound_m, accum) =
   1.185 -          accum |>> push_bound abs_T abs_M |> do_term bound_t
   1.186 +          accum |>> push_bound aa abs_T abs_M |> do_term bound_t
   1.187          val expected_bound_M = plus_set_mtype_for_dom abs_M
   1.188          val (body_m, accum) =
   1.189            accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
   1.190                  |> do_term body_t ||> apfst pop_bound
   1.191          val bound_M = mtype_of_mterm bound_m
   1.192 -        val (M1, aa, _) = dest_MFun bound_M
   1.193 +        val (M1, aa', _) = dest_MFun bound_M
   1.194        in
   1.195 -        (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
   1.196 -               MAbs (abs_s, abs_T, M1, aa,
   1.197 +        (MApp (MRaw (t0, MFun (bound_M, aa, bool_M)),
   1.198 +               MAbs (abs_s, abs_T, M1, aa',
   1.199                       MApp (MApp (MRaw (connective_t,
   1.200                                         mtype_for (fastype_of connective_t)),
   1.201                                   MApp (bound_m, MRaw (Bound 0, M1))),
   1.202 @@ -666,13 +690,21 @@
   1.203        end
   1.204      and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
   1.205                               cset)) =
   1.206 -        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.207 -                             Syntax.string_of_term ctxt t ^ " : _?");
   1.208 -         case t of
   1.209 -           Const (x as (s, T)) =>
   1.210 -           (case AList.lookup (op =) consts x of
   1.211 -              SOME M => (M, accum)
   1.212 -            | NONE =>
   1.213 +      (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.214 +                           Syntax.string_of_term ctxt t ^ " : _?");
   1.215 +       case t of
   1.216 +         Const (x as (s, T)) =>
   1.217 +         (case AList.lookup (op =) consts x of
   1.218 +            SOME M => (M, accum)
   1.219 +          | NONE =>
   1.220 +            case s of
   1.221 +              @{const_name False} =>
   1.222 +              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Fls))
   1.223 +                                      (map snd bound_frame))
   1.224 +            | @{const_name True} =>
   1.225 +              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Tru))
   1.226 +                                      (map snd bound_frame))
   1.227 +            | _ =>
   1.228                if not (could_exist_alpha_subtype alpha_T T) then
   1.229                  (mtype_for T, accum)
   1.230                else case s of
   1.231 @@ -742,8 +774,8 @@
   1.232                      MFun (mtype_for (domain_type T), V x, bool_M)
   1.233                    val a_set_T = domain_type T
   1.234                    val a_M = mtype_for (domain_type a_set_T)
   1.235 -                  val b_set_M = mtype_for_set (range_type (domain_type
   1.236 -                                                               (range_type T)))
   1.237 +                  val b_set_M =
   1.238 +                    mtype_for_set (range_type (domain_type (range_type T)))
   1.239                    val a_set_M = mtype_for_set a_set_T
   1.240                    val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
   1.241                    val ab_set_M = mtype_for_set (nth_range_type 2 T)
   1.242 @@ -788,9 +820,8 @@
   1.243                SOME t' =>
   1.244                let
   1.245                  val M = mtype_for T
   1.246 -                val aa = V (Unsynchronized.inc max_fresh)
   1.247 -                val (m', accum) = do_term t' (accum |>> push_bound T M)
   1.248 -              in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end
   1.249 +                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
   1.250 +              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
   1.251              | NONE =>
   1.252                ((case t' of
   1.253                    t1' $ Bound 0 =>
   1.254 @@ -808,13 +839,17 @@
   1.255                 handle SAME () =>
   1.256                        let
   1.257                          val M = mtype_for T
   1.258 -                        val (m', accum) = do_term t' (accum |>> push_bound T M)
   1.259 -                      in (MAbs (s, T, M, A Gen, m'), accum |>> pop_bound) end))
   1.260 +                        val aa = V (Unsynchronized.inc max_fresh)
   1.261 +                        val (m', accum) =
   1.262 +                          do_term t' (accum |>> push_bound aa T M)
   1.263 +                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   1.264           | (t0 as Const (@{const_name All}, _))
   1.265 -           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
   1.266 +           $ Abs (s', T', (t10 as @{const HOL.implies})
   1.267 +                          $ (t11 $ Bound 0) $ t12) =>
   1.268             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   1.269           | (t0 as Const (@{const_name Ex}, _))
   1.270 -           $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
   1.271 +           $ Abs (s', T', (t10 as @{const HOL.conj})
   1.272 +                          $ (t11 $ Bound 0) $ t12) =>
   1.273             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   1.274           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   1.275             do_term (betapply (t2, t1)) accum
   1.276 @@ -865,10 +900,11 @@
   1.277            fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   1.278              let
   1.279                val abs_M = mtype_for abs_T
   1.280 +              val a = Gen (* FIXME: strengthen *)
   1.281                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   1.282                val (body_m, accum) =
   1.283                  accum ||> side_cond ? add_mtype_is_complete abs_M
   1.284 -                      |>> push_bound abs_T abs_M |> do_formula sn body_t
   1.285 +                      |>> push_bound (A a) abs_T abs_M |> do_formula sn body_t
   1.286                val body_M = mtype_of_mterm body_m
   1.287              in
   1.288                (MApp (MRaw (Const quant_x,
   1.289 @@ -969,7 +1005,7 @@
   1.290          let
   1.291            val abs_M = mtype_for abs_T
   1.292            val (body_m, accum) =
   1.293 -            accum |>> push_bound abs_T abs_M |> do_formula body_t
   1.294 +            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
   1.295            val body_M = mtype_of_mterm body_m
   1.296          in
   1.297            (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
   1.298 @@ -1027,7 +1063,7 @@
   1.299  fun amass f t (ms, accum) =
   1.300    let val (m, accum) = f t accum in (m :: ms, accum) end
   1.301  
   1.302 -fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   1.303 +fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize calculus alpha_T
   1.304            (nondef_ts, def_ts) =
   1.305    let
   1.306      val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   1.307 @@ -1043,7 +1079,7 @@
   1.308      val (def_ms, (gamma, cset)) =
   1.309        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   1.310    in
   1.311 -    case solve (!max_fresh) cset of
   1.312 +    case solve calculus (!max_fresh) cset of
   1.313        SOME asgs => (print_mtype_context ctxt asgs gamma;
   1.314                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   1.315      | _ => NONE
   1.316 @@ -1055,14 +1091,15 @@
   1.317         | MTERM (loc, ms) =>
   1.318           raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
   1.319  
   1.320 -val formulas_monotonic = is_some oooo infer "Monotonicity" false
   1.321 +fun formulas_monotonic hol_ctxt =
   1.322 +  is_some oooo infer "Monotonicity" false hol_ctxt
   1.323  
   1.324  fun fin_fun_constr T1 T2 =
   1.325    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
   1.326  
   1.327 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
   1.328 -                  binarize finitizes alpha_T tsp =
   1.329 -  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   1.330 +fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
   1.331 +                  finitizes calculus alpha_T tsp =
   1.332 +  case infer "Finiteness" true hol_ctxt binarize calculus alpha_T tsp of
   1.333      SOME (asgs, msp, constr_mtypes) =>
   1.334      if forall (curry (op =) Gen o snd) asgs then
   1.335        tsp