{-# 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 = (forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent forall a b. (a -> b) -> a -> b
$ do
(Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
paramDocs, Accessibility
acc, [DataOpt]
opts) <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
(Docstring ()
doc, [(Name, Docstring ())]
paramDocs) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = 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, 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
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
paramDocs', Accessibility
acc, [DataOpt]
opts forall a. [a] -> [a] -> [a]
++ [DataOpt]
co))
(Name
tyn_in, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent 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 :: [[Char]]
syn_namespace = forall a. Show a => a -> [Char]
show (Name -> Name
nsroot Name
tyn) forall a. a -> [a] -> [a]
:
SyntaxInfo -> [[Char]]
syn_namespace SyntaxInfo
syn }
[(Name, FC, Plicity, PTerm)]
params <- forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.manyTill (SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
rsyn) (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) <- forall a. IdrisParser a -> IdrisParser a
indentedBlockS 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 = forall a b. (a -> b) -> [a] -> [b]
map (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
rsyn) (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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 (forall a b. (a, b) -> a
fst (Name, FC)
cn' forall a. a -> [a] -> [a]
: [Name]
fnames)
Maybe (Name, FC)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \FC
fc -> 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)
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
_) = forall a. a -> Maybe a
Just a
n
getName (Maybe (a, b), b, c, d)
_ = 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 <- forall s (m :: * -> *). MonadState s m => m s
get
(Maybe (Name, FC)
constructorName, Docstring ()
constructorDoc) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall a. Maybe a
Nothing, forall a. Docstring a
emptyDocstring)
(do (Docstring ()
doc, [(Name, Docstring ())]
_) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
(Name, FC)
n <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
constructor
forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IdrisParser a -> IdrisParser a
indented forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> IdrisParser
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn
forall (m :: * -> *) a. Monad m => a -> m a
return (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
-> IdrisParser
[(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn = do
Maybe (Docstring (), [(Name, Docstring ())])
doc <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
Maybe Char
c <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional forall a b. (a -> b) -> a -> b
$ 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) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"_" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
[Maybe (Name, FC)]
ns <- forall (m :: * -> *) a. Parsing m => m a -> m [a]
commaSeparated StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
oneName
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 <- 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 ())]
_) -> forall a. a -> Maybe a
Just 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 -> forall a. Maybe a
Nothing
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"constructor" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
endPlicity :: Maybe Char -> IdrisParser Plicity
endPlicity :: Maybe Char -> IdrisParser Plicity
endPlicity (Just Char
_) = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
impl
endPlicity Maybe Char
Nothing = 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 = forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode 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 -> IdrisParser (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
syn =
(do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('
(Name
n, FC
nfc, PTerm
pt) <- (SyntaxInfo
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, PTerm)
namedTy SyntaxInfo
syn forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, PTerm)
onlyName SyntaxInfo
syn)
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
(do (Name
n, FC
nfc, PTerm
pt) <- SyntaxInfo
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, PTerm)
onlyName SyntaxInfo
syn
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
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, PTerm)
namedTy SyntaxInfo
syn =
do (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
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
-> StateT
IState (WriterT FC (Parsec Void [Char])) (Name, FC, PTerm)
onlyName SyntaxInfo
syn =
do (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"data"; forall (m :: * -> *) a. Monad m => a -> m a
return []
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"codata"; forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]
recordI :: IdrisParser DataOpts
recordI :: IdrisParser [DataOpt]
recordI = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"record"; forall (m :: * -> *) a. Monad m => a -> m a
return []
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"corecord"; forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]
dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts :: [DataOpt] -> IdrisParser [DataOpt]
dataOpts [DataOpt]
opts =
do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"%error_reverse"; [DataOpt] -> IdrisParser [DataOpt]
dataOpts (DataOpt
DataErrRev forall a. a -> [a] -> [a]
: [DataOpt]
opts)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt]
opts
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 forall a b. (a -> b) -> a -> b
$
do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Accessibility
acc, [DataOpt]
dataOpts) <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
(Docstring ()
doc, [(Name, Docstring ())]
argDocs) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (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 <- forall s (m :: * -> *). MonadState s m => m s
get
let dataOpts :: [DataOpt]
dataOpts = [DataOpt]
errRev forall a. [a] -> [a] -> [a]
++ [DataOpt]
co
doc' :: Docstring (Either Err PTerm)
doc' = 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, 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 ]
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) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
(do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (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 <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (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 (forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
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 <- forall a. IdrisParser a -> IdrisParser [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 (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)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 (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
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
[Name]
args <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void [Char])) ()
notEndApp
Name
x <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x)
let ty :: PTerm
ty = [PTerm] -> PTerm -> PTerm
bindArgs (forall a b. (a -> b) -> [a] -> [b]
map (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 <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (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 (forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'=') forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where"
let kw :: [Char]
kw = (if DataOpt
Codata forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataOpt]
dataOpts then [Char]
"co" else [Char]
"") forall a. [a] -> [a] -> [a]
++ [Char]
"data "
let n :: [Char]
n = forall a. Show a => a -> [Char]
show Name
tyn_in forall a. [a] -> [a] -> [a]
++ [Char]
" "
let s :: [Char]
s = [Char]
kw forall a. [a] -> [a] -> [a]
++ [Char]
n
let as :: [Char]
as = [[Char]] -> [Char]
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Name]
args) forall a. [a] -> [a] -> [a]
++ [Char]
" "
let ns :: [Char]
ns = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse [Char]
" -> " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((\[Char]
x -> [Char]
"(" forall a. [a] -> [a] -> [a]
++ [Char]
x forall a. [a] -> [a] -> [a]
++ [Char]
" : Type)") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [Name]
args)
let ss :: [Char]
ss = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse [Char]
" -> " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> b -> a
const [Char]
"Type") [Name]
args)
let fix1 :: [Char]
fix1 = [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
as forall a. [a] -> [a] -> [a]
++ [Char]
" = ..."
let fix2 :: [Char]
fix2 = [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ [Char]
ns forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n ..."
let fix3 :: [Char]
fix3 = [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ [Char]
ss forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n ..."
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail 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 <- forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 (SyntaxInfo
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
simpleConstructor (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (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) (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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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
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 (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')
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 (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
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d))
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 (forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
xs)
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs [PTerm]
xs PTerm
t = 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) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
(Name
cn_in, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
let cn :: Name
cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
[Name]
fs <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"erase"
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
(PTerm
ty, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = 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, 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
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)
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
-> IdrisParser
(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
[Name])
simpleConstructor SyntaxInfo
syn
= (forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent forall a b. (a -> b) -> a -> b
$ do
(Docstring ()
doc, [(Name, Docstring ())]
_) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try IdrisParser (Docstring (), [(Name, Docstring ())])
docComment)
IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
let doc' :: Docstring (Either Err PTerm)
doc' = 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) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent 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 <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \FC
fc -> (Docstring (Either Err PTerm)
doc', [], Name
cn, FC
nfc, [PTerm]
args, FC
fc, []))
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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"dsl"
Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
[([Char], PTerm)]
bs <- forall a. IdrisParser a -> IdrisParser [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 <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { idris_dsls :: Ctxt DSL
idris_dsls = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n DSL
dsl (IState -> Ctxt DSL
idris_dsls IState
i) })
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Name -> DSL' t -> PDecl' t
PDSL Name
n DSL
dsl)
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 = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"variable" [([Char], PTerm)]
bs
first :: Maybe PTerm
first = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_first" [([Char], PTerm)]
bs
next :: Maybe PTerm
next = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_next" [([Char], PTerm)]
bs
leto :: Maybe PTerm
leto = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"let" [([Char], PTerm)]
bs
lambda :: Maybe PTerm
lambda = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"lambda" [([Char], PTerm)]
bs
pi :: Maybe PTerm
pi = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"pi" [([Char], PTerm)]
bs in
DSL
initDSL { dsl_var :: Maybe PTerm
dsl_var = Maybe PTerm
var,
index_first :: Maybe PTerm
index_first = Maybe PTerm
first,
index_next :: Maybe PTerm
index_next = Maybe PTerm
next,
dsl_lambda :: Maybe PTerm
dsl_lambda = Maybe PTerm
lambda,
dsl_let :: Maybe PTerm
dsl_let = Maybe PTerm
leto,
dsl_pi :: Maybe PTerm
dsl_pi = Maybe PTerm
pi }
checkDSL :: DSL -> IdrisParser ()
checkDSL :: DSL -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkDSL DSL
dsl = 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 <- forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => m [Char]
identifier forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char]
"let" forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"let"
if [Char]
o forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [[Char]]
overloadable
then forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show [Char]
o forall a. [a] -> [a] -> [a]
++ [Char]
" is not an overloading"
else do
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
PTerm
t <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
o, PTerm
t)
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"]