1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : abstract syntax for FPL

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariCopyright : (c) Christian Maeder, DFKI GmbH 2011

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariLicense : GPLv2 or higher, see LICENSE.txt

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariMaintainer : Christian.Maeder@dfki.de

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariStability : provisional

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariPortability : portable

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariabstract syntax for FPL, logic for functional programs

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegarias CASL extension

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari-}

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegarimodule Fpl.As where

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari-- DrIFT command

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari{-! global: GetRange !-}

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.AS_Annotation

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.AnnoState

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.Doc as Doc

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.DocUtils

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.Id

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Common.Keywords

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.Lexer

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.Parsec

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Common.Token hiding (innerList)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport Text.ParserCombinators.Parsec

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport CASL.AS_Basic_CASL

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport CASL.Formula

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariimport CASL.SortItem

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.OpItem

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport CASL.ToDoc

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.List (delete)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe (isNothing)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegaritype FplBasicSpec = BASIC_SPEC FplExt () TermExt

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegaritype FplTerm = TERM TermExt

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegaritype FplForm = FORMULA TermExt

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegaridata FplExt =

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari FplSortItems [Annoted FplSortItem] Range

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | FplOpItems [Annoted FplOpItem] Range

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving Show

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegaridata FplSortItem =

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari FreeType DATATYPE_DECL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | CaslSortItem (SORT_ITEM TermExt)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari deriving Show

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata FplOpItem =

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari FunOp FunDef

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | CaslOpItem (OP_ITEM TermExt)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari deriving Show

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel CalegariprepPunctBar :: [Doc] -> [Doc]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprepPunctBar = punctuate (Doc.space <> bar)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel CalegariprintDD :: DATATYPE_DECL -> Doc

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel CalegariprintDD (Datatype_decl s as _) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sep [pretty s <+> keyword freeS <+> keyword withS

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari , sep $ prepPunctBar

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari $ map (printAnnoted printALTERNATIVE) as ]

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegariinstance ListCheck FplOpItem where

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari innerList i = case i of

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari FunOp _ -> [()]

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari CaslOpItem oi -> innerList oi

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegariinstance ListCheck FplSortItem where

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari innerList i = case i of

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari FreeType _ -> [()]

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari CaslSortItem si -> innerList si

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariinstance Pretty FplExt where

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari pretty e = case e of

100ddc17625c25a9ffe83737edc53db7538b41ffDaniel Calegari FplSortItems ds _ ->

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari topSigKey (sortS ++ pluralS ds) <+> semiAnnos pretty ds

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari FplOpItems ds _ -> topSigKey (opS ++ pluralS ds) <+> semiAnnos pretty ds

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariinstance Pretty FplSortItem where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty e = case e of

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder FreeType d -> printDD d

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari CaslSortItem s -> printSortItem pretty s

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegariinstance Pretty FplOpItem where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty e = case e of

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari FunOp o -> pretty o

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari CaslOpItem s -> printOpItem pretty s

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegaridata FunDef = FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari deriving (Show, Eq, Ord)

15042bad71a157e77c0a1893759f9027b2673a1eDaniel Calegari

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarikindHead :: OpKind -> OP_HEAD -> OP_HEAD

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarikindHead k (Op_head _ args r ps) = Op_head k args r ps

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegariinstance Pretty FunDef where

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari pretty (FunDef i h@(Op_head _ l ms _) t _) =

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari let di = idLabelDoc i

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari et = equals <+> printAnnoted pretty t

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder in sep $ if isNothing ms && null l then [di, et] else

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari [keyword functS,

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari sep [(if null l then sep else cat) [di, pretty $ kindHead Total h], et]]

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | extra terms of FPL. if-then-else must use a term as guard with result

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegarisort @Bool@. To allow @true@, @false@ and an equality test an extra term

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegariparser is needed that must not be used when parsing formulas. -}

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegaridata TermExt =

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari FixDef FunDef -- ^ formula

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari | Case FplTerm [(FplTerm, FplTerm)] Range

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari | Let FunDef FplTerm Range

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari | IfThenElse FplTerm FplTerm FplTerm Range

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari | EqTerm FplTerm FplTerm Range

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari | BoolTerm FplTerm

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari deriving (Show, Eq, Ord)

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegariinstance Pretty TermExt where

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari pretty t = case t of

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari FixDef fd -> pretty fd

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari Case c l _ ->

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari sep $ (keyword caseS <+> pretty c <+> keyword ofS)

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari : prepPunctBar

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari (map (\ (p, e) -> fsep [pretty p, implies, pretty e]) l)

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari Let fd i _ -> sep [keyword letS <+> pretty fd, keyword inS <+> pretty i]

0fa27dd041f2c5affd7d4d6ad04e568a0e49737cDaniel Calegari IfThenElse i d e _ ->

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari fsep [ keyword ifS <+> pretty i

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari , keyword thenS <+> pretty d

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari , keyword elseS <+> pretty e ]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder EqTerm t1 t2 r -> pretty $ Strong_equation t1 t2 r

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder BoolTerm f -> pretty f

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarifplReservedWords :: [String]

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarifplReservedWords = [barS, functS, caseS, ofS, letS]

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfunDef :: [String] -> AParser st FunDef

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarifunDef ks = do

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari q <- asKey functS

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari o <- parseId ks

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari h <- opHead ks

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari e <- equalT

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari a <- annos

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari t <- eqTerm ks

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari return $ FunDef o (kindHead Partial h)

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari (Annoted t nullRange a []) $ toRange q [] e

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel Calegari

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarioptVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])

7ad21cf90b1053c2fa8f97535235a83a0678fc64Daniel CalegarioptVarDecls 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