{- |
Module      :  ./Common/Amalgamate.hs
Description :  data types for amalgamability options and analysis
Copyright   :  (c) Christian Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

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

Data types for amalgamability options and analysis

-}

module Common.Amalgamate where

import Data.Char
import Data.List

{- | 'CASLAmalgOpt' describes the options for CASL amalgamability analysis
     algorithms -}

data CASLAmalgOpt = Sharing         -- ^ perform the sharing checks
    | ColimitThinness -- ^ perform colimit thinness check (implies Sharing)
    | Cell            -- ^ perform cell condition check (implies Sharing)
    | NoAnalysis      -- ^ dummy option to indicate empty option string

{- | Amalgamability analysis might be undecidable, so we need
a special type for the result of ensures_amalgamability -}
data Amalgamates = Amalgamates
                 | NoAmalgamation String       -- ^ failure description
                 | DontKnow String           {- ^ the reason for unknown status
The default value for 'DontKnow' amalgamability result -}
defaultDontKnow :: Amalgamates
defaultDontKnow :: Amalgamates
defaultDontKnow = String -> Amalgamates
DontKnow "Unable to assert that amalgamability is ensured"

instance Show CASLAmalgOpt where
    show :: CASLAmalgOpt -> String
show o :: CASLAmalgOpt
o = case CASLAmalgOpt
o of
             Sharing -> "sharing"
             ColimitThinness -> "colimit-thinness"
             Cell -> "cell"
             NoAnalysis -> "none"

instance Read CASLAmalgOpt where
    readsPrec :: Int -> ReadS CASLAmalgOpt
readsPrec _ = [CASLAmalgOpt] -> ReadS CASLAmalgOpt
forall a. Show a => [a] -> ReadS a
readShow [CASLAmalgOpt]
caslAmalgOpts

-- | test all possible values, ignore leading space
readShowAux :: [(String, a)] -> ReadS a
readShowAux :: [(String, a)] -> ReadS a
readShowAux l :: [(String, a)]
l s :: String
s =
    let s' :: String
s' = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
s
        f :: (a -> Maybe b) -> [a] -> Maybe (a, b)
f _ [] = Maybe (a, b)
forall a. Maybe a
Nothing
        f g' :: a -> Maybe b
g' (x :: a
x : xs :: [a]
xs) = case a -> Maybe b
g' a
x of
                         Just res :: b
res -> (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
x, b
res)
                         _ -> (a -> Maybe b) -> [a] -> Maybe (a, b)
f a -> Maybe b
g' [a]
xs
        g :: (String, b) -> Maybe String
g (p :: String
p, _) = String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
p String
s'
    in case ((String, a) -> Maybe String)
-> [(String, a)] -> Maybe ((String, a), String)
forall a b. (a -> Maybe b) -> [a] -> Maybe (a, b)
f (String, a) -> Maybe String
forall b. (String, b) -> Maybe String
g [(String, a)]
l of
         Nothing -> []
         Just ((_, t :: a
t), s'' :: String
s'') -> [(a
t, String
s'')]

-- | input all possible values and read one as it is shown
readShow :: Show a => [a] -> ReadS a
readShow :: [a] -> ReadS a
readShow = [(String, a)] -> ReadS a
forall a. [(String, a)] -> ReadS a
readShowAux ([(String, a)] -> ReadS a)
-> ([a] -> [(String, a)]) -> [a] -> ReadS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (String, a)) -> [a] -> [(String, a)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: a
o -> (a -> String
forall a. Show a => a -> String
show a
o, a
o))

-- | possible CASL amalgamability options
caslAmalgOpts :: [CASLAmalgOpt]
caslAmalgOpts :: [CASLAmalgOpt]
caslAmalgOpts = [CASLAmalgOpt
NoAnalysis, CASLAmalgOpt
Sharing, CASLAmalgOpt
Cell, CASLAmalgOpt
ColimitThinness]