{- |
Module      :  ./Modal/Utils.hs
Copyright   :  (c) (c) Klaus Luettich and Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

-}

module Modal.Utils where

import Common.Id
import Common.AS_Annotation

-- CASL
import CASL.AS_Basic_CASL

-- ModalCASL
import Modal.AS_Modal
import Data.Maybe

getModTermSort :: Id -> Id
getModTermSort :: Id -> Id
getModTermSort rs :: Id
rs = case Id
rs of
    Id _ [s :: Id
s] _ -> Id
s
    _ -> [Char] -> Id
forall a. HasCallStack => [Char] -> a
error "Modal.Utils.getModTermSort"

addNonEmptyLabel :: String -> Maybe (Named a) -> Maybe (Named a)
addNonEmptyLabel :: [Char] -> Maybe (Named a) -> Maybe (Named a)
addNonEmptyLabel _ Nothing = Maybe (Named a)
forall a. Maybe a
Nothing
addNonEmptyLabel l :: [Char]
l (Just s :: Named a
s)
    | [Char] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
l = Named a -> Maybe (Named a)
forall a. a -> Maybe a
Just Named a
s
    | Bool
otherwise = Named a -> Maybe (Named a)
forall a. a -> Maybe a
Just (Named a -> Maybe (Named a)) -> Named a -> Maybe (Named a)
forall a b. (a -> b) -> a -> b
$ ([Char] -> [Char]) -> Named a -> Named a
forall a b s. (a -> b) -> SenAttr s a -> SenAttr s b
reName ([Char] -> [Char] -> [Char]
forall a b. a -> b -> a
const [Char]
l) Named a
s

modToTerm :: MODALITY -> Maybe (TERM M_FORMULA)
modToTerm :: MODALITY -> Maybe (TERM M_FORMULA)
modToTerm (Simple_mod _) = Maybe (TERM M_FORMULA)
forall a. Maybe a
Nothing
modToTerm (Term_mod t :: TERM M_FORMULA
t) = TERM M_FORMULA -> Maybe (TERM M_FORMULA)
forall a. a -> Maybe a
Just TERM M_FORMULA
t

addTerm :: ([VAR] -> TERM M_FORMULA -> TERM ())
        -> PRED_NAME -> [Maybe (TERM M_FORMULA)] -> [VAR]
        -> Maybe (Named CASLFORMULA) -> Maybe (Named CASLFORMULA)
addTerm :: ([VAR] -> TERM M_FORMULA -> TERM ())
-> Id
-> [Maybe (TERM M_FORMULA)]
-> [VAR]
-> Maybe (Named CASLFORMULA)
-> Maybe (Named CASLFORMULA)
addTerm _ _ mTerms :: [Maybe (TERM M_FORMULA)]
mTerms _ nCaslFrm :: Maybe (Named CASLFORMULA)
nCaslFrm
    | [TERM M_FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Maybe (TERM M_FORMULA)] -> [TERM M_FORMULA]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (TERM M_FORMULA)]
mTerms) = Maybe (Named CASLFORMULA)
nCaslFrm
    | Bool
otherwise = Maybe (Named CASLFORMULA)
nCaslFrm -- Term-Modalities not correctly treated yet

{- - run with a State across formula
   - substitute in a nice manna the Terms into the relation symbols

incomplete code:
           Predication pn as qs ->
               let term' = mapT vars term
                   (pn',as') =
                       case pn of
                       Pred_name _ -> error "Modal2CASL: untyped predication"
                       Qual_pred_name prn pType@(Pred_type sorts pps) ps
                            | prn == rel ->
                                 (Qual_pred_name prn
                                          (Pred_type (getModTermSort prn:sorts)
                                                     pps) ps,
                                       term':as)
                            | otherwise -> (pn,as)
               in Predication pn' as' qs
-}