--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 14:11:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 20:46:50 2010 +0100
@@ -33,7 +33,7 @@
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- hol_context -> int -> int Typtab.table -> kodkod_constrs
+ hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
@@ -742,12 +742,14 @@
(* nut NameTable.table -> styp -> KK.rel_expr *)
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> styp -> int -> nfa_transition list *)
-fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
- rel_table (dtypes : dtype_spec list) constr_x n =
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> styp -> int -> nfa_transition list *)
+fun nfa_transitions_for_sel hol_ctxt binarize
+ ({kk_project, ...} : kodkod_constrs) rel_table
+ (dtypes : dtype_spec list) constr_x n =
let
- val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
+ val x as (_, T) =
+ binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
val (r, R, arity) = const_triple rel_table x
val type_schema = type_schema_of_rep T R
in
@@ -756,19 +758,21 @@
else SOME (kk_project r (map KK.Num [0, j]), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> styp -> nfa_transition list *)
-fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
- maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> styp -> nfa_transition list *)
+fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
+ (x as (_, T)) =
+ maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> dtype_spec -> nfa_entry option *)
-fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
- | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
- SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
- o #const) constrs)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> dtype_spec -> nfa_entry option *)
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
+ | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
+ {typ, constrs, ...} =
+ SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
+ dtypes o #const) constrs)
val empty_rel = KK.Product (KK.None, KK.None)
@@ -825,23 +829,25 @@
fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
- -> KK.formula list *)
-fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
- map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+ -> dtype_spec list -> KK.formula list *)
+fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
+ map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
+ dtypes
|> strongly_connected_sub_nfas
|> maps (fn nfa =>
map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
-(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
- -> constr_spec -> int -> KK.formula *)
-fun sel_axiom_for_sel hol_ctxt j0
+(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
+ -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
+fun sel_axiom_for_sel hol_ctxt binarize j0
(kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
kk_join, ...}) rel_table dom_r
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
n =
let
- val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
+ val x as (_, T) =
+ binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
val (r, R, arity) = const_triple rel_table x
val R2 = dest_Func R |> snd
val z = (epsilon - delta, delta + j0)
@@ -855,9 +861,9 @@
(kk_n_ary_function kk R2 r') (kk_no r'))
end
end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
-> constr_spec -> KK.formula list *)
-fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
val honors_explicit_max =
@@ -879,19 +885,19 @@
" too small for \"max\"")
in
max_axiom ::
- map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
+ map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> KK.formula list *)
-fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
- maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
+ maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
-> KK.formula list *)
-fun uniqueness_axiom_for_constr hol_ctxt
+fun uniqueness_axiom_for_constr hol_ctxt binarize
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
: kodkod_constrs) rel_table ({const, ...} : constr_spec) =
let
@@ -899,9 +905,10 @@
fun conjunct_for_sel r =
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
val num_sels = num_sels_for_constr_type (snd const)
- val triples = map (const_triple rel_table
- o boxed_nth_sel_for_constr hol_ctxt const)
- (~1 upto num_sels - 1)
+ val triples =
+ map (const_triple rel_table
+ o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
+ (~1 upto num_sels - 1)
val j0 = case triples |> hd |> #2 of
Func (Atom (_, j0), _) => j0
| R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
@@ -916,11 +923,11 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
-> KK.formula list *)
-fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
({constrs, ...} : dtype_spec) =
- map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
+ map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
(* constr_spec -> int *)
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
@@ -937,22 +944,24 @@
kk_disjoint_sets kk rs]
end
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec -> KK.formula list *)
-fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
+fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
+ | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
(dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
+ sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> KK.formula list *)
-fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
- acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
- maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
+fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
+ dtypes =
+ acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
+ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+ dtypes
(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut bits ofs