-- DON'T USE THIS. g03 is much nicer.

{-# OPTIONS_GHC -fdefer-typed-holes #-}

import Ersatz
import Prelude hiding (and, or, not, (&&), (||), any, all)
import Ersatz.Relation
import Ersatz.Solver
import Ersatz.Solver.Minisat

g03 = [([0,0,0,0],[0,0,1,1]),([1,0,0,1],[0,0,1,0])]
g10 = [([0,0,0,0],[0,1,1,1]),([1,0,1,1],[0,0,1,0])]

main = main_for g03 20 12

main_for srs steps width = do
  result <- solveWith minisat $ do
    r <- relation ((1,1),(steps,width))
    let get s = map (\ j -> r ! (s,j)) [ 1 .. width ]
    assert $ flip all [1 .. _] $ \ s ->
      -- each step s is correct
      flip any [1 .. _] $ \ p ->
        -- the redex is at position p
        let split3 p w =
              let (w1,w23) = splitAt (p-1) w ; (w2,w3) = splitAt 4 w23
              in  (w1,w2,w3)
            enc :: [Int] -> [Bit]
            enc w = encode $ map toEnum w  
            (u1,u2,u3) = split3 p $ get s
            (v1,v2,v3) = split3 p $ get (s+1)
        in    u1 === _
           && ( flip any srs $ \ (l,r) -> _ )
           && _
    assert $ flip any [_ .. steps] $ \ s ->
      -- there is a cycle
      get 1 === get s
    return r
  case result of
    (Satisfied, Just r) -> do
      putStrLn $ table r

{- NOTE 

flip all xs p = (flip all) xs p = all p xs

-}