Parse_AS_Basic.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
4632N/A{-# LANGUAGE TypeSynonymInstances #-}
4632N/A{- |
4632N/AModule : ./CSL/Parse_AS_Basic.hs
4632N/ADescription : Parser for basic specs
4632N/ACopyright : (c) Dominik Dietrich, DFKI Bremen 2010
4632N/ALicense : GPLv2 or higher, see LICENSE.txt
4632N/A
4632N/AMaintainer : dominik.dietrich@dfki.de
4632N/AStability : experimental
4632N/APortability : non-portable
4632N/A
4632N/AParser for abstract syntax for CSL
4632N/A-}
4632N/A
4632N/Amodule CSL.Parse_AS_Basic where
4632N/A
4632N/Aimport qualified Common.AnnoState as AnnoState
4632N/Aimport Common.Id as Id
4632N/Aimport Common.Keywords as Keywords
4632N/Aimport Common.Lexer as Lexer
4632N/Aimport Common.Parsec
4632N/Aimport Common.AS_Annotation as AS_Anno
4632N/Aimport Common.GlobalAnnotations (PrefixMap)
4632N/A
4632N/Aimport CSL.AS_BASIC_CSL
4632N/Aimport CSL.ASUtils
4632N/Aimport CSL.Print_AS ()
4632N/Aimport CSL.Keywords
4632N/Aimport CSL.TreePO
4632N/A
4632N/Aimport Numeric
4632N/Aimport Data.Char
4632N/A
4632N/Aimport qualified Data.Set as Set
4632N/A
4632N/Aimport Text.ParserCombinators.Parsec as Parsec
4632N/Aimport Text.ParserCombinators.Parsec.Error
4632N/Aimport Control.Monad
4632N/A
4632N/A-- TODO: extract range information for the basic term and command types
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * Interface to the syntax class
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/AparseBasicSpec :: Maybe (PrefixMap -> AnnoState.AParser st BASIC_SPEC)
4632N/AparseBasicSpec = Just (const basicSpec)
4632N/A
4632N/AparseSymbItems :: Maybe (GenParser Char st SYMB_ITEMS)
4632N/AparseSymbItems = Just symbItems
4632N/A
4632N/AparseSymbMapItems :: Maybe (GenParser Char st SYMB_MAP_ITEMS)
4632N/AparseSymbMapItems = Just symbMapItems
4632N/A
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * Parser utils
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A
4632N/AaddToPosition :: SourcePos -- ^ original position
4632N/A -> SourcePos -- ^ relative position
4632N/A -> SourcePos -- ^ new position
4632N/AaddToPosition sp1 sp2
4632N/A | Parsec.sourceLine sp2 == 1 =
4632N/A setSourceColumn sp1 $
4632N/A Parsec.sourceColumn sp1 + Parsec.sourceColumn sp2 - 1
4632N/A | otherwise =
4632N/A setSourceColumn (setSourceLine sp1
4632N/A $ Parsec.sourceLine sp1 + Parsec.sourceLine sp2 - 1)
4632N/A $ Parsec.sourceColumn sp2
4632N/A
4632N/AposInputParser :: a -> GenParser tok st (a, SourcePos, [tok], st)
4632N/AposInputParser x = do
4632N/A pos <- getPosition
4632N/A inp <- getInput
4632N/A st <- getState
4632N/A return (x, pos, inp, st)
4632N/A
4632N/A
4632N/A{- Tests for subparser
4632N/Alet p1 = getState >>= many1 . string
4632N/ArunParser (string "h" >> runSubParser p1 "\n" "sourcename" >>= posInputParser) () "k" "h\n\nghurra"
4632N/A-}
4632N/ArunSubParser :: GenParser tok st a -> st -> SourceName
4632N/A -> GenParser tok st' (Either ParseError (st, a))
4632N/ArunSubParser sp st sn = do
4632N/A -- save the current state
4632N/A pos <- getPosition
4632N/A inp <- getInput
4632N/A case runParser (sp >>= posInputParser) st sn inp of
4632N/A Left err -> return $ Left err
4632N/A Right (x, pos', inp', st') -> do
4632N/A setPosition $ addToPosition pos pos'
4632N/A setInput inp'
4632N/A return $ Right (st', x)
4632N/A
4632N/A
4632N/Ainstance OperatorState (AnnoState.AnnoState st) where
4632N/A lookupOperator _ = lookupOperator ()
4632N/A lookupBinder _ = lookupBinder ()
4632N/A
4632N/Adata OpVarState a = OpVarState a (Set.Set String)
4632N/A
4632N/Ainstance OperatorState a => OperatorState (OpVarState a) where
4632N/A lookupOperator (OpVarState x _) = lookupOperator x
4632N/A lookupBinder (OpVarState x _) = lookupBinder x
4632N/A addVar (OpVarState st s) x = OpVarState st $ Set.insert x s
4632N/A isVar (OpVarState _ s) x = Set.member x s
4632N/A
4632N/A
4632N/A-- call opvar-state-subparser on given state
4632N/ArunWithVars :: OperatorState a => [String] -> CharParser (OpVarState a) res
4632N/A -> CharParser a res
4632N/ArunWithVars l p = do
4632N/A st <- getState
4632N/A res <- runSubParser p (OpVarState st $ Set.fromList l) ""
4632N/A case res of
4632N/A Left err -> parseError $ unlines $ map messageString $ errorMessages err
4632N/A Right (_, x) -> return x
4632N/A
4632N/A-- TEST: for subparser...
4632N/A
4632N/A
4632N/AparseError :: String -> CharParser st a
4632N/AparseError s = do
4632N/A p <- getPosition
4632N/A return $ error
4632N/A $ concat [ "Parse error at line: ", show (Parsec.sourceLine p)
4632N/A , " col: ", show (Parsec.sourceColumn p), "\n", s]
4632N/A
4632N/ApComma :: CharParser st String
4632N/ApComma = lexemeParser $ string ","
4632N/A
4632N/ApSemi :: CharParser st String
4632N/ApSemi = lexemeParser $ string ";"
4632N/A
4632N/Alstring :: String -> CharParser st String
4632N/Alstring = lexemeParser . string
4632N/A
4632N/A-- | parser for symbols followed by whitechars
4632N/AlexemeParser :: CharParser st a -> CharParser st a
4632N/AlexemeParser = (<< skip)
4632N/A
4632N/AgetOpName :: String -> [OPNAME] -> OPNAME
4632N/AgetOpName s l = f l
4632N/A where f (x : xs) = if s == show x then x else f xs
4632N/A f [] = error $ "getOpName: no op found for " ++ s ++ " in " ++ show l
4632N/A
4632N/AmkFromOps :: [OPNAME] -> String -> [EXPRESSION] -> EXPRESSION
4632N/AmkFromOps l s = mkPredefOp (getOpName s l)
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * Parser for Expressions
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A
4632N/A{- | parsing of identifiers. an identifier is a letter followed by
4632N/A letters, numbers, or _, but not a keyword -}
4632N/Aidentifier :: CharParser st Id.Token
4632N/Aidentifier =
4632N/A lexemeParser $ Lexer.pToken $ reserved allKeywords Lexer.scanAnyWords
4632N/A
4632N/Aprefixidentifier :: CharParser st Id.Token
4632N/Aprefixidentifier =
4632N/A lexemeParser $ Lexer.pToken $ Lexer.scanAnySigns <|> Lexer.scanAnyWords
4632N/A
4632N/A-- | parses a possibly signed number to an EXPRESSION
4632N/AsignednumberExp :: CharParser st EXPRESSION
4632N/AsignednumberExp =
4632N/A let f (eN, rg) = either (flip Int rg) (flip Rat rg . readRat) eN
4632N/A in signednumber >-> f
4632N/A
4632N/A-- | parses a possibly signed number (both integers and floats)
4632N/Asignednumber :: CharParser st (Either APInt String, Range)
4632N/Asignednumber =
4632N/A let f c x = return (c $ tokStr x, tokPos x)
4632N/A g x | isFloating x = f Right x
4632N/A | otherwise = f (Left . read) x
4632N/A in Lexer.pToken Lexer.scanFloatExt >>= g
4632N/A
4632N/AreadRat :: String -> APFloat
4632N/AreadRat s = case readFloat fls of
4632N/A [(r, "")] -> withSgn r
4632N/A _ -> error $ "readRat: cannot read float " ++ s
4632N/A where withSgn x = if sgn then - x else x
4632N/A (sgn, fls) = case dropWhile isSpace s of
4632N/A '-' : s' -> (True, s')
4632N/A _ -> (False, s)
4632N/A
4632N/AreadDbl :: String -> Double
4632N/AreadDbl = read
4632N/A
4632N/A{- | The version in Common.Lexer is not compatible with floating point numbers
4632N/Awhich may start with ".". This one does it.
4632N/AThis version is still not compatible with -! -}
4632N/AkeySignNumCompat :: CharParser st a -> CharParser st a
4632N/AkeySignNumCompat = try . (<< notFollowedBy (oneOf signNumCompatChars))
4632N/A
4632N/AsignNumCompatChars :: String
4632N/AsignNumCompatChars = "!#$&*+-/:<=>?@\\^|~" ++
4632N/A "\161\162\163\167\169\172\176\177\178\179\181\182\183\185\191\215\247"
4632N/A
4632N/AoneOfKeys :: [String] -> CharParser st String
4632N/AoneOfKeys l = lexemeParser $ keySignNumCompat $ choice $ map tryString l
4632N/A
4632N/Aplusmin :: OperatorState st => CharParser st EXPRESSION
4632N/Aplusmin = do
4632N/A let ops = [OP_plus, OP_minus]
4632N/A exp1 <- factor
4632N/A exps <- many $ pair (oneOfKeys $ map show ops) factor
4632N/A return $ if null exps then exp1
4632N/A else foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps
4632N/A
4632N/A-- | parse a product of basic expressions
4632N/Afactor :: OperatorState st => CharParser st EXPRESSION
4632N/Afactor = do
4632N/A let ops = [OP_mult, OP_div]
4632N/A exp1 <- expexp
4632N/A exps <- many $ pair (oneOfKeys $ map show ops) expexp
4632N/A return $ if null exps then exp1
4632N/A else foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps
4632N/A
4632N/A-- | parse a sequence of exponentiations
4632N/Aexpexp :: OperatorState st => CharParser st EXPRESSION
4632N/Aexpexp = do
4632N/A exp1 <- expatom
4632N/A exps <- many $ pair (oneOfKeys ["**", "^"]) expatom
4632N/A return $ if null exps then exp1
4632N/A else foldl (\ a b -> mkPredefOp OP_pow [a, snd b]) exp1 exps
4632N/A
4632N/A-- | parse a basic expression
4632N/Aexpatom :: OperatorState st => CharParser st EXPRESSION
4632N/Aexpatom = try signednumberExp <|> (oParenT >> plusmin << cParenT)
4632N/A <|> listexp <|> intervalexp <|> expsymbol
4632N/A
4632N/Aexpsymbol :: OperatorState st => CharParser st EXPRESSION
4632N/Aexpsymbol = do
4632N/A ident <- prefixidentifier -- EXTENDED
4632N/A ep <- option ([], [])
4632N/A $ oBracketT >> Lexer.separatedBy extparam pComma << cBracketT
4632N/A exps <- option ([], [])
4632N/A $ oParenT >> Lexer.separatedBy formulaorexpression pComma << cParenT
4632N/A st <- getState
4632N/A case mkAndAnalyzeOp' True st (tokStr ident) (fst ep) (fst exps)
4632N/A $ getRange ident of
4632N/A Left s -> parseError $ "expsymbol at op " ++ tokStr ident
4632N/A ++ show (fst exps) ++ ": " ++ s
4632N/A Right e -> return e
4632N/A
4632N/Aopdecl :: OperatorState st => CharParser st OpDecl
4632N/Aopdecl = do
4632N/A ident <- prefixidentifier -- EXTENDED
4632N/A ep <- option ([], [])
4632N/A $ oBracketT >> Lexer.separatedBy extparam pComma << cBracketT
4632N/A args <- option ([], [])
4632N/A $ oParenT >> Lexer.separatedBy prefixidentifier pComma << cParenT
4632N/A let vdl = map (flip VarDecl Nothing) $ fst args
4632N/A return $ OpDecl (SimpleConstant $ tokStr ident) (fst ep) vdl $ tokPos ident
4632N/A
4632N/A-- | parses a list expression
4632N/Alistexp :: OperatorState st => CharParser st EXPRESSION
4632N/Alistexp = do
4632N/A keySignNumCompat $ string "{"
4632N/A elems <- Lexer.separatedBy formulaorexpression pComma
4632N/A keySignNumCompat $ string "}"
4632N/A return (List (fst elems) nullRange)
4632N/A
4632N/Aintervalexp :: CharParser st EXPRESSION
4632N/Aintervalexp = do
4632N/A nums <- lstring "[" >> Lexer.separatedBy signednumber pComma << lstring "]"
4632N/A let getFloat = either fromInteger readDbl
4632N/A case fst nums of
4632N/A [(x, rg1), (y, rg2)] -> return $ Interval (getFloat x) (getFloat y) $ Range
4632N/A $ joinRanges $ map rangeToList [rg1, rg2]
4632N/A _ -> parseError
4632N/A "intervalexp: Parse error: interval with other than two arguments"
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- ** parser for extended parameter, e.g., [I=0,...]
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/Aextparam :: CharParser st EXTPARAM
4632N/Aextparam = do
4632N/A i <- identifier
4632N/A liftM2 (EP i) (oneOfKeys ["=", "<=", ">=", "!=", "<", ">", "-|"])
4632N/A $ option 0 $ signednumber
4632N/A >-> either id (error "extparam: floats not supported") . fst
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * parser for formulas
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/AparseVarList :: CharParser st EXPRESSION
4632N/AparseVarList = do
4632N/A Lexer.keySign (string "{")
4632N/A elems <- Lexer.separatedBy parseVar pComma
4632N/A Lexer.keySign (string "}")
4632N/A return (List (fst elems) nullRange)
4632N/A
4632N/AparseVar :: CharParser st EXPRESSION
4632N/AparseVar = do
4632N/A ident <- identifier
4632N/A return (Var ident)
4632N/A
4632N/A
4632N/AquantFormula :: OperatorState st => OPNAME -> CharParser st EXPRESSION
4632N/A -- TODO: static analysis requires probably a better representation of quantifiers
4632N/AquantFormula q = do
4632N/A Lexer.keySign (string $ show q)
4632N/A oParenT
4632N/A vars <- parseVar <|> parseVarList
4632N/A pComma
4632N/A expr <- formulaorexpression
4632N/A cParenT
4632N/A return (mkPredefOp q [vars, expr])
4632N/A
4632N/A
4632N/A-- | parser for atoms
4632N/AtruefalseFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AtruefalseFormula =
4632N/A do
4632N/A lexemeParser (Lexer.keyWord (tryString $ show OP_true))
4632N/A return (mkPredefOp OP_true [])
4632N/A <|>
4632N/A do
4632N/A lexemeParser (Lexer.keyWord (tryString $ show OP_false))
4632N/A return (mkPredefOp OP_false [])
4632N/A <|> quantFormula OP_ex <|> quantFormula OP_all
4632N/A
4632N/A-- | parser for predicates
4632N/ApredFormula :: OperatorState st => CharParser st EXPRESSION
4632N/ApredFormula = do
4632N/A let ops = [ OP_leq, OP_geq, OP_neq, OP_eq, OP_lt, OP_gt ]
4632N/A exp1 <- plusmin
4632N/A mExp2 <- optionMaybe
4632N/A $ pair (oneOfKeys (map show $ take 3 ops) -- the first 3 print as 2-chars
4632N/A <|> lexemeParser (single $ oneOf "=<>")) plusmin
4632N/A case mExp2 of
4632N/A Just (op, exp2) -> return $ mkFromOps ops op [exp1, exp2]
4632N/A _ -> return exp1
4632N/A
4632N/AatomicFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AatomicFormula = truefalseFormula <|> predFormula <|> parenFormula
4632N/A
4632N/A-- | parser for formulas
4632N/AaFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AaFormula = try negFormula <|> impOrFormula
4632N/A
4632N/AnegFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AnegFormula = do
4632N/A lexemeParser (Lexer.keyWord (tryString $ show OP_not))
4632N/A f <- atomicFormula
4632N/A return (mkPredefOp OP_not [f])
4632N/A
4632N/A-- | parses a formula within brackets
4632N/AparenFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AparenFormula = do
4632N/A lexemeParser oParenT
4632N/A f <- aFormula
4632N/A lexemeParser cParenT
4632N/A return f
4632N/A
4632N/A-- | parser for implications and ors (same precedence)
4632N/AimpOrFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AimpOrFormula = do
4632N/A let ops = [ OP_or, OP_impl ]
4632N/A f1 <- andFormula
4632N/A opfs <- many $ pair (lexemeParser $ Lexer.keyWord
4632N/A $ tryString (show OP_or) <|> tryString (show OP_impl))
4632N/A andFormula
4632N/A return $ if null opfs then f1
4632N/A else foldl (\ a (op, b) -> mkFromOps ops op [a, b]) f1 opfs
4632N/A
4632N/A-- | a parser for and sequence of and formulas
4632N/AandFormula :: OperatorState st => CharParser st EXPRESSION
4632N/AandFormula = do
4632N/A f1 <- atomicFormula
4632N/A opfs <- many $ pair (lexemeParser $ keyWord $ tryString $ show OP_and)
4632N/A atomicFormula
4632N/A return $ if null opfs then f1
4632N/A else foldl (\ b a -> (mkPredefOp OP_and [b, snd a])) f1 opfs
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * Parser for Commands
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A
4632N/Aformulaorexpression :: OperatorState st => CharParser st EXPRESSION
4632N/Aformulaorexpression = try aFormula <|> plusmin
4632N/A
4632N/A-- | parser for commands
4632N/Acommand :: CharParser (AnnoState.AnnoState st) CMD
4632N/Acommand = reduceCommand <|> try assignment <|> repeatExpr <|> caseExpr
4632N/A <|> sequenceExpr <|> constraint
4632N/A
4632N/AreduceCommand :: OperatorState st => CharParser st CMD
4632N/AreduceCommand = do
4632N/A cmd <- lexemeParser $ Lexer.keyWord $ choice $ map tryString
4632N/A ["solve", "simplify", "divide", "int", "rlqe", "factorize", "print"]
4632N/A oParenT
4632N/A arg1 <- formulaorexpression
4632N/A args <- many $ pComma >> formulaorexpression
4632N/A cParenT
4632N/A return $ Cmd cmd $ arg1 : args
4632N/A
4632N/Aassignment :: OperatorState st => CharParser st CMD
4632N/Aassignment = do
4632N/A ident@(OpDecl _ _ vdl _) <- opdecl
4632N/A lexemeParser $ choice [tryString ":=", tryString "="]
4632N/A exp' <- runWithVars (map varDeclName vdl) plusmin
4632N/A return $ Ass ident exp'
4632N/A
4632N/Aconstraint :: OperatorState st => CharParser st CMD
4632N/Aconstraint = do
4632N/A exp' <- try aFormula
4632N/A case exp' of
4632N/A Op {} ->
4632N/A return $ Cmd "constraint" [exp']
4632N/A _ -> fail "Malformed constraint"
4632N/A
4632N/A
4632N/AsequenceExpr :: CharParser (AnnoState.AnnoState st) CMD
4632N/AsequenceExpr = do
4632N/A lstring "sequence"
4632N/A statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
4632N/A lstring "end"
4632N/A return $ Sequence $ map AS_Anno.item statements
4632N/A
4632N/ArepeatExpr :: CharParser (AnnoState.AnnoState st) CMD
4632N/ArepeatExpr = do
4632N/A lstring "repeat"
4632N/A statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
4632N/A lstring "until"
4632N/A cstr <- aFormula
4632N/A return $ Repeat cstr $ map AS_Anno.item statements
4632N/A
4632N/AsingleCase :: CharParser (AnnoState.AnnoState st) (EXPRESSION, [CMD])
4632N/AsingleCase =
4632N/A let p1 = lstring "else" >> return (mkPredefOp OP_true [])
4632N/A in do
4632N/A lstring "case"
4632N/A cond <- choice [try p1, aFormula]
4632N/A lstring ":"
4632N/A statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)
4632N/A return (cond, map AS_Anno.item statements)
4632N/A
4632N/A
4632N/AcaseExpr :: CharParser (AnnoState.AnnoState st) CMD
4632N/AcaseExpr = many1 singleCase >-> Cond << lstring "end"
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * parser spec entries
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A
4632N/A-- | parser for operator declarations: example: operator a,b,c
4632N/AopItem :: CharParser st OP_ITEM
4632N/AopItem = do
4632N/A Lexer.keySign (lexemeParser (tryString "operator"))
4632N/A vars <- sepBy1 identifier pComma
4632N/A return $ Op_item vars nullRange
4632N/A
4632N/A
4632N/A-- | Parser for variable declarations: example: vars x,y in {1,2}; z in [-1,1]
4632N/AvarItems :: CharParser st [VAR_ITEM]
4632N/AvarItems = oneOfKeys ["vars", "var"] >> sepBy1 varItem pSemi
4632N/A
4632N/A-- | Parser for a variable declaration: example: vars x,y in {1,2}
4632N/AvarItem :: CharParser st VAR_ITEM
4632N/AvarItem = do
4632N/A vars <- sepBy1 identifier pComma
4632N/A oneOfKeys ["in"]
4632N/A dom <- parseDomain
4632N/A return $ Var_item vars dom nullRange
4632N/A
4632N/A
4632N/A{- | Parser for extended parameter declarations:
4632N/Aexample: I in [1,2]; -}
4632N/AepDecl :: CharParser st (Id.Token, EPDomain)
4632N/AepDecl = do
4632N/A epId <- identifier
4632N/A oneOfKeys ["in"]
4632N/A parseEPDomain >-> (,) epId
4632N/A
4632N/A{- | Parser for extended parameter default values and domain variable
4632N/Adeclarations: example: I = 1; n=2 -}
4632N/AepNumValAss :: CharParser st (Id.Token, APInt)
4632N/AepNumValAss = do
4632N/A epId <- identifier
4632N/A oneOfKeys ["="]
4632N/A getSignedNumber >-> (,) epId . read
4632N/A
4632N/A
4632N/AparseDomain :: CharParser st Domain
4632N/AparseDomain = do
4632N/A lp <- lexemeParser $ oneOf "{[]"
4632N/A gcl <- sepBy1 (signednumber >-> either GCI (GCR . readRat) . fst) pComma
4632N/A rp <- lexemeParser $ oneOf "[]}"
4632N/A let f o c = case gcl of
4632N/A [lb, rb] -> return $ IntVal (lb, o) (rb, c)
4632N/A _ -> parseError "parseDomain: incorrect interval-list"
4632N/A case [lp, rp] of
4632N/A "{}" -> return $ Set $ Set.fromList gcl
4632N/A "[]" -> f True True
4632N/A "[[" -> f True False
4632N/A "][" -> f False False
4632N/A "]]" -> f False True
4632N/A _ -> parseError "parseDomain: malformed domain parens"
4632N/A
4632N/AparseEPVal :: CharParser st EPVal
4632N/AparseEPVal = do
4632N/A mId <- optionMaybe identifier
4632N/A case mId of
4632N/A Just n -> return $ EPConstRef n
4632N/A _ -> getSignedNumber >-> EPVal . read
4632N/A
4632N/AparseEPDomain :: CharParser st EPDomain
4632N/AparseEPDomain = do
4632N/A lexemeParser $ string "["
4632N/A l <- parseEPVal
4632N/A pComma
4632N/A r <- parseEPVal
4632N/A lexemeParser $ string "]"
4632N/A return $ ClosedInterval l r
4632N/A
4632N/A
4632N/A-- | Toplevel parser for basic specs
4632N/AbasicSpec :: AnnoState.AParser st BASIC_SPEC
4632N/AbasicSpec =
4632N/A AnnoState.annosParser parseBasicItems >-> Basic_spec
4632N/A <|> (Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))
4632N/A
4632N/A-- | Parser for basic items
4632N/AparseBasicItems :: AnnoState.AParser st BASIC_ITEM
4632N/AparseBasicItems = parseOpDecl <|> parseVarDecl <|> parseEPDefValOrDomDecl
4632N/A <|> parseEPDecl <|> parseAxItems
4632N/A
4632N/A-- | parser for operator declarations
4632N/AparseOpDecl :: AnnoState.AParser st BASIC_ITEM
4632N/AparseOpDecl = opItem >-> Op_decl
4632N/A
4632N/A-- | parser for variable declarations
4632N/AparseVarDecl :: AnnoState.AParser st BASIC_ITEM
4632N/AparseVarDecl = varItems >-> Var_decls
4632N/A
4632N/A{- | parser for extended parameter declarations, one of:
4632N/Adefault value for an extended parameter (I=2)
4632N/Aa domain variable declaration (n=10) -}
4632N/AparseEPDefValOrDomDecl :: AnnoState.AParser st BASIC_ITEM
4632N/AparseEPDefValOrDomDecl = do
4632N/A lstring "set"
4632N/A mDef <- optionMaybe $ try $ lexemeParser $ string "default"
4632N/A case mDef of
4632N/A Nothing -> sepBy1 epNumValAss pSemi >-> EP_domdecl
4632N/A _ -> sepBy1 epNumValAss pSemi >-> EP_defval
4632N/A
4632N/A-- | parser for extended parameter declarations
4632N/AparseEPDecl :: AnnoState.AParser st BASIC_ITEM
4632N/AparseEPDecl = oneOfKeys ["eps", "ep"] >> sepBy1 epDecl pSemi >-> EP_decl
4632N/A
4632N/A-- | parser for Axiom_item
4632N/AparseAxItems :: AnnoState.AParser st BASIC_ITEM
4632N/AparseAxItems = do
4632N/A AnnoState.dotT
4632N/A cmd <- AnnoState.allAnnoParser command
4632N/A return $ Axiom_item cmd
4632N/A
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- * parser for symbol maps etc.
4632N/A
4632N/A-- ---------------------------------------------------------------------------
4632N/A
4632N/A-- | parsing a prop symbol
4632N/Asymb :: GenParser Char st SYMB
4632N/Asymb = identifier >-> Symb_id
4632N/A
4632N/A
4632N/A-- | parsing one symbol or a mapping of one to a second symbol
4632N/AsymbMap :: GenParser Char st SYMB_OR_MAP
4632N/AsymbMap = do
4632N/A s <- symb
4632N/A do f <- pToken $ toKey mapsTo
4632N/A t <- symb
4632N/A return (Symb_map s t $ tokPos f)
4632N/A <|> return (Symb s)
4632N/A
4632N/A-- | Parse a list of comma separated symbols.
4632N/AsymbItems :: GenParser Char st SYMB_ITEMS
4632N/AsymbItems = do
4632N/A (is, ps) <- symbs
4632N/A return (Symb_items is $ catRange ps)
4632N/A
4632N/A-- | parse a comma separated list of symbols
4632N/Asymbs :: GenParser Char st ([SYMB], [Token])
4632N/Asymbs = do
4632N/A s <- symb
4632N/A do c <- commaT `followedWith` symb
4632N/A (is, ps) <- symbs
4632N/A return (s : is, c : ps)
4632N/A <|> return ([s], [])
4632N/A
4632N/A-- | parse a list of symbol mappings
4632N/AsymbMapItems :: GenParser Char st SYMB_MAP_ITEMS
4632N/AsymbMapItems = do
4632N/A (is, ps) <- symbMaps
4632N/A return (Symb_map_items is $ catRange ps)
4632N/A
4632N/A-- | parse a comma separated list of symbol mappings
4632N/AsymbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])
4632N/AsymbMaps = do
4632N/A s <- symbMap
4632N/A do c <- commaT `followedWith` symb
4632N/A (is, ps) <- symbMaps
4632N/A return (s : is, c : ps)
4632N/A <|> return ([s], [])
4632N/A
4632N/AparseCommand :: String -> Maybe CMD
4632N/AparseCommand inp =
4632N/A case runParser command (AnnoState.emptyAnnos ()) "" inp of
4632N/A Left _ -> Nothing
4632N/A Right s -> Just s
4632N/A
4632N/AparseExpression :: OperatorState a => a -> String -> Maybe EXPRESSION
4632N/AparseExpression st inp =
4632N/A case runParser formulaorexpression st "" inp of
4632N/A Left _ -> Nothing
4632N/A Right s -> Just s
4632N/A