{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./Fpl/As.der.hs
Description : abstract syntax for FPL
Copyright : (c) Christian Maeder, DFKI GmbH 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
abstract syntax for FPL, logic for functional programs
as CASL extension
-}
module Fpl.As where
-- DrIFT command
{-! global: GetRange !-}
import Common.AS_Annotation
import Common.AnnoState
import Common.Doc as Doc
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token hiding (innerList)
import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.SortItem
import CASL.OpItem
import CASL.ToDoc
import Data.Data
import Data.List (delete)
import Data.Maybe (isNothing)
type FplBasicSpec = BASIC_SPEC FplExt () TermExt
type FplTerm = TERM TermExt
type FplForm = FORMULA TermExt
data FplExt =
FplSortItems [Annoted FplSortItem] Range
| FplOpItems [Annoted FplOpItem] Range
deriving (Show, Typeable, Data)
data FplSortItem =
FreeType DATATYPE_DECL
| CaslSortItem (SORT_ITEM TermExt)
deriving (Show, Typeable, Data)
data FplOpItem =
FunOp FunDef
| CaslOpItem (OP_ITEM TermExt)
deriving (Show, Typeable, Data)
prepPunctBar :: [Doc] -> [Doc]
prepPunctBar = punctuate (Doc.space <> bar)
printDD :: DATATYPE_DECL -> Doc
printDD (Datatype_decl s as _) =
sep [pretty s <+> keyword freeS <+> keyword withS
, sep $ prepPunctBar
$ map (printAnnoted printALTERNATIVE) as ]
instance ListCheck FplOpItem where
innerList i = case i of
FunOp _ -> [()]
CaslOpItem oi -> innerList oi
instance ListCheck FplSortItem where
innerList i = case i of
FreeType _ -> [()]
CaslSortItem si -> innerList si
instance Pretty FplExt where
pretty e = case e of
FplSortItems ds _ ->
topSigKey (sortS ++ pluralS ds) <+> semiAnnos pretty ds
FplOpItems ds _ -> topSigKey (opS ++ pluralS ds) <+> semiAnnos pretty ds
instance Pretty FplSortItem where
pretty e = case e of
FreeType d -> printDD d
CaslSortItem s -> printSortItem s
instance Pretty FplOpItem where
pretty e = case e of
FunOp o -> pretty o
CaslOpItem s -> printOpItem s
data FunDef = FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range
deriving (Show, Eq, Ord, Typeable, Data)
kindHead :: OpKind -> OP_HEAD -> OP_HEAD
kindHead k (Op_head _ args r ps) = Op_head k args r ps
instance Pretty FunDef where
pretty (FunDef i h@(Op_head _ l ms _) t _) =
let di = idLabelDoc i
et = equals <+> printAnnoted pretty t
in sep $ if isNothing ms && null l then [di, et] else
[keyword functS,
sep [(if null l then sep else cat) [di, pretty $ kindHead Total h], et]]
{- | extra terms of FPL. if-then-else must use a term as guard with result
sort @Bool@. To allow @true@, @false@ and an equality test an extra term
parser is needed that must not be used when parsing formulas. -}
data TermExt =
FixDef FunDef -- ^ formula
| Case FplTerm [(FplTerm, FplTerm)] Range
| Let FunDef FplTerm Range
| IfThenElse FplTerm FplTerm FplTerm Range
| EqTerm FplTerm FplTerm Range
| BoolTerm FplTerm
deriving (Show, Eq, Ord, Typeable, Data)
instance FormExtension TermExt
instance Pretty TermExt where
pretty t = case t of
FixDef fd -> pretty fd
Case c l _ ->
sep $ (keyword caseS <+> pretty c <+> keyword ofS)
: prepPunctBar
(map (\ (p, e) -> fsep [pretty p, implies, pretty e]) l)
Let fd i _ -> sep [keyword letS <+> pretty fd, keyword inS <+> pretty i]
IfThenElse i d e _ ->
fsep [ keyword ifS <+> pretty i
, keyword thenS <+> pretty d
, keyword elseS <+> pretty e ]
EqTerm t1 t2 r -> pretty $ Equation t1 Strong t2 r
BoolTerm f -> pretty f
fplReservedWords :: [String]
fplReservedWords = [barS, functS, caseS, ofS, letS]
funDef :: [String] -> AParser st FunDef
funDef ks = do
q <- asKey functS
o <- parseId ks
h <- opHead ks
e <- equalT
a <- annos
t <- eqTerm ks
return $ FunDef o (kindHead Partial h)
(Annoted t nullRange a []) $ toRange q [] e
optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
optVarDecls ks =
(oParenT >> separatedBy (varDecl ks) anSemi << cParenT)
<|> return ([], [])
constBool :: AParser st FplTerm
constBool = fmap Mixfix_token (asKey trueS <|> asKey falseS)
boolTerm :: [String] -> AParser st FplTerm
boolTerm ks = constBool <|> mixTerm ks
eqTerm :: [String] -> AParser st FplTerm
eqTerm ks = do
b <- boolTerm ks
option b $ do
e <- equalT
b2 <- boolTerm ks
return $ ExtTERM $ EqTerm b b2 $ tokPos e
{- | extra formulas to compare bool terms with true or false.
Interpreting boolean valued terms as formulas is still missing. -}
eqForm :: [String] -> AParser st TermExt
eqForm ks = do
(c, t) <- try $ pair constBool equalT
e <- mixTerm ks
return $ EqTerm c e $ tokPos t
<|> fmap (\ (e, (t, c)) -> EqTerm e c $ tokPos t)
(try $ pair (mixTerm ks) $ pair equalT constBool)
fplTerm :: [String] -> AParser st TermExt
fplTerm ks = caseTerm ks <|> letTerm ks <|> ifThenElse ks
caseTerm :: [String] -> AParser st TermExt
caseTerm ks = do
c <- asKey caseS
t <- eqTerm ks
o <- asKey ofS
(cs, qs) <- separatedBy (patTermPair ks) barT
return $ Case t cs $ toRange c qs o
patTermPair :: [String] -> AParser st (FplTerm, FplTerm)
patTermPair ks = do
p <- eqTerm ks
implKey
t <- eqTerm ks
return (p, t)
letVar :: [String] -> AParser st FunDef
letVar ks = do
v <- varId ks
e <- equalT
a <- annos
t <- eqTerm ks
return $ FunDef (simpleIdToId v) (Op_head Partial [] Nothing nullRange)
(Annoted t nullRange a []) $ tokPos e
letTerm :: [String] -> AParser st TermExt
letTerm ks = do
l <- asKey letS
d <- funDef ks <|> letVar ks
i <- asKey inS
t <- term ks
return $ Let d t $ toRange l [] i
ifThenElse :: [String] -> AParser st TermExt
ifThenElse ks = do
i <- ifKey
f <- eqTerm ks
t <- asKey thenS
a <- eqTerm ks
e <- asKey elseS
b <- eqTerm ks
return $ IfThenElse f a b $ toRange i [t] e
instance TermParser TermExt where
termParser b = if b then fplTerm fplReservedWords else
fmap FixDef (funDef fplReservedWords) <|> eqForm fplReservedWords
fplExt :: [String] -> AParser st FplExt
fplExt ks = itemList ks sortS fplSortItem FplSortItems
<|> itemList (delete functS ks) opS fplOpItem FplOpItems
<|> ((pluralKeyword etypeS <|> pluralKeyword typeS <|> pluralKeyword predS
<|> pluralKeyword esortS <|> asKey generatedS <|> asKey freeS)
>>= \ k -> unexpected $ "CASL keyword '" ++ shows k "'")
fplSortItem :: [String] -> AParser st FplSortItem
fplSortItem ks = do
s <- sortId ks
freeType ks s <|>
fmap CaslSortItem (subSortDecl ks ([s], nullRange) <|> commaSortDecl ks s
<|> isoDecl ks s <|> return (Sort_decl [s] nullRange))
freeType :: [String] -> SORT -> AParser st FplSortItem
freeType ks s = do
f <- asKey freeS
asKey withS
fmap FreeType $ parseDatatype ks s f
fplOpItem :: [String] -> AParser st FplOpItem
fplOpItem ks = fmap FunOp (funDef ks) <|> fmap CaslOpItem (opItem ks)
instance AParsable FplExt where
aparser = fplExt fplReservedWords