{-# 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
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]] forall a. [a] -> [a] -> [a]
++
[FixDecl]
-> [[Operator
(StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
toTable (forall a. [a] -> [a]
reverse [FixDecl]
fixes) 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]
"$" forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR forall a b. (a -> b) -> a -> b
$ \FC
fc Name
_ PTerm
x PTerm
y -> PTerm -> PTerm
flatten forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
x [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]
"=" forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL 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) [forall {t}. t -> PArg' t
pexp PTerm
x, 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 forall a b. (a -> b) -> a -> b
$ Int -> Const
I forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate Int
int
negateExpr FC
_ (PConstant FC
fc (BI Integer
bigInt)) = FC -> Const -> PTerm
PConstant FC
fc forall a b. (a -> b) -> a -> b
$ Integer -> Const
BI forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate Integer
bigInt
negateExpr FC
_ (PConstant FC
fc (Fl Double
dbl)) = FC -> Const -> PTerm
PConstant FC
fc forall a b. (a -> b) -> a -> b
$ Double -> Const
Fl forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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")) [forall {t}. t -> PArg' t
pexp PTerm
x]
flatten :: PTerm -> PTerm
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 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 = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN forall a b. (a -> b) -> a -> b
$ do
(Name
n, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
forall (m :: * -> *) a. Monad m => a -> m a
return 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) [forall {t}. t -> PArg' t
pexp PTerm
x, forall {t}. t -> PArg' t
pexp PTerm
y]
noFixityOperator :: P.Operator IdrisParser PTerm
noFixityOperator :: Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
noFixityOperator = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
[Char]
op <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator
forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
fromList forall a b. (a -> b) -> a -> b
$ [Char]
"Operator without known fixity: " forall a. [a] -> [a] -> [a]
++ [Char]
op
toTable :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
toTable :: [FixDecl]
-> [[Operator
(StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
toTable [FixDecl]
fs = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map FixDecl
-> Operator (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm
toBin) (forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (Fix Fixity
x [Char]
_) (Fix Fixity
y [Char]
_) -> Fixity -> Int
prec Fixity
x 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 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)) [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 (forall {m :: * -> *} {a}. Fixity -> m (a -> a -> a) -> Operator m a
assoc Fixity
f) 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) [forall {t}. t -> PArg' t
pexp PTerm
x,forall {t}. t -> PArg' t
pexp PTerm
y]
assoc :: Fixity -> m (a -> a -> a) -> Operator m a
assoc (Infixl Int
_) = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL
assoc (Infixr Int
_) = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR
assoc (InfixN Int
_) = forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixN
isBacktick :: String -> Bool
isBacktick :: [Char] -> Bool
isBacktick (Char
c : [Char]
_) = Char
c 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 forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
(Name
n, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show (Name -> Name
nsroot Name
n) forall a. Eq a => a -> a -> Bool
== [Char]
name
forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. m (a -> a) -> Operator m a
P.Prefix forall a b. (a -> b) -> a -> b
$ do
FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm
f FC
fc)
backtickOperator :: (Parsing m, MonadState IState m) => m Name
backtickOperator :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator = forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
P.between (forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'`') (forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'`') forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
operatorName :: (Parsing m, MonadState IState m) => m Name
operatorName :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName = [Char] -> Name
sUN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
backtickOperator
operatorFront :: Parsing m => m Name
operatorFront :: forall (m :: * -> *). Parsing m => m Name
operatorFront = do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Name
eqTy forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=") forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => m [Char] -> [[Char]] -> m Name
maybeWithNS (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')') []
fnName :: (Parsing m, MonadState IState m) => m Name
fnName :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall (m :: * -> *). Parsing m => m Name
operatorFront forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"function name"
fixity :: IdrisParser PDecl
fixity :: IdrisParser PDecl
fixity = do ((Int -> Fixity
f, Integer
i, [[Char]]
ops), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent 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 <- forall (m :: * -> *). Parsing m => m Integer
natural
[[Char]]
ops <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
nsroot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Fixity
f, Integer
i, [[Char]]
ops)
let prec :: Int
prec = forall a. Num a => Integer -> a
fromInteger Integer
i
IState
istate <- forall s (m :: * -> *). MonadState s m => m s
get
let infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
istate
let fs :: [FixDecl]
fs = forall a b. (a -> b) -> [a] -> [b]
map (Fixity -> [Char] -> FixDecl
Fix (Int -> Fixity
f Int
prec)) [[Char]]
ops
let redecls :: [(FixDecl, [FixDecl])]
redecls = forall a b. (a -> b) -> [a] -> [b]
map ([FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
alreadyDeclared [FixDecl]
infixes) [FixDecl]
fs
let ill :: [(FixDecl, [FixDecl])]
ill = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixDecl, [FixDecl]) -> Bool
checkValidity) [(FixDecl, [FixDecl])]
redecls
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FixDecl, [FixDecl])]
ill
then do forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
istate { idris_infixes :: [FixDecl]
idris_infixes = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
sort ([FixDecl]
fs forall a. [a] -> [a] -> [a]
++ [FixDecl]
infixes)
, ibc_write :: [IBCWrite]
ibc_write = forall a b. (a -> b) -> [a] -> [b]
map FixDecl -> IBCWrite
IBCFix [FixDecl]
fs forall a. [a] -> [a] -> [a]
++ IState -> [IBCWrite]
ibc_write IState
istate
})
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> Fixity -> [[Char]] -> PDecl' t
PFix FC
fc (Int -> Fixity
f Int
prec) [[Char]]
ops)
else forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ 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\""
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show FixDecl
f forall a. [a] -> [a] -> [a]
++ [Char]
"\" overrides \"" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show FixDecl
x forall a. [a] -> [a] -> [a]
++ [Char]
"\"") [(FixDecl, [FixDecl])]
ill
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, forall a. (a -> Bool) -> [a] -> [a]
filter ((FixDecl -> [Char]
extractName FixDecl
f forall a. Eq a => a -> a -> 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== FixDecl
f) [FixDecl]
fs
extractName :: FixDecl -> String
extractName :: FixDecl -> [Char]
extractName (Fix Fixity
_ [Char]
n) = [Char]
n
checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity IdrisParser PDecl
p = do PDecl
decl <- IdrisParser PDecl
p
case forall {t}. PDecl' t -> Maybe Name
getDeclName PDecl
decl of
Maybe Name
Nothing -> 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
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
_ ) = 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])]
_)) = forall a. a -> Maybe a
Just Name
n
getDeclName PDecl' t
_ = forall a. Maybe a
Nothing
checkNameFixity :: Name -> IdrisParser ()
checkNameFixity :: Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
n = do Bool
fOk <- forall {m :: * -> *}. MonadState IState m => Name -> m Bool
fixityOk Name
n
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
fOk forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$
[Char]
"Missing fixity declaration for " forall a. [a] -> [a] -> [a]
++ 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') | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Char]
opChars) (Text -> [Char]
str Text
n') =
do [FixDecl]
fixities <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IState -> [FixDecl]
idris_infixes forall s (m :: * -> *). MonadState s m => m s
get
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Text -> [Char]
str Text
n') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\ (Fix Fixity
_ [Char]
op) -> [Char]
op) forall a b. (a -> b) -> a -> b
$ [FixDecl]
fixities
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
fixityOk Name
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
fixityType :: IdrisParser (Int -> Fixity)
fixityType :: IdrisParser (Int -> Fixity)
fixityType = do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infixl"; forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixl
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infixr"; forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
Infixr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"infix"; forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
InfixN
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"prefix"; forall (m :: * -> *) a. Monad m => a -> m a
return Int -> Fixity
PrefixN
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 = forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.oneOf [Char]
opChars
commentMarkers :: [String]
= [ [Char]
"--", [Char]
"|||" ]
invalidOperators :: [String]
invalidOperators :: [[Char]]
invalidOperators = [[Char]
":", [Char]
"=>", [Char]
"->", [Char]
"<-", [Char]
"=", [Char]
"?=", [Char]
"|", [Char]
"**", [Char]
"==>", [Char]
"\\", [Char]
"%", [Char]
"~", [Char]
"?", [Char]
"!", [Char]
"@"]
symbolicOperator :: Parsing m => m String
symbolicOperator :: forall (m :: * -> *). Parsing m => m [Char]
symbolicOperator = do [Char]
op <- forall (m :: * -> *) a. Parsing m => m a -> m a
token forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Alternative f => f a -> f [a]
some forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => m Char
operatorLetter
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
op forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([[Char]]
invalidOperators forall a. [a] -> [a] -> [a]
++ [[Char]]
commentMarkers)) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
op forall a. [a] -> [a] -> [a]
++ [Char]
" is not a valid operator"
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
op
reservedOp :: Parsing m => String -> m ()
reservedOp :: forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
name = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$
do forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
name
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy forall (m :: * -> *). Parsing m => m Char
operatorLetter forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> ([Char]
"end of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
name)