{-|
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
                (doc, paramDocs, acc, 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
                      (doc, 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
                      ist <- get
                      let 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
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 ]
                      acc <- accessibility
                      opts <- dataOpts []
                      co <- recordI
                      return (doc', paramDocs', acc, opts ++ co))
                (tyn_in, nfc) <- withExtent fnName
                let tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                let rsyn = SyntaxInfo
syn { syn_namespace = show (nsroot tyn) :
                                                    syn_namespace syn }
                params <- P.manyTill (recordParameter rsyn) (keyword "where")
                (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn
                let 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 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 ()
                return $ \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
        ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get

        (constructorName, constructorDoc) <- P.option (Nothing, emptyDocstring)
                                             (do (doc, _) <- P.option noDocs docComment
                                                 n <- withExtent constructor
                                                 return (Just n, doc))

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

        fields <- many . indented $ fieldLine syn

        return (concat fields, constructorName, 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
            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
            c <- optional $ lchar '{'
            let oneName = (do (n, 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
                              return $ Just (expandNS syn n, 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)
            ns <- commaSeparated oneName
            lchar ':'
            -- Implicits are scoped in fields (fields aren't top level)
            t <- typeExpr (scopedImp syn)
            p <- endPlicity c
            ist <- get
            let 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
            return $ map (\Maybe (Name, FC)
n -> (Maybe (Name, FC)
n, Plicity
p, PTerm
t, Maybe (Docstring (Either Err PTerm))
doc')) 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
'('
      (n, nfc, 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)
      lchar ')'
      return (n, nfc, expl, 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 (n, nfc, pt) <- SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn
      return (n, nfc, expl, pt))
  where
    namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
    namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
namedTy SyntaxInfo
syn =
      do (n, 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
         lchar ':'
         ty <- typeExpr (allowImp syn)
         return (expandNS syn n, nfc, ty)
    onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
    onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
onlyName SyntaxInfo
syn =
      do (n, 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
         return (expandNS syn n, nfc, PType 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 (doc, argDocs, acc, 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
                    (doc, 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
                    pushIndent
                    acc <- accessibility
                    errRev <- dataOpts []
                    co <- dataI
                    ist <- get
                    let dataOpts = [DataOpt]
errRev [DataOpt] -> [DataOpt] -> [DataOpt]
forall a. [a] -> [a] -> [a]
++ [DataOpt]
co
                        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
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 ]
                    return (doc', argDocs', acc, dataOpts))
               (tyn_in, nfc) <- withExtent fnName
               (do P.try (lchar ':')
                   ty <- typeExpr (allowImp syn)
                   let tyn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                   d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
                     keyword "where"
                     cons <- indentedBlock (constructor syn)
                     accData acc tyn (map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) cons)
                     return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons))
                   terminator
                   return d) <|> (do
                    args <- many (do notEndApp
                                     x <- name
                                     return x)
                    let 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 = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
tyn_in
                    d <- P.option (PData doc argDocs syn nfc dataOpts (PLaterdecl tyn nfc ty)) (do
                      P.try (lchar '=') <|> do keyword "where"
                                               let 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  = Name -> [Char]
forall a. Show a => a -> [Char]
show Name
tyn_in [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
                                               let s  = [Char]
kw [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n
                                               let 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]] -> [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]] -> [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]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
as [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = ..."
                                               let 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]
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  ..."
                                               fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
                      cons <- P.sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")
                      let 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)
                      cons' <- 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)) cons
                      accData acc tyn (map (\ (Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
_, PTerm
_, FC
_, [Name]
_) -> Name
n) cons')
                      return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons'))
                    terminator
                    return 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 (doc, 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
         (cn_in, nfc) <- withExtent fnName
         let cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
         lchar ':'
         fs <- P.option [] (do lchar '%'; reserved "erase"
                               P.sepBy1 name (lchar ','))
         (ty, fc) <- withExtent $ typeExpr (allowImp syn)
         ist <- get
         let 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
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 ]
         checkNameFixity cn
         return (doc', argDocs', cn, nfc, ty, fc, 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
          (doc, _) <- (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)
          ist <- get
          let 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
          (cn_in, nfc) <- withExtent fnName
          let cn = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
cn_in
          args <- many (do notEndApp
                           simpleExpr syn)
          checkNameFixity cn
          return $ \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"
             n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
             bs <- indentedBlock (overload syn)
             let dsl = [([Char], PTerm)] -> DSL -> DSL
mkDSL [([Char], PTerm)]
bs (SyntaxInfo -> DSL
dsl_info SyntaxInfo
syn)
             checkDSL dsl
             i <- get
             put (i { idris_dsls = addDef n dsl (idris_dsls i) })
             return (PDSL n 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 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 o `notElem` overloadable
                     then fail $ show o ++ " is not an overloading"
                     else do
                       lchar '='
                       t <- expr syn
                       return (o, 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"]