kleene-type-0

Safe HaskellNone
LanguageHaskell2010

KleenePlugin.Matching

Description

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

Synopsis

Documentation

leading :: RE a -> [a] Source #

data MatchingError b a Source #

Constructors

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

matches Source #

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)

(>>>=) :: NonEmpty a -> (a -> Either e (NonEmpty b)) -> Either e (NonEmpty b) infixl 1 Source #

Note: not fmap join $ traverse f xs

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

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

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

derivate Source #

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 #

appendLemma 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.

starLemma 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 r) cs
-> Proof (Maybe c) b a
Proof (S r) (c ∷ cs)

Like appendLemma but for kleene star.