2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{- |

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule : $Header$

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederDescription : abstract syntax of VSE programs and dynamic logic

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCopyright : (c) C. Maeder, DFKI 2008

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuLicense : GPLv2 or higher, see LICENSE.txt

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : provisional

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : portable

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCASL extention to VSE programs and dynamic logic

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

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederBruno Langenstein's API description

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder-}

da955132262baab309a50fdffe228c9efe68251dCui Jian

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maedermodule VSE.As where

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Data.Char

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport qualified Data.Map as Map

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport Control.Monad (foldM)

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport Common.AS_Annotation

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport Common.Id

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Doc

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.DocUtils

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Result

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiimport Common.LibName

c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maederimport Common.Utils (number)

3c4e64e0b4361a24275ee8f308fa965ab1e52f2eHeng Jiang

fa388aea9cef5f9734fec346159899a74432ce26Christian Maederimport CASL.AS_Basic_CASL

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport CASL.ToDoc

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-- | input or output procedure parameter kind

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyerdata Paramkind = In | Out deriving (Show, Eq, Ord)

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder-- | a procedure parameter

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederdata Procparam = Procparam Paramkind SORT deriving (Show, Eq, Ord)

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning-- | procedure or function declaration

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederdata Profile = Profile [Procparam] (Maybe SORT) deriving (Show, Eq, Ord)

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross-- | further VSE signature entries

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederdata Sigentry = Procedure Id Profile Range deriving (Show, Eq)

a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederdata Procdecls = Procdecls [Annoted Sigentry] Range deriving (Show, Eq)

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Grossinstance GetRange Procdecls where

6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder getRange (Procdecls _ r) = r

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova-- | wrapper for positions

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulzdata Ranged a = Ranged { unRanged :: a, range :: Range }

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl deriving (Show, Eq, Ord)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder

2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder-- | attach a nullRange

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian MaedermkRanged :: a -> Ranged a

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus GrossmkRanged a = Ranged a nullRange

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross-- | programs with ranges

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grosstype Program = Ranged PlainProgram

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl-- | programs based on restricted terms and formulas

ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühldata PlainProgram =

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Abort

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Skip

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Assign VAR (TERM ())

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder | Call (FORMULA ()) -- ^ a procedure call as predication

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Return (TERM ())

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder | Block [VAR_DECL] Program

c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder | Seq Program Program

2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder | If (FORMULA ()) Program Program

fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder | While (FORMULA ()) Program

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder deriving (Show, Eq, Ord)

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder-- | alternative variable declaration

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederdata VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range deriving Show

923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl

9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina SojakovatoVarDecl :: [VAR_DECL] -> [VarDecl]

72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst SchulztoVarDecl = concatMap

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder

a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederaddInits :: [VarDecl] -> Program -> ([VarDecl], Program)

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian MaederaddInits vs p = case vs of

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder vd@(VarDecl v s Nothing z) : r -> case unRanged p of

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder Seq (Ranged (Assign av t) _) p2 | v == av

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder -> let (rs, q) = addInits r p2

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross in (VarDecl v s (Just t) z : rs, q)

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross _ -> let (rs, q) = addInits r p

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross in (vd : rs, q)

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder _ -> (vs, p)

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer-- | extend CASL formulas by box or diamond formulas and defprocs

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyerdata VSEforms =

f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettich Dlformula BoxOrDiamond Program Sentence

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer | Defprocs [Defproc]

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer | RestrictedConstraint [Constraint] (Map.Map SORT Id) Bool

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer deriving (Show, Eq, Ord)

d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maedertype Dlformula = Ranged VSEforms

type Sentence = FORMULA Dlformula

-- | box or diamond indicator

data BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord)

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

-- | procedure definitions as basic items becoming sentences

data Defproc = Defproc ProcKind Id [VAR] Program Range deriving (Show, Eq, Ord)

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

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 where

getRange _ = nullRange

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