{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
MultiParamTypeClasses, PatternGuards #-}
module Idris.Parser.Data where
import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Docstrings
import Idris.Parser.Expr
import Idris.Parser.Helpers
import Idris.Parser.Ops
import Prelude hiding (pi)
import Control.Applicative
import Control.Monad.State.Strict
import Data.List
import Data.Maybe
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
record :: SyntaxInfo -> IdrisParser PDecl
record :: SyntaxInfo -> IdrisParser PDecl
record SyntaxInfo
syn = (StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
-> IdrisParser PDecl
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
-> IdrisParser PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
-> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ do
(Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
paramDocs, Accessibility
acc, [DataOpt]
opts) <- StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 (do
(Docstring ()
doc, [(Name, Docstring ())]
paramDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
docComment
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
paramDocs' :: [(Name, Docstring (Either Err PTerm))]
paramDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
| (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
paramDocs ]
Accessibility
acc <- IdrisParser Accessibility
accessibility
[DataOpt]
opts <- [DataOpt] -> IdrisParser [DataOpt]
dataOpts []
[DataOpt]
co <- IdrisParser [DataOpt]
recordI
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
paramDocs', Accessibility
acc, [DataOpt]
opts [DataOpt] -> [DataOpt] -> [DataOpt]
forall a. [a] -> [a] -> [a]
++ [DataOpt]
co))
(Name
tyn_in, FC
nfc) <- 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
fnName
let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
let rsyn :: SyntaxInfo
rsyn = SyntaxInfo
syn { syn_namespace = show (nsroot tyn) :
syn_namespace syn }
[(Name, FC, Plicity, PTerm)]
params <- StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Name, FC, Plicity, PTerm)]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.manyTill (SyntaxInfo
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
rsyn) ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where")
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fields, Maybe (Name, FC)
cname, Docstring (Either Err PTerm)
cdoc) <- IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
indentedBlockS (IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm)))
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> Name
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody SyntaxInfo
rsyn Name
tyn
let fnames :: [Name]
fnames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
rsyn) (((Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))
-> Maybe Name)
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))
-> Maybe Name
forall {a} {b} {b} {c} {d}. (Maybe (a, b), b, c, d) -> Maybe a
getName [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fields)
case Maybe (Name, FC)
cname of
Just (Name, FC)
cn' -> Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn ((Name, FC) -> Name
forall a b. (a, b) -> a
fst (Name, FC)
cn' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
fnames)
Maybe (Name, FC)
Nothing -> () -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl))
-> (FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
forall a b. (a -> b) -> a -> b
$ \FC
fc -> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> [DataOpt]
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> PDecl
forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> [DataOpt]
-> Name
-> FC
-> [(Name, FC, Plicity, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Maybe (Name, FC), Plicity, t,
Maybe (Docstring (Either Err t)))]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> SyntaxInfo
-> PDecl' t
PRecord Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc [DataOpt]
opts Name
tyn FC
nfc [(Name, FC, Plicity, PTerm)]
params [(Name, Docstring (Either Err PTerm))]
paramDocs [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fields Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
syn)
IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"record type declaration"
where
getName :: (Maybe (a, b), b, c, d) -> Maybe a
getName (Just (a
n, b
_), b
_, c
_, d
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
getName (Maybe (a, b), b, c, d)
_ = Maybe a
forall a. Maybe a
Nothing
recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody :: SyntaxInfo
-> Name
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody SyntaxInfo
syn Name
tyn = do
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
(Maybe (Name, FC)
constructorName, Docstring ()
constructorDoc) <- (Maybe (Name, FC), Docstring ())
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Maybe (Name, FC), Docstring ())
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Maybe (Name, FC), Docstring ())
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Maybe (Name, FC)
forall a. Maybe a
Nothing, Docstring ()
forall a. Docstring a
emptyDocstring)
(do (Docstring ()
doc, [(Name, Docstring ())]
_) <- (Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
docComment
(Name, FC)
n <- 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
constructor
(Maybe (Name, FC), Docstring ())
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Maybe (Name, FC), Docstring ())
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, FC) -> Maybe (Name, FC)
forall a. a -> Maybe a
Just (Name, FC)
n, Docstring ()
doc))
let constructorDoc' :: Docstring (Either Err PTerm)
constructorDoc' = SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist Docstring ()
constructorDoc
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
fields <- StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
forall 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]
many (StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]])
-> (StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
indented (StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))],
Maybe (Name, FC), Docstring (Either Err PTerm))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]]
fields, Maybe (Name, FC)
constructorName, Docstring (Either Err PTerm)
constructorDoc')
where
fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
fieldLine :: SyntaxInfo
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn = do
Maybe (Docstring (), [(Name, Docstring ())])
doc <- StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Maybe (Docstring (), [(Name, Docstring ())]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
docComment
Maybe Char
c <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char))
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char)
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
let oneName :: StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
oneName = (do (Name
n, FC
nfc) <- 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
fnName
Maybe (Name, FC)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, FC)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC)))
-> Maybe (Name, FC)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a b. (a -> b) -> a -> b
$ (Name, FC) -> Maybe (Name, FC)
forall a. a -> Maybe a
Just (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc))
StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
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
<|> ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"_" StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a b.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) b
-> StateT IState (WriterT FC (Parsec Void [Char])) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Name, FC)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name, FC)
forall a. Maybe a
Nothing)
[Maybe (Name, FC)]
ns <- StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
IState (WriterT FC (Parsec Void [Char])) [Maybe (Name, FC)]
forall (m :: * -> *) a. Parsing m => m a -> m [a]
commaSeparated StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
oneName
Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
scopedImp SyntaxInfo
syn)
Plicity
p <- Maybe Char -> IdrisParser Plicity
endPlicity Maybe Char
c
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Maybe (Docstring (Either Err PTerm))
doc' = case Maybe (Docstring (), [(Name, Docstring ())])
doc of
Just (Docstring ()
d,[(Name, Docstring ())]
_) -> Docstring (Either Err PTerm)
-> Maybe (Docstring (Either Err PTerm))
forall a. a -> Maybe a
Just (Docstring (Either Err PTerm)
-> Maybe (Docstring (Either Err PTerm)))
-> Docstring (Either Err PTerm)
-> Maybe (Docstring (Either Err PTerm))
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist Docstring ()
d
Maybe (Docstring (), [(Name, Docstring ())])
Nothing -> Maybe (Docstring (Either Err PTerm))
forall a. Maybe a
Nothing
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))])
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
forall a b. (a -> b) -> a -> b
$ (Maybe (Name, FC)
-> (Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm))))
-> [Maybe (Name, FC)]
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
forall a b. (a -> b) -> [a] -> [b]
map (\Maybe (Name, FC)
n -> (Maybe (Name, FC)
n, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
doc')) [Maybe (Name, FC)]
ns
constructor :: (Parsing m, MonadState IState m) => m Name
constructor :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
constructor = [Char] -> m ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"constructor" m () -> 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
*> m Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
endPlicity :: Maybe Char -> IdrisParser Plicity
endPlicity :: Maybe Char -> IdrisParser Plicity
endPlicity (Just Char
_) = do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
Plicity -> IdrisParser Plicity
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
impl
endPlicity Maybe Char
Nothing = Plicity -> IdrisParser Plicity
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
expl
annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate :: SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm))
-> ([Char] -> Either Err PTerm)
-> Docstring ()
-> Docstring (Either Err PTerm)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist
recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
recordParameter :: SyntaxInfo
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
syn =
(do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('
(Name
n, FC
nfc, PTerm
pt) <- (SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy SyntaxInfo
syn IdrisParser (Name, FC, PTerm)
-> IdrisParser (Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
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
<|> SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn)
Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
(Name, FC, Plicity, PTerm)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
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 (Name
n, FC
nfc, PTerm
pt) <- SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn
(Name, FC, Plicity, PTerm)
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
where
namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy SyntaxInfo
syn =
do (Name
n, FC
nfc) <- 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
fnName
Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
(Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc, PTerm
ty)
onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn =
do (Name
n, FC
nfc) <- 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
fnName
(Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc, FC -> PTerm
PType FC
nfc)
dataI :: IdrisParser DataOpts
dataI :: IdrisParser [DataOpt]
dataI = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"data"; [DataOpt] -> IdrisParser [DataOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
IdrisParser [DataOpt]
-> IdrisParser [DataOpt] -> IdrisParser [DataOpt]
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, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"codata"; [DataOpt] -> IdrisParser [DataOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]
recordI :: IdrisParser DataOpts
recordI :: IdrisParser [DataOpt]
recordI = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"record"; [DataOpt] -> IdrisParser [DataOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
IdrisParser [DataOpt]
-> IdrisParser [DataOpt] -> IdrisParser [DataOpt]
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, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"corecord"; [DataOpt] -> IdrisParser [DataOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]
dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts :: [DataOpt] -> IdrisParser [DataOpt]
dataOpts [DataOpt]
opts =
do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"%error_reverse"; [DataOpt] -> IdrisParser [DataOpt]
dataOpts (DataOpt
DataErrRev DataOpt -> [DataOpt] -> [DataOpt]
forall a. a -> [a] -> [a]
: [DataOpt]
opts)
IdrisParser [DataOpt]
-> IdrisParser [DataOpt] -> IdrisParser [DataOpt]
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
<|> [DataOpt] -> IdrisParser [DataOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt]
opts
IdrisParser [DataOpt] -> [Char] -> IdrisParser [DataOpt]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"data options"
data_ :: SyntaxInfo -> IdrisParser PDecl
data_ :: SyntaxInfo -> IdrisParser PDecl
data_ SyntaxInfo
syn = (IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity (IdrisParser PDecl -> IdrisParser PDecl)
-> IdrisParser PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$
do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Accessibility
acc, [DataOpt]
dataOpts) <- StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 (do
(Docstring ()
doc, [(Name, Docstring ())]
argDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
docComment
StateT IState (WriterT FC (Parsec Void [Char])) ()
pushIndent
Accessibility
acc <- IdrisParser Accessibility
accessibility
[DataOpt]
errRev <- [DataOpt] -> IdrisParser [DataOpt]
dataOpts []
[DataOpt]
co <- IdrisParser [DataOpt]
dataI
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
let dataOpts :: [DataOpt]
dataOpts = [DataOpt]
errRev [DataOpt] -> [DataOpt] -> [DataOpt]
forall a. [a] -> [a] -> [a]
++ [DataOpt]
co
doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
| (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
argDocs', Accessibility
acc, [DataOpt]
dataOpts))
(Name
tyn_in, FC
nfc) <- 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
fnName
(do 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 (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':')
PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
PDecl
d <- PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where"
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons <- IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> IdrisParser
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
indentedBlock (SyntaxInfo
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
constructor SyntaxInfo
syn)
Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn (((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Name)
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons)
PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PDecl -> IdrisParser PDecl) -> PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name
-> FC
-> PTerm
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> PData' PTerm
forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tyn FC
nfc PTerm
ty [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons))
StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d) IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
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
[Name]
args <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall 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]
many (do StateT IState (WriterT FC (Parsec Void [Char])) ()
notEndApp
Name
x <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
Name -> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x)
let ty :: PTerm
ty = [PTerm] -> PTerm -> PTerm
bindArgs ((Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> Name -> PTerm
forall a b. a -> b -> a
const (FC -> PTerm
PType FC
nfc)) [Name]
args) (FC -> PTerm
PType FC
nfc)
let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
PDecl
d <- PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
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 (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])) Char
-> 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
-> 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, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where"
let kw :: [Char]
kw = (if DataOpt
Codata DataOpt -> [DataOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataOpt]
dataOpts then [Char]
"co" else [Char]
"") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"data "
let n :: [Char]
n = Name -> [Char]
forall a. Show a => a -> [Char]
show Name
tyn_in [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
let s :: [Char]
s = [Char]
kw [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n
let as :: [Char]
as = [[Char]] -> [Char]
unwords ((Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
forall a. Show a => a -> [Char]
show [Name]
args) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
let ns :: [Char]
ns = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
intersperse [Char]
" -> " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ((\[Char]
x -> [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : Type)") ([Char] -> [Char]) -> (Name -> [Char]) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
args)
let ss :: [Char]
ss = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
intersperse [Char]
" -> " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Name -> [Char]
forall a b. a -> b -> a
const [Char]
"Type") [Name]
args)
let fix1 :: [Char]
fix1 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
as [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = ..."
let fix2 :: [Char]
fix2 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ns [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n ..."
let fix3 :: [Char]
fix3 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ss [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n ..."
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) 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)
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
fixErrorMsg [Char]
"unexpected \"where\"" [[Char]
fix1, [Char]
fix2, [Char]
fix3]
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])]
cons <- StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 (SyntaxInfo
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
simpleConstructor (SyntaxInfo
syn { withAppAllowed = False })) ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"|")
let conty :: PTerm
conty = FC -> PTerm -> [PTerm] -> PTerm
mkPApp FC
nfc (FC -> [FC] -> Name -> PTerm
PRef FC
nfc [] Name
tyn) ((Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (FC -> [FC] -> Name -> PTerm
PRef FC
nfc []) [Name]
args)
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons' <- ((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name]))
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])]
-> IdrisParser
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
x, FC
xfc, [PTerm]
cargs, FC
cfc, [Name]
fs) ->
do let cty :: PTerm
cty = [PTerm] -> PTerm -> PTerm
bindArgs [PTerm]
cargs PTerm
conty
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
x, FC
xfc, PTerm
cty, FC
cfc, [Name]
fs)) [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])]
cons
Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn (((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Name)
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons')
PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PDecl -> IdrisParser PDecl) -> PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name
-> FC
-> PTerm
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> PData' PTerm
forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tyn FC
nfc PTerm
ty [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
cons'))
StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d))
IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"data type declaration"
where
mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp FC
fc PTerm
t [] = PTerm
t
mkPApp FC
fc PTerm
t [PTerm]
xs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
xs)
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs [PTerm]
xs PTerm
t = (PTerm -> PTerm -> PTerm) -> PTerm -> [PTerm] -> PTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl (Int -> [Char] -> Name
sMN Int
0 [Char]
"_t") FC
NoFC) PTerm
t [PTerm]
xs
constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])
constructor :: SyntaxInfo
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
constructor SyntaxInfo
syn
= do (Docstring ()
doc, [(Name, Docstring ())]
argDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
docComment
(Name
cn_in, FC
nfc) <- 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
fnName
let cn :: Name
cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
[Name]
fs <- [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"erase"
StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
(PTerm
ty, FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
| (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
cn
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
argDocs', Name
cn, FC
nfc, PTerm
ty, FC
fc, [Name]
fs)
IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> [Char]
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constructor"
simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])
simpleConstructor :: SyntaxInfo
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
simpleConstructor SyntaxInfo
syn
= (StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
forall a b. (a -> b) -> a -> b
$ do
(Docstring ()
doc, [(Name, Docstring ())]
_) <- (Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs (StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (), [(Name, Docstring ())])
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]))
(Docstring (), [(Name, Docstring ())])
docComment)
IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
(Name
cn_in, FC
nfc) <- 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
fnName
let cn :: Name
cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
[PTerm]
args <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) [PTerm]
forall 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]
many (do StateT IState (WriterT FC (Parsec Void [Char])) ()
notEndApp
SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
cn
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])))
-> (FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(FC
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name]))
forall a b. (a -> b) -> a -> b
$ \FC
fc -> (Docstring (Either Err PTerm)
doc', [], Name
cn, FC
nfc, [PTerm]
args, FC
fc, []))
StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
-> [Char]
-> StateT
IState
(WriterT FC (Parsec Void [Char]))
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constructor"
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"dsl"
Name
n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
[([Char], PTerm)]
bs <- IdrisParser ([Char], PTerm) -> IdrisParser [([Char], PTerm)]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
indentedBlock (SyntaxInfo -> IdrisParser ([Char], PTerm)
overload SyntaxInfo
syn)
let dsl :: DSL
dsl = [([Char], PTerm)] -> DSL -> DSL
mkDSL [([Char], PTerm)]
bs (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn)
DSL -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkDSL DSL
dsl
IState
i <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
IState -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { idris_dsls = addDef n dsl (idris_dsls i) })
PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> DSL -> PDecl
forall t. Name -> DSL' t -> PDecl' t
PDSL Name
n DSL
dsl)
IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dsl block declaration"
where mkDSL :: [(String, PTerm)] -> DSL -> DSL
mkDSL :: [([Char], PTerm)] -> DSL -> DSL
mkDSL [([Char], PTerm)]
bs DSL
dsl = let var :: Maybe PTerm
var = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"variable" [([Char], PTerm)]
bs
first :: Maybe PTerm
first = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_first" [([Char], PTerm)]
bs
next :: Maybe PTerm
next = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_next" [([Char], PTerm)]
bs
leto :: Maybe PTerm
leto = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"let" [([Char], PTerm)]
bs
lambda :: Maybe PTerm
lambda = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"lambda" [([Char], PTerm)]
bs
pi :: Maybe PTerm
pi = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"pi" [([Char], PTerm)]
bs in
DSL
initDSL { dsl_var = var,
index_first = first,
index_next = next,
dsl_lambda = lambda,
dsl_let = leto,
dsl_pi = pi }
checkDSL :: DSL -> IdrisParser ()
checkDSL :: DSL -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkDSL DSL
dsl = () -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
overload :: SyntaxInfo -> IdrisParser (String, PTerm)
overload :: SyntaxInfo -> IdrisParser ([Char], PTerm)
overload SyntaxInfo
syn = do [Char]
o <- OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) [Char]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) [Char]
-> 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 a b. (a -> b) -> a -> b
$ StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall (m :: * -> *). Parsing m => m [Char]
identifier 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 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
<|> [Char]
"let" [Char]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void [Char])) b
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"let"
if [Char]
o [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [[Char]]
overloadable
then [Char] -> IdrisParser ([Char], PTerm)
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> IdrisParser ([Char], PTerm))
-> [Char] -> IdrisParser ([Char], PTerm)
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
o [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not an overloading"
else do
Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
([Char], PTerm) -> IdrisParser ([Char], PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
o, PTerm
t)
IdrisParser ([Char], PTerm)
-> [Char] -> IdrisParser ([Char], PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dsl overload declaratioN"
where overloadable :: [[Char]]
overloadable = [[Char]
"let",[Char]
"lambda",[Char]
"pi",[Char]
"index_first",[Char]
"index_next",[Char]
"variable"]