As.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./VSE/As.hs
Description :  abstract syntax of VSE programs and dynamic logic
Copyright   :  (c) C. Maeder, DFKI 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

CASL extention to VSE programs and dynamic logic
as described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
Bruno Langenstein's API description
-}

module VSE.As where

import Data.Char
import Data.Data
import qualified Data.Map as Map
import Control.Monad (foldM)

import Common.AS_Annotation
import Common.Id
import Common.Doc
import Common.DocUtils
import Common.Result
import Common.LibName
import Common.Utils (number)

import CASL.AS_Basic_CASL
import CASL.ToDoc

-- | input or output procedure parameter kind
data Paramkind = In | Out deriving (Show, Eq, Ord, Typeable, Data)

-- | a procedure parameter
data Procparam = Procparam Paramkind SORT
  deriving (Show, Eq, Ord, Typeable, Data)

-- | procedure or function declaration
data Profile = Profile [Procparam] (Maybe SORT)
  deriving (Show, Eq, Ord, Typeable, Data)

-- | further VSE signature entries
data Sigentry = Procedure Id Profile Range
  deriving (Show, Eq, Ord, Typeable, Data)

data Procdecls = Procdecls [Annoted Sigentry] Range
  deriving (Show, Eq, Ord, Typeable, Data)

instance GetRange Procdecls where
  getRange (Procdecls _ r) = r

-- | wrapper for positions
data Ranged a = Ranged { unRanged :: a, range :: Range }
  deriving (Show, Eq, Ord, Typeable, Data)

-- | attach a nullRange
mkRanged :: a -> Ranged a
mkRanged a = Ranged a nullRange

-- | programs with ranges
type Program = Ranged PlainProgram

-- | programs based on restricted terms and formulas
data PlainProgram =
    Abort
  | Skip
  | Assign VAR (TERM ())
  | Call (FORMULA ()) -- ^ a procedure call as predication
  | Return (TERM ())
  | Block [VAR_DECL] Program
  | Seq Program Program
  | If (FORMULA ()) Program Program
  | While (FORMULA ()) Program
    deriving (Show, Eq, Ord, Typeable, Data)

-- | alternative variable declaration
data VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range
  deriving (Show, Typeable, Data)

toVarDecl :: [VAR_DECL] -> [VarDecl]
toVarDecl = concatMap
  (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)

addInits :: [VarDecl] -> Program -> ([VarDecl], Program)
addInits vs p = case vs of
  vd@(VarDecl v s Nothing z) : r -> case unRanged p of
      Seq (Ranged (Assign av t) _) p2 | v == av
          -> let (rs, q) = addInits r p2
             in (VarDecl v s (Just t) z : rs, q)
      _ -> let (rs, q) = addInits r p
           in (vd : rs, q)
  _ -> (vs, p)

-- | extend CASL formulas by box or diamond formulas and defprocs
data VSEforms =
    Dlformula BoxOrDiamond Program Sentence
  | Defprocs [Defproc]
  | RestrictedConstraint [Constraint] (Map.Map SORT Id) Bool
    deriving (Show, Eq, Ord, Typeable, Data)

type Dlformula = Ranged VSEforms
type Sentence = FORMULA Dlformula

-- | box or diamond indicator
data BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord, Typeable, Data)

data ProcKind = Proc | Func deriving (Show, Eq, Ord, Typeable, Data)

-- | procedure definitions as basic items becoming sentences
data Defproc = Defproc ProcKind Id [VAR] Program Range
  deriving (Show, Eq, Ord, Typeable, Data)

data Procs = Procs { procsMap :: Map.Map Id Profile }
  deriving (Show, Eq, Ord, Typeable, Data)

emptyProcs :: Procs
emptyProcs = Procs Map.empty

unionProcs :: Procs -> Procs -> Result Procs
unionProcs (Procs m1) (Procs m2) = fmap Procs $
  foldM (\ m (k, v) -> case Map.lookup k m1 of
    Nothing -> return $ Map.insert k v m
    Just w -> if w == v then return m else
      mkError "different union profiles for" k)
  m1 $ Map.toList m2

interProcs :: Procs -> Procs -> Result Procs
interProcs (Procs m1) (Procs m2) = fmap Procs $
  foldM (\ m (k, v) -> case Map.lookup k m1 of
    Nothing -> return m
    Just w -> if w == v then return $ Map.insert k v m else
      mkError "different intersection profiles for" k)
    Map.empty $ Map.toList m2

diffProcs :: Procs -> Procs -> Procs
diffProcs (Procs m1) (Procs m2) = Procs $ Map.difference m1 m2

isSubProcsMap :: Procs -> Procs -> Bool
isSubProcsMap (Procs m1) (Procs m2) = Map.isSubmapOfBy (==) m1 m2

-- * Pretty instances

instance Pretty Profile where
  pretty (Profile ps ores) = fsep
    [ ppWithCommas ps
    , case ores of
        Nothing -> empty
        Just s -> funArrow <+> idDoc s]

instance Pretty Sigentry where
  pretty (Procedure i p _) = fsep [idDoc i, colon <+> pretty p]

instance Pretty Procdecls where
  pretty (Procdecls l _) = if null l then empty else fsep
   [ text $ "PROCEDURE" ++ case l of
        [_] -> ""
        _ -> "S"
   , semiAnnos pretty l ]

instance Pretty Procparam where
  pretty (Procparam m s) = text (map toUpper $ show m) <+> idDoc s

block :: Doc -> Doc
block d = sep [text "BEGIN", d, text "END"]

prettyProcKind :: ProcKind -> Doc
prettyProcKind k = text $ case k of
  Proc -> "PROCEDURE"
  Func -> "FUNCTION"

assign :: Doc
assign = text ":="

instance Pretty Defproc where
  pretty (Defproc pk p ps pr _) = vcat
    [ prettyProcKind pk <+> idDoc p <> parens (ppWithCommas ps)
    , pretty pr ]

instance Pretty a => Pretty (Ranged a) where
  pretty (Ranged a _) = pretty a

instance GetRange (Ranged a) where
  getRange (Ranged _ r) = r

instance FormExtension a => FormExtension (Ranged a) where
  isQuantifierLike (Ranged a _) = isQuantifierLike a

instance Pretty VarDecl where
  pretty (VarDecl v s mt _) =
      sidDoc v <+> colon <+> idDoc s <+> case mt of
      Nothing -> empty
      Just t -> assign <+> pretty t

instance Pretty PlainProgram where
  pretty prg = case prg of
    Abort -> text "ABORT"
    Skip -> text "SKIP"
    Assign v t -> pretty v <+> assign <+> pretty t
    Call f -> pretty f
    Return t -> text "RETURN" <+> pretty t
    Block vs p -> if null vs then block $ pretty p else
      let (vds, q) = addInits (toVarDecl vs) p
      in sep [ text "DECLARE"
             , ppWithCommas vds <> semi
             , pretty q ]
    Seq p1 p2 -> vcat [pretty p1 <> semi, pretty p2]
    If f t e -> sep
      [ text "IF" <+> pretty f
      , text "THEN" <+> pretty t
      , case e of
          Ranged Skip _ -> empty
          _ -> text "ELSE" <+> pretty e
      , text "FI" ]
    While f p -> sep
      [ text "WHILE" <+> pretty f
      , text "DO" <+> pretty p
      , text "OD" ]

instance FormExtension VSEforms

instance GetRange VSEforms

instance Pretty VSEforms where
  pretty v = case v of
    Dlformula b p f -> let d = pretty p in sep
      [ case b of
         Box -> text "[:" <> d <> text ":]"
         Diamond -> text "<:" <> d <> text ":>"
      , pretty f ]
    Defprocs ps -> prettyProcdefs ps
    RestrictedConstraint constrs restr _b ->
       let l = recoverType constrs
       in fsep [ text "true %[generated type"
               , semiAnnos (printRestrTypedecl restr) l
               , text "]%"]

genSortName :: String -> SORT -> Id
genSortName str s@(Id ts cs ps) = case cs of
  [] -> genName $ str ++ show s
  i : r | isQualName s -> Id ts (genSortName str i : r) ps
  _ -> Id [genToken $ str ++ show (Id ts [] ps)] cs ps

{- since such names are generated out of sentences, the qualification
   of the sort may be misleading -}
gnUniformName :: SORT -> Id
gnUniformName = genSortName "uniform_" . unQualName

gnRestrName :: SORT -> Id
gnRestrName = genSortName "restr_"

gnEqName :: SORT -> Id
gnEqName = genSortName "eq_"

genVars :: [SORT] -> [(Token, SORT)]
genVars = map (\ (t, n) -> (genNumVar "x" n, t)) . number

xVar :: Token
xVar = genToken "x"

yVar :: Token
yVar = genToken "y"

printRestrTypedecl :: Map.Map SORT Id -> DATATYPE_DECL -> Doc
printRestrTypedecl restr (Datatype_decl s a r) =
    let pa = printAnnoted printALTERNATIVE in case a of
    [] -> printRestrTypedecl restr
           (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)
    h : t -> sep [idLabelDoc s, colon <> colon <> sep
                      ((equals <+> pa h) :
                       map ((bar <+>) . pa) t), text "restricted by",
                   pretty $ Map.findWithDefault (gnRestrName s) s restr]

prettyProcdefs :: [Defproc] -> Doc
prettyProcdefs ps = vcat
  [ text "DEFPROCS"
  , vsep . punctuate semi $ map pretty ps
  , text "DEFPROCSEND" ]

instance Pretty Procs where
  pretty (Procs m) =
    pretty $ Procdecls
       (map (\ (i, p) -> emptyAnno $ Procedure i p nullRange) $ Map.toList m)
       nullRange