-- SPDX-License-Identifier: MIT
-- Copyright (c) 2021 Chua Hou

-----------------------------------------------------------------------------
-- |
-- Module      : CFGEq.CNF
-- Copyright   : Chua Hou 2021
-- License     : MIT
--
-- Maintainer  : Chua Hou <human+github@chuahou.dev>
-- Stability   : experimental
-- Portability : non-portable
--
-- Compilation of CFGs from 'CFGEq.CFG' to Chomsky normal form.
-----------------------------------------------------------------------------

{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE ScopedTypeVariables #-}

module CFGEq.CNF ( CNF (..)
                 , CNFProduction
                 , compile
                 , enumerate
                 ) where

import           Control.Monad       (forM)
import           Control.Monad.State (State, get, put, runState)
import           Data.Map            (Map)
import qualified Data.Map            as Map
import           Data.Maybe          (fromMaybe, mapMaybe)
import           Data.Set            (Set)
import qualified Data.Set            as Set

import           CFGEq.CFG           (CFG (..), Rule (..))

-- | @CNF v t@ is the type of Chomsky normal form grammars with variables of
-- type @v@ and terminals of type @t@.
data CNF v t = CNF { CNF v t -> Map v (Set (CNFProduction v t))
rulesCNF      :: Map v (Set (CNFProduction v t))
                                           -- ^ Map of variables to their set of rules.
                   , CNF v t -> v
startCNF      :: v    -- ^ The start symbol.
                   , CNF v t -> Bool
producesEmpty :: Bool -- ^ Whether the start symbol produces epsilon.
                   }
    deriving Int -> CNF v t -> ShowS
[CNF v t] -> ShowS
CNF v t -> String
(Int -> CNF v t -> ShowS)
-> (CNF v t -> String) -> ([CNF v t] -> ShowS) -> Show (CNF v t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v t. (Show v, Show t) => Int -> CNF v t -> ShowS
forall v t. (Show v, Show t) => [CNF v t] -> ShowS
forall v t. (Show v, Show t) => CNF v t -> String
showList :: [CNF v t] -> ShowS
$cshowList :: forall v t. (Show v, Show t) => [CNF v t] -> ShowS
show :: CNF v t -> String
$cshow :: forall v t. (Show v, Show t) => CNF v t -> String
showsPrec :: Int -> CNF v t -> ShowS
$cshowsPrec :: forall v t. (Show v, Show t) => Int -> CNF v t -> ShowS
Show

-- | The type of productions in a rule for 'CNF'. Does not allow epsilon
-- productions since 'CNF' captures that for the start symbol as a 'Bool'.
type CNFProduction v t = Either (v, v) t

-- | Cons operator for 'Set's for convenience.
(<:) :: Ord a => a -> Set a -> Set a
<: :: a -> Set a -> Set a
(<:) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert

-- | Compiles a 'CFG' to 'CNF'. Requires the caller to supply a function that
-- supplies fresh variables of the correct type, that should be guaranteed to
-- return a different variable when given a different 'Int' argument.
compile :: forall v t. (Ord v, Ord t)
        => (Int -> v) -- ^ Fresh variable supplier.
        -> CFG v t    -- ^ Grammar to compile.
        -> CNF v t
compile :: (Int -> v) -> CFG v t -> CNF v t
compile Int -> v
mkFresh (CFG Set (Rule v t)
rs v
s) = Map v (Set (CNFProduction v t)) -> v -> Bool -> CNF v t
forall v t. Map v (Set (CNFProduction v t)) -> v -> Bool -> CNF v t
CNF Map v (Set (CNFProduction v t))
rules' v
newS Bool
sEmpty
    where
        -- States here are used to call @mkFresh@ with fresh 'Int's every time
        -- we need a fresh variable, keeping track of the largest number we've
        -- used so far.

        -- START step
        -- Generates a rule with a new start symbol that produces the old start
        -- symbol @oldS@.
        startStep :: v -> State Int (v, Rule v t)
        startStep :: v -> State Int (v, Rule v t)
startStep v
oldS = StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get StateT Int Identity Int
-> (Int -> State Int (v, Rule v t)) -> State Int (v, Rule v t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
gen -> Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Int
forall a. Enum a => a -> a
succ Int
gen) StateT Int Identity ()
-> State Int (v, Rule v t) -> State Int (v, Rule v t)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (v, Rule v t) -> State Int (v, Rule v t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (let s' :: v
s' = Int -> v
mkFresh Int
gen
              in (v
s', v
s' v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> [v -> Either v t
forall a b. a -> Either a b
Left v
oldS]))

        -- BIN step
        -- Converts given rule to a list of equivalent rules each with <= 2
        -- variables on the right hand side.
        bin :: Rule v t -> State Int (Set (Rule v t))
        bin :: Rule v t -> State Int (Set (Rule v t))
bin (v
var :-> (Either v t
a:Either v t
b:Either v t
c:Production v t
cs)) = do
            Int
gen <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
            let f :: v
f = Int -> v
mkFresh Int
gen
            Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> StateT Int Identity ())
-> (Int -> Int) -> Int -> StateT Int Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
succ (Int -> StateT Int Identity ()) -> Int -> StateT Int Identity ()
forall a b. (a -> b) -> a -> b
$ Int
gen
            Set (Rule v t)
recurse <- Rule v t -> State Int (Set (Rule v t))
bin (v
f v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> (Either v t
bEither v t -> Production v t -> Production v t
forall a. a -> [a] -> [a]
:Either v t
cEither v t -> Production v t -> Production v t
forall a. a -> [a] -> [a]
:Production v t
cs))
            Set (Rule v t) -> State Int (Set (Rule v t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Rule v t) -> State Int (Set (Rule v t)))
-> Set (Rule v t) -> State Int (Set (Rule v t))
forall a b. (a -> b) -> a -> b
$ (v
var v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> [Either v t
Item (Production v t)
a, v -> Either v t
forall a b. a -> Either a b
Left v
f]) Rule v t -> Set (Rule v t) -> Set (Rule v t)
forall a. Ord a => a -> Set a -> Set a
<: Set (Rule v t)
recurse
        bin Rule v t
r = Set (Rule v t) -> State Int (Set (Rule v t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Item (Set (Rule v t))
Rule v t
r]

        -- DEL step
        -- Eliminates nullable rules, giving the new list of rules, given the
        -- start symbol and list of already removed rules. At each iteration it
        -- finds a rule \(A \to \epsilon\), removes it, and changes every other
        -- rule containing \(A\) on the RHS.
        del :: v -> Set v -> Set (Rule v t) -> Set (Rule v t)
        del :: v -> Set v -> Set (Rule v t) -> Set (Rule v t)
del v
s' Set v
removed Set (Rule v t)
rs' =
            case Set (Rule v t) -> Maybe (Rule v t)
forall a. Set a -> Maybe a
Set.lookupMin (Set (Rule v t) -> Maybe (Rule v t))
-> Set (Rule v t) -> Maybe (Rule v t)
forall a b. (a -> b) -> a -> b
$
                (Rule v t -> Bool) -> Set (Rule v t) -> Set (Rule v t)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(v
var :-> Production v t
w) -> Production v t -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Production v t
w Bool -> Bool -> Bool
&& v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
s') Set (Rule v t)
rs' of
              Maybe (Rule v t)
Nothing          -> Set (Rule v t)
rs'
              Just (v
var :-> Production v t
_) -> v -> Set v -> Set (Rule v t) -> Set (Rule v t)
del v
s' (v
var v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
<: Set v
removed)
                                (Set (Rule v t) -> Set (Rule v t))
-> (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set (Rule v t)) -> Set (Rule v t)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Set (Rule v t)) -> Set (Rule v t))
-> (Set (Rule v t) -> Set (Set (Rule v t)))
-> Set (Rule v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule v t -> Set (Rule v t))
-> Set (Rule v t) -> Set (Set (Rule v t))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (v -> Rule v t -> Set (Rule v t)
go v
var) (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t) -> Set (Rule v t)
forall a b. (a -> b) -> a -> b
$ Set (Rule v t)
rs'
            where
                -- Generate the list of corresponding new rules based on @var@
                -- being nullable.
                go :: v -> Rule v t -> Set (Rule v t)
                go :: v -> Rule v t -> Set (Rule v t)
go v
var (v
var' :-> Production v t
w)
                    | v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
var' Bool -> Bool -> Bool
&& Production v t -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Production v t
w = [] -- Remove this rule.
                    | Bool
otherwise = (Production v t -> Rule v t)
-> Set (Production v t) -> Set (Rule v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (v
var' v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:->)
                                    -- Remove any added epsilon rule if it's
                                    -- been removed before.
                                (Set (Production v t) -> Set (Rule v t))
-> (Set (Production v t) -> Set (Production v t))
-> Set (Production v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if v
var' v -> Set v -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (v
var v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
<: Set v
removed)
                                      then Production v t -> Set (Production v t) -> Set (Production v t)
forall a. Ord a => a -> Set a -> Set a
Set.delete []
                                      else Set (Production v t) -> Set (Production v t)
forall a. a -> a
id)
                                (Set (Production v t) -> Set (Rule v t))
-> Set (Production v t) -> Set (Rule v t)
forall a b. (a -> b) -> a -> b
$ v -> Production v t -> Set (Production v t)
go' v
var Production v t
w
                go' :: v -> [Either v t] -> Set [Either v t]
                go' :: v -> Production v t -> Set (Production v t)
go' v
_ [] = [[]]
                go' v
var (Left v
v:Production v t
w)
                    | v
var v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v  = Set (Production v t)
next Set (Production v t)
-> Set (Production v t) -> Set (Production v t)
forall a. Semigroup a => a -> a -> a
<> (Production v t -> Production v t)
-> Set (Production v t) -> Set (Production v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (v -> Either v t
forall a b. a -> Either a b
Left v
vEither v t -> Production v t -> Production v t
forall a. a -> [a] -> [a]
:) Set (Production v t)
next
                    | Bool
otherwise = (Production v t -> Production v t)
-> Set (Production v t) -> Set (Production v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (v -> Either v t
forall a b. a -> Either a b
Left v
vEither v t -> Production v t -> Production v t
forall a. a -> [a] -> [a]
:) Set (Production v t)
next
                    where next :: Set (Production v t)
next = v -> Production v t -> Set (Production v t)
go' v
var Production v t
w
                go' v
var (Right t
t:Production v t
w) = (Production v t -> Production v t)
-> Set (Production v t) -> Set (Production v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (t -> Either v t
forall a b. b -> Either a b
Right t
tEither v t -> Production v t -> Production v t
forall a. a -> [a] -> [a]
:) (Set (Production v t) -> Set (Production v t))
-> Set (Production v t) -> Set (Production v t)
forall a b. (a -> b) -> a -> b
$ v -> Production v t -> Set (Production v t)
go' v
var Production v t
w

        -- UNIT step
        -- Eliminates unit rules of form \(A \to B\), given a set of already
        -- removed unit rules.
        unit :: Set (Rule v t) -> Set (Rule v t) -> Set (Rule v t)
        unit :: Set (Rule v t) -> Set (Rule v t) -> Set (Rule v t)
unit Set (Rule v t)
removed Set (Rule v t)
s' =
            case Set (Rule v t) -> Maybe (Rule v t)
forall a. Set a -> Maybe a
Set.lookupMin (Set (Rule v t) -> Maybe (Rule v t))
-> Set (Rule v t) -> Maybe (Rule v t)
forall a b. (a -> b) -> a -> b
$
                (Rule v t -> Bool) -> Set (Rule v t) -> Set (Rule v t)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\(v
_ :-> Production v t
w) -> case Production v t
w of
                                            [Left _] -> Bool
True
                                            Production v t
_        -> Bool
False) Set (Rule v t)
s' of
                Maybe (Rule v t)
Nothing                  -> Set (Rule v t)
s'
                Just r :: Rule v t
r@(v
v :-> [Left v']) -> Set (Rule v t) -> Set (Rule v t) -> Set (Rule v t)
unit (Rule v t
r Rule v t -> Set (Rule v t) -> Set (Rule v t)
forall a. Ord a => a -> Set a -> Set a
<: Set (Rule v t)
removed)
                                          (Set (Rule v t) -> Set (Rule v t))
-> (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set (Rule v t)) -> Set (Rule v t)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Set (Rule v t)) -> Set (Rule v t))
-> (Set (Rule v t) -> Set (Set (Rule v t)))
-> Set (Rule v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule v t -> Set (Rule v t))
-> Set (Rule v t) -> Set (Set (Rule v t))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (v -> v -> Rule v t -> Set (Rule v t)
go v
v v
v') (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t) -> Set (Rule v t)
forall a b. (a -> b) -> a -> b
$ Set (Rule v t)
s'
                Maybe (Rule v t)
_                        -> String -> Set (Rule v t)
forall a. HasCallStack => String -> a
error String
"Unreachable 'unit'"
            where
                -- Performs relevant changes for unit rule \(v \to v'\) on rule
                -- @r@. Removes \(v \to v'\) and replaces all \(v' \to w\) with
                -- both \(v \to w\) and \(v' \to w\).
                go :: v -> v -> Rule v t -> Set (Rule v t)
                go :: v -> v -> Rule v t -> Set (Rule v t)
go v
v v
v' r :: Rule v t
r@(v
u :-> Production v t
w)
                    -- Remove the current rule.
                    | v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
u Bool -> Bool -> Bool
&& Production v t
w Production v t -> Production v t -> Bool
forall a. Eq a => a -> a -> Bool
== [v -> Either v t
forall a b. a -> Either a b
Left v
v'] = []
                    -- Don't add a rule that's already removed.
                    | v
v' v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
u Bool -> Bool -> Bool
&& Bool -> Bool
not (Rule v t -> Set (Rule v t) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (v
v v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> Production v t
w) Set (Rule v t)
removed)
                                               = [v
v v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> Production v t
w, Item (Set (Rule v t))
Rule v t
r]
                    | Bool
otherwise                = [Item (Set (Rule v t))
Rule v t
r]

        -- TERM step
        -- Converts given rule into one with no nonsolitary terminals.
        term :: Set (Rule v t) -> State Int (Set (Rule v t))
        term :: Set (Rule v t) -> State Int (Set (Rule v t))
term Set (Rule v t)
s' = State Int (Map t v)
termVars State Int (Map t v)
-> (Map t v -> State Int (Set (Rule v t)))
-> State Int (Set (Rule v t))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Map t v
termVars' -> Set (Rule v t) -> State Int (Set (Rule v t))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Rule v t) -> State Int (Set (Rule v t)))
-> Set (Rule v t) -> State Int (Set (Rule v t))
forall a b. (a -> b) -> a -> b
$ (Rule v t -> Rule v t) -> Set (Rule v t) -> Set (Rule v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map t v -> Rule v t -> Rule v t
go Map t v
termVars') Set (Rule v t)
s'

                    -- New rules corresponding to @termVars'@.
                    Set (Rule v t) -> Set (Rule v t) -> Set (Rule v t)
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ((t, v) -> Rule v t) -> Set (t, v) -> Set (Rule v t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\(t
t, v
v) -> v
v v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> [t -> Either v t
forall a b. b -> Either a b
Right t
t])
                                    ([(t, v)] -> Set (t, v)
forall a. Ord a => [a] -> Set a
Set.fromList ([(t, v)] -> Set (t, v))
-> (Map t v -> [(t, v)]) -> Map t v -> Set (t, v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map t v -> [(t, v)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map t v -> Set (t, v)) -> Map t v -> Set (t, v)
forall a b. (a -> b) -> a -> b
$ Map t v
termVars')

            where
                -- Extract list of unique terminals.
                terminals :: [t]
                terminals :: [t]
terminals = Set t -> [t]
forall a. Set a -> [a]
Set.toList (Set t -> [t])
-> (Set (Rule v t) -> Set t) -> Set (Rule v t) -> [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set t) -> Set t
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Set t) -> Set t)
-> (Set (Rule v t) -> Set (Set t)) -> Set (Rule v t) -> Set t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule v t -> Set t) -> Set (Rule v t) -> Set (Set t)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Rule v t -> Set t
forall a b. Ord a => Rule b a -> Set a
go' (Set (Rule v t) -> [t]) -> Set (Rule v t) -> [t]
forall a b. (a -> b) -> a -> b
$ Set (Rule v t)
s'
                    where
                        go' :: Rule b a -> Set a
go' (b
_ :-> Production b a
w) = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$
                            (Either b a -> Maybe a) -> Production b a -> [a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((b -> Maybe a) -> (a -> Maybe a) -> Either b a -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> b -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) a -> Maybe a
forall a. a -> Maybe a
Just) Production b a
w

                -- Assign each terminal to a fresh variable.
                termVars :: State Int (Map t v)
                termVars :: State Int (Map t v)
termVars = ([(t, v)] -> Map t v)
-> StateT Int Identity [(t, v)] -> State Int (Map t v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(t, v)] -> Map t v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (StateT Int Identity [(t, v)] -> State Int (Map t v))
-> ((t -> StateT Int Identity (t, v))
    -> StateT Int Identity [(t, v)])
-> (t -> StateT Int Identity (t, v))
-> State Int (Map t v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [t]
-> (t -> StateT Int Identity (t, v))
-> StateT Int Identity [(t, v)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [t]
terminals ((t -> StateT Int Identity (t, v)) -> State Int (Map t v))
-> (t -> StateT Int Identity (t, v)) -> State Int (Map t v)
forall a b. (a -> b) -> a -> b
$ (\t
t -> do
                    Int
gen <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
                    Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> StateT Int Identity ())
-> (Int -> Int) -> Int -> StateT Int Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Enum a => a -> a
succ (Int -> StateT Int Identity ()) -> Int -> StateT Int Identity ()
forall a b. (a -> b) -> a -> b
$ Int
gen
                    (t, v) -> StateT Int Identity (t, v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t
t, Int -> v
mkFresh Int
gen))

                -- Replace all non-unit occurrences of terminals with the fresh
                -- variable.
                go :: Map t v -> Rule v t -> Rule v t
                go :: Map t v -> Rule v t -> Rule v t
go Map t v
m (v
v :-> p :: Production v t
p@[Item (Production v t)
_, Item (Production v t)
_]) = v
v v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> (Either v t -> Either v t) -> Production v t -> Production v t
forall a b. (a -> b) -> [a] -> [b]
map Either v t -> Either v t
forall b. Either v t -> Either v b
go' Production v t
p
                    where go' :: Either v t -> Either v b
go' = (v -> Either v b) -> (t -> Either v b) -> Either v t -> Either v b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either v -> Either v b
forall a b. a -> Either a b
Left (v -> Either v b
forall a b. a -> Either a b
Left (v -> Either v b) -> (t -> v) -> t -> Either v b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map t v
m Map t v -> t -> v
forall k a. Ord k => Map k a -> k -> a
Map.!))
                go Map t v
_ Rule v t
r = Rule v t
r

        -- Converts a CFG rule into a CNF rule. Errors impurely when the CFG
        -- rule cannot be converted to a CNF rule since this is an internal
        -- algorithmic error. TODO: We might consider using more fine-grained
        -- types capturing the properties introduced by each step in the future.
        toCNF :: Rule v t -> (v, Set (Either (v, v) t))
        toCNF :: Rule v t -> (v, Set (CNFProduction v t))
toCNF (v
var :-> [Left a, Left b]) = (v
var, [(v, v) -> CNFProduction v t
forall a b. a -> Either a b
Left (v
a, v
b)])
        toCNF (v
var :-> [Right c])        = (v
var, [t -> CNFProduction v t
forall a b. b -> Either a b
Right t
c])
        toCNF Rule v t
_                          = String -> (v, Set (CNFProduction v t))
forall a. HasCallStack => String -> a
error String
"toCNF internal error"

        -- Putting them all together.
        (v
newS, Map v (Set (CNFProduction v t))
rules', Bool
sEmpty) = ((v, Map v (Set (CNFProduction v t)), Bool), Int)
-> (v, Map v (Set (CNFProduction v t)), Bool)
forall a b. (a, b) -> a
fst (((v, Map v (Set (CNFProduction v t)), Bool), Int)
 -> (v, Map v (Set (CNFProduction v t)), Bool))
-> (State Int (v, Map v (Set (CNFProduction v t)), Bool)
    -> ((v, Map v (Set (CNFProduction v t)), Bool), Int))
-> State Int (v, Map v (Set (CNFProduction v t)), Bool)
-> (v, Map v (Set (CNFProduction v t)), Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State Int (v, Map v (Set (CNFProduction v t)), Bool)
 -> Int -> ((v, Map v (Set (CNFProduction v t)), Bool), Int))
-> Int
-> State Int (v, Map v (Set (CNFProduction v t)), Bool)
-> ((v, Map v (Set (CNFProduction v t)), Bool), Int)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int (v, Map v (Set (CNFProduction v t)), Bool)
-> Int -> ((v, Map v (Set (CNFProduction v t)), Bool), Int)
forall s a. State s a -> s -> (a, s)
runState Int
0 (State Int (v, Map v (Set (CNFProduction v t)), Bool)
 -> (v, Map v (Set (CNFProduction v t)), Bool))
-> State Int (v, Map v (Set (CNFProduction v t)), Bool)
-> (v, Map v (Set (CNFProduction v t)), Bool)
forall a b. (a -> b) -> a -> b
$ do
            (v
s', Rule v t
startRule) <- v -> State Int (v, Rule v t)
startStep v
s
            Set (Rule v t)
binRules        <- [Set (Rule v t)] -> Set (Rule v t)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Rule v t)] -> Set (Rule v t))
-> StateT Int Identity [Set (Rule v t)]
-> State Int (Set (Rule v t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Rule v t -> State Int (Set (Rule v t)))
-> [Rule v t] -> StateT Int Identity [Set (Rule v t)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Rule v t -> State Int (Set (Rule v t))
bin (Set (Rule v t) -> [Rule v t]
forall a. Set a -> [a]
Set.toList (Rule v t
startRule Rule v t -> Set (Rule v t) -> Set (Rule v t)
forall a. Ord a => a -> Set a -> Set a
<: Set (Rule v t)
rs))
            let delUnitRules :: Set (Rule v t)
delUnitRules = Set (Rule v t) -> Set (Rule v t) -> Set (Rule v t)
unit [] (Set (Rule v t) -> Set (Rule v t))
-> (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t)
-> Set (Rule v t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Set v -> Set (Rule v t) -> Set (Rule v t)
del v
s' [] (Set (Rule v t) -> Set (Rule v t))
-> Set (Rule v t) -> Set (Rule v t)
forall a b. (a -> b) -> a -> b
$ Set (Rule v t)
binRules
            Set (Rule v t)
termRules       <- Set (Rule v t) -> State Int (Set (Rule v t))
term Set (Rule v t)
delUnitRules
            let sEmpty' :: Bool
sEmpty'      = Rule v t -> Set (Rule v t) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (v
s' v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> []) Set (Rule v t)
termRules
            let noEmptyRules :: Set (Rule v t)
noEmptyRules = Rule v t -> Set (Rule v t) -> Set (Rule v t)
forall a. Ord a => a -> Set a -> Set a
Set.delete (v
s' v -> Production v t -> Rule v t
forall v t. v -> Production v t -> Rule v t
:-> []) Set (Rule v t)
termRules
            (v, Map v (Set (CNFProduction v t)), Bool)
-> State Int (v, Map v (Set (CNFProduction v t)), Bool)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( v
s'
                 , (Set (CNFProduction v t)
 -> Set (CNFProduction v t) -> Set (CNFProduction v t))
-> [(v, Set (CNFProduction v t))]
-> Map v (Set (CNFProduction v t))
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set (CNFProduction v t)
-> Set (CNFProduction v t) -> Set (CNFProduction v t)
forall a. Semigroup a => a -> a -> a
(<>) ([(v, Set (CNFProduction v t))] -> Map v (Set (CNFProduction v t)))
-> (Set (Rule v t) -> [(v, Set (CNFProduction v t))])
-> Set (Rule v t)
-> Map v (Set (CNFProduction v t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule v t -> (v, Set (CNFProduction v t)))
-> [Rule v t] -> [(v, Set (CNFProduction v t))]
forall a b. (a -> b) -> [a] -> [b]
map Rule v t -> (v, Set (CNFProduction v t))
toCNF ([Rule v t] -> [(v, Set (CNFProduction v t))])
-> (Set (Rule v t) -> [Rule v t])
-> Set (Rule v t)
-> [(v, Set (CNFProduction v t))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Rule v t) -> [Rule v t]
forall a. Set a -> [a]
Set.toList (Set (Rule v t) -> Map v (Set (CNFProduction v t)))
-> Set (Rule v t) -> Map v (Set (CNFProduction v t))
forall a b. (a -> b) -> a -> b
$ Set (Rule v t)
noEmptyRules
                 , Bool
sEmpty'
                 )

-- | @enumerate n c@ returns the set of all strings generated by @c@ of length
-- @n@ or less.
enumerate :: forall v t. (Ord v, Ord t)
          => Int     -- ^ Maximum length of string to generate.
          -> CNF v t -- ^ Chomsky normal form grammar to use.
          -> Set [t]
enumerate :: Int -> CNF v t -> Set [t]
enumerate Int
n (CNF Map v (Set (CNFProduction v t))
r v
s Bool
e) = (if Bool
e then [t] -> Set [t]
forall a. a -> Set a
Set.singleton [] else Set [t]
forall a. Set a
Set.empty)
        Set [t] -> Set [t] -> Set [t]
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Int -> [Either v t] -> Set [t]
go Int
n [v -> Either v t
forall a b. a -> Either a b
Left v
s]

    where
        -- Generate all possible strings of terminals of less than of equal the
        -- given length from the given string.
        go :: Int -> [Either v t] -> Set [t]
        go :: Int -> [Either v t] -> Set [t]
go Int
_  []          = [t] -> Set [t]
forall a. a -> Set a
Set.singleton []
        go Int
n' (Right t
t:[Either v t]
w) = ([t] -> [t]) -> Set [t] -> Set [t]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (t
tt -> [t] -> [t]
forall a. a -> [a] -> [a]
:) (Set [t] -> Set [t]) -> Set [t] -> Set [t]
forall a b. (a -> b) -> a -> b
$ Int -> [Either v t] -> Set [t]
go (Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Either v t]
w
        go Int
n' (Left v
v:[Either v t]
w)  = Set (Set [t]) -> Set [t]
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set (Set [t]) -> Set [t])
-> (Set [Either v t] -> Set (Set [t]))
-> Set [Either v t]
-> Set [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Either v t] -> Set [t]) -> Set [Either v t] -> Set (Set [t])
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Int -> [Either v t] -> Set [t]
go Int
n') (Set [Either v t] -> Set [t]) -> Set [Either v t] -> Set [t]
forall a b. (a -> b) -> a -> b
$ Set [Either v t]
vprods'
            where
                -- Possibilities that @v@ can become.
                vprods :: Set (CNFProduction v t)
                vprods :: Set (CNFProduction v t)
vprods = Set (CNFProduction v t)
-> Maybe (Set (CNFProduction v t)) -> Set (CNFProduction v t)
forall a. a -> Maybe a -> a
fromMaybe Set (CNFProduction v t)
forall a. Set a
Set.empty (Maybe (Set (CNFProduction v t)) -> Set (CNFProduction v t))
-> Maybe (Set (CNFProduction v t)) -> Set (CNFProduction v t)
forall a b. (a -> b) -> a -> b
$ v
-> Map v (Set (CNFProduction v t))
-> Maybe (Set (CNFProduction v t))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v (Set (CNFProduction v t))
r

                -- Make possibilities @vprods@ into a set of resulting strings
                -- after applying each possibility, then restrict them to the
                -- given length.
                vprods' :: Set [Either v t]
                vprods' :: Set [Either v t]
vprods' = ([Either v t] -> Bool) -> Set [Either v t] -> Set [Either v t]
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n') (Int -> Bool) -> ([Either v t] -> Int) -> [Either v t] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either v t] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) (Set [Either v t] -> Set [Either v t])
-> (Set (CNFProduction v t) -> Set [Either v t])
-> Set (CNFProduction v t)
-> Set [Either v t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CNFProduction v t -> [Either v t])
-> Set (CNFProduction v t) -> Set [Either v t]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map CNFProduction v t -> [Either v t]
go' (Set (CNFProduction v t) -> Set [Either v t])
-> Set (CNFProduction v t) -> Set [Either v t]
forall a b. (a -> b) -> a -> b
$ Set (CNFProduction v t)
vprods
                    where
                        go' :: CNFProduction v t -> [Either v t]
go' (Left (v
v1, v
v2)) = v -> Either v t
forall a b. a -> Either a b
Left v
v1 Either v t -> [Either v t] -> [Either v t]
forall a. a -> [a] -> [a]
: v -> Either v t
forall a b. a -> Either a b
Left v
v2 Either v t -> [Either v t] -> [Either v t]
forall a. a -> [a] -> [a]
: [Either v t]
w
                        go' (Right t
t)       = t -> Either v t
forall a b. b -> Either a b
Right t
t Either v t -> [Either v t] -> [Either v t]
forall a. a -> [a] -> [a]
: [Either v t]
w