{-# 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 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 :: 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]
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
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)
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
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
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
')') []
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"
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
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
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
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]
= [ String
"--", String
"|||" ]
invalidOperators :: [String]
invalidOperators :: [String]
invalidOperators = [String
":", String
"=>", String
"->", String
"<-", String
"=", String
"?=", String
"|", String
"**", String
"==>", String
"\\", String
"%", String
"~", String
"?", String
"!", String
"@"]
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
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)