--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 21 15:45:44 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 21 16:33:21 2011 +0100
@@ -29,13 +29,13 @@
val bound_for_sel_rel :
Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
+ val kodkod_formula_from_nut :
+ int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
hol_context -> bool -> nut list -> int -> int -> int Typtab.table
-> kodkod_constrs -> nut NameTable.table -> datatype_spec list
-> Kodkod.formula list
- val kodkod_formula_from_nut :
- int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -647,416 +647,6 @@
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
(KK.Bits i))
-fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
- kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
- (KK.Rel x)
- | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
- (FreeRel (x, _, R, _)) =
- if is_one_rep R then kk_one (KK.Rel x)
- else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
- else KK.True
- | declarative_axiom_for_plain_rel _ u =
- raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
-
-fun const_triple rel_table (x as (s, T)) =
- case the_name rel_table (ConstName (s, T, Any)) of
- FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
- | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
-
-fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-
-fun nfa_transitions_for_sel hol_ctxt binarize
- ({kk_project, ...} : kodkod_constrs) rel_table
- (dtypes : datatype_spec list) constr_x n =
- let
- 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
- map_filter (fn (j, T) =>
- if forall (not_equal T o #typ) dtypes then NONE
- else SOME ((x, kk_project r (map KK.Num [0, j])), T))
- (index_seq 1 (arity - 1) ~~ tl type_schema)
- end
-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))
-fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_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)
-
-fun direct_path_rel_exprs nfa start_T final_T =
- case AList.lookup (op =) nfa final_T of
- SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
- | NONE => []
-and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
- final_T =
- fold kk_union (direct_path_rel_exprs nfa start_T final_T)
- (if start_T = final_T then KK.Iden else empty_rel)
- | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
- kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
- (knot_path_rel_expr kk nfa Ts start_T T final_T)
-and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
- start_T knot_T final_T =
- kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
- (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
- (any_path_rel_expr kk nfa Ts start_T knot_T)
-and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
- fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
- | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
- start_T =
- if start_T = T then
- kk_closure (loop_path_rel_expr kk nfa Ts start_T)
- else
- kk_union (loop_path_rel_expr kk nfa Ts start_T)
- (knot_path_rel_expr kk nfa Ts start_T T start_T)
-
-fun add_nfa_to_graph [] = I
- | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
- | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
- add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
- Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
-
-fun strongly_connected_sub_nfas nfa =
- add_nfa_to_graph nfa Typ_Graph.empty
- |> Typ_Graph.strong_conn
- |> map (fn keys => filter (member (op =) keys o fst) nfa)
-
-fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
- start_T =
- kk_no (kk_intersect
- (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
- KK.Iden)
-(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
- the first equation. *)
-fun acyclicity_axioms_for_datatypes _ [_] = []
- | acyclicity_axioms_for_datatypes kk nfas =
- maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
-
-fun needed_value_axioms_for_datatype [] _ _ = []
- | needed_value_axioms_for_datatype needed_us ofs
- ({typ, card, constrs, ...} : datatype_spec) =
- let
- fun aux (u as Construct (ConstName (s, _, _) :: _, T, _, us)) =
- fold aux us
- #> (fn NONE => NONE
- | accum as SOME (loose, fixed) =>
- if T = typ then
- case AList.lookup (op =) fixed u of
- SOME _ => accum
- | NONE =>
- let
- val constr_s = constr_name_for_sel_like s
- val {delta, epsilon, ...} =
- constrs
- |> List.find (fn {const, ...} => fst const = constr_s)
- |> the
- val j0 = offset_of_type ofs T
- in
- case find_first (fn j => j >= delta andalso
- j < delta + epsilon) loose of
- SOME j =>
- SOME (remove (op =) j loose, (u, j0 + j) :: fixed)
- | NONE => NONE
- end
- else
- accum)
- | aux u =
- raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
- in
- case SOME (index_seq 0 card, []) |> fold aux needed_us of
- SOME (_, fixed) =>
- (* fixed |> map () *) [] (*###*)
- | NONE => [KK.False]
- end
-
-fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
- kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
-fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
- kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
-
-fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
- (delta, (epsilon, (num_binder_types T, s)))
-val constr_ord =
- prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
- o pairself constr_quadruple
-
-fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
- {card = card2, self_rec = self_rec2, constrs = constr2, ...})
- : datatype_spec * datatype_spec) =
- prod_ord int_ord (prod_ord bool_ord int_ord)
- ((card1, (self_rec1, length constr1)),
- (card2, (self_rec2, length constr2)))
-
-(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
- break cycles; otherwise, we may end up with two incompatible symmetry
- breaking orders, leading to spurious models. *)
-fun should_tabulate_suc_for_type dtypes T =
- is_asymmetric_nondatatype T orelse
- case datatype_spec dtypes T of
- SOME {self_rec, ...} => self_rec
- | NONE => false
-
-fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
- dtypes sel_quadruples =
- case sel_quadruples of
- [] => KK.True
- | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
- let val z = (x, should_tabulate_suc_for_type dtypes T) in
- if null sel_quadruples' then
- gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
- else
- kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
- (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
- (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
- (kk_join (KK.Var (1, 0)) r))
- (lex_order_rel_expr kk dtypes sel_quadruples'))
- end
- (* Skip constructors components that aren't atoms, since we cannot compare
- these easily. *)
- | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
-
-fun is_nil_like_constr_type dtypes T =
- case datatype_spec dtypes T of
- SOME {constrs, ...} =>
- (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
- [{const = (_, T'), ...}] => T = T'
- | _ => false)
- | NONE => false
-
-fun sym_break_axioms_for_constr_pair hol_ctxt binarize
- (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
- kk_join, ...}) rel_table nfas dtypes
- (constr_ord,
- ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
- {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
- : constr_spec * constr_spec) =
- let
- val dataT = body_type T1
- val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
- val rec_Ts = nfa |> map fst
- fun rec_and_nonrec_sels (x as (_, T)) =
- index_seq 0 (num_sels_for_constr_type T)
- |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
- |> List.partition (member (op =) rec_Ts o range_type o snd)
- val sel_xs1 = rec_and_nonrec_sels const1 |> op @
- in
- if constr_ord = EQUAL andalso null sel_xs1 then
- []
- else
- let
- val z =
- (case #2 (const_triple rel_table (discr_for_constr const1)) of
- Func (Atom x, Formula _) => x
- | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
- [R]), should_tabulate_suc_for_type dtypes dataT)
- val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
- val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
- fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
- (* If the two constructors are the same, we drop the first selector
- because that one is always checked by the lexicographic order.
- We sometimes also filter out direct subterms, because those are
- already handled by the acyclicity breaking in the bound
- declarations. *)
- fun filter_out_sels no_direct sel_xs =
- apsnd (filter_out
- (fn ((x, _), T) =>
- (constr_ord = EQUAL andalso x = hd sel_xs) orelse
- (T = dataT andalso
- (no_direct orelse not (member (op =) sel_xs x)))))
- fun subterms_r no_direct sel_xs j =
- loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
- (filter_out (curry (op =) dataT) (map fst nfa)) dataT
- |> kk_join (KK.Var (1, j))
- in
- [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
- KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
- (kk_implies
- (if delta2 >= epsilon1 then KK.True
- else if delta1 >= epsilon2 - 1 then KK.False
- else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
- (kk_or
- (if is_nil_like_constr_type dtypes T1 then
- KK.True
- else
- kk_some (kk_intersect (subterms_r false sel_xs2 1)
- (all_ge kk z (KK.Var (1, 0)))))
- (case constr_ord of
- EQUAL =>
- kk_and
- (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
- (kk_all [KK.DeclOne ((1, 2),
- subterms_r true sel_xs1 0)]
- (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
- | LESS =>
- kk_all [KK.DeclOne ((1, 2),
- subterms_r false sel_xs1 0)]
- (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
- | GREATER => KK.False)))]
- end
- end
-
-fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
- ({constrs, ...} : datatype_spec) =
- let
- val constrs = sort constr_ord constrs
- val constr_pairs = all_distinct_unordered_pairs_of constrs
- in
- map (pair EQUAL) (constrs ~~ constrs) @
- map (pair LESS) constr_pairs @
- map (pair GREATER) (map swap constr_pairs)
- |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
- nfas dtypes)
- end
-
-fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
- T = T' orelse exists (is_datatype_in_needed_value T) us
- | is_datatype_in_needed_value _ _ = false
-
-val min_sym_break_card = 7
-
-fun sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
- datatype_sym_break kk rel_table nfas dtypes =
- if datatype_sym_break = 0 then
- []
- else
- maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
- dtypes)
- (dtypes |> filter is_datatype_acyclic
- |> filter (fn {constrs = [_], ...} => false
- | {card, constrs, ...} =>
- card >= min_sym_break_card andalso
- forall (forall (not o is_higher_order_type)
- o binder_types o snd o #const) constrs)
- |> filter_out (fn {typ, ...} =>
- exists (is_datatype_in_needed_value typ)
- needed_us)
- |> (fn dtypes' =>
- dtypes'
- |> length dtypes' > datatype_sym_break
- ? (sort (datatype_ord o swap)
- #> take datatype_sym_break)))
-
-fun sel_axiom_for_sel hol_ctxt binarize j0
- (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
- rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
- n =
- let
- val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
- val (r, R, _) = const_triple rel_table x
- val R2 = dest_Func R |> snd
- val z = (epsilon - delta, delta + j0)
- in
- if exclusive then
- kk_n_ary_function kk (Func (Atom z, R2)) r
- else
- let val r' = kk_join (KK.Var (1, 0)) r in
- kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
- (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
- (kk_n_ary_function kk R2 r') (kk_no r'))
- end
- end
-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 =
- explicit_max < 0 orelse epsilon - delta <= explicit_max
- in
- if explicit_max = 0 then
- [formula_for_bool honors_explicit_max]
- else
- let
- val dom_r = discr_rel_expr rel_table const
- val max_axiom =
- if honors_explicit_max then
- KK.True
- else if bits = 0 orelse
- is_twos_complement_representable bits (epsilon - delta) then
- KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
- else
- raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
- "\"bits\" value " ^ string_of_int bits ^
- " too small for \"max\"")
- in
- max_axiom ::
- 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
-fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
- ({constrs, ...} : datatype_spec) =
- maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
-
-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
- 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 binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
- (~1 upto num_sels - 1)
- val set_r = triples |> hd |> #1
- in
- if num_sels = 0 then
- kk_lone set_r
- else
- kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
- (kk_implies
- (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
- (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
- end
-fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
- ({constrs, ...} : datatype_spec) =
- map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
-
-fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
-fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
- rel_table
- ({card, constrs, ...} : datatype_spec) =
- if forall #exclusive constrs then
- [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
- else
- let val rs = map (discr_rel_expr rel_table o #const) constrs in
- [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
- kk_disjoint_sets kk rs]
- end
-
-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 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
-
-fun declarative_axioms_for_datatypes hol_ctxt binarize needed_us
- datatype_sym_break bits ofs kk rel_table dtypes =
- let
- val nfas =
- dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
- rel_table dtypes)
- |> strongly_connected_sub_nfas
- in
- acyclicity_axioms_for_datatypes kk nfas @
- maps (needed_value_axioms_for_datatype needed_us ofs) dtypes @
- sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
- datatype_sym_break kk rel_table nfas dtypes @
- maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
- dtypes
- end
-
fun kodkod_formula_from_nut ofs
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
@@ -1785,4 +1375,422 @@
r
in to_f_with_polarity Pos u end
+fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
+ kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
+ (KK.Rel x)
+ | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
+ (FreeRel (x, _, R, _)) =
+ if is_one_rep R then kk_one (KK.Rel x)
+ else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
+ else KK.True
+ | declarative_axiom_for_plain_rel _ u =
+ raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
+
+fun const_triple rel_table (x as (s, T)) =
+ case the_name rel_table (ConstName (s, T, Any)) of
+ FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
+ | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
+
+fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
+
+fun nfa_transitions_for_sel hol_ctxt binarize
+ ({kk_project, ...} : kodkod_constrs) rel_table
+ (dtypes : datatype_spec list) constr_x n =
+ let
+ 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
+ map_filter (fn (j, T) =>
+ if forall (not_equal T o #typ) dtypes then NONE
+ else SOME ((x, kk_project r (map KK.Num [0, j])), T))
+ (index_seq 1 (arity - 1) ~~ tl type_schema)
+ end
+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))
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_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)
+
+fun direct_path_rel_exprs nfa start_T final_T =
+ case AList.lookup (op =) nfa final_T of
+ SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
+ | NONE => []
+and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
+ final_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T final_T)
+ (if start_T = final_T then KK.Iden else empty_rel)
+ | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
+ kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
+ (knot_path_rel_expr kk nfa Ts start_T T final_T)
+and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
+ start_T knot_T final_T =
+ kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
+ (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
+ (any_path_rel_expr kk nfa Ts start_T knot_T)
+and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
+ | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
+ start_T =
+ if start_T = T then
+ kk_closure (loop_path_rel_expr kk nfa Ts start_T)
+ else
+ kk_union (loop_path_rel_expr kk nfa Ts start_T)
+ (knot_path_rel_expr kk nfa Ts start_T T start_T)
+
+fun add_nfa_to_graph [] = I
+ | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
+ | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
+ add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
+ Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
+
+fun strongly_connected_sub_nfas nfa =
+ add_nfa_to_graph nfa Typ_Graph.empty
+ |> Typ_Graph.strong_conn
+ |> map (fn keys => filter (member (op =) keys o fst) nfa)
+
+fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
+ start_T =
+ kk_no (kk_intersect
+ (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
+ KK.Iden)
+(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
+ the first equation. *)
+fun acyclicity_axioms_for_datatypes _ [_] = []
+ | acyclicity_axioms_for_datatypes kk nfas =
+ maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
+
+fun atom_equation_for_nut ofs kk (u, j) =
+ let val dummy_u = RelReg (0, type_of u, rep_of u) in
+ case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u)
+ |> kodkod_formula_from_nut ofs kk of
+ KK.RelEq (KK.RelReg _, r) => KK.RelEq (KK.Atom j, r)
+ | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut",
+ "malformed Kodkod formula")
+ end
+
+fun needed_value_axioms_for_datatype [] _ _ _ = []
+ | needed_value_axioms_for_datatype needed_us ofs kk
+ ({typ, card, constrs, ...} : datatype_spec) =
+ let
+ fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
+ fold aux us
+ #> (fn NONE => NONE
+ | accum as SOME (loose, fixed) =>
+ if T = typ then
+ case AList.lookup (op =) fixed u of
+ SOME _ => accum
+ | NONE =>
+ let
+ val constr_s = constr_name_for_sel_like s
+ val {delta, epsilon, ...} =
+ constrs
+ |> List.find (fn {const, ...} => fst const = constr_s)
+ |> the
+ val j0 = offset_of_type ofs T
+ in
+ case find_first (fn j => j >= delta andalso
+ j < delta + epsilon) loose of
+ SOME j =>
+ SOME (remove (op =) j loose, (u, j0 + j) :: fixed)
+ | NONE => NONE
+ end
+ else
+ accum)
+ | aux u =
+ raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
+ in
+ case SOME (index_seq 0 card, []) |> fold aux needed_us of
+ SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
+ | NONE => [KK.False]
+ end
+
+fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
+ kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
+fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
+ kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
+
+fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
+ (delta, (epsilon, (num_binder_types T, s)))
+val constr_ord =
+ prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
+ o pairself constr_quadruple
+
+fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
+ {card = card2, self_rec = self_rec2, constrs = constr2, ...})
+ : datatype_spec * datatype_spec) =
+ prod_ord int_ord (prod_ord bool_ord int_ord)
+ ((card1, (self_rec1, length constr1)),
+ (card2, (self_rec2, length constr2)))
+
+(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
+ break cycles; otherwise, we may end up with two incompatible symmetry
+ breaking orders, leading to spurious models. *)
+fun should_tabulate_suc_for_type dtypes T =
+ is_asymmetric_nondatatype T orelse
+ case datatype_spec dtypes T of
+ SOME {self_rec, ...} => self_rec
+ | NONE => false
+
+fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
+ dtypes sel_quadruples =
+ case sel_quadruples of
+ [] => KK.True
+ | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
+ let val z = (x, should_tabulate_suc_for_type dtypes T) in
+ if null sel_quadruples' then
+ gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
+ else
+ kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
+ (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
+ (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
+ (kk_join (KK.Var (1, 0)) r))
+ (lex_order_rel_expr kk dtypes sel_quadruples'))
+ end
+ (* Skip constructors components that aren't atoms, since we cannot compare
+ these easily. *)
+ | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
+
+fun is_nil_like_constr_type dtypes T =
+ case datatype_spec dtypes T of
+ SOME {constrs, ...} =>
+ (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
+ [{const = (_, T'), ...}] => T = T'
+ | _ => false)
+ | NONE => false
+
+fun sym_break_axioms_for_constr_pair hol_ctxt binarize
+ (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
+ kk_join, ...}) rel_table nfas dtypes
+ (constr_ord,
+ ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
+ {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
+ : constr_spec * constr_spec) =
+ let
+ val dataT = body_type T1
+ val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
+ val rec_Ts = nfa |> map fst
+ fun rec_and_nonrec_sels (x as (_, T)) =
+ index_seq 0 (num_sels_for_constr_type T)
+ |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
+ |> List.partition (member (op =) rec_Ts o range_type o snd)
+ val sel_xs1 = rec_and_nonrec_sels const1 |> op @
+ in
+ if constr_ord = EQUAL andalso null sel_xs1 then
+ []
+ else
+ let
+ val z =
+ (case #2 (const_triple rel_table (discr_for_constr const1)) of
+ Func (Atom x, Formula _) => x
+ | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
+ [R]), should_tabulate_suc_for_type dtypes dataT)
+ val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
+ val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
+ fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
+ (* If the two constructors are the same, we drop the first selector
+ because that one is always checked by the lexicographic order.
+ We sometimes also filter out direct subterms, because those are
+ already handled by the acyclicity breaking in the bound
+ declarations. *)
+ fun filter_out_sels no_direct sel_xs =
+ apsnd (filter_out
+ (fn ((x, _), T) =>
+ (constr_ord = EQUAL andalso x = hd sel_xs) orelse
+ (T = dataT andalso
+ (no_direct orelse not (member (op =) sel_xs x)))))
+ fun subterms_r no_direct sel_xs j =
+ loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
+ (filter_out (curry (op =) dataT) (map fst nfa)) dataT
+ |> kk_join (KK.Var (1, j))
+ in
+ [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
+ KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
+ (kk_implies
+ (if delta2 >= epsilon1 then KK.True
+ else if delta1 >= epsilon2 - 1 then KK.False
+ else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
+ (kk_or
+ (if is_nil_like_constr_type dtypes T1 then
+ KK.True
+ else
+ kk_some (kk_intersect (subterms_r false sel_xs2 1)
+ (all_ge kk z (KK.Var (1, 0)))))
+ (case constr_ord of
+ EQUAL =>
+ kk_and
+ (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
+ (kk_all [KK.DeclOne ((1, 2),
+ subterms_r true sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
+ | LESS =>
+ kk_all [KK.DeclOne ((1, 2),
+ subterms_r false sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
+ | GREATER => KK.False)))]
+ end
+ end
+
+fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
+ ({constrs, ...} : datatype_spec) =
+ let
+ val constrs = sort constr_ord constrs
+ val constr_pairs = all_distinct_unordered_pairs_of constrs
+ in
+ map (pair EQUAL) (constrs ~~ constrs) @
+ map (pair LESS) constr_pairs @
+ map (pair GREATER) (map swap constr_pairs)
+ |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
+ nfas dtypes)
+ end
+
+fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
+ T = T' orelse exists (is_datatype_in_needed_value T) us
+ | is_datatype_in_needed_value _ _ = false
+
+val min_sym_break_card = 7
+
+fun sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
+ datatype_sym_break kk rel_table nfas dtypes =
+ if datatype_sym_break = 0 then
+ []
+ else
+ maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
+ dtypes)
+ (dtypes |> filter is_datatype_acyclic
+ |> filter (fn {constrs = [_], ...} => false
+ | {card, constrs, ...} =>
+ card >= min_sym_break_card andalso
+ forall (forall (not o is_higher_order_type)
+ o binder_types o snd o #const) constrs)
+ |> filter_out (fn {typ, ...} =>
+ exists (is_datatype_in_needed_value typ)
+ needed_us)
+ |> (fn dtypes' =>
+ dtypes'
+ |> length dtypes' > datatype_sym_break
+ ? (sort (datatype_ord o swap)
+ #> take datatype_sym_break)))
+
+fun sel_axiom_for_sel hol_ctxt binarize j0
+ (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
+ rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
+ n =
+ let
+ val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
+ val (r, R, _) = const_triple rel_table x
+ val R2 = dest_Func R |> snd
+ val z = (epsilon - delta, delta + j0)
+ in
+ if exclusive then
+ kk_n_ary_function kk (Func (Atom z, R2)) r
+ else
+ let val r' = kk_join (KK.Var (1, 0)) r in
+ kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
+ (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
+ (kk_n_ary_function kk R2 r') (kk_no r'))
+ end
+ end
+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 =
+ explicit_max < 0 orelse epsilon - delta <= explicit_max
+ in
+ if explicit_max = 0 then
+ [formula_for_bool honors_explicit_max]
+ else
+ let
+ val dom_r = discr_rel_expr rel_table const
+ val max_axiom =
+ if honors_explicit_max then
+ KK.True
+ else if bits = 0 orelse
+ is_twos_complement_representable bits (epsilon - delta) then
+ KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
+ else
+ raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
+ "\"bits\" value " ^ string_of_int bits ^
+ " too small for \"max\"")
+ in
+ max_axiom ::
+ 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
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
+ ({constrs, ...} : datatype_spec) =
+ maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
+
+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
+ 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 binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
+ (~1 upto num_sels - 1)
+ val set_r = triples |> hd |> #1
+ in
+ if num_sels = 0 then
+ kk_lone set_r
+ else
+ kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
+ (kk_implies
+ (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
+ (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
+ end
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
+ ({constrs, ...} : datatype_spec) =
+ map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
+
+fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
+fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
+ rel_table
+ ({card, constrs, ...} : datatype_spec) =
+ if forall #exclusive constrs then
+ [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
+ else
+ let val rs = map (discr_rel_expr rel_table o #const) constrs in
+ [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
+ kk_disjoint_sets kk rs]
+ end
+
+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 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
+
+fun declarative_axioms_for_datatypes hol_ctxt binarize needed_us
+ datatype_sym_break bits ofs kk rel_table dtypes =
+ let
+ val nfas =
+ dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
+ rel_table dtypes)
+ |> strongly_connected_sub_nfas
+ in
+ acyclicity_axioms_for_datatypes kk nfas @
+ maps (needed_value_axioms_for_datatype needed_us ofs kk) dtypes @
+ sym_break_axioms_for_datatypes hol_ctxt binarize needed_us
+ datatype_sym_break kk rel_table nfas dtypes @
+ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+ dtypes
+ end
+
end;