Adapted from a course by Thierry Coquand.
Tested with GHC 9.8.2.
module RegEx where
import Prelude hiding ( isInfinite )
data RegExp a = Empty
| Epsilon
| Symbol a
| Star (RegExp a)
| Plus (RegExp a) (RegExp a)
| Dot (RegExp a) (RegExp a)
isEmpty :: RegExp a -> Bool
Empty = True
isEmpty Plus e1 e2) = isEmpty e1 && isEmpty e2
isEmpty (Dot e1 e2) = isEmpty e1 || isEmpty e2
isEmpty (= False isEmpty _
hasEpsilon :: RegExp a -> Bool
Epsilon = True
hasEpsilon Star _) = True
hasEpsilon (Plus e1 e2) = hasEpsilon e1 || hasEpsilon e2
hasEpsilon (Dot e1 e2) = hasEpsilon e1 && hasEpsilon e2
hasEpsilon (= False hasEpsilon _
atMostEpsilon :: RegExp a -> Bool
Empty = True
atMostEpsilon Epsilon = True
atMostEpsilon Star e) = atMostEpsilon e
atMostEpsilon (Plus e1 e2) = atMostEpsilon e1 && atMostEpsilon e2
atMostEpsilon (Dot e1 e2) =
atMostEpsilon (|| isEmpty e2 || (atMostEpsilon e1 && atMostEpsilon e2)
isEmpty e1 = False atMostEpsilon _
isNotEmpty :: RegExp a -> Bool
= not . isEmpty
isNotEmpty
isInfinite :: RegExp a -> Bool
isInfinite (Star e) = not $ atMostEpsilon e
isInfinite (Plus e1 e2) = isInfinite e1 || isInfinite e2
isInfinite (Dot e1 e2) =
isInfinite e1 && isNotEmpty e2) || (isNotEmpty e1 && isInfinite e2)
(isInfinite _ = False
reDer :: Eq a => RegExp a -> a -> RegExp a
Symbol t) s = if t == s then Epsilon else Empty
reDer (Plus e1 e2) s = reDer e1 s `Plus` reDer e2 s
reDer (Star e) s = reDer e s `Dot` Star e
reDer (
Dot e1 e2) s =
reDer (if hasEpsilon e1
then (reDer e1 s `Dot` e2) `Plus` reDer e2 s
else reDer e1 s `Dot` e2
= Empty reDer _ _
reDerW :: Eq a => RegExp a -> [a] -> RegExp a
= e
reDerW e [] : xs) = reDer (reDerW e xs) x reDerW e (x
inRE :: Eq a => RegExp a -> [a] -> Bool
= hasEpsilon (reDerW e xs) inRE e xs
type RE = RegExp Char
-- 0 and 1.
_1 :: RE
_0,= Symbol '0'
_0 = Symbol '1'
_1
-- 00, 01, 10 and 11.
_11 :: RE
_00, _01, _10,= _0 `Dot` _0
_00 = _0 `Dot` _1
_01 = _1 `Dot` _0
_10 = _1 `Dot` _1
_11
-- O^* and 1^*.
_1s :: RE
_0s,= Star _0
_0s = Star _1
_1s
-- (0+1)^*.
universe :: RE
= Star (Plus _0 _1)
universe
-- (01)^* and (10)^*.
_1s0s :: RE
_0s1s,= Star (Dot _0 _1)
_0s1s = Star (Dot _1 _0) _1s0s
Alternating 0
’s and 1
’s:
(01)^* + (10)^* + 0(10)^* + 1(01)^*
.
re1 :: RE
= _0s1s `Plus` _1s0s `Plus` (_0 `Dot` _1s0s) `Plus` (_1 `Dot` _0s1s) re1
The set
{ x01y | x,y ∈ {0,1}^* }: (0 + 1)^*01(0 + 1)^*
.
re2 :: RE
= universe `Dot` _01 `Dot` universe re2
Strings over Σ = {0,1}
such that there are two
0
’s separated by a number of positions that is multiple of
2. Note that 0
is an allowable multiple of 2. (Exercise
2.3.4c). (0 + 1)^*0(01 + 10 + 11)^*0(0 + 1)^*
.
re3 :: RE
= universe
re3 `Dot` _0
`Dot` Star (_01 `Plus` _10 `Plus` _11)
`Dot` _0
`Dot` universe
Generated with pandoc 3.1.11.1 and pandoc.css running the following command:
$ pandoc -f markdown+lhs \
-s \
--highlight-style pygments \
--css pandoc.css \
-o RegEx.html \
RegEx.lhs