content: {-# 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
  