src/HOL/Tools/Nitpick/minipick.ML
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
     1 (*  Title:      HOL/Tools/Nitpick/minipick.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Finite model generation for HOL formulas using Kodkod, minimalistic version.
     6 *)
     7 
     8 signature MINIPICK =
     9 sig
    10   datatype rep = SRep | RRep
    11   type styp = Nitpick_Util.styp
    12 
    13   val vars_for_bound_var :
    14     (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    15   val rel_expr_for_bound_var :
    16     (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    17   val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    18   val false_atom : Kodkod.rel_expr
    19   val true_atom : Kodkod.rel_expr
    20   val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    21   val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    22   val kodkod_problem_from_term :
    23     Proof.context -> (typ -> int) -> term -> Kodkod.problem
    24   val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    25 end;
    26 
    27 structure Minipick : MINIPICK =
    28 struct
    29 
    30 open Kodkod
    31 open Nitpick_Util
    32 open Nitpick_HOL
    33 open Nitpick_Peephole
    34 open Nitpick_Kodkod
    35 
    36 datatype rep = SRep | RRep
    37 
    38 fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    39     List.app (check_type ctxt) Ts
    40   | check_type ctxt (Type (@{type_name prod}, Ts)) =
    41     List.app (check_type ctxt) Ts
    42   | check_type _ @{typ bool} = ()
    43   | check_type _ (TFree (_, @{sort "{}"})) = ()
    44   | check_type _ (TFree (_, @{sort HOL.type})) = ()
    45   | check_type ctxt T =
    46     raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    47 
    48 fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
    49     replicate_list (card T1) (atom_schema_of SRep card T2)
    50   | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    51     atom_schema_of SRep card T1
    52   | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    53     atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    54   | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    55     maps (atom_schema_of SRep card) Ts
    56   | atom_schema_of _ card T = [card T]
    57 val arity_of = length ooo atom_schema_of
    58 
    59 fun index_for_bound_var _ [_] 0 = 0
    60   | index_for_bound_var card (_ :: Ts) 0 =
    61     index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
    62   | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
    63 fun vars_for_bound_var card R Ts j =
    64   map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
    65                                (arity_of R card (nth Ts j)))
    66 val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
    67 fun decls_for R card Ts T =
    68   map2 (curry DeclOne o pair 1)
    69        (index_seq (index_for_bound_var card (T :: Ts) 0)
    70                   (arity_of R card (nth (T :: Ts) 0)))
    71        (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    72 
    73 val atom_product = foldl1 Product o map Atom
    74 
    75 val false_atom = Atom 0
    76 val true_atom = Atom 1
    77 
    78 fun formula_from_atom r = RelEq (r, true_atom)
    79 fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    80 
    81 fun kodkod_formula_from_term ctxt card frees =
    82   let
    83     fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    84         let
    85           val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    86                     |> all_combinations
    87         in
    88           map2 (fn i => fn js =>
    89                    RelIf (formula_from_atom (Project (r, [Num i])),
    90                           atom_product js, empty_n_ary_rel (length js)))
    91                (index_seq 0 (length jss)) jss
    92           |> foldl1 Union
    93         end
    94       | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    95         let
    96           val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    97                     |> all_combinations
    98           val arity2 = arity_of SRep card T2
    99         in
   100           map2 (fn i => fn js =>
   101                    Product (atom_product js,
   102                             Project (r, num_seq (i * arity2) arity2)
   103                             |> R_rep_from_S_rep T2))
   104                (index_seq 0 (length jss)) jss
   105           |> foldl1 Union
   106         end
   107       | R_rep_from_S_rep _ r = r
   108     fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   109         Comprehension (decls_for SRep card Ts T,
   110             RelEq (R_rep_from_S_rep T
   111                        (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
   112       | S_rep_from_R_rep _ _ r = r
   113     fun to_F Ts t =
   114       (case t of
   115          @{const Not} $ t1 => Not (to_F Ts t1)
   116        | @{const False} => False
   117        | @{const True} => True
   118        | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   119          All (decls_for SRep card Ts T, to_F (T :: Ts) t')
   120        | (t0 as Const (@{const_name All}, _)) $ t1 =>
   121          to_F Ts (t0 $ eta_expand Ts t1 1)
   122        | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   123          Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
   124        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   125          to_F Ts (t0 $ eta_expand Ts t1 1)
   126        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   127          RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   128        | Const (@{const_name ord_class.less_eq},
   129                 Type (@{type_name fun},
   130                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   131          $ t1 $ t2 =>
   132          Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   133        | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   134        | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   135        | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   136        | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   137        | Free _ => raise SAME ()
   138        | Term.Var _ => raise SAME ()
   139        | Bound _ => raise SAME ()
   140        | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   141        | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   142       handle SAME () => formula_from_atom (to_R_rep Ts t)
   143     and to_S_rep Ts t =
   144       case t of
   145         Const (@{const_name Pair}, _) $ t1 $ t2 =>
   146         Product (to_S_rep Ts t1, to_S_rep Ts t2)
   147       | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
   148       | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
   149       | Const (@{const_name fst}, _) $ t1 =>
   150         let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
   151           Project (to_S_rep Ts t1, num_seq 0 fst_arity)
   152         end
   153       | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
   154       | Const (@{const_name snd}, _) $ t1 =>
   155         let
   156           val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
   157           val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
   158           val fst_arity = pair_arity - snd_arity
   159         in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
   160       | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   161       | Bound j => rel_expr_for_bound_var card SRep Ts j
   162       | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   163     and to_R_rep Ts t =
   164       (case t of
   165          @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   166        | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   167        | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   168        | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   169        | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   170        | Const (@{const_name ord_class.less_eq},
   171                 Type (@{type_name fun},
   172                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   173          to_R_rep Ts (eta_expand Ts t 1)
   174        | Const (@{const_name ord_class.less_eq}, _) =>
   175          to_R_rep Ts (eta_expand Ts t 2)
   176        | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   177        | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   178        | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   179        | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   180        | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   181        | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   182        | Const (@{const_name bot_class.bot},
   183                 T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   184          empty_n_ary_rel (arity_of RRep card T)
   185        | Const (@{const_name insert}, _) $ t1 $ t2 =>
   186          Union (to_S_rep Ts t1, to_R_rep Ts t2)
   187        | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   188        | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   189        | Const (@{const_name trancl}, _) $ t1 =>
   190          if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
   191            Closure (to_R_rep Ts t1)
   192          else
   193            raise NOT_SUPPORTED "transitive closure for function or pair type"
   194        | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   195        | Const (@{const_name semilattice_inf_class.inf},
   196                 Type (@{type_name fun},
   197                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   198          $ t1 $ t2 =>
   199          Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   200        | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
   201          to_R_rep Ts (eta_expand Ts t 1)
   202        | Const (@{const_name semilattice_inf_class.inf}, _) =>
   203          to_R_rep Ts (eta_expand Ts t 2)
   204        | Const (@{const_name semilattice_sup_class.sup},
   205                 Type (@{type_name fun},
   206                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   207          $ t1 $ t2 =>
   208          Union (to_R_rep Ts t1, to_R_rep Ts t2)
   209        | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
   210          to_R_rep Ts (eta_expand Ts t 1)
   211        | Const (@{const_name semilattice_sup_class.sup}, _) =>
   212          to_R_rep Ts (eta_expand Ts t 2)
   213        | Const (@{const_name minus_class.minus},
   214                 Type (@{type_name fun},
   215                       [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   216          $ t1 $ t2 =>
   217          Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   218        | Const (@{const_name minus_class.minus},
   219                 Type (@{type_name fun},
   220                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   221          to_R_rep Ts (eta_expand Ts t 1)
   222        | Const (@{const_name minus_class.minus},
   223                 Type (@{type_name fun},
   224                       [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   225          to_R_rep Ts (eta_expand Ts t 2)
   226        | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   227        | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   228        | Const (@{const_name Pair}, _) => raise SAME ()
   229        | Const (@{const_name fst}, _) $ _ => raise SAME ()
   230        | Const (@{const_name fst}, _) => raise SAME ()
   231        | Const (@{const_name snd}, _) $ _ => raise SAME ()
   232        | Const (@{const_name snd}, _) => raise SAME ()
   233        | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   234        | Free (x as (_, T)) =>
   235          Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
   236        | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   237        | Bound _ => raise SAME ()
   238        | Abs (_, T, t') =>
   239          (case fastype_of1 (T :: Ts, t') of
   240             @{typ bool} => Comprehension (decls_for SRep card Ts T,
   241                                           to_F (T :: Ts) t')
   242           | T' => Comprehension (decls_for SRep card Ts T @
   243                                  decls_for RRep card (T :: Ts) T',
   244                                  Subset (rel_expr_for_bound_var card RRep
   245                                                               (T' :: T :: Ts) 0,
   246                                          to_R_rep (T :: Ts) t')))
   247        | t1 $ t2 =>
   248          (case fastype_of1 (Ts, t) of
   249             @{typ bool} => atom_from_formula (to_F Ts t)
   250           | T =>
   251             let val T2 = fastype_of1 (Ts, t2) in
   252               case arity_of SRep card T2 of
   253                 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   254               | arity2 =>
   255                 let val res_arity = arity_of RRep card T in
   256                   Project (Intersect
   257                       (Product (to_S_rep Ts t2,
   258                                 atom_schema_of RRep card T
   259                                 |> map (AtomSeq o rpair 0) |> foldl1 Product),
   260                        to_R_rep Ts t1),
   261                       num_seq arity2 res_arity)
   262                 end
   263             end)
   264        | _ => raise NOT_SUPPORTED ("term " ^
   265                                    quote (Syntax.string_of_term ctxt t)))
   266       handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   267   in to_F [] end
   268 
   269 fun bound_for_free card i (s, T) =
   270   let val js = atom_schema_of RRep card T in
   271     ([((length js, i), s)],
   272      [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
   273                    |> tuple_set_from_atom_schema])
   274   end
   275 
   276 fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   277                                    r =
   278     if body_type T2 = bool_T then
   279       True
   280     else
   281       All (decls_for SRep card Ts T1,
   282            declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   283                (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
   284   | declarative_axiom_for_rel_expr _ _ _ r = One r
   285 fun declarative_axiom_for_free card i (_, T) =
   286   declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
   287 
   288 fun kodkod_problem_from_term ctxt raw_card t =
   289   let
   290     val thy = ProofContext.theory_of ctxt
   291     fun card (Type (@{type_name fun}, [T1, T2])) =
   292         reasonable_power (card T2) (card T1)
   293       | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   294       | card @{typ bool} = 2
   295       | card T = Int.max (1, raw_card T)
   296     val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   297     val _ = fold_types (K o check_type ctxt) neg_t ()
   298     val frees = Term.add_frees neg_t []
   299     val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   300     val declarative_axioms =
   301       map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   302     val formula = kodkod_formula_from_term ctxt card frees neg_t
   303                   |> fold_rev (curry And) declarative_axioms
   304     val univ_card = univ_card 0 0 0 bounds formula
   305   in
   306     {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   307      bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   308   end
   309 
   310 fun solve_any_kodkod_problem thy problems =
   311   let
   312     val {overlord, ...} = Nitpick_Isar.default_params thy []
   313     val max_threads = 1
   314     val max_solutions = 1
   315   in
   316     case solve_any_problem overlord NONE max_threads max_solutions problems of
   317       JavaNotInstalled => "unknown"
   318     | JavaTooOld => "unknown"
   319     | KodkodiNotInstalled => "unknown"
   320     | Normal ([], _, _) => "none"
   321     | Normal _ => "genuine"
   322     | TimedOut _ => "unknown"
   323     | Interrupted _ => "unknown"
   324     | Error (s, _) => error ("Kodkod error: " ^ s)
   325   end
   326 
   327 end;