kleene-type-0

Safe HaskellNone
LanguageHaskell2010

KleenePlugin.Types

Synopsis

Documentation

data RE a Source #

Regular expression.

This is a copy of Kleene.Type.RE type in Kleene.Type.

Constructors

E

empty string

V a

variable

(RE a) :<> (RE a)

append

(RE a) :\/ (RE a)

alternative

S (RE a)

star

T

top | Z -- ^ zero

Instances
Functor RE Source # 
Instance details

Defined in KleenePlugin.Types

Methods

fmap :: (a -> b) -> RE a -> RE b #

(<$) :: a -> RE b -> RE a #

Data a => Data (RE a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RE a -> c (RE a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (RE a) #

toConstr :: RE a -> Constr #

dataTypeOf :: RE a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (RE a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RE a)) #

gmapT :: (forall b. Data b => b -> b) -> RE a -> RE a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RE a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RE a -> r #

gmapQ :: (forall d. Data d => d -> u) -> RE a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RE a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RE a -> m (RE a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RE a -> m (RE a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RE a -> m (RE a) #

Show a => Show (RE a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

showsPrec :: Int -> RE a -> ShowS #

show :: RE a -> String #

showList :: [RE a] -> ShowS #

Outputable a => Outputable (RE a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

ppr :: RE a -> SDoc #

pprPrec :: Rational -> RE a -> SDoc #

simplifyRE :: RE a -> RE a Source #

Simplify RE structure.

This is useful when pretty printing RE. "Real" use would need to produce a transformation proof (Proof cannot express that).

data Proof c b a Source #

A Proof that regular expression matches.

Constructors

ProofE
top      : Proof E []
ProofV c b a
x        : Proof (V a) [a]
ProofA (RE a) (RE a) [b] [b] (Proof c b a) (Proof c b a)
pair p q : Proof a xs -> Proof b ys -> Proof (a <> b) (xs ++ ys)
ProofL (RE a) (RE a) [b] (Proof c b a)
inl p    : Proof a xs -> Proof (a \/ b) xs
ProofR (RE a) (RE a) [b] (Proof c b a)
inr q    : Proof b xs -> Proof (a \/ b) xs
ProofN (RE a)
nil      : Proof (S re) []
ProofC (RE a) [b] [b] (Proof c b a) (Proof c b a)
cons p q : Proof a xs -> Proof (S a) ys -> Proof (S a) (xs ++ ys)
ProofT [b]
top      : Proof T xs
Instances
Functor (Proof c b) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

fmap :: (a -> b0) -> Proof c b a -> Proof c b b0 #

(<$) :: a -> Proof c b b0 -> Proof c b a #

(Data c, Data b, Data a) => Data (Proof c b a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

gfoldl :: (forall d b0. Data d => c0 (d -> b0) -> d -> c0 b0) -> (forall g. g -> c0 g) -> Proof c b a -> c0 (Proof c b a) #

gunfold :: (forall b0 r. Data b0 => c0 (b0 -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (Proof c b a) #

toConstr :: Proof c b a -> Constr #

dataTypeOf :: Proof c b a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (Proof c b a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (Proof c b a)) #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Proof c b a -> Proof c b a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proof c b a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proof c b a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Proof c b a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proof c b a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proof c b a -> m (Proof c b a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proof c b a -> m (Proof c b a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proof c b a -> m (Proof c b a) #

(Show c, Show b, Show a) => Show (Proof c b a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

showsPrec :: Int -> Proof c b a -> ShowS #

show :: Proof c b a -> String #

showList :: [Proof c b a] -> ShowS #

(Outputable a, Outputable b) => Outputable (Proof c b a) Source # 
Instance details

Defined in KleenePlugin.Types

Methods

ppr :: Proof c b a -> SDoc #

pprPrec :: Rational -> Proof c b a -> SDoc #

proofStr :: Proof c b a -> [b] Source #

What string the Proof matches. It's enough to look at the top level.

proofTy :: Proof c b a -> RE a Source #

What regex the Proof executes. It's enough to look at the top level.

traverseProofC :: Applicative f => (a -> b -> c -> f c') -> Proof c b a -> f (Proof c' b a) Source #