removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 4100111715564e2ad
parent 41000 4bbff1684465
child 41002 11a442b472c7
removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
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:33:05 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:33:09 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 3 T (nondef_ts, def_ts)
     1.8 +      formulas_monotonic hol_ctxt binarize 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:33:05 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 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 -> int -> typ -> term list * term list -> bool
     2.8 +    hol_context -> bool -> typ -> term list * term list -> bool
     2.9    val finitize_funs :
    2.10 -    hol_context -> bool -> (typ option * bool option) list -> int -> typ
    2.11 +    hol_context -> bool -> (typ option * bool option) list -> typ
    2.12      -> term list * term list -> term list * term list
    2.13  end;
    2.14  
    2.15 @@ -538,16 +538,6 @@
    2.16      PL.SOr (prop_for_exists_var_assign_literal xs Gen,
    2.17              prop_for_comp (aa1, aa2, cmp, []))
    2.18  
    2.19 -(* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
    2.20 -   the M1, M2, and M3 calculi from Blanchette & Krauss 2011. *)
    2.21 -fun variable_domain calculus =
    2.22 -  [Gen] @ (if calculus > 1 then [Fls] else [])
    2.23 -  @ (if calculus > 2 then [New, Tru] else [])
    2.24 -
    2.25 -fun prop_for_variable_domain calculus x =
    2.26 -  PL.exists (map (fn a => prop_for_assign_literal (x, (Plus, a)))
    2.27 -                 (variable_domain calculus))
    2.28 -
    2.29  fun extract_assigns max_var assigns asgs =
    2.30    fold (fn x => fn accum =>
    2.31             if AList.defined (op =) asgs x then
    2.32 @@ -558,11 +548,10 @@
    2.33                     :: accum)
    2.34         (max_var downto 1) asgs
    2.35  
    2.36 -fun print_problem calculus comps clauses =
    2.37 -  trace_msg (fn () =>
    2.38 -                "*** Problem (calculus M" ^ string_of_int calculus ^ "):\n" ^
    2.39 -                cat_lines (map string_for_comp comps @
    2.40 -                           map (string_for_assign_clause o SOME) clauses))
    2.41 +fun print_problem comps clauses =
    2.42 +  trace_msg (fn () => "*** Problem:\n" ^
    2.43 +                      cat_lines (map string_for_comp comps @
    2.44 +                                 map (string_for_assign_clause o SOME) clauses))
    2.45  
    2.46  fun print_solution asgs =
    2.47    trace_msg (fn () => "*** Solution:\n" ^
    2.48 @@ -573,20 +562,14 @@
    2.49                               string_for_vars ", " xs)
    2.50         |> space_implode "\n"))
    2.51  
    2.52 -fun solve calculus max_var (comps, clauses) =
    2.53 +fun solve max_var (comps, clauses) =
    2.54    let
    2.55      val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
    2.56      fun do_assigns assigns =
    2.57        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
    2.58 -    val _ = print_problem calculus comps clauses
    2.59 +    val _ = print_problem comps clauses
    2.60      val prop =
    2.61 -      map prop_for_comp comps @
    2.62 -      map prop_for_assign_clause clauses @
    2.63 -      (if calculus < 3 then
    2.64 -         map (prop_for_variable_domain calculus) (1 upto max_var)
    2.65 -       else
    2.66 -         [])
    2.67 -      |> PL.all
    2.68 +      PL.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
    2.69    in
    2.70      if PL.eval (K false) prop then
    2.71        do_assigns (K (SOME false))
    2.72 @@ -809,26 +792,6 @@
    2.73          M as MPair (a_M, b_M) =>
    2.74          pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
    2.75        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
    2.76 -    fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
    2.77 -      let
    2.78 -        val abs_M = mtype_for abs_T
    2.79 -        val aa = V (Unsynchronized.inc max_fresh)
    2.80 -        val (bound_m, accum) =
    2.81 -          accum |>> push_bound aa abs_T abs_M |> do_term bound_t
    2.82 -        val expected_bound_M = plus_set_mtype_for_dom abs_M
    2.83 -        val (body_m, accum) =
    2.84 -          accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
    2.85 -                |> do_term body_t ||> apfst pop_bound
    2.86 -        val bound_M = mtype_of_mterm bound_m
    2.87 -        val (M1, aa', _) = dest_MFun bound_M
    2.88 -      in
    2.89 -        (MApp (MRaw (t0, MFun (bound_M, aa, bool_M)),
    2.90 -               MAbs (abs_s, abs_T, M1, aa',
    2.91 -                     MApp (MApp (MRaw (connective_t,
    2.92 -                                       mtype_for (fastype_of connective_t)),
    2.93 -                                 MApp (bound_m, MRaw (Bound 0, M1))),
    2.94 -                           body_m))), accum)
    2.95 -      end
    2.96      and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
    2.97        let
    2.98          val frame1 = fresh_frame mdata (SOME Tru) NONE frame
    2.99 @@ -997,12 +960,6 @@
   2.100                          val (m', accum) =
   2.101                            do_term t' (accum |>> push_bound aa T M)
   2.102                        in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   2.103 -         | (t0 as Const (@{const_name All}, _))
   2.104 -           $ Abs (s', T', (t10 as @{const implies}) $ (t11 $ Bound 0) $ t12) =>
   2.105 -           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   2.106 -         | (t0 as Const (@{const_name Ex}, _))
   2.107 -           $ Abs (s', T', (t10 as @{const conj}) $ (t11 $ Bound 0) $ t12) =>
   2.108 -           do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   2.109           | @{const Not} $ t1 =>
   2.110             do_connect "\<implies>" imp_clauses @{const implies} t1
   2.111                        @{const False} accum
   2.112 @@ -1043,11 +1000,10 @@
   2.113                                         string_for_mterm ctxt m))
   2.114    in do_term end
   2.115  
   2.116 -fun force_minus_funs 0 _ = I
   2.117 -  | force_minus_funs n (M as MFun (M1, _, M2)) =
   2.118 -    add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_minus_funs (n - 1) M2
   2.119 -  | force_minus_funs _ M =
   2.120 -    raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
   2.121 +fun force_gen_funs 0 _ = I
   2.122 +  | force_gen_funs n (M as MFun (M1, _, M2)) =
   2.123 +    add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
   2.124 +  | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
   2.125  fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   2.126    let
   2.127      val (m1, accum) = consider_term mdata t1 accum
   2.128 @@ -1057,11 +1013,11 @@
   2.129      val accum = accum ||> add_mtypes_equal M1 M2
   2.130      val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   2.131      val m = MApp (MApp (MRaw (Const x,
   2.132 -                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
   2.133 +                           MFun (M1, A Gen, MFun (M2, A Fls, body_M))), m1), m2)
   2.134    in
   2.135      (m, if def then
   2.136            let val (head_m, arg_ms) = strip_mcomb m1 in
   2.137 -            accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
   2.138 +            accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
   2.139            end
   2.140          else
   2.141            accum)
   2.142 @@ -1079,9 +1035,10 @@
   2.143              val abs_M = mtype_for abs_T
   2.144              val x = Unsynchronized.inc max_fresh
   2.145              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   2.146 +            fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
   2.147              val (body_m, accum) =
   2.148                accum ||> side_cond
   2.149 -                        ? add_mtype_is_complete [(x, (Minus, Fls))] abs_M
   2.150 +                        ? add_mtype_is_complete [(x, (Minus, ann ()))] abs_M
   2.151                      |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
   2.152              val body_M = mtype_of_mterm body_m
   2.153            in
   2.154 @@ -1114,8 +1071,7 @@
   2.155             end
   2.156           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   2.157             do_quantifier x s1 T1 t1
   2.158 -         | Const (x0 as (@{const_name Ex}, T0))
   2.159 -           $ (t1 as Abs (s1, T1, t1')) =>
   2.160 +         | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
   2.161             (case sn of
   2.162                Plus => do_quantifier x0 s1 T1 t1'
   2.163              | Minus =>
   2.164 @@ -1240,7 +1196,7 @@
   2.165  fun amass f t (ms, accum) =
   2.166    let val (m, accum) = f t accum in (m :: ms, accum) end
   2.167  
   2.168 -fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize calculus alpha_T
   2.169 +fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   2.170            (nondef_ts, def_ts) =
   2.171    let
   2.172      val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   2.173 @@ -1256,7 +1212,7 @@
   2.174      val (def_ms, (gamma, cset)) =
   2.175        ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   2.176    in
   2.177 -    case solve calculus (!max_fresh) cset of
   2.178 +    case solve (!max_fresh) cset of
   2.179        SOME asgs => (print_mcontext ctxt asgs gamma;
   2.180                      SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   2.181      | _ => NONE
   2.182 @@ -1268,15 +1224,14 @@
   2.183         | MTERM (loc, ms) =>
   2.184           raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
   2.185  
   2.186 -fun formulas_monotonic hol_ctxt =
   2.187 -  is_some oooo infer "Monotonicity" false hol_ctxt
   2.188 +val formulas_monotonic = is_some oooo infer "Monotonicity" false
   2.189  
   2.190  fun fin_fun_constr T1 T2 =
   2.191    (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
   2.192  
   2.193  fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
   2.194 -                  finitizes calculus alpha_T tsp =
   2.195 -  case infer "Finiteness" true hol_ctxt binarize calculus alpha_T tsp of
   2.196 +                  finitizes alpha_T tsp =
   2.197 +  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
   2.198      SOME (asgs, msp, constr_mtypes) =>
   2.199      if forall (curry (op =) Gen o snd) asgs then
   2.200        tsp
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:33:05 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:33:09 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 3) Ts (nondef_ts, def_ts)
     3.8 +      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
     3.9      end
    3.10  
    3.11  (** Preprocessor entry point **)