{- |
Module      :  ./CASL/CompositionTable/ParseTable2.hs
Description :  parsing SparQ CompositionTables
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  fmossa@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Parses CompositionTables in SparQ(Lisp)-Format using Parsec
 <http://www.cs.uu.nl/~daan/parsec.html>
-}

module CASL.CompositionTable.ParseTable2
  ( parseSparQTableFromFile
  , parseSparQTable
  , skip
  ) where

import Text.ParserCombinators.Parsec
import CASL.CompositionTable.CompositionTable
import CASL.CompositionTable.ModelTable
import CASL.CompositionTable.Keywords
import CASL.CompositionTable.ParseSparQ
import Common.Parsec
import Common.Utils
import qualified Control.Monad.Fail as Fail

import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import Data.Char
import Data.List

parseSparQTableFromFile :: String -> IO (Either ParseError Table2)
parseSparQTableFromFile :: String -> IO (Either ParseError Table2)
parseSparQTableFromFile = Parser Table2 -> String -> IO (Either ParseError Table2)
forall a. Parser a -> String -> IO (Either ParseError a)
parseFromFile (Parser ()
skip Parser () -> Parser Table2 -> Parser Table2
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Table2
parseSparQTable Parser Table2 -> Parser () -> Parser Table2
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)

makeTable :: [Baserel] -> (BMap, Table2)
makeTable :: [Baserel] -> (BMap, Table2)
makeTable rs :: [Baserel]
rs = ([(Baserel, Int)] -> BMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Baserel, Int)] -> BMap) -> [(Baserel, Int)] -> BMap
forall a b. (a -> b) -> a -> b
$ [Baserel] -> [(Baserel, Int)]
forall a. [a] -> [(a, Int)]
number [Baserel]
rs, Table -> Table2
toTable2 (Table -> Table2) -> Table -> Table2
forall a b. (a -> b) -> a -> b
$ Table_Attrs
-> Compositiontable
-> Conversetable
-> Reflectiontable
-> Models
-> Table
Table
      (String -> Baserel -> [Baserel] -> Table_Attrs
Table_Attrs "" (String -> Baserel
Baserel "") [Baserel]
rs)
      ([Cmptabentry] -> Compositiontable
Compositiontable []) ([Contabentry] -> Conversetable
Conversetable []) ([Reftabentry] -> Reflectiontable
Reflectiontable []) (Models -> Table) -> Models -> Table
forall a b. (a -> b) -> a -> b
$ [Model] -> Models
Models [])

parseSparQTable :: Parser Table2
parseSparQTable :: Parser Table2
parseSparQTable = Parser Table2 -> Parser Table2
forall a. Parser a -> Parser a
inParens (Parser Table2 -> Parser Table2) -> Parser Table2 -> Parser Table2
forall a b. (a -> b) -> a -> b
$ do
  String
calculusName <- Parser String
parseCalculusName
  (i1 :: [Baserel]
i1, rs1 :: [Baserel]
rs1) <- Parser ([Baserel], [Baserel])
parseIdBaOths
  (m :: BMap
m, Table2 _ _ ns :: IntMap Baserel
ns bs :: BSet
bs _ _, ct :: ConTables
ct, i2 :: [Baserel]
i2) <- if [Baserel] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Baserel]
rs1 then do
      Conversetable
ctOld <- Parser Conversetable
parseConversetable
      (i2 :: [Baserel]
i2, rs2 :: [Baserel]
rs2) <- Parser ([Baserel], [Baserel])
parseIdBaOths
      let (m :: BMap
m, t :: Table2
t) = [Baserel] -> (BMap, Table2)
makeTable ([Baserel] -> (BMap, Table2)) -> [Baserel] -> (BMap, Table2)
forall a b. (a -> b) -> a -> b
$ [Baserel]
rs1 [Baserel] -> [Baserel] -> [Baserel]
forall a. [a] -> [a] -> [a]
++ [Baserel]
rs2
      (BMap, Table2, ConTables, [Baserel])
-> ParsecT String () Identity (BMap, Table2, ConTables, [Baserel])
forall (m :: * -> *) a. Monad m => a -> m a
return (BMap
m, Table2
t, BMap -> Conversetable -> ConTables
toConTables BMap
m Conversetable
ctOld, [Baserel]
i1 [Baserel] -> [Baserel] -> [Baserel]
forall a. [a] -> [a] -> [a]
++ [Baserel]
i2)
    else do
      let (m :: BMap
m, t :: Table2
t) = [Baserel] -> (BMap, Table2)
makeTable [Baserel]
rs1
      ConTables
ctNew <- BMap -> Parser ConTables
parseConv BMap
m
      (i2 :: [Baserel]
i2, _) <- Parser ([Baserel], [Baserel])
parseIdBaOths
      (BMap, Table2, ConTables, [Baserel])
-> ParsecT String () Identity (BMap, Table2, ConTables, [Baserel])
forall (m :: * -> *) a. Monad m => a -> m a
return (BMap
m, Table2
t, ConTables
ctNew, [Baserel]
i1 [Baserel] -> [Baserel] -> [Baserel]
forall a. [a] -> [a] -> [a]
++ [Baserel]
i2)
  CmpTbl
compt <- BMap -> Parser CmpTbl
parseComTab BMap
m
  (i3 :: [Baserel]
i3, _) <- Parser ([Baserel], [Baserel])
parseIdBaOths
  case [Baserel]
i2 [Baserel] -> [Baserel] -> [Baserel]
forall a. [a] -> [a] -> [a]
++ [Baserel]
i3 of
    [i :: Baserel
i] -> Table2 -> Parser Table2
forall (m :: * -> *) a. Monad m => a -> m a
return (Table2 -> Parser Table2) -> Table2 -> Parser Table2
forall a b. (a -> b) -> a -> b
$ String
-> Int -> IntMap Baserel -> BSet -> CmpTbl -> ConTables -> Table2
Table2 String
calculusName (Baserel -> BMap -> Int
forall a. (Show a, Ord a) => a -> Map a Int -> Int
lkup Baserel
i BMap
m) IntMap Baserel
ns BSet
bs CmpTbl
compt ConTables
ct
    [] -> String -> Parser Table2
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "missing identity relation"
    is :: [Baserel]
is -> String -> Parser Table2
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Parser Table2) -> String -> Parser Table2
forall a b. (a -> b) -> a -> b
$ "non-unique identity relation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Baserel] -> String
forall a. Show a => a -> String
show [Baserel]
is

parseComTab :: BMap -> Parser CmpTbl
parseComTab :: BMap -> Parser CmpTbl
parseComTab m :: BMap
m = String -> Parser ()
cKey String
compositionOperationS
  Parser () -> Parser CmpTbl -> Parser CmpTbl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser CmpTbl -> Parser CmpTbl
forall a. Parser a -> Parser a
inParens (BMap -> Parser CmpTbl
parseComptab BMap
m)

parseComptab :: BMap -> Parser CmpTbl
parseComptab :: BMap -> Parser CmpTbl
parseComptab = ([(Int, Int, BSet)] -> CmpTbl)
-> ParsecT String () Identity [(Int, Int, BSet)] -> Parser CmpTbl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  ((CmpTbl -> (Int, Int, BSet) -> CmpTbl)
-> CmpTbl -> [(Int, Int, BSet)] -> CmpTbl
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ t :: CmpTbl
t (r1 :: Int
r1, r2 :: Int
r2, rs :: BSet
rs) ->
     (IntMap BSet -> IntMap BSet -> IntMap BSet)
-> Int -> IntMap BSet -> CmpTbl -> CmpTbl
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith IntMap BSet -> IntMap BSet -> IntMap BSet
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union Int
r1
       ((BSet -> BSet -> BSet) -> Int -> BSet -> IntMap BSet -> IntMap BSet
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith BSet -> BSet -> BSet
IntSet.union Int
r2 BSet
rs IntMap BSet
forall a. IntMap a
IntMap.empty) CmpTbl
t)
  CmpTbl
forall a. IntMap a
IntMap.empty)
  (ParsecT String () Identity [(Int, Int, BSet)] -> Parser CmpTbl)
-> (BMap -> ParsecT String () Identity [(Int, Int, BSet)])
-> BMap
-> Parser CmpTbl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT String () Identity (Int, Int, BSet)
-> ParsecT String () Identity [(Int, Int, BSet)]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String () Identity (Int, Int, BSet)
 -> ParsecT String () Identity [(Int, Int, BSet)])
-> (BMap -> ParsecT String () Identity (Int, Int, BSet))
-> BMap
-> ParsecT String () Identity [(Int, Int, BSet)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BMap -> ParsecT String () Identity (Int, Int, BSet)
parseComptabent

parseComptabent :: BMap -> Parser (Int, Int, IntSet.IntSet)
parseComptabent :: BMap -> ParsecT String () Identity (Int, Int, BSet)
parseComptabent m :: BMap
m = ParsecT String () Identity (Int, Int, BSet)
-> ParsecT String () Identity (Int, Int, BSet)
forall a. Parser a -> Parser a
inParens (ParsecT String () Identity (Int, Int, BSet)
 -> ParsecT String () Identity (Int, Int, BSet))
-> ParsecT String () Identity (Int, Int, BSet)
-> ParsecT String () Identity (Int, Int, BSet)
forall a b. (a -> b) -> a -> b
$ do
  Int
rel1 <- BMap -> Parser Int
parseRel BMap
m
  Int
rel2 <- BMap -> Parser Int
parseRel BMap
m
  BSet
results <- BMap -> Parser BSet
parseComptabres BMap
m
  (Int, Int, BSet) -> ParsecT String () Identity (Int, Int, BSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
rel1, Int
rel2, BSet
results)

parseComptabres :: BMap -> Parser IntSet.IntSet
parseComptabres :: BMap -> Parser BSet
parseComptabres m :: BMap
m =
  Parser BSet -> Parser BSet
forall a. Parser a -> Parser a
inParens (([Int] -> BSet) -> ParsecT String () Identity [Int] -> Parser BSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Int] -> BSet
IntSet.fromList (ParsecT String () Identity [Int] -> Parser BSet)
-> ParsecT String () Identity [Int] -> Parser BSet
forall a b. (a -> b) -> a -> b
$ Parser Int -> ParsecT String () Identity [Int]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (Parser Int -> ParsecT String () Identity [Int])
-> Parser Int -> ParsecT String () Identity [Int]
forall a b. (a -> b) -> a -> b
$ BMap -> Parser Int
parseRel BMap
m)
  Parser BSet -> Parser BSet -> Parser BSet
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    result :: Baserel
result@(Baserel str :: String
str) <- Parser Baserel
parseRelationId
    BSet -> Parser BSet
forall (m :: * -> *) a. Monad m => a -> m a
return (BSet -> Parser BSet) -> BSet -> Parser BSet
forall a b. (a -> b) -> a -> b
$ if (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
str String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "NIL" then BSet
IntSet.empty else
                 Int -> BSet
IntSet.singleton (Int -> BSet) -> Int -> BSet
forall a b. (a -> b) -> a -> b
$ Baserel -> BMap -> Int
forall a. (Show a, Ord a) => a -> Map a Int -> Int
lkup Baserel
result BMap
m

parseConv :: BMap -> Parser ConTables
parseConv :: BMap -> Parser ConTables
parseConv m :: BMap
m = let e :: IntMap a
e = IntMap a
forall a. IntMap a
IntMap.empty in do
    IntMap BSet
e1 <- BMap -> String -> Parser (IntMap BSet)
parseContab BMap
m String
inverseOperationS
    IntMap BSet
e2 <- BMap -> String -> Parser (IntMap BSet)
parseContab BMap
m String
shortcutOperationS
    IntMap BSet
e3 <- BMap -> String -> Parser (IntMap BSet)
parseContab BMap
m String
homingOperationS
    ConTables -> Parser ConTables
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap BSet
forall a. IntMap a
e, IntMap BSet
e1, IntMap BSet
e2, IntMap BSet
e3)
  Parser ConTables -> Parser ConTables -> Parser ConTables
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (IntMap BSet -> ConTables)
-> Parser (IntMap BSet) -> Parser ConTables
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ c :: IntMap BSet
c -> (IntMap BSet
c, IntMap BSet
forall a. IntMap a
e, IntMap BSet
forall a. IntMap a
e, IntMap BSet
forall a. IntMap a
e)) (BMap -> String -> Parser (IntMap BSet)
parseContab BMap
m String
converseOperationS)

parseContab :: BMap -> String -> Parser ConTable
parseContab :: BMap -> String -> Parser (IntMap BSet)
parseContab m :: BMap
m s :: String
s = String -> Parser ()
cKey String
s Parser () -> Parser (IntMap BSet) -> Parser (IntMap BSet)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser (IntMap BSet) -> Parser (IntMap BSet)
forall a. Parser a -> Parser a
inParens (([(Int, BSet)] -> IntMap BSet)
-> ParsecT String () Identity [(Int, BSet)] -> Parser (IntMap BSet)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  ((IntMap BSet -> (Int, BSet) -> IntMap BSet)
-> IntMap BSet -> [(Int, BSet)] -> IntMap BSet
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ t :: IntMap BSet
t (i :: Int
i, r :: BSet
r) -> (BSet -> BSet -> BSet) -> Int -> BSet -> IntMap BSet -> IntMap BSet
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith BSet -> BSet -> BSet
IntSet.union Int
i BSet
r IntMap BSet
t) IntMap BSet
forall a. IntMap a
IntMap.empty)
  (ParsecT String () Identity [(Int, BSet)] -> Parser (IntMap BSet))
-> (ParsecT String () Identity (Int, BSet)
    -> ParsecT String () Identity [(Int, BSet)])
-> ParsecT String () Identity (Int, BSet)
-> Parser (IntMap BSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParsecT String () Identity (Int, BSet)
-> ParsecT String () Identity [(Int, BSet)]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String () Identity (Int, BSet) -> Parser (IntMap BSet))
-> ParsecT String () Identity (Int, BSet) -> Parser (IntMap BSet)
forall a b. (a -> b) -> a -> b
$ BMap -> ParsecT String () Identity (Int, BSet)
parseContabent BMap
m)

parseContabent :: BMap -> Parser (Int, IntSet.IntSet)
parseContabent :: BMap -> ParsecT String () Identity (Int, BSet)
parseContabent m :: BMap
m = ParsecT String () Identity (Int, BSet)
-> ParsecT String () Identity (Int, BSet)
forall a. Parser a -> Parser a
inParens (ParsecT String () Identity (Int, BSet)
 -> ParsecT String () Identity (Int, BSet))
-> ParsecT String () Identity (Int, BSet)
-> ParsecT String () Identity (Int, BSet)
forall a b. (a -> b) -> a -> b
$
  Parser Int -> Parser BSet -> ParsecT String () Identity (Int, BSet)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (BMap -> Parser Int
parseRel BMap
m) (BMap -> Parser BSet
parseRelIds BMap
m Parser BSet -> Parser BSet -> Parser BSet
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser BSet -> Parser BSet
forall a. Parser a -> Parser a
inParens (BMap -> Parser BSet
parseRelIds BMap
m))

parseRelIds :: BMap -> Parser IntSet.IntSet
parseRelIds :: BMap -> Parser BSet
parseRelIds = ([Int] -> BSet) -> ParsecT String () Identity [Int] -> Parser BSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Int] -> BSet
IntSet.fromList (ParsecT String () Identity [Int] -> Parser BSet)
-> (BMap -> ParsecT String () Identity [Int])
-> BMap
-> Parser BSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Int -> ParsecT String () Identity [Int]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Int -> ParsecT String () Identity [Int])
-> (BMap -> Parser Int) -> BMap -> ParsecT String () Identity [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BMap -> Parser Int
parseRel

type BMap = Map.Map Baserel Int

parseRel :: BMap -> Parser Int
parseRel :: BMap -> Parser Int
parseRel m :: BMap
m = (Baserel -> Int) -> Parser Baserel -> Parser Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Baserel -> BMap -> Int
forall a. (Show a, Ord a) => a -> Map a Int -> Int
`lkup` BMap
m) Parser Baserel
parseRelationId