author | blanchet |
Tue, 09 Mar 2010 09:25:23 +0100 | |
changeset 35665 | ff2bf50505ab |
parent 35625 | 9c818cab0dd0 |
child 35699 | 9ed327529a44 |
permissions | -rw-r--r-- |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
1 |
(* Title: HOL/Tools/Nitpick/minipick.ML |
33192 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34124
diff
changeset
|
3 |
Copyright 2009, 2010 |
33192 | 4 |
|
5 |
Finite model generation for HOL formulas using Kodkod, minimalistic version. |
|
6 |
*) |
|
7 |
||
8 |
signature MINIPICK = |
|
9 |
sig |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
10 |
datatype rep = SRep | RRep |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
11 |
type styp = Nitpick_Util.styp |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
12 |
|
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
13 |
val vars_for_bound_var : |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
14 |
(typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
15 |
val rel_expr_for_bound_var : |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
16 |
(typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
17 |
val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
18 |
val false_atom : Kodkod.rel_expr |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
19 |
val true_atom : Kodkod.rel_expr |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
20 |
val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
21 |
val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr |
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
22 |
val kodkod_problem_from_term : |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
23 |
Proof.context -> (typ -> int) -> term -> Kodkod.problem |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
24 |
val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string |
33192 | 25 |
end; |
26 |
||
27 |
structure Minipick : MINIPICK = |
|
28 |
struct |
|
29 |
||
30 |
open Kodkod |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
31 |
open Nitpick_Util |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
32 |
open Nitpick_HOL |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
33 |
open Nitpick_Peephole |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
34 |
open Nitpick_Kodkod |
33192 | 35 |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
36 |
datatype rep = SRep | RRep |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
37 |
|
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
38 |
(* Proof.context -> typ -> unit *) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
39 |
fun check_type ctxt (Type (@{type_name fun}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
40 |
List.app (check_type ctxt) Ts |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
41 |
| check_type ctxt (Type (@{type_name "*"}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
42 |
List.app (check_type ctxt) Ts |
33192 | 43 |
| check_type _ @{typ bool} = () |
44 |
| check_type _ (TFree (_, @{sort "{}"})) = () |
|
45 |
| check_type _ (TFree (_, @{sort HOL.type})) = () |
|
46 |
| check_type ctxt T = |
|
47 |
raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T)) |
|
48 |
||
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
49 |
(* rep -> (typ -> int) -> typ -> int list *) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
50 |
fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) = |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
51 |
replicate_list (card T1) (atom_schema_of SRep card T2) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
52 |
| atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) = |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
53 |
atom_schema_of SRep card T1 |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
54 |
| atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) = |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
55 |
atom_schema_of SRep card T1 @ atom_schema_of RRep card T2 |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
56 |
| atom_schema_of _ card (Type (@{type_name "*"}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
57 |
maps (atom_schema_of SRep card) Ts |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
58 |
| atom_schema_of _ card T = [card T] |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
59 |
(* rep -> (typ -> int) -> typ -> int *) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
60 |
val arity_of = length ooo atom_schema_of |
33192 | 61 |
|
62 |
(* (typ -> int) -> typ list -> int -> int *) |
|
63 |
fun index_for_bound_var _ [_] 0 = 0 |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
64 |
| index_for_bound_var card (_ :: Ts) 0 = |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
65 |
index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
66 |
| index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
67 |
(* (typ -> int) -> rep -> typ list -> int -> rel_expr list *) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
68 |
fun vars_for_bound_var card R Ts j = |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
69 |
map (curry Var 1) (index_seq (index_for_bound_var card Ts j) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
70 |
(arity_of R card (nth Ts j))) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
71 |
(* (typ -> int) -> rep -> typ list -> int -> rel_expr *) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
72 |
val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
73 |
(* rep -> (typ -> int) -> typ list -> typ -> decl list *) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
74 |
fun decls_for R card Ts T = |
33192 | 75 |
map2 (curry DeclOne o pair 1) |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
76 |
(index_seq (index_for_bound_var card (T :: Ts) 0) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
77 |
(arity_of R card (nth (T :: Ts) 0))) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
78 |
(map (AtomSeq o rpair 0) (atom_schema_of R card T)) |
33192 | 79 |
|
80 |
(* int list -> rel_expr *) |
|
81 |
val atom_product = foldl1 Product o map Atom |
|
82 |
||
83 |
val false_atom = Atom 0 |
|
84 |
val true_atom = Atom 1 |
|
85 |
||
86 |
(* rel_expr -> formula *) |
|
87 |
fun formula_from_atom r = RelEq (r, true_atom) |
|
88 |
(* formula -> rel_expr *) |
|
89 |
fun atom_from_formula f = RelIf (f, true_atom, false_atom) |
|
90 |
||
91 |
(* Proof.context -> (typ -> int) -> styp list -> term -> formula *) |
|
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35028
diff
changeset
|
92 |
fun kodkod_formula_from_term ctxt card frees = |
33192 | 93 |
let |
94 |
(* typ -> rel_expr -> rel_expr *) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
95 |
fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r = |
33192 | 96 |
let |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
97 |
val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
33192 | 98 |
|> all_combinations |
99 |
in |
|
100 |
map2 (fn i => fn js => |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
101 |
RelIf (formula_from_atom (Project (r, [Num i])), |
33192 | 102 |
atom_product js, empty_n_ary_rel (length js))) |
103 |
(index_seq 0 (length jss)) jss |
|
104 |
|> foldl1 Union |
|
105 |
end |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
106 |
| R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r = |
33192 | 107 |
let |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
108 |
val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
33192 | 109 |
|> all_combinations |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
110 |
val arity2 = arity_of SRep card T2 |
33192 | 111 |
in |
112 |
map2 (fn i => fn js => |
|
113 |
Product (atom_product js, |
|
114 |
Project (r, num_seq (i * arity2) arity2) |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
115 |
|> R_rep_from_S_rep T2)) |
33192 | 116 |
(index_seq 0 (length jss)) jss |
117 |
|> foldl1 Union |
|
118 |
end |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
119 |
| R_rep_from_S_rep _ r = r |
33192 | 120 |
(* typ list -> typ -> rel_expr -> rel_expr *) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
121 |
fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r = |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
122 |
Comprehension (decls_for SRep card Ts T, |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
123 |
RelEq (R_rep_from_S_rep T |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
124 |
(rel_expr_for_bound_var card SRep (T :: Ts) 0), r)) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
125 |
| S_rep_from_R_rep _ _ r = r |
33192 | 126 |
(* typ list -> term -> formula *) |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
127 |
fun to_F Ts t = |
33192 | 128 |
(case t of |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
129 |
@{const Not} $ t1 => Not (to_F Ts t1) |
33192 | 130 |
| @{const False} => False |
131 |
| @{const True} => True |
|
132 |
| Const (@{const_name All}, _) $ Abs (s, T, t') => |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
133 |
All (decls_for SRep card Ts T, to_F (T :: Ts) t') |
33192 | 134 |
| (t0 as Const (@{const_name All}, _)) $ t1 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
135 |
to_F Ts (t0 $ eta_expand Ts t1 1) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35185
diff
changeset
|
136 |
| Const (@{const_name Ex}, _) $ Abs (_, T, t') => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
137 |
Exist (decls_for SRep card Ts T, to_F (T :: Ts) t') |
33192 | 138 |
| (t0 as Const (@{const_name Ex}, _)) $ t1 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
139 |
to_F Ts (t0 $ eta_expand Ts t1 1) |
33192 | 140 |
| Const (@{const_name "op ="}, _) $ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
141 |
RelEq (to_R_rep Ts t1, to_R_rep Ts t2) |
33192 | 142 |
| Const (@{const_name ord_class.less_eq}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
143 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
144 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
145 |
$ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
146 |
Subset (to_R_rep Ts t1, to_R_rep Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
147 |
| @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
148 |
| @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
149 |
| @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
150 |
| t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1) |
33192 | 151 |
| Free _ => raise SAME () |
152 |
| Term.Var _ => raise SAME () |
|
153 |
| Bound _ => raise SAME () |
|
154 |
| Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s) |
|
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35028
diff
changeset
|
155 |
| _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t])) |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
156 |
handle SAME () => formula_from_atom (to_R_rep Ts t) |
33192 | 157 |
(* typ list -> term -> rel_expr *) |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
158 |
and to_S_rep Ts t = |
33192 | 159 |
case t of |
160 |
Const (@{const_name Pair}, _) $ t1 $ t2 => |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
161 |
Product (to_S_rep Ts t1, to_S_rep Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
162 |
| Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
163 |
| Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2) |
33192 | 164 |
| Const (@{const_name fst}, _) $ t1 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
165 |
let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
166 |
Project (to_S_rep Ts t1, num_seq 0 fst_arity) |
33192 | 167 |
end |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
168 |
| Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1) |
33192 | 169 |
| Const (@{const_name snd}, _) $ t1 => |
170 |
let |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
171 |
val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1)) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
172 |
val snd_arity = arity_of SRep card (fastype_of1 (Ts, t)) |
33192 | 173 |
val fst_arity = pair_arity - snd_arity |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
174 |
in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
175 |
| Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
176 |
| Bound j => rel_expr_for_bound_var card SRep Ts j |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
177 |
| _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t) |
33192 | 178 |
(* term -> rel_expr *) |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
179 |
and to_R_rep Ts t = |
33192 | 180 |
(case t of |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
181 |
@{const Not} => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
182 |
| Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
183 |
| Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
184 |
| Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
185 |
| Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2) |
33192 | 186 |
| Const (@{const_name ord_class.less_eq}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
187 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
188 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
189 |
to_R_rep Ts (eta_expand Ts t 1) |
33192 | 190 |
| Const (@{const_name ord_class.less_eq}, _) => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
191 |
to_R_rep Ts (eta_expand Ts t 2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
192 |
| @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
193 |
| @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
194 |
| @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
195 |
| @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
196 |
| @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
197 |
| @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2) |
33192 | 198 |
| Const (@{const_name bot_class.bot}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
199 |
T as Type (@{type_name fun}, [_, @{typ bool}])) => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
200 |
empty_n_ary_rel (arity_of RRep card T) |
33192 | 201 |
| Const (@{const_name insert}, _) $ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
202 |
Union (to_S_rep Ts t1, to_R_rep Ts t2) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
203 |
| Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
204 |
| Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2) |
33192 | 205 |
| Const (@{const_name trancl}, _) $ t1 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
206 |
if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
207 |
Closure (to_R_rep Ts t1) |
33192 | 208 |
else |
209 |
raise NOT_SUPPORTED "transitive closure for function or pair type" |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
210 |
| Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
211 |
| Const (@{const_name semilattice_inf_class.inf}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
212 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
213 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
214 |
$ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
215 |
Intersect (to_R_rep Ts t1, to_R_rep Ts t2) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
216 |
| Const (@{const_name semilattice_inf_class.inf}, _) $ _ => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
217 |
to_R_rep Ts (eta_expand Ts t 1) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
218 |
| Const (@{const_name semilattice_inf_class.inf}, _) => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
219 |
to_R_rep Ts (eta_expand Ts t 2) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
220 |
| Const (@{const_name semilattice_sup_class.sup}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
221 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
222 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
223 |
$ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
224 |
Union (to_R_rep Ts t1, to_R_rep Ts t2) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
225 |
| Const (@{const_name semilattice_sup_class.sup}, _) $ _ => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
226 |
to_R_rep Ts (eta_expand Ts t 1) |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34982
diff
changeset
|
227 |
| Const (@{const_name semilattice_sup_class.sup}, _) => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
228 |
to_R_rep Ts (eta_expand Ts t 2) |
33192 | 229 |
| Const (@{const_name minus_class.minus}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
230 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
231 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
232 |
$ t1 $ t2 => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
233 |
Difference (to_R_rep Ts t1, to_R_rep Ts t2) |
33192 | 234 |
| Const (@{const_name minus_class.minus}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
235 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
236 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
237 |
to_R_rep Ts (eta_expand Ts t 1) |
33192 | 238 |
| Const (@{const_name minus_class.minus}, |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
239 |
Type (@{type_name fun}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
240 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) => |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
241 |
to_R_rep Ts (eta_expand Ts t 2) |
33192 | 242 |
| Const (@{const_name Pair}, _) $ _ $ _ => raise SAME () |
243 |
| Const (@{const_name Pair}, _) $ _ => raise SAME () |
|
244 |
| Const (@{const_name Pair}, _) => raise SAME () |
|
245 |
| Const (@{const_name fst}, _) $ _ => raise SAME () |
|
246 |
| Const (@{const_name fst}, _) => raise SAME () |
|
247 |
| Const (@{const_name snd}, _) $ _ => raise SAME () |
|
248 |
| Const (@{const_name snd}, _) => raise SAME () |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
249 |
| Const (_, @{typ bool}) => atom_from_formula (to_F Ts t) |
33192 | 250 |
| Free (x as (_, T)) => |
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33980
diff
changeset
|
251 |
Rel (arity_of RRep card T, find_index (curry (op =) x) frees) |
33192 | 252 |
| Term.Var _ => raise NOT_SUPPORTED "schematic variables" |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35185
diff
changeset
|
253 |
| Bound _ => raise SAME () |
33192 | 254 |
| Abs (_, T, t') => |
255 |
(case fastype_of1 (T :: Ts, t') of |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
256 |
@{typ bool} => Comprehension (decls_for SRep card Ts T, |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
257 |
to_F (T :: Ts) t') |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
258 |
| T' => Comprehension (decls_for SRep card Ts T @ |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
259 |
decls_for RRep card (T :: Ts) T', |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
260 |
Subset (rel_expr_for_bound_var card RRep |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
261 |
(T' :: T :: Ts) 0, |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
262 |
to_R_rep (T :: Ts) t'))) |
33192 | 263 |
| t1 $ t2 => |
264 |
(case fastype_of1 (Ts, t) of |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
265 |
@{typ bool} => atom_from_formula (to_F Ts t) |
33192 | 266 |
| T => |
267 |
let val T2 = fastype_of1 (Ts, t2) in |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
268 |
case arity_of SRep card T2 of |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
269 |
1 => Join (to_S_rep Ts t2, to_R_rep Ts t1) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35185
diff
changeset
|
270 |
| arity2 => |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35185
diff
changeset
|
271 |
let val res_arity = arity_of RRep card T in |
33192 | 272 |
Project (Intersect |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
273 |
(Product (to_S_rep Ts t2, |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
274 |
atom_schema_of RRep card T |
33192 | 275 |
|> map (AtomSeq o rpair 0) |> foldl1 Product), |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
276 |
to_R_rep Ts t1), |
33192 | 277 |
num_seq arity2 res_arity) |
278 |
end |
|
279 |
end) |
|
280 |
| _ => raise NOT_SUPPORTED ("term " ^ |
|
281 |
quote (Syntax.string_of_term ctxt t))) |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
282 |
handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
283 |
in to_F [] end |
33192 | 284 |
|
285 |
(* (typ -> int) -> int -> styp -> bound *) |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
286 |
fun bound_for_free card i (s, T) = |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
287 |
let val js = atom_schema_of RRep card T in |
33192 | 288 |
([((length js, i), s)], |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
289 |
[TupleSet [], atom_schema_of RRep card T |> map (rpair 0) |
33192 | 290 |
|> tuple_set_from_atom_schema]) |
291 |
end |
|
292 |
||
293 |
(* (typ -> int) -> typ list -> typ -> rel_expr -> formula *) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
294 |
fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2])) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
295 |
r = |
33192 | 296 |
if body_type T2 = bool_T then |
297 |
True |
|
298 |
else |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
299 |
All (decls_for SRep card Ts T1, |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
300 |
declarative_axiom_for_rel_expr card (T1 :: Ts) T2 |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
301 |
(List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0))) |
33192 | 302 |
| declarative_axiom_for_rel_expr _ _ _ r = One r |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
303 |
(* (typ -> int) -> bool -> int -> styp -> formula *) |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
304 |
fun declarative_axiom_for_free card i (_, T) = |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
305 |
declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i)) |
33192 | 306 |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
307 |
(* Proof.context -> (typ -> int) -> term -> problem *) |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
308 |
fun kodkod_problem_from_term ctxt raw_card t = |
33192 | 309 |
let |
310 |
val thy = ProofContext.theory_of ctxt |
|
311 |
(* typ -> int *) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
312 |
fun card (Type (@{type_name fun}, [T1, T2])) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
313 |
reasonable_power (card T2) (card T1) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35625
diff
changeset
|
314 |
| card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2 |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
315 |
| card @{typ bool} = 2 |
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
316 |
| card T = Int.max (1, raw_card T) |
35625 | 317 |
val neg_t = @{const Not} $ Object_Logic.atomize_term thy t |
33192 | 318 |
val _ = fold_types (K o check_type ctxt) neg_t () |
319 |
val frees = Term.add_frees neg_t [] |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
320 |
val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees |
33192 | 321 |
val declarative_axioms = |
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
322 |
map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees |
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35028
diff
changeset
|
323 |
val formula = kodkod_formula_from_term ctxt card frees neg_t |
33192 | 324 |
|> fold_rev (curry And) declarative_axioms |
325 |
val univ_card = univ_card 0 0 0 bounds formula |
|
326 |
in |
|
35284
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
327 |
{comment = "", settings = [], univ_card = univ_card, tuple_assigns = [], |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
328 |
bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula} |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
329 |
end |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
330 |
|
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
331 |
(* theory -> problem list -> string *) |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
332 |
fun solve_any_kodkod_problem thy problems = |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
333 |
let |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
334 |
val {overlord, ...} = Nitpick_Isar.default_params thy [] |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
335 |
val max_threads = 1 |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
336 |
val max_solutions = 1 |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
337 |
in |
9edc2bd6d2bd
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
blanchet
parents:
35280
diff
changeset
|
338 |
case solve_any_problem overlord NONE max_threads max_solutions problems of |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
339 |
NotInstalled => "unknown" |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35284
diff
changeset
|
340 |
| Normal ([], _, _) => "none" |
33192 | 341 |
| Normal _ => "genuine" |
342 |
| TimedOut _ => "unknown" |
|
343 |
| Interrupted _ => "unknown" |
|
344 |
| Error (s, _) => error ("Kodkod error: " ^ s) |
|
345 |
end |
|
33980
a28733ef3a82
export symbols from Minipick (so I can use them in other programs)
blanchet
parents:
33232
diff
changeset
|
346 |
|
33192 | 347 |
end; |