{-|
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
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
table [FixDecl]
fixes
   = [[[Char]
-> (FC -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
prefix [Char]
"-" FC -> PTerm -> PTerm
negateExpr]] [[Operator
    (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
forall a. [a] -> [a] -> [a]
++
      [FixDecl]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
toTable ([FixDecl] -> [FixDecl]
forall a. [a] -> [a]
reverse [FixDecl]
fixes) [[Operator
    (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
forall a. [a] -> [a] -> [a]
++
     [[Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
noFixityBacktickOperator],
      [[Char]
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator
         (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
binary [Char]
"$" IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) 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]],
      [[Char]
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator
         (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
binary [Char]
"=" IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) 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 (StateT IState (WriterT FC (Parsec Void [Char]))) 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] ([Char] -> Name
sUN [Char]
"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 (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
noFixityBacktickOperator = IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall a b. (a -> b) -> a -> b
$ do
                                 (Name
n, FC
fc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
                                 (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
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 (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
noFixityOperator = IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall a b. (a -> b) -> a -> b
$ do
                         StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                         [Char]
op <- StateT IState (WriterT FC (Parsec Void [Char])) [Char]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator
                         ErrorItem (Token [Char]) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected (ErrorItem (Token [Char]) -> IdrisParser (PTerm -> PTerm -> PTerm))
-> ([Char] -> ErrorItem (Token [Char]))
-> [Char]
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty Char -> ErrorItem (Token [Char])
forall t. NonEmpty Char -> ErrorItem t
P.Label (NonEmpty Char -> ErrorItem (Token [Char]))
-> ([Char] -> NonEmpty Char) -> [Char] -> ErrorItem (Token [Char])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> NonEmpty Char
forall a. HasCallStack => [a] -> NonEmpty a
fromList ([Char] -> IdrisParser (PTerm -> PTerm -> PTerm))
-> [Char] -> IdrisParser (PTerm -> PTerm -> PTerm)
forall a b. (a -> b) -> a -> b
$ [Char]
"Operator without known fixity: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
op

    -- | Calculates table for fixity declarations
    toTable    :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
    toTable :: [FixDecl]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
toTable [FixDecl]
fs = ([FixDecl]
 -> [Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm])
-> [[FixDecl]]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
forall a b. (a -> b) -> [a] -> [b]
map ((FixDecl
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> [FixDecl]
-> [Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]
forall a b. (a -> b) -> [a] -> [b]
map FixDecl
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
toBin) ((FixDecl -> FixDecl -> Bool) -> [FixDecl] -> [[FixDecl]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (Fix Fixity
x [Char]
_) (Fix Fixity
y [Char]
_) -> 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 (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
toBin (Fix (PrefixN Int
_) [Char]
op) = [Char]
-> (FC -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
prefix [Char]
op ((FC -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) 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 [] ([Char] -> Name
sUN [Char]
op)) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
x]
    toBin (Fix Fixity
f [Char]
op)           = [Char]
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator
         (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
binary [Char]
op (Fixity
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall {m :: * -> *} {a}. Fixity -> m (a -> a -> a) -> Operator m a
assoc Fixity
f) ((FC -> Name -> PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) 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 :: [Char] -> Bool
isBacktick (Char
c : [Char]
_) = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char -> Bool
isAlpha Char
c
    isBacktick [Char]
_       = Bool
False

    binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
    binary :: [Char]
-> (IdrisParser (PTerm -> PTerm -> PTerm)
    -> Operator
         (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> (FC -> Name -> PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
binary [Char]
name IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
ctor FC -> Name -> PTerm -> PTerm -> PTerm
f
      | [Char] -> Bool
isBacktick [Char]
name = IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
ctor (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall a b. (a -> b) -> a -> b
$ IdrisParser (PTerm -> PTerm -> PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
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) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
                            Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ Name -> [Char]
forall a. Show a => a -> [Char]
show (Name -> Name
nsroot Name
n) [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
name
                            (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
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 (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
ctor (IdrisParser (PTerm -> PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> IdrisParser (PTerm -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall a b. (a -> b) -> a -> b
$ do
                            StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                            FC
fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
name
                            StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                            (PTerm -> PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
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 ([Char] -> Name
sUN [Char]
name)

    prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
    prefix :: [Char]
-> (FC -> PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
prefix [Char]
name FC -> PTerm -> PTerm
f = IdrisParser (PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall (m :: * -> *) a. m (a -> a) -> Operator m a
P.Prefix (IdrisParser (PTerm -> PTerm)
 -> Operator
      (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm)
-> IdrisParser (PTerm -> PTerm)
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
forall a b. (a -> b) -> a -> b
$ do
                      FC
fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
name
                      StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
                      (PTerm -> PTerm) -> IdrisParser (PTerm -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
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 :: forall (m :: * -> *). (Parsing m, MonadState IState m) => 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 a b. m a -> m b -> m b
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 a b. m a -> m b -> m b
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 :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName =     [Char] -> Name
sUN ([Char] -> Name) -> m [Char] -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Char]
forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator
               m Name -> m Name -> m Name
forall a. m a -> m a -> m a
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 :: forall (m :: * -> *). Parsing m => m Name
operatorFront = do     m Name -> m Name
forall a. m a -> m a
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 a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Name
eqTy Name -> m () -> m Name
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> m ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=") m Name -> m Char -> m Name
forall a b. m a -> m b -> m a
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 a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m [Char] -> [[Char]] -> m Name
forall (m :: * -> *). Parsing m => m [Char] -> [[Char]] -> m Name
maybeWithNS (Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' m Char -> m [Char] -> m [Char]
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m [Char]
forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator m [Char] -> m Char -> m [Char]
forall a b. m a -> m b -> m a
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 :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName = m Name -> m Name
forall a. m a -> m a
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 a. m a -> m a -> m a
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 -> [Char] -> m Name
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"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, [[Char]]
ops), FC
fc) <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Int -> Fixity, Integer, [[Char]])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     ((Int -> Fixity, Integer, [[Char]]), FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT
   IState
   (WriterT FC (Parsec Void [Char]))
   (Int -> Fixity, Integer, [[Char]])
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      ((Int -> Fixity, Integer, [[Char]]), FC))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Int -> Fixity, Integer, [[Char]])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     ((Int -> Fixity, Integer, [[Char]]), FC)
forall a b. (a -> b) -> a -> b
$ do
                StateT IState (WriterT FC (Parsec Void [Char])) ()
pushIndent
                Int -> Fixity
f <- IdrisParser (Int -> Fixity)
fixityType; Integer
i <- StateT IState (WriterT FC (Parsec Void [Char])) Integer
forall (m :: * -> *). Parsing m => m Integer
natural
                [[Char]]
ops <- StateT IState (WriterT FC (Parsec Void [Char])) [Char]
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [[Char]]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (Name -> [Char]
forall a. Show a => a -> [Char]
show (Name -> [Char]) -> (Name -> Name) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nsroot (Name -> [Char])
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName) (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
                (Int -> Fixity, Integer, [[Char]])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Int -> Fixity, Integer, [[Char]])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Fixity
f, Integer
i, [[Char]]
ops)
            let prec :: Int
prec = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
            IState
istate <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
            let infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
istate
            let fs :: [FixDecl]
fs      = ([Char] -> FixDecl) -> [[Char]] -> [FixDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Fixity -> [Char] -> FixDecl
Fix (Int -> Fixity
f Int
prec)) [[Char]]
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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FixDecl, [FixDecl])]
ill
               then do IState -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
istate { idris_infixes = nub $ sort (fs ++ infixes)
                                     , ibc_write     = map IBCFix fs ++ ibc_write istate
                                   })
                       PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Fixity -> [[Char]] -> PDecl
forall t. FC -> Fixity -> [[Char]] -> PDecl' t
PFix FC
fc (Int -> Fixity
f Int
prec) [[Char]]
ops)
               else [Char] -> IdrisParser PDecl
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> IdrisParser PDecl) -> [Char] -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ ((FixDecl, [FixDecl]) -> [Char])
-> [(FixDecl, [FixDecl])] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(FixDecl
f, (FixDecl
x:[FixDecl]
xs)) -> [Char]
"Illegal redeclaration of fixity:\n\t\""
                                                [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FixDecl -> [Char]
forall a. Show a => a -> [Char]
show FixDecl
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\" overrides \"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FixDecl -> [Char]
forall a. Show a => a -> [Char]
show FixDecl
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\"") [(FixDecl, [FixDecl])]
ill
         IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"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 -> [Char]
extractName FixDecl
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
==) ([Char] -> Bool) -> (FixDecl -> [Char]) -> FixDecl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixDecl -> [Char]
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 -> [Char]
extractName (Fix Fixity
_ [Char]
n) = [Char]
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 a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
decl
                         Just Name
n -> do Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
n
                                      PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
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 -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
n = do Bool
fOk <- Name -> StateT IState (WriterT FC (Parsec Void [Char])) Bool
forall {m :: * -> *}. MonadState IState m => Name -> m Bool
fixityOk Name
n
                       Bool
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
fOk (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> [Char]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$
                         [Char]
"Missing fixity declaration for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Show a => a -> [Char]
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) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Char -> [Char] -> Bool) -> [Char] -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Char]
opChars) (Text -> [Char]
str Text
n') =
                                 do [FixDecl]
fixities <- (IState -> [FixDecl]) -> m IState -> m [FixDecl]
forall a b. (a -> b) -> m a -> m b
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 a. a -> m a
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
. [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Text -> [Char]
str Text
n') ([[Char]] -> Bool) -> ([FixDecl] -> [[Char]]) -> [FixDecl] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixDecl -> [Char]) -> [FixDecl] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fix Fixity
_ [Char]
op) -> [Char]
op) ([FixDecl] -> m Bool) -> [FixDecl] -> m Bool
forall a b. (a -> b) -> a -> b
$ [FixDecl]
fixities
                             | Bool
otherwise = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            fixityOk Name
_ = Bool -> m Bool
forall a. a -> m a
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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infixl"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixl
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infixr"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixr
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infix";  (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
InfixN
         IdrisParser (Int -> Fixity)
-> IdrisParser (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"prefix"; (Int -> Fixity) -> IdrisParser (Int -> Fixity)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
PrefixN
         IdrisParser (Int -> Fixity)
-> [Char] -> IdrisParser (Int -> Fixity)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"fixity type"

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

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

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

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

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

-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
-- | Parses a reserved operator
reservedOp :: Parsing m => String -> m ()
reservedOp :: forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
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 a. m a -> m a
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 [Char] -> m [Char]
forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
name
     m Char -> m ()
forall a. m a -> 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 () -> [Char] -> m ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> ([Char]
"end of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
name)