liquidhaskell-0.8.10.7: tests/ple/pos/RegexpDerivative.hs
-- | http://matt.might.net/articles/implementation-of-regular-expression-matching-in-scheme-with-derivatives/
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
{-@ infixr ++ @-}
{-# LANGUAGE GADTs #-}
module RE where
import Prelude hiding ((++))
-------------------------------------------------------------------
-- | Regular Expressions
-------------------------------------------------------------------
{-@ data RE [reSize] @-}
data RE a
= None
| Empty
| Char a
| Cat (RE a) (RE a)
| Alt (RE a) (RE a)
| Star (RE a)
{-@ measure reSize @-}
{-@ reSize :: RE a -> Nat @-}
reSize :: RE a -> Int
reSize None = 0
reSize Empty = 0
reSize (Char _) = 0
reSize (Cat r1 r2) = 1 + reSize r1 + reSize r2
reSize (Alt r1 r2) = 1 + reSize r1 + reSize r2
reSize (Star r) = 1 + reSize r
-------------------------------------------------------------------
-- | Derivative-based Match
-------------------------------------------------------------------
{-@ reflect dmatch @-}
dmatch :: (Eq a) => List a -> RE a -> Bool
dmatch xs r = empty (derivs r xs)
{-@ reflect derivs @-}
{-@ derivs :: _ -> xs:_ -> _ / [size xs] @-}
derivs :: (Eq a) => RE a -> List a -> RE a
derivs r Nil = r
derivs r (Cons c cs) = derivs (deriv r c) cs
-------------------------------------------------------------------
-- | Derivative
-------------------------------------------------------------------
{-@ reflect deriv @-}
deriv :: (Eq a) => RE a -> a -> RE a
deriv None _ = None
deriv Empty _ = None
deriv (Char y) x
| x == y = Empty
| otherwise = None
deriv (Alt r1 r2) x = Alt (deriv r1 x) (deriv r2 x)
deriv (Star r) x = Cat (deriv r x) (Star r)
deriv (Cat r1 r2) x
| empty r1 = Alt (Cat (deriv r1 x) r2) (deriv r2 x)
| otherwise = (Cat (deriv r1 x) r2)
{-@ reflect empty @-}
empty :: RE a -> Bool
empty None = False
empty (Char _) = False
empty Empty = True
empty (Star _) = True
empty (Cat r1 r2) = empty r1 && empty r2
empty (Alt r1 r2) = empty r1 || empty r2
-------------------------------------------------------------------------------
data MatchP a where
Match :: List a -> RE a -> MatchP a
data Match a where
MEmpty :: Match a
MChar :: a -> Match a
MCat :: List a -> RE a -> List a -> RE a -> Match a -> Match a -> Match a
MAltL :: List a -> RE a -> RE a -> Match a -> Match a
MAltR :: List a -> RE a -> RE a -> Match a -> Match a
MStar0 :: RE a -> Match a
MStar1 :: List a -> List a -> RE a -> Match a -> Match a -> Match a
{-@ data Match [msize] a where
MEmpty :: Prop (Match Nil Empty)
MChar :: x:_ -> Prop (Match (single x) (Char x))
MCat :: s1:_ -> r1:_ -> s2:_ -> r2:_ ->
Prop (Match s1 r1) ->
Prop (Match s2 r2) ->
Prop (Match {s1 ++ s2} (Cat r1 r2))
MAltL :: s:_ -> r1:_ -> r2:_ ->
Prop (Match s r1) ->
Prop (Match s (Alt r1 r2))
MAltR :: s:_ -> r1:_ -> r2:_ ->
Prop (Match s r2) ->
Prop (Match s (Alt r1 r2))
MStar0 :: r:_ ->
Prop (Match Nil (Star r))
MStar1 :: s1:{0 < size s1} -> s2:_ -> r:_ ->
Prop (Match s1 r) ->
Prop (Match s2 (Star r)) ->
Prop (Match {s1 ++ s2} (Star r))
@-}
{-@ measure msize @-}
{-@ msize :: Match a -> Nat @-}
msize :: Match a -> Int
msize (MEmpty {}) = 0
msize (MChar {}) = 0
msize (MStar0 _) = 0
msize (MCat _ _ _ _ m1 m2) = 1 + msize m1 + msize m2
msize (MAltL _ _ _ m1) = 1 + msize m1
msize (MAltR _ _ _ m2) = 1 + msize m2
msize (MStar1 _ _ _ m1 m2) = 1 + msize m1 + msize m2
--------------------------------------------------------------------------------
-- | Theorem: Derivative Matching Equivalence
--------------------------------------------------------------------------------
{-@ thm :: cs:_ -> r:_ -> Prop (Match cs r) -> { dmatch cs r } @-}
thm :: (Eq a) => List a -> RE a -> Match a -> ()
thm cs r cs_match_r = lemEmp r_cs emp_match_r_cs
where
r_cs = derivs r cs
emp_match_r_cs = lem1s cs r cs_match_r
{-@ thm' :: cs:_ -> r:{ dmatch cs r } -> Prop (Match cs r) @-}
thm' :: (Eq a) => List a -> RE a -> Match a
thm' cs r = lem1s' cs r emp_match_r_cs
where
r_cs = derivs r cs
emp_match_r_cs = lemEmp' r_cs
--------------------------------------------------------------------------------
-- | Lemma: One-char Equivalence
--------------------------------------------------------------------------------
{-@ lem1 :: c:_ -> cs:_ -> r:_
-> pf: Prop (Match (Cons c cs) r)
-> Prop (Match cs (deriv r c)) / [msize pf]
@-}
lem1 :: (Eq a) => a -> List a -> RE a -> Match a -> Match a
lem1 _ _ None MEmpty
= MEmpty
lem1 _ _ Empty MEmpty
= MEmpty
lem1 _ _ (Char _) (MChar _)
= MEmpty
lem1 c cs (Alt r1 r2) (MAltL _ _ _ m1)
= MAltL cs (deriv r1 c) (deriv r2 c) (lem1 c cs r1 m1)
lem1 c cs (Alt r1 r2) (MAltR _ _ _ m2)
= MAltR cs (deriv r1 c) (deriv r2 c) (lem1 c cs r2 m2)
lem1 c cs (Cat r1 r2) (MCat Nil _ s2 _ m1 m2)
= lemEmp r1 m1 & MAltR cs (Cat (deriv r1 c) r2) (deriv r2 c) (lem1 c cs r2 m2)
lem1 c cs (Cat r1 r2) (MCat (Cons _ s1) _ s2 _ m1 m2)
| empty r1
= MAltL (s1 ++ s2) (Cat r1c r2) (deriv r2 c) m -- :: Match (s1 ++ s2) (deriv r c)
| otherwise
= m
where
r1c = deriv r1 c
m = MCat s1 r1c s2 r2 (lem1 c s1 r1 m1) m2 -- :: Match (s1 ++ s2) (Cat r1c r2)
lem1 _ _ (Star _) (MStar0 _)
= MEmpty
lem1 c cs (Star r) (MStar1 (Cons _ s0) s _ m0 m)
= MCat s0 r' s (Star r) m0' m -- :: Match (s0 ++ s) (Cat r' (Star r))
where
m0' = lem1 c s0 r m0 -- :: Match s0 r'
r' = deriv r c
-- m0 :: Match (Cons c s0) r
-- m :: Match s (Star r)
-- :: { cs == s0 ++ s }
{-@ lem1s :: cs:_ -> r:_ -> Prop (Match cs r) -> Prop (Match Nil (derivs r cs)) @-}
lem1s :: (Eq a) => List a -> RE a -> Match a -> Match a
lem1s Nil _ m = m
lem1s (Cons x xs) r m = lem1s xs (deriv r x) (lem1 x xs r m)
{-@ lem1a :: c:_ -> cs:_ -> r:_
-> m: Prop (Match cs (deriv r c))
-> Prop (Match (Cons c cs) r) / [msize m, 1]
@-}
lem1a :: (Eq a) => a -> List a -> RE a -> Match a -> Match a
lem1a _ _ None MEmpty = MEmpty
lem1a _ _ Empty MEmpty = MEmpty
lem1a c _ (Char _) MEmpty = MChar c
lem1a c cs (Alt r1 r2) (MAltL _ _ _ m1')
= MAltL (Cons c cs) r1 r2 (lem1a c cs r1 m1')
-- :: Match (Cons c cs) r1
lem1a c cs (Alt r1 r2) (MAltR _ _ _ m2')
= MAltR (Cons c cs) r1 r2 (lem1a c cs r2 m2')
-- :: Match (Cons c cs) r2
lem1a c cs (Star r) (MCat s0 _ s _ m0' m)
= MStar1 (Cons c s0) s r (lem1a c s0 r m0') m
-- :: Match (Cons c s0) r
lem1a c cs (Cat r1 r2) pf
| empty r1
= case pf of
MAltL _ r1c_r2 r2c m_r1c_r2 -> lemCat c cs r1 r2 m_r1c_r2
MAltR _ r1c_r2 r2c m_r2c -> MCat Nil r1 (Cons c cs) r2
(lemEmp' r1) -- :: Match Nil r1
(lem1a c cs r2 m_r2c) -- :: Match (Cons c cs) r2
| otherwise
= lemCat c cs r1 r2 pf
{-@ lemCat :: c:_ -> cs:_ -> r1:_ -> r2:_
-> pf:Prop (Match cs (Cat (deriv r1 c) r2))
-> Prop (Match (Cons c cs) (Cat r1 r2)) / [msize pf, 0]
@-}
lemCat :: (Eq a) => a -> List a -> RE a -> RE a -> Match a -> Match a
lemCat c cs r1 r2 (MCat s1 _ s2 _ m1' m2)
= MCat (Cons c s1) r1 s2 r2 (lem1a c s1 r1 m1') m2
-- :: Match (Cons c s1) r1
{-@ lem1s' :: cs:_ -> r:_ -> Prop (Match Nil (derivs r cs)) -> Prop (Match cs r) @-}
lem1s' :: (Eq a) => List a -> RE a -> Match a -> Match a
lem1s' Nil r m = m
lem1s' (Cons x xs) r m = lem1a x xs r (lem1s' xs (deriv r x) m)
{-@ lemEmp :: r:_ -> Prop (Match Nil r) -> {empty r} @-}
lemEmp :: (Eq a) => RE a -> Match a -> ()
lemEmp None MEmpty = ()
lemEmp Empty _ = ()
lemEmp (Star _) _ = ()
lemEmp (Char c) (MChar _) = ()
lemEmp (Cat r1 r2) (MCat s1 _ s2 _ e1 e2) = app_nil_nil s1 s2 & lemEmp r1 e1 & lemEmp r2 e2
lemEmp (Alt r1 r2) (MAltL _ _ _ e1) = lemEmp r1 e1
lemEmp (Alt r1 r2) (MAltR _ _ _ e2) = lemEmp r2 e2
{-@ lemEmp' :: r:{empty r} -> Prop (Match Nil r) @-}
lemEmp' :: RE a -> Match a
lemEmp' Empty = MEmpty
lemEmp' (Star r) = MStar0 r
lemEmp' (Cat r1 r2) = MCat Nil r1 Nil r2 (lemEmp' r1) (lemEmp' r2)
lemEmp' (Alt r1 r2)
| empty r1 = MAltL Nil r1 r2 (lemEmp' r1)
| empty r2 = MAltR Nil r1 r2 (lemEmp' r2)
--------------------------------------------------------------------------------
-- | Lists
--------------------------------------------------------------------------------
{-@ data List [size] @-}
data List a
= Nil
| Cons a (List a)
deriving (Eq)
{-@ measure size @-}
{-@ size :: List a -> Nat @-}
size :: List a -> Int
size Nil = 0
size (Cons _ xs) = 1 + size xs
{-@ reflect ++ @-}
(++) :: List a -> List a -> List a
Nil ++ ys = ys
(Cons x xs) ++ ys = Cons x (xs ++ ys)
{-@ reflect single @-}
single :: a -> List a
single x = Cons x Nil
{-@ app_nil_nil :: s1:_ -> s2:{s1 ++ s2 == Nil} -> {s1 == Nil && s2 == Nil} @-}
app_nil_nil :: List a -> List a -> ()
app_nil_nil Nil Nil = ()
--------------------------------------------------------------------------------
-- | Boilerplate
--------------------------------------------------------------------------------
{-@ measure prop :: a -> b @-}
{-@ type Prop E = {v:_ | prop v = E} @-}
(&) = seq
-------------------------------------------------------------------
-- | Kwangkeun Yi's Match
-- https://www.cambridge.org/core/journals/journal-of-functional-programming/article/educational-pearl-proof-directed-debugging-revisited-for-a-first-order-version/F7CC0A759398A52C35F21F13236C0E00
-------------------------------------------------------------------
{-@ kmatch :: cs:_ -> r:_ -> _ / [size cs, reSize r] @-}
kmatch :: (Eq a) => List a -> RE a -> Bool
kmatch _ None = False
kmatch Nil r = empty r
kmatch cs (Char c) = cs == Cons c Nil
kmatch cs (Alt r1 r2) = kmatch cs r1 || kmatch cs r2
kmatch (Cons c cs) (Star r) = kmatch cs (Cat (deriv r c) r)
kmatch (Cons c cs) r = kmatch cs (deriv r c)