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

import Ersatz
import Prelude hiding (and, or, not, (&&), (||), any, all)
import Control.Monad (replicateM)
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,0,1],[0,0,1,0])]

main =
  main_for g03 16 12
  -- main_for g10 _ _

step srs (u,v) = any (\ rule -> here rule (u,v)) srs
  || case (u,v) of
      ( [], [] )   -> false
      (x:u', y:v') -> x === y && step srs (u',v')

here (lhs,rhs) (u,v) =
  let (upre, usuf) = splitAt (length lhs) u
      (vpre, vsuf) = splitAt (length rhs) v
  in  (lhs === upre) && (rhs === vpre) && (usuf === vsuf)

instance Num Bit where
  fromInteger 0 = false ; fromInteger 1 = true

main_for srs steps width = do
  result <- solveWith minisat $ do
    ws <- replicateM steps $ replicateM width $ exists @Bit
    assert $ all (step srs) $ zip ws $ tail ws
    assert $ head ws === last ws
    return ws
  case result of
    (Satisfied, Just ws) -> mapM_ (print . map fromEnum) ws