# HG changeset patch # User blanchet # Date 1291638785 -3600 # Node ID 4bbff1684465afca01548c1c00a8982af3573f86 # Parent 69d0d445c46af5ecd2bb63b6a302aae266659216 implemented All rules from new monotonicity calculus diff -r 69d0d445c46a -r 4bbff1684465 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:30:57 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:05 2010 +0100 @@ -457,37 +457,37 @@ | do_notin_mtype_fv Plus [] MAlpha _ = NONE | do_notin_mtype_fv Plus [asg] MAlpha (SOME clauses) = clauses |> add_assign_literal asg - | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) = - SOME (insert (op =) clause clauses) - | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset = - cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus clause M1 + | do_notin_mtype_fv Plus unless MAlpha (SOME clauses) = + SOME (insert (op =) unless clauses) + | do_notin_mtype_fv sn unless (MFun (M1, A a, M2)) cset = + cset |> (if a <> Gen andalso sn = Plus then do_notin_mtype_fv Plus unless M1 else I) - |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus clause M1 + |> (if a = Gen orelse sn = Plus then do_notin_mtype_fv Minus unless M1 else I) - |> do_notin_mtype_fv sn clause M2 - | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset = - cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME clause) of + |> do_notin_mtype_fv sn unless M2 + | do_notin_mtype_fv Plus unless (MFun (M1, V x, M2)) cset = + cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME unless) of NONE => I - | SOME clause' => do_notin_mtype_fv Plus clause' M1) - |> 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)) cset = + | SOME unless' => do_notin_mtype_fv Plus unless' M1) + |> do_notin_mtype_fv Minus unless M1 + |> do_notin_mtype_fv Plus unless M2 + | do_notin_mtype_fv Minus unless (MFun (M1, V x, M2)) cset = cset |> (case fold (fn a => add_assign_disjunct (x, (Plus, a))) [Fls, Tru] - (SOME clause) of + (SOME unless) of NONE => I - | SOME clause' => do_notin_mtype_fv Plus clause' M1) - |> do_notin_mtype_fv Minus clause M2 - | do_notin_mtype_fv sn clause (MPair (M1, M2)) cset = - cset |> fold (do_notin_mtype_fv sn clause) [M1, M2] - | do_notin_mtype_fv sn clause (MType (_, Ms)) cset = - cset |> fold (do_notin_mtype_fv sn clause) Ms + | SOME unless' => do_notin_mtype_fv Plus unless' M1) + |> do_notin_mtype_fv Minus unless M2 + | do_notin_mtype_fv sn unless (MPair (M1, M2)) cset = + cset |> fold (do_notin_mtype_fv sn unless) [M1, M2] + | do_notin_mtype_fv sn unless (MType (_, Ms)) cset = + cset |> fold (do_notin_mtype_fv sn unless) Ms | do_notin_mtype_fv _ _ M _ = raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], []) -fun add_notin_mtype_fv sn M (comps, clauses) = +fun add_notin_mtype_fv sn unless M (comps, clauses) = (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^ (case sn of Minus => "concrete" | Plus => "complete")); - case SOME clauses |> do_notin_mtype_fv sn [] M of + case SOME clauses |> do_notin_mtype_fv sn unless M of NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) | SOME clauses => (comps, clauses)) @@ -695,8 +695,8 @@ | V x => add_annotation_clause_from_quasi_clause rest accum |> Option.map (cons (x, (sign_for_comp_op cmp, a))) -fun assign_clause_from_quasi_clause clause = - add_annotation_clause_from_quasi_clause clause (SOME []) +fun assign_clause_from_quasi_clause unless = + add_annotation_clause_from_quasi_clause unless (SOME []) fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 = (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^ @@ -767,7 +767,7 @@ val body_M = mtype_for (body_type T) in (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M), - (gamma, cset |> add_mtype_is_complete abs_M)) + (gamma, cset |> add_mtype_is_complete [] abs_M)) end fun do_equals T (gamma, cset) = let @@ -775,7 +775,7 @@ val aa = V (Unsynchronized.inc max_fresh) in (MFun (M, A Gen, MFun (M, aa, mtype_for (nth_range_type 2 T))), - (gamma, cset |> add_mtype_is_concrete M + (gamma, cset |> add_mtype_is_concrete [] M |> add_annotation_atom_comp Leq [] (A Fls) aa)) end fun do_robust_set_operation T (gamma, cset) = @@ -797,7 +797,7 @@ else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2) | custom_mtype_for T = mtype_for T in - (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M)) + (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete [] set_M)) end fun do_pair_constr T accum = case mtype_for (nth_range_type 2 T) of @@ -1067,89 +1067,89 @@ accum) end -fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = +fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh, + ...}) = let val mtype_for = fresh_mtype_for_type mdata false val do_term = consider_term mdata fun do_formula sn t (accum as (gamma, _)) = - let - 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 (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, - MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)), - MAbs (abs_s, abs_T, abs_M, A Gen, body_m)), - accum |>> pop_bound) - end - fun do_equals x t1 t2 = - case sn of - Plus => do_term t accum - | Minus => consider_general_equals mdata false x t1 t2 accum - in - (trace_msg (fn () => " " ^ string_for_mcontext ctxt t gamma ^ - " \ " ^ Syntax.string_of_term ctxt t ^ - " : o\<^sup>" ^ string_for_sign sn ^ "?"); - case t of - Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) => - do_quantifier x s1 T1 t1 - | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2 - | @{const Trueprop} $ t1 => - let val (m1, accum) = do_formula sn t1 accum in - (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), - m1), accum) - end - | @{const Not} $ t1 => - let val (m1, accum) = do_formula (negate_sign sn) t1 accum in - (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1), + let + fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t = + let + val abs_M = mtype_for abs_T + val x = Unsynchronized.inc max_fresh + val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) + val (body_m, accum) = + accum ||> side_cond + ? add_mtype_is_complete [(x, (Minus, Fls))] abs_M + |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t + val body_M = mtype_of_mterm body_m + in + (MApp (MRaw (Const quant_x, + MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)), + MAbs (abs_s, abs_T, abs_M, A Gen, body_m)), + accum |>> pop_bound) + end + fun do_equals x t1 t2 = + case sn of + Plus => do_term t accum + | Minus => consider_general_equals mdata false x t1 t2 accum + in + (trace_msg (fn () => " " ^ string_for_mcontext ctxt t gamma ^ + " \ " ^ Syntax.string_of_term ctxt t ^ + " : o\<^sup>" ^ string_for_sign sn ^ "?"); + case t of + Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) => + do_quantifier x s1 T1 t1 + | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2 + | @{const Trueprop} $ t1 => + let val (m1, accum) = do_formula sn t1 accum in + (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), + m1), accum) + end + | @{const Not} $ t1 => + let val (m1, accum) = do_formula (negate_sign sn) t1 accum in + (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1), + accum) + end + | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) => + do_quantifier x s1 T1 t1 + | Const (x0 as (@{const_name Ex}, T0)) + $ (t1 as Abs (s1, T1, t1')) => + (case sn of + Plus => do_quantifier x0 s1 T1 t1' + | Minus => + (* FIXME: Move elsewhere *) + do_term (@{const Not} + $ (HOLogic.eq_const (domain_type T0) $ t1 + $ Abs (Name.uu, T1, @{const False}))) accum) + | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => + do_equals x t1 t2 + | Const (@{const_name Let}, _) $ t1 $ t2 => + do_formula sn (betapply (t2, t1)) accum + | (t0 as Const (s0, _)) $ t1 $ t2 => + if s0 = @{const_name "==>"} orelse + s0 = @{const_name Pure.conjunction} orelse + s0 = @{const_name conj} orelse s0 = @{const_name disj} orelse + s0 = @{const_name implies} then + let + val impl = (s0 = @{const_name "==>"} orelse + s0 = @{const_name implies}) + val (m1, accum) = do_formula (sn |> impl ? negate_sign) t1 accum + val (m2, accum) = do_formula sn t2 accum + in + (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) end - | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) => - do_quantifier x s1 T1 t1 - | Const (x0 as (@{const_name Ex}, T0)) - $ (t1 as Abs (s1, T1, t1')) => - (case sn of - Plus => do_quantifier x0 s1 T1 t1' - | Minus => - (* FIXME: Move elsewhere *) - do_term (@{const Not} - $ (HOLogic.eq_const (domain_type T0) $ t1 - $ Abs (Name.uu, T1, @{const False}))) accum) - | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => - do_equals x t1 t2 - | Const (@{const_name Let}, _) $ t1 $ t2 => - do_formula sn (betapply (t2, t1)) accum - | (t0 as Const (s0, _)) $ t1 $ t2 => - if s0 = @{const_name "==>"} orelse - s0 = @{const_name Pure.conjunction} orelse - s0 = @{const_name conj} orelse - s0 = @{const_name disj} orelse - s0 = @{const_name implies} then - let - val impl = (s0 = @{const_name "==>"} orelse - s0 = @{const_name implies}) - val (m1, accum) = - do_formula (sn |> impl ? negate_sign) t1 accum - val (m2, accum) = do_formula sn t2 accum - in - (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), - accum) - end - else - do_term t accum - | _ => do_term t accum) - end - |> tap (fn (m, (gamma, _)) => - trace_msg (fn () => string_for_mcontext ctxt t gamma ^ - " \ " ^ - string_for_mterm ctxt m ^ " : o\<^sup>" ^ - string_for_sign sn)) + else + do_term t accum + | _ => do_term t accum) + end + |> tap (fn (m, (gamma, _)) => + trace_msg (fn () => string_for_mcontext ctxt t gamma ^ + " \ " ^ + string_for_mterm ctxt m ^ " : o\<^sup>" ^ + string_for_sign sn)) in do_formula end (* The harmless axiom optimization below is somewhat too aggressive in the face