src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41001 11715564e2ad
parent 41000 4bbff1684465
child 41002 11a442b472c7
equal deleted inserted replaced
41000:4bbff1684465 41001:11715564e2ad
     9 sig
     9 sig
    10   type hol_context = Nitpick_HOL.hol_context
    10   type hol_context = Nitpick_HOL.hol_context
    11 
    11 
    12   val trace : bool Unsynchronized.ref
    12   val trace : bool Unsynchronized.ref
    13   val formulas_monotonic :
    13   val formulas_monotonic :
    14     hol_context -> bool -> int -> typ -> term list * term list -> bool
    14     hol_context -> bool -> typ -> term list * term list -> bool
    15   val finitize_funs :
    15   val finitize_funs :
    16     hol_context -> bool -> (typ option * bool option) list -> int -> typ
    16     hol_context -> bool -> (typ option * bool option) list -> typ
    17     -> term list * term list -> term list * term list
    17     -> term list * term list -> term list * term list
    18 end;
    18 end;
    19 
    19 
    20 structure Nitpick_Mono : NITPICK_MONO =
    20 structure Nitpick_Mono : NITPICK_MONO =
    21 struct
    21 struct
   536     PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
   536     PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
   537   | prop_for_comp (aa1, aa2, cmp, xs) =
   537   | prop_for_comp (aa1, aa2, cmp, xs) =
   538     PL.SOr (prop_for_exists_var_assign_literal xs Gen,
   538     PL.SOr (prop_for_exists_var_assign_literal xs Gen,
   539             prop_for_comp (aa1, aa2, cmp, []))
   539             prop_for_comp (aa1, aa2, cmp, []))
   540 
   540 
   541 (* The "calculus" parameter may be 1, 2, or 3, corresponding approximately to
       
   542    the M1, M2, and M3 calculi from Blanchette & Krauss 2011. *)
       
   543 fun variable_domain calculus =
       
   544   [Gen] @ (if calculus > 1 then [Fls] else [])
       
   545   @ (if calculus > 2 then [New, Tru] else [])
       
   546 
       
   547 fun prop_for_variable_domain calculus x =
       
   548   PL.exists (map (fn a => prop_for_assign_literal (x, (Plus, a)))
       
   549                  (variable_domain calculus))
       
   550 
       
   551 fun extract_assigns max_var assigns asgs =
   541 fun extract_assigns max_var assigns asgs =
   552   fold (fn x => fn accum =>
   542   fold (fn x => fn accum =>
   553            if AList.defined (op =) asgs x then
   543            if AList.defined (op =) asgs x then
   554              accum
   544              accum
   555            else case (fst_var x, snd_var x) |> pairself assigns of
   545            else case (fst_var x, snd_var x) |> pairself assigns of
   556              (NONE, NONE) => accum
   546              (NONE, NONE) => accum
   557            | bp => (x, annotation_from_bools (pairself (the_default false) bp))
   547            | bp => (x, annotation_from_bools (pairself (the_default false) bp))
   558                    :: accum)
   548                    :: accum)
   559        (max_var downto 1) asgs
   549        (max_var downto 1) asgs
   560 
   550 
   561 fun print_problem calculus comps clauses =
   551 fun print_problem comps clauses =
   562   trace_msg (fn () =>
   552   trace_msg (fn () => "*** Problem:\n" ^
   563                 "*** Problem (calculus M" ^ string_of_int calculus ^ "):\n" ^
   553                       cat_lines (map string_for_comp comps @
   564                 cat_lines (map string_for_comp comps @
   554                                  map (string_for_assign_clause o SOME) clauses))
   565                            map (string_for_assign_clause o SOME) clauses))
       
   566 
   555 
   567 fun print_solution asgs =
   556 fun print_solution asgs =
   568   trace_msg (fn () => "*** Solution:\n" ^
   557   trace_msg (fn () => "*** Solution:\n" ^
   569       (asgs
   558       (asgs
   570        |> map swap
   559        |> map swap
   571        |> AList.group (op =)
   560        |> AList.group (op =)
   572        |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
   561        |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
   573                              string_for_vars ", " xs)
   562                              string_for_vars ", " xs)
   574        |> space_implode "\n"))
   563        |> space_implode "\n"))
   575 
   564 
   576 fun solve calculus max_var (comps, clauses) =
   565 fun solve max_var (comps, clauses) =
   577   let
   566   let
   578     val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
   567     val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
   579     fun do_assigns assigns =
   568     fun do_assigns assigns =
   580       SOME (extract_assigns max_var assigns asgs |> tap print_solution)
   569       SOME (extract_assigns max_var assigns asgs |> tap print_solution)
   581     val _ = print_problem calculus comps clauses
   570     val _ = print_problem comps clauses
   582     val prop =
   571     val prop =
   583       map prop_for_comp comps @
   572       PL.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
   584       map prop_for_assign_clause clauses @
       
   585       (if calculus < 3 then
       
   586          map (prop_for_variable_domain calculus) (1 upto max_var)
       
   587        else
       
   588          [])
       
   589       |> PL.all
       
   590   in
   573   in
   591     if PL.eval (K false) prop then
   574     if PL.eval (K false) prop then
   592       do_assigns (K (SOME false))
   575       do_assigns (K (SOME false))
   593     else if PL.eval (K true) prop then
   576     else if PL.eval (K true) prop then
   594       do_assigns (K (SOME true))
   577       do_assigns (K (SOME true))
   807     fun do_nth_pair_sel n T =
   790     fun do_nth_pair_sel n T =
   808       case mtype_for (domain_type T) of
   791       case mtype_for (domain_type T) of
   809         M as MPair (a_M, b_M) =>
   792         M as MPair (a_M, b_M) =>
   810         pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   793         pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   811       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   794       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   812     fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
       
   813       let
       
   814         val abs_M = mtype_for abs_T
       
   815         val aa = V (Unsynchronized.inc max_fresh)
       
   816         val (bound_m, accum) =
       
   817           accum |>> push_bound aa abs_T abs_M |> do_term bound_t
       
   818         val expected_bound_M = plus_set_mtype_for_dom abs_M
       
   819         val (body_m, accum) =
       
   820           accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
       
   821                 |> do_term body_t ||> apfst pop_bound
       
   822         val bound_M = mtype_of_mterm bound_m
       
   823         val (M1, aa', _) = dest_MFun bound_M
       
   824       in
       
   825         (MApp (MRaw (t0, MFun (bound_M, aa, bool_M)),
       
   826                MAbs (abs_s, abs_T, M1, aa',
       
   827                      MApp (MApp (MRaw (connective_t,
       
   828                                        mtype_for (fastype_of connective_t)),
       
   829                                  MApp (bound_m, MRaw (Bound 0, M1))),
       
   830                            body_m))), accum)
       
   831       end
       
   832     and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
   795     and do_connect conn mk_quasi_clauses t0 t1 t2 (accum as ({frame, ...}, _)) =
   833       let
   796       let
   834         val frame1 = fresh_frame mdata (SOME Tru) NONE frame
   797         val frame1 = fresh_frame mdata (SOME Tru) NONE frame
   835         val frame2 = fresh_frame mdata (SOME Fls) NONE frame
   798         val frame2 = fresh_frame mdata (SOME Fls) NONE frame
   836         val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   799         val (m1, accum) = accum |>> set_frame frame1 |> do_term t1
   995                         val M = mtype_for T
   958                         val M = mtype_for T
   996                         val aa = V (Unsynchronized.inc max_fresh)
   959                         val aa = V (Unsynchronized.inc max_fresh)
   997                         val (m', accum) =
   960                         val (m', accum) =
   998                           do_term t' (accum |>> push_bound aa T M)
   961                           do_term t' (accum |>> push_bound aa T M)
   999                       in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
   962                       in (MAbs (s, T, M, aa, m'), accum |>> pop_bound) end))
  1000          | (t0 as Const (@{const_name All}, _))
       
  1001            $ Abs (s', T', (t10 as @{const implies}) $ (t11 $ Bound 0) $ t12) =>
       
  1002            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
       
  1003          | (t0 as Const (@{const_name Ex}, _))
       
  1004            $ Abs (s', T', (t10 as @{const conj}) $ (t11 $ Bound 0) $ t12) =>
       
  1005            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
       
  1006          | @{const Not} $ t1 =>
   963          | @{const Not} $ t1 =>
  1007            do_connect "\<implies>" imp_clauses @{const implies} t1
   964            do_connect "\<implies>" imp_clauses @{const implies} t1
  1008                       @{const False} accum
   965                       @{const False} accum
  1009          | (t0 as @{const conj}) $ t1 $ t2 =>
   966          | (t0 as @{const conj}) $ t1 $ t2 =>
  1010            do_connect "\<and>" conj_clauses t0 t1 t2 accum
   967            do_connect "\<and>" conj_clauses t0 t1 t2 accum
  1041                    trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   998                    trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
  1042                                        " \<turnstile> " ^
   999                                        " \<turnstile> " ^
  1043                                        string_for_mterm ctxt m))
  1000                                        string_for_mterm ctxt m))
  1044   in do_term end
  1001   in do_term end
  1045 
  1002 
  1046 fun force_minus_funs 0 _ = I
  1003 fun force_gen_funs 0 _ = I
  1047   | force_minus_funs n (M as MFun (M1, _, M2)) =
  1004   | force_gen_funs n (M as MFun (M1, _, M2)) =
  1048     add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_minus_funs (n - 1) M2
  1005     add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
  1049   | force_minus_funs _ M =
  1006   | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
  1050     raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
       
  1051 fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
  1007 fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
  1052   let
  1008   let
  1053     val (m1, accum) = consider_term mdata t1 accum
  1009     val (m1, accum) = consider_term mdata t1 accum
  1054     val (m2, accum) = consider_term mdata t2 accum
  1010     val (m2, accum) = consider_term mdata t2 accum
  1055     val M1 = mtype_of_mterm m1
  1011     val M1 = mtype_of_mterm m1
  1056     val M2 = mtype_of_mterm m2
  1012     val M2 = mtype_of_mterm m2
  1057     val accum = accum ||> add_mtypes_equal M1 M2
  1013     val accum = accum ||> add_mtypes_equal M1 M2
  1058     val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
  1014     val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
  1059     val m = MApp (MApp (MRaw (Const x,
  1015     val m = MApp (MApp (MRaw (Const x,
  1060                            MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
  1016                            MFun (M1, A Gen, MFun (M2, A Fls, body_M))), m1), m2)
  1061   in
  1017   in
  1062     (m, if def then
  1018     (m, if def then
  1063           let val (head_m, arg_ms) = strip_mcomb m1 in
  1019           let val (head_m, arg_ms) = strip_mcomb m1 in
  1064             accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
  1020             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
  1065           end
  1021           end
  1066         else
  1022         else
  1067           accum)
  1023           accum)
  1068   end
  1024   end
  1069 
  1025 
  1077         fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
  1033         fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
  1078           let
  1034           let
  1079             val abs_M = mtype_for abs_T
  1035             val abs_M = mtype_for abs_T
  1080             val x = Unsynchronized.inc max_fresh
  1036             val x = Unsynchronized.inc max_fresh
  1081             val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
  1037             val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
       
  1038             fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
  1082             val (body_m, accum) =
  1039             val (body_m, accum) =
  1083               accum ||> side_cond
  1040               accum ||> side_cond
  1084                         ? add_mtype_is_complete [(x, (Minus, Fls))] abs_M
  1041                         ? add_mtype_is_complete [(x, (Minus, ann ()))] abs_M
  1085                     |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
  1042                     |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
  1086             val body_M = mtype_of_mterm body_m
  1043             val body_M = mtype_of_mterm body_m
  1087           in
  1044           in
  1088             (MApp (MRaw (Const quant_x,
  1045             (MApp (MRaw (Const quant_x,
  1089                          MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
  1046                          MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
  1112              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
  1069              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
  1113               accum)
  1070               accum)
  1114            end
  1071            end
  1115          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
  1072          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
  1116            do_quantifier x s1 T1 t1
  1073            do_quantifier x s1 T1 t1
  1117          | Const (x0 as (@{const_name Ex}, T0))
  1074          | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
  1118            $ (t1 as Abs (s1, T1, t1')) =>
       
  1119            (case sn of
  1075            (case sn of
  1120               Plus => do_quantifier x0 s1 T1 t1'
  1076               Plus => do_quantifier x0 s1 T1 t1'
  1121             | Minus =>
  1077             | Minus =>
  1122               (* FIXME: Move elsewhere *)
  1078               (* FIXME: Move elsewhere *)
  1123               do_term (@{const Not}
  1079               do_term (@{const Not}
  1238       |> cat_lines)
  1194       |> cat_lines)
  1239 
  1195 
  1240 fun amass f t (ms, accum) =
  1196 fun amass f t (ms, accum) =
  1241   let val (m, accum) = f t accum in (m :: ms, accum) end
  1197   let val (m, accum) = f t accum in (m :: ms, accum) end
  1242 
  1198 
  1243 fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize calculus alpha_T
  1199 fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
  1244           (nondef_ts, def_ts) =
  1200           (nondef_ts, def_ts) =
  1245   let
  1201   let
  1246     val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
  1202     val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
  1247                                 string_for_mtype MAlpha ^ " is " ^
  1203                                 string_for_mtype MAlpha ^ " is " ^
  1248                                 Syntax.string_of_typ ctxt alpha_T)
  1204                                 Syntax.string_of_typ ctxt alpha_T)
  1254                   |> fold (amass (consider_nondefinitional_axiom mdata))
  1210                   |> fold (amass (consider_nondefinitional_axiom mdata))
  1255                           (tl nondef_ts)
  1211                           (tl nondef_ts)
  1256     val (def_ms, (gamma, cset)) =
  1212     val (def_ms, (gamma, cset)) =
  1257       ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
  1213       ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
  1258   in
  1214   in
  1259     case solve calculus (!max_fresh) cset of
  1215     case solve (!max_fresh) cset of
  1260       SOME asgs => (print_mcontext ctxt asgs gamma;
  1216       SOME asgs => (print_mcontext ctxt asgs gamma;
  1261                     SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
  1217                     SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
  1262     | _ => NONE
  1218     | _ => NONE
  1263   end
  1219   end
  1264   handle UNSOLVABLE () => NONE
  1220   handle UNSOLVABLE () => NONE
  1266          raise BAD (loc, commas (map string_for_mtype Ms @
  1222          raise BAD (loc, commas (map string_for_mtype Ms @
  1267                                  map (Syntax.string_of_typ ctxt) Ts))
  1223                                  map (Syntax.string_of_typ ctxt) Ts))
  1268        | MTERM (loc, ms) =>
  1224        | MTERM (loc, ms) =>
  1269          raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
  1225          raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
  1270 
  1226 
  1271 fun formulas_monotonic hol_ctxt =
  1227 val formulas_monotonic = is_some oooo infer "Monotonicity" false
  1272   is_some oooo infer "Monotonicity" false hol_ctxt
       
  1273 
  1228 
  1274 fun fin_fun_constr T1 T2 =
  1229 fun fin_fun_constr T1 T2 =
  1275   (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
  1230   (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
  1276 
  1231 
  1277 fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
  1232 fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
  1278                   finitizes calculus alpha_T tsp =
  1233                   finitizes alpha_T tsp =
  1279   case infer "Finiteness" true hol_ctxt binarize calculus alpha_T tsp of
  1234   case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
  1280     SOME (asgs, msp, constr_mtypes) =>
  1235     SOME (asgs, msp, constr_mtypes) =>
  1281     if forall (curry (op =) Gen o snd) asgs then
  1236     if forall (curry (op =) Gen o snd) asgs then
  1282       tsp
  1237       tsp
  1283     else
  1238     else
  1284       let
  1239       let