076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{- |

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederModule : $Header$

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederDescription : abstract syntax of VSE programs and dynamic logic

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) C. Maeder, DFKI 2008

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederMaintainer : Christian.Maeder@dfki.de

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederCASL extention to VSE programs and dynamic logic

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederas described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian MaederBruno Langenstein's API description

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule VSE.As where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maederimport Data.Char

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maederimport Common.Id

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport Common.Doc

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Common.DocUtils

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport CASL.AS_Basic_CASL

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederimport CASL.ToDoc ()

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | further VSE signature entries

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Sigentry = Procedure Id [Procparam] Range deriving (Show, Eq)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | a procedure parameter

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Procparam = Procparam VAR Paramkind SORT deriving (Show, Eq, Ord)

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

6e5180855658f12f9059d9041f447bf0935de344Christian Maeder-- | input or output procedure parameter kind

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Paramkind = In | Out deriving (Show, Eq, Ord)

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | wrapper for positions

76647324ed70f33b95a881b536d883daccf9568dChristian Maederdata Ranged a = Ranged a Range deriving (Show, Eq, Ord)

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder-- | programs with ranges

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedertype Program = Ranged PlainProgram

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder-- | programs based on restricted terms and formulas

76647324ed70f33b95a881b536d883daccf9568dChristian Maederdata PlainProgram =

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder Abort

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder | Skip

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder | Assign VAR (TERM ())

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder | Block [VAR_DECL] Program

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder | Seq Program Program

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder | If (FORMULA ()) Program Program

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder | While (FORMULA ()) Program

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder | Call Id [TERM ()] -- ^ a procedure call

b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder deriving (Show, Eq, Ord)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder{- For functions a return is needed, but functions could be emulated

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederby an extra out parameter -}

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder{- vardecls do not consider initialization terms here as these may be

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederseens as initial assignments of the program block -}

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder-- | extend CASL formulas by box or diamond formulas

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Dlformula = Dlformula BoxOrDiamond Program (FORMULA Dlformula) Range

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder deriving (Show, Eq, Ord)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | box or diamond indicator

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder-- | procedure definitions as basic items becoming sentences

4be371b81d055e03a5946e4ec333613f313d689bChristian Maederdata Defproc = Defproc Id [Procparam] Program deriving (Show, Eq, Ord)

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder-- maybe CASL ops can be associated to programs as well

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | the sentences for the logic

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederdata Sentence =

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder FormulaSen Dlformula

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder | DefprocSen [Defproc]

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder deriving (Show, Eq, Ord)

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder{- formula kinds should be covered by Named Sentence -}

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

f0920567c5a918c34a69cdb6b56826ef49becfb5Christian Maeder-- * Pretty instances

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian MaederppWithSemis :: Pretty a => [a] -> Doc

ac510075311023bf24175f7a76b89ec2bbda0626Christian MaederppWithSemis = fsep .punctuate semi . map pretty

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederproc :: Doc

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederproc = text "PROCEDURE"

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederparams :: Doc -> Doc

76647324ed70f33b95a881b536d883daccf9568dChristian Maederparams = (text "PARAMS" <+>)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maederinstance Pretty Sigentry where

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder pretty (Procedure p ps _) = vcat

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder [ proc <+> idDoc p

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , if null ps then empty else params $ ppWithSemis ps ]

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

instance Pretty Procparam where

pretty (Procparam v m s) =

sidDoc v <+> colon <+> text (map toUpper $ show m) <+> idDoc s

block :: Doc -> Doc

block d = vcat [text "BEGIN", d, text "END"]

instance Pretty Defproc where

pretty (Defproc p ps pr) = vcat

[ proc <+> idDoc p

, if null ps then empty else

params $ ppWithSemis ps

, text "BODY" <+> pretty pr

, text "PROCEDUREEND"]

instance Pretty a => Pretty (Ranged a) where

pretty (Ranged a _) = pretty a

instance Pretty PlainProgram where

pretty prg = case prg of

Abort -> text "ABORT"

Skip -> text "SKIP"

Assign v t -> pretty v <+> text ":=" <+> pretty t

Block vs p -> block $ fsep [ppWithSemis vs, pretty p]

Seq p1 p2 -> vcat [pretty p1 <> semi, pretty p2]

If f t e -> vcat

[ text "IF" <+> pretty f

, text "THEN" <+> pretty t

, text "ELSE" <+> pretty e

, text "FI" ]

While f p -> vcat

[ text "WHILE" <+> pretty f

, text "DO" <+> pretty p

, text "OD" ]

Call p ts -> idDoc p <>

if null ts then empty else parens $ ppWithCommas ts

instance Pretty Dlformula where

pretty (Dlformula b p f _) = let d = pretty p in

(case b of

Box -> brackets d

Diamond -> less <> d <> greater)

<+> parens (pretty f)

instance Pretty Sentence where

pretty sen = case sen of

FormulaSen f -> pretty f

DefprocSen ps -> ppWithSemis ps