{-# LANGUAGE TypeSynonymInstances #-}

{- |

Module : ./CSL/Parse_AS_Basic.hs

Description : Parser for basic specs

Copyright : (c) Dominik Dietrich, DFKI Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : dominik.dietrich@dfki.de

Stability : experimental

Portability : non-portable

Parser for abstract syntax for CSL

-}

module CSL.Parse_AS_Basic where

import qualified Common.AnnoState as AnnoState

import Common.Id as Id

import Common.Keywords as Keywords

import Common.Lexer as Lexer

import Common.Parsec

import Common.AS_Annotation as AS_Anno

import Common.GlobalAnnotations (PrefixMap)

import CSL.AS_BASIC_CSL

import CSL.ASUtils

import CSL.Print_AS ()

import CSL.Keywords

import CSL.TreePO

import Numeric

import Data.Char

import qualified Data.Set as Set

import Text.ParserCombinators.Parsec as Parsec

import Text.ParserCombinators.Parsec.Error

import Control.Monad

-- TODO: extract range information for the basic term and command types

-- ---------------------------------------------------------------------------

-- * Interface to the syntax class

-- ---------------------------------------------------------------------------

parseBasicSpec :: Maybe (PrefixMap -> AnnoState.AParser st BASIC_SPEC)

parseBasicSpec = Just (const basicSpec)

parseSymbItems :: Maybe (GenParser Char st SYMB_ITEMS)

parseSymbItems = Just symbItems

parseSymbMapItems :: Maybe (GenParser Char st SYMB_MAP_ITEMS)

parseSymbMapItems = Just symbMapItems

-- ---------------------------------------------------------------------------

-- * Parser utils

-- ---------------------------------------------------------------------------

addToPosition :: SourcePos -- ^ original position

-> SourcePos -- ^ relative position

-> SourcePos -- ^ new position

addToPosition sp1 sp2

| Parsec.sourceLine sp2 == 1 =

setSourceColumn sp1 $

Parsec.sourceColumn sp1 + Parsec.sourceColumn sp2 - 1

| otherwise =

setSourceColumn (setSourceLine sp1

$ Parsec.sourceLine sp1 + Parsec.sourceLine sp2 - 1)

$ Parsec.sourceColumn sp2

posInputParser :: a -> GenParser tok st (a, SourcePos, [tok], st)

posInputParser x = do

pos <- getPosition

inp <- getInput

st <- getState

return (x, pos, inp, st)

{- Tests for subparser

let p1 = getState >>= many1 . string

runParser (string "h" >> runSubParser p1 "\n" "sourcename" >>= posInputParser) () "k" "h\n\nghurra"

-}

runSubParser :: GenParser tok st a -> st -> SourceName

-> GenParser tok st' (Either ParseError (st, a))

runSubParser sp st sn = do

-- save the current state

pos <- getPosition

inp <- getInput

case runParser (sp >>= posInputParser) st sn inp of

Left err -> return $ Left err

Right (x, pos', inp', st') -> do

setPosition $ addToPosition pos pos'

setInput inp'

return $ Right (st', x)

instance OperatorState (AnnoState.AnnoState st) where

lookupOperator _ = lookupOperator ()

lookupBinder _ = lookupBinder ()

data OpVarState a = OpVarState a (Set.Set String)

instance OperatorState a => OperatorState (OpVarState a) where

lookupOperator (OpVarState x _) = lookupOperator x

lookupBinder (OpVarState x _) = lookupBinder x

addVar (OpVarState st s) x = OpVarState st $ Set.insert x s

isVar (OpVarState _ s) x = Set.member x s

-- call opvar-state-subparser on given state

runWithVars :: OperatorState a => [String] -> CharParser (OpVarState a) res

-> CharParser a res

runWithVars l p = do

st <- getState

res <- runSubParser p (OpVarState st $ Set.fromList l) ""

case res of

Left err -> parseError $ unlines $ map messageString $ errorMessages err

Right (_, x) -> return x

-- TEST: for subparser...

parseError :: String -> CharParser st a

parseError s = do

p <- getPosition

return $ error

$ concat [ "Parse error at line: ", show (Parsec.sourceLine p)

, " col: ", show (Parsec.sourceColumn p), "\n", s]

pComma :: CharParser st String

pComma = lexemeParser $ string ","

pSemi :: CharParser st String

pSemi = lexemeParser $ string ";"

lstring :: String -> CharParser st String

lstring = lexemeParser . string

-- | parser for symbols followed by whitechars

lexemeParser :: CharParser st a -> CharParser st a

lexemeParser = (<< skip)

getOpName :: String -> [OPNAME] -> OPNAME

getOpName s l = f l

where f (x : xs) = if s == show x then x else f xs

f [] = error $ "getOpName: no op found for " ++ s ++ " in " ++ show l

mkFromOps :: [OPNAME] -> String -> [EXPRESSION] -> EXPRESSION

mkFromOps l s = mkPredefOp (getOpName s l)

-- ---------------------------------------------------------------------------

-- * Parser for Expressions

-- ---------------------------------------------------------------------------

{- | parsing of identifiers. an identifier is a letter followed by

letters, numbers, or _, but not a keyword -}

identifier :: CharParser st Id.Token

identifier =

lexemeParser $ Lexer.pToken $ reserved allKeywords Lexer.scanAnyWords

prefixidentifier :: CharParser st Id.Token

prefixidentifier =

lexemeParser $ Lexer.pToken $ Lexer.scanAnySigns <|> Lexer.scanAnyWords

-- | parses a possibly signed number to an EXPRESSION

signednumberExp :: CharParser st EXPRESSION

signednumberExp =

let f (eN, rg) = either (flip Int rg) (flip Rat rg . readRat) eN

in signednumber >-> f

-- | parses a possibly signed number (both integers and floats)

signednumber :: CharParser st (Either APInt String, Range)

signednumber =

let f c x = return (c $ tokStr x, tokPos x)

g x | isFloating x = f Right x

| otherwise = f (Left . read) x

in Lexer.pToken Lexer.scanFloatExt >>= g

readRat :: String -> APFloat

readRat s = case readFloat fls of

[(r, "")] -> withSgn r

_ -> error $ "readRat: cannot read float " ++ s

where withSgn x = if sgn then - x else x

(sgn, fls) = case dropWhile isSpace s of

'-' : s' -> (True, s')

_ -> (False, s)

readDbl :: String -> Double

readDbl = read

{- | The version in Common.Lexer is not compatible with floating point numbers

which may start with ".". This one does it.

This version is still not compatible with -! -}

keySignNumCompat :: CharParser st a -> CharParser st a

keySignNumCompat = try . (<< notFollowedBy (oneOf signNumCompatChars))

signNumCompatChars :: String

signNumCompatChars = "!#$&*+-/:<=>?@\\^|~" ++

"\161\162\163\167\169\172\176\177\178\179\181\182\183\185\191\215\247"

oneOfKeys :: [String] -> CharParser st String

oneOfKeys l = lexemeParser $ keySignNumCompat $ choice $ map tryString l

plusmin :: OperatorState st => CharParser st EXPRESSION

plusmin = do

let ops = [OP_plus, OP_minus]

exp1 <- factor

exps <- many $ pair (oneOfKeys $ map show ops) factor

return $ if null exps then exp1

else foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps

-- | parse a product of basic expressions

factor :: OperatorState st => CharParser st EXPRESSION

factor = do

let ops = [OP_mult, OP_div]

exp1 <- expexp

exps <- many $ pair (oneOfKeys $ map show ops) expexp

return $ if null exps then exp1

else foldl (\ a b -> mkFromOps ops (fst b) [a, snd b]) exp1 exps

-- | parse a sequence of exponentiations

expexp :: OperatorState st => CharParser st EXPRESSION

expexp = do

exp1 <- expatom

exps <- many $ pair (oneOfKeys ["**", "^"]) expatom

return $ if null exps then exp1

else foldl (\ a b -> mkPredefOp OP_pow [a, snd b]) exp1 exps

-- | parse a basic expression

expatom :: OperatorState st => CharParser st EXPRESSION

expatom = try signednumberExp <|> (oParenT >> plusmin << cParenT)

<|> listexp <|> intervalexp <|> expsymbol

expsymbol :: OperatorState st => CharParser st EXPRESSION

expsymbol = do

ident <- prefixidentifier -- EXTENDED

ep <- option ([], [])

$ oBracketT >> Lexer.separatedBy extparam pComma << cBracketT

exps <- option ([], [])

$ oParenT >> Lexer.separatedBy formulaorexpression pComma << cParenT

st <- getState

case mkAndAnalyzeOp' True st (tokStr ident) (fst ep) (fst exps)

$ getRange ident of

Left s -> parseError $ "expsymbol at op " ++ tokStr ident

++ show (fst exps) ++ ": " ++ s

Right e -> return e

opdecl :: OperatorState st => CharParser st OpDecl

opdecl = do

ident <- prefixidentifier -- EXTENDED

ep <- option ([], [])

$ oBracketT >> Lexer.separatedBy extparam pComma << cBracketT

args <- option ([], [])

$ oParenT >> Lexer.separatedBy prefixidentifier pComma << cParenT

let vdl = map (flip VarDecl Nothing) $ fst args

return $ OpDecl (SimpleConstant $ tokStr ident) (fst ep) vdl $ tokPos ident

-- | parses a list expression

listexp :: OperatorState st => CharParser st EXPRESSION

listexp = do

keySignNumCompat $ string "{"

elems <- Lexer.separatedBy formulaorexpression pComma

keySignNumCompat $ string "}"

return (List (fst elems) nullRange)

intervalexp :: CharParser st EXPRESSION

intervalexp = do

nums <- lstring "[" >> Lexer.separatedBy signednumber pComma << lstring "]"

let getFloat = either fromInteger readDbl

case fst nums of

[(x, rg1), (y, rg2)] -> return $ Interval (getFloat x) (getFloat y) $ Range

$ joinRanges $ map rangeToList [rg1, rg2]

_ -> parseError

"intervalexp: Parse error: interval with other than two arguments"

-- ---------------------------------------------------------------------------

-- ** parser for extended parameter, e.g., [I=0,...]

-- ---------------------------------------------------------------------------

extparam :: CharParser st EXTPARAM

extparam = do

i <- identifier

liftM2 (EP i) (oneOfKeys ["=", "<=", ">=", "!=", "<", ">", "-|"])

$ option 0 $ signednumber

>-> either id (error "extparam: floats not supported") . fst

-- ---------------------------------------------------------------------------

-- * parser for formulas

-- ---------------------------------------------------------------------------

parseVarList :: CharParser st EXPRESSION

parseVarList = do

Lexer.keySign (string "{")

elems <- Lexer.separatedBy parseVar pComma

Lexer.keySign (string "}")

return (List (fst elems) nullRange)

parseVar :: CharParser st EXPRESSION

parseVar = do

ident <- identifier

return (Var ident)

quantFormula :: OperatorState st => OPNAME -> CharParser st EXPRESSION

-- TODO: static analysis requires probably a better representation of quantifiers

quantFormula q = do

Lexer.keySign (string $ show q)

oParenT

vars <- parseVar <|> parseVarList

pComma

expr <- formulaorexpression

cParenT

return (mkPredefOp q [vars, expr])

-- | parser for atoms

truefalseFormula :: OperatorState st => CharParser st EXPRESSION

truefalseFormula =

do

lexemeParser (Lexer.keyWord (tryString $ show OP_true))

return (mkPredefOp OP_true [])

<|>

do

lexemeParser (Lexer.keyWord (tryString $ show OP_false))

return (mkPredefOp OP_false [])

<|> quantFormula OP_ex <|> quantFormula OP_all

-- | parser for predicates

predFormula :: OperatorState st => CharParser st EXPRESSION

predFormula = do

let ops = [ OP_leq, OP_geq, OP_neq, OP_eq, OP_lt, OP_gt ]

exp1 <- plusmin

mExp2 <- optionMaybe

$ pair (oneOfKeys (map show $ take 3 ops) -- the first 3 print as 2-chars

<|> lexemeParser (single $ oneOf "=<>")) plusmin

case mExp2 of

Just (op, exp2) -> return $ mkFromOps ops op [exp1, exp2]

_ -> return exp1

atomicFormula :: OperatorState st => CharParser st EXPRESSION

atomicFormula = truefalseFormula <|> predFormula <|> parenFormula

-- | parser for formulas

aFormula :: OperatorState st => CharParser st EXPRESSION

aFormula = try negFormula <|> impOrFormula

negFormula :: OperatorState st => CharParser st EXPRESSION

negFormula = do

lexemeParser (Lexer.keyWord (tryString $ show OP_not))

f <- atomicFormula

return (mkPredefOp OP_not [f])

-- | parses a formula within brackets

parenFormula :: OperatorState st => CharParser st EXPRESSION

parenFormula = do

lexemeParser oParenT

f <- aFormula

lexemeParser cParenT

return f

-- | parser for implications and ors (same precedence)

impOrFormula :: OperatorState st => CharParser st EXPRESSION

impOrFormula = do

let ops = [ OP_or, OP_impl ]

f1 <- andFormula

opfs <- many $ pair (lexemeParser $ Lexer.keyWord

$ tryString (show OP_or) <|> tryString (show OP_impl))

andFormula

return $ if null opfs then f1

else foldl (\ a (op, b) -> mkFromOps ops op [a, b]) f1 opfs

-- | a parser for and sequence of and formulas

andFormula :: OperatorState st => CharParser st EXPRESSION

andFormula = do

f1 <- atomicFormula

opfs <- many $ pair (lexemeParser $ keyWord $ tryString $ show OP_and)

atomicFormula

return $ if null opfs then f1

else foldl (\ b a -> (mkPredefOp OP_and [b, snd a])) f1 opfs

-- ---------------------------------------------------------------------------

-- * Parser for Commands

-- ---------------------------------------------------------------------------

formulaorexpression :: OperatorState st => CharParser st EXPRESSION

formulaorexpression = try aFormula <|> plusmin

-- | parser for commands

command :: CharParser (AnnoState.AnnoState st) CMD

command = reduceCommand <|> try assignment <|> repeatExpr <|> caseExpr

<|> sequenceExpr <|> constraint

reduceCommand :: OperatorState st => CharParser st CMD

reduceCommand = do

cmd <- lexemeParser $ Lexer.keyWord $ choice $ map tryString

["solve", "simplify", "divide", "int", "rlqe", "factorize", "print"]

oParenT

arg1 <- formulaorexpression

args <- many $ pComma >> formulaorexpression

cParenT

return $ Cmd cmd $ arg1 : args

assignment :: OperatorState st => CharParser st CMD

assignment = do

ident@(OpDecl _ _ vdl _) <- opdecl

lexemeParser $ choice [tryString ":=", tryString "="]

exp' <- runWithVars (map varDeclName vdl) plusmin

return $ Ass ident exp'

constraint :: OperatorState st => CharParser st CMD

constraint = do

exp' <- try aFormula

case exp' of

Op {} ->

return $ Cmd "constraint" [exp']

_ -> fail "Malformed constraint"

sequenceExpr :: CharParser (AnnoState.AnnoState st) CMD

sequenceExpr = do

lstring "sequence"

statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)

lstring "end"

return $ Sequence $ map AS_Anno.item statements

repeatExpr :: CharParser (AnnoState.AnnoState st) CMD

repeatExpr = do

lstring "repeat"

statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)

lstring "until"

cstr <- aFormula

return $ Repeat cstr $ map AS_Anno.item statements

singleCase :: CharParser (AnnoState.AnnoState st) (EXPRESSION, [CMD])

singleCase =

let p1 = lstring "else" >> return (mkPredefOp OP_true [])

in do

lstring "case"

cond <- choice [try p1, aFormula]

lstring ":"

statements <- many1 (AnnoState.dotT >> AnnoState.allAnnoParser command)

return (cond, map AS_Anno.item statements)

caseExpr :: CharParser (AnnoState.AnnoState st) CMD

caseExpr = many1 singleCase >-> Cond << lstring "end"

-- ---------------------------------------------------------------------------

-- * parser spec entries

-- ---------------------------------------------------------------------------

-- | parser for operator declarations: example: operator a,b,c

opItem :: CharParser st OP_ITEM

opItem = do

Lexer.keySign (lexemeParser (tryString "operator"))

vars <- sepBy1 identifier pComma

return $ Op_item vars nullRange

-- | Parser for variable declarations: example: vars x,y in {1,2}; z in [-1,1]

varItems :: CharParser st [VAR_ITEM]

varItems = oneOfKeys ["vars", "var"] >> sepBy1 varItem pSemi

-- | Parser for a variable declaration: example: vars x,y in {1,2}

varItem :: CharParser st VAR_ITEM

varItem = do

vars <- sepBy1 identifier pComma

oneOfKeys ["in"]

dom <- parseDomain

return $ Var_item vars dom nullRange

{- | Parser for extended parameter declarations:

example: I in [1,2]; -}

epDecl :: CharParser st (Id.Token, EPDomain)

epDecl = do

epId <- identifier

oneOfKeys ["in"]

parseEPDomain >-> (,) epId

{- | Parser for extended parameter default values and domain variable

declarations: example: I = 1; n=2 -}

epNumValAss :: CharParser st (Id.Token, APInt)

epNumValAss = do

epId <- identifier

oneOfKeys ["="]

getSignedNumber >-> (,) epId . read

parseDomain :: CharParser st Domain

parseDomain = do

lp <- lexemeParser $ oneOf "{[]"

gcl <- sepBy1 (signednumber >-> either GCI (GCR . readRat) . fst) pComma

rp <- lexemeParser $ oneOf "[]}"

let f o c = case gcl of

[lb, rb] -> return $ IntVal (lb, o) (rb, c)

_ -> parseError "parseDomain: incorrect interval-list"

case [lp, rp] of

"{}" -> return $ Set $ Set.fromList gcl

"[]" -> f True True

"[[" -> f True False

"][" -> f False False

"]]" -> f False True

_ -> parseError "parseDomain: malformed domain parens"

parseEPVal :: CharParser st EPVal

parseEPVal = do

mId <- optionMaybe identifier

case mId of

Just n -> return $ EPConstRef n

_ -> getSignedNumber >-> EPVal . read

parseEPDomain :: CharParser st EPDomain

parseEPDomain = do

lexemeParser $ string "["

l <- parseEPVal

pComma

r <- parseEPVal

lexemeParser $ string "]"

return $ ClosedInterval l r

-- | Toplevel parser for basic specs

basicSpec :: AnnoState.AParser st BASIC_SPEC

basicSpec =

AnnoState.annosParser parseBasicItems >-> Basic_spec

<|> (Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))

-- | Parser for basic items

parseBasicItems :: AnnoState.AParser st BASIC_ITEM

parseBasicItems = parseOpDecl <|> parseVarDecl <|> parseEPDefValOrDomDecl

<|> parseEPDecl <|> parseAxItems

-- | parser for operator declarations

parseOpDecl :: AnnoState.AParser st BASIC_ITEM

parseOpDecl = opItem >-> Op_decl

-- | parser for variable declarations

parseVarDecl :: AnnoState.AParser st BASIC_ITEM

parseVarDecl = varItems >-> Var_decls

{- | parser for extended parameter declarations, one of:

default value for an extended parameter (I=2)

a domain variable declaration (n=10) -}

parseEPDefValOrDomDecl :: AnnoState.AParser st BASIC_ITEM

parseEPDefValOrDomDecl = do

lstring "set"

mDef <- optionMaybe $ try $ lexemeParser $ string "default"

case mDef of

Nothing -> sepBy1 epNumValAss pSemi >-> EP_domdecl

_ -> sepBy1 epNumValAss pSemi >-> EP_defval

-- | parser for extended parameter declarations

parseEPDecl :: AnnoState.AParser st BASIC_ITEM

parseEPDecl = oneOfKeys ["eps", "ep"] >> sepBy1 epDecl pSemi >-> EP_decl

-- | parser for Axiom_item

parseAxItems :: AnnoState.AParser st BASIC_ITEM

parseAxItems = do

AnnoState.dotT

cmd <- AnnoState.allAnnoParser command

return $ Axiom_item cmd

-- ---------------------------------------------------------------------------

-- * parser for symbol maps etc.

-- ---------------------------------------------------------------------------

-- | parsing a prop symbol

symb :: GenParser Char st SYMB

symb = identifier >-> Symb_id

-- | parsing one symbol or a mapping of one to a second symbol

symbMap :: GenParser Char st SYMB_OR_MAP

symbMap = do

s <- symb

do f <- pToken $ toKey mapsTo

t <- symb

return (Symb_map s t $ tokPos f)

<|> return (Symb s)

-- | Parse a list of comma separated symbols.

symbItems :: GenParser Char st SYMB_ITEMS

symbItems = do

(is, ps) <- symbs

return (Symb_items is $ catRange ps)

-- | parse a comma separated list of symbols

symbs :: GenParser Char st ([SYMB], [Token])

symbs = do

s <- symb

do c <- commaT `followedWith` symb

(is, ps) <- symbs

return (s : is, c : ps)

<|> return ([s], [])

-- | parse a list of symbol mappings

symbMapItems :: GenParser Char st SYMB_MAP_ITEMS

symbMapItems = do

(is, ps) <- symbMaps

return (Symb_map_items is $ catRange ps)

-- | parse a comma separated list of symbol mappings

symbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])

symbMaps = do

s <- symbMap

do c <- commaT `followedWith` symb

(is, ps) <- symbMaps

return (s : is, c : ps)

<|> return ([s], [])

parseCommand :: String -> Maybe CMD

parseCommand inp =

case runParser command (AnnoState.emptyAnnos ()) "" inp of

Left _ -> Nothing

Right s -> Just s

parseExpression :: OperatorState a => a -> String -> Maybe EXPRESSION

parseExpression st inp =

case runParser formulaorexpression st "" inp of

Left _ -> Nothing

Right s -> Just s