liquidhaskell-0.8.10.7: tests/todo/RegexpDerivative.hs
-- | http://matt.might.net/articles/implementation-of-regular-expression-matching-in-scheme-with-derivatives/
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
{-@ LIQUID "--diff" @-}
{-@ 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
-------------------------------------------------------------------
-- | 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:_ -> _ / [len cs, reSize r] @-}
kmatch :: (Eq a) => [a] -> RE a -> Bool
kmatch _ None = False
kmatch [] r = empty r
kmatch cs (Char c) = cs == [c]
kmatch cs (Alt r1 r2) = kmatch cs r1 || kmatch cs r2
kmatch (c:cs) (Star r) = kmatch cs (Cat (deriv r c) r)
kmatch (c:cs) r = kmatch cs (deriv r c)
-------------------------------------------------------------------
-- | Derivative-based Regular Expression Matching
-------------------------------------------------------------------
{-@ reflect dmatch @-}
dmatch :: (Eq a) => [a] -> RE a -> Bool
dmatch xs r = empty (derivs r xs)
{-@ reflect derivs @-}
{-@ derivs :: _ -> xs:_ -> _ / [len xs] @-}
derivs :: (Eq a) => RE a -> [a] -> RE a
derivs r [] = r
derivs r (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 :: [a] -> RE a -> MatchP a
data Match a where
MEmpty :: Match a
MChar :: a -> Match a
MCat :: [a] -> RE a -> [a] -> RE a -> Match a -> Match a -> Match a
MAltL :: [a] -> RE a -> RE a -> Match a -> Match a
MAltR :: [a] -> RE a -> RE a -> Match a -> Match a
MStar0 :: RE a -> Match a
MStar1 :: [a] -> [a] -> RE a -> Match a -> Match a -> Match a
{-@ data Match a where
MEmpty :: Prop (Match [] 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 [] (Star r))
| MStar1 :: s1:_ -> s2:_ -> r:_ ->
Prop (Match s1 r) ->
Prop (Match s2 (Star r)) ->
Prop (Match {s1 ++ s2} (Star r))
@-}
--------------------------------------------------------------------------------
-- | Theorem: Derivative Matching Equivalence
--------------------------------------------------------------------------------
{-@ thm :: cs:_ -> r:_ -> Prop (Match cs r) -> { dmatch cs r } @-}
thm :: (Eq a) => [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) => [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:_
-> Prop (Match (cons c cs) r)
-> Prop (Match cs (deriv r c))
@-}
lem1 :: (Eq a) => a -> [a] -> RE a -> Match a -> Match a
lem1 _ _ None MEmpty = MEmpty
lem1 c cs Empty MEmpty = cons_nil c cs `seq` MEmpty
-- lem1 c cs (Char _) (MChar _) = MEmpty
lem1 _ _ _ _ = undefined -- HARD
{-@ lem1s :: cs:_ -> r:_
-> Prop (Match cs r)
-> Prop (Match [] (derivs r cs))
@-}
lem1s :: (Eq a) => [a] -> RE a -> Match a -> Match a
lem1s [] _ m = m
lem1s (x:xs) r m = lem1s xs (deriv r x) (lem1 x xs r m)
{-@ lem1' :: c:_ -> cs:_ -> r:_
-> Prop (Match cs (deriv r c))
-> Prop (Match (cons c cs) r)
@-}
lem1' :: (Eq a) => a -> [a] -> RE a -> Match a -> Match a
lem1' = undefined -- HARD
{-@ lem1s' :: cs:_ -> r:_
-> Prop (Match [] (derivs r cs))
-> Prop (Match cs r)
@-}
lem1s' :: (Eq a) => [a] -> RE a -> Match a -> Match a
lem1s' [] r m = m
lem1s' (x:xs) r m = lem1' x xs r (lem1s' xs (deriv r x) m)
{-@ lemEmp :: r:_ -> Prop (Match [] r) -> {empty r} @-}
lemEmp :: (Eq a) => RE a -> Match a -> ()
lemEmp None MEmpty = ()
lemEmp Empty _ = ()
lemEmp (Star _) _ = ()
lemEmp (Cat r1 r2) (MCat s1 _ s2 _ e1 e2) = app_nil_nil s1 s2 `seq`
lemEmp r1 e1 `seq`
lemEmp r2 e2
lemEmp (Alt r1 r2) (MAltL _ _ _ e1) = lemEmp r1 e1
lemEmp (Alt r1 r2) (MAltR _ _ _ e2) = lemEmp r2 e2
lemEmp (Char c) (MChar _) = cons_nil c [] `seq` ()
{-@ lemEmp' :: r:{empty r} -> Prop (Match [] r) @-}
lemEmp' :: RE a -> Match a
lemEmp' Empty = MEmpty
lemEmp' (Star r) = MStar0 r
lemEmp' (Cat r1 r2) = MCat [] r1 [] r2 (lemEmp' r1) (lemEmp' r2)
lemEmp' (Alt r1 r2)
| empty r1 = MAltL [] r1 r2 (lemEmp' r1)
| empty r2 = MAltR [] r1 r2 (lemEmp' r2)
--------------------------------------------------------------------------------
-- | Boilerplate
--------------------------------------------------------------------------------
{-@ measure prop :: a -> b @-}
{-@ type Prop E = {v:_ | prop v = E} @-}
{-@ reflect ++ @-}
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
{-@ inline single @-}
single :: a -> [a]
single x = [x]
{-@ inline cons @-}
cons :: a -> [a] -> [a]
cons x xs = x : xs
(&&&) = seq
--------------------------------------------------------------------------------
-- Because GHC Lists are not encoded as ADT for some reason.
--------------------------------------------------------------------------------
{-@ single_nil :: c:_ -> { single c /= [] } @-}
single_nil :: a -> ()
single_nil _ = ()
{-@ cons_nil :: c:_ -> cs:_ -> { cons c cs /= [] } @-}
cons_nil :: a -> [a] -> ()
cons_nil _ _ = undefined
{-@ app_nil_nil :: s1:_ -> s2:{ s1 ++ s2 == [] }
-> { s1 == [] && s2 == [] }
@-}
app_nil_nil :: [a] -> [a] -> ()
app_nil_nil [] [] = ()