As.der.hs revision 118b1dee4954776d7fae2e4b0c93fec07f88133e
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : abstract syntax for FPL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : Christian.Maeder@dfki.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederabstract syntax for FPL, logic for functional programs
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederas CASL extension
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule Fpl.As where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- DrIFT command
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-! global: GetRange !-}
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.AS_Annotation
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Common.AnnoState
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Doc as Doc
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.DocUtils
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport Common.Id
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Common.Keywords
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.Lexer
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Common.Parsec
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Common.Token hiding (innerList)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Text.ParserCombinators.Parsec
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport CASL.AS_Basic_CASL
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.Formula
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.SortItem
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport CASL.OpItem
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport CASL.ToDoc
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Data.List (delete)
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maedertype FplBasicSpec = BASIC_SPEC FplExt () TermExt
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maedertype FplTerm = TERM TermExt
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichtype FplForm = FORMULA TermExt
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederdata FplExt =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski FplSortItems [Annoted FplSortItem] Range
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | FplOpItems [Annoted FplOpItem] Range
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu deriving Show
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maederdata FplSortItem =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder FreeType DATATYPE_DECL
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder | CaslSortItem (SORT_ITEM TermExt)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder deriving Show
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata FplOpItem =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder FunOp FunDef
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | CaslOpItem (OP_ITEM TermExt)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder deriving Show
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederprepPunctBar :: [Doc] -> [Doc]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederprepPunctBar = punctuate (Doc.space <> bar)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederprintDD :: DATATYPE_DECL -> Doc
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederprintDD (Datatype_decl s as _) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder sep [pretty s <+> keyword freeS <+> keyword withS
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder , sep $ prepPunctBar
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder $ map (printAnnoted printALTERNATIVE) as ]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance ListCheck FplOpItem where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder innerList i = case i of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder FunOp _ -> [()]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder CaslOpItem oi -> innerList oi
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederinstance ListCheck FplSortItem where
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder innerList i = case i of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder FreeType _ -> [()]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder CaslSortItem si -> innerList si
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederinstance Pretty FplExt where
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder pretty e = case e of
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder FplSortItems ds _ ->
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder topSigKey (sortS ++ pluralS ds) <+> semiAnnos pretty ds
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder FplOpItems ds _ -> topSigKey (opS ++ pluralS ds) <+> semiAnnos pretty ds
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederinstance Pretty FplSortItem where
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder pretty e = case e of
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder FreeType d -> printDD d
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder CaslSortItem s -> printSortItem pretty s
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederinstance Pretty FplOpItem where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder pretty e = case e of
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder FunOp o -> pretty o
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder CaslOpItem s -> printOpItem pretty s
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maederdata FunDef = FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder deriving (Show, Eq, Ord)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederinstance Pretty FunDef where
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder pretty (FunDef i h@(Op_head _ l _ _) t _) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sep [keyword functS
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , sep [ (if null l then sep else cat) [idLabelDoc i, pretty h]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , equals <+> printAnnoted pretty t]]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederdata TermExt =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder FixDef FunDef -- ^ formula
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | Case FplTerm [(FplTerm, FplTerm)] Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | Let FunDef FplTerm Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder | IfThenElse FplForm FplTerm FplTerm Range
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder deriving (Show, Eq, Ord)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederinstance Pretty TermExt where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pretty t = case t of
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder FixDef fd -> pretty fd
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Case c l _ ->
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder sep $ (keyword caseS <+> pretty c <+> keyword ofS)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder : prepPunctBar
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (map (\ (p, e) -> fsep [pretty p, implies, pretty e]) l)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Let fd i _ -> sep [keyword letS <+> pretty fd, keyword inS <+> pretty i]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder IfThenElse i d e _ ->
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder fsep [ keyword ifS <+> pretty i
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , keyword thenS <+> pretty d
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , keyword elseS <+> pretty e ]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederfplReservedWords :: [String]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskifplReservedWords = [barS, functS, caseS, ofS, letS]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskifunDef :: [String] -> AParser st FunDef
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederfunDef ks = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder q <- asKey functS
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder o <- parseId ks
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder h <- opHead ks
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder e <- equalT
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder a <- annos
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder t <- term ks
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ FunDef o h (Annoted t nullRange a []) $ toRange q [] e
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederoptVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederoptVarDecls ks =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (oParenT >> separatedBy (varDecl ks) anSemi << cParenT)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <|> return ([], [])
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederfplTerm :: [String] -> AParser st TermExt
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederfplTerm ks = caseTerm ks <|> letTerm ks <|> ifThenElse ks
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedercaseTerm :: [String] -> AParser st TermExt
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedercaseTerm ks = do
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder c <- asKey caseS
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder t <- mixTerm ks
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder o <- asKey ofS
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (cs, qs) <- separatedBy (patTermPair ks) barT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Case t cs $ toRange c qs o
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederpatTermPair :: [String] -> AParser st (FplTerm, FplTerm)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederpatTermPair ks = do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder p <- mixTerm ks
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder implKey
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder t <- mixTerm ks
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (p, t)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederletTerm :: [String] -> AParser st TermExt
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiletTerm ks = do
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz l <- asKey letS
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz d <- funDef ks
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz i <- asKey inS
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz t <- term ks
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return $ Let d t $ toRange l [] i
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzifThenElse :: [String] -> AParser st TermExt
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzifThenElse ks = do
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz i <- ifKey
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder f <- primFormula ks
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder t <- asKey thenS
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz a <- mixTerm ks
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz e <- asKey elseS
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz b <- mixTerm ks
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return $ IfThenElse f a b $ toRange i [t] e
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzinstance TermParser TermExt where
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz termParser b = if b then fplTerm fplReservedWords else
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder fmap FixDef $ funDef fplReservedWords
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederfplExt :: [String] -> AParser st FplExt
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederfplExt ks = itemList ks sortS fplSortItem FplSortItems
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <|> itemList (delete functS ks) opS fplOpItem FplOpItems
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederfplSortItem :: [String] -> AParser st FplSortItem
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederfplSortItem ks = do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder s <- sortId ks
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder freeType ks s <|>
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder fmap CaslSortItem (subSortDecl ks ([s], nullRange) <|> commaSortDecl ks s
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder <|> isoDecl ks s <|> return (Sort_decl [s] nullRange))
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfreeType :: [String] -> SORT -> AParser st FplSortItem
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfreeType ks s = do
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder f <- asKey freeS
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder asKey withS
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder fmap FreeType $ parseDatatype ks s f
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfplOpItem :: [String] -> AParser st FplOpItem
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederfplOpItem ks = fmap FunOp (funDef ks) <|> fmap CaslOpItem (opItem ks)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maederinstance AParsable FplExt where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder aparser = fplExt fplReservedWords
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder