745 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = |
745 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = |
746 kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) |
746 kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) |
747 fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 = |
747 fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 = |
748 kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z)))) |
748 kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z)))) |
749 |
749 |
750 fun constr_ord (({const = (s1, _), delta = delta1, epsilon = epsilon1, ...}, |
750 fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) = |
751 {const = (s2, _), delta = delta2, epsilon = epsilon2, ...}) |
751 (delta, (epsilon, (num_binder_types T, s))) |
752 : constr_spec * constr_spec) = |
752 val constr_ord = |
753 prod_ord int_ord (prod_ord int_ord string_ord) |
753 prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord)) |
754 ((delta1, (epsilon2, s1)), (delta2, (epsilon2, s2))) |
754 o pairself constr_quadruple |
755 |
755 |
756 fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, |
756 fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, |
757 {card = card2, self_rec = self_rec2, constrs = constr2, ...}) |
757 {card = card2, self_rec = self_rec2, constrs = constr2, ...}) |
758 : datatype_spec * datatype_spec) = |
758 : datatype_spec * datatype_spec) = |
759 prod_ord int_ord (prod_ord bool_ord int_ord) |
759 prod_ord int_ord (prod_ord bool_ord int_ord) |
797 | NONE => false |
797 | NONE => false |
798 |
798 |
799 fun sym_break_axioms_for_constr_pair hol_ctxt binarize |
799 fun sym_break_axioms_for_constr_pair hol_ctxt binarize |
800 (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset, |
800 (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset, |
801 kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes |
801 kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes |
802 (({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, |
802 (constr_ord, |
|
803 ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, |
803 {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...}) |
804 {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...}) |
804 : constr_spec * constr_spec) = |
805 : constr_spec * constr_spec) = |
805 let |
806 let |
806 val dataT = body_type T1 |
807 val dataT = body_type T1 |
807 val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these |
808 val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these |
808 val rec_Ts = nfa |> map fst |
809 val rec_Ts = nfa |> map fst |
809 val same_constr = (const1 = const2) |
|
810 fun rec_and_nonrec_sels (x as (_, T)) = |
810 fun rec_and_nonrec_sels (x as (_, T)) = |
811 index_seq 0 (num_sels_for_constr_type T) |
811 index_seq 0 (num_sels_for_constr_type T) |
812 |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x) |
812 |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x) |
813 |> List.partition (member (op =) rec_Ts o range_type o snd) |
813 |> List.partition (member (op =) rec_Ts o range_type o snd) |
814 val sel_xs1 = rec_and_nonrec_sels const1 |> op @ |
814 val sel_xs1 = rec_and_nonrec_sels const1 |> op @ |
815 in |
815 in |
816 if same_constr andalso null sel_xs1 then |
816 if constr_ord = EQUAL andalso null sel_xs1 then |
817 [] |
817 [] |
818 else |
818 else |
819 let |
819 let |
820 val z = |
820 val z = |
821 (case #2 (const_triple rel_table (discr_for_constr const1)) of |
821 (case #2 (const_triple rel_table (discr_for_constr const1)) of |
831 already handled by the acyclicity breaking in the bound |
831 already handled by the acyclicity breaking in the bound |
832 declarations. *) |
832 declarations. *) |
833 fun filter_out_sels no_direct sel_xs = |
833 fun filter_out_sels no_direct sel_xs = |
834 apsnd (filter_out |
834 apsnd (filter_out |
835 (fn ((x, _), T) => |
835 (fn ((x, _), T) => |
836 (same_constr andalso x = hd sel_xs) orelse |
836 (constr_ord = EQUAL andalso x = hd sel_xs) orelse |
837 (T = dataT andalso |
837 (T = dataT andalso |
838 (no_direct orelse not (member (op =) sel_xs x))))) |
838 (no_direct orelse not (member (op =) sel_xs x))))) |
839 (* FIXME: why the last disjunct above? *) |
839 (* FIXME: why the last disjunct above? *) |
840 fun subterms_r no_direct sel_xs j = |
840 fun subterms_r no_direct sel_xs j = |
841 loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa) |
841 loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa) |
842 (filter_out (curry (op =) dataT) (map fst nfa)) dataT |
842 (filter_out (curry (op =) dataT) (map fst nfa)) dataT |
843 |> kk_join (KK.Var (1, j)) |
843 |> kk_join (KK.Var (1, j)) |
844 in |
844 in |
845 [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1), |
845 [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1), |
846 KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)] |
846 KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)] |
847 ((if same_constr then kk_implies else kk_iff) |
847 (kk_implies |
848 (if delta2 >= epsilon1 then KK.True |
848 (if delta2 >= epsilon1 then KK.True |
|
849 else if delta1 >= epsilon2 - 1 then KK.False |
849 else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0))) |
850 else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0))) |
850 (kk_or |
851 (kk_or |
851 (if is_nil_like_constr_type dtypes T1 then |
852 (if is_nil_like_constr_type dtypes T1 then |
852 KK.True |
853 KK.True |
853 else |
854 else |
854 kk_some (kk_intersect (subterms_r false sel_xs2 1) |
855 kk_some (kk_intersect (subterms_r false sel_xs2 1) |
855 (all_ge kk z (KK.Var (1, 0))))) |
856 (all_ge kk z (KK.Var (1, 0))))) |
856 (if same_constr then |
857 (case constr_ord of |
|
858 EQUAL => |
857 kk_and |
859 kk_and |
858 (lex_order_rel_expr kk dtypes (sel_quadruples2 ())) |
860 (lex_order_rel_expr kk dtypes (sel_quadruples2 ())) |
859 (if length rec_sel_xs2 > 1 then |
861 (if length rec_sel_xs2 > 1 then |
860 kk_all [KK.DeclOne ((1, 2), |
862 kk_all [KK.DeclOne ((1, 2), |
861 subterms_r true sel_xs1 0)] |
863 subterms_r true sel_xs1 0)] |
862 (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) |
864 (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) |
863 else |
865 else |
864 KK.True) |
866 KK.True) |
865 else |
867 | LESS => |
866 kk_all [KK.DeclOne ((1, 2), |
868 kk_all [KK.DeclOne ((1, 2), |
867 subterms_r false sel_xs1 0)] |
869 subterms_r false sel_xs1 0)] |
868 (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))))] |
870 (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) |
|
871 | GREATER => KK.False)))] |
869 end |
872 end |
870 end |
873 end |
871 |
874 |
872 fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes |
875 fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes |
873 ({constrs, ...} : datatype_spec) = |
876 ({constrs, ...} : datatype_spec) = |
874 let val constrs = sort constr_ord constrs in |
877 let |
875 maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table nfas |
878 val constrs = sort constr_ord constrs |
876 dtypes) |
879 val constr_pairs = all_distinct_unordered_pairs_of constrs |
877 ((constrs ~~ constrs) @ all_distinct_unordered_pairs_of constrs) |
880 in |
878 end |
881 map (pair EQUAL) (constrs ~~ constrs) @ |
|
882 map (pair LESS) constr_pairs @ |
|
883 map (pair GREATER) (map swap constr_pairs) |
|
884 |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table |
|
885 nfas dtypes) |
|
886 end |
879 |
887 |
880 val min_sym_break_card = 7 |
888 val min_sym_break_card = 7 |
881 |
889 |
882 fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk |
890 fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk |
883 rel_table nfas dtypes = |
891 rel_table nfas dtypes = |