{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.RegExp (
RegExp(..)
, RegExpMatchable(..)
, exactly
, oneOf
, newline, whiteSpaceNoNewLine, whiteSpace
, tab, punctuation
, asciiLetter, asciiLower, asciiUpper
, digit, octDigit, hexDigit
, decimal, octal, hexadecimal, floating
, identifier
) where
import Prelude hiding (length, take, elem, notElem, head)
import qualified Prelude as P
import qualified Data.List as L
import Data.SBV.Core.Data
import Data.SBV.Core.Model ()
import Data.SBV.String
import qualified Data.Char as C
import Data.Proxy
import Data.SBV.Char
class RegExpMatchable a where
match :: a -> RegExp -> SBool
instance RegExpMatchable SChar where
match :: SChar -> RegExp -> SBool
match = SString -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
match (SString -> RegExp -> SBool)
-> (SChar -> SString) -> SChar -> RegExp -> SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SChar -> SString
singleton
instance RegExpMatchable SString where
match :: SString -> RegExp -> SBool
match input :: SString
input regExp :: RegExp
regExp = StrOp -> Maybe (String -> Bool) -> SString -> SBool
forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 (RegExp -> StrOp
StrInRe RegExp
regExp) ((String -> Bool) -> Maybe (String -> Bool)
forall a. a -> Maybe a
Just (RegExp -> (String -> Bool) -> String -> Bool
go RegExp
regExp String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null)) SString
input
where
go :: RegExp -> (String -> Bool) -> String -> Bool
go :: RegExp -> (String -> Bool) -> String -> Bool
go (Literal l :: String
l) k :: String -> Bool
k s :: String
s = String
l String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` String
s Bool -> Bool -> Bool
&& String -> Bool
k (Int -> String -> String
forall a. Int -> [a] -> [a]
P.drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length String
l) String
s)
go All _ _ = Bool
True
go None _ _ = Bool
False
go (Range _ _) _ [] = Bool
False
go (Range a :: Char
a b :: Char
b) k :: String -> Bool
k (c :: Char
c:cs :: String
cs) = Char
a Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
c Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
b Bool -> Bool -> Bool
&& String -> Bool
k String
cs
go (Conc []) k :: String -> Bool
k s :: String
s = String -> Bool
k String
s
go (Conc (r :: RegExp
r:rs :: [RegExp]
rs)) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go RegExp
r (RegExp -> (String -> Bool) -> String -> Bool
go ([RegExp] -> RegExp
Conc [RegExp]
rs) String -> Bool
k) String
s
go (KStar r :: RegExp
r) k :: String -> Bool
k s :: String
s = String -> Bool
k String
s Bool -> Bool -> Bool
|| RegExp -> (String -> Bool) -> String -> Bool
go RegExp
r (Int -> (String -> Bool) -> String -> Bool
forall (t :: * -> *) a.
Foldable t =>
Int -> (t a -> Bool) -> t a -> Bool
smaller (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length String
s) (RegExp -> (String -> Bool) -> String -> Bool
go (RegExp -> RegExp
KStar RegExp
r) String -> Bool
k)) String
s
go (KPlus r :: RegExp
r) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go ([RegExp] -> RegExp
Conc [RegExp
r, RegExp -> RegExp
KStar RegExp
r]) String -> Bool
k String
s
go (Opt r :: RegExp
r) k :: String -> Bool
k s :: String
s = String -> Bool
k String
s Bool -> Bool -> Bool
|| RegExp -> (String -> Bool) -> String -> Bool
go RegExp
r String -> Bool
k String
s
go (Loop i :: Int
i j :: Int
j r :: RegExp
r) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go ([RegExp] -> RegExp
Conc (Int -> RegExp -> [RegExp]
forall a. Int -> a -> [a]
replicate Int
i RegExp
r [RegExp] -> [RegExp] -> [RegExp]
forall a. [a] -> [a] -> [a]
++ Int -> RegExp -> [RegExp]
forall a. Int -> a -> [a]
replicate (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) (RegExp -> RegExp
Opt RegExp
r))) String -> Bool
k String
s
go (Union []) _ _ = Bool
False
go (Union [x :: RegExp
x]) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go RegExp
x String -> Bool
k String
s
go (Union (x :: RegExp
x:xs :: [RegExp]
xs)) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go RegExp
x String -> Bool
k String
s Bool -> Bool -> Bool
|| RegExp -> (String -> Bool) -> String -> Bool
go ([RegExp] -> RegExp
Union [RegExp]
xs) String -> Bool
k String
s
go (Inter a :: RegExp
a b :: RegExp
b) k :: String -> Bool
k s :: String
s = RegExp -> (String -> Bool) -> String -> Bool
go RegExp
a String -> Bool
k String
s Bool -> Bool -> Bool
&& RegExp -> (String -> Bool) -> String -> Bool
go RegExp
b String -> Bool
k String
s
smaller :: Int -> (t a -> Bool) -> t a -> Bool
smaller orig :: Int
orig k :: t a -> Bool
k inp :: t a
inp = t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length t a
inp Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
orig Bool -> Bool -> Bool
&& t a -> Bool
k t a
inp
exactly :: String -> RegExp
exactly :: String -> RegExp
exactly = String -> RegExp
Literal
oneOf :: String -> RegExp
oneOf :: String -> RegExp
oneOf xs :: String
xs = [RegExp] -> RegExp
Union [String -> RegExp
exactly [Char
x] | Char
x <- String
xs]
newline :: RegExp
newline :: RegExp
newline = String -> RegExp
oneOf "\n\r\f"
tab :: RegExp
tab :: RegExp
tab = String -> RegExp
oneOf "\t"
whiteSpaceNoNewLine :: RegExp
whiteSpaceNoNewLine :: RegExp
whiteSpaceNoNewLine = RegExp
tab RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ String -> RegExp
oneOf "\v\160 "
whiteSpace :: RegExp
whiteSpace :: RegExp
whiteSpace = RegExp
newline RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
whiteSpaceNoNewLine
punctuation :: RegExp
punctuation :: RegExp
punctuation = String -> RegExp
oneOf (String -> RegExp) -> String -> RegExp
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter Char -> Bool
C.isPunctuation (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ (Int -> Char) -> [Int] -> String
forall a b. (a -> b) -> [a] -> [b]
map Int -> Char
C.chr [0..255]
asciiLetter :: RegExp
asciiLetter :: RegExp
asciiLetter = RegExp
asciiLower RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
asciiUpper
asciiLower :: RegExp
asciiLower :: RegExp
asciiLower = Char -> Char -> RegExp
Range 'a' 'z'
asciiUpper :: RegExp
asciiUpper :: RegExp
asciiUpper = Char -> Char -> RegExp
Range 'A' 'Z'
digit :: RegExp
digit :: RegExp
digit = Char -> Char -> RegExp
Range '0' '9'
octDigit :: RegExp
octDigit :: RegExp
octDigit = Char -> Char -> RegExp
Range '0' '7'
hexDigit :: RegExp
hexDigit :: RegExp
hexDigit = RegExp
digit RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ Char -> Char -> RegExp
Range 'a' 'f' RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ Char -> Char -> RegExp
Range 'A' 'F'
decimal :: RegExp
decimal :: RegExp
decimal = RegExp -> RegExp
KPlus RegExp
digit
octal :: RegExp
octal :: RegExp
octal = ("0o" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "0O") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
KPlus RegExp
octDigit
hexadecimal :: RegExp
hexadecimal :: RegExp
hexadecimal = ("0x" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "0X") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
KPlus RegExp
hexDigit
floating :: RegExp
floating :: RegExp
floating = RegExp
withFraction RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
withoutFraction
where withFraction :: RegExp
withFraction = RegExp
decimal RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* "." RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
decimal RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
Opt RegExp
expt
withoutFraction :: RegExp
withoutFraction = RegExp
decimal RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
expt
expt :: RegExp
expt = ("e" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "E") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
Opt (String -> RegExp
oneOf "+-") RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp
decimal
identifier :: RegExp
identifier :: RegExp
identifier = RegExp
asciiLower RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
* RegExp -> RegExp
KStar (RegExp
asciiLetter RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ RegExp
digit RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "_" RegExp -> RegExp -> RegExp
forall a. Num a => a -> a -> a
+ "'")
lift1 :: forall a b. (SymVal a, SymVal b) => StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 :: StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 w :: StrOp
w mbOp :: Maybe (a -> b)
mbOp a :: SBV a
a
| Just cv :: SBV b
cv <- Maybe (a -> b) -> SBV a -> Maybe (SBV b)
forall a b.
(SymVal a, SymVal b) =>
Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Maybe (a -> b)
mbOp SBV a
a
= SBV b
cv
| Bool
True
= SVal -> SBV b
forall a. SVal -> SBV a
SBV (SVal -> SBV b) -> SVal -> SBV b
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
where k :: Kind
k = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)
r :: State -> IO SV
r st :: State
st = do SV
sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (StrOp -> Op
StrOp StrOp
w) [SV
sva])
concEval1 :: (SymVal a, SymVal b) => Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 :: Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 mbOp :: Maybe (a -> b)
mbOp a :: SBV a
a = b -> SBV b
forall a. SymVal a => a -> SBV a
literal (b -> SBV b) -> Maybe b -> Maybe (SBV b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b)
mbOp Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a)
__unused :: a
__unused :: a
__unused = (SChar -> SBool)
-> (SString -> SInteger)
-> (SInteger -> SString -> SString)
-> (SChar -> SString -> SBool)
-> (SChar -> SString -> SBool)
-> (SString -> SChar)
-> a
forall a. HasCallStack => a
undefined SChar -> SBool
isSpace SString -> SInteger
length SInteger -> SString -> SString
take SChar -> SString -> SBool
elem SChar -> SString -> SBool
notElem SString -> SChar
head