(* val zero : sym *)

val zero = Sym.fromString "0";

(* val one : sym *)

val one = Sym.fromString "1";

(* val minAndRen : dfa -> dfa *)

val minAndRen =
      DFA.renameStatesCanonically o DFA.minimize o DFA.renameStatesCanonically;

(* val efaToDFA : efa -> dfa *)

val efaToDFA = nfaToDFA o efaToNFA;

(* val allStrDFA : dfa

   allStrDFA accepts {0, 1}* *)

val allStrDFA =
      minAndRen(efaToDFA(EFA.closure(EFA.union(EFA.fromSym zero,
                                               EFA.fromSym one))));

(* val swapRel : sym_rel *)

val swapRel = SymRel.fromString "(0, 1), (1, 0)";

(* val zeroAllPrefPosEFA : int -> efa

   if n >= 0, then zeroAllPrefPosEFA n returns an efa that accepts all
   w in {0, 1}* such that diff w = 0 and all prefixes of w have diff's
   between 0 and n *)

fun zeroAllPrefPosEFA 0 = EFA.emptyStr
  | zeroAllPrefPosEFA n =
      EFA.closure(EFA.concat(EFA.fromSym one,
                             EFA.concat(zeroAllPrefPosEFA(n - 1),
                                        EFA.fromSym zero)));

(* val zeroAllPrefPosDFA : int -> dfa

   if n >= 0, then zeroAllPrefPosDFA n returns a dfa that accepts
   all w in {0, 1}* such that diff w = 0 and all prefixes of w
   have diff's between 0 and n *)

fun zeroAllPrefPosDFA n = minAndRen(efaToDFA(zeroAllPrefPosEFA n));

(* val justBadPosEFA : int -> efa

   if n >= 0, then justBadPosEFA n returns an efa that accepts all w
   in {0, 1}* such that diff w = n + 1 and all proper prefixes of w
   have diff's between 0 and n *)

fun justBadPosEFA 0 = EFA.fromSym one
  | justBadPosEFA n =
      EFA.concat(injDFAToEFA(zeroAllPrefPosDFA n),
                 EFA.concat(EFA.fromSym one, justBadPosEFA(n - 1)));

(* val justBadPosDFA : int -> dfa

   if n >= 0, then justBadPosDFA n returns a dfa that accepts all w in
   {0, 1}* such that diff w = n + 1 and all proper prefixes of w have
   diff's between 0 and n *)

fun justBadPosDFA n = minAndRen(efaToDFA(justBadPosEFA n));

(* val justBadNegDFA : int -> dfa

   if n >= 0, then justBadNegDFA n returns a dfa that accepts all w in
   {0, 1}* such that diff w = ~(n + 1) and all proper prefixes of w
   have diff's between 0 and ~n *)

fun justBadNegDFA n = DFA.renameAlphabet(justBadPosDFA n, swapRel);

(* val justBadPosOrNegDFA : int -> dfa

   if n >= 0, then justBadPosOrNegDFA n returns a dfa accepting all w
   in {0, 1}* such that either:

     diff w = n + 1 and all proper prefixes of w have diff's between 0
     and n; or

     diff w = ~(n + 1) and all proper prefixes of w have diff's
     between 0 and ~n *)

fun justBadPosOrNegDFA n =
      minAndRen(efaToDFA(EFA.union(injDFAToEFA(justBadPosDFA n),
                                   injDFAToEFA(justBadNegDFA n))));

(* val someSubBadEFA : int -> efa

   if n >= 0, then someSubBadEFA n returns an efa that accepts all w in
   {0, 1}* such that some substring of w has a diff that is < ~n or > n *)

fun someSubBadEFA n =
      EFA.concat(injDFAToEFA allStrDFA,
                 EFA.concat(injDFAToEFA(justBadPosOrNegDFA n),
                            injDFAToEFA allStrDFA));

(* val someSubBadDFA : int -> dfa

   if n >= 0, then someSubBadDFA n returns a dfa that accepts all w in
   {0, 1}* such that some substring of w has a diff that is < ~n or > n *)

fun someSubBadDFA n = minAndRen(efaToDFA(someSubBadEFA n));

(* val allSubGoodDFA : int -> dfa

   if n >= 0, then allSubGoodDFA n returns a minimized dfa that
   accepts all w in {0, 1}* such that all substrings of w have diff's
   between ~n and n *)

fun allSubGoodDFA n = minAndRen(DFA.minus(allStrDFA, someSubBadDFA n));