wneuper/isa: src/HOL/Tools/Nitpick/minipick.ML@9edc2bd6d2bd

     1 (*  Title:      HOL/Tools/Nitpick/minipick.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009, 2010

     5 Finite model generation for HOL formulas using Kodkod, minimalistic version.

     6 *)

     8 signature MINIPICK =

     9 sig

    10   datatype rep = SRep | RRep

    11   type styp = Nitpick_Util.styp

    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;

    27 structure Minipick : MINIPICK =

    28 struct

    30 open Kodkod

    31 open Nitpick_Util

    32 open Nitpick_HOL

    33 open Nitpick_Peephole

    34 open Nitpick_Kodkod

    36 datatype rep = SRep | RRep

    38 (* Proof.context -> typ -> unit *)

    39 fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts

    40   | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts

    41   | check_type _ @{typ bool} = ()

    42   | check_type _ (TFree (_, @{sort "{}"})) = ()

    43   | check_type _ (TFree (_, @{sort HOL.type})) = ()

    44   | check_type ctxt T =

    45     raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))

    47 (* rep -> (typ -> int) -> typ -> int list *)

    48 fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =

    49     replicate_list (card T1) (atom_schema_of SRep card T2)

    50   | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =

    51     atom_schema_of SRep card T1

    52   | atom_schema_of RRep card (Type ("fun", [T1, T2])) =

    53     atom_schema_of SRep card T1 @ atom_schema_of RRep card T2

    54   | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts

    55   | atom_schema_of _ card T = [card T]

    56 (* rep -> (typ -> int) -> typ -> int *)

    57 val arity_of = length ooo atom_schema_of

    59 (* (typ -> int) -> typ list -> int -> int *)

    60 fun index_for_bound_var _ [_] 0 = 0

    61   | index_for_bound_var card (_ :: Ts) 0 =

    62     index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)

    63   | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)

    64 (* (typ -> int) -> rep -> typ list -> int -> rel_expr list *)

    65 fun vars_for_bound_var card R Ts j =

    66   map (curry Var 1) (index_seq (index_for_bound_var card Ts j)

    67                                (arity_of R card (nth Ts j)))

    68 (* (typ -> int) -> rep -> typ list -> int -> rel_expr *)

    69 val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var

    70 (* rep -> (typ -> int) -> typ list -> typ -> decl list *)

    71 fun decls_for R card Ts T =

    72   map2 (curry DeclOne o pair 1)

    73        (index_seq (index_for_bound_var card (T :: Ts) 0)

    74                   (arity_of R card (nth (T :: Ts) 0)))

    75        (map (AtomSeq o rpair 0) (atom_schema_of R card T))

    77 (* int list -> rel_expr *)

    78 val atom_product = foldl1 Product o map Atom

    80 val false_atom = Atom 0

    81 val true_atom = Atom 1

    83 (* rel_expr -> formula *)

    84 fun formula_from_atom r = RelEq (r, true_atom)

    85 (* formula -> rel_expr *)

    86 fun atom_from_formula f = RelIf (f, true_atom, false_atom)

    88 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)

    89 fun kodkod_formula_from_term ctxt card frees =

    90   let

    91     (* typ -> rel_expr -> rel_expr *)

    92     fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =

    93         let

    94           val jss = atom_schema_of SRep card T1 |> map (rpair 0)

    95                     |> all_combinations

    96         in

    97           map2 (fn i => fn js =>

    98                    RelIf (formula_from_atom (Project (r, [Num i])),

    99                           atom_product js, empty_n_ary_rel (length js)))

   100                (index_seq 0 (length jss)) jss

   101           |> foldl1 Union

   102         end

   103       | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =

   104         let

   105           val jss = atom_schema_of SRep card T1 |> map (rpair 0)

   106                     |> all_combinations

   107           val arity2 = arity_of SRep card T2

   108         in

   109           map2 (fn i => fn js =>

   110                    Product (atom_product js,

   111                             Project (r, num_seq (i * arity2) arity2)

   112                             |> R_rep_from_S_rep T2))

   113                (index_seq 0 (length jss)) jss

   114           |> foldl1 Union

   115         end

   116       | R_rep_from_S_rep _ r = r

   117     (* typ list -> typ -> rel_expr -> rel_expr *)

   118     fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =

   119         Comprehension (decls_for SRep card Ts T,

   120             RelEq (R_rep_from_S_rep T

   121                        (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))

   122       | S_rep_from_R_rep _ _ r = r

   123     (* typ list -> term -> formula *)

   124     fun to_F Ts t =

   125       (case t of

   126          @{const Not} $ t1 => Not (to_F Ts t1)

   127        | @{const False} => False

   128        | @{const True} => True

   129        | Const (@{const_name All}, _) $ Abs (s, T, t') =>

   130          All (decls_for SRep card Ts T, to_F (T :: Ts) t')

   131        | (t0 as Const (@{const_name All}, _)) $ t1 =>

   132          to_F Ts (t0 $ eta_expand Ts t1 1)

   133        | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>

   134          Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')

   135        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>

   136          to_F Ts (t0 $ eta_expand Ts t1 1)

   137        | Const (@{const_name "op ="}, _) $ t1 $ t2 =>

   138          RelEq (to_R_rep Ts t1, to_R_rep Ts t2)

   139        | Const (@{const_name ord_class.less_eq},

   140                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>

   141          Subset (to_R_rep Ts t1, to_R_rep Ts t2)

   142        | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)

   143        | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)

   144        | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)

   145        | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)

   146        | Free _ => raise SAME ()

   147        | Term.Var _ => raise SAME ()

   148        | Bound _ => raise SAME ()

   149        | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)

   150        | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))

   151       handle SAME () => formula_from_atom (to_R_rep Ts t)

   152     (* typ list -> term -> rel_expr *)

   153     and to_S_rep Ts t =

   154         case t of

   155           Const (@{const_name Pair}, _) $ t1 $ t2 =>

   156           Product (to_S_rep Ts t1, to_S_rep Ts t2)

   157         | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)

   158         | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)

   159         | Const (@{const_name fst}, _) $ t1 =>

   160           let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in

   161             Project (to_S_rep Ts t1, num_seq 0 fst_arity)

   162           end

   163         | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)

   164         | Const (@{const_name snd}, _) $ t1 =>

   165           let

   166             val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))

   167             val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))

   168             val fst_arity = pair_arity - snd_arity

   169           in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end

   170         | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)

   171         | Bound j => rel_expr_for_bound_var card SRep Ts j

   172         | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)

   173     (* term -> rel_expr *)

   174     and to_R_rep Ts t =

   175       (case t of

   176          @{const Not} => to_R_rep Ts (eta_expand Ts t 1)

   177        | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)

   178        | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)

   179        | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)

   180        | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)

   181        | Const (@{const_name ord_class.less_eq},

   182                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>

   183          to_R_rep Ts (eta_expand Ts t 1)

   184        | Const (@{const_name ord_class.less_eq}, _) =>

   185          to_R_rep Ts (eta_expand Ts t 2)

   186        | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   187        | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)

   188        | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   189        | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)

   190        | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)

   191        | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)

   192        | Const (@{const_name bot_class.bot},

   193                 T as Type ("fun", [_, @{typ bool}])) =>

   194          empty_n_ary_rel (arity_of RRep card T)

   195        | Const (@{const_name insert}, _) $ t1 $ t2 =>

   196          Union (to_S_rep Ts t1, to_R_rep Ts t2)

   197        | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)

   198        | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)

   199        | Const (@{const_name trancl}, _) $ t1 =>

   200          if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then

   201            Closure (to_R_rep Ts t1)

   202          else

   203            raise NOT_SUPPORTED "transitive closure for function or pair type"

   204        | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)

   205        | Const (@{const_name semilattice_inf_class.inf},

   206                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>

   207          Intersect (to_R_rep Ts t1, to_R_rep Ts t2)

   208        | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>

   209          to_R_rep Ts (eta_expand Ts t 1)

   210        | Const (@{const_name semilattice_inf_class.inf}, _) =>

   211          to_R_rep Ts (eta_expand Ts t 2)

   212        | Const (@{const_name semilattice_sup_class.sup},

   213                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>

   214          Union (to_R_rep Ts t1, to_R_rep Ts t2)

   215        | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>

   216          to_R_rep Ts (eta_expand Ts t 1)

   217        | Const (@{const_name semilattice_sup_class.sup}, _) =>

   218          to_R_rep Ts (eta_expand Ts t 2)

   219        | Const (@{const_name minus_class.minus},

   220                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>

   221          Difference (to_R_rep Ts t1, to_R_rep Ts t2)

   222        | Const (@{const_name minus_class.minus},

   223                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>

   224          to_R_rep Ts (eta_expand Ts t 1)

   225        | Const (@{const_name minus_class.minus},

   226                 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>

   227          to_R_rep Ts (eta_expand Ts t 2)

   228        | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()

   229        | Const (@{const_name Pair}, _) $ _ => raise SAME ()

   230        | Const (@{const_name Pair}, _) => raise SAME ()

   231        | Const (@{const_name fst}, _) $ _ => raise SAME ()

   232        | Const (@{const_name fst}, _) => raise SAME ()

   233        | Const (@{const_name snd}, _) $ _ => raise SAME ()

   234        | Const (@{const_name snd}, _) => raise SAME ()

   235        | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)

   236        | Free (x as (_, T)) =>

   237          Rel (arity_of RRep card T, find_index (curry (op =) x) frees)

   238        | Term.Var _ => raise NOT_SUPPORTED "schematic variables"

   239        | Bound _ => raise SAME ()

   240        | Abs (_, T, t') =>

   241          (case fastype_of1 (T :: Ts, t') of

   242             @{typ bool} => Comprehension (decls_for SRep card Ts T,

   243                                           to_F (T :: Ts) t')

   244           | T' => Comprehension (decls_for SRep card Ts T @

   245                                  decls_for RRep card (T :: Ts) T',

   246                                  Subset (rel_expr_for_bound_var card RRep

   247                                                               (T' :: T :: Ts) 0,

   248                                          to_R_rep (T :: Ts) t')))

   249        | t1 $ t2 =>

   250          (case fastype_of1 (Ts, t) of

   251             @{typ bool} => atom_from_formula (to_F Ts t)

   252           | T =>

   253             let val T2 = fastype_of1 (Ts, t2) in

   254               case arity_of SRep card T2 of

   255                 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)

   256               | arity2 =>

   257                 let val res_arity = arity_of RRep card T in

   258                   Project (Intersect

   259                       (Product (to_S_rep Ts t2,

   260                                 atom_schema_of RRep card T

   261                                 |> map (AtomSeq o rpair 0) |> foldl1 Product),

   262                        to_R_rep Ts t1),

   263                       num_seq arity2 res_arity)

   264                 end

   265             end)

   266        | _ => raise NOT_SUPPORTED ("term " ^

   267                                    quote (Syntax.string_of_term ctxt t)))

   268       handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)

   269   in to_F [] end

   271 (* (typ -> int) -> int -> styp -> bound *)

   272 fun bound_for_free card i (s, T) =

   273   let val js = atom_schema_of RRep card T in

   274     ([((length js, i), s)],

   275      [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)

   276                    |> tuple_set_from_atom_schema])

   277   end

   279 (* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)

   280 fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =

   281     if body_type T2 = bool_T then

   282       True

   283     else

   284       All (decls_for SRep card Ts T1,

   285            declarative_axiom_for_rel_expr card (T1 :: Ts) T2

   286                (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))

   287   | declarative_axiom_for_rel_expr _ _ _ r = One r

   288 (* (typ -> int) -> bool -> int -> styp -> formula *)

   289 fun declarative_axiom_for_free card i (_, T) =

   290   declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))

   292 (* Proof.context -> (typ -> int) -> term -> problem *)

   293 fun kodkod_problem_from_term ctxt raw_card t =

   294   let

   295     val thy = ProofContext.theory_of ctxt

   296     (* typ -> int *)

   297     fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)

   298       | card (Type ("*", [T1, T2])) = card T1 * card T2

   299       | card @{typ bool} = 2

   300       | card T = Int.max (1, raw_card T)

   301     val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t

   302     val _ = fold_types (K o check_type ctxt) neg_t ()

   303     val frees = Term.add_frees neg_t []

   304     val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees

   305     val declarative_axioms =

   306       map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees

   307     val formula = kodkod_formula_from_term ctxt card frees neg_t

   308                   |> fold_rev (curry And) declarative_axioms

   309     val univ_card = univ_card 0 0 0 bounds formula

   310   in

   311     {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],

   312      bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}

   313   end

   315 (* theory -> problem list -> string *)

   316 fun solve_any_kodkod_problem thy problems =

   317   let

   318     val {overlord, ...} = Nitpick_Isar.default_params thy []

   319     val max_threads = 1

   320     val max_solutions = 1

   321   in

   322     case solve_any_problem overlord NONE max_threads max_solutions problems of

   323       NotInstalled => "unknown"

   324     | Normal ([], _) => "none"

   325     | Normal _ => "genuine"

   326     | TimedOut _ => "unknown"

   327     | Interrupted _ => "unknown"

   328     | Error (s, _) => error ("Kodkod error: " ^ s)

   329   end

   331 end;

author	blanchet
	Mon, 22 Feb 2010 19:31:00 +0100
changeset 35284	9edc2bd6d2bd
parent 35280	54ab4921f826
child 35333	f61de25f71f9
permissions	-rw-r--r--