As.hs revision 7868299829c1318b888152243ec2cea4f598b568
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescription : abstract syntax of VSE programs and dynamic logic
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) C. Maeder, DFKI 2008
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCASL extention to VSE programs and dynamic logic
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederas described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian MaederBruno Langenstein's API description
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport CASL.ToDoc (isJunct)
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski-- | input or output procedure parameter kind
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maederdata Paramkind = In | Out deriving (Show, Eq, Ord)
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski-- | a procedure parameter
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederdata Procparam = Procparam Paramkind SORT deriving (Show, Eq, Ord)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | procedure or function declaration
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata Profile = Profile [Procparam] (Maybe SORT) deriving (Show, Eq)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder-- | further VSE signature entries
8410667510a76409aca9bb24ff0eda0420088274Christian Maederdata Sigentry = Procedure Id Profile Range deriving (Show, Eq)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata Procdecls = Procdecls [Annoted Sigentry] Range deriving (Show, Eq)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- | wrapper for positions
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederdata Ranged a = Ranged { unRanged :: a, range :: Range }
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder deriving (Show, Eq, Ord)
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder-- | programs with ranges
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maedertype Program = Ranged PlainProgram
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | programs based on restricted terms and formulas
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederdata PlainProgram =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder | Assign VAR (TERM ())
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Call Id [TERM ()] -- ^ a procedure call
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder | Return (TERM ())
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder | Block [VAR_DECL] Program
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder | Seq Program Program
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder | If (FORMULA ()) Program Program
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder | While (FORMULA ()) Program
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder deriving (Show, Eq, Ord)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | fold record
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maederdata FoldRec a = FoldRec
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder { foldAbort :: Program -> a
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , foldSkip :: Program -> a
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , foldAssign :: Program -> VAR -> TERM () -> a
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder , foldCall :: Program -> Id -> [TERM ()] -> a
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder , foldReturn :: Program -> (TERM ()) -> a
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder , foldBlock :: Program -> [VAR_DECL] -> a -> a
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder , foldSeq :: Program -> a -> a -> a
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder , foldIf :: Program -> FORMULA () -> a -> a -> a
2c9df69accd8924e7cef3bf8f686626958499c7aChristian Maeder , foldWhile :: Program -> FORMULA () -> a -> a }
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | fold function
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian MaederfoldProg :: FoldRec a -> Program -> a
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian MaederfoldProg r p = case unRanged p of
4ed0007ac9caea5b468f202521352d153481423cChristian Maeder Abort -> foldAbort r p
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder Skip -> foldSkip r p
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder Assign v t-> foldAssign r p v t
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder Call i ts -> foldCall r p i ts
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder Return t -> foldReturn r p t
c2a4d8ae266aa37cc922eba97077520229a19902Christian Maeder Block vs q -> foldBlock r p vs $ foldProg r q
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder Seq p1 p2 -> foldSeq r p (foldProg r p1) $ foldProg r p2
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder If f p1 p2 -> foldIf r p f (foldProg r p1) $ foldProg r p2
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder While f q -> foldWhile r p f $ foldProg r q
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun WangmapRec :: FoldRec Program
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus LuettichmapRec = FoldRec
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus Luettich { foldAbort = id
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus Luettich , foldSkip = id
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich , foldAssign = \ (Ranged _ r) v t -> Ranged (Assign v t) r
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich , foldCall = \ (Ranged _ r) i ts -> Ranged (Call i ts) r
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich , foldReturn = \ (Ranged _ r) t -> Ranged (Return t) r
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang , foldBlock = \ (Ranged _ r) vs p -> Ranged (Block vs p) r
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder , foldSeq = \ (Ranged _ r) p1 p2 -> Ranged (Seq p1 p2) r
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , foldIf = \ (Ranged _ r) c p1 p2 -> Ranged (If c p1 p2) r
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder , foldWhile = \ (Ranged _ r) c p -> Ranged (While c p) r }
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder-- | alternative variable declaration
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichdata VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range deriving Show
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedertoVarDecl :: [VAR_DECL] -> [VarDecl]
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedertoVarDecl = concatMap
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederaddInits :: [VarDecl] -> Program -> ([VarDecl], Program)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederaddInits vs p = case vs of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder vd@(VarDecl v s Nothing z) : r -> case unRanged p of
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Seq (Ranged (Assign av t) _) p2 | v == av
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -> let (rs, q) = addInits r p2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder in (VarDecl v s (Just t) z : rs, q)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder _ -> let (rs, q) = addInits r p
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder in (vd : rs, q)
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang-- | extend CASL formulas by box or diamond formulas and defprocs
a6082d6cfdfbdc6a4e70430bb25638dfa4f0db9bHeng Jiangdata VSEforms =
a6082d6cfdfbdc6a4e70430bb25638dfa4f0db9bHeng Jiang Dlformula BoxOrDiamond Program Sentence
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder | Defprocs [Defproc]
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder deriving (Show, Eq, Ord)
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maedertype Dlformula = Ranged VSEforms
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maedertype Sentence = FORMULA Dlformula
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder-- | box or diamond indicator
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederdata BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederdata ProcKind = Proc | Func deriving (Show, Eq, Ord)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | procedure definitions as basic items becoming sentences
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata Defproc = Defproc ProcKind Id [VAR] Program Range deriving (Show, Eq, Ord)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- * Pretty instances
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederinstance Pretty Profile where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder pretty (Profile ps ores) = fsep
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [ ppWithCommas ps
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder , case ores of
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian Maeder Nothing -> empty
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just s -> funArrow <+> idDoc s]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Pretty Sigentry where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder pretty (Procedure i p _) = fsep [idDoc i, colon <+> pretty p]
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maederinstance Pretty Procdecls where
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder pretty (Procdecls l _) = fsep
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder [ text $ "PROCEDURE" ++ case l of
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder , semiAnnos pretty l ]
2d130d212db7208777ca896a7ecad619a8944971Christian Maederinstance Pretty Procparam where
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder pretty (Procparam m s) = text (map toUpper $ show m) <+> idDoc s
2d130d212db7208777ca896a7ecad619a8944971Christian Maederblock :: Doc -> Doc
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederblock d = sep [text "BEGIN", d, text "END"]
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian MaederprettyProcKind :: ProcKind -> Doc
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederprettyProcKind k = text $ case k of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Proc -> "PROCEDURE"
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder Func -> "FUNCTION"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederassign = text ":="
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Pretty Defproc where
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder pretty (Defproc pk p ps pr _) = vcat
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [ prettyProcKind pk <+> idDoc p <> parens (ppWithCommas ps)
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder , pretty pr ]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Pretty a => Pretty (Ranged a) where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder pretty (Ranged a _) = pretty a
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederinstance Pretty VarDecl where
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder pretty (VarDecl v s mt _) =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sidDoc v <+> colon <+> idDoc s <+> case mt of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> empty
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just t -> assign <+> pretty t
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederinstance Pretty PlainProgram where
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder pretty prg = case prg of
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder Abort -> text "ABORT"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Skip -> text "SKIP"
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich Assign v t -> pretty v <+> assign <+> pretty t
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Call p ts -> idDoc p <>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if null ts then empty else parens $ ppWithCommas ts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Return t -> text "RETURN" <+> pretty t
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Block vs p -> if null vs then block $ pretty p else
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder let (vds, q) = addInits (toVarDecl vs) p
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder in sep [ text "DECLARE"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder , ppWithCommas vds <> semi
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Seq p1 p2 -> vcat [pretty p1 <> semi, pretty p2]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder If f t e -> sep
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [ text "IF" <+> pretty f
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , text "THEN" <+> pretty t
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , text "ELSE" <+> pretty e
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , text "FI" ]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder While f p -> sep
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder [ text "WHILE" <+> pretty f
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , text "DO" <+> pretty p
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , text "OD" ]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederinstance Pretty VSEforms where
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder pretty v = case v of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Dlformula b p f -> let d = pretty p in
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Box -> text "[:" <> d <> text ":]"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Diamond -> text "<:" <> d <> text ":>")
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder <+> (if isJunct f then parens else id) (pretty f)
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Defprocs ps -> prettyProcdefs ps
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederprettyProcdefs :: [Defproc] -> Doc
363939beade943a02b31004cea09dec34fa8a6d9Christian MaederprettyProcdefs ps = vcat
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder [ text "DEFPROCS"
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich , vsep . punctuate semi $ map pretty ps
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , text "DEFPROCSEND" ]