{-|
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 [Char])) (FC -> PDecl)
-> IdrisParser PDecl
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
 -> IdrisParser PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
-> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ do
                (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
paramDocs, Accessibility
acc, [DataOpt]
opts) <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
                      (Docstring ()
doc, [(Name, Docstring ())]
paramDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment
                      IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
                          paramDocs' :: [(Name, Docstring (Either Err PTerm))]
paramDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
                                     | (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
paramDocs ]
                      Accessibility
acc <- IdrisParser Accessibility
accessibility
                      [DataOpt]
opts <- [DataOpt] -> IdrisParser [DataOpt]
dataOpts []
                      [DataOpt]
co <- IdrisParser [DataOpt]
recordI
                      (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
paramDocs', Accessibility
acc, [DataOpt]
opts [DataOpt] -> [DataOpt] -> [DataOpt]
forall a. [a] -> [a] -> [a]
++ [DataOpt]
co))
                (Name
tyn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                let rsyn :: SyntaxInfo
rsyn = SyntaxInfo
syn { syn_namespace = show (nsroot tyn) :
                                                    syn_namespace syn }
                [(Name, FC, Plicity, PTerm)]
params <- StateT
  IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Name, FC, Plicity, PTerm)]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.manyTill (SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
rsyn) ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where")
                ([(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields, Maybe (Name, FC)
cname, Docstring (Either Err PTerm)
cdoc) <- IdrisParser
  ([(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))],
   Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
indentedBlockS (IdrisParser
   ([(Maybe (Name, FC), Plicity, PTerm,
      Maybe (Docstring (Either Err PTerm)))],
    Maybe (Name, FC), Docstring (Either Err PTerm))
 -> IdrisParser
      ([(Maybe (Name, FC), Plicity, PTerm,
         Maybe (Docstring (Either Err PTerm)))],
       Maybe (Name, FC), Docstring (Either Err PTerm)))
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> Name
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody SyntaxInfo
rsyn Name
tyn
                let fnames :: [Name]
fnames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
rsyn) (((Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))
 -> Maybe Name)
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Name, FC), Plicity, PTerm,
 Maybe (Docstring (Either Err PTerm)))
-> Maybe Name
forall {a} {b} {b} {c} {d}. (Maybe (a, b), b, c, d) -> Maybe a
getName [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields)
                case Maybe (Name, FC)
cname of
                     Just (Name, FC)
cn' -> Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn ((Name, FC) -> Name
forall a b. (a, b) -> a
fst (Name, FC)
cn' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
fnames)
                     Maybe (Name, FC)
Nothing -> () -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                (FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PDecl)
 -> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl))
-> (FC -> PDecl)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PDecl)
forall a b. (a -> b) -> a -> b
$ \FC
fc -> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> [DataOpt]
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> PDecl
forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> [DataOpt]
-> Name
-> FC
-> [(Name, FC, Plicity, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Maybe (Name, FC), Plicity, t,
     Maybe (Docstring (Either Err t)))]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> SyntaxInfo
-> PDecl' t
PRecord Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc [DataOpt]
opts Name
tyn FC
nfc [(Name, FC, Plicity, PTerm)]
params [(Name, Docstring (Either Err PTerm))]
paramDocs [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
syn)
              IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"record type declaration"
  where
    getName :: (Maybe (a, b), b, c, d) -> Maybe a
getName (Just (a
n, b
_), b
_, c
_, d
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
    getName (Maybe (a, b), b, c, d)
_ = Maybe a
forall a. Maybe a
Nothing

    recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
    recordBody :: SyntaxInfo
-> Name
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
recordBody SyntaxInfo
syn Name
tyn = do
        IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get

        (Maybe (Name, FC)
constructorName, Docstring ()
constructorDoc) <- (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Maybe (Name, FC), Docstring ())
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Maybe (Name, FC)
forall a. Maybe a
Nothing, Docstring ()
forall a. Docstring a
emptyDocstring)
                                             (do (Docstring ()
doc, [(Name, Docstring ())]
_) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment
                                                 (Name, FC)
n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
constructor
                                                 (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Maybe (Name, FC), Docstring ())
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, FC) -> Maybe (Name, FC)
forall a. a -> Maybe a
Just (Name, FC)
n, Docstring ()
doc))

        let constructorDoc' :: Docstring (Either Err PTerm)
constructorDoc' = SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist Docstring ()
constructorDoc

        [[(Maybe (Name, FC), Plicity, PTerm,
   Maybe (Docstring (Either Err PTerm)))]]
fields <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  [(Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [[(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT
   IState
   (WriterT FC (Parsec Void [Char]))
   [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      [[(Maybe (Name, FC), Plicity, PTerm,
         Maybe (Docstring (Either Err PTerm)))]])
-> (StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      [(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]
    -> StateT
         IState
         (WriterT FC (Parsec Void [Char]))
         [(Maybe (Name, FC), Plicity, PTerm,
           Maybe (Docstring (Either Err PTerm)))])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [[(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  [(Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
indented (StateT
   IState
   (WriterT FC (Parsec Void [Char]))
   [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      [[(Maybe (Name, FC), Plicity, PTerm,
         Maybe (Docstring (Either Err PTerm)))]])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [[(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))]]
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn

        ([(Maybe (Name, FC), Plicity, PTerm,
   Maybe (Docstring (Either Err PTerm)))],
 Maybe (Name, FC), Docstring (Either Err PTerm))
-> IdrisParser
     ([(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))],
      Maybe (Name, FC), Docstring (Either Err PTerm))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[(Maybe (Name, FC), Plicity, PTerm,
   Maybe (Docstring (Either Err PTerm)))]]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Maybe (Name, FC), Plicity, PTerm,
   Maybe (Docstring (Either Err PTerm)))]]
fields, Maybe (Name, FC)
constructorName, Docstring (Either Err PTerm)
constructorDoc')
      where
        fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
        fieldLine :: SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
fieldLine SyntaxInfo
syn = do
            Maybe (Docstring (), [(Name, Docstring ())])
doc <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Maybe (Docstring (), [(Name, Docstring ())]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment
            Maybe Char
c <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT IState (WriterT FC (Parsec Void [Char])) Char
 -> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char))
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) (Maybe Char)
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
            let oneName :: StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
oneName = (do (Name
n, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                              Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, FC)
 -> StateT
      IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC)))
-> Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a b. (a -> b) -> a -> b
$ (Name, FC) -> Maybe (Name, FC)
forall a. a -> Maybe a
Just (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc))
                          StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"_" StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a b.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) b
-> StateT IState (WriterT FC (Parsec Void [Char])) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name, FC)
forall a. Maybe a
Nothing)
            [Maybe (Name, FC)]
ns <- StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void [Char])) [Maybe (Name, FC)]
forall (m :: * -> *) a. Parsing m => m a -> m [a]
commaSeparated StateT IState (WriterT FC (Parsec Void [Char])) (Maybe (Name, FC))
oneName
            Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
            -- 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 [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
            let doc' :: Maybe (Docstring (Either Err PTerm))
doc' = case Maybe (Docstring (), [(Name, Docstring ())])
doc of -- 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 [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Maybe (Name, FC), Plicity, PTerm,
   Maybe (Docstring (Either Err PTerm)))]
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      [(Maybe (Name, FC), Plicity, PTerm,
        Maybe (Docstring (Either Err PTerm)))])
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Maybe (Name, FC), Plicity, PTerm,
       Maybe (Docstring (Either Err PTerm)))]
forall a b. (a -> b) -> a -> b
$ (Maybe (Name, FC)
 -> (Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm))))
-> [Maybe (Name, FC)]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
forall a b. (a -> b) -> [a] -> [b]
map (\Maybe (Name, FC)
n -> (Maybe (Name, FC)
n, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
doc')) [Maybe (Name, FC)]
ns

        constructor :: (Parsing m, MonadState IState m) => m Name
        constructor :: forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
constructor = [Char] -> m ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"constructor" m () -> m Name -> m Name
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName

        endPlicity :: Maybe Char -> IdrisParser Plicity
        endPlicity :: Maybe Char -> IdrisParser Plicity
endPlicity (Just Char
_) = do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
                                 Plicity -> IdrisParser Plicity
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
impl
        endPlicity Maybe Char
Nothing = Plicity -> IdrisParser Plicity
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Plicity
expl

        annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
        annotate :: SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (([Char] -> Either Err PTerm)
 -> Docstring () -> Docstring (Either Err PTerm))
-> ([Char] -> Either Err PTerm)
-> Docstring ()
-> Docstring (Either Err PTerm)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist

recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
recordParameter :: SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
recordParameter SyntaxInfo
syn =
  (do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('
      (Name
n, FC
nfc, PTerm
pt) <- (SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy SyntaxInfo
syn IdrisParser (Name, FC, PTerm)
-> IdrisParser (Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn)
      Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
      (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
  StateT
  IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  (do (Name
n, FC
nfc, PTerm
pt) <- SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn
      (Name, FC, Plicity, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Name, FC, Plicity, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, Plicity
expl, PTerm
pt))
  where
    namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
    namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy SyntaxInfo
syn =
      do (Name
n, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
         Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
         PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
         (Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc, PTerm
ty)
    onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
    onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn =
      do (Name
n, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
         (Name, FC, PTerm) -> IdrisParser (Name, FC, PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n, FC
nfc, FC -> PTerm
PType FC
nfc)

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

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

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

{- | 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 [Char]))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
                    (Docstring ()
doc, [(Name, Docstring ())]
argDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment
                    StateT IState (WriterT FC (Parsec Void [Char])) ()
pushIndent
                    Accessibility
acc <- IdrisParser Accessibility
accessibility
                    [DataOpt]
errRev <- [DataOpt] -> IdrisParser [DataOpt]
dataOpts []
                    [DataOpt]
co <- IdrisParser [DataOpt]
dataI
                    IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
                    let dataOpts :: [DataOpt]
dataOpts = [DataOpt]
errRev [DataOpt] -> [DataOpt] -> [DataOpt]
forall a. [a] -> [a] -> [a]
++ [DataOpt]
co
                        doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
                        argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
                                   | (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
                    (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility, [DataOpt])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
argDocs', Accessibility
acc, [DataOpt]
dataOpts))
               (Name
tyn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
               (do StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':')
                   PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
                   let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                   PDecl
d <- PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
                     [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where"
                     [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons <- IdrisParser
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
   [Name])
-> IdrisParser
     [(Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
       [Name])]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
indentedBlock (SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
      [Name])
constructor SyntaxInfo
syn)
                     Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn (((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])
 -> Name)
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons)
                     PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PDecl -> IdrisParser PDecl) -> PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name
-> FC
-> PTerm
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> PData' PTerm
forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tyn FC
nfc PTerm
ty [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons))
                   StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
                   PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d) IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
                    [Name]
args <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void [Char])) ()
notEndApp
                                     Name
x <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                                     Name -> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x)
                    let ty :: PTerm
ty = [PTerm] -> PTerm -> PTerm
bindArgs ((Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> Name -> PTerm
forall a b. a -> b -> a
const (FC -> PTerm
PType FC
nfc)) [Name]
args) (FC -> PTerm
PType FC
nfc)
                    let tyn :: Name
tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                    PDecl
d <- PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl Name
tyn FC
nfc PTerm
ty)) (do
                      StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'=') StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"where"
                                               let kw :: [Char]
kw = (if DataOpt
Codata DataOpt -> [DataOpt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataOpt]
dataOpts then [Char]
"co" else [Char]
"") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"data "
                                               let n :: [Char]
n  = Name -> [Char]
forall a. Show a => a -> [Char]
show Name
tyn_in [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
                                               let s :: [Char]
s  = [Char]
kw [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n
                                               let as :: [Char]
as = [[Char]] -> [Char]
unwords ((Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
forall a. Show a => a -> [Char]
show [Name]
args) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
                                               let ns :: [Char]
ns = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
intersperse [Char]
" -> " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ((\[Char]
x -> [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : Type)") ([Char] -> [Char]) -> (Name -> [Char]) -> Name -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
args)
                                               let ss :: [Char]
ss = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
intersperse [Char]
" -> " ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Name -> [Char]
forall a b. a -> b -> a
const [Char]
"Type") [Name]
args)
                                               let fix1 :: [Char]
fix1 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
as [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = ..."
                                               let fix2 :: [Char]
fix2 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ns [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n  ..."
                                               let fix3 :: [Char]
fix3 = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
ss [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> Type where\n  ..."
                                               [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Char)
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
fixErrorMsg [Char]
"unexpected \"where\"" [[Char]
fix1, [Char]
fix2, [Char]
fix3]
                      [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
  [Name])]
cons <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
   [Name])
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     [(Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
       [Name])]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 (SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
simpleConstructor (SyntaxInfo
syn { withAppAllowed = False })) ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"|")
                      let conty :: PTerm
conty = FC -> PTerm -> [PTerm] -> PTerm
mkPApp FC
nfc (FC -> [FC] -> Name -> PTerm
PRef FC
nfc [] Name
tyn) ((Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (FC -> [FC] -> Name -> PTerm
PRef FC
nfc []) [Name]
args)
                      [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons' <- ((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
  [Name])
 -> IdrisParser
      (Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
       [Name]))
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
     [Name])]
-> IdrisParser
     [(Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
       [Name])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
x, FC
xfc, [PTerm]
cargs, FC
cfc, [Name]
fs) ->
                                   do let cty :: PTerm
cty = [PTerm] -> PTerm -> PTerm
bindArgs [PTerm]
cargs PTerm
conty
                                      (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
 [Name])
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
      [Name])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
x, FC
xfc, PTerm
cty, FC
cfc, [Name]
fs)) [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
  [Name])]
cons
                      Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
accData Accessibility
acc Name
tyn (((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])
 -> Name)
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons')
                      PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PDecl -> IdrisParser PDecl) -> PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$ Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' PTerm
-> PDecl
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [DataOpt]
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
nfc [DataOpt]
dataOpts (Name
-> FC
-> PTerm
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
     [Name])]
-> PData' PTerm
forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl Name
tyn FC
nfc PTerm
ty [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
  [Name])]
cons'))
                    StateT IState (WriterT FC (Parsec Void [Char])) ()
terminator
                    PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PDecl
d))
           IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"data type declaration"
  where
    mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
    mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp FC
fc PTerm
t [] = PTerm
t
    mkPApp FC
fc PTerm
t [PTerm]
xs = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
t ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
xs)
    bindArgs :: [PTerm] -> PTerm -> PTerm
    bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs [PTerm]
xs PTerm
t = (PTerm -> PTerm -> PTerm) -> PTerm -> [PTerm] -> PTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl (Int -> [Char] -> Name
sMN Int
0 [Char]
"_t") FC
NoFC) PTerm
t [PTerm]
xs


{- | 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 [Char]))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment
         (Name
cn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
         let cn :: Name
cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
         Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
         [Name]
fs <- [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"erase"
                               StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
P.sepBy1 StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
         (PTerm
ty, FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
         IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
         let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
             argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
                        | (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
         Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
cn
         (Docstring (Either Err PTerm),
 [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
 [Name])
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
      [Name])
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
argDocs', Name
cn, FC
nfc, PTerm
ty, FC
fc, [Name]
fs)
      IdrisParser
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
   [Name])
-> [Char]
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
      [Name])
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constructor"

{- | 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 [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
simpleConstructor SyntaxInfo
syn
     = (StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (FC
   -> (Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
       [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT
   IState
   (WriterT FC (Parsec Void [Char]))
   (FC
    -> (Docstring (Either Err PTerm),
        [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
        [Name]))
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      (Docstring (Either Err PTerm),
       [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
       [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (FC
      -> (Docstring (Either Err PTerm),
          [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
          [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
forall a b. (a -> b) -> a -> b
$ do
          (Docstring ()
doc, [(Name, Docstring ())]
_) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs (StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (), [(Name, Docstring ())])
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (), [(Name, Docstring ())])
docComment)
          IState
ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
          let doc' :: Docstring (Either Err PTerm)
doc' = ([Char] -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. ([Char] -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
          (Name
cn_in, FC
nfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          let cn :: Name
cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
          [PTerm]
args <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) [PTerm]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void [Char])) ()
notEndApp
                           SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
          Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkNameFixity Name
cn
          (FC
 -> (Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
     [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (FC
      -> (Docstring (Either Err PTerm),
          [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
          [Name]))
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC
  -> (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name]))
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      (FC
       -> (Docstring (Either Err PTerm),
           [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
           [Name])))
-> (FC
    -> (Docstring (Either Err PTerm),
        [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
        [Name]))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (FC
      -> (Docstring (Either Err PTerm),
          [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
          [Name]))
forall a b. (a -> b) -> a -> b
$ \FC
fc -> (Docstring (Either Err PTerm)
doc', [], Name
cn, FC
nfc, [PTerm]
args, FC
fc, []))
        StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
   [Name])
-> [Char]
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC,
      [Name])
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constructor"
{- | Parses a dsl block declaration
DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
 -}
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"dsl"
             Name
n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
             [([Char], PTerm)]
bs <- IdrisParser ([Char], PTerm) -> IdrisParser [([Char], PTerm)]
forall a.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> StateT IState (WriterT FC (Parsec Void [Char])) [a]
indentedBlock (SyntaxInfo -> IdrisParser ([Char], PTerm)
overload SyntaxInfo
syn)
             let dsl :: DSL
dsl = [([Char], PTerm)] -> DSL -> DSL
mkDSL [([Char], PTerm)]
bs (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn)
             DSL -> StateT IState (WriterT FC (Parsec Void [Char])) ()
checkDSL DSL
dsl
             IState
i <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
             IState -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { idris_dsls = addDef n dsl (idris_dsls i) })
             PDecl -> IdrisParser PDecl
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> DSL -> PDecl
forall t. Name -> DSL' t -> PDecl' t
PDSL Name
n DSL
dsl)
          IdrisParser PDecl -> [Char] -> IdrisParser PDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dsl block declaration"
    where mkDSL :: [(String, PTerm)] -> DSL -> DSL
          mkDSL :: [([Char], PTerm)] -> DSL -> DSL
mkDSL [([Char], PTerm)]
bs DSL
dsl = let var :: Maybe PTerm
var    = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"variable" [([Char], PTerm)]
bs
                             first :: Maybe PTerm
first  = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_first" [([Char], PTerm)]
bs
                             next :: Maybe PTerm
next   = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"index_next" [([Char], PTerm)]
bs
                             leto :: Maybe PTerm
leto   = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"let" [([Char], PTerm)]
bs
                             lambda :: Maybe PTerm
lambda = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"lambda" [([Char], PTerm)]
bs
                             pi :: Maybe PTerm
pi     = [Char] -> [([Char], PTerm)] -> Maybe PTerm
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
"pi" [([Char], PTerm)]
bs in
                             DSL
initDSL { dsl_var = var,
                                       index_first = first,
                                       index_next = next,
                                       dsl_lambda = lambda,
                                       dsl_let = leto,
                                       dsl_pi = pi }

{- | 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 [Char])) ()
checkDSL DSL
dsl = () -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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