{-|
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.Options
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 syn :: 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
                (doc :: Docstring (Either Err PTerm)
doc, paramDocs :: [(Name, Docstring (Either Err PTerm))]
paramDocs, acc :: Accessibility
acc, opts :: [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
                      (doc :: Docstring ()
doc, paramDocs :: [(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)
                                     | (n :: Name
n, d :: 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))
                (tyn_in :: Name
tyn_in, nfc :: 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 "where")
                (fields :: [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields, cname :: Maybe (Name, FC)
cname, cdoc :: 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 cn' :: (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)
                     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
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
<?> "record type declaration"
  where
    getName :: (Maybe (a, b), b, c, d) -> Maybe a
getName (Just (n :: a
n, _), _, _, _) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
    getName _ = 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 syn :: SyntaxInfo
syn tyn :: Name
tyn = do
        IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get

        (constructorName :: Maybe (Name, FC)
constructorName, constructorDoc :: 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 (doc :: Docstring ()
doc, _) <- (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 syn :: 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 '{'
            let oneName :: StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
oneName = (do (n :: Name
n, nfc :: 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 "_" 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 ':'
            -- 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 (d :: Docstring ()
d,_) -> 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
                        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 (\n :: 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 "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 _) = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
                                 Plicity -> IdrisParser Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
impl
        endPlicity 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 syn :: SyntaxInfo
syn ist :: 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 syn :: SyntaxInfo
syn =
  (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '('
      (n :: Name
n, nfc :: FC
nfc, pt :: 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 ')'
      (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 (n :: Name
n, nfc :: FC
nfc, pt :: 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 syn :: SyntaxInfo
syn =
      do (n :: Name
n, nfc :: 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 ':'
         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 syn :: SyntaxInfo
syn =
      do (n :: Name
n, nfc :: 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 "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 "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 "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 "corecord"; [DataOpt] -> IdrisParser [DataOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return [DataOpt
Codata]

dataOpts :: DataOpts -> IdrisParser DataOpts
dataOpts :: [DataOpt] -> IdrisParser [DataOpt]
dataOpts opts :: [DataOpt]
opts =
      do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "%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
<?> "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_ syn :: SyntaxInfo
syn = (IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity (IdrisParser PDecl -> IdrisParser PDecl)
-> IdrisParser PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$
            do (doc :: Docstring (Either Err PTerm)
doc, argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs, acc :: Accessibility
acc, dataOpts :: [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
                    (doc :: Docstring ()
doc, argDocs :: [(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)
                                   | (n :: Name
n, d :: 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))
               (tyn_in :: Name
tyn_in, nfc :: 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 ':')
                   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 "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 (\ (_, _, n :: Name
n, _, _, _, _) -> 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 '=') 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 "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 "co" else "") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "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]
++ " "
                                               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]
++ " "
                                               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]
forall a b. (a -> b) -> a -> b
$ (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((\x :: String
x -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : 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]
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 "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]
++ " = ..."
                                               let fix2 :: String
fix2 = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> Type where\n  ..."
                                               let fix3 :: String
fix3 = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ss String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> 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 "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 "|")
                      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 (\ (doc :: Docstring (Either Err PTerm)
doc, argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs, x :: Name
x, xfc :: FC
xfc, cargs :: [PTerm]
cargs, cfc :: FC
cfc, fs :: [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 (\ (_, _, n :: Name
n, _, _, _, _) -> 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
<?> "data type declaration"
  where
    mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
    mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp fc :: FC
fc t :: PTerm
t [] = PTerm
t
    mkPApp fc :: FC
fc t :: PTerm
t xs :: [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 xs :: [PTerm]
xs t :: 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 0 "_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 syn :: SyntaxInfo
syn
    = do (doc :: Docstring ()
doc, argDocs :: [(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
         (cn_in :: Name
cn_in, nfc :: 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 ':'
         [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 '%'; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "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 ','))
         (ty :: PTerm
ty, fc :: 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)
                        | (n :: Name
n, d :: 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
<?> "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 syn :: 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
          (doc :: Docstring ()
doc, _) <- (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
          (cn_in :: Name
cn_in, nfc :: 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
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
<?> "constructor"
{- | Parses a dsl block declaration
DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
 -}
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "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
<?> "dsl block declaration"
    where mkDSL :: [(String, PTerm)] -> DSL -> DSL
          mkDSL :: [(String, PTerm)] -> DSL -> DSL
mkDSL bs :: [(String, PTerm)]
bs dsl :: DSL
dsl = let var :: Maybe PTerm
var    = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "variable" [(String, PTerm)]
bs
                             first :: Maybe PTerm
first  = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "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 "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 "let" [(String, PTerm)]
bs
                             lambda :: Maybe PTerm
lambda = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "lambda" [(String, PTerm)]
bs
                             pi :: Maybe PTerm
pi     = String -> [(String, PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "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
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 syn :: 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
<|> "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 "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]
++ " is not an overloading"
                     else do
                       Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
                       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
<?> "dsl overload declaratioN"
    where overloadable :: [String]
overloadable = ["let","lambda","pi","index_first","index_next","variable"]