As.hs revision ac3ee7f6fc2e0b684e8a05485c9309b8eefb665d
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Header$
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : abstract syntax of VSE programs and dynamic logic
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) C. Maeder, DFKI 2008
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : Christian.Maeder@dfki.de
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCASL extention to VSE programs and dynamic logic
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederas described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederBruno Langenstein's API description
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | input or output procedure parameter kind
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Paramkind = In | Out deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | a procedure parameter
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata Procparam = Procparam Paramkind SORT deriving (Show, Eq, Ord)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-- | procedure or function declaration
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Profile = Profile [Procparam] (Maybe SORT) deriving (Show, Eq)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | further VSE signature entries
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata Sigentry = Procedure Id Profile Range deriving (Show, Eq)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Procdecls = Procdecls [Annoted Sigentry] Range deriving (Show, Eq)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | wrapper for positions
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata Ranged a = Ranged { unRanged :: a, range :: Range }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | programs with ranges
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedertype Program = Ranged PlainProgram
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- | programs based on restricted terms and formulas
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskidata PlainProgram =
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Assign VAR (TERM ())
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Call Id [TERM ()] -- ^ a procedure call
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Return (TERM ())
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Block [VAR_DECL] Program
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Seq Program Program
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | If (FORMULA ()) Program Program
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | While (FORMULA ()) Program
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Show, Eq, Ord)
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski-- | fold record
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata FoldRec a = FoldRec
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder { foldAbort :: Program -> a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , foldSkip :: Program -> a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , foldAssign :: Program -> VAR -> TERM () -> a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , foldCall :: Program -> Id -> [TERM ()] -> a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , foldReturn :: Program -> (TERM ()) -> a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , foldBlock :: Program -> [VAR_DECL] -> a -> a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , foldSeq :: Program -> a -> a -> a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , foldIf :: Program -> FORMULA () -> a -> a -> a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , foldWhile :: Program -> FORMULA () -> a -> a }
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | fold function
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederfoldProg :: FoldRec a -> Program -> a
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederfoldProg r p = case unRanged p of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Abort -> foldAbort r p
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Skip -> foldSkip r p
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Assign v t-> foldAssign r p v t
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Call i ts -> foldCall r p i ts
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Return t -> foldReturn r p t
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Block vs q -> foldBlock r p vs $ foldProg r q
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Seq p1 p2 -> foldSeq r p (foldProg r p1) $ foldProg r p2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder If f p1 p2 -> foldIf r p f (foldProg r p1) $ foldProg r p2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder While f q -> foldWhile r p f $ foldProg r q
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermapRec :: FoldRec Program
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermapRec = FoldRec
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder { foldAbort = id
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldSkip = id
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldAssign = \ (Ranged _ r) v t -> Ranged (Assign v t) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldCall = \ (Ranged _ r) i ts -> Ranged (Call i ts) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldReturn = \ (Ranged _ r) t -> Ranged (Return t) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldBlock = \ (Ranged _ r) vs p -> Ranged (Block vs p) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldSeq = \ (Ranged _ r) p1 p2 -> Ranged (Seq p1 p2) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldIf = \ (Ranged _ r) c p1 p2 -> Ranged (If c p1 p2) r
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski , foldWhile = \ (Ranged _ r) c p -> Ranged (While c p) r }
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | alternative variable declaration
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedertoVarDecl :: [VAR_DECL] -> [VarDecl]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedertoVarDecl = concatMap
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederaddInits :: [VarDecl] -> Program -> ([VarDecl], Program)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederaddInits vs p = case vs of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder vd@(VarDecl v s Nothing z) : r -> case unRanged p of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Seq (Ranged (Assign av t) _) p2 | v == av
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> let (rs, q) = addInits r p2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in (VarDecl v s (Just t) z : rs, q)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> let (rs, q) = addInits r p
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in (vd : rs, q)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | extend CASL formulas by box or diamond formulas and defprocs
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata VSEforms =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Dlformula BoxOrDiamond Program Sentence
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Defprocs [Defproc]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedertype Dlformula = Ranged VSEforms
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maedertype Sentence = FORMULA Dlformula
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | box or diamond indicator
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata ProcKind = Proc | Func deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- | procedure definitions as basic items becoming sentences
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata Defproc = Defproc ProcKind Id [VAR] Program Range deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- * Pretty instances
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Profile where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty (Profile ps ores) = fsep
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder [ ppWithCommas ps
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , case ores of
07baaf27fc0029203075ed916999006dcc619ef0Christian Maeder Nothing -> empty
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Just s -> funArrow <+> idDoc s]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Sigentry where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty (Procedure i p _) = fsep [idDoc i, colon <+> pretty p]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Procdecls where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty (Procdecls l _) = fsep
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [ text $ "PROCEDURE" ++ case l of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , semiAnnos pretty l ]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Procparam where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty (Procparam m s) = text (map toUpper $ show m) <+> idDoc s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederblock :: Doc -> Doc
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederblock d = sep [text "BEGIN", d, text "END"]
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederprettyProcKind :: ProcKind -> Doc
999f839e42d594e4ae288208fec398626837c41cTill MossakowskiprettyProcKind k = text $ case k of
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski Proc -> "PROCEDURE"
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski Func -> "FUNCTION"
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maederassign = text ":="
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowskiinstance Pretty Defproc where