{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
module Language.Alloy.Parser (
parseInstance,
) where
import qualified Data.Set as S (fromList)
import qualified Data.Map as M
(alter, empty, insert, singleton)
import Control.Applicative ((<|>))
import Control.Monad (void)
import Control.Monad.Except (MonadError, throwError)
import Data.ByteString (ByteString)
import Data.Functor (($>))
import Data.List (intercalate)
import Data.List.Extra (unsnoc)
import Data.Maybe (fromJust)
import Data.Set (Set)
import Text.Trifecta
import Language.Alloy.Types (
AlloyInstance,
Annotation (..),
Entries,
Entry (..),
Object (..),
Relation (..),
Signature (..),
)
parseInstance :: (MonadError ErrInfo m) => ByteString -> m AlloyInstance
parseInstance :: ByteString -> m AlloyInstance
parseInstance ByteString
inst = case Parser [Entries (,)] -> Delta -> ByteString -> Result [Entries (,)]
forall a. Parser a -> Delta -> ByteString -> Result a
parseByteString Parser [Entries (,)]
alloyInstance Delta
forall a. Monoid a => a
mempty ByteString
inst of
Failure ErrInfo
l -> ErrInfo -> m AlloyInstance
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrInfo
l
Success [Entries (,)]
r -> AlloyInstance -> m AlloyInstance
forall (m :: * -> *) a. Monad m => a -> m a
return (AlloyInstance -> m AlloyInstance)
-> AlloyInstance -> m AlloyInstance
forall a b. (a -> b) -> a -> b
$ [Entries (,)] -> AlloyInstance
combineEntries [Entries (,)]
r
combineEntries :: [Entries (,)] -> AlloyInstance
combineEntries :: [Entries (,)] -> AlloyInstance
combineEntries = (AlloyInstance -> Entries (,) -> AlloyInstance)
-> AlloyInstance -> [Entries (,)] -> AlloyInstance
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl AlloyInstance -> Entries (,) -> AlloyInstance
forall k (b :: * -> *).
Ord k =>
Map k (Entry Map b) -> (k, Entry (,) b) -> Map k (Entry Map b)
createOrInsert AlloyInstance
forall k a. Map k a
M.empty
where
createOrInsert :: Map k (Entry Map b) -> (k, Entry (,) b) -> Map k (Entry Map b)
createOrInsert Map k (Entry Map b)
ys (k
s, Entry (,) b
e) = (Maybe (Entry Map b) -> Maybe (Entry Map b))
-> k -> Map k (Entry Map b) -> Map k (Entry Map b)
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter (Entry Map b -> Maybe (Entry Map b)
forall a. a -> Maybe a
Just (Entry Map b -> Maybe (Entry Map b))
-> (Maybe (Entry Map b) -> Entry Map b)
-> Maybe (Entry Map b)
-> Maybe (Entry Map b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry (,) b -> Maybe (Entry Map b) -> Entry Map b
forall (b :: * -> *).
Entry (,) b -> Maybe (Entry Map b) -> Entry Map b
alterSig Entry (,) b
e) k
s Map k (Entry Map b)
ys
alterSig :: Entry (,) b -> Maybe (Entry Map b) -> Entry Map b
alterSig Entry (,) b
e Maybe (Entry Map b)
Nothing = Entry (,) b
e { relation :: Map String (Relation b)
relation = (String -> Relation b -> Map String (Relation b))
-> (String, Relation b) -> Map String (Relation b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> Relation b -> Map String (Relation b)
forall k a. k -> a -> Map k a
M.singleton ((String, Relation b) -> Map String (Relation b))
-> (String, Relation b) -> Map String (Relation b)
forall a b. (a -> b) -> a -> b
$ Entry (,) b -> (String, Relation b)
forall (a :: * -> * -> *) (b :: * -> *).
Entry a b -> a String (Relation b)
relation Entry (,) b
e}
alterSig Entry (,) b
e (Just Entry Map b
y) = Entry Map b
y { relation :: Map String (Relation b)
relation = (String
-> Relation b
-> Map String (Relation b)
-> Map String (Relation b))
-> (String, Relation b)
-> Map String (Relation b)
-> Map String (Relation b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String
-> Relation b -> Map String (Relation b) -> Map String (Relation b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Entry (,) b -> (String, Relation b)
forall (a :: * -> * -> *) (b :: * -> *).
Entry a b -> a String (Relation b)
relation Entry (,) b
e) (Entry Map b -> Map String (Relation b)
forall (a :: * -> * -> *) (b :: * -> *).
Entry a b -> a String (Relation b)
relation Entry Map b
y) }
crlf :: Parser Char
crlf :: Parser Char
crlf = Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'\r' Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'\n'
endOfLine :: Parser Char
endOfLine :: Parser Char
endOfLine = Parser Char
forall (m :: * -> *). CharParsing m => m Char
newline Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char
crlf
alloyInstance :: Parser [Entries (,)]
alloyInstance :: Parser [Entries (,)]
alloyInstance = [Entries (,)] -> [Entries (,)] -> [Entries (,)]
forall a. [a] -> [a] -> [a]
(++)
([Entries (,)] -> [Entries (,)] -> [Entries (,)])
-> Parser [Entries (,)] -> Parser ([Entries (,)] -> [Entries (,)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Parser [Entries (,)]
entrySection String
"---INSTANCE---"
Parser ([Entries (,)] -> [Entries (,)])
-> Parser [Entries (,)] -> Parser [Entries (,)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Parser [Entries (,)]
entrySection String
"------State 0-------"
where
entrySection :: String -> Parser [Entries (,)]
entrySection String
x = (Parser () -> Parser ()
forall (m :: * -> *) a. Parsing m => m a -> m a
try (Parser Char -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Parser Char -> Parser ()) -> Parser Char -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
x Parser String -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char
endOfLine) Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> () -> Parser ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Parser () -> Parser [Entries (,)] -> Parser [Entries (,)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (Entries (,)) -> Parser [Entries (,)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser (Entries (,))
entry
entry :: Parser (Entries (,))
entry :: Parser (Entries (,))
entry = do
Maybe Annotation
entryAnnotation <- Parser (Maybe Annotation) -> Parser (Maybe Annotation)
forall (m :: * -> *) a. Parsing m => m a -> m a
try (String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
"skolem " Parser String -> Maybe Annotation -> Parser (Maybe Annotation)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Annotation -> Maybe Annotation
forall a. a -> Maybe a
Just Annotation
Skolem) Parser (Maybe Annotation)
-> Parser (Maybe Annotation) -> Parser (Maybe Annotation)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Annotation -> Parser (Maybe Annotation)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Annotation
forall a. Maybe a
Nothing
Signature
entrySignature <- Parser Signature
sig
(Signature
entrySignature,)
(Entry (,) Set -> Entries (,))
-> Parser (Entry (,) Set) -> Parser (Entries (,))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe Annotation -> (String, Relation Set) -> Entry (,) Set
forall (a :: * -> * -> *) (b :: * -> *).
Maybe Annotation -> a String (Relation b) -> Entry a b
Entry Maybe Annotation
entryAnnotation
((String, Relation Set) -> Entry (,) Set)
-> Parser (String, Relation Set) -> Parser (Entry (,) Set)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,)
(String -> Relation Set -> (String, Relation Set))
-> Parser String -> Parser (Relation Set -> (String, Relation Set))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
"<:" Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String
word) Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Parser String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"")
Parser (Relation Set -> (String, Relation Set))
-> Parser (Relation Set) -> Parser (String, Relation Set)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Relation Set)
parseRelations Parser (String, Relation Set)
-> Parser () -> Parser (String, Relation Set)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser Char -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Parser Char
endOfLine Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
forall (m :: * -> *). Parsing m => m ()
eof)))
sig :: Parser Signature
sig :: Parser Signature
sig = do
[String]
xs' <- Parser [String]
slashedWord
Signature -> Parser Signature
forall (m :: * -> *) a. Monad m => a -> m a
return (Signature -> Parser Signature) -> Signature -> Parser Signature
forall a b. (a -> b) -> a -> b
$ case Maybe ([String], String) -> ([String], String)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe ([String], String) -> ([String], String))
-> Maybe ([String], String) -> ([String], String)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe ([String], String)
forall a. [a] -> Maybe ([a], a)
unsnoc [String]
xs' of
([], String
x) -> Maybe String -> String -> Signature
Signature Maybe String
forall a. Maybe a
Nothing String
x
([String]
xs, String
x) -> Maybe String -> String -> Signature
Signature (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"/" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take ([String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
xs') [String]
xs) String
x
parseRelations :: Parser (Relation Set)
parseRelations :: Parser (Relation Set)
parseRelations = Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'='
Parser Char -> Parser (Relation Set) -> Parser (Relation Set)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Parser (Relation Set) -> Parser (Relation Set)
forall (m :: * -> *) a. Parsing m => m a -> m a
try (String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
"{}" Parser String -> Relation Set -> Parser (Relation Set)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Relation Set
forall (a :: * -> *). Relation a
EmptyRelation)
Parser (Relation Set)
-> Parser (Relation Set) -> Parser (Relation Set)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Object -> Relation Set
forall (a :: * -> *). Object -> Relation a
Id (Object -> Relation Set) -> Parser Object -> Parser (Relation Set)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Object -> Parser Object
forall (m :: * -> *) a. Parsing m => m a -> m a
try Parser Object
object)
Parser (Relation Set)
-> Parser (Relation Set) -> Parser (Relation Set)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Set (Object, Object, Object) -> Relation Set)
-> Parser (Set (Object, Object, Object)) -> Parser (Relation Set)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set (Object, Object, Object) -> Relation Set
forall (a :: * -> *). a (Object, Object, Object) -> Relation a
Triple (Parser (Set (Object, Object, Object))
-> Parser (Set (Object, Object, Object))
forall (m :: * -> *) a. Parsing m => m a -> m a
try (Parser (Set (Object, Object, Object))
-> Parser (Set (Object, Object, Object)))
-> Parser (Set (Object, Object, Object))
-> Parser (Set (Object, Object, Object))
forall a b. (a -> b) -> a -> b
$ Parser (Object, Object, Object)
-> Parser (Set (Object, Object, Object))
forall (f :: * -> *) a. (Ord a, CharParsing f) => f a -> f (Set a)
sep Parser (Object, Object, Object)
tripleRel)
Parser (Relation Set)
-> Parser (Relation Set) -> Parser (Relation Set)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Set (Object, Object) -> Relation Set)
-> Parser (Set (Object, Object)) -> Parser (Relation Set)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set (Object, Object) -> Relation Set
forall (a :: * -> *). a (Object, Object) -> Relation a
Double (Parser (Set (Object, Object)) -> Parser (Set (Object, Object))
forall (m :: * -> *) a. Parsing m => m a -> m a
try (Parser (Set (Object, Object)) -> Parser (Set (Object, Object)))
-> Parser (Set (Object, Object)) -> Parser (Set (Object, Object))
forall a b. (a -> b) -> a -> b
$ Parser (Object, Object) -> Parser (Set (Object, Object))
forall (f :: * -> *) a. (Ord a, CharParsing f) => f a -> f (Set a)
sep Parser (Object, Object)
doubleRel)
Parser (Relation Set)
-> Parser (Relation Set) -> Parser (Relation Set)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Set Object -> Relation Set)
-> Parser (Set Object) -> Parser (Relation Set)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Set Object -> Relation Set
forall (a :: * -> *). a Object -> Relation a
Single (Parser Object -> Parser (Set Object)
forall (f :: * -> *) a. (Ord a, CharParsing f) => f a -> f (Set a)
sep Parser Object
singleRel))
where
sep :: f a -> f (Set a)
sep f a
rel = [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList
([a] -> Set a) -> f [a] -> f (Set a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Char -> f Char -> f [a] -> f [a]
forall (m :: * -> *) bra ket a.
Applicative m =>
m bra -> m ket -> m a -> m a
between (Char -> f Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'{') (Char -> f Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'}') (f a
rel f a -> f String -> f [a]
forall (m :: * -> *) a sep. Alternative m => m a -> m sep -> m [a]
`sepBy` String -> f String
forall (m :: * -> *). CharParsing m => String -> m String
string String
", ")
tripleRel :: Parser (Object, Object, Object)
tripleRel = (,,) (Object -> Object -> Object -> (Object, Object, Object))
-> Parser Object
-> Parser (Object -> Object -> (Object, Object, Object))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Object
nextObject Parser (Object -> Object -> (Object, Object, Object))
-> Parser Object -> Parser (Object -> (Object, Object, Object))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Object
nextObject Parser (Object -> (Object, Object, Object))
-> Parser Object -> Parser (Object, Object, Object)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Object
object
doubleRel :: Parser (Object, Object)
doubleRel = (,) (Object -> Object -> (Object, Object))
-> Parser Object -> Parser (Object -> (Object, Object))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Object
nextObject Parser (Object -> (Object, Object))
-> Parser Object -> Parser (Object, Object)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Object
object
singleRel :: Parser Object
singleRel = Parser Object
object
nextObject :: Parser Object
nextObject = Parser Object
object Parser Object -> Parser String -> Parser Object
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
"->"
object :: Parser Object
object :: Parser Object
object =
Parser Object -> Parser Object
forall (m :: * -> *) a. Parsing m => m a -> m a
try (String -> Int -> Object
Object (String -> Int -> Object)
-> ([String] -> String) -> [String] -> Int -> Object
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"/" ([String] -> Int -> Object)
-> Parser [String] -> Parser (Int -> Object)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [String]
slashedWord Parser (Int -> Object) -> Parser Char -> Parser (Int -> Object)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'$' Parser (Int -> Object) -> Parser Int -> Parser Object
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Int
forall a. Read a => String -> a
read (String -> Int) -> Parser String -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some Parser Char
forall (m :: * -> *). CharParsing m => m Char
digit))
Parser Object -> Parser Object -> Parser Object
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Object -> Parser Object
forall (m :: * -> *) a. Parsing m => m a -> m a
try (Int -> Object
NumberObject (Int -> Object) -> Parser Int -> Parser Object
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Int
int)
Parser Object -> Parser Object -> Parser Object
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Object
NamedObject (String -> Object) -> Parser String -> Parser Object
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
word
int :: Parser Int
int :: Parser Int
int = (String -> Int) -> Parser String -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Int
forall a. Read a => String -> a
read (Parser String -> Parser Int) -> Parser String -> Parser Int
forall a b. (a -> b) -> a -> b
$ String -> String -> String
forall a. [a] -> [a] -> [a]
(++)
(String -> String -> String)
-> Parser String -> Parser (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser String -> Parser String
forall (m :: * -> *) a. Parsing m => m a -> m a
try (String -> Parser String
forall (m :: * -> *). CharParsing m => String -> m String
string String
"-") Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Parser String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"")
Parser (String -> String) -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Char -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some Parser Char
forall (m :: * -> *). CharParsing m => m Char
digit
slashedWord :: Parser [String]
slashedWord :: Parser [String]
slashedWord = Parser String
word Parser String -> Parser Char -> Parser [String]
forall (m :: * -> *) a sep. Alternative m => m a -> m sep -> m [a]
`sepBy1` Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'/'
word :: Parser String
word :: Parser String
word = (:)
(Char -> String -> String)
-> Parser Char -> Parser (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Char
forall (m :: * -> *). CharParsing m => m Char
letter Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'$')
Parser (String -> String) -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Char -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser Char
forall (m :: * -> *). CharParsing m => m Char
letter Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char
forall (m :: * -> *). CharParsing m => m Char
digit Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'_' Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char Char
'\'')