src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35384 88dbcfe75c45
parent 35280 54ab4921f826
child 35385 29f81babefd7
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 10:08:44 2010 +0100
     1.3 @@ -2,16 +2,15 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Copyright   2009, 2010
     1.6  
     1.7 -Monotonicity predicate for higher-order logic.
     1.8 +Monotonicity inference for higher-order logic.
     1.9  *)
    1.10  
    1.11  signature NITPICK_MONO =
    1.12  sig
    1.13 -  datatype sign = Plus | Minus
    1.14    type hol_context = Nitpick_HOL.hol_context
    1.15  
    1.16    val formulas_monotonic :
    1.17 -    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
    1.18 +    hol_context -> bool -> typ -> term list * term list * term -> bool
    1.19  end;
    1.20  
    1.21  structure Nitpick_Mono : NITPICK_MONO =
    1.22 @@ -270,8 +269,13 @@
    1.23    if could_exist_alpha_sub_ctype thy alpha_T T then
    1.24      case AList.lookup (op =) (!constr_cache) x of
    1.25        SOME C => C
    1.26 -    | NONE => (fresh_ctype_for_type cdata (body_type T);
    1.27 -               AList.lookup (op =) (!constr_cache) x |> the)
    1.28 +    | NONE => if T = alpha_T then
    1.29 +                let val C = fresh_ctype_for_type cdata T in
    1.30 +                  (Unsynchronized.change constr_cache (cons (x, C)); C)
    1.31 +                end
    1.32 +              else
    1.33 +                (fresh_ctype_for_type cdata (body_type T);
    1.34 +                 AList.lookup (op =) (!constr_cache) x |> the)
    1.35    else
    1.36      fresh_ctype_for_type cdata T
    1.37  fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
    1.38 @@ -435,12 +439,13 @@
    1.39  val add_ctype_is_right_unique = add_notin_ctype_fv Minus
    1.40  val add_ctype_is_right_total = add_notin_ctype_fv Plus
    1.41  
    1.42 +val bool_from_minus = true
    1.43 +
    1.44  (* sign -> bool *)
    1.45 -fun bool_from_sign Plus = false
    1.46 -  | bool_from_sign Minus = true
    1.47 +fun bool_from_sign Plus = not bool_from_minus
    1.48 +  | bool_from_sign Minus = bool_from_minus
    1.49  (* bool -> sign *)
    1.50 -fun sign_from_bool false = Plus
    1.51 -  | sign_from_bool true = Minus
    1.52 +fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
    1.53  
    1.54  (* literal -> PropLogic.prop_formula *)
    1.55  fun prop_for_literal (x, sn) =
    1.56 @@ -492,7 +497,7 @@
    1.57               "-: " ^ commas (map (string_for_var o fst) neg))
    1.58    end
    1.59  
    1.60 -(* var -> constraint_set -> literal list list option *)
    1.61 +(* var -> constraint_set -> literal list option *)
    1.62  fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
    1.63    | solve max_var (CSet (lits, comps, sexps)) =
    1.64      let
    1.65 @@ -812,8 +817,8 @@
    1.66                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
    1.67                val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
    1.68              in
    1.69 -              (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
    1.70 -                                                |>> pop_bound
    1.71 +              (gamma |> push_bound abs_C, cset)
    1.72 +              |> do_co_formula body_t |>> pop_bound
    1.73              end
    1.74            (* typ -> term -> accumulator *)
    1.75            fun do_bounded_quantifier abs_T body_t =
    1.76 @@ -932,19 +937,20 @@
    1.77    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
    1.78    |> cat_lines |> print_g
    1.79  
    1.80 -(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
    1.81 -   -> bool *)
    1.82 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
    1.83 -                       nondef_ts core_t =
    1.84 +(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
    1.85 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
    1.86 +                       (def_ts, nondef_ts, core_t) =
    1.87    let
    1.88 -    val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
    1.89 +    val _ = print_g ("****** Monotonicity analysis: " ^
    1.90 +                     string_for_ctype CAlpha ^ " is " ^
    1.91                       Syntax.string_of_typ ctxt alpha_T)
    1.92 -    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
    1.93 -    val (gamma, cset) =
    1.94 +    val cdata as {max_fresh, constr_cache, ...} =
    1.95 +      initial_cdata hol_ctxt binarize alpha_T
    1.96 +    val (gamma as {frees, consts, ...}, cset) =
    1.97        (initial_gamma, slack)
    1.98        |> fold (consider_definitional_axiom cdata) def_ts
    1.99        |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
   1.100 -      |> consider_general_formula cdata sn core_t
   1.101 +      |> consider_general_formula cdata Plus core_t
   1.102    in
   1.103      case solve (!max_fresh) cset of
   1.104        SOME lits => (print_ctype_context ctxt lits gamma; true)