{-|
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 :: [FixDecl] -> [[Operator IdrisParser PTerm]]
table [FixDecl]
fixes
   = [[String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
prefix String
"-" FC -> PTerm -> PTerm
negateExpr]] [[Operator IdrisParser PTerm]]
-> [[Operator IdrisParser PTerm]] -> [[Operator IdrisParser PTerm]]
forall a. [a] -> [a] -> [a]
++
      [FixDecl] -> [[Operator IdrisParser PTerm]]
toTable ([FixDecl] -> [FixDecl]
forall a. [a] -> [a]
reverse [FixDecl]
fixes) [[Operator IdrisParser PTerm]]
-> [[Operator IdrisParser PTerm]] -> [[Operator IdrisParser PTerm]]
forall a. [a] -> [a] -> [a]
++
     [[Operator IdrisParser PTerm
noFixityBacktickOperator],
      [String
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
binary String
"$" IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ \FC
fc Name
_ PTerm
x PTerm
y -> PTerm -> PTerm
flatten (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
x [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
y]],
      [String
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
binary String
"=" IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ \FC
fc Name
_ PTerm
x PTerm
y -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
eqTy) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x, PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
y]],
      [Operator IdrisParser PTerm
noFixityOperator]]
  where

    negateExpr                               :: FC -> PTerm -> PTerm
    negateExpr :: FC -> PTerm -> PTerm
negateExpr FC
_  (PConstant FC
fc (I Int
int))     = FC -> Const -> PTerm
PConstant FC
fc (Const -> PTerm) -> Const -> PTerm
forall a b. (a -> b) -> a -> b
$ Int -> Const
I (Int -> Const) -> Int -> Const
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
negate Int
int
    negateExpr FC
_  (PConstant FC
fc (BI Integer
bigInt)) = FC -> Const -> PTerm
PConstant FC
fc (Const -> PTerm) -> Const -> PTerm
forall a b. (a -> b) -> a -> b
$ Integer -> Const
BI (Integer -> Const) -> Integer -> Const
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
negate Integer
bigInt
    negateExpr FC
_  (PConstant FC
fc (Fl Double
dbl))    = FC -> Const -> PTerm
PConstant FC
fc (Const -> PTerm) -> Const -> PTerm
forall a b. (a -> b) -> a -> b
$ Double -> Const
Fl (Double -> Const) -> Double -> Const
forall a b. (a -> b) -> a -> b
$ Double -> Double
forall a. Num a => a -> a
negate Double
dbl
    negateExpr FC
_  (PConstSugar FC
fc PTerm
term)      = FC -> PTerm -> PTerm
negateExpr FC
fc PTerm
term
    negateExpr FC
fc (PAlternative [(Name, Name)]
ns PAltType
tp [PTerm]
terms) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ns PAltType
tp ([PTerm] -> PTerm) -> [PTerm] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (FC -> PTerm -> PTerm
negateExpr FC
fc) [PTerm]
terms
    negateExpr FC
fc PTerm
x                          = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] (String -> Name
sUN String
"negate")) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x]

    flatten                            :: PTerm -> PTerm -- flatten application
    flatten :: PTerm -> PTerm
flatten (PApp FC
fc (PApp FC
_ PTerm
f [PArg]
as) [PArg]
bs) = PTerm -> PTerm
flatten (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
as [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
bs))
    flatten PTerm
t                          = PTerm
t

    noFixityBacktickOperator :: P.Operator IdrisParser PTerm
    noFixityBacktickOperator :: Operator IdrisParser PTerm
noFixityBacktickOperator = IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                                 (Name
n, FC
fc) <- IdrisParser Name -> IdrisParser (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
                                 (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((PTerm -> PTerm -> PTerm)
 -> IdrisParser (PTerm -> PTerm -> PTerm))
-> (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ \PTerm
x PTerm
y -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
n) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x, PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
y]

    -- | Operator without fixity (throws an error)
    noFixityOperator :: P.Operator IdrisParser PTerm
    noFixityOperator :: Operator IdrisParser PTerm
noFixityOperator = IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                         IdrisParser ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                         String
op <- IdrisParser String -> IdrisParser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try IdrisParser String
forall (m :: * -> *). Parsing m => m String
symbolicOperator
                         ErrorItem Char -> IdrisParser (PTerm -> PTerm -> PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected (ErrorItem Char -> IdrisParser (PTerm -> PTerm -> PTerm))
-> (String -> ErrorItem Char)
-> String
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> ErrorItem Char
forall t. NonEmpty Char -> ErrorItem t
P.Label (NonEmpty Char -> ErrorItem Char)
-> (String -> NonEmpty Char) -> String -> ErrorItem Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> NonEmpty Char
forall a. [a] -> NonEmpty a
fromList (String -> IdrisParser (PTerm -> PTerm -> PTerm))
-> String -> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ String
"Operator without known fixity: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op

    -- | Calculates table for fixity declarations
    toTable    :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
    toTable :: [FixDecl] -> [[Operator IdrisParser PTerm]]
toTable [FixDecl]
fs = ([FixDecl] -> [Operator IdrisParser PTerm])
-> [[FixDecl]] -> [[Operator IdrisParser PTerm]]
forall a b. (a -> b) -> [a] -> [b]
map ((FixDecl -> Operator IdrisParser PTerm)
-> [FixDecl] -> [Operator IdrisParser PTerm]
forall a b. (a -> b) -> [a] -> [b]
map FixDecl -> Operator IdrisParser PTerm
toBin) ((FixDecl -> FixDecl -> Bool) -> [FixDecl] -> [[FixDecl]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (Fix Fixity
x String
_) (Fix Fixity
y String
_) -> Fixity -> Int
prec Fixity
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Fixity -> Int
prec Fixity
y) [FixDecl]
fs)

    toBin :: FixDecl -> Operator IdrisParser PTerm
toBin (Fix (PrefixN Int
_) String
op) = String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
prefix String
op ((FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm)
-> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ \FC
fc PTerm
x ->
                                   FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
op)) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x]
    toBin (Fix Fixity
f String
op)           = String
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
binary String
op (Fixity
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall (m :: * -> *) a. Fixity -> m (a -> a -> a) -> Operator m a
assoc Fixity
f) ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ \FC
fc Name
n PTerm
x PTerm
y ->
                                   FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x,PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
y]

    assoc :: Fixity -> m (a -> a -> a) -> Operator m a
assoc (Infixl Int
_) = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL
    assoc (Infixr Int
_) = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR
    assoc (InfixN Int
_) = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN

    isBacktick         :: String -> Bool
    isBacktick :: String -> Bool
isBacktick (Char
c : String
_) = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char -> Bool
isAlpha Char
c
    isBacktick String
_       = Bool
False

    binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
    binary :: String
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator IdrisParser PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
binary String
name IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
ctor FC -> Name -> PTerm -> PTerm -> PTerm
f
      | String -> Bool
isBacktick String
name = IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
ctor (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ IdrisParser (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser (PTerm -> PTerm -> PTerm)
 -> IdrisParser (PTerm -> PTerm -> PTerm))
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ do
                            (Name
n, FC
fc) <- IdrisParser Name -> IdrisParser (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
                            Bool -> IdrisParser ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> IdrisParser ()) -> Bool -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
name
                            (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((PTerm -> PTerm -> PTerm)
 -> IdrisParser (PTerm -> PTerm -> PTerm))
-> (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ FC -> Name -> PTerm -> PTerm -> PTerm
f FC
fc Name
n
      | Bool
otherwise       = IdrisParser (PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
ctor (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator IdrisParser PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                            IdrisParser ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                            FC
fc <- IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (IdrisParser ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp String
name
                            IdrisParser ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                            (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((PTerm -> PTerm -> PTerm)
 -> IdrisParser (PTerm -> PTerm -> PTerm))
-> (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ FC -> Name -> PTerm -> PTerm -> PTerm
f FC
fc (String -> Name
sUN String
name)

    prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
    prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
prefix String
name FC -> PTerm -> PTerm
f = IdrisParser (PTerm -> PTerm) -> Operator IdrisParser PTerm
forall (m :: * -> *) a. m (a -> a) -> Operator m a
P.Prefix (IdrisParser (PTerm -> PTerm) -> Operator IdrisParser PTerm)
-> IdrisParser (PTerm -> PTerm) -> Operator IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                      FC
fc <- IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (IdrisParser ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> IdrisParser ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp String
name
                      IdrisParser ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                      (PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm
f FC
fc)

{- | Parses a function used as an operator -- enclosed in backticks

@
  BacktickOperator ::=
    '`' Name '`'
    ;
@
-}
backtickOperator :: (Parsing m, MonadState IState m) => m Name
backtickOperator :: m Name
backtickOperator = m Char -> m Char -> m Name -> m Name
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
P.between (m ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt m () -> m Char -> m Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'`') (m ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt m () -> m Char -> m Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'`') m Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
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 :: m Name
operatorName =     String -> Name
sUN (String -> Name) -> m String -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). Parsing m => m String
symbolicOperator
               m Name -> m Name -> m Name
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
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 :: m Name
operatorFront = do     m Name -> m Name
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m Name -> m Name) -> m Name -> m Name
forall a b. (a -> b) -> a -> b
$ Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' m Char -> m Name -> m Name
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Name
eqTy Name -> m () -> m Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp String
"=") m Name -> m Char -> m Name
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
                   m Name -> m Name -> m Name
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m String -> [String] -> m Name
forall (m :: * -> *). Parsing m => m String -> [String] -> m Name
maybeWithNS (Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' m Char -> m String -> m String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m String
forall (m :: * -> *). Parsing m => m String
symbolicOperator m String -> m Char -> m String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')') []

{- | Parses a function (either normal name or operator)

@
  FnName ::= Name | OperatorFront;
@
-}
fnName :: (Parsing m, MonadState IState m) => m Name
fnName :: m Name
fnName = m Name -> m Name
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try m Name
forall (m :: * -> *). Parsing m => m Name
operatorFront m Name -> m Name -> m Name
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name m Name -> String -> m Name
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function name"

{- | Parses a fixity declaration
@
Fixity ::=
  FixityType Natural_t OperatorList Terminator
  ;
@
-}
fixity :: IdrisParser PDecl
fixity :: IdrisParser PDecl
fixity = do ((Int -> Fixity
f, Integer
i, [String]
ops), FC
fc) <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Int -> Fixity, Integer, [String])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ((Int -> Fixity, Integer, [String]), FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT
   IState
   (WriterT FC (Parsec Void String))
   (Int -> Fixity, Integer, [String])
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      ((Int -> Fixity, Integer, [String]), FC))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Int -> Fixity, Integer, [String])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ((Int -> Fixity, Integer, [String]), FC)
forall a b. (a -> b) -> a -> b
$ do
                IdrisParser ()
pushIndent
                Int -> Fixity
f <- IdrisParser (Int -> Fixity)
fixityType; Integer
i <- StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
natural
                [String]
ops <- IdrisParser String
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [String]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (Name -> String
forall a. Show a => a -> String
show (Name -> String) -> (Name -> Name) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nsroot (Name -> String) -> IdrisParser Name -> IdrisParser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IdrisParser Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                IdrisParser ()
terminator
                (Int -> Fixity, Integer, [String])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Int -> Fixity, Integer, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Fixity
f, Integer
i, [String]
ops)
            let prec :: Int
prec = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
            IState
istate <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
            let infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
istate
            let fs :: [FixDecl]
fs      = (String -> FixDecl) -> [String] -> [FixDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Fixity -> String -> FixDecl
Fix (Int -> Fixity
f Int
prec)) [String]
ops
            let redecls :: [(FixDecl, [FixDecl])]
redecls = (FixDecl -> (FixDecl, [FixDecl]))
-> [FixDecl] -> [(FixDecl, [FixDecl])]
forall a b. (a -> b) -> [a] -> [b]
map ([FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
alreadyDeclared [FixDecl]
infixes) [FixDecl]
fs
            let ill :: [(FixDecl, [FixDecl])]
ill     = ((FixDecl, [FixDecl]) -> Bool)
-> [(FixDecl, [FixDecl])] -> [(FixDecl, [FixDecl])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((FixDecl, [FixDecl]) -> Bool) -> (FixDecl, [FixDecl]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixDecl, [FixDecl]) -> Bool
checkValidity) [(FixDecl, [FixDecl])]
redecls
            if [(FixDecl, [FixDecl])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FixDecl, [FixDecl])]
ill
               then do IState -> IdrisParser ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
istate { idris_infixes :: [FixDecl]
idris_infixes = [FixDecl] -> [FixDecl]
forall a. Eq a => [a] -> [a]
nub ([FixDecl] -> [FixDecl]) -> [FixDecl] -> [FixDecl]
forall a b. (a -> b) -> a -> b
$ [FixDecl] -> [FixDecl]
forall a. Ord a => [a] -> [a]
sort ([FixDecl]
fs [FixDecl] -> [FixDecl] -> [FixDecl]
forall a. [a] -> [a] -> [a]
++ [FixDecl]
infixes)
                                     , ibc_write :: [IBCWrite]
ibc_write     = (FixDecl -> IBCWrite) -> [FixDecl] -> [IBCWrite]
forall a b. (a -> b) -> [a] -> [b]
map FixDecl -> IBCWrite
IBCFix [FixDecl]
fs [IBCWrite] -> [IBCWrite] -> [IBCWrite]
forall a. [a] -> [a] -> [a]
++ IState -> [IBCWrite]
ibc_write IState
istate
                                   })
                       PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Fixity -> [String] -> PDecl
forall t. FC -> Fixity -> [String] -> PDecl' t
PFix FC
fc (Int -> Fixity
f Int
prec) [String]
ops)
               else String -> IdrisParser PDecl
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IdrisParser PDecl) -> String -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ ((FixDecl, [FixDecl]) -> String)
-> [(FixDecl, [FixDecl])] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(FixDecl
f, (FixDecl
x:[FixDecl]
xs)) -> String
"Illegal redeclaration of fixity:\n\t\""
                                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ FixDecl -> String
forall a. Show a => a -> String
show FixDecl
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" overrides \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FixDecl -> String
forall a. Show a => a -> String
show FixDecl
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"") [(FixDecl, [FixDecl])]
ill
         IdrisParser PDecl -> String -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"fixity declaration"
  where
    alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
    alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
alreadyDeclared [FixDecl]
fs FixDecl
f = (FixDecl
f, (FixDecl -> Bool) -> [FixDecl] -> [FixDecl]
forall a. (a -> Bool) -> [a] -> [a]
filter ((FixDecl -> String
extractName FixDecl
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (FixDecl -> String) -> FixDecl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixDecl -> String
extractName) [FixDecl]
fs)

    checkValidity :: (FixDecl, [FixDecl]) -> Bool
    checkValidity :: (FixDecl, [FixDecl]) -> Bool
checkValidity (FixDecl
f, [FixDecl]
fs) = (FixDecl -> Bool) -> [FixDecl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (FixDecl -> FixDecl -> Bool
forall a. Eq a => a -> a -> Bool
== FixDecl
f) [FixDecl]
fs

    extractName :: FixDecl -> String
    extractName :: FixDecl -> String
extractName (Fix Fixity
_ String
n) = String
n

-- | Check that a declaration of an operator also has fixity declared
checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity IdrisParser PDecl
p = do PDecl
decl <- IdrisParser PDecl
p
                       case PDecl -> Maybe Name
forall t. PDecl' t -> Maybe Name
getDeclName PDecl
decl of
                         Maybe Name
Nothing -> PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
decl
                         Just Name
n -> do Name -> IdrisParser ()
checkNameFixity Name
n
                                      PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
decl
  where getDeclName :: PDecl' t -> Maybe Name
getDeclName (PTy Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ FnOpts
_ Name
n FC
_ t
_ )                = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
        getDeclName (PData Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ (PDatadecl Name
n FC
_ t
_ [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
_)) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
        getDeclName PDecl' t
_ = Maybe Name
forall a. Maybe a
Nothing

-- | Checks that an operator name also has a fixity declaration
checkNameFixity :: Name -> IdrisParser ()
checkNameFixity :: Name -> IdrisParser ()
checkNameFixity Name
n = do Bool
fOk <- Name -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *). MonadState IState m => Name -> m Bool
fixityOk Name
n
                       Bool -> IdrisParser () -> IdrisParser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
fOk (IdrisParser () -> IdrisParser ())
-> (String -> IdrisParser ()) -> String -> IdrisParser ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IdrisParser ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IdrisParser ()) -> String -> IdrisParser ()
forall a b. (a -> b) -> a -> b
$
                         String
"Missing fixity declaration for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
      where fixityOk :: Name -> m Bool
fixityOk (NS Name
n' [Text]
_) = Name -> m Bool
fixityOk Name
n'
            fixityOk (UN Text
n') | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Char -> String -> Bool) -> String -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) (Text -> String
str Text
n') =
                                 do [FixDecl]
fixities <- (IState -> [FixDecl]) -> m IState -> m [FixDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IState -> [FixDecl]
idris_infixes m IState
forall s (m :: * -> *). MonadState s m => m s
get
                                    Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> ([FixDecl] -> Bool) -> [FixDecl] -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Text -> String
str Text
n') ([String] -> Bool) -> ([FixDecl] -> [String]) -> [FixDecl] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixDecl -> String) -> [FixDecl] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fix Fixity
_ String
op) -> String
op) ([FixDecl] -> m Bool) -> [FixDecl] -> m Bool
forall a b. (a -> b) -> a -> b
$ [FixDecl]
fixities
                             | Bool
otherwise = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            fixityOk Name
_ = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
@
    FixityType ::=
      'infixl'
      | 'infixr'
      | 'infix'
      | 'prefix'
      ;
@
 -}
fixityType :: IdrisParser (Int -> Fixity)
fixityType :: IdrisParser (Int -> Fixity)
fixityType = do String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"infixl"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixl
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"infixr"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixr
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"infix";  (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
InfixN
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> IdrisParser ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"prefix"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
PrefixN
         IdrisParser (Int -> Fixity)
-> String -> IdrisParser (Int -> Fixity)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"fixity type"

opChars :: String
opChars :: String
opChars = String
":!#$%&*+./<=>?@\\^|-~"

operatorLetter :: Parsing m => m Char
operatorLetter :: m Char
operatorLetter = [Token String] -> m (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf String
[Token String]
opChars

commentMarkers :: [String]
commentMarkers :: [String]
commentMarkers = [ String
"--", String
"|||" ]

invalidOperators :: [String]
invalidOperators :: [String]
invalidOperators = [String
":", String
"=>", String
"->", String
"<-", String
"=", String
"?=", String
"|", String
"**", String
"==>", String
"\\", String
"%", String
"~", String
"?", String
"!", String
"@"]

-- | Parses an operator
symbolicOperator :: Parsing m => m String
symbolicOperator :: m String
symbolicOperator = do String
op <- m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m String -> m String)
-> (m Char -> m String) -> m Char -> m String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m Char -> m String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (m Char -> m String) -> m Char -> m String
forall a b. (a -> b) -> a -> b
$ m Char
forall (m :: * -> *). Parsing m => m Char
operatorLetter
                      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
op String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([String]
invalidOperators [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
commentMarkers)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                           String -> m ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a valid operator"
                      String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
op

-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
-- | Parses a reserved operator
reservedOp :: Parsing m => String -> m ()
reservedOp :: String -> m ()
reservedOp String
name = m () -> m ()
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> m ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
  do String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string String
name
     m Char -> m ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy m Char
forall (m :: * -> *). Parsing m => m Char
operatorLetter m () -> String -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> (String
"end of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
name)