Parse_AS_Basic.hs revision 7594b91154e299c9bcecd2bd62698705b55f99e8
6ae232055d4d8a97267517c5e50074c2c819941and{-# LANGUAGE TypeSynonymInstances #-}
fd9abdda70912b99b24e3bf1a38f26fde908a74cndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Parser for basic specs
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Dominik Dietrich, DFKI Bremen 2010
6ae232055d4d8a97267517c5e50074c2c819941andLicense : GPLv2 or higher, see LICENSE.txt
6ae232055d4d8a97267517c5e50074c2c819941andMaintainer : dominik.dietrich@dfki.de
6ae232055d4d8a97267517c5e50074c2c819941andStability : experimental
96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcPortability : non-portable
6ae232055d4d8a97267517c5e50074c2c819941andParser for abstract syntax for CSL
6ae232055d4d8a97267517c5e50074c2c819941andimport qualified Common.AnnoState as AnnoState
6ae232055d4d8a97267517c5e50074c2c819941andimport Common.Id as Id
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport Common.Keywords as Keywords
3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Common.Lexer as Lexer
6ae232055d4d8a97267517c5e50074c2c819941andimport Common.AS_Annotation as AS_Anno
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung-- TODO: extract range information for the basic term and command types
b43f840409794ed298e8634f6284741f193b6c4ftakashi-- ---------------------------------------------------------------------------
b43f840409794ed298e8634f6284741f193b6c4ftakashi-- * Interface to the syntax class
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941andparseBasicSpec :: Maybe (AnnoState.AParser st BASIC_SPEC)
6ae232055d4d8a97267517c5e50074c2c819941andparseBasicSpec = Just basicSpec
6ae232055d4d8a97267517c5e50074c2c819941andparseSymbItems :: Maybe (GenParser Char st SYMB_ITEMS)
6ae232055d4d8a97267517c5e50074c2c819941andparseSymbItems = Just symbItems
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohparseSymbMapItems :: Maybe (GenParser Char st SYMB_MAP_ITEMS)
6ae232055d4d8a97267517c5e50074c2c819941andparseSymbMapItems = Just symbMapItems
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * Parser utils
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941andinstance OperatorState (AnnoState.AnnoState st) where
6ae232055d4d8a97267517c5e50074c2c819941and lookupOperator _ = lookupOpInfoForParsing operatorInfoMap
6ae232055d4d8a97267517c5e50074c2c819941andparseError :: String -> CharParser st a
6ae232055d4d8a97267517c5e50074c2c819941andparseError s = do
6ae232055d4d8a97267517c5e50074c2c819941and p <- getPosition
6ae232055d4d8a97267517c5e50074c2c819941and return $ error
6ae232055d4d8a97267517c5e50074c2c819941and $ concat [ "Parse error at line: ", show (Parsec.sourceLine p)
6ae232055d4d8a97267517c5e50074c2c819941and , " col: ", show (Parsec.sourceColumn p), "\n", s]
6ae232055d4d8a97267517c5e50074c2c819941andpComma :: CharParser st String
6ae232055d4d8a97267517c5e50074c2c819941andpComma = lexemeParser $ string ","
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpSemi :: CharParser st String
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndpSemi = lexemeParser $ string ";"
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndlstring :: String -> CharParser st String
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndlstring = lexemeParser . string
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd-- | parser for symbols followed by whitechars
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndlexemeParser :: CharParser st a -> CharParser st a
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndlexemeParser = (<< skip)
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndgetOpName :: String -> [OPNAME] -> OPNAME
1ac39787115a288f5e848344b1b1e8dccb1c58f1ndgetOpName s l = f l
6ae232055d4d8a97267517c5e50074c2c819941and where f (x:xs) = if s == show x then x else f xs
6ae232055d4d8a97267517c5e50074c2c819941and f [] = error $ "getOpName: no op found for " ++ s ++ " in " ++ show l
6ae232055d4d8a97267517c5e50074c2c819941andmkFromOps :: [OPNAME] -> String -> [EXPRESSION] -> EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andmkFromOps l s exps = mkPredefOp (getOpName s l) exps
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * Parser for Expressions
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and{- | parsing of identifiers. an identifier is a letter followed by
6ae232055d4d8a97267517c5e50074c2c819941and letters, numbers, or _, but not a keyword -}
6ae232055d4d8a97267517c5e50074c2c819941andidentifier :: CharParser st Id.Token
6ae232055d4d8a97267517c5e50074c2c819941andidentifier =
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser $ Lexer.pToken $ reserved allKeywords Lexer.scanAnyWords
6ae232055d4d8a97267517c5e50074c2c819941andprefixidentifier :: CharParser st Id.Token
6ae232055d4d8a97267517c5e50074c2c819941andprefixidentifier =
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser $ Lexer.pToken $ Lexer.scanAnySigns <|> Lexer.scanAnyWords
6ae232055d4d8a97267517c5e50074c2c819941and-- | parses a possibly signed number to an EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andsignednumberExp :: CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andsignednumberExp =
6ae232055d4d8a97267517c5e50074c2c819941and let f (eN, rg) = either (flip Int rg) (flip Double rg) eN
6ae232055d4d8a97267517c5e50074c2c819941and in signednumber >-> f
6ae232055d4d8a97267517c5e50074c2c819941and-- | parses a possibly signed number (both integers and floats)
6ae232055d4d8a97267517c5e50074c2c819941andsignednumber :: CharParser st (Either APInt APFloat, Range)
6ae232055d4d8a97267517c5e50074c2c819941andsignednumber =
6ae232055d4d8a97267517c5e50074c2c819941and let f c x = return (c $ read $ tokStr x, tokPos x)
6ae232055d4d8a97267517c5e50074c2c819941and g x | isFloating x = f Right x
6ae232055d4d8a97267517c5e50074c2c819941and | otherwise = f Left x
6ae232055d4d8a97267517c5e50074c2c819941and-- | The version in Common.Lexer is not compatible with floating point numbers
6ae232055d4d8a97267517c5e50074c2c819941and-- which may start with ".". This one does it.
6ae232055d4d8a97267517c5e50074c2c819941andkeySignNumCompat :: CharParser st a -> CharParser st a
6ae232055d4d8a97267517c5e50074c2c819941andkeySignNumCompat = try . (<< notFollowedBy (oneOf signNumCompatChars))
6ae232055d4d8a97267517c5e50074c2c819941andsignNumCompatChars :: String
6ae232055d4d8a97267517c5e50074c2c819941andsignNumCompatChars = "!#$&*+-/:<=>?@\\^|~" ++
6ae232055d4d8a97267517c5e50074c2c819941and "\161\162\163\167\169\172\176\177\178\179\181\182\183\185\191\215\247"
6ae232055d4d8a97267517c5e50074c2c819941andoneOfKeys :: [String] -> CharParser st String
6ae232055d4d8a97267517c5e50074c2c819941andoneOfKeys l = lexemeParser $ keySignNumCompat $ choice $ map tryString l
6ae232055d4d8a97267517c5e50074c2c819941andplusmin :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andplusmin = do
6ae232055d4d8a97267517c5e50074c2c819941and let ops = [OP_plus, OP_minus]
6ae232055d4d8a97267517c5e50074c2c819941and exp1 <- factor
6ae232055d4d8a97267517c5e50074c2c819941and exps <- many $ pair (oneOfKeys $ map show ops) factor
6ae232055d4d8a97267517c5e50074c2c819941and return $ if null exps then exp1
6ae232055d4d8a97267517c5e50074c2c819941and else foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps
6ae232055d4d8a97267517c5e50074c2c819941and-- | parse a product of basic expressions
6ae232055d4d8a97267517c5e50074c2c819941andfactor :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andfactor = do
6ae232055d4d8a97267517c5e50074c2c819941and let ops = [OP_mult, OP_div]
6ae232055d4d8a97267517c5e50074c2c819941and exp1 <- expexp
6ae232055d4d8a97267517c5e50074c2c819941and exps <- many $ pair (oneOfKeys $ map show ops) expexp
6ae232055d4d8a97267517c5e50074c2c819941and if null exps then return exp1
6ae232055d4d8a97267517c5e50074c2c819941and else return $ foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps
6ae232055d4d8a97267517c5e50074c2c819941and-- | parse a sequence of exponentiations
6ae232055d4d8a97267517c5e50074c2c819941andexpexp :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andexpexp = do
6ae232055d4d8a97267517c5e50074c2c819941and exp1 <- expatom
6ae232055d4d8a97267517c5e50074c2c819941and exps <- many $ pair (oneOfKeys ["**", "^"]) expatom
6ae232055d4d8a97267517c5e50074c2c819941and if null exps then return exp1
6ae232055d4d8a97267517c5e50074c2c819941and else return $ foldl (\ a b -> mkPredefOp OP_pow [a, snd b]) exp1 exps
6ae232055d4d8a97267517c5e50074c2c819941and-- | parse a basic expression
6ae232055d4d8a97267517c5e50074c2c819941andexpatom :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andexpatom = try signednumberExp <|> (oParenT >> plusmin << cParenT)
6ae232055d4d8a97267517c5e50074c2c819941and <|> listexp <|> intervalexp <|> expsymbol
6ae232055d4d8a97267517c5e50074c2c819941andexpsymbol :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andexpsymbol =
6ae232055d4d8a97267517c5e50074c2c819941and ident <- prefixidentifier -- EXTENDED
6ae232055d4d8a97267517c5e50074c2c819941and ep <- option ([],[])
6ae232055d4d8a97267517c5e50074c2c819941and $ oBracketT >> Lexer.separatedBy extparam pComma << cBracketT
6ae232055d4d8a97267517c5e50074c2c819941and exps <- option ([],[])
6ae232055d4d8a97267517c5e50074c2c819941and $ oParenT >> Lexer.separatedBy formulaorexpression pComma
6ae232055d4d8a97267517c5e50074c2c819941and << cParenT
6ae232055d4d8a97267517c5e50074c2c819941and st <- getState
6ae232055d4d8a97267517c5e50074c2c819941and return $ mkAndAnalyzeOp st (tokStr ident) (fst ep) (fst exps) nullRange
6ae232055d4d8a97267517c5e50074c2c819941and-- | parses a list expression
6ae232055d4d8a97267517c5e50074c2c819941andlistexp :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andlistexp = do
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign $ string "{"
6ae232055d4d8a97267517c5e50074c2c819941and elems <- Lexer.separatedBy formulaorexpression pComma
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign $ string "}"
6ae232055d4d8a97267517c5e50074c2c819941and return (List (fst elems) nullRange)
6ae232055d4d8a97267517c5e50074c2c819941andintervalexp :: CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andintervalexp = do
6ae232055d4d8a97267517c5e50074c2c819941and nums <- lstring "[" >> Lexer.separatedBy signednumber pComma << lstring "]"
6ae232055d4d8a97267517c5e50074c2c819941and let getFloat = either fromInteger id
6ae232055d4d8a97267517c5e50074c2c819941and case fst nums of
6ae232055d4d8a97267517c5e50074c2c819941and [(x, rg1), (y, rg2)] -> return $ Interval (getFloat x) (getFloat y) $ Range
6ae232055d4d8a97267517c5e50074c2c819941and $ joinRanges $ map rangeToList [rg1, rg2]
6ae232055d4d8a97267517c5e50074c2c819941and _ -> parseError
6ae232055d4d8a97267517c5e50074c2c819941and "intervalexp: Parse error: interval with other than two arguments"
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- ** parser for extended parameter, e.g., [I=0,...]
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941andextparam :: CharParser st EXTPARAM
6ae232055d4d8a97267517c5e50074c2c819941andextparam = do
6ae232055d4d8a97267517c5e50074c2c819941and i <- identifier
6ae232055d4d8a97267517c5e50074c2c819941and liftM2 (EP i) (oneOfKeys ["=", "<=", ">=", "!=", "<", ">", "-|"])
6ae232055d4d8a97267517c5e50074c2c819941and $ option 0 $ signednumber
6ae232055d4d8a97267517c5e50074c2c819941and >-> either id (error "extparam: floats not supported") . fst
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * parser for formulas
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941andparseVarList :: CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andparseVarList = do
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign (string "{")
6ae232055d4d8a97267517c5e50074c2c819941and elems <- Lexer.separatedBy parseVar pComma
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign (string "}")
6ae232055d4d8a97267517c5e50074c2c819941and return (List (fst elems) nullRange)
6ae232055d4d8a97267517c5e50074c2c819941andparseVar :: CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andparseVar = do
6ae232055d4d8a97267517c5e50074c2c819941and ident <- identifier
1ac39787115a288f5e848344b1b1e8dccb1c58f1nd return (Var ident)
6ae232055d4d8a97267517c5e50074c2c819941andquantFormula :: OperatorState st => OPNAME -> CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941and -- TODO: static analysis requires probably a better representation of quantifiers
6ae232055d4d8a97267517c5e50074c2c819941andquantFormula q = do
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign (string $ show q)
6ae232055d4d8a97267517c5e50074c2c819941and vars <- ( parseVar <|> parseVarList)
6ae232055d4d8a97267517c5e50074c2c819941and expr <- formulaorexpression
6ae232055d4d8a97267517c5e50074c2c819941and return (mkPredefOp q [vars, expr])
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for atoms
6ae232055d4d8a97267517c5e50074c2c819941andtruefalseFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andtruefalseFormula =
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser (Lexer.keyWord (tryString $ show OP_true))
6ae232055d4d8a97267517c5e50074c2c819941and return (mkPredefOp OP_true [])
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser (Lexer.keyWord (tryString $ show OP_false))
4aa603e6448b99f9371397d439795c91a93637eand return (mkPredefOp OP_false [])
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen <|> quantFormula OP_ex <|> quantFormula OP_all
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen-- | parser for predicates
6ae232055d4d8a97267517c5e50074c2c819941andpredFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andpredFormula = do
6ae232055d4d8a97267517c5e50074c2c819941and let ops = [ OP_leq, OP_geq, OP_neq, OP_eq, OP_lt, OP_gt ]
6ae232055d4d8a97267517c5e50074c2c819941and exp1 <- plusmin
6ae232055d4d8a97267517c5e50074c2c819941and mExp2 <- optionMaybe
6ae232055d4d8a97267517c5e50074c2c819941and $ pair (oneOfKeys (map show $ take 3 ops) -- the first 3 print as 2-chars
6ae232055d4d8a97267517c5e50074c2c819941and <|> lexemeParser (single $ oneOf "=<>")) plusmin
6ae232055d4d8a97267517c5e50074c2c819941and case mExp2 of
6ae232055d4d8a97267517c5e50074c2c819941and Just (op, exp2) -> return $ mkFromOps ops op [exp1, exp2]
6ae232055d4d8a97267517c5e50074c2c819941and _ -> return $ exp1
6ae232055d4d8a97267517c5e50074c2c819941andatomicFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andatomicFormula = truefalseFormula <|> predFormula <|> parenFormula
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for formulas
6ae232055d4d8a97267517c5e50074c2c819941andaFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andaFormula = try negFormula <|> impOrFormula
6ae232055d4d8a97267517c5e50074c2c819941andnegFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andnegFormula = do
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser (Lexer.keyWord (tryString $ show OP_not))
6ae232055d4d8a97267517c5e50074c2c819941and f <- atomicFormula
6ae232055d4d8a97267517c5e50074c2c819941and return (mkPredefOp OP_not [f])
6ae232055d4d8a97267517c5e50074c2c819941and-- | parses a formula within brackets
6ae232055d4d8a97267517c5e50074c2c819941andparenFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andparenFormula = do
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser oParenT
6ae232055d4d8a97267517c5e50074c2c819941and f <- aFormula
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser cParenT
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for implications and ors (same precedence)
6ae232055d4d8a97267517c5e50074c2c819941andimpOrFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andimpOrFormula = do
6ae232055d4d8a97267517c5e50074c2c819941and let ops = [ OP_or, OP_impl ]
6ae232055d4d8a97267517c5e50074c2c819941and f1 <- andFormula
6ae232055d4d8a97267517c5e50074c2c819941and opfs <- many $ pair (lexemeParser $ Lexer.keyWord
6ae232055d4d8a97267517c5e50074c2c819941and $ tryString (show OP_or) <|> tryString (show OP_impl))
6ae232055d4d8a97267517c5e50074c2c819941and andFormula
6ae232055d4d8a97267517c5e50074c2c819941and if null opfs then return f1
6ae232055d4d8a97267517c5e50074c2c819941and else return $ foldl (\ a (op, b) -> mkFromOps ops op [a, b]) f1 opfs
6ae232055d4d8a97267517c5e50074c2c819941and-- | a parser for and sequence of and formulas
6ae232055d4d8a97267517c5e50074c2c819941andandFormula :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andandFormula = do
6ae232055d4d8a97267517c5e50074c2c819941and f1 <- atomicFormula
6ae232055d4d8a97267517c5e50074c2c819941and opfs <- many $ pair (lexemeParser $ keyWord $ tryString $ show OP_and)
6ae232055d4d8a97267517c5e50074c2c819941and atomicFormula
6ae232055d4d8a97267517c5e50074c2c819941and if null opfs then return f1
6ae232055d4d8a97267517c5e50074c2c819941and else return $ foldl (\ b a -> (mkPredefOp OP_and [b, snd a])) f1 opfs
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * Parser for Commands
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941andformulaorexpression :: OperatorState st => CharParser st EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andformulaorexpression = try aFormula <|> plusmin
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for commands
6ae232055d4d8a97267517c5e50074c2c819941andcommand :: CharParser (AnnoState.AnnoState st) CMD
6ae232055d4d8a97267517c5e50074c2c819941andcommand = reduceCommand <|> try assignment <|> repeatExpr <|> caseExpr
6ae232055d4d8a97267517c5e50074c2c819941and <|> sequenceExpr <|> constraint
6ae232055d4d8a97267517c5e50074c2c819941andreduceCommand :: OperatorState st => CharParser st CMD
6ae232055d4d8a97267517c5e50074c2c819941andreduceCommand = do
6ae232055d4d8a97267517c5e50074c2c819941and cmd <- lexemeParser $ Lexer.keyWord $ choice $ map tryString
6ae232055d4d8a97267517c5e50074c2c819941and ["solve", "simplify", "divide", "int", "rlqe", "factorize", "print"]
6ae232055d4d8a97267517c5e50074c2c819941and arg1 <- formulaorexpression
6ae232055d4d8a97267517c5e50074c2c819941and args <- many $ pComma >> formulaorexpression
6ae232055d4d8a97267517c5e50074c2c819941and return $ Cmd cmd $ arg1 : args
6ae232055d4d8a97267517c5e50074c2c819941andassignment :: OperatorState st => CharParser st CMD
6ae232055d4d8a97267517c5e50074c2c819941andassignment = do
6ae232055d4d8a97267517c5e50074c2c819941and ident <- expsymbol
6ae232055d4d8a97267517c5e50074c2c819941and lexemeParser $ tryString ":="
6ae232055d4d8a97267517c5e50074c2c819941and exp' <- plusmin
6ae232055d4d8a97267517c5e50074c2c819941and return $ Ass ident exp'
6ae232055d4d8a97267517c5e50074c2c819941andconstraint :: OperatorState st => CharParser st CMD
6ae232055d4d8a97267517c5e50074c2c819941andconstraint = do
6ae232055d4d8a97267517c5e50074c2c819941and exp' <- try aFormula
6ae232055d4d8a97267517c5e50074c2c819941and case exp' of
6ae232055d4d8a97267517c5e50074c2c819941and Op _ _ _ _ ->
6ae232055d4d8a97267517c5e50074c2c819941and return $ Cmd "constraint" [exp']
6ae232055d4d8a97267517c5e50074c2c819941and _ -> fail "Malformed constraint"
6ae232055d4d8a97267517c5e50074c2c819941andsequenceExpr :: CharParser (AnnoState.AnnoState st) CMD
6ae232055d4d8a97267517c5e50074c2c819941andsequenceExpr = do
6ae232055d4d8a97267517c5e50074c2c819941and lstring "sequence"
6ae232055d4d8a97267517c5e50074c2c819941and statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
6ae232055d4d8a97267517c5e50074c2c819941and lstring "end"
6ae232055d4d8a97267517c5e50074c2c819941and return $ Sequence $ map AS_Anno.item statements
6ae232055d4d8a97267517c5e50074c2c819941andrepeatExpr :: CharParser (AnnoState.AnnoState st) CMD
6ae232055d4d8a97267517c5e50074c2c819941andrepeatExpr = do
6ae232055d4d8a97267517c5e50074c2c819941and lstring "repeat"
6ae232055d4d8a97267517c5e50074c2c819941and statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
6ae232055d4d8a97267517c5e50074c2c819941and lstring "until"
6ae232055d4d8a97267517c5e50074c2c819941and cstr <- aFormula
6ae232055d4d8a97267517c5e50074c2c819941and return $ Repeat cstr $ map AS_Anno.item statements
6ae232055d4d8a97267517c5e50074c2c819941andsingleCase :: CharParser (AnnoState.AnnoState st) (EXPRESSION, [CMD])
6ae232055d4d8a97267517c5e50074c2c819941andsingleCase =
6ae232055d4d8a97267517c5e50074c2c819941and let p1 = lstring "else" >> return (mkPredefOp OP_true [])
6ae232055d4d8a97267517c5e50074c2c819941and lstring "case"
6ae232055d4d8a97267517c5e50074c2c819941and cond <- choice [try p1, aFormula]
6ae232055d4d8a97267517c5e50074c2c819941and lstring ":"
6ae232055d4d8a97267517c5e50074c2c819941and statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
6ae232055d4d8a97267517c5e50074c2c819941and return (cond, map AS_Anno.item statements)
6ae232055d4d8a97267517c5e50074c2c819941andcaseExpr :: CharParser (AnnoState.AnnoState st) CMD
6ae232055d4d8a97267517c5e50074c2c819941andcaseExpr = many1 singleCase >-> Cond << lstring "end"
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * parser spec entries
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for operator declarations: example: operator a,b,c
6ae232055d4d8a97267517c5e50074c2c819941andopItem :: CharParser st OP_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andopItem = do
6ae232055d4d8a97267517c5e50074c2c819941and Lexer.keySign (lexemeParser (tryString "operator"))
6ae232055d4d8a97267517c5e50074c2c819941and vars <- sepBy1 identifier pComma
6ae232055d4d8a97267517c5e50074c2c819941and return $ Op_item vars nullRange
6ae232055d4d8a97267517c5e50074c2c819941and-- | Parser for variable declarations: example: vars x,y in {1,2}; z in [-1,1]
6ae232055d4d8a97267517c5e50074c2c819941andvarItems :: CharParser st [VAR_ITEM]
6ae232055d4d8a97267517c5e50074c2c819941andvarItems = oneOfKeys ["vars", "var"] >> sepBy1 varItem pSemi
6ae232055d4d8a97267517c5e50074c2c819941and-- | Parser for a variable declaration: example: vars x,y in {1,2}
6ae232055d4d8a97267517c5e50074c2c819941andvarItem :: CharParser st VAR_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andvarItem = do
6ae232055d4d8a97267517c5e50074c2c819941and vars <- sepBy1 identifier pComma
6ae232055d4d8a97267517c5e50074c2c819941and oneOfKeys ["in"]
6ae232055d4d8a97267517c5e50074c2c819941and dom <- parseDomain
6ae232055d4d8a97267517c5e50074c2c819941and return $ Var_item vars dom nullRange
6ae232055d4d8a97267517c5e50074c2c819941andparseDomain :: CharParser st Domain
6ae232055d4d8a97267517c5e50074c2c819941andparseDomain = do
6ae232055d4d8a97267517c5e50074c2c819941and lp <- lexemeParser $ oneOf "{[]"
6ae232055d4d8a97267517c5e50074c2c819941and gcl <- sepBy1 (signednumber >-> either GCI GCR . fst) pComma
6ae232055d4d8a97267517c5e50074c2c819941and rp <- lexemeParser $ oneOf "[]}"
6ae232055d4d8a97267517c5e50074c2c819941and let f o c = case gcl of
6ae232055d4d8a97267517c5e50074c2c819941and [lb, rb] -> return $ IntVal (lb, o) (rb, c)
6ae232055d4d8a97267517c5e50074c2c819941and _ -> parseError "parseDomain: incorrect interval-list"
6ae232055d4d8a97267517c5e50074c2c819941and case [lp, rp] of
6ae232055d4d8a97267517c5e50074c2c819941and "{}" -> return $ Set gcl
6ae232055d4d8a97267517c5e50074c2c819941and "[]" -> f True True
6ae232055d4d8a97267517c5e50074c2c819941and "[[" -> f True False
6ae232055d4d8a97267517c5e50074c2c819941and "][" -> f False False
6ae232055d4d8a97267517c5e50074c2c819941and "]]" -> f False True
6ae232055d4d8a97267517c5e50074c2c819941and _ -> parseError "parseDomain: malformed domain parens"
6ae232055d4d8a97267517c5e50074c2c819941and-- | Toplevel parser for basic specs
6ae232055d4d8a97267517c5e50074c2c819941andbasicSpec :: AnnoState.AParser st BASIC_SPEC
6ae232055d4d8a97267517c5e50074c2c819941andbasicSpec =
6ae232055d4d8a97267517c5e50074c2c819941and AnnoState.annosParser parseBasicItems >-> Basic_spec
6ae232055d4d8a97267517c5e50074c2c819941and <|> (Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))
6ae232055d4d8a97267517c5e50074c2c819941and-- | Parser for basic items
6ae232055d4d8a97267517c5e50074c2c819941andparseBasicItems :: AnnoState.AParser st BASIC_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andparseBasicItems = parseOpDecl <|> parseVarDecl <|> parseAxItems
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for predicate declarations
6ae232055d4d8a97267517c5e50074c2c819941andparseOpDecl :: AnnoState.AParser st BASIC_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andparseOpDecl = opItem >-> Op_decl
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for predicate declarations
6ae232055d4d8a97267517c5e50074c2c819941andparseVarDecl :: AnnoState.AParser st BASIC_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andparseVarDecl = varItems >-> Var_decls
6ae232055d4d8a97267517c5e50074c2c819941and-- | parser for Axiom_item
6ae232055d4d8a97267517c5e50074c2c819941andparseAxItems :: AnnoState.AParser st BASIC_ITEM
6ae232055d4d8a97267517c5e50074c2c819941andparseAxItems = do
6ae232055d4d8a97267517c5e50074c2c819941and cmd <- (AnnoState.allAnnoParser command)
6ae232055d4d8a97267517c5e50074c2c819941and return $ Axiom_item cmd
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- * parser for symbol maps etc.
6ae232055d4d8a97267517c5e50074c2c819941and-- ---------------------------------------------------------------------------
6ae232055d4d8a97267517c5e50074c2c819941and-- | parsing a prop symbol
6ae232055d4d8a97267517c5e50074c2c819941andsymb :: GenParser Char st SYMB
6ae232055d4d8a97267517c5e50074c2c819941andsymb = identifier >-> Symb_id
6ae232055d4d8a97267517c5e50074c2c819941and-- | parsing one symbol or a mapping of one to a second symbol
6ae232055d4d8a97267517c5e50074c2c819941andsymbMap :: GenParser Char st SYMB_OR_MAP
6ae232055d4d8a97267517c5e50074c2c819941andsymbMap = do
6ae232055d4d8a97267517c5e50074c2c819941and do f <- pToken $ toKey mapsTo
6ae232055d4d8a97267517c5e50074c2c819941and return (Symb_map s t $ tokPos f)
6ae232055d4d8a97267517c5e50074c2c819941and <|> return (Symb s)
6ae232055d4d8a97267517c5e50074c2c819941and-- | Parse a list of comma separated symbols.
6ae232055d4d8a97267517c5e50074c2c819941andsymbItems :: GenParser Char st SYMB_ITEMS
6ae232055d4d8a97267517c5e50074c2c819941andsymbItems = do
6ae232055d4d8a97267517c5e50074c2c819941and (is, ps) <- symbs
6ae232055d4d8a97267517c5e50074c2c819941and return (Symb_items is $ catRange ps)
4aa603e6448b99f9371397d439795c91a93637eand-- | parse a comma separated list of symbols
51b60896224b408a35684bd6ec0fafe5e4abe322rbowensymbs :: GenParser Char st ([SYMB], [Token])
4aa603e6448b99f9371397d439795c91a93637eand do c <- commaT `followedWith` symb
51b60896224b408a35684bd6ec0fafe5e4abe322rbowen (is, ps) <- symbs
6ae232055d4d8a97267517c5e50074c2c819941and return (s : is, c : ps)
6ae232055d4d8a97267517c5e50074c2c819941and <|> return ([s], [])
6ae232055d4d8a97267517c5e50074c2c819941and-- | parse a list of symbol mappings
6ae232055d4d8a97267517c5e50074c2c819941andsymbMapItems :: GenParser Char st SYMB_MAP_ITEMS
6ae232055d4d8a97267517c5e50074c2c819941andsymbMapItems = do
6ae232055d4d8a97267517c5e50074c2c819941and (is, ps) <- symbMaps
6ae232055d4d8a97267517c5e50074c2c819941and return (Symb_map_items is $ catRange ps)
6ae232055d4d8a97267517c5e50074c2c819941and-- | parse a comma separated list of symbol mappings
6ae232055d4d8a97267517c5e50074c2c819941andsymbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])
6ae232055d4d8a97267517c5e50074c2c819941andsymbMaps = do
6ae232055d4d8a97267517c5e50074c2c819941and s <- symbMap
6ae232055d4d8a97267517c5e50074c2c819941and do c <- commaT `followedWith` symb
6ae232055d4d8a97267517c5e50074c2c819941and (is, ps) <- symbMaps
6ae232055d4d8a97267517c5e50074c2c819941and return (s : is, c : ps)
6ae232055d4d8a97267517c5e50074c2c819941and <|> return ([s], [])
6ae232055d4d8a97267517c5e50074c2c819941andparseCommand :: String -> Maybe CMD
6ae232055d4d8a97267517c5e50074c2c819941andparseCommand inp =
6ae232055d4d8a97267517c5e50074c2c819941and case runParser command (AnnoState.emptyAnnos ()) "" inp of
6ae232055d4d8a97267517c5e50074c2c819941and Left _ -> Nothing
6ae232055d4d8a97267517c5e50074c2c819941and Right s -> Just s
6ae232055d4d8a97267517c5e50074c2c819941andparseExpression :: OpInfoMap -> String -> Maybe EXPRESSION
6ae232055d4d8a97267517c5e50074c2c819941andparseExpression st inp =
6ae232055d4d8a97267517c5e50074c2c819941and case runParser formulaorexpression st "" inp of
6ae232055d4d8a97267517c5e50074c2c819941and Left _ -> Nothing
6ae232055d4d8a97267517c5e50074c2c819941and Right s -> Just s