src/HOL/Tools/Nitpick/minipick.ML
changeset 39223 022f16801e4e
parent 39218 7f4fb691e4b6
parent 39222 decf607a5a67
child 39224 39e0d3b86112
child 39225 52960d359969
child 39257 eec61233dbad
     1.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Sep 08 14:46:21 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,327 +0,0 @@
     1.4 -(*  Title:      HOL/Tools/Nitpick/minipick.ML
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009, 2010
     1.7 -
     1.8 -Finite model generation for HOL formulas using Kodkod, minimalistic version.
     1.9 -*)
    1.10 -
    1.11 -signature MINIPICK =
    1.12 -sig
    1.13 -  datatype rep = SRep | RRep
    1.14 -  type styp = Nitpick_Util.styp
    1.15 -
    1.16 -  val vars_for_bound_var :
    1.17 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    1.18 -  val rel_expr_for_bound_var :
    1.19 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    1.20 -  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    1.21 -  val false_atom : Kodkod.rel_expr
    1.22 -  val true_atom : Kodkod.rel_expr
    1.23 -  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    1.24 -  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    1.25 -  val kodkod_problem_from_term :
    1.26 -    Proof.context -> (typ -> int) -> term -> Kodkod.problem
    1.27 -  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    1.28 -end;
    1.29 -
    1.30 -structure Minipick : MINIPICK =
    1.31 -struct
    1.32 -
    1.33 -open Kodkod
    1.34 -open Nitpick_Util
    1.35 -open Nitpick_HOL
    1.36 -open Nitpick_Peephole
    1.37 -open Nitpick_Kodkod
    1.38 -
    1.39 -datatype rep = SRep | RRep
    1.40 -
    1.41 -fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    1.42 -    List.app (check_type ctxt) Ts
    1.43 -  | check_type ctxt (Type (@{type_name prod}, Ts)) =
    1.44 -    List.app (check_type ctxt) Ts
    1.45 -  | check_type _ @{typ bool} = ()
    1.46 -  | check_type _ (TFree (_, @{sort "{}"})) = ()
    1.47 -  | check_type _ (TFree (_, @{sort HOL.type})) = ()
    1.48 -  | check_type ctxt T =
    1.49 -    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    1.50 -
    1.51 -fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
    1.52 -    replicate_list (card T1) (atom_schema_of SRep card T2)
    1.53 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    1.54 -    atom_schema_of SRep card T1
    1.55 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    1.56 -    atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    1.57 -  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    1.58 -    maps (atom_schema_of SRep card) Ts
    1.59 -  | atom_schema_of _ card T = [card T]
    1.60 -val arity_of = length ooo atom_schema_of
    1.61 -
    1.62 -fun index_for_bound_var _ [_] 0 = 0
    1.63 -  | index_for_bound_var card (_ :: Ts) 0 =
    1.64 -    index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
    1.65 -  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
    1.66 -fun vars_for_bound_var card R Ts j =
    1.67 -  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
    1.68 -                               (arity_of R card (nth Ts j)))
    1.69 -val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
    1.70 -fun decls_for R card Ts T =
    1.71 -  map2 (curry DeclOne o pair 1)
    1.72 -       (index_seq (index_for_bound_var card (T :: Ts) 0)
    1.73 -                  (arity_of R card (nth (T :: Ts) 0)))
    1.74 -       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    1.75 -
    1.76 -val atom_product = foldl1 Product o map Atom
    1.77 -
    1.78 -val false_atom = Atom 0
    1.79 -val true_atom = Atom 1
    1.80 -
    1.81 -fun formula_from_atom r = RelEq (r, true_atom)
    1.82 -fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    1.83 -
    1.84 -fun kodkod_formula_from_term ctxt card frees =
    1.85 -  let
    1.86 -    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    1.87 -        let
    1.88 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    1.89 -                    |> all_combinations
    1.90 -        in
    1.91 -          map2 (fn i => fn js =>
    1.92 -                   RelIf (formula_from_atom (Project (r, [Num i])),
    1.93 -                          atom_product js, empty_n_ary_rel (length js)))
    1.94 -               (index_seq 0 (length jss)) jss
    1.95 -          |> foldl1 Union
    1.96 -        end
    1.97 -      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    1.98 -        let
    1.99 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
   1.100 -                    |> all_combinations
   1.101 -          val arity2 = arity_of SRep card T2
   1.102 -        in
   1.103 -          map2 (fn i => fn js =>
   1.104 -                   Product (atom_product js,
   1.105 -                            Project (r, num_seq (i * arity2) arity2)
   1.106 -                            |> R_rep_from_S_rep T2))
   1.107 -               (index_seq 0 (length jss)) jss
   1.108 -          |> foldl1 Union
   1.109 -        end
   1.110 -      | R_rep_from_S_rep _ r = r
   1.111 -    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   1.112 -        Comprehension (decls_for SRep card Ts T,
   1.113 -            RelEq (R_rep_from_S_rep T
   1.114 -                       (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
   1.115 -      | S_rep_from_R_rep _ _ r = r
   1.116 -    fun to_F Ts t =
   1.117 -      (case t of
   1.118 -         @{const Not} $ t1 => Not (to_F Ts t1)
   1.119 -       | @{const False} => False
   1.120 -       | @{const True} => True
   1.121 -       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   1.122 -         All (decls_for SRep card Ts T, to_F (T :: Ts) t')
   1.123 -       | (t0 as Const (@{const_name All}, _)) $ t1 =>
   1.124 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   1.125 -       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   1.126 -         Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
   1.127 -       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   1.128 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   1.129 -       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   1.130 -         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   1.131 -       | Const (@{const_name ord_class.less_eq},
   1.132 -                Type (@{type_name fun},
   1.133 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.134 -         $ t1 $ t2 =>
   1.135 -         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   1.136 -       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   1.137 -       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   1.138 -       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   1.139 -       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   1.140 -       | Free _ => raise SAME ()
   1.141 -       | Term.Var _ => raise SAME ()
   1.142 -       | Bound _ => raise SAME ()
   1.143 -       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   1.144 -       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   1.145 -      handle SAME () => formula_from_atom (to_R_rep Ts t)
   1.146 -    and to_S_rep Ts t =
   1.147 -      case t of
   1.148 -        Const (@{const_name Pair}, _) $ t1 $ t2 =>
   1.149 -        Product (to_S_rep Ts t1, to_S_rep Ts t2)
   1.150 -      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
   1.151 -      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
   1.152 -      | Const (@{const_name fst}, _) $ t1 =>
   1.153 -        let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
   1.154 -          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
   1.155 -        end
   1.156 -      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
   1.157 -      | Const (@{const_name snd}, _) $ t1 =>
   1.158 -        let
   1.159 -          val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
   1.160 -          val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
   1.161 -          val fst_arity = pair_arity - snd_arity
   1.162 -        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
   1.163 -      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   1.164 -      | Bound j => rel_expr_for_bound_var card SRep Ts j
   1.165 -      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   1.166 -    and to_R_rep Ts t =
   1.167 -      (case t of
   1.168 -         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   1.169 -       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   1.170 -       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   1.171 -       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.172 -       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   1.173 -       | Const (@{const_name ord_class.less_eq},
   1.174 -                Type (@{type_name fun},
   1.175 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   1.176 -         to_R_rep Ts (eta_expand Ts t 1)
   1.177 -       | Const (@{const_name ord_class.less_eq}, _) =>
   1.178 -         to_R_rep Ts (eta_expand Ts t 2)
   1.179 -       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.180 -       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   1.181 -       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.182 -       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   1.183 -       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.184 -       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   1.185 -       | Const (@{const_name bot_class.bot},
   1.186 -                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   1.187 -         empty_n_ary_rel (arity_of RRep card T)
   1.188 -       | Const (@{const_name insert}, _) $ t1 $ t2 =>
   1.189 -         Union (to_S_rep Ts t1, to_R_rep Ts t2)
   1.190 -       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   1.191 -       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   1.192 -       | Const (@{const_name trancl}, _) $ t1 =>
   1.193 -         if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
   1.194 -           Closure (to_R_rep Ts t1)
   1.195 -         else
   1.196 -           raise NOT_SUPPORTED "transitive closure for function or pair type"
   1.197 -       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   1.198 -       | Const (@{const_name semilattice_inf_class.inf},
   1.199 -                Type (@{type_name fun},
   1.200 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.201 -         $ t1 $ t2 =>
   1.202 -         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   1.203 -       | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
   1.204 -         to_R_rep Ts (eta_expand Ts t 1)
   1.205 -       | Const (@{const_name semilattice_inf_class.inf}, _) =>
   1.206 -         to_R_rep Ts (eta_expand Ts t 2)
   1.207 -       | Const (@{const_name semilattice_sup_class.sup},
   1.208 -                Type (@{type_name fun},
   1.209 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.210 -         $ t1 $ t2 =>
   1.211 -         Union (to_R_rep Ts t1, to_R_rep Ts t2)
   1.212 -       | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
   1.213 -         to_R_rep Ts (eta_expand Ts t 1)
   1.214 -       | Const (@{const_name semilattice_sup_class.sup}, _) =>
   1.215 -         to_R_rep Ts (eta_expand Ts t 2)
   1.216 -       | Const (@{const_name minus_class.minus},
   1.217 -                Type (@{type_name fun},
   1.218 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   1.219 -         $ t1 $ t2 =>
   1.220 -         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   1.221 -       | Const (@{const_name minus_class.minus},
   1.222 -                Type (@{type_name fun},
   1.223 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   1.224 -         to_R_rep Ts (eta_expand Ts t 1)
   1.225 -       | Const (@{const_name minus_class.minus},
   1.226 -                Type (@{type_name fun},
   1.227 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   1.228 -         to_R_rep Ts (eta_expand Ts t 2)
   1.229 -       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   1.230 -       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   1.231 -       | Const (@{const_name Pair}, _) => raise SAME ()
   1.232 -       | Const (@{const_name fst}, _) $ _ => raise SAME ()
   1.233 -       | Const (@{const_name fst}, _) => raise SAME ()
   1.234 -       | Const (@{const_name snd}, _) $ _ => raise SAME ()
   1.235 -       | Const (@{const_name snd}, _) => raise SAME ()
   1.236 -       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   1.237 -       | Free (x as (_, T)) =>
   1.238 -         Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
   1.239 -       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   1.240 -       | Bound _ => raise SAME ()
   1.241 -       | Abs (_, T, t') =>
   1.242 -         (case fastype_of1 (T :: Ts, t') of
   1.243 -            @{typ bool} => Comprehension (decls_for SRep card Ts T,
   1.244 -                                          to_F (T :: Ts) t')
   1.245 -          | T' => Comprehension (decls_for SRep card Ts T @
   1.246 -                                 decls_for RRep card (T :: Ts) T',
   1.247 -                                 Subset (rel_expr_for_bound_var card RRep
   1.248 -                                                              (T' :: T :: Ts) 0,
   1.249 -                                         to_R_rep (T :: Ts) t')))
   1.250 -       | t1 $ t2 =>
   1.251 -         (case fastype_of1 (Ts, t) of
   1.252 -            @{typ bool} => atom_from_formula (to_F Ts t)
   1.253 -          | T =>
   1.254 -            let val T2 = fastype_of1 (Ts, t2) in
   1.255 -              case arity_of SRep card T2 of
   1.256 -                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   1.257 -              | arity2 =>
   1.258 -                let val res_arity = arity_of RRep card T in
   1.259 -                  Project (Intersect
   1.260 -                      (Product (to_S_rep Ts t2,
   1.261 -                                atom_schema_of RRep card T
   1.262 -                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
   1.263 -                       to_R_rep Ts t1),
   1.264 -                      num_seq arity2 res_arity)
   1.265 -                end
   1.266 -            end)
   1.267 -       | _ => raise NOT_SUPPORTED ("term " ^
   1.268 -                                   quote (Syntax.string_of_term ctxt t)))
   1.269 -      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   1.270 -  in to_F [] end
   1.271 -
   1.272 -fun bound_for_free card i (s, T) =
   1.273 -  let val js = atom_schema_of RRep card T in
   1.274 -    ([((length js, i), s)],
   1.275 -     [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
   1.276 -                   |> tuple_set_from_atom_schema])
   1.277 -  end
   1.278 -
   1.279 -fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   1.280 -                                   r =
   1.281 -    if body_type T2 = bool_T then
   1.282 -      True
   1.283 -    else
   1.284 -      All (decls_for SRep card Ts T1,
   1.285 -           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   1.286 -               (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
   1.287 -  | declarative_axiom_for_rel_expr _ _ _ r = One r
   1.288 -fun declarative_axiom_for_free card i (_, T) =
   1.289 -  declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
   1.290 -
   1.291 -fun kodkod_problem_from_term ctxt raw_card t =
   1.292 -  let
   1.293 -    val thy = ProofContext.theory_of ctxt
   1.294 -    fun card (Type (@{type_name fun}, [T1, T2])) =
   1.295 -        reasonable_power (card T2) (card T1)
   1.296 -      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   1.297 -      | card @{typ bool} = 2
   1.298 -      | card T = Int.max (1, raw_card T)
   1.299 -    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   1.300 -    val _ = fold_types (K o check_type ctxt) neg_t ()
   1.301 -    val frees = Term.add_frees neg_t []
   1.302 -    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   1.303 -    val declarative_axioms =
   1.304 -      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   1.305 -    val formula = kodkod_formula_from_term ctxt card frees neg_t
   1.306 -                  |> fold_rev (curry And) declarative_axioms
   1.307 -    val univ_card = univ_card 0 0 0 bounds formula
   1.308 -  in
   1.309 -    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   1.310 -     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   1.311 -  end
   1.312 -
   1.313 -fun solve_any_kodkod_problem thy problems =
   1.314 -  let
   1.315 -    val {overlord, ...} = Nitpick_Isar.default_params thy []
   1.316 -    val max_threads = 1
   1.317 -    val max_solutions = 1
   1.318 -  in
   1.319 -    case solve_any_problem overlord NONE max_threads max_solutions problems of
   1.320 -      JavaNotInstalled => "unknown"
   1.321 -    | JavaTooOld => "unknown"
   1.322 -    | KodkodiNotInstalled => "unknown"
   1.323 -    | Normal ([], _, _) => "none"
   1.324 -    | Normal _ => "genuine"
   1.325 -    | TimedOut _ => "unknown"
   1.326 -    | Interrupted _ => "unknown"
   1.327 -    | Error (s, _) => error ("Kodkod error: " ^ s)
   1.328 -  end
   1.329 -
   1.330 -end;