{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy         #-}
-- | Context free grammars, where
-- each production is a regular-expression.
module RERE.CFG (
    -- * Context-free grammars
    CFG,
    CFGBase,
    -- * Conversion to recursive regular expressions
    cfgToRE,
    ) where

import Data.Fin      (Fin (..))
import Data.Nat      (Nat (..))
import Data.Vec.Lazy (Vec (..))

import qualified Data.Type.Nat as N
import qualified Data.Vec.Lazy as V

import RERE.Type
import RERE.Var

#if !MIN_VERSION_base(4,8,0)
import Data.Traversable (Traversable (..))
#endif

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import Data.Fin      (Fin (..))
-- >>> import Data.Vec.Lazy (Vec (..))
-- >>> import RERE

-- | Context-free grammar represented as @n@ equations
-- of 'RE' ('CFGBase') with @n@ variables.
--
type CFG n a = Vec n (CFGBase n a)

-- | Single equation in context-free-grammar equation.
type CFGBase n a = RE (Either (Fin n) a)

-- | Convert 'CFG' (with names for productions) into 'RE'.
-- Note: the start symbol have to be last equation.
--
-- >>> let a = Eps \/ ch_ 'a' <> Var (Left FZ)
-- >>> let b = Eps \/ ch_ 'b' <> Var (Left (FS FZ))
-- >>> let cfg = b ::: a ::: VNil
--
-- \[
-- \begin{aligned}
-- {\mathit{b}} &= {\varepsilon}\cup\mathtt{b}{\mathit{a}} \\
-- {\mathit{a}} &= {\varepsilon}\cup\mathtt{a}{\mathit{b}} \\
-- \end{aligned}
-- \]
--
-- >>> cfgToRE ("b" ::: "a" ::: VNil) cfg
-- Fix "a" (Let "b" (Alt Eps (App (Ch "b") (Var B))) (Alt Eps (App (Ch "a") (Var B))))
--
-- which represents \(\mathbf{fix}\,{\mathit{a}}=\mathbf{let}\,{\mathit{b}}={\varepsilon}\cup\mathtt{b}{\mathit{a}}\,\mathbf{in}\,{\varepsilon}\cup\mathtt{a}{\mathit{b}}\)
-- recursive regular expression.
--
cfgToRE :: (N.SNatI n, Ord a) => Vec ('S n) Name -> CFG ('S n) a -> RE a
cfgToRE :: forall (n :: Nat) a.
(SNatI n, Ord a) =>
Vec ('S n) Name -> CFG ('S n) a -> RE a
cfgToRE = forall (n :: Nat) a.
CfgToRE n a -> Vec ('S n) Name -> CFG ('S n) a -> RE a
getCfgToRE (forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
N.induction1 CfgToRE 'Z a
start forall a (m :: Nat). Ord a => CfgToRE m a -> CfgToRE ('S m) a
step) where
    start :: CfgToRE 'Z a
start = forall (n :: Nat) a.
(Vec ('S n) Name -> CFG ('S n) a -> RE a) -> CfgToRE n a
CfgToRE forall a. Ord a => Vec Nat1 Name -> CFG Nat1 a -> RE a
baseCase

    step :: Ord a => CfgToRE m a -> CfgToRE ('S m) a
    step :: forall a (m :: Nat). Ord a => CfgToRE m a -> CfgToRE ('S m) a
step (CfgToRE Vec ('S m) Name -> CFG ('S m) a -> RE a
rec) = forall (n :: Nat) a.
(Vec ('S n) Name -> CFG ('S n) a -> RE a) -> CfgToRE n a
CfgToRE forall a b. (a -> b) -> a -> b
$ \Vec ('S ('S m)) Name
names CFG ('S ('S m)) a
cfg ->
        Vec ('S m) Name -> CFG ('S m) a -> RE a
rec (forall (n :: Nat) a. Vec ('S n) a -> Vec n a
V.tail Vec ('S ('S m)) Name
names) (forall a (n :: Nat).
Ord a =>
Vec ('S n) Name -> CFG ('S n) a -> CFG n a
consCase Vec ('S ('S m)) Name
names CFG ('S ('S m)) a
cfg)

newtype CfgToRE n a = CfgToRE { forall (n :: Nat) a.
CfgToRE n a -> Vec ('S n) Name -> CFG ('S n) a -> RE a
getCfgToRE :: Vec ('S n) Name -> CFG ('S n) a -> RE a }

baseCase :: Ord a => Vec N.Nat1 Name -> CFG N.Nat1 a -> RE a
baseCase :: forall a. Ord a => Vec Nat1 Name -> CFG Nat1 a -> RE a
baseCase (Name
name ::: Vec n1 Name
VNil) (CFGBase Nat1 a
cfg ::: Vec n1 (CFGBase Nat1 a)
VNil) =
    forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
name (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Fin Nat1
FZ -> forall a. Var a
B) forall a. a -> Var a
F) CFGBase Nat1 a
cfg)
#if __GLASGOW_HASKELL__  <711
baseCase _ _ = error "silly GHC"
#endif

consCase
    :: forall a n. Ord a
    => Vec ('S n) Name
    -> CFG ('S n) a
    -> CFG n a
consCase :: forall a (n :: Nat).
Ord a =>
Vec ('S n) Name -> CFG ('S n) a -> CFG n a
consCase (Name
name ::: Vec n1 Name
_names) (CFGBase ('S n) a
f ::: Vec n1 (CFGBase ('S n) a)
gs) =
    forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
V.map (\CFGBase ('S n) a
g -> forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
name CFGBase n a
f' (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Fin ('S n)) a -> Var (Either (Fin n) a)
sub CFGBase ('S n) a
g)) Vec n1 (CFGBase ('S n) a)
gs
  where
    f' :: CFGBase n a
f' = forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
name (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Fin ('S n)) a -> Var (Either (Fin n) a)
sub' CFGBase ('S n) a
f)

    sub :: Either (Fin ('S n)) a -> Var (Either (Fin n) a)
    sub :: Either (Fin ('S n)) a -> Var (Either (Fin n) a)
sub (Right a
a)     = forall a. a -> Var a
F (forall a b. b -> Either a b
Right a
a)
    sub (Left (FS Fin n1
n)) = forall a. a -> Var a
F (forall a b. a -> Either a b
Left Fin n1
n)
    sub (Left Fin ('S n)
FZ)     = forall a. Var a
B

    sub' :: Either (Fin ('S n)) a -> Var (Either (Fin n) a)
    sub' :: Either (Fin ('S n)) a -> Var (Either (Fin n) a)
sub' (Right a
a)     = forall a. a -> Var a
F (forall a b. b -> Either a b
Right a
a)
    sub' (Left (FS Fin n1
n)) = forall a. a -> Var a
F (forall a b. a -> Either a b
Left Fin n1
n)
    sub' (Left Fin ('S n)
FZ)     = forall a. Var a
B

-------------------------------------------------------------------------------
-- Dummier fix and let
-------------------------------------------------------------------------------

-- This functions only rearrange fix and let,
-- and don't perform other simplifications.

fix' :: Eq a => Name -> RE (Var a) -> RE a
-- fix' n (Let m r s)
--     | Just r' <- traverse (unvar Nothing Just) r
--     = Let m r' (fix' n (fmap swapVar s))
fix' :: forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
n RE (Var a)
r
    | Just RE a
r' <- forall a b.
(Eq a, Eq b) =>
RE (Var a)
-> (Var a -> Maybe b)
-> (RE (Var (Var a)) -> RE (Var b))
-> Maybe (RE b)
floatOut RE (Var a)
r (forall r a. r -> (a -> r) -> Var a -> r
unvar forall a. Maybe a
Nothing forall a. a -> Maybe a
Just) (forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
n)
    = RE a
r'
    | Just RE a
r' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall r a. r -> (a -> r) -> Var a -> r
unvar forall a. Maybe a
Nothing forall a. a -> Maybe a
Just) RE (Var a)
r
    = RE a
r'
fix' Name
n RE (Var a)
r = forall a. Name -> RE (Var a) -> RE a
Fix Name
n RE (Var a)
r

floatOut
    :: (Eq a, Eq b)
    => RE (Var a)                        -- ^ expression
    -> (Var a -> Maybe b)                -- ^ float out var
    -> (RE (Var (Var a)) -> RE (Var b))  -- ^ binder
    -> Maybe (RE b)                      -- ^ maybe an expression with let floaten out
floatOut :: forall a b.
(Eq a, Eq b) =>
RE (Var a)
-> (Var a -> Maybe b)
-> (RE (Var (Var a)) -> RE (Var b))
-> Maybe (RE b)
floatOut (Let Name
m RE (Var a)
r RE (Var (Var a))
s) Var a -> Maybe b
un RE (Var (Var a)) -> RE (Var b)
mk
    | Just RE b
r' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Var a -> Maybe b
un RE (Var a)
r
    = forall a. a -> Maybe a
Just
    forall a b. (a -> b) -> a -> b
$ forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m RE b
r' forall a b. (a -> b) -> a -> b
$ RE (Var (Var a)) -> RE (Var b)
mk forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Var (Var a) -> Var (Var a)
swapVar RE (Var (Var a))
s
    | Bool
otherwise
    = forall a b.
(Eq a, Eq b) =>
RE (Var a)
-> (Var a -> Maybe b)
-> (RE (Var (Var a)) -> RE (Var b))
-> Maybe (RE b)
floatOut
        RE (Var (Var a))
s
        (forall r a. r -> (a -> r) -> Var a -> r
unvar forall a. Maybe a
Nothing Var a -> Maybe b
un)
        (RE (Var (Var a)) -> RE (Var b)
mk forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Var a
F) RE (Var a)
r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Var (Var a) -> Var (Var a)
swapVar))
floatOut RE (Var a)
_ Var a -> Maybe b
_ RE (Var (Var a)) -> RE (Var b)
_ = forall a. Maybe a
Nothing

let' :: Eq a => Name -> RE a -> RE (Var a) -> RE a
let' :: forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
n (Let Name
m RE a
x RE (Var a)
r) RE (Var a)
s
    = forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m RE a
x
    forall a b. (a -> b) -> a -> b
$ forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
n RE (Var a)
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall r a. r -> (a -> r) -> Var a -> r
unvar forall a. Var a
B (forall a. a -> Var a
F forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Var a
F)) RE (Var a)
s)
let' Name
n RE a
r RE (Var a)
s = forall a. Name -> RE a -> RE (Var a) -> RE a
postlet' Name
n RE a
r (forall b. Eq b => b -> RE b -> RE b -> RE b
go forall a. Var a
B (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Var a
F RE a
r) RE (Var a)
s) where
    -- This simple CSE only looks for lets. i.e
    --
    --     let x = a; y = a in ...body x y...
    --     -- >
    --     let x = a in ...body x x...
    --
    -- 'consCase' introduces same lets, so this fires a lot.
    --
    -- Note: not using let' or fix' in the bodies
    -- makes this faster.
    go :: Eq b => b -> RE b -> RE b -> RE b
    go :: forall b. Eq b => b -> RE b -> RE b -> RE b
go b
v RE b
x (Let Name
m RE b
a RE (Var b)
b)
        | RE b
x forall a. Eq a => a -> a -> Bool
== RE b
a    = forall b. Eq b => b -> RE b -> RE b -> RE b
go b
v RE b
x (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall r a. r -> (a -> r) -> Var a -> r
unvar b
v forall a. a -> a
id) RE (Var b)
b)
        | Bool
otherwise = forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
m (forall b. Eq b => b -> RE b -> RE b -> RE b
go b
v RE b
x RE b
a) (forall b. Eq b => b -> RE b -> RE b -> RE b
go (forall a. a -> Var a
F b
v) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Var a
F RE b
x) RE (Var b)
b)
    go b
v RE b
x (Fix Name
m RE (Var b)
a) = forall a. Name -> RE (Var a) -> RE a
Fix Name
m (forall b. Eq b => b -> RE b -> RE b -> RE b
go (forall a. a -> Var a
F b
v) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Var a
F RE b
x) RE (Var b)
a)

    go b
_ RE b
_ RE b
r' = RE b
r'

postlet' :: Name -> RE a -> RE (Var a) -> RE a
postlet' :: forall a. Name -> RE a -> RE (Var a) -> RE a
postlet' Name
_ RE a
r (Var Var a
B)                       = RE a
r
postlet' Name
_ RE a
_ RE (Var a)
s       | Just RE a
s' <- forall a. RE (Var a) -> Maybe (RE a)
unused RE (Var a)
s = RE a
s'
postlet' Name
n RE a
r RE (Var a)
s                             = forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
n RE a
r RE (Var a)
s

unused :: RE (Var a) -> Maybe (RE a)
unused :: forall a. RE (Var a) -> Maybe (RE a)
unused = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall r a. r -> (a -> r) -> Var a -> r
unvar forall a. Maybe a
Nothing forall a. a -> Maybe a
Just)