hets/Fpl/As.der.hs

	As.der.hs revision 3d4f336bca521e5cd85ce5fcfc572469c88c942c
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{- |
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederModule      :  $Header$
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederDescription :  abstract syntax for FPL
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederCopyright   :  (c) Christian Maeder, DFKI GmbH 2011
54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian MaederLicense     :  GPLv2 or higher, see LICENSE.txt
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer  :  Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability   :  provisional
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability :  portable
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederabstract syntax for FPL, logic for functional programs
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederas CASL extension
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-}
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule Fpl.As where
da955132262baab309a50fdffe228c9efe68251dCui Jian
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder-- DrIFT command
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder{-! global: GetRange !-}
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Common.AS_Annotation
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport Common.AnnoState
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maederimport Common.Doc as Doc
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport Common.DocUtils
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederimport Common.Id
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Keywords
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Lexer
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederimport Common.Parsec
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maederimport Common.Token hiding (innerList)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederimport Text.ParserCombinators.Parsec
dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maederimport CASL.AS_Basic_CASL
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyerimport CASL.Formula
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyerimport CASL.SortItem
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederimport CASL.OpItem
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport CASL.ToDoc
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder
da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröningimport Data.List (delete)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanutype FplBasicSpec = BASIC_SPEC FplExt () TermExt
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maedertype FplTerm = TERM TermExt
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maedertype FplForm = FORMULA TermExt
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanudata FplExt =
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross    FplSortItems [Annoted FplSortItem] Range
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder  | FplOpItems [Annoted FplOpItem] Range
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder  deriving Show
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder
6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maederdata FplSortItem =
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl    FreeType DATATYPE_DECL
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova  | CaslSortItem (SORT_ITEM TermExt)
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz  deriving Show
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maederdata FplOpItem =
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder    FunOp FunDef
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder  | CaslOpItem (OP_ITEM TermExt)
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder  deriving Show
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian MaederprepPunctBar :: [Doc] -> [Doc]
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin KühlprepPunctBar = prepPunctuate (bar <> Doc.space)
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
2b873214c9ab511bbca437c036371ab664aedaceChristian MaederprintDD :: DATATYPE_DECL -> Doc
fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian MaederprintDD (Datatype_decl s as _) =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder    sep [pretty s <+> keyword freeS <+> keyword withS
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder        , sep $ prepPunctBar
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder          $ map (printAnnoted printALTERNATIVE) as ]
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grossinstance ListCheck FplOpItem where
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross  innerList i = case i of
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    FunOp _ -> [()]
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    CaslOpItem oi -> innerList oi
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance ListCheck FplSortItem where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder  innerList i = case i of
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    FreeType _ -> [()]
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    CaslSortItem si -> innerList si
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance Pretty FplExt where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder  pretty e = case e of
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    FplSortItems ds _ ->
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder        topSigKey (sortS ++ pluralS ds) <+> semiAnnos pretty ds
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    FplOpItems ds _ -> topSigKey (opS ++ pluralS ds) <+> semiAnnos pretty ds
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance Pretty FplSortItem where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder  pretty e = case e of
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    FreeType d -> printDD d
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder    CaslSortItem s -> printSortItem pretty s
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlinstance Pretty FplOpItem where
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl  pretty e = case e of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder    FunOp o -> pretty o
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder    CaslOpItem s -> printOpItem pretty s
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederdata FunDef = FunDef OP_NAME [VAR_DECL] SORT (Annoted FplTerm) Range
bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas  deriving (Show, Eq, Ord)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maederinstance Pretty FunDef where
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder  pretty (FunDef n vs s t _) =
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder    fsep [keyword functS
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder         , pretty n <>
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder          (if null vs then empty else parens (printVarDecls vs))
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder         , colon <+> pretty s
fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder         , equals <+> printAnnoted pretty t]
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata TermExt =
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder    FixDef FunDef -- ^ formula
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder  | Case FplTerm [(FplTerm, FplTerm)] Range
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl  | Let FunDef FplTerm Range
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova  | IfThenElse FplForm FplTerm FplTerm Range
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz  deriving (Show, Eq, Ord)
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederinstance Pretty TermExt where
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder  pretty t = case t of
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder    FixDef fd -> pretty fd
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder    Case c l _ ->
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder      sep $ (keyword caseS <+> pretty c <+> keyword ofS)
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross          : prepPunctBar
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross            (map (\ (p, e) -> fsep [pretty p, implies, pretty e]) l)
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross    Let fd i _ -> sep [keyword letS <+> pretty fd <+> keyword inS, pretty i]
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer    IfThenElse i d e _ ->
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer        fsep [ keyword ifS <+> pretty i
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder             , keyword thenS <+> pretty d
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder             , keyword elseS <+> pretty e ]
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder
f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus LuettichfplReservedWords :: [String]
9175e29c044318498a40f323f189f9dfd50378efChristian MaederfplReservedWords = [barS, functS, caseS, ofS, letS]
f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder
funDef :: [String] -> AParser st FunDef
funDef ks = do
  q <- asKey functS
  o <- parseId ks
  (vs, qs) <- optVarDecls ks
  c <- anColon
  s <- sortId ks
  e <- equalT
  a <- annos
  t <- term ks
  return $ FunDef o vs s (Annoted t nullRange a [])
         $ appRange (toRange q qs c) $ tokPos e

optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
optVarDecls ks =
    (oParenT >> separatedBy (varDecl ks) anSemi << cParenT)
    <|> return ([], [])

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 <- mixTerm 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 <- mixTerm ks
  implKey
  t <- mixTerm ks
  return (p, t)

letTerm :: [String] -> AParser st TermExt
letTerm ks = do
  l <- asKey letS
  d <- funDef 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 <- primFormula ks
  t <- asKey thenS
  a <- mixTerm ks
  e <- asKey elseS
  b <- mixTerm 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

fplExt :: [String] -> AParser st FplExt
fplExt ks = itemList ks sortS fplSortItem FplSortItems
  <|> itemList (delete functS ks) opS fplOpItem FplOpItems

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