Brzozowski derivatives in PureScript - MIT License

00Pattern.purs

module Patterns
  ( Pattern(..)
  , unite
  , concat
  , repeat
  , complement
  , derivative
  ) where

import Data.Boolean (otherwise)
import Data.BooleanAlgebra (class BooleanAlgebra, class HeytingAlgebra, (&&), (||), not)
import Data.Eq (class Eq, (==))
import Data.KleeneAlgebra (class KleeneAlgebra, class StarSemiring)
import Data.Lattice (class BoundedJoinSemilattice, class BoundedLattice, class BoundedMeetSemilattice, class JoinSemilattice, class Lattice, class MeetSemilattice)
import Data.Monoid (class Monoid, class Semigroup, (<>))
import Data.PartialOrd (class LowerBounded, class PartialOrd, class UpperBounded, comparableDefault)
import Data.Semiring (class Semiring)
import Data.Show (class Show, show)

data Pattern a
  = Null
  | All
  | Empty
  | Chr a
  | Any
  -- | Set (Array a)
  | Not (Pattern a)
  | Seq (Pattern a) (Pattern a)
  | Alt (Pattern a) (Pattern a)
  | Mut (Pattern a) (Pattern a)
  | Rep (Pattern a)

derive instance eqPattern :: Eq a => Eq (Pattern a)
instance partialOrdPattern :: Eq a => PartialOrd (Pattern a) where
  comparable = comparableDefault
  leq Null _ = true
  leq _ Null = false
  leq All _ = false
  leq _ All = true
  -- TODO: partial ordering for patterns
  leq _ _ = false

instance lowerBoundedPattern :: Eq a => LowerBounded (Pattern a) where
  bottom = Null

instance upperBoundedPattern :: Eq a => UpperBounded (Pattern a) where
  top = All

instance semigroupPattern :: Semigroup (Pattern a) where
  append = concat

instance monoidPattern :: Monoid (Pattern a) where
  mempty = Empty

instance semiringPattern :: Eq a => Semiring (Pattern a) where
  add = unite
  zero = Null
  mul = concat
  one = Empty

instance starSemiringPattern :: Eq a => StarSemiring (Pattern a) where
  star = repeat

instance joinSemilatticePattern :: Eq a => JoinSemilattice (Pattern a) where
  join = unite

instance meetSemilatticePattern :: Eq a => MeetSemilattice (Pattern a) where
  meet = intersect

instance latticePattern :: Eq a => Lattice (Pattern a)

instance boundedJoinSemilatticePattern ::
  Eq a =>
  BoundedJoinSemilattice (Pattern a)

instance boundedMeetSemilatticePattern ::
  Eq a =>
  BoundedMeetSemilattice (Pattern a)

instance boundedLatticePattern :: Eq a => BoundedLattice (Pattern a)

instance heytingAlgebraPattern :: Eq a => HeytingAlgebra (Pattern a) where
  ff = Null
  tt = Empty
  implies a b = (complement a) || b
  conj = intersect
  disj = unite
  not = complement

instance booleanAlgebraPattern :: Eq a => BooleanAlgebra (Pattern a)
instance kleeneAlgebraPattern :: Eq a => KleeneAlgebra (Pattern a)

instance showPattern :: Show a => Show (Pattern a) where
  show Null = "Null"
  show All = "All"
  show Empty = "Empty"
  show (Chr c) = show c
  show Any = "Any"
  show (Seq r s) = "(" <> (show r) <> " <> " <> (show s) <> ")"
  show (Alt r s) = "(" <> (show r) <> " || " <> (show s) <> ")"
  show (Mut r s) = "(" <> (show r) <> " && " <> (show s) <> ")"
  show (Rep r) = show r <> "*"
  show (Not r) = "~" <> show r

complement :: forall a. Pattern a -> Pattern a
complement r@(Not _) = r
complement r = Not r

concat :: forall a. Pattern a -> Pattern a -> Pattern a
concat Null _ = Null
concat _ Null = Null
concat Empty r = r
concat r Empty = r
concat r s = Seq r s

unite :: forall a. Eq a => Pattern a -> Pattern a -> Pattern a
unite r s | r == s = r
unite Null r = r
unite r Null = r
unite All _ = All
unite _ All = All
-- unite (Chr x) (Chr y) = Set x `union` y
unite Empty r | nullable r = r
unite r Empty | nullable r = r
unite r s = Alt r s

intersect :: forall a. Eq a => Pattern a -> Pattern a -> Pattern a
intersect r s | r == s = r
intersect Null _ = Null
intersect _ Null = Null
intersect All r = r
intersect r All = r
-- intersect (Chr x) (Chr y) = Set x `intersection` y
intersect Empty r | nullable r = r
intersect r Empty | nullable r = r
intersect r s = Mut r s

repeat :: forall a. Pattern a -> Pattern a
repeat Null = Empty
repeat Empty = Empty
repeat All = All
repeat (Alt Empty Any) = All
repeat (Alt Any Empty) = All
repeat r@(Rep _) = r
repeat r = Rep r

nullable :: forall a. Pattern a -> Boolean
nullable Null = false
nullable All = true
nullable Empty = true
nullable (Chr _) = false
nullable Any = false
nullable (Not r) = not (nullable r)
nullable (Seq r s) = nullable r && nullable s
nullable (Alt r s) = nullable r || nullable s
nullable (Mut r s) = nullable r && nullable s
nullable (Rep _) = true

derivative :: forall a. Eq a => a -> Pattern a -> Pattern a
derivative _ Null = Null
derivative _ All = All
derivative _ Empty = Null
derivative c (Chr x)
  | c == x = Empty
  | otherwise = Null
derivative _ Any = Empty
derivative c (Not r) = complement (derivative c r)
derivative c (Seq r s)
  | nullable r = derivative c s || derivative c r <> s
  | otherwise = derivative c r <> s
derivative c (Alt r s) = derivative c r || derivative c s
derivative c (Mut r s) = derivative c r && derivative c s
derivative c r0@(Rep r) = derivative c r <> r0

01KleeneAlgebra.purs

module Data.KleeneAlgebra
  ( class KleeneAlgebra
  , class StarSemiring
  , star
  ) where

import Data.BooleanAlgebra (class BooleanAlgebra)
import Data.Lattice (class BoundedLattice)
import Data.Semiring (class Semiring)

class Semiring a <= StarSemiring a where
  star :: a -> a

class
  ( BooleanAlgebra a
  , BoundedLattice a
  , StarSemiring a
  ) <=
  KleeneAlgebra a

02Lattice.purs

module Data.Lattice
  ( (/\)
  , (\/)
  , class BoundedJoinSemilattice
  , class BoundedLattice
  , class BoundedMeetSemilattice
  , class JoinSemilattice
  , class Lattice
  , class MeetSemilattice
  , join
  , meet
  ) where

import Data.HeytingAlgebra (conj, disj)
import Data.Ordering (Ordering(..))
import Data.PartialOrd (class LowerBounded, class PartialOrd, class UpperBounded)
import Data.Unit (Unit, unit)

class
  ( BoundedJoinSemilattice a
  , BoundedMeetSemilattice a
  , Lattice a
  ) <=
  BoundedLattice a

class (JoinSemilattice a, LowerBounded a) <= BoundedJoinSemilattice a
class (MeetSemilattice a, UpperBounded a) <= BoundedMeetSemilattice a

class (JoinSemilattice a, MeetSemilattice a) <= Lattice a
class PartialOrd a <= JoinSemilattice a where
  join :: a -> a -> a

class PartialOrd a <= MeetSemilattice a where
  meet :: a -> a -> a

infixr 6 meet as /\
infixr 5 join as \/

instance boundedLatticeUnit :: BoundedLattice Unit
instance boundedJoinSemilatticeUnit :: BoundedJoinSemilattice Unit
instance boundedMeetSemilatticeUnit :: BoundedMeetSemilattice Unit

instance latticeUnit :: Lattice Unit
instance joinSemilatticeUnit :: JoinSemilattice Unit where
  join _ _ = unit

instance meetSemilatticeUnit :: MeetSemilattice Unit where
  meet _ _ = unit

instance boundedLatticeBoolean :: BoundedLattice Boolean
instance boundedJoinSemilatticeBoolean :: BoundedJoinSemilattice Boolean
instance boundedMeetSemilatticeBoolean :: BoundedMeetSemilattice Boolean

instance latticeBoolean :: Lattice Boolean
instance joinSemilatticeBoolean :: JoinSemilattice Boolean where
  join = disj

instance meetSemilatticeBoolean :: MeetSemilattice Boolean where
  meet = conj

instance boundedLatticeOrdering :: BoundedLattice Ordering
instance boundedJoinSemilatticeOrdering :: BoundedJoinSemilattice Ordering
instance boundedMeetSemilatticeOrdering :: BoundedMeetSemilattice Ordering

instance latticeOrdering :: Lattice Ordering
instance joinSemilatticeOrdering :: JoinSemilattice Ordering where
  join LT _ = LT
  join _ LT = LT
  join EQ EQ = EQ
  join _ _ = GT

instance meetSemilatticeOrdering :: MeetSemilattice Ordering where
  meet GT _ = GT
  meet _ GT = GT
  meet EQ EQ = EQ
  meet _ _ = LT

03PartialOrd.purs

module Data.PartialOrd
  ( class LowerBounded
  , class PartialOrd
  , class UpperBounded
  , bottom
  , comparable
  , comparableDefault
  , leq
  , partialOrdEq
  , top
  ) where

import Data.Eq (class Eq)
import Data.HeytingAlgebra ((&&), (||))
import Data.Ord (Ordering(..), lessThanOrEq)
import Data.Unit (Unit, unit)

class Eq a <= PartialOrd a where
  leq :: a -> a -> Boolean
  comparable :: a -> a -> Boolean

comparableDefault :: forall a. PartialOrd a => a -> a -> Boolean
comparableDefault x y = leq x y || leq y x

partialOrdEq :: forall a. PartialOrd a => a -> a -> Boolean
partialOrdEq x y = leq x y && leq y x

class PartialOrd a <= LowerBounded a where
  bottom :: a

class PartialOrd a <= UpperBounded a where
  top :: a

instance upperBoundedUnit :: UpperBounded Unit where
  top = unit

instance lowerBoundedUnit :: LowerBounded Unit where
  bottom = unit

instance partialOrdUnit :: PartialOrd Unit where
  leq _ _ = true
  comparable _ _ = true

instance upperBoundedBoolean :: UpperBounded Boolean where
  top = true

instance lowerBoundedBoolean :: LowerBounded Boolean where
  bottom = false

instance partialOrdBoolean :: PartialOrd Boolean where
  leq = lessThanOrEq
  comparable _ _ = true

instance upperBoundedOrdering :: UpperBounded Ordering where
  top = GT

instance lowerBoundedOrdering :: LowerBounded Ordering where
  bottom = LT

instance partialOrdOrdering :: PartialOrd Ordering where
  leq = lessThanOrEq
  comparable _ _ = true

foreign import topChar :: Char
foreign import bottomChar :: Char

instance upperBoundedChar :: UpperBounded Char where
  top = topChar

instance lowerBoundedChar :: LowerBounded Char where
  bottom = bottomChar

instance partialOrdChar :: PartialOrd Char where
  leq = lessThanOrEq
  comparable _ _ = true

foreign import topInt :: Int
foreign import bottomInt :: Int

instance upperBoundedInt :: UpperBounded Int where
  top = topInt

instance lowerBoundedInt :: LowerBounded Int where
  bottom = bottomInt

instance partialOrdInt :: PartialOrd Int where
  leq = lessThanOrEq
  comparable _ _ = true

foreign import topNumber :: Number
foreign import bottomNumber :: Number

instance upperBoundedNumber :: UpperBounded Number where
  top = topNumber

instance lowerBoundedNumber :: LowerBounded Number where
  bottom = bottomNumber

instance partialOrdNumber :: PartialOrd Number where
  leq = lessThanOrEq
  comparable _ _ = true

04PartialOrd.js

export const topInt = Number.MAX_SAFE_INTEGER;
export const bottomInt = Number.MIN_SAFE_INTEGER;

export const topChar = String.fromCharCode(65535);
export const bottomChar = String.fromCharCode(0);

export const topNumber = Number.POSITIVE_INFINITY;
export const bottomNumber = Number.NEGATIVE_INFINITY;