{-|
Module      : Idris.Parser.Data
Description : Parse Data declarations.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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

{- | Parses a record type declaration
Record ::=
    DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
-}
record :: SyntaxInfo -> IdrisParser PDecl
record :: SyntaxInfo -> IdrisParser PDecl
record SyntaxInfo
syn = (StateT IState (WriterT FC (Parsec Void String)) (FC -> PDecl)
-> IdrisParser PDecl
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT IState (WriterT FC (Parsec Void String)) (FC -> PDecl)
 -> IdrisParser PDecl)
-> StateT IState (WriterT FC (Parsec Void String)) (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 String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
  (Docstring (), [(Name, Docstring ())])
docComment
                      IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      let doc' :: Docstring (Either Err PTerm)
doc' = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
                          paramDocs' :: [(Name, Docstring (Either Err PTerm))]
paramDocs' = [ (Name
n, (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> 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 String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) 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 :: [String]
syn_namespace = Name -> String
forall a. Show a => a -> String
show (Name -> Name
nsroot Name
tyn) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                                                    SyntaxInfo -> [String]
syn_namespace SyntaxInfo
syn }
                [(Name, FC, Plicity, PTerm)]
params <- StateT
  IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(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 String)) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
rsyn) (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"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. IdrisParser a -> IdrisParser 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 String)) ()
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 String)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                (FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PDecl)
 -> StateT IState (WriterT FC (Parsec Void String)) (FC -> PDecl))
-> (FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void String)) (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 -> String -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"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 String)) 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 String))
     (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
  (Docstring (), [(Name, Docstring ())])
docComment
                                                 (Name, FC)
n <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
constructor
                                                 (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
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 String))
  [(Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [[(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT
   IState
   (WriterT FC (Parsec Void String))
   [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      [[(Maybe (Name, FC), Plicity, PTerm,
         Maybe (Docstring (Either Err PTerm)))]])
-> (StateT
      IState
      (WriterT FC (Parsec Void String))
      [(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]
    -> StateT
         IState
         (WriterT FC (Parsec Void String))
         [(Maybe (Name, FC), Plicity, PTerm,
           Maybe (Docstring (Either Err PTerm)))])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [[(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 String))
  [(Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
forall a. IdrisParser a -> IdrisParser a
indented (StateT
   IState
   (WriterT FC (Parsec Void String))
   [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      [[(Maybe (Name, FC), Plicity, PTerm,
         Maybe (Docstring (Either Err PTerm)))]])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [[(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]]
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(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 (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 String))
     [(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 String))
  (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Docstring (), [(Name, Docstring ())]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
docComment
            Maybe Char
c <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Char)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT IState (WriterT FC (Parsec Void String)) Char
 -> StateT IState (WriterT FC (Parsec Void String)) (Maybe Char))
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Char)
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
            let oneName :: StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
oneName = (do (Name
n, FC
nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                              Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, FC)
 -> StateT
      IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC)))
-> Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void String)) (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 String)) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"_" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
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 String)) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void String)) [Maybe (Name, FC)]
forall (m :: * -> *) a. Parsing m => m a -> m [a]
commaSeparated StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
oneName
            Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
            -- Implicits are scoped in fields (fields aren't top level)
            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 String)) 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 -- Temp: Throws away any possible arg docs
                        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 String))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
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 String))
      [(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 String))
     [(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 :: m Name
constructor = String -> m ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"constructor" m () -> m Name -> m Name
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 String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
                                 Plicity -> IdrisParser Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
impl
        endPlicity Maybe Char
Nothing = Plicity -> IdrisParser Plicity
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 = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode ((String -> Either Err PTerm)
 -> Docstring () -> Docstring (Either Err PTerm))
-> (String -> Either Err PTerm)
-> Docstring ()
-> Docstring (Either Err PTerm)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist

recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
recordParameter :: SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
syn =
  (do Char -> StateT IState (WriterT FC (Parsec Void String)) 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 (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 String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
      (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
  StateT
  IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, Plicity, PTerm)
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 String)) (Name, FC, Plicity, PTerm)
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 String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
         Char -> StateT IState (WriterT FC (Parsec Void String)) 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 (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 String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
         (Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc, FC -> PTerm
PType FC
nfc)

{- | Parses data declaration type (normal or codata)
DataI ::= 'data' | 'codata';
-}
dataI :: IdrisParser DataOpts
dataI :: IdrisParser [DataOpt]
dataI = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"data"; [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    IdrisParser [DataOpt]
-> IdrisParser [DataOpt] -> IdrisParser [DataOpt]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"codata"; [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]

recordI :: IdrisParser DataOpts
recordI :: IdrisParser [DataOpt]
recordI = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"record"; [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          IdrisParser [DataOpt]
-> IdrisParser [DataOpt] -> IdrisParser [DataOpt]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"corecord"; [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]

dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts :: [DataOpt] -> IdrisParser [DataOpt]
dataOpts [DataOpt]
opts =
      do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"%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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt]
opts
  IdrisParser [DataOpt] -> String -> IdrisParser [DataOpt]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"data options"

{- | Parses a data type declaration
Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
       | DocComment? Accessibility? DataI FnName Name*   DataRest?
       ;
Constructor' ::= Constructor KeepTerminator;
ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

DataRest ::= '=' SimpleConstructorList Terminator
            | 'where'!
           ;
SimpleConstructorList ::=
    SimpleConstructor
  | SimpleConstructor '|' SimpleConstructorList
  ;
-}
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 String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
  (Docstring (), [(Name, Docstring ())])
docComment
                    StateT IState (WriterT FC (Parsec Void String)) ()
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 String)) 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' = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
                        argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> 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 String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
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 String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
               (do StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) 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
                     String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"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. 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 String)) ()
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 (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 String)) ()
terminator
                   PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d) IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
                    [Name]
args <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndApp
                                     Name
x <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                                     Name -> StateT IState (WriterT FC (Parsec Void String)) Name
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 String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'=') StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
                                               let kw :: String
kw = (if DataOpt
Codata DataOpt -> [DataOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataOpt]
dataOpts then String
"co" else String
"") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"data "
                                               let n :: String
n  = Name -> String
forall a. Show a => a -> String
show Name
tyn_in String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                                               let s :: String
s  = String
kw String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n
                                               let as :: String
as = [String] -> String
unwords ((Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
forall a. Show a => a -> String
show [Name]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
                                               let ns :: String
ns = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
" -> " ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((\String
x -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : Type)") (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show) [Name]
args)
                                               let ss :: String
ss = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
" -> " ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Name -> String
forall a b. a -> b -> a
const String
"Type") [Name]
args)
                                               let fix1 :: String
fix1 = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = ..."
                                               let fix2 :: String
fix2 = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> Type where\n  ..."
                                               let fix3 :: String
fix3 = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ss String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> Type where\n  ..."
                                               String -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT IState (WriterT FC (Parsec Void String)) Char)
-> String -> StateT IState (WriterT FC (Parsec Void String)) Char
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
fixErrorMsg String
"unexpected \"where\"" [String
fix1, String
fix2, String
fix3]
                      [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
  [Name])]
cons <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
   [Name])
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(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 String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
simpleConstructor (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp String
"|")
                      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)
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 (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 String)) ()
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 (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 String)) ()
terminator
                    PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d))
           IdrisParser PDecl -> String -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"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 (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl (Int -> String -> Name
sMN Int
0 String
"_t") FC
NoFC) PTerm
t [PTerm]
xs


{- | Parses a type constructor declaration
  Constructor ::= DocComment? FnName TypeSig;
-}
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 String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
  (Docstring (), [(Name, Docstring ())])
docComment
         (Name
cn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) 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 String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
         [Name]
fs <- [Name]
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"erase"
                               StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
         (PTerm
ty, FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (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 String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
         let doc' :: Docstring (Either Err PTerm)
doc' = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
             argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
                        | (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
         Name -> StateT IState (WriterT FC (Parsec Void String)) ()
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 (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])
-> String
-> 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 -> String -> m a
<?> String
"constructor"

{- | Parses a constructor for simple discriminated union data types
  SimpleConstructor ::= FnName SimpleExpr* DocComment?
-}
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 String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
simpleConstructor SyntaxInfo
syn
     = (StateT
  IState
  (WriterT FC (Parsec Void String))
  (FC
   -> (Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
       [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
   (FC
    -> (Docstring (Either Err PTerm),
        [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
        [Name]))
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      (Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
       [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (FC
      -> (Docstring (Either Err PTerm),
          [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
          [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 String))
  (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (), [(Name, Docstring ())])
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
docComment)
          IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
          let doc' :: Docstring (Either Err PTerm)
doc' = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
          (Name
cn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) 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 String)) [PTerm]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndApp
                           SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
          Name -> StateT IState (WriterT FC (Parsec Void String)) ()
checkNameFixity Name
cn
          (FC
 -> (Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
     [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (FC
      -> (Docstring (Either Err PTerm),
          [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
          [Name]))
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 String))
      (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 String))
     (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 String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
   [Name])
-> String
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (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 -> String -> m a
<?> String
"constructor"
{- | Parses a dsl block declaration
DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
 -}
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"dsl"
             Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
             [(String, PTerm)]
bs <- IdrisParser (String, PTerm) -> IdrisParser [(String, PTerm)]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock (SyntaxInfo -> IdrisParser (String, PTerm)
overload SyntaxInfo
syn)
             let dsl :: DSL
dsl = [(String, PTerm)] -> DSL -> DSL
mkDSL [(String, PTerm)]
bs (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn)
             DSL -> StateT IState (WriterT FC (Parsec Void String)) ()
checkDSL DSL
dsl
             IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
             IState -> StateT IState (WriterT FC (Parsec Void String)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { idris_dsls :: Ctxt DSL
idris_dsls = Name -> DSL -> Ctxt DSL -> Ctxt DSL
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n DSL
dsl (IState -> Ctxt DSL
idris_dsls IState
i) })
             PDecl -> IdrisParser PDecl
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 -> String -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"dsl block declaration"
    where mkDSL :: [(String, PTerm)] -> DSL -> DSL
          mkDSL :: [(String, PTerm)] -> DSL -> DSL
mkDSL [(String, PTerm)]
bs DSL
dsl = let var :: Maybe PTerm
var    = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"variable" [(String, PTerm)]
bs
                             first :: Maybe PTerm
first  = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"index_first" [(String, PTerm)]
bs
                             next :: Maybe PTerm
next   = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"index_next" [(String, PTerm)]
bs
                             leto :: Maybe PTerm
leto   = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"let" [(String, PTerm)]
bs
                             lambda :: Maybe PTerm
lambda = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"lambda" [(String, PTerm)]
bs
                             pi :: Maybe PTerm
pi     = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
"pi" [(String, 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 }

{- | Checks DSL for errors -}
-- FIXME: currently does nothing, check if DSL is really sane
--
-- Issue #1595 on the Issue Tracker
--
--     https://github.com/idris-lang/Idris-dev/issues/1595
--
checkDSL :: DSL -> IdrisParser ()
checkDSL :: DSL -> StateT IState (WriterT FC (Parsec Void String)) ()
checkDSL DSL
dsl = () -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{- | Parses a DSL overload declaration
OverloadIdentifier ::= 'let' | Identifier;
Overload ::= OverloadIdentifier '=' Expr;
-}
overload :: SyntaxInfo -> IdrisParser (String, PTerm)
overload :: SyntaxInfo -> IdrisParser (String, PTerm)
overload SyntaxInfo
syn = do String
o <- OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void String)) String
 -> StateT IState (WriterT FC (Parsec Void String)) String)
-> StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall a b. (a -> b) -> a -> b
$ StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
identifier StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String
"let" String
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"let"
                  if String
o String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
overloadable
                     then String -> IdrisParser (String, PTerm)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IdrisParser (String, PTerm))
-> String -> IdrisParser (String, PTerm)
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not an overloading"
                     else do
                       Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
                       PTerm
t <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                       (String, PTerm) -> IdrisParser (String, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
o, PTerm
t)
               IdrisParser (String, PTerm)
-> String -> IdrisParser (String, PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"dsl overload declaratioN"
    where overloadable :: [String]
overloadable = [String
"let",String
"lambda",String
"pi",String
"index_first",String
"index_next",String
"variable"]