author blanchet Mon, 06 Dec 2010 13:18:25 +0100 changeset 40993 52ee2a187cdb parent 40992 8cacefe9851c child 40994 3bdb8df0daf0
support 3 monotonicity calculi in one and fix soundness bug
```--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 06 13:18:25 2010 +0100
@@ -347,7 +347,7 @@
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
is_number_type ctxt T orelse is_bit_type T
fun is_type_actually_monotonic T =
-      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
+      formulas_monotonic hol_ctxt binarize 3 T (nondef_ts, def_ts)
fun is_type_kind_of_monotonic T =
case triple_lookup (type_match thy) monos T of
SOME (SOME false) => false```
```--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
@@ -11,9 +11,9 @@

val trace : bool Unsynchronized.ref
val formulas_monotonic :
-    hol_context -> bool -> typ -> term list * term list -> bool
+    hol_context -> bool -> int -> typ -> term list * term list -> bool
val finitize_funs :
-    hol_context -> bool -> (typ option * bool option) list -> typ
+    hol_context -> bool -> (typ option * bool option) list -> int -> typ
-> term list * term list -> term list * term list
end;

@@ -373,32 +373,41 @@
fun add_assign_disjunct _ NONE = NONE
| add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)

-fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
+fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
(case (aa1, aa2) of
(A a1, A a2) => if a1 = a2 then SOME accum else NONE
| (V x1, A a2) =>
SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
| (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
-     | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum)
-  | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
+     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
+  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
(case (aa1, aa2) of
(_, A Gen) => SOME accum
| (A Gen, A _) => NONE
| (A a1, A a2) => if a1 = a2 then SOME accum else NONE
| _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
-  | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
+  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)

+fun add_annotation_atom_comp cmp xs aa1 aa2
+                             ((asgs, comps, clauses) : constraint_set) =
+  (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom aa1 ^ " " ^
+                       string_for_comp_op cmp ^ " " ^
+                       string_for_annotation_atom aa2);
+   case do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) of
+     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
+   | SOME (asgs, comps) => (asgs, comps, clauses))
+
fun do_mtype_comp _ _ _ _ NONE = NONE
| do_mtype_comp _ _ MAlpha MAlpha accum = accum
| do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
(SOME accum) =
-     accum |> add_annotation_atom_comp Eq xs aa1 aa2
+     accum |> do_annotation_atom_comp Eq xs aa1 aa2
|> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
| do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
(SOME accum) =
(if exists_alpha_sub_mtype M11 then
-       accum |> add_annotation_atom_comp Leq xs aa1 aa2
+       accum |> do_annotation_atom_comp Leq xs aa1 aa2
|> do_mtype_comp Leq xs M21 M11
|> (case aa2 of
A Gen => I
@@ -435,12 +444,12 @@
SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
| do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
SOME (asgs, insert (op =) clause clauses)
-  | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum =
-    accum |> (if aa <> Gen andalso sn = Plus then
+  | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) accum =
+    accum |> (if a <> Gen andalso sn = Plus then
do_notin_mtype_fv Plus clause M1
else
I)
-          |> (if aa = Gen orelse sn = Plus then
+          |> (if a = Gen orelse sn = Plus then
do_notin_mtype_fv Minus clause M1
else
I)
@@ -452,7 +461,7 @@
|> do_notin_mtype_fv Minus clause M1
|> do_notin_mtype_fv Plus clause M2
| do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
-    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru]
+    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
(SOME clause) of
NONE => I
| SOME clause' => do_notin_mtype_fv Plus clause' M1)
@@ -474,15 +483,15 @@
val add_mtype_is_concrete = add_notin_mtype_fv Minus
val add_mtype_is_complete = add_notin_mtype_fv Plus

-fun fst_var n = 2 * n
-fun snd_var n = 2 * n + 1
-
val bool_table =
[(Gen, (false, false)),
(New, (false, true)),
(Fls, (true, false)),
(Tru, (true, true))]

+fun fst_var n = 2 * n
+fun snd_var n = 2 * n + 1
+
val bools_from_annotation = AList.lookup (op =) bool_table #> the
val annotation_from_bools = AList.find (op =) bool_table #> the_single

@@ -514,10 +523,14 @@
PL.SOr (prop_for_exists_var_assign xs Gen,
prop_for_comp (aa1, aa2, cmp, []))

-fun fix_bool_options (NONE, NONE) = (false, false)
-  | fix_bool_options (NONE, SOME b) = (b, b)
-  | fix_bool_options (SOME b, NONE) = (b, b)
-  | fix_bool_options (SOME b1, SOME b2) = (b1, b2)
+(* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
+   the M1, M2, and M3 calculi from Blanchette & Krauss 2011. *)
+fun variable_domain calculus =
+  [Gen] @ (if calculus > 1 then [Fls] else [])
+  @ (if calculus > 2 then [New, Tru] else [])
+
+fun prop_for_variable_domain calculus x =
+  PL.exists (map (curry prop_for_assign x) (variable_domain calculus))

fun extract_assigns max_var assigns asgs =
fold (fn x => fn accum =>
@@ -525,7 +538,8 @@
accum
else case (fst_var x, snd_var x) |> pairself assigns of
(NONE, NONE) => accum
-           | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
+           | bp => (x, annotation_from_bools (pairself (the_default false) bp))
+                   :: accum)
(max_var downto 1) asgs

fun print_problem asgs comps clauses =
@@ -543,14 +557,20 @@
string_for_vars ", " xs)
|> space_implode "\n"))

-fun solve max_var (asgs, comps, clauses) =
+fun solve calculus max_var (asgs, comps, clauses) =
let
fun do_assigns assigns =
SOME (extract_assigns max_var assigns asgs |> tap print_solution)
val _ = print_problem asgs comps clauses
-    val prop = PL.all (map prop_for_assign asgs @
-                       map prop_for_comp comps @
-                       map prop_for_assign_clause clauses)
+    val prop =
+      map prop_for_assign asgs @
+      map prop_for_comp comps @
+      map prop_for_assign_clause clauses @
+      (if calculus < 3 then
+         map (prop_for_variable_domain calculus) (1 upto max_var)
+       else
+         [])
+      |> PL.all
in
if PL.eval (K false) prop then
do_assigns (K (SOME false))
@@ -581,11 +601,14 @@
val initial_gamma =
{bound_Ts = [], bound_Ms = [], bound_frame = [], frees = [], consts = []}

-fun push_bound T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
+fun push_bound aa T M {bound_Ts, bound_Ms, bound_frame, frees, consts} =
{bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms,
-   bound_frame = bound_frame, frees = frees, consts = consts}
+   bound_frame = (length bound_Ts, aa) :: bound_frame, frees = frees,
+   consts = consts}
fun pop_bound {bound_Ts, bound_Ms, bound_frame, frees, consts} =
-  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, bound_frame = bound_frame,
+  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms,
+   bound_frame = bound_frame
+                 |> filter_out (fn (depth, _) => depth = length bound_Ts - 1),
frees = frees, consts = consts}
handle List.Empty => initial_gamma (* FIXME: needed? *)

@@ -648,17 +671,18 @@
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
let
val abs_M = mtype_for abs_T
+        val aa = V (Unsynchronized.inc max_fresh)
val (bound_m, accum) =
-          accum |>> push_bound abs_T abs_M |> do_term bound_t
+          accum |>> push_bound aa abs_T abs_M |> do_term bound_t
val expected_bound_M = plus_set_mtype_for_dom abs_M
val (body_m, accum) =
accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
|> do_term body_t ||> apfst pop_bound
val bound_M = mtype_of_mterm bound_m
-        val (M1, aa, _) = dest_MFun bound_M
+        val (M1, aa', _) = dest_MFun bound_M
in
-        (MApp (MRaw (t0, MFun (bound_M, A Gen, bool_M)),
-               MAbs (abs_s, abs_T, M1, aa,
+        (MApp (MRaw (t0, MFun (bound_M, aa, bool_M)),
+               MAbs (abs_s, abs_T, M1, aa',
MApp (MApp (MRaw (connective_t,
mtype_for (fastype_of connective_t)),
MApp (bound_m, MRaw (Bound 0, M1))),
@@ -666,13 +690,21 @@
end
and do_term t (accum as ({bound_Ts, bound_Ms, bound_frame, frees, consts},
cset)) =
-        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
-                             Syntax.string_of_term ctxt t ^ " : _?");
-         case t of
-           Const (x as (s, T)) =>
-           (case AList.lookup (op =) consts x of
-              SOME M => (M, accum)
-            | NONE =>
+      (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
+                           Syntax.string_of_term ctxt t ^ " : _?");
+       case t of
+         Const (x as (s, T)) =>
+         (case AList.lookup (op =) consts x of
+            SOME M => (M, accum)
+          | NONE =>
+            case s of
+              @{const_name False} =>
+              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Fls))
+                                      (map snd bound_frame))
+            | @{const_name True} =>
+              (bool_M, accum ||> fold (add_annotation_atom_comp Leq [] (A Tru))
+                                      (map snd bound_frame))
+            | _ =>
if not (could_exist_alpha_subtype alpha_T T) then
(mtype_for T, accum)
else case s of
@@ -742,8 +774,8 @@
MFun (mtype_for (domain_type T), V x, bool_M)
val a_set_T = domain_type T
val a_M = mtype_for (domain_type a_set_T)
-                  val b_set_M = mtype_for_set (range_type (domain_type
-                                                               (range_type T)))
+                  val b_set_M =
+                    mtype_for_set (range_type (domain_type (range_type T)))
val a_set_M = mtype_for_set a_set_T
val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
val ab_set_M = mtype_for_set (nth_range_type 2 T)
@@ -788,9 +820,8 @@
SOME t' =>
let
val M = mtype_for T
-                val aa = V (Unsynchronized.inc max_fresh)
-                val (m', accum) = do_term t' (accum |>> push_bound T M)
-              in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end
+                val (m', accum) = do_term t' (accum |>> push_bound (A Fls) T M)
+              in (MAbs (s, T, M, A Fls, m'), accum |>> pop_bound) end
| NONE =>
((case t' of
t1' \$ Bound 0 =>
@@ -808,13 +839,17 @@
handle SAME () =>
let
val M = mtype_for T
-                        val (m', accum) = do_term t' (accum |>> push_bound T M)
-                      in (MAbs (s, T, M, A Gen, m'), accum |>> pop_bound) end))
+                        val aa = V (Unsynchronized.inc max_fresh)
+                        val (m', accum) =
+                          do_term t' (accum |>> push_bound aa T M)
+                      in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
| (t0 as Const (@{const_name All}, _))
-           \$ Abs (s', T', (t10 as @{const HOL.implies}) \$ (t11 \$ Bound 0) \$ t12) =>
+           \$ Abs (s', T', (t10 as @{const HOL.implies})
+                          \$ (t11 \$ Bound 0) \$ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| (t0 as Const (@{const_name Ex}, _))
-           \$ Abs (s', T', (t10 as @{const HOL.conj}) \$ (t11 \$ Bound 0) \$ t12) =>
+           \$ Abs (s', T', (t10 as @{const HOL.conj})
+                          \$ (t11 \$ Bound 0) \$ t12) =>
do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| Const (@{const_name Let}, _) \$ t1 \$ t2 =>
do_term (betapply (t2, t1)) accum
@@ -865,10 +900,11 @@
fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
let
val abs_M = mtype_for abs_T
+              val a = Gen (* FIXME: strengthen *)
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
val (body_m, accum) =
accum ||> side_cond ? add_mtype_is_complete abs_M
-                      |>> push_bound abs_T abs_M |> do_formula sn body_t
+                      |>> push_bound (A a) abs_T abs_M |> do_formula sn body_t
val body_M = mtype_of_mterm body_m
in
(MApp (MRaw (Const quant_x,
@@ -969,7 +1005,7 @@
let
val abs_M = mtype_for abs_T
val (body_m, accum) =
-            accum |>> push_bound abs_T abs_M |> do_formula body_t
+            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
val body_M = mtype_of_mterm body_m
in
(MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
@@ -1027,7 +1063,7 @@
fun amass f t (ms, accum) =
let val (m, accum) = f t accum in (m :: ms, accum) end

-fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
+fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize calculus alpha_T
(nondef_ts, def_ts) =
let
val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
@@ -1043,7 +1079,7 @@
val (def_ms, (gamma, cset)) =
([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
in
-    case solve (!max_fresh) cset of
+    case solve calculus (!max_fresh) cset of
SOME asgs => (print_mtype_context ctxt asgs gamma;
SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
| _ => NONE
@@ -1055,14 +1091,15 @@
| MTERM (loc, ms) =>
raise BAD (loc, commas (map (string_for_mterm ctxt) ms))

-val formulas_monotonic = is_some oooo infer "Monotonicity" false
+fun formulas_monotonic hol_ctxt =
+  is_some oooo infer "Monotonicity" false hol_ctxt

fun fin_fun_constr T1 T2 =
(@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))

-fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...})
-                  binarize finitizes alpha_T tsp =
-  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
+fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
+                  finitizes calculus alpha_T tsp =
+  case infer "Finiteness" true hol_ctxt binarize calculus alpha_T tsp of
SOME (asgs, msp, constr_mtypes) =>
if forall (curry (op =) Gen o snd) asgs then
tsp```
```--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Dec 06 13:18:25 2010 +0100
@@ -1261,7 +1261,7 @@
triple_lookup (type_match thy) monos T
= SOME (SOME false))
in
-      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
+      fold (finitize_funs hol_ctxt binarize finitizes 3) Ts (nondef_ts, def_ts)
end

(** Preprocessor entry point **)```