# HG changeset patch # User blanchet # Date 1261134029 -3600 # Node ID 8a2c5d7aff51f7938bd06a1cfb1647a41f81237e # Parent 7aac4d74bb76664535cd951c4bfdd5cd199609ec polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation diff -r 7aac4d74bb76 -r 8a2c5d7aff51 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Thu Dec 17 15:22:27 2009 +0100 +++ b/doc-src/Nitpick/nitpick.tex Fri Dec 18 12:00:29 2009 +0100 @@ -740,7 +740,7 @@ \prew \textbf{lemma} ``$\exists n.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100,\, \textit{verbose}] \\[2\smallskipamount] +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] \slshape The inductive predicate ``\textit{even}'' was proved well-founded. Nitpick can compute it efficiently. \\[2\smallskipamount] Trying 1 scope: \\ @@ -758,7 +758,7 @@ \prew \textbf{lemma} ``$\exists n \mathbin{\le} 99.\; \textit{even}~n \mathrel{\land} \textit{even}~(\textit{Suc}~n)$'' \\ -\textbf{nitpick}~[\textit{card nat}~= 100] \\[2\smallskipamount] +\textbf{nitpick}~[\textit{card nat}~= 100, \textit{unary\_ints}] \\[2\smallskipamount] \slshape Nitpick found a counterexample: \\[2\smallskipamount] \hbox{}\qquad Empty assignment \postw @@ -1752,7 +1752,7 @@ \textbf{Warning:} For technical reasons, Nitpick always reverts to unary for problems that refer to the types \textit{rat} or \textit{real} or the constants -\textit{gcd} or \textit{lcm}. +\textit{Suc}, \textit{gcd}, or \textit{lcm}. {\small See also \textit{bits} (\S\ref{scope-of-search}) and \textit{show\_datatypes} (\S\ref{output-format}).} diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Divides.thy Fri Dec 18 12:00:29 2009 +0100 @@ -2443,6 +2443,17 @@ declare dvd_eq_mod_eq_0_number_of [simp] +subsubsection {* Nitpick *} + +lemma zmod_zdiv_equality': +"(m\int) mod n = m - (m div n) * n" +by (rule_tac P="%x. m mod n = x - (m div n) * n" + in subst [OF mod_div_equality [of _ n]]) + arith + +lemmas [nitpick_def] = mod_div_equality' [THEN eq_reflection] + zmod_zdiv_equality' [THEN eq_reflection] + subsubsection {* Code generation *} definition pdivmod :: "int \ int \ int \ int" where diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/IsaMakefile Fri Dec 18 12:00:29 2009 +0100 @@ -610,13 +610,13 @@ HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ - Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ - Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \ - Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ - Nitpick_Examples/Nitpick_Examples.thy \ - Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ - Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ + Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ + Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Integer_Nits.thy \ + Nitpick_Examples/Manual_Nits.thy Nitpick_Examples/Mini_Nits.thy \ + Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \ + Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ + Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -876,7 +876,7 @@ by auto lemma "I = (\x\'a set. x) \ uminus = (\x. uminus (I x))" -nitpick [expect = none] +nitpick [card = 1\7, expect = none] by auto lemma "A \ - A = UNIV" @@ -892,7 +892,7 @@ oops lemma "I = (\x. x) \ finite = (\x. finite (I x))" -nitpick [expect = none] +nitpick [card = 1\7, expect = none] oops lemma "finite A" diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -14,21 +14,11 @@ nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s] primrec rot where -"rot Nibble0 = Nibble1" | -"rot Nibble1 = Nibble2" | -"rot Nibble2 = Nibble3" | -"rot Nibble3 = Nibble4" | -"rot Nibble4 = Nibble5" | -"rot Nibble5 = Nibble6" | -"rot Nibble6 = Nibble7" | -"rot Nibble7 = Nibble8" | -"rot Nibble8 = Nibble9" | -"rot Nibble9 = NibbleA" | -"rot NibbleA = NibbleB" | -"rot NibbleB = NibbleC" | -"rot NibbleC = NibbleD" | -"rot NibbleD = NibbleE" | -"rot NibbleE = NibbleF" | +"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" | +"rot Nibble3 = Nibble4" | "rot Nibble4 = Nibble5" | "rot Nibble5 = Nibble6" | +"rot Nibble6 = Nibble7" | "rot Nibble7 = Nibble8" | "rot Nibble8 = Nibble9" | +"rot Nibble9 = NibbleA" | "rot NibbleA = NibbleB" | "rot NibbleB = NibbleC" | +"rot NibbleC = NibbleD" | "rot NibbleD = NibbleE" | "rot NibbleE = NibbleF" | "rot NibbleF = Nibble0" lemma "rot n \ n" diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Integer_Nits.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -0,0 +1,209 @@ +(* Title: HOL/Nitpick_Examples/Integer_Nits.thy + Author: Jasmin Blanchette, TU Muenchen + Copyright 2009 + +Examples featuring Nitpick applied to natural numbers and integers. +*) + +header {* Examples Featuring Nitpick Applied to Natural Numbers and Integers *} + +theory Integer_Nits +imports Nitpick +begin + +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s, + card = 1\6, bits = 1,2,3,4,6,8] + +lemma "Suc x = x + 1" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x < Suc x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y \ (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y > (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y = y + (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x > y \ x - y \ (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ y \ x - y = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x - (0::nat) = x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "0 * y = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y * 0 = (0::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (y::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x * y div y = (x::nat)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "y \ 0 \ x * y div y = (x::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "5 * 55 < (260::nat)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +nitpick [binary_ints, bits = 9, expect = genuine] +oops + +lemma "nat (of_nat n) = n" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x + y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y \ (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ 0 \ x + y \ (y::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ 0 \ x + y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x + y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y \ 0 \ x + y > (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x + y = y + (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x > y \ x - y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "x \ y \ x - y = (0::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x - (0::int) = x" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "0 * y = (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "y * 0 = (0::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "\x \ 0; y \ 0\ \ x * y \ (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "\x \ 0; y \ 0\ \ x * y \ (y::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "x * y div y = (x::int)" +nitpick [unary_ints, expect = genuine] +nitpick [binary_ints, expect = genuine] +oops + +lemma "y \ 0 \ x * y div y = (x::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none, card = 1\5, bits = 1\5] +sorry + +lemma "(x * y < 0) \ (x > 0 \ y < 0) \ (x < 0 \ y > (0::int))" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +lemma "-5 * 55 > (-260::int)" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +nitpick [binary_ints, bits = 9, expect = genuine] +oops + +lemma "nat (of_nat n) = n" +nitpick [unary_ints, expect = none] +nitpick [binary_ints, expect = none] +sorry + +end diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -59,7 +59,7 @@ nitpick oops -subsection {* 3.5. Numbers *} +subsection {* 3.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" nitpick @@ -121,11 +121,11 @@ "even n \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" -nitpick [card nat = 100, verbose] +nitpick [card nat = 100, unary_ints, verbose] oops lemma "\n \ 99. even n \ even (Suc n)" -nitpick [card nat = 100] +nitpick [card nat = 100, unary_ints, verbose] oops inductive even' where @@ -134,7 +134,7 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" -nitpick [card nat = 10, verbose, show_consts] +nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *) oops lemma "even' (n - 2) \ even' n" diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Nitpick_Examples.thy --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy Fri Dec 18 12:00:29 2009 +0100 @@ -6,9 +6,8 @@ *) theory Nitpick_Examples -imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits - Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits +imports Core_Nits Datatype_Nits Induct_Nits Integer_Nits Manual_Nits Mini_Nits + Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits Typedef_Nits begin - end diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Special_Nits.thy --- a/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -135,7 +135,7 @@ lemma "\a. g a = a \ \b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\nat). b\<^isub>1 < b\<^isub>11 \ f5 g x = f5 (\a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x" -nitpick [expect = none] +nitpick [expect = potential] nitpick [dont_specialize, expect = none] nitpick [dont_box, expect = none] nitpick [dont_box, dont_specialize, expect = none] diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Dec 18 12:00:29 2009 +0100 @@ -11,7 +11,7 @@ imports Main Rational begin -nitpick_params [card = 1\4, timeout = 5 s] +nitpick_params [card = 1\4, timeout = 30 s] typedef three = "{0\nat, 1, 2}" by blast @@ -67,7 +67,7 @@ sorry lemma "x \ (y\(bool \ bool) bounded) \ z = x \ z = y" -nitpick [card = 1\5, timeout = 10 s, expect = genuine] +nitpick [card = 1\5, expect = genuine] oops lemma "True \ ((\x\bool. x) = (\x. x))" @@ -157,15 +157,15 @@ by (rule Rep_Nat_inverse) lemma "0 \ Abs_Integ (intrel `` {(0, 0)})" -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none] +nitpick [card = 1, unary_ints, max_potential = 0, expect = none] by (rule Zero_int_def_raw) lemma "Abs_Integ (Rep_Integ a) = a" -nitpick [card = 1, timeout = 60 s, max_potential = 0, expect = none] +nitpick [card = 1, unary_ints, max_potential = 0, expect = none] by (rule Rep_Integ_inverse) lemma "Abs_list (Rep_list a) = a" -nitpick [card = 1\2, timeout = 60 s, expect = none] +nitpick [card = 1\2, expect = none] by (rule Rep_list_inverse) record point = diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Dec 18 12:00:29 2009 +0100 @@ -75,6 +75,8 @@ open Nitpick_Kodkod open Nitpick_Model +structure KK = Kodkod + type params = { cards_assigns: (typ option * int list) list, maxes_assigns: (styp option * int list) list, @@ -126,10 +128,10 @@ rel_table: nut NameTable.table, liberal: bool, scope: scope, - core: Kodkod.formula, - defs: Kodkod.formula list} + core: KK.formula, + defs: KK.formula list} -type rich_problem = Kodkod.problem * problem_extension +type rich_problem = KK.problem * problem_extension (* Proof.context -> string -> term list -> Pretty.T list *) fun pretties_for_formulas _ _ [] = [] @@ -344,8 +346,8 @@ val _ = if verbose andalso binary_ints = SOME true andalso exists (member (op =) [nat_T, int_T]) Ts then print_v (K "The option \"binary_ints\" will be ignored because \ - \of the presence of rationals, reals, \"gcd\", or \ - \\"lcm\" in the problem.") + \of the presence of rationals, reals, \"Suc\", \ + \\"gcd\", or \"lcm\" in the problem.") else () val (all_dataTs, all_free_Ts) = @@ -447,7 +449,7 @@ NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1 val min_univ_card = NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table - (univ_card nat_card int_card main_j0 [] Kodkod.True) + (univ_card nat_card int_card main_j0 [] KK.True) val _ = check_arity min_univ_card min_highest_arity val core_u = choose_reps_in_nut scope liberal rep_table false core_u @@ -469,7 +471,7 @@ val core_u = rename_vars_in_nut pool rel_table core_u val def_us = map (rename_vars_in_nut pool rel_table) def_us val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us - (* nut -> Kodkod.formula *) + (* nut -> KK.formula *) val to_f = kodkod_formula_from_nut bits ofs liberal kk val core_f = to_f core_u val def_fs = map to_f def_us @@ -510,7 +512,7 @@ fold Integer.max (map (fst o fst) (maps fst bounds)) 0 val formula = fold_rev s_and declarative_axioms formula val _ = if bits = 0 then () else check_bits bits formula - val _ = if formula = Kodkod.False then () + val _ = if formula = KK.False then () else check_arity univ_card highest_arity in SOME ({comment = comment, settings = settings, univ_card = univ_card, @@ -525,7 +527,7 @@ defs = nondef_fs @ def_fs @ declarative_axioms}) end handle TOO_LARGE (loc, msg) => - if loc = "Nitpick_Kodkod.check_arity" + if loc = "Nitpick_KK.check_arity" andalso not (Typtab.is_empty ofs) then problem_for_scope liberal {ext_ctxt = ext_ctxt, card_assigns = card_assigns, @@ -548,10 +550,9 @@ " component of scope.")); NONE) - (* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *) + (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *) fun tuple_set_for_rel univ_card = - Kodkod.TupleSet o map (kk_tuple debug univ_card) o the - oo AList.lookup (op =) + KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =) val word_model = if falsify then "counterexample" else "model" @@ -566,7 +567,7 @@ List.app (Unsynchronized.change checked_problems o Option.map o cons o nth problems) - (* bool -> Kodkod.raw_bound list -> problem_extension -> bool option *) + (* bool -> KK.raw_bound list -> problem_extension -> bool option *) fun print_and_check_model genuine bounds ({free_names, sel_names, nonsel_names, rel_table, scope, ...} : problem_extension) = @@ -663,7 +664,7 @@ let val max_potential = Int.max (0, max_potential) val max_genuine = Int.max (0, max_genuine) - (* bool -> int * Kodkod.raw_bound list -> bool option *) + (* bool -> int * KK.raw_bound list -> bool option *) fun print_and_check genuine (j, bounds) = print_and_check_model genuine bounds (snd (nth problems j)) val max_solutions = max_potential + max_genuine @@ -672,15 +673,15 @@ if max_solutions <= 0 then (0, 0, donno) else - case Kodkod.solve_any_problem overlord deadline max_threads - max_solutions (map fst problems) of - Kodkod.NotInstalled => + case KK.solve_any_problem overlord deadline max_threads max_solutions + (map fst problems) of + KK.NotInstalled => (print_m install_kodkodi_message; (max_potential, max_genuine, donno + 1)) - | Kodkod.Normal ([], unsat_js) => + | KK.Normal ([], unsat_js) => (update_checked_problems problems unsat_js; (max_potential, max_genuine, donno)) - | Kodkod.Normal (sat_ps, unsat_js) => + | KK.Normal (sat_ps, unsat_js) => let val (lib_ps, con_ps) = List.partition (#liberal o snd o nth problems o fst) sat_ps @@ -739,13 +740,12 @@ in solve_any_problem 0 max_genuine donno false problems end end end - | Kodkod.TimedOut unsat_js => + | KK.TimedOut unsat_js => (update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) - | Kodkod.Interrupted NONE => - (checked_problems := NONE; do_interrupted ()) - | Kodkod.Interrupted (SOME unsat_js) => + | KK.Interrupted NONE => (checked_problems := NONE; do_interrupted ()) + | KK.Interrupted (SOME unsat_js) => (update_checked_problems problems unsat_js; do_interrupted ()) - | Kodkod.Error (s, unsat_js) => + | KK.Error (s, unsat_js) => (update_checked_problems problems unsat_js; print_v (K ("Kodkod error: " ^ s ^ ".")); (max_potential, max_genuine, donno + 1)) @@ -787,8 +787,8 @@ SOME problem => (problems |> (null problems orelse - not (Kodkod.problems_equivalent (fst problem) - (fst (hd problems)))) + not (KK.problems_equivalent (fst problem) + (fst (hd problems)))) ? cons problem, donno) | NONE => (problems, donno + 1)) val (problems, donno) = @@ -832,7 +832,7 @@ "") ^ "." end - (* int -> int -> scope list -> int * int * int -> Kodkod.outcome *) + (* int -> int -> scope list -> int * int * int -> KK.outcome *) fun run_batches _ _ [] (max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then (print_m (fn () => excipit "ran out of some resource"); "unknown") diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Dec 18 12:00:29 2009 +0100 @@ -968,7 +968,8 @@ | @{typ unit} => 1 | Type _ => (case datatype_constrs ext_ctxt T of - [] => if is_integer_type T then 0 else raise SAME () + [] => if is_integer_type T orelse is_bit_type T then 0 + else raise SAME () | constrs => let val constr_cards = @@ -1220,7 +1221,7 @@ (* Proof.context -> term list -> const_table *) fun const_def_table ctxt ts = - table_for (rev o map prop_of o Nitpick_Defs.get) ctxt + table_for (map prop_of o Nitpick_Defs.get) ctxt |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) (* term list -> const_table *) @@ -3350,13 +3351,13 @@ (* term -> bool *) fun may_use_binary_ints (t1 $ t2) = may_use_binary_ints t1 andalso may_use_binary_ints t2 - | may_use_binary_ints (Const (s, _)) = + | may_use_binary_ints (t as Const (s, _)) = + t <> @{const Suc} andalso not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, - @{const_name Frac}, @{const_name norm_frac}, - @{const_name nat_gcd}, @{const_name nat_lcm}] s) + @{const_name nat_gcd}, @{const_name nat_lcm}, + @{const_name Frac}, @{const_name norm_frac}] s) | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' | may_use_binary_ints _ = true - fun should_use_binary_ints (t1 $ t2) = should_use_binary_ints t1 orelse should_use_binary_ints t2 | should_use_binary_ints (Const (s, _)) = diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Dec 18 12:00:29 2009 +0100 @@ -49,44 +49,46 @@ open Nitpick_Rep open Nitpick_Nut -type nfa_transition = Kodkod.rel_expr * typ +structure KK = Kodkod + +type nfa_transition = KK.rel_expr * typ type nfa_entry = typ * nfa_transition list type nfa_table = nfa_entry list structure NfaGraph = Graph(type key = typ val ord = TermOrd.typ_ord) -(* int -> Kodkod.int_expr list *) -fun flip_nums n = index_seq 1 n @ [0] |> map Kodkod.Num +(* int -> KK.int_expr list *) +fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num -(* int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int *) +(* int -> int -> int -> KK.bound list -> KK.formula -> int *) fun univ_card nat_card int_card main_j0 bounds formula = let - (* Kodkod.rel_expr -> int -> int *) + (* KK.rel_expr -> int -> int *) fun rel_expr_func r k = Int.max (k, case r of - Kodkod.Atom j => j + 1 - | Kodkod.AtomSeq (k', j0) => j0 + k' + KK.Atom j => j + 1 + | KK.AtomSeq (k', j0) => j0 + k' | _ => 0) - (* Kodkod.tuple -> int -> int *) + (* KK.tuple -> int -> int *) fun tuple_func t k = case t of - Kodkod.Tuple js => fold Integer.max (map (Integer.add 1) js) k + KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k | _ => k - (* Kodkod.tuple_set -> int -> int *) + (* KK.tuple_set -> int -> int *) fun tuple_set_func ts k = - Int.max (k, case ts of Kodkod.TupleAtomSeq (k', j0) => j0 + k' | _ => 0) + Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0) val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, int_expr_func = K I} val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func} - val card = fold (Kodkod.fold_bound expr_F tuple_F) bounds 1 - |> Kodkod.fold_formula expr_F formula + val card = fold (KK.fold_bound expr_F tuple_F) bounds 1 + |> KK.fold_formula expr_F formula in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end -(* int -> Kodkod.formula -> unit *) +(* int -> KK.formula -> unit *) fun check_bits bits formula = let - (* Kodkod.int_expr -> unit -> unit *) - fun int_expr_func (Kodkod.Num k) () = + (* KK.int_expr -> unit -> unit *) + fun int_expr_func (KK.Num k) () = if is_twos_complement_representable bits k then () else @@ -96,39 +98,38 @@ | int_expr_func _ () = () val expr_F = {formula_func = K I, rel_expr_func = K I, int_expr_func = int_expr_func} - in Kodkod.fold_formula expr_F formula () end + in KK.fold_formula expr_F formula () end (* int -> int -> unit *) fun check_arity univ_card n = - if n > Kodkod.max_arity univ_card then + if n > KK.max_arity univ_card then raise TOO_LARGE ("Nitpick_Kodkod.check_arity", "arity " ^ string_of_int n ^ " too large for universe of \ \cardinality " ^ string_of_int univ_card) else () -(* bool -> int -> int list -> Kodkod.tuple *) +(* bool -> int -> int list -> KK.tuple *) fun kk_tuple debug univ_card js = if debug then - Kodkod.Tuple js + KK.Tuple js else - Kodkod.TupleIndex (length js, - fold (fn j => fn accum => accum * univ_card + j) js 0) + KK.TupleIndex (length js, + fold (fn j => fn accum => accum * univ_card + j) js 0) -(* (int * int) list -> Kodkod.tuple_set *) -val tuple_set_from_atom_schema = - foldl1 Kodkod.TupleProduct o map Kodkod.TupleAtomSeq -(* rep -> Kodkod.tuple_set *) +(* (int * int) list -> KK.tuple_set *) +val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq +(* rep -> KK.tuple_set *) val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep -(* int -> Kodkod.tuple_set *) -val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single -(* int -> Kodkod.int_bound list *) +(* int -> KK.tuple_set *) +val single_atom = KK.TupleSet o single o KK.Tuple o single +(* int -> KK.int_bound list *) fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] -(* int -> int -> Kodkod.int_bound list *) +(* int -> int -> KK.int_bound list *) fun pow_of_two_int_bounds bits j0 univ_card = let - (* int -> int -> int -> Kodkod.int_bound list *) + (* int -> int -> int -> KK.int_bound list *) fun aux 0 _ _ = [] | aux 1 pow_of_two j = if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else [] @@ -137,11 +138,11 @@ aux (iter - 1) (2 * pow_of_two) (j + 1) in aux (bits + 1) 1 j0 end -(* Kodkod.formula -> Kodkod.n_ary_index list *) +(* KK.formula -> KK.n_ary_index list *) fun built_in_rels_in_formula formula = let - (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *) - fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) = + (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *) + fun rel_expr_func (r as KK.Rel (x as (n, j))) = if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then I else @@ -151,7 +152,7 @@ | rel_expr_func _ = I val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, int_expr_func = K I} - in Kodkod.fold_formula expr_F formula [] end + in KK.fold_formula expr_F formula [] end val max_table_size = 65536 @@ -163,7 +164,7 @@ else () -(* bool -> int -> int * int -> (int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int -> int) -> KK.tuple list *) fun tabulate_func1 debug univ_card (k, j0) f = (check_table_size k; map_filter (fn j1 => let val j2 = f j1 in @@ -172,7 +173,7 @@ else NONE end) (index_seq 0 k)) -(* bool -> int -> int * int -> int -> (int * int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> int -> (int * int -> int) -> KK.tuple list *) fun tabulate_op2 debug univ_card (k, j0) res_j0 f = (check_table_size (k * k); map_filter (fn j => let @@ -187,7 +188,7 @@ NONE end) (index_seq 0 (k * k))) (* bool -> int -> int * int -> int -> (int * int -> int * int) - -> Kodkod.tuple list *) + -> KK.tuple list *) fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f = (check_table_size (k * k); map_filter (fn j => let @@ -202,13 +203,13 @@ else NONE end) (index_seq 0 (k * k))) -(* bool -> int -> int * int -> (int * int -> int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int * int -> int) -> KK.tuple list *) fun tabulate_nat_op2 debug univ_card (k, j0) f = tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f) fun tabulate_int_op2 debug univ_card (k, j0) f = tabulate_op2 debug univ_card (k, j0) j0 (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0))) -(* bool -> int -> int * int -> (int * int -> int * int) -> Kodkod.tuple list *) +(* bool -> int -> int * int -> (int * int -> int * int) -> KK.tuple list *) fun tabulate_int_op2_2 debug univ_card (k, j0) f = tabulate_op2_2 debug univ_card (k, j0) j0 (pairself (atom_for_int (k, 0)) o f @@ -228,7 +229,7 @@ else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end (* bool -> int -> int -> int -> int -> int * int - -> string * bool * Kodkod.tuple list *) + -> string * bool * KK.tuple list *) fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) = (check_arity univ_card n; if x = not3_rel then @@ -269,15 +270,14 @@ else raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) -(* bool -> int -> int -> int -> int -> int * int -> Kodkod.rel_expr - -> Kodkod.bound *) +(* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *) fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x = let val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card j0 x - in ([(x, nick)], [Kodkod.TupleSet ts]) end + in ([(x, nick)], [KK.TupleSet ts]) end -(* bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list *) +(* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *) fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 = map (bound_for_built_in_rel debug univ_card nat_card int_card j0) o built_in_rels_in_formula @@ -288,7 +288,7 @@ (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T) else "") ^ " : " ^ string_for_rep R -(* Proof.context -> bool -> nut -> Kodkod.bound *) +(* Proof.context -> bool -> nut -> KK.bound *) fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) = ([(x, bound_comment ctxt debug nick T R)], if nick = @{const_name bisim_iterator_max} then @@ -296,11 +296,11 @@ Atom (k, j0) => [single_atom (k - 1 + j0)] | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) else - [Kodkod.TupleSet [], upper_bound_for_rep R]) + [KK.TupleSet [], upper_bound_for_rep R]) | bound_for_plain_rel _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) -(* Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound *) +(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *) fun bound_for_sel_rel ctxt debug dtypes (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2), nick)) = @@ -310,26 +310,24 @@ in ([(x, bound_comment ctxt debug nick T R)], if explicit_max = 0 then - [Kodkod.TupleSet []] + [KK.TupleSet []] else - let val ts = Kodkod.TupleAtomSeq (epsilon - delta, delta + j0) in + let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in if R2 = Formula Neut then - [ts] |> not exclusive ? cons (Kodkod.TupleSet []) + [ts] |> not exclusive ? cons (KK.TupleSet []) else - [Kodkod.TupleSet [], - Kodkod.TupleProduct (ts, upper_bound_for_rep R2)] + [KK.TupleSet [], KK.TupleProduct (ts, upper_bound_for_rep R2)] end) end | bound_for_sel_rel _ _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) -(* Kodkod.bound list -> Kodkod.bound list *) +(* KK.bound list -> KK.bound list *) fun merge_bounds bs = let - (* Kodkod.bound -> int *) + (* KK.bound -> int *) fun arity (zs, _) = fst (fst (hd zs)) - (* Kodkod.bound list -> Kodkod.bound -> Kodkod.bound list - -> Kodkod.bound list *) + (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *) fun add_bound ds b [] = List.revAppend (ds, [b]) | add_bound ds b (c :: cs) = if arity b = arity c andalso snd b = snd c then @@ -338,40 +336,40 @@ add_bound (c :: ds) b cs in fold (add_bound []) bs [] end -(* int -> int -> Kodkod.rel_expr list *) -fun unary_var_seq j0 n = map (curry Kodkod.Var 1) (index_seq j0 n) +(* int -> int -> KK.rel_expr list *) +fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n) -(* int list -> Kodkod.rel_expr *) -val singleton_from_combination = foldl1 Kodkod.Product o map Kodkod.Atom -(* rep -> Kodkod.rel_expr list *) +(* int list -> KK.rel_expr *) +val singleton_from_combination = foldl1 KK.Product o map KK.Atom +(* rep -> KK.rel_expr list *) fun all_singletons_for_rep R = if is_lone_rep R then all_combinations_for_rep R |> map singleton_from_combination else raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) -(* Kodkod.rel_expr -> Kodkod.rel_expr list *) -fun unpack_products (Kodkod.Product (r1, r2)) = +(* KK.rel_expr -> KK.rel_expr list *) +fun unpack_products (KK.Product (r1, r2)) = unpack_products r1 @ unpack_products r2 | unpack_products r = [r] -fun unpack_joins (Kodkod.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 +fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 | unpack_joins r = [r] -(* rep -> Kodkod.rel_expr *) +(* rep -> KK.rel_expr *) val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep fun full_rel_for_rep R = case atom_schema_of_rep R of [] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) - | schema => foldl1 Kodkod.Product (map Kodkod.AtomSeq schema) + | schema => foldl1 KK.Product (map KK.AtomSeq schema) -(* int -> int list -> Kodkod.decl list *) +(* int -> int list -> KK.decl list *) fun decls_for_atom_schema j0 schema = - map2 (fn j => fn x => Kodkod.DeclOne ((1, j), Kodkod.AtomSeq x)) + map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) (index_seq j0 (length schema)) schema (* The type constraint below is a workaround for a Poly/ML bug. *) -(* kodkod_constrs -> rep -> Kodkod.rel_expr -> Kodkod.formula *) +(* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *) fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) R r = let val body_R = body_rep R in @@ -380,13 +378,13 @@ val binder_schema = atom_schema_of_reps (binder_reps R) val body_schema = atom_schema_of_rep body_R val one = is_one_rep body_R - val opt_x = case r of Kodkod.Rel x => SOME x | _ => NONE + val opt_x = case r of KK.Rel x => SOME x | _ => NONE in if opt_x <> NONE andalso length binder_schema = 1 andalso length body_schema = 1 then - (if one then Kodkod.Function else Kodkod.Functional) - (the opt_x, Kodkod.AtomSeq (hd binder_schema), - Kodkod.AtomSeq (hd body_schema)) + (if one then KK.Function else KK.Functional) + (the opt_x, KK.AtomSeq (hd binder_schema), + KK.AtomSeq (hd body_schema)) else let val decls = decls_for_atom_schema ~1 binder_schema @@ -395,12 +393,12 @@ in kk_all decls (kk_xone (fold kk_join vars r)) end end else - Kodkod.True + KK.True end -fun kk_n_ary_function kk R (r as Kodkod.Rel x) = +fun kk_n_ary_function kk R (r as KK.Rel x) = if not (is_opt_rep R) then if x = suc_rel then - Kodkod.False + KK.False else if x = nat_add_rel then formula_for_bool (card_of_rep (body_rep R) = 1) else if x = nat_multiply_rel then @@ -408,58 +406,56 @@ else d_n_ary_function kk R r else if x = nat_subtract_rel then - Kodkod.True + KK.True else d_n_ary_function kk R r | kk_n_ary_function kk R r = d_n_ary_function kk R r -(* kodkod_constrs -> Kodkod.rel_expr list -> Kodkod.formula *) -fun kk_disjoint_sets _ [] = Kodkod.True +(* kodkod_constrs -> KK.rel_expr list -> KK.formula *) +fun kk_disjoint_sets _ [] = KK.True | kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) (r :: rs) = fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs) -(* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr *) fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = if inline_rel_expr r then f r else - let val x = (Kodkod.arity_of_rel_expr r, j) in - kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x)) + let val x = (KK.arity_of_rel_expr r, j) in + kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x)) end -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr - -> Kodkod.rel_expr *) +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr *) val single_rel_rel_let = basic_rel_rel_let 0 -(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr + -> KK.rel_expr -> KK.rel_expr *) fun double_rel_rel_let kk f r1 r2 = single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 -(* kodkod_constrs - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr - -> Kodkod.rel_expr *) +(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr) + -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) fun tripl_rel_rel_let kk f r1 r2 r3 = double_rel_rel_let kk (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 -(* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *) +(* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *) fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = - kk_rel_if f (Kodkod.Atom (j0 + 1)) (Kodkod.Atom j0) -(* kodkod_constrs -> rep -> Kodkod.formula -> Kodkod.rel_expr *) + kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) +(* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *) fun rel_expr_from_formula kk R f = case unopt_rep R of Atom (2, j0) => atom_from_formula kk j0 f | _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R]) -(* kodkod_cotrs -> int -> int -> Kodkod.rel_expr -> Kodkod.rel_expr list *) +(* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *) fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity num_chunks r = List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity) chunk_arity) -(* kodkod_constrs -> bool -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr - -> Kodkod.rel_expr *) +(* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr + -> KK.rel_expr *) fun kk_n_fold_join (kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1 res_R r1 r2 = @@ -479,8 +475,8 @@ arity1 (arity_of_rep res_R) end -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr list - -> Kodkod.rel_expr list -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list + -> KK.rel_expr list -> KK.rel_expr *) fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 = if rs1 = rs2 then r else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2)) @@ -488,7 +484,7 @@ val lone_rep_fallback_max_card = 4096 val some_j0 = 0 -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) fun lone_rep_fallback kk new_R old_R r = if old_R = new_R then r @@ -505,7 +501,7 @@ else raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) end -(* kodkod_constrs -> int * int -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *) and atom_from_rel_expr kk (x as (k, j0)) old_R r = case old_R of Func (R1, R2) => @@ -518,7 +514,7 @@ end | Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) | _ => lone_rep_fallback kk (Atom x) old_R r -(* kodkod_constrs -> rep list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *) and struct_from_rel_expr kk Rs old_R r = case old_R of Atom _ => lone_rep_fallback kk (Struct Rs) old_R r @@ -542,7 +538,7 @@ lone_rep_fallback kk (Struct Rs) old_R r end | _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) -(* kodkod_constrs -> int -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and vect_from_rel_expr kk k R old_R r = case old_R of Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r @@ -565,7 +561,7 @@ (kk_n_fold_join kk true R1 R2 arg_r r)) (all_singletons_for_rep R1)) | _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = let val dom_card = card_of_rep R1 @@ -594,9 +590,9 @@ let val args_rs = all_singletons_for_rep R1 val vals_rs = unpack_vect_in_chunks kk 1 k r - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) fun empty_or_singleton_set_for arg_r val_r = - #kk_join kk val_r (#kk_product kk (Kodkod.Atom (j0 + 1)) arg_r) + #kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) in fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) end @@ -613,11 +609,11 @@ #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) end | Func (Unit, (Atom (2, j0))) => - #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1))) + #kk_rel_if kk (#kk_rel_eq kk r (KK.Atom (j0 + 1))) (full_rel_for_rep R1) (empty_rel_for_rep R1) | Func (R1', Atom (2, j0)) => func_from_no_opt_rel_expr kk R1 (Formula Neut) - (Func (R1', Formula Neut)) (#kk_join kk r (Kodkod.Atom (j0 + 1))) + (Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1))) | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, Formula Neut)])) | func_from_no_opt_rel_expr kk R1 R2 old_R r = @@ -633,14 +629,14 @@ Atom (x as (2, j0)) => let val schema = atom_schema_of_rep R1 in if length schema = 1 then - #kk_override kk (#kk_product kk (Kodkod.AtomSeq (hd schema)) - (Kodkod.Atom j0)) - (#kk_product kk r (Kodkod.Atom (j0 + 1))) + #kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) + (KK.Atom j0)) + (#kk_product kk r (KK.Atom (j0 + 1))) else let val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) |> rel_expr_from_rel_expr kk R1' R1 - val r2 = Kodkod.Var (1, ~(length schema) - 1) + val r2 = KK.Var (1, ~(length schema) - 1) val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) in #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x])) @@ -652,7 +648,7 @@ | Func (Unit, R2') => let val j0 = some_j0 in func_from_no_opt_rel_expr kk R1 R2 (Func (Atom (1, j0), R2')) - (#kk_product kk (Kodkod.Atom j0) r) + (#kk_product kk (KK.Atom j0) r) end | Func (R1', R2') => if R1 = R1' andalso R2 = R2' then @@ -677,7 +673,7 @@ end | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)]) -(* kodkod_constrs -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and rel_expr_from_rel_expr kk new_R old_R r = let val unopt_old_R = unopt_rep old_R @@ -697,43 +693,43 @@ [old_R, new_R])) unopt_old_R r end -(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *) and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *) +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *) fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r = - kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then - unsigned_bit_word_sel_rel - else - signed_bit_word_sel_rel)) -(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *) -val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom -(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *) + kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then + unsigned_bit_word_sel_rel + else + signed_bit_word_sel_rel)) +(* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *) +val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom +(* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *) fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...} : kodkod_constrs) T R i = kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) - (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1))) - (Kodkod.Bits i)) + (kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) + (KK.Bits i)) -(* kodkod_constrs -> nut -> Kodkod.formula *) +(* kodkod_constrs -> nut -> KK.formula *) 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) - (Kodkod.Rel x) + (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 (Kodkod.Rel x) - else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (Kodkod.Rel x) - else Kodkod.True + 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]) -(* nut NameTable.table -> styp -> Kodkod.rel_expr * rep * int *) +(* nut NameTable.table -> styp -> KK.rel_expr * rep * int *) fun const_triple rel_table (x as (s, T)) = case the_name rel_table (ConstName (s, T, Any)) of - FreeRel ((n, j), _, R, _) => (Kodkod.Rel (n, j), R, n) + FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n) | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x]) -(* nut NameTable.table -> styp -> Kodkod.rel_expr *) +(* nut NameTable.table -> styp -> KK.rel_expr *) fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list @@ -747,7 +743,7 @@ in map_filter (fn (j, T) => if forall (not_equal T o #typ) dtypes then NONE - else SOME (kk_project r (map Kodkod.Num [0, j]), T)) + else SOME (kk_project r (map KK.Num [0, j]), T)) (index_seq 1 (arity - 1) ~~ tl type_schema) end (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list @@ -763,28 +759,28 @@ SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes o #const) constrs) -val empty_rel = Kodkod.Product (Kodkod.None, Kodkod.None) +val empty_rel = KK.Product (KK.None, KK.None) -(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *) +(* nfa_table -> typ -> typ -> KK.rel_expr list *) fun direct_path_rel_exprs nfa start final = case AList.lookup (op =) nfa final of SOME trans => map fst (filter (curry (op =) start o snd) trans) | NONE => [] -(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *) +(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *) and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final = fold kk_union (direct_path_rel_exprs nfa start final) - (if start = final then Kodkod.Iden else empty_rel) + (if start = final then KK.Iden else empty_rel) | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final = kk_union (any_path_rel_expr kk nfa qs start final) (knot_path_rel_expr kk nfa qs start q final) (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ - -> Kodkod.rel_expr *) + -> KK.rel_expr *) and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start knot final = kk_join (kk_join (any_path_rel_expr kk nfa qs knot final) (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot))) (any_path_rel_expr kk nfa qs start knot) -(* kodkod_constrs -> nfa_table -> typ list -> typ -> Kodkod.rel_expr *) +(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *) and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start = fold kk_union (direct_path_rel_exprs nfa start start) empty_rel | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start = @@ -812,12 +808,12 @@ nfa |> graph_for_nfa |> NfaGraph.strong_conn |> map (fn keys => filter (member (op =) keys o fst) nfa) -(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> Kodkod.formula *) +(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *) fun acyclicity_axiom_for_datatype dtypes kk nfa start = #kk_no kk (#kk_intersect kk - (loop_path_rel_expr kk nfa (map fst nfa) start) Kodkod.Iden) + (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden) (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list - -> Kodkod.formula list *) + -> KK.formula list *) fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes = map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes |> strongly_connected_sub_nfas @@ -825,7 +821,7 @@ nfa) (* extended_context -> int -> kodkod_constrs -> nut NameTable.table - -> Kodkod.rel_expr -> constr_spec -> int -> Kodkod.formula *) + -> KK.rel_expr -> constr_spec -> int -> KK.formula *) fun sel_axiom_for_sel ext_ctxt j0 (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no, kk_join, ...}) rel_table dom_r @@ -840,15 +836,14 @@ if exclusive then kk_n_ary_function kk (Func (Atom z, R2)) r else - let val r' = kk_join (Kodkod.Var (1, 0)) r in - kk_all [Kodkod.DeclOne ((1, 0), Kodkod.AtomSeq z)] - (kk_formula_if (kk_subset (Kodkod.Var (1, 0)) dom_r) - (kk_n_ary_function kk R2 r') - (kk_no r')) + 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 (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table - -> constr_spec -> Kodkod.formula list *) + -> constr_spec -> KK.formula list *) fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table (constr as {const, delta, epsilon, explicit_max, ...}) = let @@ -862,9 +857,9 @@ val ran_r = discr_rel_expr rel_table const val max_axiom = if honors_explicit_max then - Kodkod.True + KK.True else if is_twos_complement_representable bits (epsilon - delta) then - Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max) + KK.LE (KK.Cardinality ran_r, KK.Num explicit_max) else raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr", "\"bits\" value " ^ string_of_int bits ^ @@ -876,21 +871,20 @@ end end (* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table - -> dtype_spec -> Kodkod.formula list *) + -> dtype_spec -> KK.formula list *) fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table ({constrs, ...} : dtype_spec) = maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun uniqueness_axiom_for_constr ext_ctxt ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} : kodkod_constrs) rel_table ({const, ...} : constr_spec) = let - (* Kodkod.rel_expr -> Kodkod.formula *) + (* KK.rel_expr -> KK.formula *) fun conjunct_for_sel r = - kk_rel_eq (kk_join (Kodkod.Var (1, 0)) r) - (kk_join (Kodkod.Var (1, 1)) 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 ext_ctxt const) @@ -904,13 +898,13 @@ if num_sels = 0 then kk_lone set_r else - kk_all (map (Kodkod.DeclOne o rpair set_r o pair 1) [0, 1]) + 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 (Kodkod.Var (1, 0)) (Kodkod.Var (1, 1)))) + (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) end (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table ({constrs, ...} : dtype_spec) = map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs @@ -918,7 +912,7 @@ (* constr_spec -> int *) fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta (* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec - -> Kodkod.formula list *) + -> KK.formula list *) fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) rel_table ({card, constrs, ...} : dtype_spec) = @@ -926,12 +920,12 @@ [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) (Kodkod.AtomSeq (card, j0)), + [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), kk_disjoint_sets kk rs] end (* extended_context -> int -> int Typtab.table -> kodkod_constrs - -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *) + -> nut NameTable.table -> dtype_spec -> KK.formula list *) fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = [] | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table (dtype as {typ, ...}) = @@ -942,12 +936,12 @@ end (* extended_context -> int -> int Typtab.table -> kodkod_constrs - -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *) + -> nut NameTable.table -> dtype_spec list -> KK.formula list *) fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes = acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @ maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes -(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *) +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *) fun kodkod_formula_from_nut bits ofs liberal (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, kk_one, @@ -959,20 +953,20 @@ val main_j0 = offset_of_type ofs bool_T val bool_j0 = main_j0 val bool_atom_R = Atom (2, main_j0) - val false_atom = Kodkod.Atom bool_j0 - val true_atom = Kodkod.Atom (bool_j0 + 1) + val false_atom = KK.Atom bool_j0 + val true_atom = KK.Atom (bool_j0 + 1) - (* polarity -> int -> Kodkod.rel_expr -> Kodkod.formula *) + (* polarity -> int -> KK.rel_expr -> KK.formula *) fun formula_from_opt_atom polar j0 r = case polar of - Neg => kk_not (kk_rel_eq r (Kodkod.Atom j0)) - | _ => kk_rel_eq r (Kodkod.Atom (j0 + 1)) - (* int -> Kodkod.rel_expr -> Kodkod.formula *) + Neg => kk_not (kk_rel_eq r (KK.Atom j0)) + | _ => kk_rel_eq r (KK.Atom (j0 + 1)) + (* int -> KK.rel_expr -> KK.formula *) val formula_from_atom = formula_from_opt_atom Pos - (* Kodkod.formula -> Kodkod.formula -> Kodkod.formula *) + (* KK.formula -> KK.formula -> KK.formula *) fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2) - (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) val kk_or3 = double_rel_rel_let kk (fn r1 => fn r2 => @@ -985,27 +979,27 @@ (kk_intersect r1 r2)) fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2) - (* int -> Kodkod.rel_expr -> Kodkod.formula list *) + (* int -> KK.rel_expr -> KK.formula list *) val unpack_formulas = map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr + -> KK.rel_expr -> KK.rel_expr *) fun kk_vect_set_op connective k r1 r2 = fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective) (unpack_formulas k r1) (unpack_formulas k r2)) - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) -> int - -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula *) + (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr + -> KK.rel_expr -> KK.formula *) fun kk_vect_set_bool_op connective k r1 r2 = fold1 kk_and (map2 connective (unpack_formulas k r1) (unpack_formulas k r2)) - (* nut -> Kodkod.formula *) + (* nut -> KK.formula *) fun to_f u = case rep_of u of Formula polar => (case u of - Cst (False, _, _) => Kodkod.False - | Cst (True, _, _) => Kodkod.True + Cst (False, _, _) => KK.False + | Cst (True, _, _) => KK.True | Op1 (Not, _, _, u1) => kk_not (to_f_with_polarity (flip_polarity polar) u1) | Op1 (Finite, _, _, u1) => @@ -1014,9 +1008,9 @@ Neut => if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) else - Kodkod.True + KK.True | Pos => formula_for_bool (not opt1) - | Neg => Kodkod.True + | Neg => KK.True end | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1 | Op2 (All, _, _, u1, u2) => @@ -1052,7 +1046,7 @@ else let (* FIXME: merge with similar code below *) - (* bool -> nut -> Kodkod.rel_expr *) + (* bool -> nut -> KK.rel_expr *) fun set_to_r widen u = if widen then kk_difference (full_rel_for_rep dom_R) @@ -1065,7 +1059,7 @@ end | Op2 (DefEq, _, _, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => Kodkod.True + Unit => KK.True | Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => @@ -1085,7 +1079,7 @@ end) | Op2 (Eq, T, R, u1, u2) => (case min_rep (rep_of u1) (rep_of u2) of - Unit => Kodkod.True + Unit => KK.True | Formula polar => kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) | min_R => @@ -1114,7 +1108,7 @@ else if is_lone_rep min_R then if arity_of_rep min_R = 1 then - kk_subset (kk_product r1 r2) Kodkod.Iden + kk_subset (kk_product r1 r2) KK.Iden else if not both_opt then (r1, r2) |> is_opt_rep (rep_of u2) ? swap |-> kk_subset @@ -1139,8 +1133,8 @@ val rs2 = unpack_products r2 in if length rs1 = length rs2 - andalso map Kodkod.arity_of_rel_expr rs1 - = map Kodkod.arity_of_rel_expr rs2 then + andalso map KK.arity_of_rel_expr rs1 + = map KK.arity_of_rel_expr rs2 then fold1 kk_and (map2 kk_subset rs1 rs2) else kk_subset r1 r2 @@ -1165,26 +1159,25 @@ | Op3 (If, _, _, u1, u2, u3) => kk_formula_if (to_f u1) (to_f_with_polarity polar u2) (to_f_with_polarity polar u3) - | FormulaReg (j, _, _) => Kodkod.FormulaReg j + | FormulaReg (j, _, _) => KK.FormulaReg j | _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) | Atom (2, j0) => formula_from_atom j0 (to_r u) | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) - (* polarity -> nut -> Kodkod.formula *) + (* polarity -> nut -> KK.formula *) and to_f_with_polarity polar u = case rep_of u of Formula _ => to_f u | Atom (2, j0) => formula_from_atom j0 (to_r u) | Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u) | _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) - (* nut -> Kodkod.rel_expr *) + (* nut -> KK.rel_expr *) and to_r u = case u of Cst (False, _, Atom _) => false_atom | Cst (True, _, Atom _) => true_atom | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) => if R1 = R2 andalso arity_of_rep R1 = 1 then - kk_intersect Kodkod.Iden (kk_product (full_rel_for_rep R1) - Kodkod.Univ) + kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) else let val schema1 = atom_schema_of_rep R1 @@ -1200,106 +1193,100 @@ (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) (rel_expr_from_rel_expr kk min_R R2 r2)) end - | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0 + | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) => to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut))) | Cst (Num j, T, R) => if is_word_type T then - atom_from_int_expr kk T R (Kodkod.Num j) + atom_from_int_expr kk T R (KK.Num j) else if T = int_T then case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of - ~1 => if is_opt_rep R then Kodkod.None + ~1 => if is_opt_rep R then KK.None else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) - | j' => Kodkod.Atom j' + | j' => KK.Atom j' else - if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T) - else if is_opt_rep R then Kodkod.None + if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T) + else if is_opt_rep R then KK.None else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) | Cst (Unknown, _, R) => empty_rel_for_rep R | Cst (Unrep, _, R) => empty_rel_for_rep R - | Cst (Suc, T, Func (Atom x, _)) => - if domain_type T <> nat_T then - Kodkod.Rel suc_rel - else - kk_intersect (Kodkod.Rel suc_rel) - (kk_product Kodkod.Univ (Kodkod.AtomSeq x)) - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel + | Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) => + to_bit_word_unary_op T R (curry KK.Add (KK.Num 1)) + | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) => + kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x)) + | Cst (Suc, _, Func (Atom x, _)) => KK.Rel suc_rel + | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel + | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => - to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add)) + to_bit_word_binary_op T R NONE (SOME (curry KK.Add)) | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => to_bit_word_binary_op T R (SOME (fn i1 => fn i2 => fn i3 => - kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2))) - (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3))))) - (SOME (curry Kodkod.Add)) + kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2))) + (KK.LE (KK.Num 0, KK.BitXor (i2, i3))))) + (SOME (curry KK.Add)) | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => - Kodkod.Rel nat_subtract_rel + KK.Rel nat_subtract_rel | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => - Kodkod.Rel int_subtract_rel + KK.Rel int_subtract_rel | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => to_bit_word_binary_op T R NONE (SOME (fn i1 => fn i2 => - Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0, - Kodkod.Sub (i1, i2)))) + KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2)))) | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => to_bit_word_binary_op T R (SOME (fn i1 => fn i2 => fn i3 => - kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0)) - (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0)))) - (SOME (curry Kodkod.Sub)) + kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0)) + (KK.LT (KK.BitXor (i2, i3), KK.Num 0)))) + (SOME (curry KK.Sub)) | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => - Kodkod.Rel nat_multiply_rel + KK.Rel nat_multiply_rel | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => - Kodkod.Rel int_multiply_rel + KK.Rel int_multiply_rel | Cst (Multiply, T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) => to_bit_word_binary_op T R (SOME (fn i1 => fn i2 => fn i3 => - kk_or (Kodkod.IntEq (i2, Kodkod.Num 0)) - (Kodkod.IntEq (Kodkod.Div (i3, i2), i1) + kk_or (KK.IntEq (i2, KK.Num 0)) + (KK.IntEq (KK.Div (i3, i2), i1) |> bit_T = @{typ signed_bit} - ? kk_and (Kodkod.LE (Kodkod.Num 0, - foldl1 Kodkod.BitAnd [i1, i2, i3]))))) - (SOME (curry Kodkod.Mult)) - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => - Kodkod.Rel nat_divide_rel - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => - Kodkod.Rel int_divide_rel + ? kk_and (KK.LE (KK.Num 0, + foldl1 KK.BitAnd [i1, i2, i3]))))) + (SOME (curry KK.Mult)) + | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel + | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => to_bit_word_binary_op T R NONE (SOME (fn i1 => fn i2 => - Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0), - Kodkod.Num 0, Kodkod.Div (i1, i2)))) + KK.IntIf (KK.IntEq (i2, KK.Num 0), + KK.Num 0, KK.Div (i1, i2)))) | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => to_bit_word_binary_op T R (SOME (fn i1 => fn i2 => fn i3 => - Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3]))) + KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3]))) (SOME (fn i1 => fn i2 => - Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0)) - (Kodkod.LT (Kodkod.Num 0, i2)), - Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2), - Kodkod.Num 1), - Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1)) - (Kodkod.LT (i2, Kodkod.Num 0)), - Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1), - i2), Kodkod.Num 1), - Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0), - Kodkod.Num 0, Kodkod.Div (i1, i2)))))) - | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel - | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel - | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None + KK.IntIf (kk_and (KK.LT (i1, KK.Num 0)) + (KK.LT (KK.Num 0, i2)), + KK.Sub (KK.Div (KK.Add (i1, KK.Num 1), i2), KK.Num 1), + KK.IntIf (kk_and (KK.LT (KK.Num 0, i1)) + (KK.LT (i2, KK.Num 0)), + KK.Sub (KK.Div (KK.Sub (i1, KK.Num 1), i2), KK.Num 1), + KK.IntIf (KK.IntEq (i2, KK.Num 0), + KK.Num 0, KK.Div (i1, i2)))))) + | Cst (Gcd, _, _) => KK.Rel gcd_rel + | Cst (Lcm, _, _) => KK.Rel lcm_rel + | Cst (Fracs, _, Func (Atom (1, _), _)) => KK.None | Cst (Fracs, _, Func (Struct _, _)) => - kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2 - | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel + kk_project_seq (KK.Rel norm_frac_rel) 2 2 + | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) => - Kodkod.Iden + KK.Iden | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) => if nat_j0 = int_j0 then - kk_intersect Kodkod.Iden - (kk_product (Kodkod.AtomSeq (max_int_for_card int_k + 1, nat_j0)) - Kodkod.Univ) + kk_intersect KK.Iden + (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0)) + KK.Univ) else raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"") | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) => @@ -1312,21 +1299,19 @@ val overlap = Int.min (nat_k, abs_card) in if nat_j0 = int_j0 then - kk_union (kk_product (Kodkod.AtomSeq (int_k - abs_card, - int_j0 + abs_card)) - (Kodkod.Atom nat_j0)) - (kk_intersect Kodkod.Iden - (kk_product (Kodkod.AtomSeq (overlap, int_j0)) - Kodkod.Univ)) + kk_union (kk_product (KK.AtomSeq (int_k - abs_card, + int_j0 + abs_card)) + (KK.Atom nat_j0)) + (kk_intersect KK.Iden + (kk_product (KK.AtomSeq (overlap, int_j0)) KK.Univ)) else raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"") end | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) => to_bit_word_unary_op T R - (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0), - Kodkod.Num 0, i)) + (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i)) | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1) - | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None + | Op1 (Finite, _, Opt (Atom _), _) => KK.None | Op1 (Converse, T, R, u1) => let val (b_T, a_T) = HOLogic.dest_prodT (domain_type T) @@ -1346,9 +1331,9 @@ val body_arity = arity_of_rep body_R in kk_project (to_rep (Func (Struct [a_R, b_R], body_R)) u1) - (map Kodkod.Num (index_seq a_arity b_arity @ - index_seq 0 a_arity @ - index_seq ab_arity body_arity)) + (map KK.Num (index_seq a_arity b_arity @ + index_seq 0 a_arity @ + index_seq ab_arity body_arity)) |> rel_expr_from_rel_expr kk R (Func (Struct [b_R, a_R], body_R)) end | Op1 (Closure, _, R, u1) => @@ -1410,13 +1395,13 @@ | Op2 (Exist, T, Opt _, u1, u2) => let val rs1 = untuple to_decl u1 in if not (is_opt_rep (rep_of u2)) then - kk_rel_if (kk_exist rs1 (to_f u2)) true_atom Kodkod.None + kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None else let val r2 = to_r u2 in kk_union (kk_rel_if (kk_exist rs1 (kk_rel_eq r2 true_atom)) - true_atom Kodkod.None) + true_atom KK.None) (kk_rel_if (kk_all rs1 (kk_rel_eq r2 false_atom)) - false_atom Kodkod.None) + false_atom KK.None) end end | Op2 (Or, _, _, u1, u2) => @@ -1437,10 +1422,10 @@ kk_rel_if (fold kk_and (map_filter (fn (u, r) => if is_opt_rep (rep_of u) then SOME (kk_some r) - else NONE) [(u1, r1), (u2, r2)]) Kodkod.True) - (atom_from_formula kk bool_j0 (Kodkod.LT (pairself + else NONE) [(u1, r1), (u2, r2)]) KK.True) + (atom_from_formula kk bool_j0 (KK.LT (pairself (int_expr_from_atom kk (type_of u1)) (r1, r2)))) - Kodkod.None) + KK.None) (to_r u1) (to_r u2)) | Op2 (The, T, R, u1, u2) => if is_opt_rep R then @@ -1485,8 +1470,8 @@ if f1 = f2 then atom_from_formula kk j0 f1 else - kk_union (kk_rel_if f1 true_atom Kodkod.None) - (kk_rel_if f2 Kodkod.None false_atom) + kk_union (kk_rel_if f1 true_atom KK.None) + (kk_rel_if f2 KK.None false_atom) end | Op2 (Union, _, R, u1, u2) => to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2 @@ -1518,7 +1503,7 @@ | Opt (Atom (2, _)) => let (* FIXME: merge with similar code above *) - (* rep -> rep -> nut -> Kodkod.rel_expr *) + (* rep -> rep -> nut -> KK.rel_expr *) fun must R1 R2 u = kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom fun may R1 R2 u = @@ -1553,9 +1538,9 @@ (to_rep (Func (b_R, Formula Neut)) u2) | Opt (Atom (2, _)) => let - (* Kodkod.rel_expr -> rep -> nut -> Kodkod.rel_expr *) + (* KK.rel_expr -> rep -> nut -> KK.rel_expr *) fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r - (* Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr *) fun do_term r = kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r in kk_union (do_term true_atom) (do_term false_atom) end @@ -1567,7 +1552,7 @@ (Func (R11, R12), Func (R21, Formula Neut)) => if R21 = R11 andalso is_lone_rep R12 then let - (* Kodkod.rel_expr -> Kodkod.rel_expr *) + (* KK.rel_expr -> KK.rel_expr *) fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1) val core_r = big_join (to_r u2) val core_R = Func (R12, Formula Neut) @@ -1593,9 +1578,9 @@ | Op2 (Apply, @{typ nat}, _, Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) => if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then - Kodkod.Atom (offset_of_type ofs nat_T) + KK.Atom (offset_of_type ofs nat_T) else - fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel) + fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel) | Op2 (Apply, _, R, u1, u2) => if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso is_FreeName u1 then @@ -1603,7 +1588,7 @@ else to_apply R u1 u2 | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) => - to_guard [u1, u2] R (Kodkod.Atom j0) + to_guard [u1, u2] R (KK.Atom j0) | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) => kk_comprehension (untuple to_decl u1) (to_f u2) | Op2 (Lambda, T, Func (_, R2), u1, u2) => @@ -1639,10 +1624,9 @@ | Vect (k, R) => to_product (replicate k R) us | Atom (1, j0) => (case filter (not_equal Unit o rep_of) us of - [] => Kodkod.Atom j0 - | us' => - kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) - (Kodkod.Atom j0) Kodkod.None) + [] => KK.Atom j0 + | us' => kk_rel_if (kk_some (fold1 kk_product (map to_r us'))) + (KK.Atom j0) KK.None) | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) | Construct ([u'], _, _, []) => to_r u' | Construct (_ :: sel_us, T, R, arg_us) => @@ -1660,47 +1644,46 @@ else kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R1)) - (kk_rel_eq (kk_join (Kodkod.Var (1, ~1)) sel_r) - arg_r) + (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r) end) sel_us arg_us in fold1 kk_intersect set_rs end - | BoundRel (x, _, _, _) => Kodkod.Var x - | FreeRel (x, _, _, _) => Kodkod.Rel x - | RelReg (j, _, R) => Kodkod.RelReg (arity_of_rep R, j) + | BoundRel (x, _, _, _) => KK.Var x + | FreeRel (x, _, _, _) => KK.Rel x + | RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j) | u => raise NUT ("Nitpick_Kodkod.to_r", [u]) - (* nut -> Kodkod.decl *) + (* nut -> KK.decl *) and to_decl (BoundRel (x, _, R, _)) = - Kodkod.DeclOne (x, Kodkod.AtomSeq (the_single (atom_schema_of_rep R))) + KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R))) | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u]) - (* nut -> Kodkod.expr_assign *) + (* nut -> KK.expr_assign *) and to_expr_assign (FormulaReg (j, _, R)) u = - Kodkod.AssignFormulaReg (j, to_f u) + KK.AssignFormulaReg (j, to_f u) | to_expr_assign (RelReg (j, _, R)) u = - Kodkod.AssignRelReg ((arity_of_rep R, j), to_r u) + KK.AssignRelReg ((arity_of_rep R, j), to_r u) | to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1]) - (* int * int -> nut -> Kodkod.rel_expr *) + (* int * int -> nut -> KK.rel_expr *) and to_atom (x as (k, j0)) u = case rep_of u of Formula _ => atom_from_formula kk j0 (to_f u) - | Unit => if k = 1 then Kodkod.Atom j0 + | Unit => if k = 1 then KK.Atom j0 else raise NUT ("Nitpick_Kodkod.to_atom", [u]) | R => atom_from_rel_expr kk x R (to_r u) - (* rep list -> nut -> Kodkod.rel_expr *) + (* rep list -> nut -> KK.rel_expr *) and to_struct Rs u = case rep_of u of Unit => full_rel_for_rep (Struct Rs) | R' => struct_from_rel_expr kk Rs R' (to_r u) - (* int -> rep -> nut -> Kodkod.rel_expr *) + (* int -> rep -> nut -> KK.rel_expr *) and to_vect k R u = case rep_of u of Unit => full_rel_for_rep (Vect (k, R)) | R' => vect_from_rel_expr kk k R R' (to_r u) - (* rep -> rep -> nut -> Kodkod.rel_expr *) + (* rep -> rep -> nut -> KK.rel_expr *) and to_func R1 R2 u = case rep_of u of Unit => full_rel_for_rep (Func (R1, R2)) | R' => rel_expr_to_func kk R1 R2 R' (to_r u) - (* rep -> nut -> Kodkod.rel_expr *) + (* rep -> nut -> KK.rel_expr *) and to_opt R u = let val old_R = rep_of u in if is_opt_rep old_R then @@ -1708,16 +1691,16 @@ else to_rep R u end - (* rep -> nut -> Kodkod.rel_expr *) + (* rep -> nut -> KK.rel_expr *) and to_rep (Atom x) u = to_atom x u | to_rep (Struct Rs) u = to_struct Rs u | to_rep (Vect (k, R)) u = to_vect k R u | to_rep (Func (R1, R2)) u = to_func R1 R2 u | to_rep (Opt R) u = to_opt R u | to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R]) - (* nut -> Kodkod.rel_expr *) + (* nut -> KK.rel_expr *) and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u - (* nut list -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *) + (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *) and to_guard guard_us R r = let val unpacked_rs = unpack_joins r @@ -1737,16 +1720,16 @@ else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r end - (* rep -> rep -> Kodkod.rel_expr -> int -> Kodkod.rel_expr *) + (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *) and to_project new_R old_R r j0 = rel_expr_from_rel_expr kk new_R old_R (kk_project_seq r j0 (arity_of_rep old_R)) - (* rep list -> nut list -> Kodkod.rel_expr *) + (* rep list -> nut list -> KK.rel_expr *) and to_product Rs us = case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of [] => raise REP ("Nitpick_Kodkod.to_product", Rs) | rs => fold1 kk_product rs - (* int -> typ -> rep -> nut -> Kodkod.rel_expr *) + (* int -> typ -> rep -> nut -> KK.rel_expr *) and to_nth_pair_sel n res_T res_R u = case u of Tuple (_, _, us) => to_rep res_R (nth us n) @@ -1774,9 +1757,9 @@ (to_rep res_R (Cst (Unity, res_T, Unit))) | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0 end - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> nut -> nut - -> Kodkod.formula *) + (* (KK.formula -> KK.formula -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut + -> KK.formula *) and to_set_bool_op connective set_oper u1 u2 = let val min_R = min_rep (rep_of u1) (rep_of u2) @@ -1792,12 +1775,12 @@ (kk_join r2 true_atom) | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]) end - (* (Kodkod.formula -> Kodkod.formula -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) - -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.formula) -> bool -> rep - -> nut -> nut -> Kodkod.rel_expr *) + (* (KK.formula -> KK.formula -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) + -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut + -> nut -> KK.rel_expr *) and to_set_op connective connective3 set_oper true_set_oper false_set_oper neg_second R u1 u2 = let @@ -1829,51 +1812,47 @@ r1 r2 | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R])) end - (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *) + (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *) and to_bit_word_unary_op T R oper = let val Ts = strip_type T ||> single |> op @ - (* int -> Kodkod.int_expr *) - fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j)) + (* int -> KK.int_expr *) + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j)) in kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R)) - (Kodkod.FormulaLet - (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1), - Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0)))) + (KK.FormulaLet + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1), + KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0)))) end - (* typ -> rep - -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option - -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option - -> Kodkod.rel_expr *) + (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option + -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *) and to_bit_word_binary_op T R opt_guard opt_oper = let val Ts = strip_type T ||> single |> op @ - (* int -> Kodkod.int_expr *) - fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j)) + (* int -> KK.int_expr *) + fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j)) in kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R)) - (Kodkod.FormulaLet - (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2), + (KK.FormulaLet + (map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 2), fold1 kk_and ((case opt_guard of NONE => [] | SOME guard => - [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1) - (Kodkod.IntReg 2)]) @ + [guard (KK.IntReg 0) (KK.IntReg 1) (KK.IntReg 2)]) @ (case opt_oper of NONE => [] | SOME oper => - [Kodkod.IntEq (Kodkod.IntReg 2, - oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))])))) + [KK.IntEq (KK.IntReg 2, + oper (KK.IntReg 0) (KK.IntReg 1))])))) end - (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *) + (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *) and to_apply res_R func_u arg_u = case unopt_rep (rep_of func_u) of Unit => let val j0 = offset_of_type ofs (type_of func_u) in to_guard [arg_u] res_R - (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) - (Kodkod.Atom j0)) + (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (KK.Atom j0)) end | Atom (1, j0) => to_guard [arg_u] res_R @@ -1902,7 +1881,7 @@ (kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u)) |> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R | _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u]) - (* int -> rep -> rep -> Kodkod.rel_expr -> nut *) + (* int -> rep -> rep -> KK.rel_expr -> nut *) and to_apply_vect k R' res_R func_r arg_u = let val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u)) @@ -1912,11 +1891,10 @@ kk_case_switch kk arg_R res_R (to_opt arg_R arg_u) (all_singletons_for_rep arg_R) vect_rs end - (* bool -> nut -> Kodkod.formula *) + (* bool -> nut -> KK.formula *) and to_could_be_unrep neg u = - if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) - else Kodkod.False - (* nut -> Kodkod.rel_expr -> Kodkod.rel_expr *) + if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False + (* nut -> KK.rel_expr -> KK.rel_expr *) and to_compare_with_unrep u r = if is_opt_rep (rep_of u) then kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u)) diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Dec 18 12:00:29 2009 +0100 @@ -40,6 +40,8 @@ open Nitpick_Rep open Nitpick_Nut +structure KK = Kodkod + type params = { show_skolems: bool, show_datatypes: bool, @@ -71,19 +73,22 @@ else Const (atom_name "" T j, T) +(* term -> real *) +fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) = + real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) + | extract_real_number t = real (snd (HOLogic.dest_number t)) (* term * term -> order *) fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) - | nice_term_ord (t1, t2) = - int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2)) + | nice_term_ord tp = Real.compare (pairself extract_real_number tp) handle TERM ("dest_number", _) => - case (t1, t2) of + case tp of (t11 $ t12, t21 $ t22) => (case nice_term_ord (t11, t21) of EQUAL => nice_term_ord (t12, t22) | ord => ord) - | _ => TermOrd.term_ord (t1, t2) + | _ => TermOrd.fast_term_ord tp -(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *) +(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *) fun tuple_list_for_name rel_table bounds name = the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] @@ -240,8 +245,8 @@ | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) (* string * string * string * string -> scope -> nut list -> nut list - -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ - -> rep -> int list list -> term *) + -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep + -> int list list -> term *) fun reconstruct_term (maybe_name, base_name, step_name, abs_name) ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...} : scope) sel_names rel_table bounds = @@ -324,7 +329,7 @@ | _ => t (* bool -> typ -> typ -> typ -> term list -> term list -> term *) fun make_fun maybe_opt T1 T2 T' ts1 ts2 = - ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev + ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst) |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2 |> unbit_and_unbox_term |> typecast_fun (unbit_and_unbox_type T') @@ -506,7 +511,7 @@ oooo term_for_rep [] end -(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut +(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut -> term *) fun term_for_name scope sel_names rel_table bounds name = let val T = type_of name in @@ -563,7 +568,7 @@ end (* params -> scope -> (term option * int list) list -> styp list -> nut list - -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list + -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> Pretty.T * bool *) fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts} ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms, @@ -704,7 +709,7 @@ end (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table - -> Kodkod.raw_bound list -> term -> bool option *) + -> KK.raw_bound list -> term -> bool option *) fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...}) auto_timeout free_names sel_names rel_table bounds prop = let diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Dec 18 12:00:29 2009 +0100 @@ -130,6 +130,8 @@ open Nitpick_Peephole open Nitpick_Rep +structure KK = Kodkod + datatype cst = Unity | False | @@ -196,8 +198,8 @@ BoundName of int * typ * rep * string | FreeName of string * typ * rep | ConstName of string * typ * rep | - BoundRel of Kodkod.n_ary_index * typ * rep * string | - FreeRel of Kodkod.n_ary_index * typ * rep * string | + BoundRel of KK.n_ary_index * typ * rep * string | + FreeRel of KK.n_ary_index * typ * rep * string | RelReg of int * typ * rep | FormulaReg of int * typ * rep @@ -439,7 +441,7 @@ case NameTable.lookup table name of SOME u => u | NONE => raise NUT ("Nitpick_Nut.the_name", [name]) -(* nut NameTable.table -> nut -> Kodkod.n_ary_index *) +(* nut NameTable.table -> nut -> KK.n_ary_index *) fun the_rel table name = case the_name table name of FreeRel (x, _, _, _) => x @@ -915,10 +917,8 @@ | Cst (True, T, _) => Cst (True, T, Formula Neut) | Cst (Num j, T, _) => if is_word_type T then - if is_twos_complement_representable bits j then - Cst (Num j, T, best_non_opt_set_rep_for_type scope T) - else - Cst (Unrep, T, best_opt_set_rep_for_type scope T) + Cst (if is_twos_complement_representable bits j then Num j + else Unrep, T, best_opt_set_rep_for_type scope T) else (case spec_of_type scope T of (1, j0) => if j = 0 then Cst (Unity, T, Unit) @@ -1239,8 +1239,8 @@ |> optimize_unit in aux table def Pos end -(* int -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list - -> int * Kodkod.n_ary_index list *) +(* int -> KK.n_ary_index list -> KK.n_ary_index list + -> int * KK.n_ary_index list *) fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys) | fresh_n_ary_index n ((m, j) :: xs) ys = if m = n then (j, ys @ ((m, j + 1) :: xs)) diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Dec 18 12:00:29 2009 +0100 @@ -266,7 +266,7 @@ (* bool -> int *) val from_bool = atom_for_bool main_j0 - (* int -> Kodkod.rel_expr *) + (* int -> rel_expr *) fun from_nat n = Atom (n + main_j0) val from_int = Atom o atom_for_int (int_card, main_j0) (* int -> int *) @@ -347,7 +347,7 @@ (* rel_expr -> formula *) fun s_no None = True | s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2) - | s_no (Intersect (Closure (Kodkod.Rel x), Kodkod.Iden)) = Acyclic x + | s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x | s_no r = if is_one_rel_expr r then False else No r fun s_lone None = True | s_lone r = if is_one_rel_expr r then True else Lone r @@ -409,8 +409,8 @@ s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2) else RelEq (r1, r2) - | (_, Kodkod.None) => s_no r1 - | (Kodkod.None, _) => s_no r2 + | (_, None) => s_no r1 + | (None, _) => s_no r2 | _ => RelEq (r1, r2) fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2) | s_subset (Atom j) (AtomSeq (k, j0)) = diff -r 7aac4d74bb76 -r 8a2c5d7aff51 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Dec 17 15:22:27 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Dec 18 12:00:29 2009 +0100 @@ -249,6 +249,10 @@ [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)] else if T = @{typ signed_bit} then [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)] + else if T = @{typ "unsigned_bit word"} then + [(Card T, lookup_type_ints_assign thy cards_assigns nat_T)] + else if T = @{typ "signed_bit word"} then + [(Card T, lookup_type_ints_assign thy cards_assigns int_T)] else if T = @{typ bisim_iterator} then [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)] else if is_fp_iterator_type T then @@ -316,32 +320,20 @@ [] => false | xs => let - val exact_cards = - map (Integer.prod - o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns) + val dom_cards = + map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns) o binder_types o snd) xs val maxes = map (constr_max max_assigns) xs (* int -> int -> int *) - fun effective_max 0 ~1 = k - | effective_max 0 max = max - | effective_max card ~1 = card + fun effective_max card ~1 = card | effective_max card max = Int.min (card, max) - val max = map2 effective_max exact_cards maxes |> Integer.sum - (* unit -> int *) - fun doms_card () = - xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns) - o binder_types o snd) - |> Integer.sum - in - max < k - orelse (forall (not_equal 0) exact_cards andalso doms_card () < k) - end - handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false - -(* extended_context -> scope_desc -> bool *) -fun is_surely_inconsistent_scope_description ext_ctxt - (desc as (card_assigns, _)) = - exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns + val max = map2 effective_max dom_cards maxes |> Integer.sum + in max < k end +(* extended_context -> (typ * int) list -> (typ * int) list + -> (styp * int) list -> bool *) +fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns = + exists (is_surely_inconsistent_card_assign ext_ctxt + (seen @ rest, max_assigns)) seen (* extended_context -> scope_desc -> (typ * int) list option *) fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) = @@ -349,15 +341,15 @@ (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) fun aux seen [] = SOME seen | aux seen ((T, 0) :: _) = NONE - | aux seen ((T, k) :: assigns) = - (if is_surely_inconsistent_scope_description ext_ctxt - ((T, k) :: seen, max_assigns) then + | aux seen ((T, k) :: rest) = + (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen) + rest max_assigns then raise SAME () else - case aux ((T, k) :: seen) assigns of + case aux ((T, k) :: seen) rest of SOME assigns => SOME assigns | NONE => raise SAME ()) - handle SAME () => aux seen ((T, k - 1) :: assigns) + handle SAME () => aux seen ((T, k - 1) :: rest) in aux [] (rev card_assigns) end (* theory -> (typ * int) list -> typ * int -> typ * int *)