Safe Haskell	None
Language	Haskell2010

KleenePlugin.Matching

Description

Match RE on a list (and produce a Proof).

Synopsis

leading :: RE a -> [a]
data MatchingError b a
- = UnexpectedEnd (RE a) [a]
- | NonMatch (RE a) b [b] [Maybe a]
matches :: (Outputable a, Outputable b) => (a -> b -> Either c Bool) -> RE a -> [b] -> Either (MatchingError b a) (NonEmpty (Proof (Maybe c) b a))
(>>>=) :: NonEmpty a -> (a -> Either e (NonEmpty b)) -> Either e (NonEmpty b)
(<&&>) :: (Functor f, Functor g) => f (g a) -> (a -> b) -> f (g b)
nullable :: RE a -> Maybe (Proof (Maybe c) b a)
derivate :: forall a b c. (Outputable a, Outputable b) => (a -> b -> Either c Bool) -> b -> RE a -> [(RE a, Proof (Maybe c) b a -> Proof (Maybe c) b a)]
exists :: RE a -> (Proof (Maybe c) b a -> Proof (Maybe c) b a) -> (RE a, Proof (Maybe c) b a -> Proof (Maybe c) b a)
appendLemma :: (Outputable a, Outputable b) => b -> RE a -> (Proof (Maybe c) b a -> Proof (Maybe c) b a) -> Proof (Maybe c) b a -> Proof (Maybe c) b a
starLemma :: (Outputable a, Outputable b) => b -> RE a -> (Proof (Maybe c) b a -> Proof (Maybe c) b a) -> Proof (Maybe c) b a -> Proof (Maybe c) b a

Documentation

Constructors

UnexpectedEnd (RE a) [a]
NonMatch (RE a) b [b] [Maybe a]

Arguments

:: (Outputable a, Outputable b)
=> (a -> b -> Either c Bool)	`a,b`-equality
-> RE a	regular expression
-> [b]	string
-> Either (MatchingError b a) (NonEmpty (Proof (Maybe c) b a))

Return a list of match-proofs of re to cs.

matches : (re : Re) → (cs : List *) → List (Proof re cs)

Note: not fmap join $ traverse f xs

(<&&>) :: (Functor f, Functor g) => f (g a) -> (a -> b) -> f (g b) infixl 1 Source #

nullable : (re : Re) → Maybe (Proof re [])

Arguments

:: (Outputable a, Outputable b)
=> (a -> b -> Either c Bool)	atom decidable equality
-> b	atom
-> RE a	regular expression
-> [(RE a, Proof (Maybe c) b a -> Proof (Maybe c) b a)]	result

derivate
  : (c : *) → (re : Re)
  → List (Σ Re λ re′ → (cs : List *) → Proof re′ cs → Proof re (c ∷ cs))

exists :: RE a -> (Proof (Maybe c) b a -> Proof (Maybe c) b a) -> (RE a, Proof (Maybe c) b a -> Proof (Maybe c) b a) Source #

Arguments

:: (Outputable a, Outputable b)
=> b	(c : *)
-> RE a	(r : RE)
-> (Proof (Maybe c) b a -> Proof (Maybe c) b a)	((cs′ : List *) → Proof r′ cs′ → Proof r (c ∷ cs′))
-> Proof (Maybe c) b a	Proof (r′ ∙ s) cs
-> Proof (Maybe c) b a	Proof (r ∙ s) (c ∷ cs)

Append Lemma for implementation of derivate.

append-lemma {c} {r} {cs} f r′s =
  let pair r′ s = r′s
  in pair (f r′) s

Note: As we don't have left rules in Proof, r′s must be ProofA.

Arguments

:: (Outputable a, Outputable b)
=> b	(c : *)
-> RE a	(r : RE)
-> (Proof (Maybe c) b a -> Proof (Maybe c) b a)	((cs′ : List *) → Proof r′ cs′ → Proof r (c ∷ cs′))
-> Proof (Maybe c) b a	Proof (r′ ∙ S r) cs
-> Proof (Maybe c) b a	Proof (S r) (c ∷ cs)

Like appendLemma but for kleene star.