SMLBDD

(* Test that words can handle numbers between 0 and 31 *)
val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));

structure Uint32 : sig
  val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
  val shiftl : Word32.word -> IntInf.int -> Word32.word
  val shiftr : Word32.word -> IntInf.int -> Word32.word
  val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
  val test_bit : Word32.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
  let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
  in if b then Word32.orb (x, mask)
     else Word32.andb (x, Word32.notb mask)
  end

fun shiftl x n =
  Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
  Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
  Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
  Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0

end; (* struct Uint32 *)


   fun array_blit src si dst di len = (
      src=dst andalso raise Fail ("array_blit: Same arrays");
      ArraySlice.copy {
        di = IntInf.toInt di,
        src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
        dst = dst})

    fun array_nth_oo v a i () = Array.sub(a,IntInf.toInt i) handle Subscript => v | Overflow => v
    fun array_upd_oo f i x a () = 
      (Array.update(a,IntInf.toInt i,x); a) handle Subscript => f () | Overflow => f ()



structure Bits_Integer : sig
  val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
  val shiftl : IntInf.int -> IntInf.int -> IntInf.int
  val shiftr : IntInf.int -> IntInf.int -> IntInf.int
  val test_bit : IntInf.int -> IntInf.int -> bool
end = struct

val maxWord = IntInf.pow (2, Word.wordSize);

fun set_bit x n b =
  if n < maxWord then
    if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
    else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

fun shiftl x n =
  if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun shiftr x n =
  if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
  else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun test_bit x n =
  if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
  else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

end; (*struct Bits_Integer*)

structure IBDD : sig
  type nat
  type num
  type 'a set
  type char
  type 'a bddi_ext
  val ex_2_3 : (unit -> (char list))
  val bdd_from_sc :
    nat set set -> nat -> unit bddi_ext -> (unit -> (nat * unit bddi_ext))
end = struct

datatype nat = Nat of IntInf.int;

fun integer_of_nat (Nat x) = x;

fun equal_nata m n = (((integer_of_nat m) : IntInf.int) = (integer_of_nat n));

type 'a equal = {equal : 'a -> 'a -> bool};
val equal = #equal : 'a equal -> 'a -> 'a -> bool;

val equal_nat = {equal = equal_nata} : nat equal;

datatype typerepa = Typerep of string * typerepa list;

datatype 'a itself = Type;

fun typerep_nata t = Typerep ("Nat.nat", []);

type 'a typerep = {typerep : 'a itself -> typerepa};
val typerep = #typerep : 'a typerep -> 'a itself -> typerepa;

type 'a countable = {};

type 'a heap = {countable_heap : 'a countable, typerep_heap : 'a typerep};
val countable_heap = #countable_heap : 'a heap -> 'a countable;
val typerep_heap = #typerep_heap : 'a heap -> 'a typerep;

val countable_nat = {} : nat countable;

val typerep_nat = {typerep = typerep_nata} : nat typerep;

val heap_nat = {countable_heap = countable_nat, typerep_heap = typerep_nat} :
  nat heap;

val zero_nata : nat = Nat (0 : IntInf.int);

type 'a zero = {zero : 'a};
val zero = #zero : 'a zero -> 'a;

val zero_nat = {zero = zero_nata} : nat zero;

val default_nata : nat = zero_nata;

type 'a default = {default : 'a};
val default = #default : 'a default -> 'a;

val default_nat = {default = default_nata} : nat default;

fun less_eq_nat m n = IntInf.<= (integer_of_nat m, integer_of_nat n);

type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool;
val less = #less : 'a ord -> 'a -> 'a -> bool;

fun less_nat m n = IntInf.< (integer_of_nat m, integer_of_nat n);

val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat ord;

type 'a preorder = {ord_preorder : 'a ord};
val ord_preorder = #ord_preorder : 'a preorder -> 'a ord;

type 'a order = {preorder_order : 'a preorder};
val preorder_order = #preorder_order : 'a order -> 'a preorder;

val preorder_nat = {ord_preorder = ord_nat} : nat preorder;

val order_nat = {preorder_order = preorder_nat} : nat order;

fun max A_ a b = (if less_eq A_ a b then b else a);

val ord_integer =
  {less_eq = (fn a => fn b => IntInf.<= (a, b)),
    less = (fn a => fn b => IntInf.< (a, b))}
  : IntInf.int ord;

fun nat_of_integer k = Nat (max ord_integer (0 : IntInf.int) k);

datatype num = One | Bit0 of num | Bit1 of num;

fun def_hashmap_size_nat x = (fn _ => nat_of_integer (16 : IntInf.int)) x;

type 'a hashable =
  {hashcode : 'a -> Word32.word, def_hashmap_size : 'a itself -> nat};
val hashcode = #hashcode : 'a hashable -> 'a -> Word32.word;
val def_hashmap_size = #def_hashmap_size : 'a hashable -> 'a itself -> nat;

datatype int = Int_of_integer of IntInf.int;

fun int_of_nat n = Int_of_integer (integer_of_nat n);

fun integer_of_int (Int_of_integer k) = k;

fun uint32_of_int i = Word32.fromLargeInt (IntInf.toLarge (integer_of_int i));

fun hashcode_nat n = uint32_of_int (int_of_nat n);

val hashable_nat =
  {hashcode = hashcode_nat, def_hashmap_size = def_hashmap_size_nat} :
  nat hashable;

type 'a linorder = {order_linorder : 'a order};
val order_linorder = #order_linorder : 'a linorder -> 'a order;

val linorder_nat = {order_linorder = order_nat} : nat linorder;

fun list_all p [] = true
  | list_all p (x :: xs) = p x andalso list_all p xs;

datatype 'a set = Set of 'a list | Coset of 'a list;

fun eq A_ a b = equal A_ a b;

fun membera A_ [] y = false
  | membera A_ (x :: xs) y = eq A_ x y orelse membera A_ xs y;

fun member A_ x (Coset xs) = not (membera A_ xs x)
  | member A_ x (Set xs) = membera A_ xs x;

fun less_eq_set A_ (Coset []) (Set []) = false
  | less_eq_set A_ a (Coset ys) = list_all (fn y => not (member A_ y a)) ys
  | less_eq_set A_ (Set xs) b = list_all (fn x => member A_ x b) xs;

fun equal_seta A_ a b = less_eq_set A_ a b andalso less_eq_set A_ b a;

fun equal_set A_ = {equal = equal_seta A_} : 'a set equal;

fun equal_lista A_ [] (x21 :: x22) = false
  | equal_lista A_ (x21 :: x22) [] = false
  | equal_lista A_ (x21 :: x22) (y21 :: y22) =
    eq A_ x21 y21 andalso equal_lista A_ x22 y22
  | equal_lista A_ [] [] = true;

fun equal_list A_ = {equal = equal_lista A_} : ('a list) equal;

fun typerep_lista A_ t = Typerep ("List.list", [typerep A_ Type]);

fun countable_list A_ = {} : ('a list) countable;

fun typerep_list A_ = {typerep = typerep_lista A_} : ('a list) typerep;

fun heap_list A_ =
  {countable_heap = countable_list (countable_heap A_),
    typerep_heap = typerep_list (typerep_heap A_)}
  : ('a list) heap;

fun equal_bool p true = p
  | equal_bool p false = not p
  | equal_bool true p = p
  | equal_bool false p = not p;

datatype char = Chara of bool * bool * bool * bool * bool * bool * bool * bool;

fun equal_chara (Chara (x1, x2, x3, x4, x5, x6, x7, x8))
  (Chara (y1, y2, y3, y4, y5, y6, y7, y8)) =
  equal_bool x1 y1 andalso
    (equal_bool x2 y2 andalso
      (equal_bool x3 y3 andalso
        (equal_bool x4 y4 andalso
          (equal_bool x5 y5 andalso
            (equal_bool x6 y6 andalso
              (equal_bool x7 y7 andalso equal_bool x8 y8))))));

val equal_char = {equal = equal_chara} : char equal;

fun equal_proda A_ B_ (x1, x2) (y1, y2) = eq A_ x1 y1 andalso eq B_ x2 y2;

fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) equal;

fun typerep_proda A_ B_ t =
  Typerep ("Product_Type.prod", [typerep A_ Type, typerep B_ Type]);

fun countable_prod A_ B_ = {} : ('a * 'b) countable;

fun typerep_prod A_ B_ = {typerep = typerep_proda A_ B_} : ('a * 'b) typerep;

fun heap_prod A_ B_ =
  {countable_heap = countable_prod (countable_heap A_) (countable_heap B_),
    typerep_heap = typerep_prod (typerep_heap A_) (typerep_heap B_)}
  : ('a * 'b) heap;

fun default_proda A_ B_ = (default A_, default B_);

fun default_prod A_ B_ = {default = default_proda A_ B_} : ('a * 'b) default;

fun plus_nat m n = Nat (IntInf.+ (integer_of_nat m, integer_of_nat n));

fun def_hashmap_size_prod A_ B_ =
  (fn _ => plus_nat (def_hashmap_size A_ Type) (def_hashmap_size B_ Type));

fun snd (x1, x2) = x2;

fun fst (x1, x2) = x1;

fun hashcode_prod A_ B_ x =
  Word32.+ (Word32.* (hashcode A_
                        (fst x), Word32.fromLargeInt (IntInf.toLarge (33 : IntInf.int))), hashcode
            B_ (snd x));

fun hashable_prod A_ B_ =
  {hashcode = hashcode_prod A_ B_,
    def_hashmap_size = def_hashmap_size_prod A_ B_}
  : ('a * 'b) hashable;

datatype 'a linorder_list = LinorderList of 'a list;

fun equal_linorder_lista (A1_, A2_) (LinorderList x) (LinorderList ya) =
  equal_lista A1_ x ya;

fun equal_linorder_list (A1_, A2_) = {equal = equal_linorder_lista (A1_, A2_)} :
  'a linorder_list equal;

fun less_eq_linorder_list_pre (A1_, A2_) (LinorderList []) (LinorderList []) =
  true
  | less_eq_linorder_list_pre (A1_, A2_) (LinorderList [])
    (LinorderList (va :: vb)) = true
  | less_eq_linorder_list_pre (A1_, A2_) (LinorderList (va :: vb))
    (LinorderList []) = false
  | less_eq_linorder_list_pre (A1_, A2_) (LinorderList (a :: asa))
    (LinorderList (b :: bs)) =
    (if eq A1_ a b
      then less_eq_linorder_list_pre (A1_, A2_) (LinorderList asa)
             (LinorderList bs)
      else less ((ord_preorder o preorder_order o order_linorder) A2_) a b);

fun less_eq_linorder_list (A1_, A2_) x y =
  less_eq_linorder_list_pre (A1_, A2_) x y;

fun less_linorder_list (A1_, A2_) x y =
  less_eq_linorder_list_pre (A1_, A2_) x y andalso
    not (less_eq_linorder_list_pre (A1_, A2_) y x);

fun ord_linorder_list (A1_, A2_) =
  {less_eq = less_eq_linorder_list (A1_, A2_),
    less = less_linorder_list (A1_, A2_)}
  : 'a linorder_list ord;

fun preorder_linorder_list (A1_, A2_) =
  {ord_preorder = ord_linorder_list (A1_, A2_)} : 'a linorder_list preorder;

fun order_linorder_list (A1_, A2_) =
  {preorder_order = preorder_linorder_list (A1_, A2_)} : 'a linorder_list order;

fun linorder_linorder_list (A1_, A2_) =
  {order_linorder = order_linorder_list (A1_, A2_)} : 'a linorder_list linorder;

datatype ('a, 'b) ifexd = TD | FD | IFD of 'a * 'b * 'b;

datatype ('a, 'b) hashtable = HashTable of (('a * 'b) list) array * nat;

datatype ('a, 'b) pointermap_impl_ext =
  Pointermap_impl_ext of ('a array * nat) * ('a, nat) hashtable * 'b;

datatype 'a bddi_ext =
  Bddi_ext of
    ((nat * (nat * nat)), unit) pointermap_impl_ext *
      ((nat * (nat * nat)), nat) hashtable * 'a;

fun id x = (fn xa => xa) x;

val one_nat : nat = Nat (1 : IntInf.int);

fun suc n = plus_nat n one_nat;

fun minus_nat m n =
  Nat (max ord_integer (0 : IntInf.int)
        (IntInf.- (integer_of_nat m, integer_of_nat n)));

fun nth (x :: xs) n =
  (if equal_nata n zero_nata then x else nth xs (minus_nat n one_nat));

fun fold f (x :: xs) s = fold f xs (f x s)
  | fold f [] s = s;

fun rev xs = fold (fn a => fn b => a :: b) xs [];

fun upt i j = (if less_nat i j then i :: upt (suc i) j else []);

fun len A_ a =
  (fn f_ => fn () => f_ (((fn () => IntInf.fromInt (Array.length a))) ()) ())
    (fn i => (fn () => (nat_of_integer i)));

fun new A_ =
  (fn a => fn b => (fn () => Array.array (IntInf.toInt a, b))) o integer_of_nat;

fun ntha A_ a n = (fn () => Array.sub (a, IntInf.toInt (integer_of_nat n)));

fun upd A_ i x a =
  (fn f_ => fn () => f_
    (((fn () => Array.update (a, IntInf.toInt (integer_of_nat i), x))) ()) ())
    (fn _ => (fn () => a));

fun const x uu = x;

fun maps f [] = []
  | maps f (x :: xs) = f x @ maps f xs;

fun map f [] = []
  | map f (x21 :: x22) = f x21 :: map f x22;

fun image f (Set xs) = Set (map f xs);

fun entriesi (Pointermap_impl_ext (entriesi, getentryi, more)) = entriesi;

fun arl_nth A_ = (fn (a, _) => ntha A_ a);

fun pm_pthi A_ m p = arl_nth A_ (entriesi m) p;

fun dpmi (Bddi_ext (dpmi, dcli, more)) = dpmi;

fun destrci n bdd =
  (if equal_nata n zero_nata then (fn () => FD)
    else (if equal_nata (minus_nat n one_nat) zero_nata then (fn () => TD)
           else (fn f_ => fn () => f_
                  ((pm_pthi (heap_prod heap_nat (heap_prod heap_nat heap_nat))
                     (dpmi bdd) (minus_nat (minus_nat n one_nat) one_nat))
                  ()) ())
                  (fn (v, (t, e)) => (fn () => (IFD (v, t, e))))));

fun remdups A_ [] = []
  | remdups A_ (x :: xs) =
    (if membera A_ xs x then remdups A_ xs else x :: remdups A_ xs);

fun serializeci p s =
  (fn f_ => fn () => f_ ((destrci p s) ()) ())
    (fn a =>
      (case a of TD => (fn () => []) | FD => (fn () => [])
        | IFD (_, t, e) =>
          (fn f_ => fn () => f_ ((serializeci t s) ()) ())
            (fn r =>
              (fn f_ => fn () => f_ ((serializeci e s) ()) ())
                (fn l =>
                  (fn () =>
                    (remdups
                      (equal_prod (equal_prod equal_nat equal_nat) equal_nat)
                      ([((p, t), one_nat), ((p, e), zero_nata)] @ r @ l)))))));

fun apsnd f (x, y) = (x, f y);

fun divmod_integer k l =
  (if ((k : IntInf.int) = (0 : IntInf.int))
    then ((0 : IntInf.int), (0 : IntInf.int))
    else (if IntInf.< ((0 : IntInf.int), l)
           then (if IntInf.< ((0 : IntInf.int), k)
                  then IntInf.divMod (IntInf.abs k, IntInf.abs l)
                  else let
                         val (r, s) =
                           IntInf.divMod (IntInf.abs k, IntInf.abs l);
                       in
                         (if ((s : IntInf.int) = (0 : IntInf.int))
                           then (IntInf.~ r, (0 : IntInf.int))
                           else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
                                  IntInf.- (l, s)))
                       end)
           else (if ((l : IntInf.int) = (0 : IntInf.int))
                  then ((0 : IntInf.int), k)
                  else apsnd IntInf.~
                         (if IntInf.< (k, (0 : IntInf.int))
                           then IntInf.divMod (IntInf.abs k, IntInf.abs l)
                           else let
                                  val (r, s) =
                                    IntInf.divMod (IntInf.abs k, IntInf.abs l);
                                in
                                  (if ((s : IntInf.int) = (0 : IntInf.int))
                                    then (IntInf.~ r, (0 : IntInf.int))
                                    else (IntInf.- (IntInf.~
              r, (1 : IntInf.int)),
   IntInf.- (IntInf.~ l, s)))
                                end))));

fun modulo_integer k l = snd (divmod_integer k l);

fun modulo_nat m n = Nat (modulo_integer (integer_of_nat m) (integer_of_nat n));

fun divide_integer k l = fst (divmod_integer k l);

fun divide_nat m n = Nat (divide_integer (integer_of_nat m) (integer_of_nat n));

fun bit_cut_integer k =
  (if ((k : IntInf.int) = (0 : IntInf.int)) then ((0 : IntInf.int), false)
    else let
           val (r, s) =
             IntInf.divMod (IntInf.abs k, IntInf.abs (2 : IntInf.int));
         in
           ((if IntInf.< ((0 : IntInf.int), k) then r
              else IntInf.- (IntInf.~ r, s)),
             ((s : IntInf.int) = (1 : IntInf.int)))
         end);

fun char_of_integer k = let
                          val (q0, b0) = bit_cut_integer k;
                          val (q1, b1) = bit_cut_integer q0;
                          val (q2, b2) = bit_cut_integer q1;
                          val (q3, b3) = bit_cut_integer q2;
                          val (q4, b4) = bit_cut_integer q3;
                          val (q5, b5) = bit_cut_integer q4;
                          val (q6, b6) = bit_cut_integer q5;
                          val a = bit_cut_integer q6;
                          val (_, aa) = a;
                        in
                          Chara (b0, b1, b2, b3, b4, b5, b6, aa)
                        end;

fun char_of_nat x = (char_of_integer o integer_of_nat) x;

fun string_of_nat n =
  (if less_nat n (nat_of_integer (10 : IntInf.int))
    then [char_of_nat (plus_nat (nat_of_integer (48 : IntInf.int)) n)]
    else string_of_nat (divide_nat n (nat_of_integer (10 : IntInf.int))) @
           [char_of_nat
              (plus_nat (nat_of_integer (48 : IntInf.int))
                (modulo_nat n (nat_of_integer (10 : IntInf.int))))]);

fun graphifyci1 bdd a =
  let
    val aa = a;
    val (ab, b) = aa;
  in
    let
      val (f, t) = ab;
    in
      (fn y =>
        let
          val c =
            string_of_nat f @
              [Chara (false, false, false, false, false, true, false, false),
                Chara (true, false, true, true, false, true, false, false),
                Chara (false, true, true, true, true, true, false, false),
                Chara (false, false, false, false, false, true, false, false)] @
                string_of_nat t;
        in
          (fn () =>
            (c @ (if equal_nata y zero_nata
                   then [Chara (false, false, false, false, false, true, false,
                                 false),
                          Chara (true, true, false, true, true, false, true,
                                  false),
                          Chara (true, true, false, false, true, true, true,
                                  false),
                          Chara (false, false, true, false, true, true, true,
                                  false),
                          Chara (true, false, false, true, true, true, true,
                                  false),
                          Chara (false, false, true, true, false, true, true,
                                  false),
                          Chara (true, false, true, false, false, true, true,
                                  false),
                          Chara (true, false, true, true, true, true, false,
                                  false),
                          Chara (false, false, true, false, false, true, true,
                                  false),
                          Chara (true, true, true, true, false, true, true,
                                  false),
                          Chara (false, false, true, false, true, true, true,
                                  false),
                          Chara (false, false, true, false, true, true, true,
                                  false),
                          Chara (true, false, true, false, false, true, true,
                                  false),
                          Chara (false, false, true, false, false, true, true,
                                  false),
                          Chara (true, false, true, true, true, false, true,
                                  false)]
                   else []) @
                   [Chara (true, true, false, true, true, true, false, false),
                     Chara (false, true, false, true, false, false, false,
                             false)]))
        end)
    end
      b
  end;

fun map_filter f [] = []
  | map_filter f (x :: xs) =
    (case f x of NONE => map_filter f xs | SOME y => y :: map_filter f xs);

fun the_thing_By A_ f l =
  let
    val a = remdups A_ (map fst l);
  in
    map (fn e =>
          (e, map_filter (fn x => (if f e (fst x) then SOME (snd x) else NONE))
                l))
      a
  end;

fun the_thing A_ = the_thing_By A_ (eq A_);

fun labelci s n =
  (fn f_ => fn () => f_ ((destrci n s) ()) ())
    (fn d =>
      let
        val son = string_of_nat n;
        val label =
          (case d
            of TD =>
              [Chara (false, false, true, false, true, false, true, false)]
            | FD =>
              [Chara (false, true, true, false, false, false, true, false)]
            | IFD (v, _, _) => string_of_nat v);
      in
        (fn () =>
          (label,
            (son, son @ [Chara (true, true, false, true, true, false, true,
                                 false),
                          Chara (false, false, true, true, false, true, true,
                                  false),
                          Chara (true, false, false, false, false, true, true,
                                  false),
                          Chara (false, true, false, false, false, true, true,
                                  false),
                          Chara (true, false, true, false, false, true, true,
                                  false),
                          Chara (false, false, true, true, false, true, true,
                                  false),
                          Chara (true, false, true, true, true, true, false,
                                  false)] @
                          label @
                            [Chara (true, false, true, true, true, false, true,
                                     false),
                              Chara (true, true, false, true, true, true, false,
                                      false),
                              Chara (false, true, false, true, false, false,
                                      false, false)])))
      end);

fun mapM f [] = (fn () => [])
  | mapM f (a :: asa) =
    (fn f_ => fn () => f_ ((f a) ()) ())
      (fn r =>
        (fn f_ => fn () => f_ ((mapM f asa) ()) ())
          (fn rs => (fn () => (r :: rs))));

fun fstp x = apsnd fst x;

fun trd x = (snd o snd) x;

fun foldr f [] = id
  | foldr f (x :: xs) = f x o foldr f xs;

fun concat xss = foldr (fn a => fn b => a @ b) xss [];

fun graphifyci name ep bdd =
  (fn f_ => fn () => f_ ((serializeci ep bdd) ()) ())
    (fn s =>
      let
        val e = map fst s;
      in
        (fn f_ => fn () => f_
          ((mapM (labelci bdd)
             (rev (remdups equal_nat (map fst e @ map snd e))))
          ()) ())
          (fn l =>
            let
              val grp =
                map (fn la =>
                      foldr (fn a => fn t =>
                              t @ a @ [Chara
 (true, true, false, true, true, true, false, false)])
                        (snd la)
                        [Chara (true, true, false, true, true, true, true,
                                 false),
                          Chara (false, true, false, false, true, true, true,
                                  false),
                          Chara (true, false, false, false, false, true, true,
                                  false),
                          Chara (false, true, true, true, false, true, true,
                                  false),
                          Chara (true, true, false, true, false, true, true,
                                  false),
                          Chara (true, false, true, true, true, true, false,
                                  false),
                          Chara (true, true, false, false, true, true, true,
                                  false),
                          Chara (true, false, false, false, false, true, true,
                                  false),
                          Chara (true, false, true, true, false, true, true,
                                  false),
                          Chara (true, false, true, false, false, true, true,
                                  false),
                          Chara (true, true, false, true, true, true, false,
                                  false)] @
                        [Chara (true, false, true, true, true, true, true,
                                 false),
                          Chara (false, true, false, true, false, false, false,
                                  false)])
                  (the_thing (equal_list equal_char) (map fstp l));
            in
              (fn f_ => fn () => f_ ((mapM (graphifyci1 bdd) s) ()) ())
                (fn ea =>
                  let
                    val emptyhlp =
                      (if equal_nata ep zero_nata
                        then [Chara (false, true, true, false, false, false,
                                      true, false),
                               Chara (true, true, false, true, true, true,
                                       false, false),
                               Chara (false, true, false, true, false, false,
                                       false, false)]
                        else (if equal_nata (minus_nat ep one_nat) zero_nata
                               then [Chara (false, false, true, false, true,
     false, true, false),
                                      Chara
(true, true, false, true, true, true, false, false),
                                      Chara
(false, true, false, true, false, false, false, false)]
                               else []));
                  in
                    (fn () =>
                      ([Chara (false, false, true, false, false, true, true,
                                false),
                         Chara (true, false, false, true, false, true, true,
                                 false),
                         Chara (true, true, true, false, false, true, true,
                                 false),
                         Chara (false, true, false, false, true, true, true,
                                 false),
                         Chara (true, false, false, false, false, true, true,
                                 false),
                         Chara (false, false, false, false, true, true, true,
                                 false),
                         Chara (false, false, false, true, false, true, true,
                                 false),
                         Chara (false, false, false, false, false, true, false,
                                 false)] @
                        name @
                          [Chara (false, false, false, false, false, true,
                                   false, false),
                            Chara (true, true, false, true, true, true, true,
                                    false),
                            Chara (false, true, false, true, false, false,
                                    false, false)] @
                            maps trd l @
                              concat grp @
                                concat ea @
                                  emptyhlp @
                                    [Chara (true, false, true, true, true, true,
     true, false)]))
                  end)
            end)
      end);

val bot_set : 'a set = Set [];

fun removeAll A_ x [] = []
  | removeAll A_ x (y :: xs) =
    (if eq A_ x y then removeAll A_ x xs else y :: removeAll A_ x xs);

fun inserta A_ x xs = (if membera A_ xs x then xs else x :: xs);

fun insert A_ x (Coset xs) = Coset (removeAll A_ x xs)
  | insert A_ x (Set xs) = Set (inserta A_ x xs);

val sc_threshold_2_3 : nat set set =
  insert (equal_set equal_nat) bot_set
    (insert (equal_set equal_nat) (insert equal_nat zero_nata bot_set)
      (insert (equal_set equal_nat) (insert equal_nat one_nat bot_set)
        (insert (equal_set equal_nat)
          (insert equal_nat (nat_of_integer (2 : IntInf.int)) bot_set)
          (insert (equal_set equal_nat)
            (insert equal_nat (nat_of_integer (3 : IntInf.int)) bot_set)
            (insert (equal_set equal_nat)
              (insert equal_nat zero_nata (insert equal_nat one_nat bot_set))
              (insert (equal_set equal_nat)
                (insert equal_nat zero_nata
                  (insert equal_nat (nat_of_integer (2 : IntInf.int)) bot_set))
                (insert (equal_set equal_nat)
                  (insert equal_nat zero_nata
                    (insert equal_nat (nat_of_integer (3 : IntInf.int))
                      bot_set))
                  (insert (equal_set equal_nat)
                    (insert equal_nat one_nat
                      (insert equal_nat (nat_of_integer (2 : IntInf.int))
                        bot_set))
                    (insert (equal_set equal_nat)
                      (insert equal_nat one_nat
                        (insert equal_nat (nat_of_integer (3 : IntInf.int))
                          bot_set))
                      (insert (equal_set equal_nat)
                        (insert equal_nat (nat_of_integer (2 : IntInf.int))
                          (insert equal_nat (nat_of_integer (3 : IntInf.int))
                            bot_set))
                        bot_set))))))))));

fun gen_length n (x :: xs) = gen_length (suc n) xs
  | gen_length n [] = n;

fun size_list x = gen_length zero_nata x;

fun part B_ f pivot (x :: xs) =
  let
    val (lts, (eqs, gts)) = part B_ f pivot xs;
    val xa = f x;
  in
    (if less ((ord_preorder o preorder_order o order_linorder) B_) xa pivot
      then (x :: lts, (eqs, gts))
      else (if less ((ord_preorder o preorder_order o order_linorder) B_) pivot
                 xa
             then (lts, (eqs, x :: gts)) else (lts, (x :: eqs, gts))))
  end
  | part B_ f pivot [] = ([], ([], []));

fun sort_key B_ f xs =
  (case xs of [] => [] | [_] => xs
    | [x, y] =>
      (if less_eq ((ord_preorder o preorder_order o order_linorder) B_) (f x)
            (f y)
        then xs else [y, x])
    | _ :: _ :: _ :: _ =>
      let
        val (lts, (eqs, gts)) =
          part B_ f
            (f (nth xs
                 (divide_nat (size_list xs) (nat_of_integer (2 : IntInf.int)))))
            xs;
      in
        sort_key B_ f lts @ eqs @ sort_key B_ f gts
      end);

fun sorted_list_of_set (A1_, A2_) (Set xs) =
  sort_key A2_ (fn x => x) (remdups A1_ xs);

fun linorder_list_unwrap A_ l = let
                                  val LinorderList la = l;
                                in
                                  la
                                end;

fun sorted_list_of_list_set (A1_, A2_) l =
  map (linorder_list_unwrap A2_)
    (sorted_list_of_set
      (equal_linorder_list (A1_, A2_), linorder_linorder_list (A1_, A2_))
      (image LinorderList l));

fun nat_list_from_vertex (A1_, A2_) v = sorted_list_of_set (A1_, A2_) v;

fun nat_list_from_sc (A1_, A2_) k =
  sorted_list_of_list_set (A1_, A2_)
    (image (nat_list_from_vertex (A1_, A2_)) k);

fun getentryi (Pointermap_impl_ext (entriesi, getentryi, more)) = getentryi;

fun times_nat m n = Nat (IntInf.* (integer_of_nat m, integer_of_nat n));

fun blit A_ src si dst di len =
  (fn () => 
    array_blit src (integer_of_nat
                     si) dst (integer_of_nat di) (integer_of_nat len));

fun array_grow A_ a s x =
  (fn f_ => fn () => f_ ((len A_ a) ()) ())
    (fn l =>
      (if equal_nata l s then (fn () => a)
        else (fn f_ => fn () => f_ ((new A_ s x) ()) ())
               (fn aa =>
                 (fn f_ => fn () => f_ ((blit A_ a zero_nata aa zero_nata l) ())
                   ())
                   (fn _ => (fn () => aa)))));

fun arl_append (A1_, A2_) =
  (fn (a, n) => fn x =>
    (fn f_ => fn () => f_ ((len A2_ a) ()) ())
      (fn lena =>
        (if less_nat n lena
          then (fn f_ => fn () => f_ ((upd A2_ n x a) ()) ())
                 (fn aa => (fn () => (aa, plus_nat n one_nat)))
          else let
                 val newcap = times_nat (nat_of_integer (2 : IntInf.int)) lena;
               in
                 (fn f_ => fn () => f_ ((array_grow A2_ a newcap (default A1_))
                   ()) ())
                   (fn aa =>
                     (fn f_ => fn () => f_ ((upd A2_ n x aa) ()) ())
                       (fn ab => (fn () => (ab, plus_nat n one_nat))))
               end)));

val load_factor : nat = nat_of_integer (75 : IntInf.int);

fun the_array (HashTable (a, uu)) = a;

fun replicate n x =
  (if equal_nata n zero_nata then []
    else x :: replicate (minus_nat n one_nat) x);

fun ht_new_sz (A1_, A2_) B_ n =
  let
    val l = replicate n [];
  in
    (fn f_ => fn () => f_ (((fn () => Array.fromList l)) ()) ())
      (fn a => (fn () => (HashTable (a, zero_nata))))
  end;

fun nat_of_uint32 x =
  nat_of_integer (IntInf.fromLarge (Word32.toLargeInt x) : IntInf.int);

fun nat_of_hashcode x = nat_of_uint32 x;

fun bounded_hashcode_nat A_ n x =
  modulo_nat (nat_of_hashcode (hashcode A_ x)) n;

fun ls_update A_ k v [] = ([(k, v)], false)
  | ls_update A_ k v ((l, w) :: ls) =
    (if eq A_ k l then ((k, v) :: ls, true)
      else let
             val r = ls_update A_ k v ls;
           in
             ((l, w) :: fst r, snd r)
           end);

fun the_size (HashTable (uu, n)) = n;

fun ht_upd (A1_, A2_, A3_) B_ k v ht =
  (fn f_ => fn () => f_ ((len (heap_list (heap_prod A3_ B_)) (the_array ht)) ())
    ())
    (fn m =>
      let
        val i = bounded_hashcode_nat A2_ m k;
      in
        (fn f_ => fn () => f_
          ((ntha (heap_list (heap_prod A3_ B_)) (the_array ht) i) ()) ())
          (fn l =>
            let
              val la = ls_update A1_ k v l;
            in
              (fn f_ => fn () => f_
                ((upd (heap_list (heap_prod A3_ B_)) i (fst la) (the_array ht))
                ()) ())
                (fn _ =>
                  let
                    val n = (if snd la then the_size ht else suc (the_size ht));
                  in
                    (fn () => (HashTable (the_array ht, n)))
                  end)
            end)
      end);

fun ht_insls (A1_, A2_, A3_) B_ [] ht = (fn () => ht)
  | ht_insls (A1_, A2_, A3_) B_ ((k, v) :: l) ht =
    (fn f_ => fn () => f_ ((ht_upd (A1_, A2_, A3_) B_ k v ht) ()) ())
      (ht_insls (A1_, A2_, A3_) B_ l);

fun ht_copy (A1_, A2_, A3_) B_ n src dst =
  (if equal_nata n zero_nata then (fn () => dst)
    else (fn f_ => fn () => f_
           ((ntha (heap_list (heap_prod A3_ B_)) (the_array src)
              (minus_nat n one_nat))
           ()) ())
           (fn l =>
             (fn f_ => fn () => f_ ((ht_insls (A1_, A2_, A3_) B_ l dst) ()) ())
               (ht_copy (A1_, A2_, A3_) B_ (minus_nat n one_nat) src)));

fun ht_rehash (A1_, A2_, A3_) B_ ht =
  (fn f_ => fn () => f_ ((len (heap_list (heap_prod A3_ B_)) (the_array ht)) ())
    ())
    (fn n =>
      (fn f_ => fn () => f_
        ((ht_new_sz (A2_, A3_) B_
           (times_nat (nat_of_integer (2 : IntInf.int)) n))
        ()) ())
        (ht_copy (A1_, A2_, A3_) B_ n ht));

fun ht_update (A1_, A2_, A3_) B_ k v ht =
  (fn f_ => fn () => f_ ((len (heap_list (heap_prod A3_ B_)) (the_array ht)) ())
    ())
    (fn m =>
      (fn f_ => fn () => f_
        ((if less_eq_nat (times_nat m load_factor)
               (times_nat (the_size ht) (nat_of_integer (100 : IntInf.int)))
           then ht_rehash (A1_, A2_, A3_) B_ ht else (fn () => ht))
        ()) ())
        (ht_upd (A1_, A2_, A3_) B_ k v));

fun ls_lookup A_ x [] = NONE
  | ls_lookup A_ x ((k, v) :: l) =
    (if eq A_ x k then SOME v else ls_lookup A_ x l);

fun ht_lookup (A1_, A2_, A3_) B_ x ht =
  (fn f_ => fn () => f_ ((len (heap_list (heap_prod A3_ B_)) (the_array ht)) ())
    ())
    (fn m =>
      let
        val i = bounded_hashcode_nat A2_ m x;
      in
        (fn f_ => fn () => f_
          ((ntha (heap_list (heap_prod A3_ B_)) (the_array ht) i) ()) ())
          (fn l => (fn () => (ls_lookup A1_ x l)))
      end);

fun pointermap_getmki (A1_, A2_, A3_, A4_) a m =
  (fn f_ => fn () => f_ ((ht_lookup (A2_, A3_, A4_) heap_nat a (getentryi m))
    ()) ())
    (fn b =>
      (case b
        of NONE =>
          (fn f_ => fn () => f_ ((fn () => (snd (entriesi m))) ()) ())
            (fn p =>
              (fn f_ => fn () => f_ ((arl_append (A1_, A4_) (entriesi m) a) ())
                ())
                (fn ent =>
                  (fn f_ => fn () => f_
                    ((ht_update (A2_, A3_, A4_) heap_nat a p (getentryi m)) ())
                    ())
                    (fn lut =>
                      (fn f_ => fn () => f_
                        ((fn () => (Pointermap_impl_ext (ent, lut, ()))) ()) ())
                        (fn u => (fn () => (p, u))))))
        | SOME l => (fn () => (l, m))));

fun dpmi_update dpmia (Bddi_ext (dpmi, dcli, more)) =
  Bddi_ext (dpmia dpmi, dcli, more);

fun ifci v t e bdd =
  (if equal_nata t e then (fn () => (t, bdd))
    else (fn f_ => fn () => f_
           ((pointermap_getmki
              (default_prod default_nat (default_prod default_nat default_nat),
                equal_prod equal_nat (equal_prod equal_nat equal_nat),
                hashable_prod hashable_nat
                  (hashable_prod hashable_nat hashable_nat),
                heap_prod heap_nat (heap_prod heap_nat heap_nat))
              (v, (t, e)) (dpmi bdd))
           ()) ())
           (fn (p, u) => (fn () => (suc (suc p), dpmi_update (const u) bdd))));

fun tci bdd = (fn () => (one_nat, bdd));

fun fci bdd = (fn () => (zero_nata, bdd));

fun litci v bdd =
  (fn f_ => fn () => f_ ((tci bdd) ()) ())
    (fn (t, bdda) =>
      (fn f_ => fn () => f_ ((fci bdda) ()) ()) (fn (a, b) => ifci v t a b));

fun dcli_update dclia (Bddi_ext (dpmi, dcli, more)) =
  Bddi_ext (dpmi, dclia dcli, more);

fun case_ifexici fti ffi fii ni bddi =
  (fn f_ => fn () => f_ ((destrci ni bddi) ()) ())
    (fn a => (case a of TD => fti | FD => ffi | IFD (aa, b, c) => fii aa b c));

fun restrict_topci p vr vl bdd =
  case_ifexici (fn () => p) (fn () => p)
    (fn v => fn te => fn ee =>
      (fn () => (if equal_nata v vr then (if vl then te else ee) else p)))
    p bdd;

fun min A_ a b = (if less_eq A_ a b then a else b);

fun lowest_topsci [] s = (fn () => NONE)
  | lowest_topsci (e :: es) s =
    case_ifexici (lowest_topsci es s) (lowest_topsci es s)
      (fn v => fn _ => fn _ =>
        (fn f_ => fn () => f_ ((lowest_topsci es s) ()) ())
          (fn a =>
            (case a of NONE => (fn () => (SOME v))
              | SOME u => (fn () => (SOME (min ord_nat u v))))))
      e s;

fun equal_IFEXD A_ B_ FD (IFD (x31, x32, x33)) = false
  | equal_IFEXD A_ B_ (IFD (x31, x32, x33)) FD = false
  | equal_IFEXD A_ B_ TD (IFD (x31, x32, x33)) = false
  | equal_IFEXD A_ B_ (IFD (x31, x32, x33)) TD = false
  | equal_IFEXD A_ B_ TD FD = false
  | equal_IFEXD A_ B_ FD TD = false
  | equal_IFEXD A_ B_ (IFD (x31, x32, x33)) (IFD (y31, y32, y33)) =
    eq A_ x31 y31 andalso (eq B_ x32 y32 andalso eq B_ x33 y33)
  | equal_IFEXD A_ B_ FD FD = true
  | equal_IFEXD A_ B_ TD TD = true;

fun param_optci i t e bdd =
  (fn f_ => fn () => f_ ((tci bdd) ()) ())
    (fn (tr, bdda) =>
      (fn f_ => fn () => f_ ((fci bdda) ()) ())
        (fn (fl, bddb) =>
          (fn f_ => fn () => f_ ((destrci i bddb) ()) ())
            (fn id =>
              (fn f_ => fn () => f_ ((destrci t bddb) ()) ())
                (fn td =>
                  (fn f_ => fn () => f_ ((destrci e bddb) ()) ())
                    (fn ed =>
                      (fn () =>
                        ((if equal_IFEXD equal_nat equal_nat id TD then SOME t
                           else (if equal_IFEXD equal_nat equal_nat id FD
                                  then SOME e
                                  else (if equal_IFEXD equal_nat equal_nat td
     TD andalso
     equal_IFEXD equal_nat equal_nat ed FD
 then SOME i
 else (if equal_nata t e then SOME t
        else (if equal_IFEXD equal_nat equal_nat ed TD andalso equal_nata i t
               then SOME tr
               else (if equal_IFEXD equal_nat equal_nat td FD andalso
                          equal_nata i e
                      then SOME fl else NONE)))))),
                          bddb)))))));

fun dcli (Bddi_ext (dpmi, dcli, more)) = dcli;

fun iteci_lu i t e s =
  (fn f_ => fn () => f_
    ((ht_lookup
       (equal_prod equal_nat (equal_prod equal_nat equal_nat),
         hashable_prod hashable_nat (hashable_prod hashable_nat hashable_nat),
         heap_prod heap_nat (heap_prod heap_nat heap_nat))
       heap_nat (i, (t, e)) (dcli s))
    ()) ())
    (fn a =>
      (case a
        of NONE =>
          (fn f_ => fn () => f_ ((param_optci i t e s) ()) ())
            (fn aa =>
              (case aa
                of (NONE, sa) =>
                  (fn f_ => fn () => f_ ((lowest_topsci [i, t, e] sa) ()) ())
                    (fn ab =>
                      (case ab of NONE => (raise Fail "Cannot happen")
                        | SOME ac =>
                          (fn f_ => fn () => f_ ((restrict_topci i ac true sa)
                            ()) ())
                            (fn ti =>
                              (fn f_ => fn () => f_
                                ((restrict_topci t ac true sa) ()) ())
                                (fn tt =>
                                  (fn f_ => fn () => f_
                                    ((restrict_topci e ac true sa) ()) ())
                                    (fn te =>
                                      (fn f_ => fn () => f_
((restrict_topci i ac false sa) ()) ())
(fn fi =>
  (fn f_ => fn () => f_ ((restrict_topci t ac false sa) ()) ())
    (fn ft =>
      (fn f_ => fn () => f_ ((restrict_topci e ac false sa) ()) ())
        (fn fe =>
          (fn f_ => fn () => f_ ((iteci_lu ti tt te sa) ()) ())
            (fn (tb, sb) =>
              (fn f_ => fn () => f_ ((iteci_lu fi ft fe sb) ()) ())
                (fn (fb, sc) =>
                  (fn f_ => fn () => f_ ((ifci ac tb fb sc) ()) ())
                    (fn (r, sd) =>
                      (fn f_ => fn () => f_
                        ((ht_update
                           (equal_prod equal_nat
                              (equal_prod equal_nat equal_nat),
                             hashable_prod hashable_nat
                               (hashable_prod hashable_nat hashable_nat),
                             heap_prod heap_nat (heap_prod heap_nat heap_nat))
                           heap_nat (i, (t, e)) r (dcli sd))
                        ()) ())
                        (fn cl =>
                          (fn () => (r, dcli_update (const cl) sd))))))))))))))
                | (SOME b, sa) => (fn () => (b, sa))))
        | SOME b => (fn () => (b, s))));

fun andci e1 e2 s =
  (fn f_ => fn () => f_ ((fci s) ()) ()) (fn (a, b) => iteci_lu e1 e2 a b);

fun bdd_from_vertex_list n [] s = tci s
  | bdd_from_vertex_list n (f :: fs) s =
    (fn f_ => fn () => f_ ((if membera equal_nat n f then tci s else litci f s)
      ()) ())
      (fn (fa, sa) =>
        (fn f_ => fn () => f_ ((bdd_from_vertex_list n fs sa) ()) ())
          (fn (fsa, a) => andci fsa fa a));

fun orci e1 e2 s =
  (fn f_ => fn () => f_ ((tci s) ()) ()) (fn (t, a) => iteci_lu e1 t e2 a);

fun bdd_from_sc_list lUNIV [] s = fci s
  | bdd_from_sc_list lUNIV (la :: l) s =
    (fn f_ => fn () => f_ ((bdd_from_vertex_list la lUNIV s) ()) ())
      (fn (laa, sa) =>
        (fn f_ => fn () => f_ ((bdd_from_sc_list lUNIV l sa) ()) ())
          (fn (lb, a) => orci lb laa a));

val initial_capacity : nat = nat_of_integer (16 : IntInf.int);

fun arl_empty (A1_, A2_) B_ =
  (fn f_ => fn () => f_ ((new A2_ initial_capacity (default A1_)) ()) ())
    (fn a => (fn () => (a, zero B_)));

fun ht_new (A1_, A2_) B_ = ht_new_sz (A1_, A2_) B_ (def_hashmap_size A1_ Type);

fun pointermap_empty (A1_, A2_, A3_) =
  (fn f_ => fn () => f_ ((ht_new (A2_, A3_) heap_nat) ()) ())
    (fn hm =>
      (fn f_ => fn () => f_ ((arl_empty (A1_, A3_) zero_nat) ()) ())
        (fn arl => (fn () => (Pointermap_impl_ext (arl, hm, ())))));

val emptyci : (unit -> unit bddi_ext) =
  (fn f_ => fn () => f_
    ((pointermap_empty
       (default_prod default_nat (default_prod default_nat default_nat),
         hashable_prod hashable_nat (hashable_prod hashable_nat hashable_nat),
         heap_prod heap_nat (heap_prod heap_nat heap_nat)))
    ()) ())
    (fn ep =>
      (fn f_ => fn () => f_
        ((ht_new
           (hashable_prod hashable_nat
              (hashable_prod hashable_nat hashable_nat),
             heap_prod heap_nat (heap_prod heap_nat heap_nat))
           heap_nat)
        ()) ())
        (fn ehm => (fn () => (Bddi_ext (ep, ehm, ())))));

val ex_2_3 : (unit -> (char list)) =
  (fn f_ => fn () => f_ (emptyci ()) ())
    (fn s =>
      (fn f_ => fn () => f_
        ((bdd_from_sc_list
           [zero_nata, one_nat, nat_of_integer (2 : IntInf.int),
             nat_of_integer (3 : IntInf.int)]
           (nat_list_from_sc (equal_nat, linorder_nat) sc_threshold_2_3) s)
        ()) ())
        (fn (a, b) =>
          graphifyci
            [Chara (false, false, true, false, true, true, true, false),
              Chara (false, false, false, true, false, true, true, false),
              Chara (false, true, false, false, true, true, true, false),
              Chara (true, false, true, false, false, true, true, false),
              Chara (true, true, false, false, true, true, true, false),
              Chara (false, false, false, true, false, true, true, false),
              Chara (true, true, true, true, false, true, true, false),
              Chara (false, false, true, true, false, true, true, false),
              Chara (false, false, true, false, false, true, true, false),
              Chara (true, true, true, true, true, false, true, false),
              Chara (false, false, true, false, true, true, true, false),
              Chara (true, true, true, false, true, true, true, false),
              Chara (true, true, true, true, false, true, true, false),
              Chara (true, true, true, true, true, false, true, false),
              Chara (false, false, true, false, true, true, true, false),
              Chara (false, false, false, true, false, true, true, false),
              Chara (false, true, false, false, true, true, true, false),
              Chara (true, false, true, false, false, true, true, false),
              Chara (true, false, true, false, false, true, true, false)]
            a b));

fun bdd_from_sc k n =
  bdd_from_sc_list
    (nat_list_from_vertex (equal_nat, linorder_nat) (Set (upt zero_nata n)))
    (nat_list_from_sc (equal_nat, linorder_nat) k);

end; (*struct IBDD*)