34 open Nitpick_Kodkod |
34 open Nitpick_Kodkod |
35 |
35 |
36 datatype rep = SRep | RRep |
36 datatype rep = SRep | RRep |
37 |
37 |
38 (* Proof.context -> typ -> unit *) |
38 (* Proof.context -> typ -> unit *) |
39 fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts |
39 fun check_type ctxt (Type (@{type_name fun}, Ts)) = |
40 | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts |
40 List.app (check_type ctxt) Ts |
|
41 | check_type ctxt (Type (@{type_name "*"}, Ts)) = |
|
42 List.app (check_type ctxt) Ts |
41 | check_type _ @{typ bool} = () |
43 | check_type _ @{typ bool} = () |
42 | check_type _ (TFree (_, @{sort "{}"})) = () |
44 | check_type _ (TFree (_, @{sort "{}"})) = () |
43 | check_type _ (TFree (_, @{sort HOL.type})) = () |
45 | check_type _ (TFree (_, @{sort HOL.type})) = () |
44 | check_type ctxt T = |
46 | check_type ctxt T = |
45 raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T)) |
47 raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T)) |
46 |
48 |
47 (* rep -> (typ -> int) -> typ -> int list *) |
49 (* rep -> (typ -> int) -> typ -> int list *) |
48 fun atom_schema_of SRep card (Type ("fun", [T1, T2])) = |
50 fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) = |
49 replicate_list (card T1) (atom_schema_of SRep card T2) |
51 replicate_list (card T1) (atom_schema_of SRep card T2) |
50 | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) = |
52 | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) = |
51 atom_schema_of SRep card T1 |
53 atom_schema_of SRep card T1 |
52 | atom_schema_of RRep card (Type ("fun", [T1, T2])) = |
54 | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) = |
53 atom_schema_of SRep card T1 @ atom_schema_of RRep card T2 |
55 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 |
56 | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) = |
|
57 maps (atom_schema_of SRep card) Ts |
55 | atom_schema_of _ card T = [card T] |
58 | atom_schema_of _ card T = [card T] |
56 (* rep -> (typ -> int) -> typ -> int *) |
59 (* rep -> (typ -> int) -> typ -> int *) |
57 val arity_of = length ooo atom_schema_of |
60 val arity_of = length ooo atom_schema_of |
58 |
61 |
59 (* (typ -> int) -> typ list -> int -> int *) |
62 (* (typ -> int) -> typ list -> int -> int *) |
87 |
90 |
88 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *) |
91 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *) |
89 fun kodkod_formula_from_term ctxt card frees = |
92 fun kodkod_formula_from_term ctxt card frees = |
90 let |
93 let |
91 (* typ -> rel_expr -> rel_expr *) |
94 (* typ -> rel_expr -> rel_expr *) |
92 fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r = |
95 fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r = |
93 let |
96 let |
94 val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
97 val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
95 |> all_combinations |
98 |> all_combinations |
96 in |
99 in |
97 map2 (fn i => fn js => |
100 map2 (fn i => fn js => |
98 RelIf (formula_from_atom (Project (r, [Num i])), |
101 RelIf (formula_from_atom (Project (r, [Num i])), |
99 atom_product js, empty_n_ary_rel (length js))) |
102 atom_product js, empty_n_ary_rel (length js))) |
100 (index_seq 0 (length jss)) jss |
103 (index_seq 0 (length jss)) jss |
101 |> foldl1 Union |
104 |> foldl1 Union |
102 end |
105 end |
103 | R_rep_from_S_rep (Type ("fun", [T1, T2])) r = |
106 | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r = |
104 let |
107 let |
105 val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
108 val jss = atom_schema_of SRep card T1 |> map (rpair 0) |
106 |> all_combinations |
109 |> all_combinations |
107 val arity2 = arity_of SRep card T2 |
110 val arity2 = arity_of SRep card T2 |
108 in |
111 in |
113 (index_seq 0 (length jss)) jss |
116 (index_seq 0 (length jss)) jss |
114 |> foldl1 Union |
117 |> foldl1 Union |
115 end |
118 end |
116 | R_rep_from_S_rep _ r = r |
119 | R_rep_from_S_rep _ r = r |
117 (* typ list -> typ -> rel_expr -> rel_expr *) |
120 (* typ list -> typ -> rel_expr -> rel_expr *) |
118 fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r = |
121 fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r = |
119 Comprehension (decls_for SRep card Ts T, |
122 Comprehension (decls_for SRep card Ts T, |
120 RelEq (R_rep_from_S_rep T |
123 RelEq (R_rep_from_S_rep T |
121 (rel_expr_for_bound_var card SRep (T :: Ts) 0), r)) |
124 (rel_expr_for_bound_var card SRep (T :: Ts) 0), r)) |
122 | S_rep_from_R_rep _ _ r = r |
125 | S_rep_from_R_rep _ _ r = r |
123 (* typ list -> term -> formula *) |
126 (* typ list -> term -> formula *) |
135 | (t0 as Const (@{const_name Ex}, _)) $ t1 => |
138 | (t0 as Const (@{const_name Ex}, _)) $ t1 => |
136 to_F Ts (t0 $ eta_expand Ts t1 1) |
139 to_F Ts (t0 $ eta_expand Ts t1 1) |
137 | Const (@{const_name "op ="}, _) $ t1 $ t2 => |
140 | Const (@{const_name "op ="}, _) $ t1 $ t2 => |
138 RelEq (to_R_rep Ts t1, to_R_rep Ts t2) |
141 RelEq (to_R_rep Ts t1, to_R_rep Ts t2) |
139 | Const (@{const_name ord_class.less_eq}, |
142 | Const (@{const_name ord_class.less_eq}, |
140 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => |
143 Type (@{type_name fun}, |
|
144 [Type (@{type_name fun}, [_, @{typ bool}]), _])) |
|
145 $ t1 $ t2 => |
141 Subset (to_R_rep Ts t1, to_R_rep Ts t2) |
146 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) |
147 | @{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) |
148 | @{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) |
149 | @{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) |
150 | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1) |
177 | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1) |
182 | 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) |
183 | 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) |
184 | 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) |
185 | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2) |
181 | Const (@{const_name ord_class.less_eq}, |
186 | Const (@{const_name ord_class.less_eq}, |
182 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ => |
187 Type (@{type_name fun}, |
|
188 [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ => |
183 to_R_rep Ts (eta_expand Ts t 1) |
189 to_R_rep Ts (eta_expand Ts t 1) |
184 | Const (@{const_name ord_class.less_eq}, _) => |
190 | Const (@{const_name ord_class.less_eq}, _) => |
185 to_R_rep Ts (eta_expand Ts t 2) |
191 to_R_rep Ts (eta_expand Ts t 2) |
186 | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
192 | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
187 | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2) |
193 | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2) |
188 | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
194 | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
189 | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2) |
195 | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2) |
190 | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
196 | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1) |
191 | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2) |
197 | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2) |
192 | Const (@{const_name bot_class.bot}, |
198 | Const (@{const_name bot_class.bot}, |
193 T as Type ("fun", [_, @{typ bool}])) => |
199 T as Type (@{type_name fun}, [_, @{typ bool}])) => |
194 empty_n_ary_rel (arity_of RRep card T) |
200 empty_n_ary_rel (arity_of RRep card T) |
195 | Const (@{const_name insert}, _) $ t1 $ t2 => |
201 | Const (@{const_name insert}, _) $ t1 $ t2 => |
196 Union (to_S_rep Ts t1, to_R_rep Ts t2) |
202 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) |
203 | 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) |
204 | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2) |
201 Closure (to_R_rep Ts t1) |
207 Closure (to_R_rep Ts t1) |
202 else |
208 else |
203 raise NOT_SUPPORTED "transitive closure for function or pair type" |
209 raise NOT_SUPPORTED "transitive closure for function or pair type" |
204 | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1) |
210 | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1) |
205 | Const (@{const_name semilattice_inf_class.inf}, |
211 | Const (@{const_name semilattice_inf_class.inf}, |
206 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => |
212 Type (@{type_name fun}, |
|
213 [Type (@{type_name fun}, [_, @{typ bool}]), _])) |
|
214 $ t1 $ t2 => |
207 Intersect (to_R_rep Ts t1, to_R_rep Ts t2) |
215 Intersect (to_R_rep Ts t1, to_R_rep Ts t2) |
208 | Const (@{const_name semilattice_inf_class.inf}, _) $ _ => |
216 | Const (@{const_name semilattice_inf_class.inf}, _) $ _ => |
209 to_R_rep Ts (eta_expand Ts t 1) |
217 to_R_rep Ts (eta_expand Ts t 1) |
210 | Const (@{const_name semilattice_inf_class.inf}, _) => |
218 | Const (@{const_name semilattice_inf_class.inf}, _) => |
211 to_R_rep Ts (eta_expand Ts t 2) |
219 to_R_rep Ts (eta_expand Ts t 2) |
212 | Const (@{const_name semilattice_sup_class.sup}, |
220 | Const (@{const_name semilattice_sup_class.sup}, |
213 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => |
221 Type (@{type_name fun}, |
|
222 [Type (@{type_name fun}, [_, @{typ bool}]), _])) |
|
223 $ t1 $ t2 => |
214 Union (to_R_rep Ts t1, to_R_rep Ts t2) |
224 Union (to_R_rep Ts t1, to_R_rep Ts t2) |
215 | Const (@{const_name semilattice_sup_class.sup}, _) $ _ => |
225 | Const (@{const_name semilattice_sup_class.sup}, _) $ _ => |
216 to_R_rep Ts (eta_expand Ts t 1) |
226 to_R_rep Ts (eta_expand Ts t 1) |
217 | Const (@{const_name semilattice_sup_class.sup}, _) => |
227 | Const (@{const_name semilattice_sup_class.sup}, _) => |
218 to_R_rep Ts (eta_expand Ts t 2) |
228 to_R_rep Ts (eta_expand Ts t 2) |
219 | Const (@{const_name minus_class.minus}, |
229 | Const (@{const_name minus_class.minus}, |
220 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 => |
230 Type (@{type_name fun}, |
|
231 [Type (@{type_name fun}, [_, @{typ bool}]), _])) |
|
232 $ t1 $ t2 => |
221 Difference (to_R_rep Ts t1, to_R_rep Ts t2) |
233 Difference (to_R_rep Ts t1, to_R_rep Ts t2) |
222 | Const (@{const_name minus_class.minus}, |
234 | Const (@{const_name minus_class.minus}, |
223 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ => |
235 Type (@{type_name fun}, |
|
236 [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ => |
224 to_R_rep Ts (eta_expand Ts t 1) |
237 to_R_rep Ts (eta_expand Ts t 1) |
225 | Const (@{const_name minus_class.minus}, |
238 | Const (@{const_name minus_class.minus}, |
226 Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) => |
239 Type (@{type_name fun}, |
|
240 [Type (@{type_name fun}, [_, @{typ bool}]), _])) => |
227 to_R_rep Ts (eta_expand Ts t 2) |
241 to_R_rep Ts (eta_expand Ts t 2) |
228 | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME () |
242 | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME () |
229 | Const (@{const_name Pair}, _) $ _ => raise SAME () |
243 | Const (@{const_name Pair}, _) $ _ => raise SAME () |
230 | Const (@{const_name Pair}, _) => raise SAME () |
244 | Const (@{const_name Pair}, _) => raise SAME () |
231 | Const (@{const_name fst}, _) $ _ => raise SAME () |
245 | Const (@{const_name fst}, _) $ _ => raise SAME () |
292 (* Proof.context -> (typ -> int) -> term -> problem *) |
307 (* Proof.context -> (typ -> int) -> term -> problem *) |
293 fun kodkod_problem_from_term ctxt raw_card t = |
308 fun kodkod_problem_from_term ctxt raw_card t = |
294 let |
309 let |
295 val thy = ProofContext.theory_of ctxt |
310 val thy = ProofContext.theory_of ctxt |
296 (* typ -> int *) |
311 (* typ -> int *) |
297 fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1) |
312 fun card (Type (@{type_name fun}, [T1, T2])) = |
298 | card (Type ("*", [T1, T2])) = card T1 * card T2 |
313 reasonable_power (card T2) (card T1) |
|
314 | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2 |
299 | card @{typ bool} = 2 |
315 | card @{typ bool} = 2 |
300 | card T = Int.max (1, raw_card T) |
316 | card T = Int.max (1, raw_card T) |
301 val neg_t = @{const Not} $ Object_Logic.atomize_term thy t |
317 val neg_t = @{const Not} $ Object_Logic.atomize_term thy t |
302 val _ = fold_types (K o check_type ctxt) neg_t () |
318 val _ = fold_types (K o check_type ctxt) neg_t () |
303 val frees = Term.add_frees neg_t [] |
319 val frees = Term.add_frees neg_t [] |