-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Strings.RegexCrossword
-- Copyright : (c) Joel Burget
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- This example solves regex crosswords from <http://regexcrossword.com>
-----------------------------------------------------------------------------

{-# LANGUAGE OverloadedStrings #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Strings.RegexCrossword where

import Data.List (genericLength, transpose)

import Data.SBV
import Data.SBV.Control

import Prelude hiding ((!!))
import Data.SBV.String ((!!))

import qualified Data.SBV.String as S
import qualified Data.SBV.RegExp as R

-- | Solve a given crossword, returning the corresponding rows
solveCrossword :: [R.RegExp] -> [R.RegExp] -> IO [String]
solveCrossword :: [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rowRegExps [RegExp]
colRegExps = Symbolic [String] -> IO [String]
forall a. Symbolic a -> IO a
runSMT (Symbolic [String] -> IO [String])
-> Symbolic [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ do
        let numRows :: Integer
numRows = [RegExp] -> Integer
forall i a. Num i => [a] -> i
genericLength [RegExp]
rowRegExps
            numCols :: Integer
numCols = [RegExp] -> Integer
forall i a. Num i => [a] -> i
genericLength [RegExp]
colRegExps

        -- constrain rows
        let mkRow :: RegExp -> SymbolicT IO (SBV String)
mkRow RegExp
rowRegExp = do row <- SymbolicT IO (SBV String)
forall a. SymVal a => Symbolic (SBV a)
free_
                                 constrain $ row `R.match` rowRegExp
                                 constrain $ S.length row .== literal numCols
                                 return row

        rows <- (RegExp -> SymbolicT IO (SBV String))
-> [RegExp] -> SymbolicT IO [SBV String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM RegExp -> SymbolicT IO (SBV String)
mkRow [RegExp]
rowRegExps

        -- constrain columns
        let mkCol RegExp
colRegExp = do col <- SymbolicT IO (SBV String)
forall a. SymVal a => Symbolic (SBV a)
free_
                                 constrain $ col `R.match` colRegExp
                                 constrain $ S.length col .== literal numRows
                                 return col

        cols <- mapM mkCol colRegExps

        -- constrain each "cell" as they rows/columns intersect:
        let rowss =           [[SBV String
r SBV String -> SInteger -> SChar
!! Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [Integer
0..Integer
numColsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]] | SBV String
r <- [SBV String]
rows]
        let colss = [[SChar]] -> [[SChar]]
forall a. [[a]] -> [[a]]
transpose [[SBV String
c SBV String -> SInteger -> SChar
!! Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i | Integer
i <- [Integer
0..Integer
numRowsInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]] | SBV String
c <- [SBV String]
cols]

        constrain $ sAnd $ zipWith (.==) (concat rowss) (concat colss)

        -- Now query to extract the solution
        query $ do cs <- checkSat
                   case cs of
                     CheckSatResult
Unk    -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"Solver returned unknown!"
                     DSat{} -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"Solver returned delta-sat!"
                     CheckSatResult
Unsat  -> String -> Query [String]
forall a. HasCallStack => String -> a
error String
"There are no solutions to this puzzle!"
                     CheckSatResult
Sat    -> (SBV String -> QueryT IO String) -> [SBV String] -> Query [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SBV String -> QueryT IO String
forall a. SymVal a => SBV a -> Query a
getValue [SBV String]
rows

-- | Solve <http://regexcrossword.com/challenges/intermediate/puzzles/1>
--
-- >>> puzzle1
-- ["ATO","WEL"]
puzzle1 :: IO [String]
puzzle1 :: IO [String]
puzzle1 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
  where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"NOTAD")  -- [NOTAD]*
             , RegExp
"WEL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"BAL" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"EAR"      -- WEL|BAL|EAR
             ]

        cs :: [RegExp]
cs = [ RegExp
"UB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"IE" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AW"         -- UB|IE|AW
             , RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"TUBE")   -- [TUBE]*
             , String -> RegExp
R.oneOf String
"BORF" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
R.All     -- [BORF].
             ]

-- | Solve <http://regexcrossword.com/challenges/intermediate/puzzles/2>
--
-- >>> puzzle2
-- ["WA","LK","ER"]
puzzle2 :: IO [String]
puzzle2 :: IO [String]
puzzle2 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
  where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf String
"AWE")       -- [AWE]+
             , RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf String
"ALP") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"K" -- [ALP]+K
             , RegExp
"PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"ER" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"EP"            -- (PR|ER|EP)
             ]

        cs :: [RegExp]
cs = [ String -> RegExp
R.oneOf String
"BQW" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* (RegExp
"PR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"LE") -- [BQW](PR|LE)
             , RegExp -> RegExp
R.KPlus (String -> RegExp
R.oneOf String
"RANK")      -- [RANK]+
             ]

-- | Solve <http://regexcrossword.com/challenges/palindromeda/puzzles/3>
--
-- >>> puzzle3
-- ["RATS","ABUT","TUBA","STAR"]
puzzle3 :: IO [String]
puzzle3 :: IO [String]
puzzle3 = [RegExp] -> [RegExp] -> IO [String]
solveCrossword [RegExp]
rs [RegExp]
cs
 where rs :: [RegExp]
rs = [ RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"TRASH")                -- [TRASH]*
            , (RegExp
"FA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AB") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar (String -> RegExp
R.oneOf String
"TUP")  -- (FA|AB)[TUP]*
            , RegExp -> RegExp
R.KStar (RegExp
"BA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"TH" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"TU")             -- (BA|TH|TU)*
            , RegExp -> RegExp
R.KStar RegExp
R.All RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All      -- .*A.*
            ]

       cs :: [RegExp]
cs = [ RegExp -> RegExp
R.KStar (RegExp
"TS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"RA" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"QA")                     -- (TS|RA|QA)*
            , RegExp -> RegExp
R.KStar (RegExp
"AB" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"UT" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"AR")                     -- (AB|UT|AR)*
            , (RegExp
"K" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"T") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
"U" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
R.KStar RegExp
R.All RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* (RegExp
"A" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"R")  -- (K|T)U.*(A|R)
            , RegExp -> RegExp
R.KPlus (RegExp
"AR" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"FS" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
"ST")                     -- (AR|FS|ST)+
            ]