{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | Coalgebraic compiler: parser syntax trees become Process state machines.
--
-- A parser in 'Circuit.Parser.Syntax' is already a relation.  This
-- module turns that relation into a coalgebra by Brzozowski derivation:
--
-- * machine state = a parser syntax tree;
-- * input token   = the next stream element;
-- * transition    = Brzozowski derivative of the current tree;
-- * output        = the nullable value of the current tree, if any.
--
-- The regular/applicative fragment is fully supported: primitives, '@<|>@',
-- '@<*@', 'fmap', and 'many'.  'CombBind' is rejected because it is dependent
-- composition.  Explicit 'SigCompose' nodes are also rejected; use the
-- 'Functor'/'Applicative'/'Alternative' constructors instead.
--
-- === doctests
--
-- >>> import Circuit.Process (scan, fold)
-- >>> import Circuit.Parser.Syntax (charS, stringS, manyS)
-- >>> import Control.Applicative ((<|>))
--
-- >>> scan (compileProcess (stringS "ab" <|> stringS "a" :: ParserSyntax String Char String)) "ab"
-- [Just "a",Just "ab"]
--
-- >>> fold (compileProcess (stringS "ab" <|> stringS "a" :: ParserSyntax String Char String)) "ab"
-- Just (Just "ab")
--
-- >>> scan (compileProcess (manyS (charS 'a') :: ParserSyntax String Char String)) "aaab"
-- [Just "a",Just "aa",Just "aaa",Nothing]
module Circuit.Parser.ProcessCompiler
  ( -- * Plain Process compiler
    compileProcess,
    compileProcessWithInput,
  )
where

import Circuit.Parser (Uncons (..))
import Circuit.Parser.Syntax (ParserSyntax, derive, nullableValue)
import Circuit.Process (Process (..))
import Data.Proxy (Proxy (..))
import Data.These (These (..))
import Prelude

-- $setup
-- >>> import Circuit.Process (scan, fold)
-- >>> import Circuit.Parser.Syntax (ParserSyntax, charS, stringS, manyS)
-- >>> import Control.Applicative ((<|>))

-- | Drop one element from a stream, returning the empty stream if the element
-- was the last one.
dropOne :: forall f s. (Uncons f s) => Proxy s -> f -> f
dropOne :: forall f s. Uncons f s => Proxy s -> f -> f
dropOne Proxy s
_ f
xs = case forall f s. Uncons f s => f -> These s f
uncons @f @s f
xs of
  These s
_ f
rest -> f
rest
  This s
_ -> forall f s. Uncons f s => f
nil @f @s
  That f
_ -> f
xs

-- ---------------------------------------------------------------------------
-- Plain Process compiler
-- ---------------------------------------------------------------------------

-- | Compile a parser into a Process machine whose output is the parse result of
-- the prefix consumed so far.
--
-- The machine state is the Brzozowski derivative of the original parser after
-- the tokens seen to date.  Extraction succeeds exactly when that derivative
-- is nullable.
--
-- >>> scan (compileProcess (stringS "ab" <|> stringS "a" :: ParserSyntax String Char String)) "ab"
-- [Just "a",Just "ab"]
compileProcess ::
  (Eq s, Uncons f s) =>
  ParserSyntax f s a ->
  Process s (Maybe a)
compileProcess :: forall s f a.
(Eq s, Uncons f s) =>
ParserSyntax f s a -> Process s (Maybe a)
compileProcess ParserSyntax f s a
p0 = (s -> ParserSyntax f s a)
-> (ParserSyntax f s a -> s -> ParserSyntax f s a)
-> (ParserSyntax f s a -> Maybe a)
-> Process s (Maybe a)
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process s -> ParserSyntax f s a
inject ParserSyntax f s a -> s -> ParserSyntax f s a
forall {s} {f} {a}.
(Eq s, Uncons f s) =>
ParserSyntax f s a -> s -> ParserSyntax f s a
step ParserSyntax f s a -> Maybe a
forall {a}. ParserSyntax f s a -> Maybe a
extract
  where
    inject :: s -> ParserSyntax f s a
inject s
c = s -> ParserSyntax f s a -> ParserSyntax f s a
forall s f a.
(Eq s, Uncons f s) =>
s -> ParserSyntax f s a -> ParserSyntax f s a
derive s
c ParserSyntax f s a
p0
    step :: ParserSyntax f s a -> s -> ParserSyntax f s a
step ParserSyntax f s a
p s
c = s -> ParserSyntax f s a -> ParserSyntax f s a
forall s f a.
(Eq s, Uncons f s) =>
s -> ParserSyntax f s a -> ParserSyntax f s a
derive s
c ParserSyntax f s a
p
    extract :: ParserSyntax f s a -> Maybe a
extract = ParserSyntax f s a -> Maybe a
forall f s a. Uncons f s => ParserSyntax f s a -> Maybe a
nullableValue

-- | Compile a parser into a Process machine tied to a known input stream.
--
-- The state carries the current derivative /and/ the remaining suffix of the
-- input.  This lets extraction return both a parse result and the leftover
-- stream, matching the usual parser output shape.
--
-- Because a 'Process' has no explicit initial state, the input stream is
-- captured at compile time and threaded through 'inject' and 'step'.
--
-- >>> scan (compileProcessWithInput "ab" (stringS "ab" <|> stringS "a" :: ParserSyntax String Char String)) "ab"
-- [Just ("a","b"),Just ("ab","")]
compileProcessWithInput ::
  forall f s a.
  (Eq s, Uncons f s) =>
  f ->
  ParserSyntax f s a ->
  Process s (Maybe (a, f))
compileProcessWithInput :: forall f s a.
(Eq s, Uncons f s) =>
f -> ParserSyntax f s a -> Process s (Maybe (a, f))
compileProcessWithInput f
input ParserSyntax f s a
p0 = (s -> (ParserSyntax f s a, f))
-> ((ParserSyntax f s a, f) -> s -> (ParserSyntax f s a, f))
-> ((ParserSyntax f s a, f) -> Maybe (a, f))
-> Process s (Maybe (a, f))
forall s a b. (a -> s) -> (s -> a -> s) -> (s -> b) -> Process a b
Process s -> (ParserSyntax f s a, f)
inject (ParserSyntax f s a, f) -> s -> (ParserSyntax f s a, f)
step (ParserSyntax f s a, f) -> Maybe (a, f)
forall {f} {s} {a} {t}.
Uncons f s =>
(ParserSyntax f s a, t) -> Maybe (a, t)
extract
  where
    inject :: s -> (ParserSyntax f s a, f)
inject s
c = (s -> ParserSyntax f s a -> ParserSyntax f s a
forall s f a.
(Eq s, Uncons f s) =>
s -> ParserSyntax f s a -> ParserSyntax f s a
derive s
c ParserSyntax f s a
p0, Proxy s -> f -> f
forall f s. Uncons f s => Proxy s -> f -> f
dropOne (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) f
input)
    step :: (ParserSyntax f s a, f) -> s -> (ParserSyntax f s a, f)
step (ParserSyntax f s a
p, f
rest) s
c = (s -> ParserSyntax f s a -> ParserSyntax f s a
forall s f a.
(Eq s, Uncons f s) =>
s -> ParserSyntax f s a -> ParserSyntax f s a
derive s
c ParserSyntax f s a
p, Proxy s -> f -> f
forall f s. Uncons f s => Proxy s -> f -> f
dropOne (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) f
rest)
    extract :: (ParserSyntax f s a, t) -> Maybe (a, t)
extract (ParserSyntax f s a
p, t
rest) = (,t
rest) (a -> (a, t)) -> Maybe a -> Maybe (a, t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserSyntax f s a -> Maybe a
forall f s a. Uncons f s => ParserSyntax f s a -> Maybe a
nullableValue ParserSyntax f s a
p