--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Oct 22 14:51:47 2009 +0200
@@ -0,0 +1,643 @@
+(* Title: HOL/Nitpick/Tools/nitpick_peephole.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2008, 2009
+
+Peephole optimizer for Nitpick.
+*)
+
+signature NITPICK_PEEPHOLE =
+sig
+ type formula = Kodkod.formula
+ type int_expr = Kodkod.int_expr
+ type rel_expr = Kodkod.rel_expr
+ type decl = Kodkod.decl
+ type expr_assign = Kodkod.expr_assign
+
+ type name_pool = {
+ rels: Kodkod.n_ary_index list,
+ vars: Kodkod.n_ary_index list,
+ formula_reg: int,
+ rel_reg: int}
+
+ val initial_pool : name_pool
+ val not3_rel : rel_expr
+ val suc_rel : rel_expr
+ val nat_add_rel : rel_expr
+ val int_add_rel : rel_expr
+ val nat_subtract_rel : rel_expr
+ val int_subtract_rel : rel_expr
+ val nat_multiply_rel : rel_expr
+ val int_multiply_rel : rel_expr
+ val nat_divide_rel : rel_expr
+ val int_divide_rel : rel_expr
+ val nat_modulo_rel : rel_expr
+ val int_modulo_rel : rel_expr
+ val nat_less_rel : rel_expr
+ val int_less_rel : rel_expr
+ val gcd_rel : rel_expr
+ val lcm_rel : rel_expr
+ val norm_frac_rel : rel_expr
+ val atom_for_bool : int -> bool -> rel_expr
+ val formula_for_bool : bool -> formula
+ val atom_for_nat : int * int -> int -> int
+ val min_int_for_card : int -> int
+ val max_int_for_card : int -> int
+ val int_for_atom : int * int -> int -> int
+ val atom_for_int : int * int -> int -> int
+ val inline_rel_expr : rel_expr -> bool
+ val empty_n_ary_rel : int -> rel_expr
+ val num_seq : int -> int -> int_expr list
+ val s_and : formula -> formula -> formula
+
+ type kodkod_constrs = {
+ kk_all: decl list -> formula -> formula,
+ kk_exist: decl list -> formula -> formula,
+ kk_formula_let: expr_assign list -> formula -> formula,
+ kk_formula_if: formula -> formula -> formula -> formula,
+ kk_or: formula -> formula -> formula,
+ kk_not: formula -> formula,
+ kk_iff: formula -> formula -> formula,
+ kk_implies: formula -> formula -> formula,
+ kk_and: formula -> formula -> formula,
+ kk_subset: rel_expr -> rel_expr -> formula,
+ kk_rel_eq: rel_expr -> rel_expr -> formula,
+ kk_no: rel_expr -> formula,
+ kk_lone: rel_expr -> formula,
+ kk_one: rel_expr -> formula,
+ kk_some: rel_expr -> formula,
+ kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+ kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+ kk_union: rel_expr -> rel_expr -> rel_expr,
+ kk_difference: rel_expr -> rel_expr -> rel_expr,
+ kk_override: rel_expr -> rel_expr -> rel_expr,
+ kk_intersect: rel_expr -> rel_expr -> rel_expr,
+ kk_product: rel_expr -> rel_expr -> rel_expr,
+ kk_join: rel_expr -> rel_expr -> rel_expr,
+ kk_closure: rel_expr -> rel_expr,
+ kk_reflexive_closure: rel_expr -> rel_expr,
+ kk_comprehension: decl list -> formula -> rel_expr,
+ kk_project: rel_expr -> int_expr list -> rel_expr,
+ kk_project_seq: rel_expr -> int -> int -> rel_expr,
+ kk_not3: rel_expr -> rel_expr,
+ kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+ kk_int_less: rel_expr -> rel_expr -> rel_expr
+ }
+
+ val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
+end;
+
+structure NitpickPeephole : NITPICK_PEEPHOLE =
+struct
+
+open Kodkod
+open NitpickUtil
+
+type name_pool = {
+ rels: n_ary_index list,
+ vars: n_ary_index list,
+ formula_reg: int,
+ rel_reg: int}
+
+(* If you add new built-in relations, make sure to increment the counters here
+ as well to avoid name clashes (which fortunately would be detected by
+ Kodkodi). *)
+val initial_pool =
+ {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
+ rel_reg = 10}
+
+val not3_rel = Rel (2, 0)
+val suc_rel = Rel (2, 1)
+val nat_add_rel = Rel (3, 0)
+val int_add_rel = Rel (3, 1)
+val nat_subtract_rel = Rel (3, 2)
+val int_subtract_rel = Rel (3, 3)
+val nat_multiply_rel = Rel (3, 4)
+val int_multiply_rel = Rel (3, 5)
+val nat_divide_rel = Rel (3, 6)
+val int_divide_rel = Rel (3, 7)
+val nat_modulo_rel = Rel (3, 8)
+val int_modulo_rel = Rel (3, 9)
+val nat_less_rel = Rel (3, 10)
+val int_less_rel = Rel (3, 11)
+val gcd_rel = Rel (3, 12)
+val lcm_rel = Rel (3, 13)
+val norm_frac_rel = Rel (4, 0)
+
+(* int -> bool -> rel_expr *)
+fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
+(* bool -> formula *)
+fun formula_for_bool b = if b then True else False
+
+(* int * int -> int -> int *)
+fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
+(* int -> int *)
+fun min_int_for_card k = ~k div 2 + 1
+fun max_int_for_card k = k div 2
+(* int * int -> int -> int *)
+fun int_for_atom (k, j0) j =
+ let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
+fun atom_for_int (k, j0) n =
+ if n < min_int_for_card k orelse n > max_int_for_card k then ~1
+ else if n < 0 then n + k + j0
+ else n + j0
+
+(* rel_expr -> bool *)
+fun is_none_product (Product (r1, r2)) =
+ is_none_product r1 orelse is_none_product r2
+ | is_none_product None = true
+ | is_none_product _ = false
+
+(* rel_expr -> bool *)
+fun is_one_rel_expr (Atom _) = true
+ | is_one_rel_expr (AtomSeq (1, _)) = true
+ | is_one_rel_expr (Var _) = true
+ | is_one_rel_expr _ = false
+
+(* rel_expr -> bool *)
+fun inline_rel_expr (Product (r1, r2)) =
+ inline_rel_expr r1 andalso inline_rel_expr r2
+ | inline_rel_expr Iden = true
+ | inline_rel_expr Ints = true
+ | inline_rel_expr None = true
+ | inline_rel_expr Univ = true
+ | inline_rel_expr (Atom _) = true
+ | inline_rel_expr (AtomSeq _) = true
+ | inline_rel_expr (Rel _) = true
+ | inline_rel_expr (Var _) = true
+ | inline_rel_expr (RelReg _) = true
+ | inline_rel_expr _ = false
+
+(* rel_expr -> rel_expr -> bool option *)
+fun rel_expr_equal None (Atom _) = SOME false
+ | rel_expr_equal None (AtomSeq (k, _)) = SOME (k = 0)
+ | rel_expr_equal (Atom _) None = SOME false
+ | rel_expr_equal (AtomSeq (k, _)) None = SOME (k = 0)
+ | rel_expr_equal (Atom j1) (Atom j2) = SOME (j1 = j2)
+ | rel_expr_equal (Atom j) (AtomSeq (k, j0)) = SOME (j = j0 andalso k = 1)
+ | rel_expr_equal (AtomSeq (k, j0)) (Atom j) = SOME (j = j0 andalso k = 1)
+ | rel_expr_equal (AtomSeq x1) (AtomSeq x2) = SOME (x1 = x2)
+ | rel_expr_equal r1 r2 = if r1 = r2 then SOME true else NONE
+
+(* rel_expr -> rel_expr -> bool option *)
+fun rel_expr_intersects (Atom j1) (Atom j2) = SOME (j1 = j2)
+ | rel_expr_intersects (Atom j) (AtomSeq (k, j0)) = SOME (j < j0 + k)
+ | rel_expr_intersects (AtomSeq (k, j0)) (Atom j) = SOME (j < j0 + k)
+ | rel_expr_intersects (AtomSeq (k1, j01)) (AtomSeq (k2, j02)) =
+ SOME (k1 > 0 andalso k2 > 0 andalso j01 + k1 > j02 andalso j02 + k2 > j01)
+ | rel_expr_intersects r1 r2 =
+ if is_none_product r1 orelse is_none_product r2 then SOME false else NONE
+
+(* int -> rel_expr *)
+fun empty_n_ary_rel 0 = raise ARG ("NitpickPeephole.empty_n_ary_rel", "0")
+ | empty_n_ary_rel n = funpow (n - 1) (curry Product None) None
+
+(* decl -> rel_expr *)
+fun decl_one_set (DeclOne (_, r)) = r
+ | decl_one_set _ =
+ raise ARG ("NitpickPeephole.decl_one_set", "not \"DeclOne\"")
+
+(* int_expr -> bool *)
+fun is_Num (Num _) = true
+ | is_Num _ = false
+(* int_expr -> int *)
+fun dest_Num (Num k) = k
+ | dest_Num _ = raise ARG ("NitpickPeephole.dest_Num", "not \"Num\"")
+(* int -> int -> int_expr list *)
+fun num_seq j0 n = map Num (index_seq j0 n)
+
+(* rel_expr -> rel_expr -> bool *)
+fun occurs_in_union r (Union (r1, r2)) =
+ occurs_in_union r r1 orelse occurs_in_union r r2
+ | occurs_in_union r r' = (r = r')
+
+(* rel_expr -> rel_expr -> rel_expr *)
+fun s_and True f2 = f2
+ | s_and False _ = False
+ | s_and f1 True = f1
+ | s_and _ False = False
+ | s_and f1 f2 = And (f1, f2)
+
+type kodkod_constrs = {
+ kk_all: decl list -> formula -> formula,
+ kk_exist: decl list -> formula -> formula,
+ kk_formula_let: expr_assign list -> formula -> formula,
+ kk_formula_if: formula -> formula -> formula -> formula,
+ kk_or: formula -> formula -> formula,
+ kk_not: formula -> formula,
+ kk_iff: formula -> formula -> formula,
+ kk_implies: formula -> formula -> formula,
+ kk_and: formula -> formula -> formula,
+ kk_subset: rel_expr -> rel_expr -> formula,
+ kk_rel_eq: rel_expr -> rel_expr -> formula,
+ kk_no: rel_expr -> formula,
+ kk_lone: rel_expr -> formula,
+ kk_one: rel_expr -> formula,
+ kk_some: rel_expr -> formula,
+ kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+ kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+ kk_union: rel_expr -> rel_expr -> rel_expr,
+ kk_difference: rel_expr -> rel_expr -> rel_expr,
+ kk_override: rel_expr -> rel_expr -> rel_expr,
+ kk_intersect: rel_expr -> rel_expr -> rel_expr,
+ kk_product: rel_expr -> rel_expr -> rel_expr,
+ kk_join: rel_expr -> rel_expr -> rel_expr,
+ kk_closure: rel_expr -> rel_expr,
+ kk_reflexive_closure: rel_expr -> rel_expr,
+ kk_comprehension: decl list -> formula -> rel_expr,
+ kk_project: rel_expr -> int_expr list -> rel_expr,
+ kk_project_seq: rel_expr -> int -> int -> rel_expr,
+ kk_not3: rel_expr -> rel_expr,
+ kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+ kk_int_less: rel_expr -> rel_expr -> rel_expr
+}
+
+(* We assume throughout that Kodkod variables have a "one" constraint. This is
+ always the case if Kodkod's skolemization is disabled. *)
+(* bool -> int -> int -> int -> kodkod_constrs *)
+fun kodkod_constrs optim nat_card int_card main_j0 =
+ let
+ val false_atom = Atom main_j0
+ val true_atom = Atom (main_j0 + 1)
+
+ (* bool -> int *)
+ val from_bool = atom_for_bool main_j0
+ (* int -> Kodkod.rel_expr *)
+ fun from_nat n = Atom (n + main_j0)
+ val from_int = Atom o atom_for_int (int_card, main_j0)
+ (* int -> int *)
+ fun to_nat j = j - main_j0
+ val to_int = int_for_atom (int_card, main_j0)
+
+ (* decl list -> formula -> formula *)
+ fun s_all _ True = True
+ | s_all _ False = False
+ | s_all [] f = f
+ | s_all ds (All (ds', f)) = All (ds @ ds', f)
+ | s_all ds f = All (ds, f)
+ fun s_exist _ True = True
+ | s_exist _ False = False
+ | s_exist [] f = f
+ | s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
+ | s_exist ds f = Exist (ds, f)
+
+ (* expr_assign list -> formula -> formula *)
+ fun s_formula_let _ True = True
+ | s_formula_let _ False = False
+ | s_formula_let assigns f = FormulaLet (assigns, f)
+
+ (* formula -> formula *)
+ fun s_not True = False
+ | s_not False = True
+ | s_not (All (ds, f)) = Exist (ds, s_not f)
+ | s_not (Exist (ds, f)) = All (ds, s_not f)
+ | s_not (Or (f1, f2)) = And (s_not f1, s_not f2)
+ | s_not (Implies (f1, f2)) = And (f1, s_not f2)
+ | s_not (And (f1, f2)) = Or (s_not f1, s_not f2)
+ | s_not (Not f) = f
+ | s_not (No r) = Some r
+ | s_not (Some r) = No r
+ | s_not f = Not f
+
+ (* formula -> formula -> formula *)
+ fun s_or True _ = True
+ | s_or False f2 = f2
+ | s_or _ True = True
+ | s_or f1 False = f1
+ | s_or f1 f2 = if f1 = f2 then f1 else Or (f1, f2)
+ fun s_iff True f2 = f2
+ | s_iff False f2 = s_not f2
+ | s_iff f1 True = f1
+ | s_iff f1 False = s_not f1
+ | s_iff f1 f2 = if f1 = f2 then True else Iff (f1, f2)
+ fun s_implies True f2 = f2
+ | s_implies False _ = True
+ | s_implies _ True = True
+ | s_implies f1 False = s_not f1
+ | s_implies f1 f2 = if f1 = f2 then True else Implies (f1, f2)
+
+ (* formula -> formula -> formula -> formula *)
+ fun s_formula_if True f2 _ = f2
+ | s_formula_if False _ f3 = f3
+ | s_formula_if f1 True f3 = s_or f1 f3
+ | s_formula_if f1 False f3 = s_and (s_not f1) f3
+ | s_formula_if f1 f2 True = s_implies f1 f2
+ | s_formula_if f1 f2 False = s_and f1 f2
+ | s_formula_if f f1 f2 = FormulaIf (f, f1, f2)
+
+ (* rel_expr -> int_expr list -> rel_expr *)
+ fun s_project r is =
+ (case r of
+ Project (r1, is') =>
+ if forall is_Num is then
+ s_project r1 (map (nth is' o dest_Num) is)
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let val n = length is in
+ if arity_of_rel_expr r = n andalso is = num_seq 0 n then r
+ else Project (r, is)
+ end
+
+ (* 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 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
+ fun s_one None = False
+ | s_one r =
+ if is_one_rel_expr r then
+ True
+ else if inline_rel_expr r then
+ case arity_of_rel_expr r of
+ 1 => One r
+ | arity => foldl1 And (map (One o s_project r o single o Num)
+ (index_seq 0 arity))
+ else
+ One r
+ fun s_some None = False
+ | s_some (Atom _) = True
+ | s_some (Product (r1, r2)) = s_and (s_some r1) (s_some r2)
+ | s_some r = if is_one_rel_expr r then True else Some r
+
+ (* rel_expr -> rel_expr *)
+ fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1)
+ | s_not3 (r as Join (r1, r2)) =
+ if r2 = not3_rel then r1 else Join (r, not3_rel)
+ | s_not3 r = Join (r, not3_rel)
+
+ (* rel_expr -> rel_expr -> formula *)
+ fun s_rel_eq r1 r2 =
+ (case (r1, r2) of
+ (Join (r11, r12), _) =>
+ if r12 = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
+ | (_, Join (r21, r22)) =>
+ if r22 = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ case rel_expr_equal r1 r2 of
+ SOME true => True
+ | SOME false => False
+ | NONE =>
+ case (r1, r2) of
+ (_, RelIf (f, r21, r22)) =>
+ if inline_rel_expr r1 then
+ s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22)
+ else
+ RelEq (r1, r2)
+ | (RelIf (f, r11, r12), _) =>
+ if inline_rel_expr r2 then
+ 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
+ | _ => RelEq (r1, r2)
+ fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
+ | s_subset (Atom j) (AtomSeq (k, j0)) =
+ formula_for_bool (j >= j0 andalso j < j0 + k)
+ | s_subset (r1 as Union (r11, r12)) r2 =
+ s_and (s_subset r11 r2) (s_subset r12 r2)
+ | s_subset r1 (r2 as Union (r21, r22)) =
+ if is_one_rel_expr r1 then
+ s_or (s_subset r1 r21) (s_subset r1 r22)
+ else
+ if s_subset r1 r21 = True orelse s_subset r1 r22 = True
+ orelse r1 = r2 then
+ True
+ else
+ Subset (r1, r2)
+ | s_subset r1 r2 =
+ if r1 = r2 orelse is_none_product r1 then True
+ else if is_none_product r2 then s_no r1
+ else if forall is_one_rel_expr [r1, r2] then s_rel_eq r1 r2
+ else Subset (r1, r2)
+
+ (* expr_assign list -> rel_expr -> rel_expr *)
+ fun s_rel_let [b as AssignRelReg (x', r')] (r as RelReg x) =
+ if x = x' then r' else RelLet ([b], r)
+ | s_rel_let bs r = RelLet (bs, r)
+
+ (* formula -> rel_expr -> rel_expr -> rel_expr *)
+ fun s_rel_if f r1 r2 =
+ (case (f, r1, r2) of
+ (True, _, _) => r1
+ | (False, _, _) => r2
+ | (No r1', None, RelIf (One r2', r3', r4')) =>
+ if r1' = r2' andalso r2' = r3' then s_rel_if (Lone r1') r1' r4'
+ else raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () => if r1 = r2 then r1 else RelIf (f, r1, r2)
+
+ (* rel_expr -> rel_expr -> rel_expr *)
+ fun s_union r1 (Union (r21, r22)) = s_union (s_union r1 r21) r22
+ | s_union r1 r2 =
+ if is_none_product r1 then r2
+ else if is_none_product r2 then r1
+ else if r1 = r2 then r1
+ else if occurs_in_union r2 r1 then r1
+ else Union (r1, r2)
+ fun s_difference r1 r2 =
+ if is_none_product r1 orelse is_none_product r2 then r1
+ else if r1 = r2 then empty_n_ary_rel (arity_of_rel_expr r1)
+ else Difference (r1, r2)
+ fun s_override r1 r2 =
+ if is_none_product r2 then r1
+ else if is_none_product r1 then r2
+ else Override (r1, r2)
+ fun s_intersect r1 r2 =
+ case rel_expr_intersects r1 r2 of
+ SOME true => if r1 = r2 then r1 else Intersect (r1, r2)
+ | SOME false => empty_n_ary_rel (arity_of_rel_expr r1)
+ | NONE => if is_none_product r1 then r1
+ else if is_none_product r2 then r2
+ else Intersect (r1, r2)
+ fun s_product r1 r2 =
+ if is_none_product r1 then
+ Product (r1, empty_n_ary_rel (arity_of_rel_expr r2))
+ else if is_none_product r2 then
+ Product (empty_n_ary_rel (arity_of_rel_expr r1), r2)
+ else
+ Product (r1, r2)
+ fun s_join r1 (Product (Product (r211, r212), r22)) =
+ Product (s_join r1 (Product (r211, r212)), r22)
+ | s_join (Product (r11, Product (r121, r122))) r2 =
+ Product (r11, s_join (Product (r121, r122)) r2)
+ | s_join None r = empty_n_ary_rel (arity_of_rel_expr r - 1)
+ | s_join r None = empty_n_ary_rel (arity_of_rel_expr r - 1)
+ | s_join (Product (None, None)) r = empty_n_ary_rel (arity_of_rel_expr r)
+ | s_join r (Product (None, None)) = empty_n_ary_rel (arity_of_rel_expr r)
+ | s_join Iden r2 = r2
+ | s_join r1 Iden = r1
+ | s_join (Product (r1, r2)) Univ =
+ if arity_of_rel_expr r2 = 1 then r1
+ else Product (r1, s_join r2 Univ)
+ | s_join Univ (Product (r1, r2)) =
+ if arity_of_rel_expr r1 = 1 then r2
+ else Product (s_join Univ r1, r2)
+ | s_join r1 (r2 as Product (r21, r22)) =
+ if arity_of_rel_expr r1 = 1 then
+ case rel_expr_intersects r1 r21 of
+ SOME true => r22
+ | SOME false => empty_n_ary_rel (arity_of_rel_expr r2 - 1)
+ | NONE => Join (r1, r2)
+ else
+ Join (r1, r2)
+ | s_join (r1 as Product (r11, r12)) r2 =
+ if arity_of_rel_expr r2 = 1 then
+ case rel_expr_intersects r2 r12 of
+ SOME true => r11
+ | SOME false => empty_n_ary_rel (arity_of_rel_expr r1 - 1)
+ | NONE => Join (r1, r2)
+ else
+ Join (r1, r2)
+ | s_join r1 (r2 as RelIf (f, r21, r22)) =
+ if inline_rel_expr r1 then s_rel_if f (s_join r1 r21) (s_join r1 r22)
+ else Join (r1, r2)
+ | s_join (r1 as RelIf (f, r11, r12)) r2 =
+ if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
+ else Join (r1, r2)
+ | s_join (r1 as Atom j1) (r2 as Rel (2, j2)) =
+ if r2 = suc_rel then
+ let val n = to_nat j1 + 1 in
+ if n < nat_card then from_nat n else None
+ end
+ else
+ Join (r1, r2)
+ | s_join r1 (r2 as Project (r21, Num k :: is)) =
+ if k = arity_of_rel_expr r21 - 1 andalso arity_of_rel_expr r1 = 1 then
+ s_project (s_join r21 r1) is
+ else
+ Join (r1, r2)
+ | s_join r1 (Join (r21, r22 as Rel (3, j22))) =
+ ((if r22 = nat_add_rel then
+ case (r21, r1) of
+ (Atom j1, Atom j2) =>
+ let val n = to_nat j1 + to_nat j2 in
+ if n < nat_card then from_nat n else None
+ end
+ | (Atom j, r) =>
+ (case to_nat j of
+ 0 => r
+ | 1 => s_join r suc_rel
+ | _ => raise SAME ())
+ | (r, Atom j) =>
+ (case to_nat j of
+ 0 => r
+ | 1 => s_join r suc_rel
+ | _ => raise SAME ())
+ | _ => raise SAME ()
+ else if r22 = nat_subtract_rel then
+ case (r21, r1) of
+ (Atom j1, Atom j2) => from_nat (to_nat j1 nat_minus to_nat j2)
+ | _ => raise SAME ()
+ else if r22 = nat_multiply_rel then
+ case (r21, r1) of
+ (Atom j1, Atom j2) =>
+ let val n = to_nat j1 * to_nat j2 in
+ if n < nat_card then from_nat n else None
+ end
+ | (Atom j, r) =>
+ (case to_nat j of 0 => Atom j | 1 => r | _ => raise SAME ())
+ | (r, Atom j) =>
+ (case to_nat j of 0 => Atom j | 1 => r | _ => raise SAME ())
+ | _ => raise SAME ()
+ else
+ raise SAME ())
+ handle SAME () => List.foldr Join r22 [r1, r21])
+ | s_join r1 r2 = Join (r1, r2)
+
+ (* rel_expr -> rel_expr *)
+ fun s_closure Iden = Iden
+ | s_closure r = if is_none_product r then r else Closure r
+ fun s_reflexive_closure Iden = Iden
+ | s_reflexive_closure r =
+ if is_none_product r then Iden else ReflexiveClosure r
+
+ (* decl list -> formula -> rel_expr *)
+ fun s_comprehension ds False = empty_n_ary_rel (length ds)
+ | s_comprehension ds True = fold1 s_product (map decl_one_set ds)
+ | s_comprehension [d as DeclOne ((1, j1), r)]
+ (f as RelEq (Var (1, j2), Atom j)) =
+ if j1 = j2 andalso rel_expr_intersects (Atom j) r = SOME true then
+ Atom j
+ else
+ Comprehension ([d], f)
+ | s_comprehension ds f = Comprehension (ds, f)
+
+ (* rel_expr -> int -> int -> rel_expr *)
+ fun s_project_seq r =
+ let
+ (* int -> rel_expr -> int -> int -> rel_expr *)
+ fun aux arity r j0 n =
+ if j0 = 0 andalso arity = n then
+ r
+ else case r of
+ RelIf (f, r1, r2) =>
+ s_rel_if f (aux arity r1 j0 n) (aux arity r2 j0 n)
+ | Product (r1, r2) =>
+ let
+ val arity2 = arity_of_rel_expr r2
+ val arity1 = arity - arity2
+ val n1 = Int.min (arity1 nat_minus j0, n)
+ val n2 = n - n1
+ (* unit -> rel_expr *)
+ fun one () = aux arity1 r1 j0 n1
+ fun two () = aux arity2 r2 (j0 nat_minus arity1) n2
+ in
+ case (n1, n2) of
+ (0, _) => s_rel_if (s_some r1) (two ()) (empty_n_ary_rel n2)
+ | (_, 0) => s_rel_if (s_some r2) (one ()) (empty_n_ary_rel n1)
+ | _ => s_product (one ()) (two ())
+ end
+ | _ => s_project r (num_seq j0 n)
+ in aux (arity_of_rel_expr r) r end
+
+ (* rel_expr -> rel_expr -> rel_expr *)
+ fun s_nat_subtract r1 r2 = fold s_join [r1, r2] nat_subtract_rel
+ fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
+ | s_nat_less r1 r2 = fold s_join [r1, r2] nat_less_rel
+ fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
+ | s_int_less r1 r2 = fold s_join [r1, r2] int_less_rel
+
+ (* rel_expr -> int -> int -> rel_expr *)
+ fun d_project_seq r j0 n = Project (r, num_seq j0 n)
+ (* rel_expr -> rel_expr *)
+ fun d_not3 r = Join (r, not3_rel)
+ (* rel_expr -> rel_expr -> rel_expr *)
+ fun d_nat_subtract r1 r2 = List.foldl Join nat_subtract_rel [r1, r2]
+ fun d_nat_less r1 r2 = List.foldl Join nat_less_rel [r1, r2]
+ fun d_int_less r1 r2 = List.foldl Join int_less_rel [r1, r2]
+ in
+ if optim then
+ {kk_all = s_all, kk_exist = s_exist, kk_formula_let = s_formula_let,
+ kk_formula_if = s_formula_if, kk_or = s_or, kk_not = s_not,
+ kk_iff = s_iff, kk_implies = s_implies, kk_and = s_and,
+ kk_subset = s_subset, kk_rel_eq = s_rel_eq, kk_no = s_no,
+ kk_lone = s_lone, kk_one = s_one, kk_some = s_some,
+ kk_rel_let = s_rel_let, kk_rel_if = s_rel_if, kk_union = s_union,
+ kk_difference = s_difference, kk_override = s_override,
+ kk_intersect = s_intersect, kk_product = s_product, kk_join = s_join,
+ kk_closure = s_closure, kk_reflexive_closure = s_reflexive_closure,
+ kk_comprehension = s_comprehension, kk_project = s_project,
+ kk_project_seq = s_project_seq, kk_not3 = s_not3,
+ kk_nat_less = s_nat_less, kk_int_less = s_int_less}
+ else
+ {kk_all = curry All, kk_exist = curry Exist,
+ kk_formula_let = curry FormulaLet, kk_formula_if = curry3 FormulaIf,
+ kk_or = curry Or,kk_not = Not, kk_iff = curry Iff, kk_implies = curry
+ Implies, kk_and = curry And, kk_subset = curry Subset, kk_rel_eq = curry
+ RelEq, kk_no = No, kk_lone = Lone, kk_one = One, kk_some = Some,
+ kk_rel_let = curry RelLet, kk_rel_if = curry3 RelIf, kk_union = curry
+ Union, kk_difference = curry Difference, kk_override = curry Override,
+ kk_intersect = curry Intersect, kk_product = curry Product,
+ kk_join = curry Join, kk_closure = Closure,
+ kk_reflexive_closure = ReflexiveClosure, kk_comprehension = curry
+ Comprehension, kk_project = curry Project,
+ kk_project_seq = d_project_seq, kk_not3 = d_not3,
+ kk_nat_less = d_nat_less, kk_int_less = d_int_less}
+ end
+
+end;