1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./VSE/As.hs
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederDescription : abstract syntax of VSE programs and dynamic logic
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederCopyright : (c) C. Maeder, DFKI 2008
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederMaintainer : Christian.Maeder@dfki.de
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederStability : provisional
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederPortability : portable
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederCASL extention to VSE programs and dynamic logic
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederas described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederBruno Langenstein's API description
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-}
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maedermodule VSE.As where
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederimport Data.Char
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Data.Data
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maederimport qualified Data.Map as Map
32562a567baac248a00782d2727716c13117dc4aChristian Maederimport Control.Monad (foldM)
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederimport Common.AS_Annotation
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederimport Common.Id
0243238805d31e597195ef974e8e7eccb587a390Christian Maederimport Common.Doc
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederimport Common.DocUtils
32562a567baac248a00782d2727716c13117dc4aChristian Maederimport Common.Result
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maederimport Common.LibName
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maederimport Common.Utils (number)
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederimport CASL.AS_Basic_CASL
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederimport CASL.ToDoc
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder-- | input or output procedure parameter kind
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Paramkind = In | Out deriving (Show, Eq, Ord, Typeable, Data)
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder-- | a procedure parameter
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Procparam = Procparam Paramkind SORT
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder-- | procedure or function declaration
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Profile = Profile [Procparam] (Maybe SORT)
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | further VSE signature entries
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Sigentry = Procedure Id Profile Range
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Procdecls = Procdecls [Annoted Sigentry] Range
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maederinstance GetRange Procdecls where
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder getRange (Procdecls _ r) = r
d2e1ea7e00412ba6a7c29b491e6fca6ca4d6fb18Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | wrapper for positions
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederdata Ranged a = Ranged { unRanged :: a, range :: Range }
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder-- | attach a nullRange
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian MaedermkRanged :: a -> Ranged a
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian MaedermkRanged a = Ranged a nullRange
7bcc3181abc49d4327cfdd4f3d98ee9522f4243eChristian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | programs with ranges
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maedertype Program = Ranged PlainProgram
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | programs based on restricted terms and formulas
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maederdata PlainProgram =
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Abort
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | Skip
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | Assign VAR (TERM ())
dcf7a9c571e15547fd5302de8064663a486c26faChristian Maeder | Call (FORMULA ()) -- ^ a procedure call as predication
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder | Return (TERM ())
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | Block [VAR_DECL] Program
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | Seq Program Program
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | If (FORMULA ()) Program Program
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder | While (FORMULA ()) Program
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder-- | alternative variable declaration
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedertoVarDecl :: [VAR_DECL] -> [VarDecl]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaedertoVarDecl = concatMap
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (\ (Var_decl vs s r) -> map (\ v -> VarDecl v s Nothing r) vs)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederaddInits :: [VarDecl] -> Program -> ([VarDecl], Program)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederaddInits vs p = case vs of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder vd@(VarDecl v s Nothing z) : r -> case unRanged p of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Seq (Ranged (Assign av t) _) p2 | v == av
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -> let (rs, q) = addInits r p2
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder in (VarDecl v s (Just t) z : rs, q)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder _ -> let (rs, q) = addInits r p
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder in (vd : rs, q)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder _ -> (vs, p)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder-- | extend CASL formulas by box or diamond formulas and defprocs
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maederdata VSEforms =
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder Dlformula BoxOrDiamond Program Sentence
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder | Defprocs [Defproc]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder | RestrictedConstraint [Constraint] (Map.Map SORT Id) Bool
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maedertype Dlformula = Ranged VSEforms
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maedertype Sentence = FORMULA Dlformula
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | box or diamond indicator
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata BoxOrDiamond = Box | Diamond deriving (Show, Eq, Ord, Typeable, Data)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata ProcKind = Proc | Func deriving (Show, Eq, Ord, Typeable, Data)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- | procedure definitions as basic items becoming sentences
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Defproc = Defproc ProcKind Id [VAR] Program Range
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata Procs = Procs { procsMap :: Map.Map Id Profile }
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederemptyProcs :: Procs
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederemptyProcs = Procs Map.empty
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
32562a567baac248a00782d2727716c13117dc4aChristian MaederunionProcs :: Procs -> Procs -> Result Procs
32562a567baac248a00782d2727716c13117dc4aChristian MaederunionProcs (Procs m1) (Procs m2) = fmap Procs $
32562a567baac248a00782d2727716c13117dc4aChristian Maeder foldM (\ m (k, v) -> case Map.lookup k m1 of
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Nothing -> return $ Map.insert k v m
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Just w -> if w == v then return m else
32562a567baac248a00782d2727716c13117dc4aChristian Maeder mkError "different union profiles for" k)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder m1 $ Map.toList m2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder
32562a567baac248a00782d2727716c13117dc4aChristian MaederinterProcs :: Procs -> Procs -> Result Procs
32562a567baac248a00782d2727716c13117dc4aChristian MaederinterProcs (Procs m1) (Procs m2) = fmap Procs $
32562a567baac248a00782d2727716c13117dc4aChristian Maeder foldM (\ m (k, v) -> case Map.lookup k m1 of
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Nothing -> return m
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Just w -> if w == v then return $ Map.insert k v m else
32562a567baac248a00782d2727716c13117dc4aChristian Maeder mkError "different intersection profiles for" k)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder Map.empty $ Map.toList m2
57a32fb13a6acc1748bb1c68028cb2382d6bdb3fChristian Maeder
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederdiffProcs :: Procs -> Procs -> Procs
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederdiffProcs (Procs m1) (Procs m2) = Procs $ Map.difference m1 m2
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian MaederisSubProcsMap :: Procs -> Procs -> Bool
32562a567baac248a00782d2727716c13117dc4aChristian MaederisSubProcsMap (Procs m1) (Procs m2) = Map.isSubmapOfBy (==) m1 m2
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder-- * Pretty instances
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Pretty Profile where
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder pretty (Profile ps ores) = fsep
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder [ ppWithCommas ps
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder , case ores of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> empty
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just s -> funArrow <+> idDoc s]
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance Pretty Sigentry where
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder pretty (Procedure i p _) = fsep [idDoc i, colon <+> pretty p]
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Pretty Procdecls where
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder pretty (Procdecls l _) = if null l then empty else fsep
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder [ text $ "PROCEDURE" ++ case l of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder [_] -> ""
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder _ -> "S"
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder , semiAnnos pretty l ]
e68cfdc781c4fd65d42f99173efc2aef342ce0eeChristian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Pretty Procparam where
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder pretty (Procparam m s) = text (map toUpper $ show m) <+> idDoc s
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederblock :: Doc -> Doc
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maederblock d = sep [text "BEGIN", d, text "END"]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederprettyProcKind :: ProcKind -> Doc
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederprettyProcKind k = text $ case k of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Proc -> "PROCEDURE"
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Func -> "FUNCTION"
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederassign :: Doc
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederassign = text ":="
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance Pretty Defproc where
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder pretty (Defproc pk p ps pr _) = vcat
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder [ prettyProcKind pk <+> idDoc p <> parens (ppWithCommas ps)
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder , pretty pr ]
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance Pretty a => Pretty (Ranged a) where
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder pretty (Ranged a _) = pretty a
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance GetRange (Ranged a) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder getRange (Ranged _ r) = r
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension a => FormExtension (Ranged a) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder isQuantifierLike (Ranged a _) = isQuantifierLike a
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maederinstance Pretty VarDecl where
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder pretty (VarDecl v s mt _) =
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder sidDoc v <+> colon <+> idDoc s <+> case mt of
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Nothing -> empty
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Just t -> assign <+> pretty t
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
0243238805d31e597195ef974e8e7eccb587a390Christian Maederinstance Pretty PlainProgram where
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder pretty prg = case prg of
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder Abort -> text "ABORT"
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder Skip -> text "SKIP"
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Assign v t -> pretty v <+> assign <+> pretty t
dcf7a9c571e15547fd5302de8064663a486c26faChristian Maeder Call f -> pretty f
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder Return t -> text "RETURN" <+> pretty t
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder Block vs p -> if null vs then block $ pretty p else
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder let (vds, q) = addInits (toVarDecl vs) p
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder in sep [ text "DECLARE"
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder , ppWithCommas vds <> semi
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder , pretty q ]
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder Seq p1 p2 -> vcat [pretty p1 <> semi, pretty p2]
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder If f t e -> sep
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder [ text "IF" <+> pretty f
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder , text "THEN" <+> pretty t
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder , case e of
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder Ranged Skip _ -> empty
0a757184b9336a91b2ba735dd58c5ed4e4378e51Christian Maeder _ -> text "ELSE" <+> pretty e
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder , text "FI" ]
4eeeca8e688ff5fb58bad5610d12f3f7a9866e85Christian Maeder While f p -> sep
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder [ text "WHILE" <+> pretty f
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder , text "DO" <+> pretty p
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder , text "OD" ]
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension VSEforms
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder
8526922fb6f17657dfc0e89c01306d3d18a8e1ceChristian Maederinstance GetRange VSEforms
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maederinstance Pretty VSEforms where
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder pretty v = case v of
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder Dlformula b p f -> let d = pretty p in sep
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder [ case b of
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder Box -> text "[:" <> d <> text ":]"
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder Diamond -> text "<:" <> d <> text ":>"
ac3ee7f6fc2e0b684e8a05485c9309b8eefb665dChristian Maeder , pretty f ]
6e0d665ee3ea887134ce2d54431fb25568a702e4Christian Maeder Defprocs ps -> prettyProcdefs ps
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu RestrictedConstraint constrs restr _b ->
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder let l = recoverType constrs
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder in fsep [ text "true %[generated type"
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder , semiAnnos (printRestrTypedecl restr) l
2dbb344c4f3fe8f3b9c49db7f95f851d0472c2b2Christian Maeder , text "]%"]
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedergenSortName :: String -> SORT -> Id
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedergenSortName str s@(Id ts cs ps) = case cs of
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder [] -> genName $ str ++ show s
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder i : r | isQualName s -> Id ts (genSortName str i : r) ps
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder _ -> Id [genToken $ str ++ show (Id ts [] ps)] cs ps
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder{- since such names are generated out of sentences, the qualification
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian Maeder of the sort may be misleading -}
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaedergnUniformName :: SORT -> Id
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedergnUniformName = genSortName "uniform_" . unQualName
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaedergnRestrName :: SORT -> Id
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedergnRestrName = genSortName "restr_"
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian MaedergnEqName :: SORT -> Id
5dc46f6d0fdd8747d730f9e79a93978145ed43bbChristian MaedergnEqName = genSortName "eq_"
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaedergenVars :: [SORT] -> [(Token, SORT)]
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian MaedergenVars = map (\ (t, n) -> (genNumVar "x" n, t)) . number
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederxVar :: Token
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederxVar = genToken "x"
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederyVar :: Token
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaederyVar = genToken "y"
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian MaederprintRestrTypedecl :: Map.Map SORT Id -> DATATYPE_DECL -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintRestrTypedecl restr (Datatype_decl s a r) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu let pa = printAnnoted printALTERNATIVE in case a of
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder [] -> printRestrTypedecl restr
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder h : t -> sep [idLabelDoc s, colon <> colon <> sep
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu ((equals <+> pa h) :
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu map ((bar <+>) . pa) t), text "restricted by",
b5dec828644f9f441c6d5dc38325ac6332b6eef7Christian Maeder pretty $ Map.findWithDefault (gnRestrName s) s restr]
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederprettyProcdefs :: [Defproc] -> Doc
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederprettyProcdefs ps = vcat
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder [ text "DEFPROCS"
904efdc72d29946a966c65fcc624068f38127c84Christian Maeder , vsep . punctuate semi $ map pretty ps
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder , text "DEFPROCSEND" ]
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maederinstance Pretty Procs where
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder pretty (Procs m) =
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder pretty $ Procdecls
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder (map (\ (i, p) -> emptyAnno $ Procedure i p nullRange) $ Map.toList m)
e59da4ae089bcbbdc655bae5b00d57703dc96bb4Christian Maeder nullRange