{-# LANGUAGE CPP               #-}
{-# LANGUAGE OverloadedStrings #-}
#ifndef RERE_NO_CFG
{-# LANGUAGE Trustworthy       #-}
#elif __GLASGOW_HASKELL__ >=704
{-# LANGUAGE Safe              #-}
#elif __GLASGOW_HASKELL__ >=702
{-# LANGUAGE Trustworthy       #-}
#endif
-- | Various examples of using @rere@,
-- as used [in the blog post](#).
module RERE.Examples where

import Control.Applicative (some, (<|>))
import Control.Monad       (void)
import Data.Void           (Void)

import qualified Text.Parsec        as P
import qualified Text.Parsec.String as P

import RERE

#ifndef RERE_NO_CFG
import Data.Vec.Lazy (Vec (..))

import qualified Data.Fin      as F
import qualified Data.Type.Nat as N
#endif

#ifdef RERE_INTERSECTION
import Data.Void (vacuous)
#endif

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((*>))
#endif

#if !MIN_VERSION_base(4,11,0)
import Data.Semigroup (Semigroup (..))
#endif

-- $setup
-- >>> import Test.QuickCheck.Random (mkQCGen)
-- >>> import Test.QuickCheck.Gen (unGen)
-- >>> import Control.Monad.ST (runST)
-- >>> import RERE
-- >>> let runGen seed = maybe "<<null>>" (\g' -> unGen g' (mkQCGen seed) 10)
-- >>> let showRef re = matchDebugR re ""

-------------------------------------------------------------------------------
-- * Syntax
-------------------------------------------------------------------------------

-- | Demonstrates how various constructors are pretty printed.
syntaxExamples :: IO ()
syntaxExamples :: IO ()
syntaxExamples = do
    RE Void -> IO ()
putLatex RE Void
forall a. RE a
Null
    RE Void -> IO ()
putLatex RE Void
forall a. RE a
Eps

    RE Void -> IO ()
putLatex (RE Void -> IO ()) -> RE Void -> IO ()
forall a b. (a -> b) -> a -> b
$ Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a'
    RE Void -> IO ()
putLatex (RE Void -> IO ()) -> RE Void -> IO ()
forall a b. (a -> b) -> a -> b
$ Char -> RE Void
forall a. Char -> RE a
ch_ Char
'b'

    RE Void -> IO ()
putLatex (RE Void -> IO ()) -> RE Void -> IO ()
forall a b. (a -> b) -> a -> b
$ Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" RE Void
forall a. RE a
Eps (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var Void) -> RE (Var (Var Void)) -> RE (Var Void)
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" RE (Var Void)
forall a. RE a
Eps (RE (Var (Var Void)) -> RE (Var Void))
-> RE (Var (Var Void)) -> RE (Var Void)
forall a b. (a -> b) -> a -> b
$ RE (Var (Var Void)) -> RE (Var (Var Void)) -> RE (Var (Var Void))
forall a. RE a -> RE a -> RE a
App (Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var Var (Var Void)
forall a. Var a
B) (Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var (Var Void -> Var (Var Void)
forall a. a -> Var a
F Var Void
forall a. Var a
B))
    RE Void -> IO ()
putLatex (RE Void -> IO ()) -> RE Void -> IO ()
forall a b. (a -> b) -> a -> b
$ Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" RE Void
forall a. RE a
Eps (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var Void) -> RE (Var (Var Void)) -> RE (Var Void)
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" RE (Var Void)
forall a. RE a
Eps (RE (Var (Var Void)) -> RE (Var Void))
-> RE (Var (Var Void)) -> RE (Var Void)
forall a b. (a -> b) -> a -> b
$ RE (Var (Var Void)) -> RE (Var (Var Void)) -> RE (Var (Var Void))
forall a. RE a -> RE a -> RE a
Alt (Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var Var (Var Void)
forall a. Var a
B) (Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var (Var Void -> Var (Var Void)
forall a. a -> Var a
F Var Void
forall a. Var a
B))
    RE Void -> IO ()
putLatex (RE Void -> IO ()) -> RE Void -> IO ()
forall a b. (a -> b) -> a -> b
$ Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" RE Void
forall a. RE a
Eps (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ RE (Var Void) -> RE (Var Void)
forall a. RE a -> RE a
Star (Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B)

-------------------------------------------------------------------------------
-- * Example 1
-------------------------------------------------------------------------------

-- |
--
-- >>> match ex1 "abab"
-- True
--
-- >>> match ex1 "ababa"
-- False
--
-- >>> ex1
-- Star (App (Ch "a") (Ch "b"))
--
-- >>> charClasses ex1
-- fromList "\NULabc"
--
-- >>> showRef ex1
-- size: 4
-- show: Star (App (Ch "a") (Ch "b"))
-- null: True
--
-- >>> matchR ex1 "abab"
-- True
--
-- >>> matchR ex1 "ababa"
-- False
--
-- >>> runGen 43 (generate 10 20 ex1)
-- "abababababababababab"
--
-- >>> runGen 44 (generate 10 20 ex1)
-- "ababab"
--
ex1 :: RE Void
ex1 :: RE Void
ex1 = RE Void -> RE Void
forall a. RE a -> RE a
star_ (Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a' RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> Char -> RE Void
forall a. Char -> RE a
ch_ Char
'b')

ex1run1 :: IO ()
ex1run1 :: IO ()
ex1run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex1 String
"abab"

-------------------------------------------------------------------------------
-- * Example 2
-------------------------------------------------------------------------------

-- |
--
-- >>> match ex2 "aaa"
-- True
--
-- Note: how "sharing" is preserved.
--
-- >>> showRef ex2
-- size: 5
-- show: App (Star (Ch "a")) (Star (Ch "a"))
-- null: True
--
-- >> matchR ex2 "aaa"
-- True
--
-- >>> runGen 42 (generate 10 20 ex2)
-- "aaaaaa"
--
-- >>> runGen 44 (generate 10 20 ex2)
-- "aaaaaaaaaa"
--
ex2 :: RE Void
ex2 :: RE Void
ex2 = Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Name -> RE a -> RE (Var a) -> RE a
Let Name
"r" (RE Void -> RE Void
forall a. RE a -> RE a
star_ (Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a')) (Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B)

ex2run1 :: IO ()
ex2run1 :: IO ()
ex2run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex2 String
"aaa"

-------------------------------------------------------------------------------
-- * Example 3
-------------------------------------------------------------------------------

-- |
--
-- >>> match ex3 "abab"
-- True
--
-- >>> match ex3 "ababa"
-- False
--
-- >>> showRef ex3
-- size: 8
-- show: Ref 0 (Alt Eps (App (Ch "a") (App (Ch "b") (Ref 0 <<loop>>))))
-- null: True
--
-- >>> matchR ex3 "abab"
-- True
--
-- >>> matchR ex3 "ababa"
-- False
--
-- >>> runGen 43 (generate 10 20 ex3)
-- "abababab"
--
-- >>> runGen 44 (generate 10 20 ex3)
-- "abab"
--
ex3 :: RE Void
ex3 :: RE Void
ex3 = Name -> RE (Var Void) -> RE Void
forall a. Name -> RE (Var a) -> RE a
Fix Name
"x" (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'a' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'b' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B)

ex3run1 :: IO ()
ex3run1 :: IO ()
ex3run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex3 String
"abab"

-------------------------------------------------------------------------------
-- * Example 4
-------------------------------------------------------------------------------

-- |
--
-- >>> match ex4 "aaaabbbb"
-- True
--
-- >>> showRef ex4
-- size: 8
-- show: Ref 0 (Alt Eps (App (Ch "a") (App (Ref 0 <<loop>>) (Ch "b"))))
-- null: True
--
-- >>> matchR ex4 "aaaabbbb"
-- True
--
-- >>> runGen 43 (generate 10 20 ex4)
-- "ab"
--
-- >>> runGen 47 (generate 10 20 ex4)
-- "aaaabbbb"
--
ex4 :: RE Void
ex4 :: RE Void
ex4 = Name -> RE (Var Void) -> RE Void
forall a. Name -> RE (Var a) -> RE a
Fix Name
"x" (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'a' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'b')

ex4run1 :: IO ()
ex4run1 :: IO ()
ex4run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex4 String
"aaaabbbb"

-------------------------------------------------------------------------------
-- * Example 5
-------------------------------------------------------------------------------

-- |
--
-- >>> match ex5 "abab"
-- True
--
-- >>> match ex5 "ababa"
-- False
--
-- >>> showRef ex5
-- size: 8
-- show: Ref 0 (Alt Eps (App (Ref 0 <<loop>>) (App (Ch "a") (Ch "b"))))
-- null: True
--
-- >>> matchR ex5 "abab"
-- True
--
-- >>> matchR ex5 "ababa"
-- False
--
-- >>> runGen 43 (generate 10 20 ex5)
-- "ab"
--
-- >>> runGen 51 (generate 10 20 ex5)
-- "abab"
--
ex5 :: RE Void
ex5 :: RE Void
ex5 = Name -> RE (Var Void) -> RE Void
forall a. Name -> RE (Var a) -> RE a
Fix Name
"x" (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'a' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'b')

ex5run1 :: IO ()
ex5run1 :: IO ()
ex5run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex5 String
"abab"

-------------------------------------------------------------------------------
-- * Example 6
-------------------------------------------------------------------------------

-- |
--
-- Using fix-point operator:
--
-- @
-- fix expr = "(" expr ")" | "1" | "2" | ... | "9" | expr "+" expr | expr "*" expr
-- @
--
-- which in BNF is almost he same
--
-- @
-- expr ::= "(" expr ")" | "1" | "2" | ... | "9" | expr "+" expr | expr "*" expr
-- @
--
-- >>> matchR ex6 "(1+2)*3"
-- True
--
-- >>> runGen 43 (generate 5 5 ex6)
-- "74501+(534*19450)*(99050)"
--
ex6 :: RE Void
ex6 :: RE Void
ex6 = Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"d" (CharSet -> RE Void
forall a. CharSet -> RE a
Ch CharSet
"0123456789")
    (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var Void) -> RE (Var (Var Void)) -> RE (Var Void)
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"n" (Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> RE (Var Void) -> RE (Var Void)
forall a. RE a -> RE a
star_ (Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B))
    (RE (Var (Var Void)) -> RE (Var Void))
-> RE (Var (Var Void)) -> RE (Var Void)
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var (Var (Var Void))) -> RE (Var (Var Void))
forall a. Ord a => Name -> RE (Var a) -> RE a
fix_ Name
"e"
    (RE (Var (Var (Var Void))) -> RE (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var Void))
forall a b. (a -> b) -> a -> b
$  Char -> RE (Var (Var (Var Void)))
forall a. Char -> RE a
ch_ Char
'(' RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var Var (Var (Var Void))
forall a. Var a
B RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var (Var (Var Void)))
forall a. Char -> RE a
ch_ Char
')'
    RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Ord a => RE a -> RE a -> RE a
\/ Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var (Var (Var Void) -> Var (Var (Var Void))
forall a. a -> Var a
F Var (Var Void)
forall a. Var a
B)
    RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Ord a => RE a -> RE a -> RE a
\/ Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var Var (Var (Var Void))
forall a. Var a
B RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var (Var (Var Void)))
forall a. Char -> RE a
ch_ Char
'+' RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var Var (Var (Var Void))
forall a. Var a
B
    RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Ord a => RE a -> RE a -> RE a
\/ Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var Var (Var (Var Void))
forall a. Var a
B RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var (Var (Var Void)))
forall a. Char -> RE a
ch_ Char
'*' RE (Var (Var (Var Void)))
-> RE (Var (Var (Var Void))) -> RE (Var (Var (Var Void)))
forall a. Semigroup a => a -> a -> a
<> Var (Var (Var Void)) -> RE (Var (Var (Var Void)))
forall a. a -> RE a
Var Var (Var (Var Void))
forall a. Var a
B

--
-- (displayTraced . traced) is "match" function, which
-- also prints the trace of execution.
--
-- True
ex6run1 :: IO ()
ex6run1 :: IO ()
ex6run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex6 String
"1*(20+3)"

-------------------------------------------------------------------------------
-- * Example 7
-------------------------------------------------------------------------------

#ifndef RERE_NO_CFG
exCfg :: Ord a => CFG N.Nat5 a
exCfg :: forall a. Ord a => CFG Nat5 a
exCfg =
    RE (Either (Fin Nat5) a)
forall a. RE a
digit RE (Either (Fin Nat5) a)
-> Vec Nat4 (RE (Either (Fin Nat5) a))
-> Vec Nat5 (RE (Either (Fin Nat5) a))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: RE (Either (Fin Nat5) a)
digits RE (Either (Fin Nat5) a)
-> Vec Nat3 (RE (Either (Fin Nat5) a))
-> Vec Nat4 (RE (Either (Fin Nat5) a))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: RE (Either (Fin Nat5) a)
term RE (Either (Fin Nat5) a)
-> Vec Nat2 (RE (Either (Fin Nat5) a))
-> Vec Nat3 (RE (Either (Fin Nat5) a))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: RE (Either (Fin Nat5) a)
mult RE (Either (Fin Nat5) a)
-> Vec Nat1 (RE (Either (Fin Nat5) a))
-> Vec Nat2 (RE (Either (Fin Nat5) a))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: RE (Either (Fin Nat5) a)
expr RE (Either (Fin Nat5) a)
-> Vec Nat0 (RE (Either (Fin Nat5) a))
-> Vec Nat1 (RE (Either (Fin Nat5) a))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (RE (Either (Fin Nat5) a))
forall a. Vec Nat0 a
VNil
  where
    expr :: RE (Either (Fin Nat5) a)
expr = RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. RE a -> RE a -> RE a
Alt (RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
multV RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Either (Fin Nat5) a)
forall a. Char -> RE a
ch_ Char
'*' RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
exprV) RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
multV
    mult :: RE (Either (Fin Nat5) a)
mult = RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. RE a -> RE a -> RE a
Alt (RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
termV RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Either (Fin Nat5) a)
forall a. Char -> RE a
ch_ Char
'+' RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
multV) RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
termV
    term :: RE (Either (Fin Nat5) a)
term = RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. RE a -> RE a -> RE a
Alt RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
digitsV (Char -> RE (Either (Fin Nat5) a)
forall a. Char -> RE a
ch_ Char
'(' RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
exprV RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Either (Fin Nat5) a)
forall a. Char -> RE a
ch_ Char
')')

    digit :: RE a
digit = CharSet -> RE a
forall a. CharSet -> RE a
Ch CharSet
"0123456789"
    digits :: RE (Either (Fin Nat5) a)
digits = RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
digitV RE (Either (Fin Nat5) a)
-> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. Semigroup a => a -> a -> a
<> RE (Either (Fin Nat5) a) -> RE (Either (Fin Nat5) a)
forall a. RE a -> RE a
star_ RE (Either (Fin Nat5) a)
forall a. CFGBase Nat5 a
digitV

    digitV, digitsV, exprV, multV, termV :: CFGBase N.Nat5 a
    exprV :: forall a. CFGBase Nat5 a
exprV   = Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a. a -> RE a
Var (Either (Fin Nat5) a -> RE (Either (Fin Nat5) a))
-> Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a b. (a -> b) -> a -> b
$ Fin Nat5 -> Either (Fin Nat5) a
forall a b. a -> Either a b
Left Fin Nat5
Fin (Plus Nat4 Nat1)
forall (n :: Nat). Fin (Plus Nat4 ('S n))
F.fin4
    multV :: forall a. CFGBase Nat5 a
multV   = Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a. a -> RE a
Var (Either (Fin Nat5) a -> RE (Either (Fin Nat5) a))
-> Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a b. (a -> b) -> a -> b
$ Fin Nat5 -> Either (Fin Nat5) a
forall a b. a -> Either a b
Left Fin Nat5
Fin (Plus Nat3 Nat2)
forall (n :: Nat). Fin (Plus Nat3 ('S n))
F.fin3
    termV :: forall a. CFGBase Nat5 a
termV   = Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a. a -> RE a
Var (Either (Fin Nat5) a -> RE (Either (Fin Nat5) a))
-> Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a b. (a -> b) -> a -> b
$ Fin Nat5 -> Either (Fin Nat5) a
forall a b. a -> Either a b
Left Fin Nat5
Fin (Plus Nat2 Nat3)
forall (n :: Nat). Fin (Plus Nat2 ('S n))
F.fin2
    digitsV :: forall a. CFGBase Nat5 a
digitsV = Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a. a -> RE a
Var (Either (Fin Nat5) a -> RE (Either (Fin Nat5) a))
-> Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a b. (a -> b) -> a -> b
$ Fin Nat5 -> Either (Fin Nat5) a
forall a b. a -> Either a b
Left Fin Nat5
Fin (Plus Nat1 Nat4)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
F.fin1
    digitV :: forall a. CFGBase Nat5 a
digitV  = Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a. a -> RE a
Var (Either (Fin Nat5) a -> RE (Either (Fin Nat5) a))
-> Either (Fin Nat5) a -> RE (Either (Fin Nat5) a)
forall a b. (a -> b) -> a -> b
$ Fin Nat5 -> Either (Fin Nat5) a
forall a b. a -> Either a b
Left Fin Nat5
Fin (Plus Nat0 Nat5)
forall (n :: Nat). Fin (Plus Nat0 ('S n))
F.fin0

exCfgN :: Vec N.Nat5 Name
exCfgN :: Vec Nat5 Name
exCfgN = Name
"digit" Name -> Vec Nat4 Name -> Vec Nat5 Name
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Name
"digits" Name -> Vec Nat3 Name -> Vec Nat4 Name
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Name
"term" Name -> Vec Nat2 Name -> Vec Nat3 Name
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Name
"mult" Name -> Vec Nat1 Name -> Vec Nat2 Name
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Name
"expr" Name -> Vec Nat0 Name -> Vec Nat1 Name
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 Name
forall a. Vec Nat0 a
VNil

-- |
--
-- >>> matchR ex7 "12"
-- True
--
-- >>> matchR ex7 "(1+2)*3"
-- True
--
-- >>> charClasses ex7
-- fromList "\NUL()*+,0:"
--
-- >>> runGen 43 (generate 5 5 ex7)
-- "(3431*((0337+5+070346+4))+76848+((4126+350875)*98769+308194+270+03118)+888*(95+90904)+(301069+7+715835)+2809)"
--
ex7 :: Ord a => RE a
ex7 :: forall a. Ord a => RE a
ex7 = Vec Nat5 Name -> CFG Nat5 a -> RE a
forall (n :: Nat) a.
(SNatI n, Ord a) =>
Vec ('S n) Name -> CFG ('S n) a -> RE a
cfgToRE Vec Nat5 Name
exCfgN CFG Nat5 a
forall a. Ord a => CFG Nat5 a
exCfg

-- ex7 :: RE Void
-- ex7 = Let "digit" (Ch '0' \/ Ch '1' \/ Ch '2' \/ Ch '3')
--     $ Let "digits" (Var B <> star (Var B))
--     $ Fix "expr"
--     $ Let "term" (Var (F B) \/ Ch '(' <> Var B <> Ch ')')
--     $ Let "mult" (Fix "mult" $ Var (F B) <> Ch '+' <> Var B \/ Var (F B))
--     $ Var B <> Ch '*' <> Var (F B) \/ Var B

ex7run1 :: IO ()
ex7run1 :: IO ()
ex7run1 = String -> IO ()
ex7run String
"1*(20+3)"

ex7run :: String -> IO ()
ex7run :: String -> IO ()
ex7run String
str = RE Void -> String -> IO ()
putLatexTrace RE Void
forall a. Ord a => RE a
ex7 String
str
#endif

ex7parsec :: P.Parser ()
ex7parsec :: Parser ()
ex7parsec = Parser ()
forall {u}. ParsecT String u Identity ()
expr where
    expr :: ParsecT String u Identity ()
expr   = ParsecT String u Identity () -> ParsecT String u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT String u Identity () -> ParsecT String u Identity ())
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a b. (a -> b) -> a -> b
$ ParsecT String u Identity () -> ParsecT String u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
P.try (ParsecT String u Identity ()
mult ParsecT String u Identity ()
-> ParsecT String u Identity Char -> ParsecT String u Identity Char
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'*' ParsecT String u Identity Char
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String u Identity ()
expr) ParsecT String u Identity ()
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a.
ParsecT String u Identity a
-> ParsecT String u Identity a -> ParsecT String u Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT String u Identity ()
mult
    mult :: ParsecT String u Identity ()
mult   = ParsecT String u Identity () -> ParsecT String u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT String u Identity () -> ParsecT String u Identity ())
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a b. (a -> b) -> a -> b
$ ParsecT String u Identity () -> ParsecT String u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
P.try (ParsecT String u Identity ()
term ParsecT String u Identity ()
-> ParsecT String u Identity Char -> ParsecT String u Identity Char
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'+' ParsecT String u Identity Char
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String u Identity ()
mult) ParsecT String u Identity ()
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a.
ParsecT String u Identity a
-> ParsecT String u Identity a -> ParsecT String u Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT String u Identity ()
term
    term :: ParsecT String u Identity ()
term   = ParsecT String u Identity () -> ParsecT String u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
P.try ParsecT String u Identity ()
forall {u}. ParsecT String u Identity ()
digits ParsecT String u Identity ()
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a.
ParsecT String u Identity a
-> ParsecT String u Identity a -> ParsecT String u Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT String u Identity Char -> ParsecT String u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
'(' ParsecT String u Identity Char
-> ParsecT String u Identity () -> ParsecT String u Identity ()
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String u Identity ()
expr ParsecT String u Identity ()
-> ParsecT String u Identity Char -> ParsecT String u Identity Char
forall a b.
ParsecT String u Identity a
-> ParsecT String u Identity b -> ParsecT String u Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
P.char Char
')')
    digits :: ParsecT String u Identity ()
digits = ParsecT String u Identity String -> ParsecT String u Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT String u Identity String -> ParsecT String u Identity ())
-> ParsecT String u Identity String -> ParsecT String u Identity ()
forall a b. (a -> b) -> a -> b
$ ParsecT String u Identity Char -> ParsecT String u Identity String
forall a.
ParsecT String u Identity a -> ParsecT String u Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT String u Identity Char
forall {u}. ParsecT String u Identity Char
digit
    digit :: ParsecT String u Identity Char
digit  = (Char -> Bool) -> ParsecT String u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
P.satisfy (\Char
c -> Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
>= Char
'0' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9')

ex7parsecRun :: IO ()
ex7parsecRun :: IO ()
ex7parsecRun = Parser () -> String -> IO ()
forall s t a.
(Stream s Identity t, Show a) =>
Parsec s () a -> s -> IO ()
P.parseTest Parser ()
ex7parsec String
"1*(20+3)"

-------------------------------------------------------------------------------
-- * Example 8
-------------------------------------------------------------------------------

#ifdef RERE_INTERSECTION
xnyn :: Name -> Char -> Char -> RE Void
xnyn :: Name -> Char -> Char -> RE Void
xnyn Name
n Char
x Char
y = Name -> RE (Var Void) -> RE Void
forall a. Name -> RE (Var a) -> RE a
Fix Name
n (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
x RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
y)

ambncn :: RE Void
ambncn :: RE Void
ambncn = RE Void -> RE Void
forall a. RE a -> RE a
star_ (Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a') RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> Name -> Char -> Char -> RE Void
xnyn Name
"bc" Char
'b' Char
'c'

anbncm :: RE Void
anbncm :: RE Void
anbncm = Name -> Char -> Char -> RE Void
xnyn Name
"ab" Char
'a' Char
'b' RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> RE Void -> RE Void
forall a. RE a -> RE a
star_ (Char -> RE Void
forall a. Char -> RE a
ch_ Char
'c')

-- |
--
-- >>> match ex8 "aabbcc"
-- True
--
-- >>> match ex8 "aabbccc"
-- False
--
-- >> matchR ex8 "aabbcc"
-- True
--
-- >> matchR ex8 "aabbccc"
-- False
--
-- >>> runGen 42 (generate 10 20 ex8)
-- "<<null>>"
--
ex8 :: RE Void
ex8 :: RE Void
ex8 = RE Void
ambncn RE Void -> RE Void -> RE Void
forall a. Ord a => RE a -> RE a -> RE a
/\ RE Void
anbncm

ex8run1 :: IO ()
ex8run1 :: IO ()
ex8run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex8 String
"aaabbbccc"

-- |
--
-- >> matchR ex8b "aabbccaaabbbccc"
-- True
ex8b :: RE Void
ex8b :: RE Void
ex8b = Name -> RE (Var Void) -> RE Void
forall a. Name -> RE (Var a) -> RE a
Fix Name
"abc" (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ RE Void -> RE (Var Void)
forall (f :: * -> *) a. Functor f => f Void -> f a
vacuous RE Void
ex8 RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B)

ex8run2 :: IO ()
ex8run2 :: IO ()
ex8run2 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex8b String
"aabbccaabbcc"

#endif

-------------------------------------------------------------------------------
-- * Example 9
-------------------------------------------------------------------------------

#ifdef RERE_INTERSECTION

evenRE :: RE Void
evenRE :: RE Void
evenRE = RE Void -> RE Void
forall a. RE a -> RE a
star_ (Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a' RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a')

oddRE :: RE Void
oddRE :: RE Void
oddRE = Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a' RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> RE Void
evenRE

evenRE' :: RE Void
evenRE' :: RE Void
evenRE' = Name -> RE (Var Void) -> RE Void
forall a. Ord a => Name -> RE (Var a) -> RE a
fix_ Name
"even" (RE (Var Void)
forall a. RE a
Eps RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Ord a => RE a -> RE a -> RE a
\/ Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'a' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Char -> RE (Var Void)
forall a. Char -> RE a
ch_ Char
'a' RE (Var Void) -> RE (Var Void) -> RE (Var Void)
forall a. Semigroup a => a -> a -> a
<> Var Void -> RE (Var Void)
forall a. a -> RE a
Var Var Void
forall a. Var a
B)

oddRE' :: RE Void
oddRE' :: RE Void
oddRE' = Char -> RE Void
forall a. Char -> RE a
ch_ Char
'a' RE Void -> RE Void -> RE Void
forall a. Semigroup a => a -> a -> a
<> RE Void
evenRE'

ex9 :: RE Void
ex9 :: RE Void
ex9 = Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"odd" RE Void
oddRE
    (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var Void) -> RE (Var (Var Void)) -> RE (Var Void)
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"even" ((Void -> Var Void) -> RE Void -> RE (Var Void)
forall a b. (a -> b) -> RE a -> RE b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> Var Void
forall a. a -> Var a
F RE Void
evenRE)
    (RE (Var (Var Void)) -> RE (Var Void))
-> RE (Var (Var Void)) -> RE (Var Void)
forall a b. (a -> b) -> a -> b
$ Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var Var (Var Void)
forall a. Var a
B RE (Var (Var Void)) -> RE (Var (Var Void)) -> RE (Var (Var Void))
forall a. Ord a => RE a -> RE a -> RE a
/\ Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var (Var Void -> Var (Var Void)
forall a. a -> Var a
F Var Void
forall a. Var a
B)

ex9run1 :: IO ()
ex9run1 :: IO ()
ex9run1 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex9 String
"aaa"

ex9b :: RE Void
ex9b :: RE Void
ex9b = Name -> RE Void -> RE (Var Void) -> RE Void
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"odd" RE Void
oddRE'
     (RE (Var Void) -> RE Void) -> RE (Var Void) -> RE Void
forall a b. (a -> b) -> a -> b
$ Name -> RE (Var Void) -> RE (Var (Var Void)) -> RE (Var Void)
forall a. Ord a => Name -> RE a -> RE (Var a) -> RE a
let_ Name
"even" ((Void -> Var Void) -> RE Void -> RE (Var Void)
forall a b. (a -> b) -> RE a -> RE b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> Var Void
forall a. a -> Var a
F RE Void
evenRE')
     (RE (Var (Var Void)) -> RE (Var Void))
-> RE (Var (Var Void)) -> RE (Var Void)
forall a b. (a -> b) -> a -> b
$ Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var Var (Var Void)
forall a. Var a
B RE (Var (Var Void)) -> RE (Var (Var Void)) -> RE (Var (Var Void))
forall a. Ord a => RE a -> RE a -> RE a
/\ Var (Var Void) -> RE (Var (Var Void))
forall a. a -> RE a
Var (Var Void -> Var (Var Void)
forall a. a -> Var a
F Var Void
forall a. Var a
B)

ex9run2 :: IO ()
ex9run2 :: IO ()
ex9run2 = RE Void -> String -> IO ()
putLatexTrace RE Void
ex9b String
"aaa"
#endif