{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections #-}
{-|
Module      : Language.Alloy.Parser
Description : A generic Alloy instance parser for Call Alloy library
Copyright   : (c) Marcellus Siegburg, 2019
License     : MIT
Maintainer  : marcellus.siegburg@uni-due.de

This module allows for parsing and converting instances into Haskell data
structures.
Basically all modules are parsed into a Map of Map of Set allowing easy lookup
of every returned set and relation.
-}
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.Set                         (Set)
import Text.Trifecta

import Language.Alloy.Types (
  AlloyInstance,
  Annotation (..),
  Entries,
  Entry (..),
  Object (..),
  Relation (..),
  Signature (..),
  )

{-|
Parse an Alloy instance from a given String.
May fail with 'ErrInfo'.
-}
parseInstance :: (MonadError ErrInfo m) => ByteString -> m AlloyInstance
parseInstance :: ByteString -> m AlloyInstance
parseInstance inst :: 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 l :: ErrInfo
l -> ErrInfo -> m AlloyInstance
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ErrInfo
l
  Success r :: [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 ys :: Map k (Entry Map b)
ys (s :: k
s, e :: 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 e :: Entry (,) b
e 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 e :: Entry (,) b
e (Just y :: 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) }

alloyInstance :: Parser [Entries (,)]
alloyInstance :: Parser [Entries (,)]
alloyInstance = (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 "---INSTANCE---" Parser String -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char
forall (m :: * -> *). CharParsing m => m Char
newline) 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 "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 "<:" 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 "")
              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
forall (m :: * -> *). CharParsing m => m Char
newline 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 =
  Parser Signature -> Parser Signature
forall (m :: * -> *) a. Parsing m => m a -> m a
try (Maybe String -> String -> Signature
Signature (Maybe String -> String -> Signature)
-> Parser (Maybe String) -> Parser (String -> Signature)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> Parser String -> Parser (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
word) Parser (String -> Signature)
-> Parser Char -> Parser (String -> Signature)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m Char
char '/' Parser (String -> Signature) -> Parser String -> Parser Signature
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser String
word)
  Parser Signature -> Parser Signature -> Parser Signature
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe String -> String -> Signature
Signature Maybe String
forall a. Maybe a
Nothing (String -> Signature) -> Parser String -> Parser Signature
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
word

parseRelations :: Parser (Relation Set)
parseRelations :: Parser (Relation Set)
parseRelations = Char -> Parser Char
forall (m :: * -> *). CharParsing m => Char -> m 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 "{}" 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
<|> (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 rel :: 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 -> f Char
forall (m :: * -> *). CharParsing m => Char -> m 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 ", ")
    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 "->"

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)
-> Parser String -> Parser (Int -> Object)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
word 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 '$' 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 "-") 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 "")
  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

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 '$')
  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 '_' 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 '\'')