{-# 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 :: Vec ('S n) Name -> CFG ('S n) a -> RE a
cfgToRE = CfgToRE n a -> Vec ('S n) Name -> CFG ('S n) a -> RE a
forall (n :: Nat) a.
CfgToRE n a -> Vec ('S n) Name -> CFG ('S n) a -> RE a
getCfgToRE (CfgToRE 'Z a
-> (forall (m :: Nat). SNatI m => CfgToRE m a -> CfgToRE ('S m) a)
-> CfgToRE n a
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
forall (m :: Nat). SNatI m => CfgToRE m a -> CfgToRE ('S m) a
step) where
    start :: CfgToRE 'Z a
start = (Vec ('S 'Z) Name -> CFG ('S 'Z) a -> RE a) -> CfgToRE 'Z a
forall (n :: Nat) a.
(Vec ('S n) Name -> CFG ('S n) a -> RE a) -> CfgToRE n a
CfgToRE Vec ('S 'Z) Name -> CFG ('S 'Z) a -> RE a
forall a. Ord a => Vec ('S 'Z) Name -> CFG ('S 'Z) a -> RE a
baseCase

    step :: Ord a => CfgToRE m a -> CfgToRE ('S m) a
    step :: CfgToRE m a -> CfgToRE ('S m) a
step (CfgToRE Vec ('S m) Name -> CFG ('S m) a -> RE a
rec) = (Vec ('S ('S m)) Name -> CFG ('S ('S m)) a -> RE a)
-> CfgToRE ('S m) a
forall (n :: Nat) a.
(Vec ('S n) Name -> CFG ('S n) a -> RE a) -> CfgToRE n a
CfgToRE ((Vec ('S ('S m)) Name -> CFG ('S ('S m)) a -> RE a)
 -> CfgToRE ('S m) a)
-> (Vec ('S ('S m)) Name -> CFG ('S ('S m)) a -> RE a)
-> CfgToRE ('S m) a
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 (Vec ('S ('S m)) Name -> Vec ('S m) Name
forall (n :: Nat) a. Vec ('S n) a -> Vec n a
V.tail Vec ('S ('S m)) Name
names) (Vec ('S ('S m)) Name -> CFG ('S ('S m)) a -> CFG ('S m) a
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 { 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 :: Vec ('S 'Z) Name -> CFG ('S 'Z) a -> RE a
baseCase (Name
name ::: Vec n1 Name
VNil) (CFGBase ('S 'Z) a
cfg ::: Vec n1 (CFGBase ('S 'Z) a)
VNil) =
    Name -> RE (Var a) -> RE a
forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
name ((Either (Fin ('S 'Z)) a -> Var a)
-> CFGBase ('S 'Z) a -> RE (Var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin ('S 'Z) -> Var a)
-> (a -> Var a) -> Either (Fin ('S 'Z)) a -> Var a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Fin ('S 'Z)
FZ -> Var a
forall a. Var a
B) a -> Var a
forall a. a -> Var a
F) CFGBase ('S 'Z) 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 :: 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) =
    (CFGBase ('S n) a -> RE (Either (Fin n) a))
-> Vec n1 (CFGBase ('S n) a) -> Vec n1 (RE (Either (Fin n) a))
forall a b (n :: Nat). (a -> b) -> Vec n a -> Vec n b
V.map (\CFGBase ('S n) a
g -> Name
-> RE (Either (Fin n) a)
-> RE (Var (Either (Fin n) a))
-> RE (Either (Fin n) a)
forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
name RE (Either (Fin n) a)
f' ((Either (Fin ('S n)) a -> Var (Either (Fin n) a))
-> CFGBase ('S n) a -> RE (Var (Either (Fin n) a))
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' :: RE (Either (Fin n) a)
f' = Name -> RE (Var (Either (Fin n) a)) -> RE (Either (Fin n) a)
forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
name ((Either (Fin ('S n)) a -> Var (Either (Fin n) a))
-> CFGBase ('S n) a -> RE (Var (Either (Fin n) a))
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)     = Either (Fin n) a -> Var (Either (Fin n) a)
forall a. a -> Var a
F (a -> Either (Fin n) a
forall a b. b -> Either a b
Right a
a)
    sub (Left (FS Fin n1
n)) = Either (Fin n1) a -> Var (Either (Fin n1) a)
forall a. a -> Var a
F (Fin n1 -> Either (Fin n1) a
forall a b. a -> Either a b
Left Fin n1
n)
    sub (Left Fin ('S n)
FZ)     = Var (Either (Fin n) a)
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)     = Either (Fin n) a -> Var (Either (Fin n) a)
forall a. a -> Var a
F (a -> Either (Fin n) a
forall a b. b -> Either a b
Right a
a)
    sub' (Left (FS Fin n1
n)) = Either (Fin n1) a -> Var (Either (Fin n1) a)
forall a. a -> Var a
F (Fin n1 -> Either (Fin n1) a
forall a b. a -> Either a b
Left Fin n1
n)
    sub' (Left Fin ('S n)
FZ)     = Var (Either (Fin n) a)
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' :: Name -> RE (Var a) -> RE a
fix' Name
n RE (Var a)
r
    | Just RE a
r' <- RE (Var a)
-> (Var a -> Maybe a)
-> (RE (Var (Var a)) -> RE (Var a))
-> Maybe (RE a)
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 (Maybe a -> (a -> Maybe a) -> Var a -> Maybe a
forall r a. r -> (a -> r) -> Var a -> r
unvar Maybe a
forall a. Maybe a
Nothing a -> Maybe a
forall a. a -> Maybe a
Just) (Name -> RE (Var (Var a)) -> RE (Var a)
forall a. Eq a => Name -> RE (Var a) -> RE a
fix' Name
n)
    = RE a
r'
    | Just RE a
r' <- (Var a -> Maybe a) -> RE (Var a) -> Maybe (RE a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Maybe a -> (a -> Maybe a) -> Var a -> Maybe a
forall r a. r -> (a -> r) -> Var a -> r
unvar Maybe a
forall a. Maybe a
Nothing a -> Maybe a
forall a. a -> Maybe a
Just) RE (Var a)
r
    = RE a
r'
fix' Name
n RE (Var a)
r = Name -> RE (Var a) -> RE a
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 :: 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' <- (Var a -> Maybe b) -> RE (Var a) -> Maybe (RE b)
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
    = RE b -> Maybe (RE b)
forall a. a -> Maybe a
Just
    (RE b -> Maybe (RE b)) -> RE b -> Maybe (RE b)
forall a b. (a -> b) -> a -> b
$ Name -> RE b -> RE (Var b) -> RE b
forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m RE b
r' (RE (Var b) -> RE b) -> RE (Var b) -> RE b
forall a b. (a -> b) -> a -> b
$ RE (Var (Var a)) -> RE (Var b)
mk (RE (Var (Var a)) -> RE (Var b)) -> RE (Var (Var a)) -> RE (Var b)
forall a b. (a -> b) -> a -> b
$ (Var (Var a) -> Var (Var a))
-> RE (Var (Var a)) -> RE (Var (Var a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var (Var a) -> Var (Var a)
forall a. Var (Var a) -> Var (Var a)
swapVar RE (Var (Var a))
s
    | Bool
otherwise
    = RE (Var (Var a))
-> (Var (Var a) -> Maybe b)
-> (RE (Var (Var (Var a))) -> RE (Var b))
-> Maybe (RE b)
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
        (Maybe b -> (Var a -> Maybe b) -> Var (Var a) -> Maybe b
forall r a. r -> (a -> r) -> Var a -> r
unvar Maybe b
forall a. Maybe a
Nothing Var a -> Maybe b
un)
        (RE (Var (Var a)) -> RE (Var b)
mk (RE (Var (Var a)) -> RE (Var b))
-> (RE (Var (Var (Var a))) -> RE (Var (Var a)))
-> RE (Var (Var (Var a)))
-> RE (Var b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> RE (Var (Var a)) -> RE (Var (Var (Var a))) -> RE (Var (Var a))
forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m ((Var a -> Var (Var a)) -> RE (Var a) -> RE (Var (Var a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> Var a) -> Var a -> Var (Var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var a
forall a. a -> Var a
F) RE (Var a)
r) (RE (Var (Var (Var a))) -> RE (Var (Var a)))
-> (RE (Var (Var (Var a))) -> RE (Var (Var (Var a))))
-> RE (Var (Var (Var a)))
-> RE (Var (Var a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Var (Var a)) -> Var (Var (Var a)))
-> RE (Var (Var (Var a))) -> RE (Var (Var (Var a)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Var (Var a) -> Var (Var a))
-> Var (Var (Var a)) -> Var (Var (Var a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var (Var a) -> Var (Var a)
forall a. Var (Var a) -> Var (Var a)
swapVar))
floatOut RE (Var a)
_ Var a -> Maybe b
_ RE (Var (Var a)) -> RE (Var b)
_ = Maybe (RE b)
forall a. Maybe a
Nothing

let' :: Eq a => Name -> RE a -> RE (Var a) -> RE a
let' :: 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
    = Name -> RE a -> RE (Var a) -> RE a
forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
m RE a
x
    (RE (Var a) -> RE a) -> RE (Var a) -> RE a
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var a) -> RE (Var (Var a)) -> RE (Var a)
forall a. Eq a => Name -> RE a -> RE (Var a) -> RE a
let' Name
n RE (Var a)
r ((Var a -> Var (Var a)) -> RE (Var a) -> RE (Var (Var a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var (Var a) -> (a -> Var (Var a)) -> Var a -> Var (Var a)
forall r a. r -> (a -> r) -> Var a -> r
unvar Var (Var a)
forall a. Var a
B (Var a -> Var (Var a)
forall a. a -> Var a
F (Var a -> Var (Var a)) -> (a -> Var a) -> a -> Var (Var a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Var a
forall a. a -> Var a
F)) RE (Var a)
s)
let' Name
n RE a
r RE (Var a)
s = Name -> RE a -> RE (Var a) -> RE a
forall a. Name -> RE a -> RE (Var a) -> RE a
postlet' Name
n RE a
r (Var a -> RE (Var a) -> RE (Var a) -> RE (Var a)
forall b. Eq b => b -> RE b -> RE b -> RE b
go Var a
forall a. Var a
B ((a -> Var a) -> RE a -> RE (Var a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Var a
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 :: 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 RE b -> RE b -> Bool
forall a. Eq a => a -> a -> Bool
== RE b
a    = b -> RE b -> RE b -> RE b
forall b. Eq b => b -> RE b -> RE b -> RE b
go b
v RE b
x ((Var b -> b) -> RE (Var b) -> RE b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> (b -> b) -> Var b -> b
forall r a. r -> (a -> r) -> Var a -> r
unvar b
v b -> b
forall a. a -> a
id) RE (Var b)
b)
        | Bool
otherwise = Name -> RE b -> RE (Var b) -> RE b
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
m (b -> RE b -> RE b -> RE b
forall b. Eq b => b -> RE b -> RE b -> RE b
go b
v RE b
x RE b
a) (Var b -> RE (Var b) -> RE (Var b) -> RE (Var b)
forall b. Eq b => b -> RE b -> RE b -> RE b
go (b -> Var b
forall a. a -> Var a
F b
v) ((b -> Var b) -> RE b -> RE (Var b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Var b
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) = Name -> RE (Var b) -> RE b
forall a. Name -> RE (Var a) -> RE a
Fix Name
m (Var b -> RE (Var b) -> RE (Var b) -> RE (Var b)
forall b. Eq b => b -> RE b -> RE b -> RE b
go (b -> Var b
forall a. a -> Var a
F b
v) ((b -> Var b) -> RE b -> RE (Var b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Var b
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' :: 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' <- RE (Var a) -> Maybe (RE a)
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                             = Name -> RE a -> RE (Var a) -> RE a
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 :: RE (Var a) -> Maybe (RE a)
unused = (Var a -> Maybe a) -> RE (Var a) -> Maybe (RE a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Maybe a -> (a -> Maybe a) -> Var a -> Maybe a
forall r a. r -> (a -> r) -> Var a -> r
unvar Maybe a
forall a. Maybe a
Nothing a -> Maybe a
forall a. a -> Maybe a
Just)