content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CSL/Sign.hs
  Description :  Signatures for the EnCL logic
  Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  dominik.dietrich@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  Types and functions for EnCL logic signatures
  -}
  
  module CSL.Sign
      ( Sign (Sign)                   -- EnCL Signatures
      , opIds
      , OpType (..)                   -- Operator Information attached to ids
      , pretty                        -- pretty printing
      , isLegalSignature              -- is a signature ok?
      , addToSig                      -- adds an id to the given Signature
      , unite                         -- union of signatures
      , emptySig                      -- empty signature
      , isSubSigOf                    -- is subsiganture?
      , sigDiff                       -- Difference of Signatures
      , sigUnion                      -- Union for Logic.Logic
      , lookupSym
      , optypeFromArity
      , addEPDefValToSig
      , addEPDeclToSig
      , addEPDomVarDeclToSig
      ) where
  
  import Data.Data
  import Data.Maybe
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import Common.Id
  import Common.Result
  import Common.Doc
  import Common.DocUtils
  
  import CSL.TreePO (ClosedInterval (ClosedInterval))
  import CSL.AS_BASIC_CSL
  import CSL.Print_AS ()
  
  data OpType = OpType { opArity :: Int
                       } deriving (Show, Eq, Ord, Typeable, Data)
  
  defaultType :: OpType
  defaultType = OpType { opArity = 0 }
  
  optypeFromArity :: Int -> OpType
  optypeFromArity i = defaultType { opArity = i }
  
  {- | Datatype for EnCL Signatures
  Signatures are just sets of Tokens for the operators -}
  data Sign = Sign { items :: Map.Map Token OpType
                   , epvars :: Map.Map Token (Maybe APInt)
                   , epdecls :: Map.Map Token EPDecl
                   } deriving (Show, Eq, Ord, Typeable, Data)
  
  opIds :: Sign -> Set.Set Id
  opIds = Set.map simpleIdToId . Map.keysSet . items
  
  -- | The empty signature, use this one to create new signatures
  emptySig :: Sign
  emptySig = Sign { items = Map.empty
                  , epvars = Map.empty
                  , epdecls = Map.empty
                  }
  
  instance Pretty Sign where
      pretty = printSign
  
  -- | pretty printer for EnCL signatures
  printSign :: Sign -> Doc
  printSign s = vcat [ printEPVars $ Map.toList $ epvars s
                     , printEPDecls $ Map.elems $ epdecls s]
  
  printEPVars :: [(Token, Maybe APInt)] -> Doc
  printEPVars [] = empty
  printEPVars l = hsep [text "set", sepBySemis $ map f l] where
      f (x, Nothing) = pretty x
      f (x, Just y) = hcat [pretty x, text "=", pretty y]
  
  printEPDecls :: [EPDecl] -> Doc
  printEPDecls l = vcat $ map f l where
      f x = hsep [text "ep", pretty x]
  
  
  -- | checks whether a Id is declared in the signature
  lookupSym :: Sign -> Id -> Bool
  lookupSym sig item = Map.member (idToSimpleId item) $ items sig
  
  -- TODO: adapt the operations to new signature components
  
  
  -- | determines whether a signature is valid. all sets are ok, so glued to true
  isLegalSignature :: Sign -> Bool
  isLegalSignature _ = True
  
  -- | Basic function to extend a given signature by adding an item (id) to it
  addToSig :: Sign -> Token -> OpType -> Sign
  addToSig sig tok ot = sig {items = Map.insert tok ot $ items sig}
  
  
  addEPDefValToSig :: Sign -> Token -> APInt -> Sign
  addEPDefValToSig sig tok i
      | isNothing mD = error $ "addEPDefValToSig: The extended parameter"
                        ++ " declaration for " ++ show tok ++ " is missing"
      | otherwise = sig {epdecls = ed'}
      where (mD, ed') = Map.insertLookupWithKey f tok err $ epdecls sig
            err = error "addEPDefValToSig: dummyval"
            f _ _ (EPDecl _ dom Nothing) = EPDecl tok dom $ Just i
            f _ _ (EPDecl _ _ (Just j)) =
                error $ "addEPDefValToSig: default value already set to "
                          ++ show j
  
  addEmptyEPDomVarDeclToSig :: Sign -> Token -> Sign
  addEmptyEPDomVarDeclToSig sig tok = sig {epvars = ev'}
      where ev' = Map.insertWith f tok Nothing $ epvars sig
            f _ v = v
  
  addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign
  addEPDomVarDeclToSig sig tok i = sig {epvars = ev'}
      where ev' = Map.insertWith f tok (Just i) $ epvars sig
            f _ (Just x)
                | x == i = error $ "addEPDomVarDeclToSig: equal values for "
                           ++ show tok
                | otherwise = error $ "addEPDomVarDeclToSig: variable already"
                              ++ " set to different value " ++ show tok ++ "="
                              ++ show x
            f n _ = n
  
  {- | Adds an extended parameter declaration for a given domain and
  eventually implicitly defined EP domain vars, e.g., for 'I = [0, n]'
  'n' is implicitly added -}
  addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign
  addEPDeclToSig sig tok dom = g $ sig {epdecls = ed'}
      where (mD, ed') = Map.insertLookupWithKey f tok epd $ epdecls sig
            epd = EPDecl tok dom Nothing
            f _ _ v@(EPDecl _ dom' _)
                | dom' == dom = v
                | otherwise = error $ "addEPDeclToSig: EP already"
                              ++ " assigned another domain: " ++ show tok ++ "in"
                              ++ show dom'
            g s =
                case (mD, dom) of
                  (Nothing, ClosedInterval a b) ->
                      case mapMaybe getEPVarRef [a, b] of
                        [] -> s
                        l -> foldl addEmptyEPDomVarDeclToSig s l
                  _ -> s
  
  
  -- TODO: add support for epdecls and report errors if they do not match!
  
  {- Two signatures s1 and s2 are compatible if the common part has the
     following properties:
  
     * if the default value of an extparam is defined in s1 and s2 it has to be the same
     * if the domains (of extparams or vars) are both given, they must not be disjoint
     * the arities must conincide for the same operator
  
  -}
  
  -- | Union of signatures
  unite :: Sign -> Sign -> Sign
  unite sig1 sig2 =
      sig1 { items = Map.union (items sig1) $ items sig2
           }
  
  -- | Determines if sig1 is subsignature of sig2
  isSubSigOf :: Sign -> Sign -> Bool
  isSubSigOf sig1 sig2 = Map.isSubmapOf (items sig1) $ items sig2
  
  -- | difference of Signatures
  sigDiff :: Sign -> Sign -> Sign
  sigDiff sig1 sig2 = sig1 {items = Map.difference (items sig1) $ items sig2}
  
  {- | union of Signatures
  or do I have to care about more things here? -}
  sigUnion :: Sign -> Sign -> Result Sign
  sigUnion s1 = Result [Diag Debug "All fine sigUnion" nullRange]
      . Just . unite s1
  