{-| Module : Idris.Parser.Ops Description : Parser for operators and fixity declarations. License : BSD3 Maintainer : The Idris Community. -} {-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving, MultiParamTypeClasses, PatternGuards #-} module Idris.Parser.Ops where import Idris.AbsSyntax import Idris.Core.TT import Idris.Parser.Helpers import Prelude hiding (pi) import Control.Applicative import Control.Monad import qualified Control.Monad.Combinators.Expr as P import Control.Monad.State.Strict import Data.Char (isAlpha) import Data.List import Data.List.NonEmpty (fromList) import Text.Megaparsec (()) import qualified Text.Megaparsec as P -- | Creates table for fixity declarations to build expression parser -- using pre-build and user-defined operator/fixity declarations table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]] table fixes = [[prefix "-" negateExpr]] ++ toTable (reverse fixes) ++ [[noFixityBacktickOperator], [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]], [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]], [noFixityOperator]] where negateExpr :: FC -> PTerm -> PTerm negateExpr _ (PConstant fc (I int)) = PConstant fc $ I $ negate int negateExpr _ (PConstant fc (BI bigInt)) = PConstant fc $ BI $ negate bigInt negateExpr _ (PConstant fc (Fl dbl)) = PConstant fc $ Fl $ negate dbl negateExpr _ (PConstSugar fc term) = negateExpr fc term negateExpr fc (PAlternative ns tp terms) = PAlternative ns tp $ map (negateExpr fc) terms negateExpr fc x = PApp fc (PRef fc [fc] (sUN "negate")) [pexp x] flatten :: PTerm -> PTerm -- flatten application flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs)) flatten t = t noFixityBacktickOperator :: P.Operator IdrisParser PTerm noFixityBacktickOperator = P.InfixN $ do (n, fc) <- withExtent backtickOperator return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y] -- | Operator without fixity (throws an error) noFixityOperator :: P.Operator IdrisParser PTerm noFixityOperator = P.InfixN $ do indentGt op <- P.try symbolicOperator P.unexpected . P.Label . fromList $ "Operator without known fixity: " ++ op -- | Calculates table for fixity declarations toTable :: [FixDecl] -> [[P.Operator IdrisParser PTerm]] toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs) toBin (Fix (PrefixN _) op) = prefix op $ \fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x] toBin (Fix f op) = binary op (assoc f) $ \fc n x y -> PApp fc (PRef fc [] n) [pexp x,pexp y] assoc (Infixl _) = P.InfixL assoc (Infixr _) = P.InfixR assoc (InfixN _) = P.InfixN isBacktick :: String -> Bool isBacktick (c : _) = c == '_' || isAlpha c isBacktick _ = False binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm binary name ctor f | isBacktick name = ctor $ P.try $ do (n, fc) <- withExtent backtickOperator guard $ show (nsroot n) == name return $ f fc n | otherwise = ctor $ do indentGt fc <- extent $ reservedOp name indentGt return $ f fc (sUN name) prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm prefix name f = P.Prefix $ do fc <- extent $ reservedOp name indentGt return (f fc) {- | Parses a function used as an operator -- enclosed in backticks @ BacktickOperator ::= '`' Name '`' ; @ -} backtickOperator :: (Parsing m, MonadState IState m) => m Name backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name {- | Parses an operator name (either a symbolic name or a backtick-quoted name) @ OperatorName ::= SymbolicOperator | BacktickOperator ; @ -} operatorName :: (Parsing m, MonadState IState m) => m Name operatorName = sUN <$> symbolicOperator <|> backtickOperator {- | Parses an operator in function position i.e. enclosed by `()', with an optional namespace @ OperatorFront ::= '(' '=' ')' | (Identifier_t '.')? '(' Operator_t ')' ; @ -} operatorFront :: Parsing m => m Name operatorFront = do P.try $ lchar '(' *> (eqTy <$ reservedOp "=") <* lchar ')' <|> maybeWithNS (lchar '(' *> symbolicOperator <* lchar ')') [] {- | Parses a function (either normal name or operator) @ FnName ::= Name | OperatorFront; @ -} fnName :: (Parsing m, MonadState IState m) => m Name fnName = P.try operatorFront <|> name "function name" {- | Parses a fixity declaration @ Fixity ::= FixityType Natural_t OperatorList Terminator ; @ -} fixity :: IdrisParser PDecl fixity = do ((f, i, ops), fc) <- withExtent $ do pushIndent f <- fixityType; i <- natural ops <- P.sepBy1 (show . nsroot <$> operatorName) (lchar ',') terminator return (f, i, ops) let prec = fromInteger i istate <- get let infixes = idris_infixes istate let fs = map (Fix (f prec)) ops let redecls = map (alreadyDeclared infixes) fs let ill = filter (not . checkValidity) redecls if null ill then do put (istate { idris_infixes = nub $ sort (fs ++ infixes) , ibc_write = map IBCFix fs ++ ibc_write istate }) return (PFix fc (f prec) ops) else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\"" ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill "fixity declaration" where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl]) alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs) checkValidity :: (FixDecl, [FixDecl]) -> Bool checkValidity (f, fs) = all (== f) fs extractName :: FixDecl -> String extractName (Fix _ n) = n -- | Check that a declaration of an operator also has fixity declared checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl checkDeclFixity p = do decl <- p case getDeclName decl of Nothing -> return decl Just n -> do checkNameFixity n return decl where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n getDeclName _ = Nothing -- | Checks that an operator name also has a fixity declaration checkNameFixity :: Name -> IdrisParser () checkNameFixity n = do fOk <- fixityOk n unless fOk . fail $ "Missing fixity declaration for " ++ show n where fixityOk (NS n' _) = fixityOk n' fixityOk (UN n') | all (flip elem opChars) (str n') = do fixities <- fmap idris_infixes get return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities | otherwise = return True fixityOk _ = return True {- | Parses a fixity declaration type (i.e. infix or prefix, associtavity) @ FixityType ::= 'infixl' | 'infixr' | 'infix' | 'prefix' ; @ -} fixityType :: IdrisParser (Int -> Fixity) fixityType = do reserved "infixl"; return Infixl <|> do reserved "infixr"; return Infixr <|> do reserved "infix"; return InfixN <|> do reserved "prefix"; return PrefixN "fixity type" opChars :: String opChars = ":!#$%&*+./<=>?@\\^|-~" operatorLetter :: Parsing m => m Char operatorLetter = P.oneOf opChars commentMarkers :: [String] commentMarkers = [ "--", "|||" ] invalidOperators :: [String] invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"] -- | Parses an operator symbolicOperator :: Parsing m => m String symbolicOperator = do op <- token . some $ operatorLetter when (op `elem` (invalidOperators ++ commentMarkers)) $ fail $ op ++ " is not a valid operator" return op -- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007 -- | Parses a reserved operator reservedOp :: Parsing m => String -> m () reservedOp name = token $ P.try $ do string name P.notFollowedBy operatorLetter ("end of " ++ show name)