{-|
Module      : Idris.Parser.Expr
Description : Parse Expressions.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts, TupleSections #-}
module Idris.Parser.Expr where

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.DSL
import Idris.Options
import Idris.Parser.Helpers
import Idris.Parser.Ops

import Prelude hiding (pi)

import Control.Applicative
import Control.Arrow (left)
import Control.Monad
import qualified Control.Monad.Combinators.Expr as P
import Control.Monad.State.Strict
import Data.Function (on)
import Data.List
import Data.Maybe
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P

-- | Allow implicit type declarations
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed = True,
                     constraintAllowed = False }

-- | Disallow implicit type declarations
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp = SyntaxInfo -> SyntaxInfo
scopedImp

-- | Implicits hare are scoped rather than top level
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed = False,
                      constraintAllowed = False }

-- | Allow scoped constraint arguments
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn = SyntaxInfo
syn { constraintAllowed = True }

{-| Parses an expression as a whole
@
  FullExpr ::= Expr EOF_t;
@
 -}
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr SyntaxInfo
syn = do x <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                  P.eof
                  i <- get
                  return $ debindApp syn (desugar syn i x)

tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr :: SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
st = (ParseError -> Err) -> Either ParseError PTerm -> Either Err PTerm
forall b c d. (b -> c) -> Either b d -> Either c d
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left ([Char] -> Err
forall t. [Char] -> Err' t
Msg ([Char] -> Err) -> (ParseError -> [Char]) -> ParseError -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> (ParseError -> Doc) -> ParseError -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> Doc
parseErrorDoc) (Either ParseError PTerm -> Either Err PTerm)
-> ([Char] -> Either ParseError PTerm)
-> [Char]
-> Either Err PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IdrisParser PTerm
-> IState -> [Char] -> [Char] -> Either ParseError PTerm
forall st res.
Parser st res -> st -> [Char] -> [Char] -> Either ParseError res
runparser (SyntaxInfo -> IdrisParser PTerm
fullExpr SyntaxInfo
syn) IState
st [Char]
""

{- | Parses an expression
@
  Expr ::= Pi
@
 -}
expr :: SyntaxInfo -> IdrisParser PTerm
expr :: SyntaxInfo -> IdrisParser PTerm
expr = SyntaxInfo -> IdrisParser PTerm
pi

{- | Parses an expression with possible operator applied
@
  OpExpr ::= {- Expression Parser with Operators based on Expr' -};
@
-}
opExpr :: SyntaxInfo -> IdrisParser PTerm
opExpr :: SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn = do i <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
                P.makeExprParser (expr' syn) (table (idris_infixes i))

{- | Parses either an internally defined expression or
    a user-defined one
@
Expr' ::=  "External (User-defined) Syntax"
      |   InternalExpr;
@
 -}
expr' :: SyntaxInfo -> IdrisParser PTerm
expr' :: SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn = IdrisParser PTerm -> IdrisParser PTerm
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 (SyntaxInfo -> IdrisParser PTerm
externalExpr SyntaxInfo
syn)
            IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
internalExpr SyntaxInfo
syn
            IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression"

{- | Parses a user-defined expression -}
externalExpr :: SyntaxInfo -> IdrisParser PTerm
externalExpr :: SyntaxInfo -> IdrisParser PTerm
externalExpr SyntaxInfo
syn = do i <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      (expr, outerFC@(FC fn _ _)) <- withExtent $ extensions syn (syntaxRulesList $ syntax_rules i)
                      return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)
                   IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"user-defined expression"
  where -- Fix non-highlighting FCs by approximating with the span of the syntax application
        fixFC :: FC -> FC -> FC
fixFC FC
outer FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                          | Bool
otherwise          = FC
outer
        -- Fix highlighting FCs by making them useless, to avoid spurious highlights
        fixFCH :: [Char] -> FC -> FC -> FC
fixFCH [Char]
fn FC
outer FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                              | Bool
otherwise          = [Char] -> FC
FileFC [Char]
fn

{- | Parses a simple user-defined expression -}
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn = do i <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
                            extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
  where
    isSimple :: Syntax -> Bool
isSimple (Rule (Expr Name
x:[SSymbol]
xs) PTerm
_ SynContext
_) = Bool
False
    isSimple (Rule (SimpleExpr Name
x:[SSymbol]
xs) PTerm
_ SynContext
_) = Bool
False
    isSimple (Rule [Keyword Name
_] PTerm
_ SynContext
_) = Bool
True
    isSimple (Rule [Symbol [Char]
_]  PTerm
_ SynContext
_) = Bool
True
    isSimple (Rule (SSymbol
_:[SSymbol]
xs) PTerm
_ SynContext
_) = case [SSymbol] -> SSymbol
forall a. HasCallStack => [a] -> a
last [SSymbol]
xs of
        Keyword Name
_ -> Bool
True
        Symbol [Char]
_  -> Bool
True
        SSymbol
_ -> Bool
False
    isSimple Syntax
_ = Bool
False

{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions SyntaxInfo
syn [Syntax]
rules = SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension SyntaxInfo
syn [] ((Syntax -> Bool) -> [Syntax] -> [Syntax]
forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isValid [Syntax]
rules)
                       IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"user-defined expression"
  where
    isValid :: Syntax -> Bool
    isValid :: Syntax -> Bool
isValid (Rule [SSymbol]
_ PTerm
_ SynContext
AnySyntax) = Bool
True
    isValid (Rule [SSymbol]
_ PTerm
_ SynContext
PatternSyntax) = SyntaxInfo -> Bool
inPattern SyntaxInfo
syn
    isValid (Rule [SSymbol]
_ PTerm
_ SynContext
TermSyntax) = Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
    isValid (DeclRule [SSymbol]
_ [PDecl]
_) = Bool
False

data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
  deriving Int -> SynMatch -> ShowS
[SynMatch] -> ShowS
SynMatch -> [Char]
(Int -> SynMatch -> ShowS)
-> (SynMatch -> [Char]) -> ([SynMatch] -> ShowS) -> Show SynMatch
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SynMatch -> ShowS
showsPrec :: Int -> SynMatch -> ShowS
$cshow :: SynMatch -> [Char]
show :: SynMatch -> [Char]
$cshowList :: [SynMatch] -> ShowS
showList :: [SynMatch] -> ShowS
Show

extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension :: SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension SyntaxInfo
syn [Maybe (Name, SynMatch)]
ns [Syntax]
rules =
  [IdrisParser PTerm] -> IdrisParser PTerm
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice ([IdrisParser PTerm] -> IdrisParser PTerm)
-> [IdrisParser PTerm] -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ (([Syntax] -> IdrisParser PTerm)
 -> [[Syntax]] -> [IdrisParser PTerm])
-> [[Syntax]]
-> ([Syntax] -> IdrisParser PTerm)
-> [IdrisParser PTerm]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Syntax] -> IdrisParser PTerm)
-> [[Syntax]] -> [IdrisParser PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((Syntax -> Syntax -> Bool) -> [Syntax] -> [[Syntax]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ([SSymbol] -> [SSymbol] -> Bool
forall {a}. Eq a => [a] -> [a] -> Bool
ruleGroup ([SSymbol] -> [SSymbol] -> Bool)
-> (Syntax -> [SSymbol]) -> Syntax -> Syntax -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Syntax -> [SSymbol]
syntaxSymbols) [Syntax]
rules) (([Syntax] -> IdrisParser PTerm) -> [IdrisParser PTerm])
-> ([Syntax] -> IdrisParser PTerm) -> [IdrisParser PTerm]
forall a b. (a -> b) -> a -> b
$ \[Syntax]
rs ->
    case [Syntax] -> Syntax
forall a. HasCallStack => [a] -> a
head [Syntax]
rs of -- can never be []
      Rule (SSymbol
symb:[SSymbol]
_) PTerm
_ SynContext
_ -> IdrisParser PTerm -> IdrisParser PTerm
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 (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
        n <- SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol SSymbol
symb
        extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]
      -- If we have more than one Rule in this bucket, our grammar is
      -- nondeterministic.
      Rule [] PTerm
ptm SynContext
_ -> PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
flatten ([(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch ((Maybe (Name, SynMatch) -> Maybe (Name, SynMatch))
-> [Maybe (Name, SynMatch)] -> [(Name, SynMatch)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe (Name, SynMatch) -> Maybe (Name, SynMatch)
forall a. a -> a
id [Maybe (Name, SynMatch)]
ns) PTerm
ptm))
  where
    ruleGroup :: [a] -> [a] -> Bool
ruleGroup [] [] = Bool
True
    ruleGroup (a
s1:[a]
_) (a
s2:[a]
_) = a
s1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
s2
    ruleGroup [a]
_ [a]
_ = Bool
False

    extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
    extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol (Keyword Name
n)    = Maybe (Name, SynMatch)
forall a. Maybe a
Nothing Maybe (Name, SynMatch)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser (Maybe (Name, SynMatch))
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, MonadState IState m) =>
[Char] -> m ()
keyword (Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n)
    extensionSymbol (Expr Name
n)       = do tm <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                        return $ Just (n, SynTm tm)
    extensionSymbol (SimpleExpr Name
n) = do tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                        return $ Just (n, SynTm tm)
    extensionSymbol (Binding Name
n)    = do (b, fc) <- 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
name
                                        return $ Just (n, SynBind fc b)
    extensionSymbol (Symbol [Char]
s)     = Maybe (Name, SynMatch)
forall a. Maybe a
Nothing Maybe (Name, SynMatch)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser (Maybe (Name, SynMatch))
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
<$ OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
s)

    flatten :: PTerm -> PTerm -- flatten application
    flatten :: PTerm -> PTerm
flatten (PApp FC
fc (PApp FC
_ PTerm
f [PArg]
as) [PArg]
bs) = PTerm -> PTerm
flatten (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
as [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
bs))
    flatten PTerm
t = PTerm
t

updateSynMatch :: [(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch = [(Name, SynMatch)] -> PTerm -> PTerm
update
  where
    updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
    updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc) = case Name -> [(Name, SynMatch)] -> Maybe SynMatch
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, SynMatch)]
ns of
                           Just (SynBind FC
tfc Name
t) -> (Name
t, FC
tfc)
                           Maybe SynMatch
_ -> (Name
n, FC
fc)

    update :: [(Name, SynMatch)] -> PTerm -> PTerm
    update :: [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns (PRef FC
fc [FC]
hls Name
n) = case Name -> [(Name, SynMatch)] -> Maybe SynMatch
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, SynMatch)]
ns of
                                  Just (SynTm PTerm
t) -> PTerm
t
                                  Maybe SynMatch
_ -> FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n
    update [(Name, SynMatch)]
ns (PPatvar FC
fc Name
n) = (Name -> FC -> PTerm) -> (Name, FC) -> PTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((FC -> Name -> PTerm) -> Name -> FC -> PTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PPatvar) ((Name, FC) -> PTerm) -> (Name, FC) -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
    update [(Name, SynMatch)]
ns (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
sc)
      = let (Name
n', FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
nfc)
        in FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n' FC
nfc' ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update [(Name, SynMatch)]
ns (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc)
      = let (Name
n', FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
        in Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([(Name, SynMatch)] -> Plicity -> Plicity
updTacImp [(Name, SynMatch)]
ns Plicity
p) Name
n' FC
nfc'
               ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update [(Name, SynMatch)]
ns (PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
val PTerm
sc)
      = let (Name
n', FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
nfc)
        in FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n' FC
nfc' ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty)
                ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
val) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update [(Name, SynMatch)]
ns (PApp FC
fc PTerm
t [PArg]
args)
      = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall a b. (a -> b) -> PArg' a -> PArg' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [PArg]
args)
    update [(Name, SynMatch)]
ns (PAppBind FC
fc PTerm
t [PArg]
args)
      = FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall a b. (a -> b) -> PArg' a -> PArg' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [PArg]
args)
    update [(Name, SynMatch)]
ns (PMatchApp FC
fc Name
n) = let (Name
n', FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
                                 in FC -> Name -> PTerm
PMatchApp FC
nfc' Name
n'
    update [(Name, SynMatch)]
ns (PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f)
      = FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
c) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
f)
    update [(Name, SynMatch)]
ns (PCase FC
fc PTerm
c [(PTerm, PTerm)]
opts)
      = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
c) (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> (PTerm, PTerm) -> (PTerm, PTerm)
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
pmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [(PTerm, PTerm)]
opts)
    update [(Name, SynMatch)]
ns (PRewrite FC
fc Maybe Name
by PTerm
eq PTerm
tm Maybe PTerm
mty)
      = FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
by ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
eq) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm) ((PTerm -> PTerm) -> Maybe PTerm -> Maybe PTerm
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) Maybe PTerm
mty)
    update [(Name, SynMatch)]
ns (PPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
p ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)
    update [(Name, SynMatch)]
ns (PDPair FC
fc [FC]
hls PunInfo
p PTerm
l PTerm
t PTerm
r)
      = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
p ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)
    update [(Name, SynMatch)]
ns (PAs FC
fc Name
n PTerm
t) = FC -> Name -> PTerm -> PTerm
PAs FC
fc ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    update [(Name, SynMatch)]
ns (PAlternative [(Name, Name)]
ms PAltType
a [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) [PTerm]
as)
    update [(Name, SynMatch)]
ns (PHidden PTerm
t) = PTerm -> PTerm
PHidden ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    update [(Name, SynMatch)]
ns (PGoal FC
fc PTerm
r Name
n PTerm
sc) = FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r) Name
n ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
sc)
    update [(Name, SynMatch)]
ns (PDoBlock [PDo]
ds) = [PDo] -> PTerm
PDoBlock ([PDo] -> PTerm) -> [PDo] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PDo -> PDo) -> [PDo] -> [PDo]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDo -> PDo
upd [(Name, SynMatch)]
ns) [PDo]
ds
      where upd :: [(Name, SynMatch)] -> PDo -> PDo
            upd :: [(Name, SynMatch)] -> PDo -> PDo
upd [(Name, SynMatch)]
ns (DoExp FC
fc PTerm
t) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd [(Name, SynMatch)]
ns (DoBind FC
fc Name
n FC
nfc PTerm
t) = FC -> Name -> FC -> PTerm -> PDo
forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
n FC
nfc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd [(Name, SynMatch)]
ns (DoLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
t) = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
fc RigCount
rc Name
n FC
nfc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd [(Name, SynMatch)]
ns (DoBindP FC
fc PTerm
i PTerm
t [(PTerm, PTerm)]
ts)
                    = FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
i) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
                                 (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(PTerm
l,PTerm
r) -> ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l, [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)) [(PTerm, PTerm)]
ts)
            upd [(Name, SynMatch)]
ns (DoLetP FC
fc PTerm
i PTerm
t [(PTerm, PTerm)]
ts)
                    = FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
i) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
                                (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(PTerm
l,PTerm
r) -> ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l, [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)) [(PTerm, PTerm)]
ts)
            upd [(Name, SynMatch)]
ns (DoRewrite FC
fc PTerm
h) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoRewrite FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
h)
    update [(Name, SynMatch)]
ns (PIdiom FC
fc PTerm
t) = FC -> PTerm -> PTerm
PIdiom FC
fc (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update [(Name, SynMatch)]
ns (PMetavar FC
fc Name
n) = (Name -> FC -> PTerm) -> (Name, FC) -> PTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((FC -> Name -> PTerm) -> Name -> FC -> PTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PMetavar) ((Name, FC) -> PTerm) -> (Name, FC) -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
    update [(Name, SynMatch)]
ns (PProof [PTactic]
tacs) = [PTactic] -> PTerm
PProof ([PTactic] -> PTerm) -> [PTactic] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTactic -> PTactic) -> [PTactic] -> [PTactic]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns) [PTactic]
tacs
    update [(Name, SynMatch)]
ns (PTactics [PTactic]
tacs) = [PTactic] -> PTerm
PTactics ([PTactic] -> PTerm) -> [PTactic] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTactic -> PTactic) -> [PTactic] -> [PTactic]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns) [PTactic]
tacs
    update [(Name, SynMatch)]
ns (PDisamb [[Text]]
nsps PTerm
t) = [[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
nsps (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update [(Name, SynMatch)]
ns (PUnifyLog PTerm
t) = PTerm -> PTerm
PUnifyLog (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update [(Name, SynMatch)]
ns (PNoImplicits PTerm
t) = PTerm -> PTerm
PNoImplicits (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update [(Name, SynMatch)]
ns (PQuasiquote PTerm
tm Maybe PTerm
mty) = PTerm -> Maybe PTerm -> PTerm
PQuasiquote ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm) ((PTerm -> PTerm) -> Maybe PTerm -> Maybe PTerm
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) Maybe PTerm
mty)
    update [(Name, SynMatch)]
ns (PUnquote PTerm
t) = PTerm -> PTerm
PUnquote (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update [(Name, SynMatch)]
ns (PQuoteName Name
n Bool
res FC
fc) = let (Name
n', FC
fc') = ([(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc))
                                      in Name -> Bool -> FC -> PTerm
PQuoteName Name
n' Bool
res FC
fc'
    update [(Name, SynMatch)]
ns (PRunElab FC
fc PTerm
t [[Char]]
nsp) = FC -> PTerm -> [[Char]] -> PTerm
PRunElab FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) [[Char]]
nsp
    update [(Name, SynMatch)]
ns (PConstSugar FC
fc PTerm
t) = FC -> PTerm -> PTerm
PConstSugar FC
fc (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    -- PConstSugar probably can't contain anything substitutable, but it's hard to track
    update [(Name, SynMatch)]
ns PTerm
t = PTerm
t

    updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
    -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
    updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns (Intro [Name]
ns') = [Name] -> PTactic
forall t. [Name] -> PTactic' t
Intro ([Name] -> PTactic) -> [Name] -> PTactic
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
ns'
    updTactic [(Name, SynMatch)]
ns (Focus Name
n) = Name -> PTactic
forall t. Name -> PTactic' t
Focus (Name -> PTactic) -> ((Name, FC) -> Name) -> (Name, FC) -> PTactic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> PTactic) -> (Name, FC) -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)
    updTactic [(Name, SynMatch)]
ns (Refine Name
n [Bool]
bs) = Name -> [Bool] -> PTactic
forall t. Name -> [Bool] -> PTactic' t
Refine ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) [Bool]
bs
    updTactic [(Name, SynMatch)]
ns (Claim Name
n PTerm
t) = Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
Claim ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    updTactic [(Name, SynMatch)]
ns (MatchRefine Name
n) = Name -> PTactic
forall t. Name -> PTactic' t
MatchRefine ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC))
    updTactic [(Name, SynMatch)]
ns (LetTac Name
n PTerm
t) = Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
LetTac ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    updTactic [(Name, SynMatch)]
ns (LetTacTy Name
n PTerm
ty PTerm
tm) = Name -> PTerm -> PTerm -> PTactic
forall t. Name -> t -> t -> PTactic' t
LetTacTy ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm)
    updTactic [(Name, SynMatch)]
ns (ProofSearch Bool
rec Bool
prover Int
depth Maybe Name
top [Name]
psns [Name]
hints) = Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
rec Bool
prover Int
depth
      ((Name -> Name) -> Maybe Name -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) Maybe Name
top) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
psns) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
hints)
    updTactic [(Name, SynMatch)]
ns (Try PTactic
l PTactic
r) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
Try ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
l) ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
r)
    updTactic [(Name, SynMatch)]
ns (TSeq PTactic
l PTactic
r) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
l) ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
r)
    updTactic [(Name, SynMatch)]
ns (GoalType [Char]
s PTactic
tac) = [Char] -> PTactic -> PTactic
forall t. [Char] -> PTactic' t -> PTactic' t
GoalType [Char]
s (PTactic -> PTactic) -> PTactic -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
tac
    updTactic [(Name, SynMatch)]
ns (TDocStr (Left Name
n)) = Either Name Const -> PTactic
forall t. Either Name Const -> PTactic' t
TDocStr (Either Name Const -> PTactic)
-> ((Name, FC) -> Either Name Const) -> (Name, FC) -> PTactic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Either Name Const
forall a b. a -> Either a b
Left (Name -> Either Name Const)
-> ((Name, FC) -> Name) -> (Name, FC) -> Either Name Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> PTactic) -> (Name, FC) -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)
    updTactic [(Name, SynMatch)]
ns PTactic
t = (PTerm -> PTerm) -> PTactic -> PTactic
forall a b. (a -> b) -> PTactic' a -> PTactic' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) PTactic
t

    updTacImp :: [(Name, SynMatch)] -> Plicity -> Plicity
updTacImp [(Name, SynMatch)]
ns (TacImp [ArgOpt]
o Static
st PTerm
scr RigCount
r) = [ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
o Static
st ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
scr) RigCount
r
    updTacImp [(Name, SynMatch)]
_  Plicity
x                   = Plicity
x

    dropn :: Name -> [(Name, a)] -> [(Name, a)]
    dropn :: forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [] = []
    dropn Name
n ((Name
x,a
t) : [(Name, a)]
xs) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = [(Name, a)]
xs
                         | Bool
otherwise = (Name
x,a
t)(Name, a) -> [(Name, a)] -> [(Name, a)]
forall a. a -> [a] -> [a]
:Name -> [(Name, a)] -> [(Name, a)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, a)]
xs


{- | Parses a (normal) built-in expression
@
InternalExpr ::=
    UnifyLog
  | RecordType
  | SimpleExpr
  | Lambda
  | QuoteGoal
  | Let
  | If
  | RewriteTerm
  | CaseExpr
  | DoBlock
  | App
  ;
@
-}
internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr SyntaxInfo
syn =
         SyntaxInfo -> IdrisParser PTerm
unifyLog SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
runElab SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
disamb SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
noImplicits SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
recordType SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
if_ SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
lambda SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
quoteGoal SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
let_ SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
rewriteTerm SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
doBlock SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
caseExpr SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
app SyntaxInfo
syn
     IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression"

{- | Parses the "impossible" keyword
@
Impossible ::= 'impossible'
@
-}
impossible :: IdrisParser PTerm
impossible :: IdrisParser PTerm
impossible = PTerm
PImpossible PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser PTerm
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, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"impossible"

{- | Parses a case expression
@
CaseExpr ::=
  'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
@
-}
caseExpr :: SyntaxInfo -> IdrisParser PTerm
caseExpr :: SyntaxInfo -> IdrisParser PTerm
caseExpr SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"case"
                  (scr, 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
expr SyntaxInfo
syn
                  keyword "of"
                  opts <- indentedBlock1 (caseOption syn)
                  return (PCase fc scr opts)
               IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"case expression"

{- | Parses a case in a case expression
@
CaseOption ::=
  Expr (Impossible | '=>' Expr) Terminator
  ;
@
-}
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption SyntaxInfo
syn = do lhs <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern = True }))
                    r <- impossible <|> symbol "=>" *> expr syn
                    return (lhs, r)
                 IdrisParser (PTerm, PTerm) -> [Char] -> IdrisParser (PTerm, PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"case option"

warnTacticDeprecation :: FC -> IdrisParser ()
warnTacticDeprecation :: FC -> StateT IState (WriterT FC (Parsec Void [Char])) ()
warnTacticDeprecation FC
fc =
 FC
-> Maybe Opt
-> Err
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
parserWarning FC
fc (Opt -> Maybe Opt
forall a. a -> Maybe a
Just Opt
NoOldTacticDeprecationWarnings) ([Char] -> Err
forall t. [Char] -> Err' t
Msg [Char]
"This style of tactic proof is deprecated. See %runElab for the replacement.")

{- | Parses a proof block
@
ProofExpr ::=
  'proof' OpenBlock Tactic'* CloseBlock
  ;
@
-}
proofExpr :: SyntaxInfo -> IdrisParser PTerm
proofExpr :: SyntaxInfo -> IdrisParser PTerm
proofExpr SyntaxInfo
syn = do kw <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"proof"
                   ts <- indentedBlock1 (tactic syn)
                   warnTacticDeprecation kw
                   return $ PProof ts
                IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"proof block"

{- | Parses a tactics block
@
TacticsExpr :=
  'tactics' OpenBlock Tactic'* CloseBlock
;
@
-}
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
tacticsExpr SyntaxInfo
syn = do kw <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"tactics"
                     ts <- indentedBlock1 (tactic syn)
                     warnTacticDeprecation kw
                     return $ PTactics ts
                  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"tactics block"

{- | Parses a simple expression
@
SimpleExpr ::=
    {- External (User-defined) Simple Expression -}
  | '?' Name
  | % 'implementation'
  | 'Refl' ('{' Expr '}')?
  | ProofExpr
  | TacticsExpr
  | FnName
  | Idiom
  | List
  | Alt
  | Bracketed
  | Constant
  | Type
  | 'Void'
  | Quasiquote
  | NameQuote
  | Unquote
  | '_'
  ;
@
-}
simpleExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn =
            IdrisParser PTerm -> IdrisParser PTerm
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 (SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 (x, FC f (l, c) end) <- StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
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])) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) (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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> 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
name)
               return (PMetavar (FC f (l, c-1) end) x)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"implementation"; return (PResolveTC fc)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"instance"
               parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."
               return (PResolveTC fc)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
proofExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
tacticsExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm -> IdrisParser PTerm
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 fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"Type*"); return $ PUniverse fc AllTypes)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"AnyType"; return $ PUniverse fc AllTypes
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> FC -> PTerm
PType (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
-> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"Type")
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"UniqueType"; return $ PUniverse fc UniqueType
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 fc <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"NullType"; return $ PUniverse fc NullType
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 (c, cfc) <- StateT IState (WriterT FC (Parsec Void [Char])) Const
-> StateT IState (WriterT FC (Parsec Void [Char])) (Const, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Const
forall (m :: * -> *). Parsing m => m Const
constant
               return (modifyConst syn cfc (PConstant cfc c))
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"'"; (str, fc) <- 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
name
               return (PApp fc (PRef fc [] (sUN "Symbol_"))
                          [pexp (PConstant NoFC (Str (show str)))])
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 (x, fc) <- 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
               if inPattern syn
                  then P.option (PRef fc [fc] x)
                                (do reservedOp "@"
                                    (s, fcIn) <- withExtent $ simpleExpr syn
                                    return (PAs fcIn x s))
                  else return (PRef fc [fc] x)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
idiom SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
listExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
alt SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"!"
               (s, 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
simpleExpr SyntaxInfo
syn
               return (PAppBind fc s [])
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
bracketed (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
quasiquote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
namequote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
unquote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'_'; PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
Placeholder
        IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression"

{- |Parses an expression in parentheses
@
Bracketed ::= '(' Bracketed'
@
 -}
bracketed :: SyntaxInfo -> IdrisParser PTerm
bracketed :: SyntaxInfo -> IdrisParser PTerm
bracketed SyntaxInfo
syn = do (FC fn (sl, sc) _) <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (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])) FC
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"parenthesized expression"
                   bracketed' (FC fn (sl, sc) (sl, sc+1)) (syn { withAppAllowed = True })

{- |Parses the rest of an expression in braces
@
Bracketed' ::=
  ')'
  | Expr ')'
  | ExprList ')'
  | DependentPair ')'
  | Operator Expr ')'
  | Expr Operator ')'
  ;
@
-}
bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' FC
open SyntaxInfo
syn =
            do fc <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (FC -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). MonadWriter FC m => FC -> m ()
addExtent FC
open StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')')
               return $ PTrue fc TypeOrTerm
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm -> IdrisParser PTerm
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 (PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
TypeOrTerm [] FC
open SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm -> IdrisParser PTerm
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 (opName, fc) <- 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
operatorName
                      guardNotPrefix opName

                      e <- expr syn
                      lchar ')'
                      return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
                        (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),
                                                      pexp e]))
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm -> IdrisParser PTerm
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 (SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn IdrisParser PTerm
-> (PTerm -> IdrisParser PTerm) -> IdrisParser PTerm
forall a b.
StateT IState (WriterT FC (Parsec Void [Char])) a
-> (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 -> (a -> m b) -> m b
>>= \PTerm
l ->
                     IdrisParser PTerm -> IdrisParser PTerm
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 (opName, fc) <- 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
operatorName
                               lchar ')'
                               return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
                                 (PApp fc (PRef fc [] opName) [pexp l,
                                                               pexp (PRef fc [] (sMN 1000 "ARG"))]))
                 IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr SyntaxInfo
syn FC
open PTerm
l)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 l <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
               bracketedExpr (allowConstr syn) open l
  where
    justPrefix                          :: FixDecl -> Maybe Name
    justPrefix :: FixDecl -> Maybe Name
justPrefix (Fix (PrefixN Int
_) [Char]
opName) = Name -> Maybe Name
forall a. a -> Maybe a
Just ([Char] -> Name
sUN [Char]
opName)
    justPrefix FixDecl
_                        = Maybe Name
forall a. Maybe a
Nothing

    guardNotPrefix        :: Name -> IdrisParser ()
    guardNotPrefix :: Name -> StateT IState (WriterT FC (Parsec Void [Char])) ()
guardNotPrefix Name
opName = do
      Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ Name
opName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char] -> Name
sUN [Char]
"-"
      Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ Name
opName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char] -> Name
sUN [Char]
"!"

      ops <- IState -> [FixDecl]
idris_infixes (IState -> [FixDecl])
-> StateT IState (WriterT FC (Parsec Void [Char])) IState
-> StateT IState (WriterT FC (Parsec Void [Char])) [FixDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
      guard . not . (opName `elem`) . mapMaybe justPrefix $ ops

{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
dependentPair :: PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
pun [(PTerm, Maybe (FC, PTerm), FC)]
prev FC
openFC SyntaxInfo
syn =
  if [(PTerm, Maybe (FC, PTerm), FC)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PTerm, Maybe (FC, PTerm), FC)]
prev then
      IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm
namePart
  else
    case PunInfo
pun of
      PunInfo
IsType -> IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm
namePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> Bool -> IdrisParser PTerm
exprPart Bool
True
      PunInfo
IsTerm -> Bool -> IdrisParser PTerm
exprPart Bool
False
      PunInfo
TypeOrTerm -> IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> IdrisParser PTerm
namePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> Bool -> IdrisParser PTerm
exprPart Bool
False
  where nametypePart :: IdrisParser PTerm
nametypePart = do
          (ln, lnfc, colonFC) <- StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC, FC)
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])) (Name, FC, FC)
 -> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC, FC))
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC, FC)
forall a b. (a -> b) -> a -> b
$ do
            (ln, lnfc) <- 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
name
            colonFC <- extent (lchar ':')
            return (ln, lnfc, colonFC)
          lty <- expr' syn
          starsFC <- extent $ reservedOp "**"
          dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
        namePart :: IdrisParser PTerm
namePart = IdrisParser PTerm -> IdrisParser PTerm
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 (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
          (ln, lnfc) <- 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
name
          starsFC <- extent $ reservedOp "**"
          dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
        exprPart :: Bool -> IdrisParser PTerm
exprPart Bool
isEnd = do
          e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          sepFCE <-
            let stars = (FC -> Either FC b
forall a b. a -> Either a b
Left (FC -> Either FC b)
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
-> StateT IState (WriterT FC (Parsec Void [Char])) (Either FC b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"))
                ending = (FC -> Either a FC
forall a b. b -> Either a b
Right (FC -> Either a FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
-> StateT IState (WriterT FC (Parsec Void [Char])) (Either a FC)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'))
            in if isEnd then ending else stars <|> ending
          case sepFCE of
            Left FC
starsFC -> PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsTerm ((PTerm
e, Maybe (FC, PTerm)
forall a. Maybe a
Nothing, FC
starsFC)(PTerm, Maybe (FC, PTerm), FC)
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
            Right FC
closeFC ->
              PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PunInfo
-> FC -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
mkPDPairs PunInfo
pun FC
openFC FC
closeFC ([(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. [a] -> [a]
reverse [(PTerm, Maybe (FC, PTerm), FC)]
prev) PTerm
e)
        mkPDPairs :: PunInfo
-> FC -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
mkPDPairs PunInfo
pun FC
openFC FC
closeFC ((PTerm
e, Maybe (FC, PTerm)
cfclty, FC
starsFC):[(PTerm, Maybe (FC, PTerm), FC)]
bnds) PTerm
r =
              (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
openFC ([FC
openFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC] -> ((FC, PTerm) -> [FC]) -> Maybe (FC, PTerm) -> [FC]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FC -> [FC] -> [FC]
forall a. a -> [a] -> [a]
: []) (FC -> [FC]) -> ((FC, PTerm) -> FC) -> (FC, PTerm) -> [FC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FC, PTerm) -> FC
forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC
starsFC, FC
closeFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ ((PTerm, Maybe (FC, PTerm), FC) -> [FC])
-> [(PTerm, Maybe (FC, PTerm), FC)] -> [FC]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<) (\(PTerm
_,Maybe (FC, PTerm)
cfclty,FC
sfc) -> [FC] -> ((FC, PTerm) -> [FC]) -> Maybe (FC, PTerm) -> [FC]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FC -> [FC] -> [FC]
forall a. a -> [a] -> [a]
: []) (FC -> [FC]) -> ((FC, PTerm) -> FC) -> (FC, PTerm) -> [FC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FC, PTerm) -> FC
forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC
sfc]) [(PTerm, Maybe (FC, PTerm), FC)]
bnds)
                               PunInfo
pun PTerm
e (PTerm -> ((FC, PTerm) -> PTerm) -> Maybe (FC, PTerm) -> PTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder (FC, PTerm) -> PTerm
forall a b. (a, b) -> b
snd Maybe (FC, PTerm)
cfclty) (PunInfo -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
forall {a}.
PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs PunInfo
pun FC
starsFC [(PTerm, Maybe (FC, PTerm), FC)]
bnds PTerm
r))
        mergePDPairs :: PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs PunInfo
pun FC
starsFC' [] PTerm
r = PTerm
r
        mergePDPairs PunInfo
pun FC
starsFC' ((PTerm
e, Maybe (a, PTerm)
cfclty, FC
starsFC):[(PTerm, Maybe (a, PTerm), FC)]
bnds) PTerm
r =
           FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
starsFC' [] PunInfo
pun PTerm
e (PTerm -> ((a, PTerm) -> PTerm) -> Maybe (a, PTerm) -> PTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder (a, PTerm) -> PTerm
forall a b. (a, b) -> b
snd Maybe (a, PTerm)
cfclty) (PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs PunInfo
pun FC
starsFC [(PTerm, Maybe (a, PTerm), FC)]
bnds PTerm
r)

-- | Parse the contents of parentheses, after an expression has been parsed.
bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr SyntaxInfo
syn FC
openParenFC PTerm
e =
             do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'; PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
e
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 exprs <- StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) [(PTerm, FC)]
forall a. IdrisParser a -> IdrisParser [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (do comma <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                  r <- expr syn
                                  return (r, comma))
                closeParenFC <- extent (lchar ')')
                let hilite = [FC
openParenFC, FC
closeParenFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ ((PTerm, FC) -> FC) -> [(PTerm, FC)] -> [FC]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, FC) -> FC
forall a b. (a, b) -> b
snd [(PTerm, FC)]
exprs
                return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 starsFC <- StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"
                dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
        IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"end of bracketed expression"
  where mergePairs :: [(PTerm, FC)] -> PTerm
        mergePairs :: [(PTerm, FC)] -> PTerm
mergePairs [(PTerm
t, FC
fc)]    = PTerm
t
        mergePairs ((PTerm
t, FC
fc):[(PTerm, FC)]
rs) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [] PunInfo
TypeOrTerm PTerm
t ([(PTerm, FC)] -> PTerm
mergePairs [(PTerm, FC)]
rs)

-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
-- big integer, otherwise try fromInteger and the constants as alternatives.
-- a better solution would be to fix fromInteger to work with Integer, as the
-- name suggests, rather than Int
{-| Finds optimal type for integer constant -}
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst SyntaxInfo
syn FC
fc (PConstant FC
inFC (BI Integer
x))
    | Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
        = FC -> PTerm -> PTerm
PConstSugar FC
inFC (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ -- wrap in original span for highlighting
            [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess
              (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"fromInteger")) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC (Integer -> Const
BI (Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
x)))]
              PTerm -> [PTerm] -> [PTerm]
forall a. a -> [a] -> [a]
: [PTerm]
consts)
    | Bool
otherwise = FC -> PTerm -> PTerm
PConstSugar FC
inFC (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                    [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess [PTerm]
consts
    where
      consts :: [PTerm]
consts = [ FC -> Const -> PTerm
PConstant FC
inFC (Integer -> Const
BI Integer
x)
               , FC -> Const -> PTerm
PConstant FC
inFC (Int -> Const
I (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word8 -> Const
B8 (Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word16 -> Const
B16 (Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word32 -> Const
B32 (Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word64 -> Const
B64 (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
x))
               ]
modifyConst SyntaxInfo
syn FC
fc PTerm
x = PTerm
x

{- | Parses an alternative expression
@
  Alt ::= '(|' Expr_List '|)';

  Expr_List ::=
    Expr'
    | Expr' ',' Expr_List
  ;
@
-}
alt :: SyntaxInfo -> IdrisParser PTerm
alt :: SyntaxInfo -> IdrisParser PTerm
alt SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"(|"; alts <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [PTerm]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { withAppAllowed = False })) (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','); symbol "|)"
             return (PAlternative [] FirstSuccess alts)

{- | Parses a possibly hidden simple expression
@
HSimpleExpr ::=
  '.' SimpleExpr
  | SimpleExpr
  ;
@
-}
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr SyntaxInfo
syn =
  do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'.'
     e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
     return $ PHidden e
  IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 PTerm
simpleExpr SyntaxInfo
syn
  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression"

{- | Parses a unification log expression
UnifyLog ::=
  '%' 'unifyLog' SimpleExpr
  ;
-}
unifyLog :: SyntaxInfo -> IdrisParser PTerm
unifyLog :: SyntaxInfo -> IdrisParser PTerm
unifyLog SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [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 (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [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
'%' StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"unifyLog"
                  PTerm -> PTerm
PUnifyLog (PTerm -> PTerm) -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
               IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"unification log expression"

{- | Parses a new-style tactics expression
RunTactics ::=
  '%' 'runElab' SimpleExpr
  ;
-}
runElab :: SyntaxInfo -> IdrisParser PTerm
runElab :: SyntaxInfo -> IdrisParser PTerm
runElab SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [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 (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [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
'%' StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"runElab"
                 (tm, 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
simpleExpr SyntaxInfo
syn
                 return $ PRunElab fc tm (syn_namespace syn)
              IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"new-style tactics expression"

{- | Parses a disambiguation expression
Disamb ::=
  'with' NameList Expr
  ;
-}
disamb :: SyntaxInfo -> IdrisParser PTerm
disamb :: SyntaxInfo -> IdrisParser PTerm
disamb SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"with"
                ns <- 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 sep. MonadPlus m => m a -> m sep -> 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
',')
                tm <- expr' syn
                return (PDisamb (map tons ns) tm)
               IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"namespace disambiguation expression"
  where tons :: Name -> [Text]
tons (NS Name
n [Text]
s) = [Char] -> Text
txt (Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
s
        tons Name
n = [[Char] -> Text
txt (Name -> [Char]
forall a. Show a => a -> [Char]
show Name
n)]
{- | Parses a no implicits expression
@
NoImplicits ::=
  '%' 'noImplicits' SimpleExpr
  ;
@
-}
noImplicits :: SyntaxInfo -> IdrisParser PTerm
noImplicits :: SyntaxInfo -> IdrisParser PTerm
noImplicits SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [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])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"noImplicits")
                     tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                     return (PNoImplicits tm)
                 IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"no implicits expression"

{- | Parses a function application expression
@
App ::=
  'mkForeign' Arg Arg*
  | MatchApp
  | SimpleExpr Arg*
  ;
MatchApp ::=
  SimpleExpr '<==' FnName
  ;
@
-}
app :: SyntaxInfo -> IdrisParser PTerm
app :: SyntaxInfo -> IdrisParser PTerm
app SyntaxInfo
syn = (StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
-> IdrisParser PTerm
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
 -> IdrisParser PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
-> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
    f <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
    (do P.try $ reservedOp "<=="
        ff <- fnName
        return (\FC
fc -> (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW (Int -> [Char] -> Name
sMN Int
0 [Char]
"match") FC
NoFC
                          PTerm
f
                          (FC -> Name -> PTerm
PMatchApp FC
fc Name
ff)
                          (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
0 [Char]
"match"))))
          <?> "matching application expression") <|>
      (do args <- many (do notEndApp; arg syn)
          wargs <- if withAppAllowed syn && not (inPattern syn)
                     then many (do notEndApp; reservedOp "|"; expr' syn)
                     else return []
          case args of
            [] -> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PTerm)
 -> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm))
-> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
forall a b. (a -> b) -> a -> b
$ \FC
fc -> PTerm
f
            [PArg]
_  -> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PTerm)
 -> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm))
-> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) (FC -> PTerm)
forall a b. (a -> b) -> a -> b
$ \FC
fc -> (FC -> PTerm -> [PTerm] -> PTerm
withApp FC
fc (FC -> PTerm -> [PArg] -> PTerm
flattenFromInt FC
fc PTerm
f [PArg]
args) [PTerm]
wargs)))
     IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"function application"
  where
    -- bit of a hack to deal with the situation where we're applying a
    -- literal to an argument, which we may want for obscure applications
    -- of fromInteger, and this will help disambiguate better.
    -- We know, at least, it won't be one of the constants!
    flattenFromInt :: FC -> PTerm -> [PArg] -> PTerm
flattenFromInt FC
fc (PAlternative [(Name, Name)]
_ PAltType
x [PTerm]
alts) [PArg]
args
      | Just PArg
i <- [PTerm] -> Maybe PArg
getFromInt [PTerm]
alts
           = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"fromInteger")) (PArg
i PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
args)
    flattenFromInt FC
fc PTerm
f [PArg]
args = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
args

    withApp :: FC -> PTerm -> [PTerm] -> PTerm
withApp FC
fc PTerm
tm [] = PTerm
tm
    withApp FC
fc PTerm
tm (PTerm
a : [PTerm]
as) = FC -> PTerm -> [PTerm] -> PTerm
withApp FC
fc (FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc PTerm
tm PTerm
a) [PTerm]
as

    getFromInt :: [PTerm] -> Maybe PArg
getFromInt ((PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg
a]) : [PTerm]
_) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Name
sUN [Char]
"fromInteger" = PArg -> Maybe PArg
forall a. a -> Maybe a
Just PArg
a
    getFromInt (PTerm
_ : [PTerm]
xs) = [PTerm] -> Maybe PArg
getFromInt [PTerm]
xs
    getFromInt [PTerm]
_ = Maybe PArg
forall a. Maybe a
Nothing

{-| Parses a function argument
@
Arg ::=
  ImplicitArg
  | ConstraintArg
  | SimpleExpr
  ;
@
-}
arg :: SyntaxInfo -> IdrisParser PArg
arg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
arg SyntaxInfo
syn =  SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
implicitArg SyntaxInfo
syn
       StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> StateT IState (WriterT FC (Parsec Void [Char])) PArg
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 -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
constraintArg SyntaxInfo
syn
       StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> StateT IState (WriterT FC (Parsec Void [Char])) PArg
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 e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
              return (pexp e)
       StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"function argument"

{-| Parses an implicit function argument
@
ImplicitArg ::=
  '{' Name ('=' Expr)? '}'
  ;
@
-}
implicitArg :: SyntaxInfo -> IdrisParser PArg
implicitArg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
implicitArg SyntaxInfo
syn = do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
                     (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
name
                     v <- P.option (PRef nfc [nfc] n) (do lchar '='
                                                          expr syn)
                     lchar '}'
                     return (pimp n v True)
                  StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"implicit function argument"

{-| Parses a constraint argument (for selecting a named interface implementation)

>    ConstraintArg ::=
>      '@{' Expr '}'
>      ;

-}
constraintArg :: SyntaxInfo -> IdrisParser PArg
constraintArg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
constraintArg SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"@{"
                       e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                       symbol "}"
                       return (pconst e)
                    StateT IState (WriterT FC (Parsec Void [Char])) PArg
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constraint argument"

{-| Parses a quasiquote expression (for building reflected terms using the elaborator)

> Quasiquote ::= '`(' Expr ')'

-}
quasiquote :: SyntaxInfo -> IdrisParser PTerm
quasiquote :: SyntaxInfo -> IdrisParser PTerm
quasiquote SyntaxInfo
syn = (OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                    OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`("
                    e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
                                    inPattern = False }
                    g <- optional $
                           do highlight AnnKeyword $ symbol ":"
                              expr syn { inPattern = False } -- don't allow antiquotes
                    highlight AnnKeyword $ symbol ")"
                    return $ PQuasiquote e g)
                  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"quasiquotation"
{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

> Unquote ::= ',' Expr

-}
unquote :: SyntaxInfo -> IdrisParser PTerm
unquote :: SyntaxInfo -> IdrisParser PTerm
unquote SyntaxInfo
syn = (OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnAntiquote (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                 Bool -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
                 OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"~"
                 e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
                 return $ PUnquote e)
               IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"unquotation"
{-| Parses a quotation of a name (for using the elaborator to resolve boring details)

> NameQuote ::= '`{' Name '}'

-}
namequote :: SyntaxInfo -> IdrisParser PTerm
namequote :: SyntaxInfo -> IdrisParser PTerm
namequote SyntaxInfo
syn = OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote ((IdrisParser PTerm -> IdrisParser PTerm
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 (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                     OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`{{"
                     (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
                     highlight AnnKeyword $ symbol "}}"
                     return (PQuoteName n False nfc))
                  IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`{"
                          (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
                          highlight AnnKeyword $ symbol "}"
                          return (PQuoteName n True nfc)))
                IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"quoted name"


{-| Parses a record field setter expression
@
RecordType ::=
  'record' '{' FieldTypeList '}';
@
@
FieldTypeList ::=
  FieldType
  | FieldType ',' FieldTypeList
  ;
@
@
FieldType ::=
  FnName '=' Expr
  ;
@
-}

data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm

recordType :: SyntaxInfo -> IdrisParser PTerm
recordType :: SyntaxInfo -> IdrisParser PTerm
recordType SyntaxInfo
syn =
      do ((fgs, rec), fc) <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     ((Either [([Name], SetOrUpdate)] [Name], Maybe PTerm), FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT
   IState
   (WriterT FC (Parsec Void [Char]))
   (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
 -> StateT
      IState
      (WriterT FC (Parsec Void [Char]))
      ((Either [([Name], SetOrUpdate)] [Name], Maybe PTerm), FC))
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     ((Either [([Name], SetOrUpdate)] [Name], Maybe PTerm), FC)
forall a b. (a -> b) -> a -> b
$ do
            [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"record"
            Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
            fgs <- IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet
            lchar '}'
            rec <- optional (do notEndApp; simpleExpr syn)
            return (fgs, rec)
         case fgs of
              Left [([Name], SetOrUpdate)]
fields ->
                case Maybe PTerm
rec of
                   Maybe PTerm
Nothing ->
                       PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> [Char] -> Name
sMN Int
0 [Char]
"fldx") FC
NoFC PTerm
Placeholder
                                   (FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
fields (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
0 [Char]
"fldx"))))
                   Just PTerm
v -> PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
fields PTerm
v)
              Right [Name]
fields ->
                case Maybe PTerm
rec of
                   Maybe PTerm
Nothing ->
                       PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> [Char] -> Name
sMN Int
0 [Char]
"fldx") FC
NoFC PTerm
Placeholder
                                 (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
fields)
                                     (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
0 [Char]
"fldx"))))
                   Just PTerm
v -> PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
fields) PTerm
v)

       IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"record setting expression"
   where fieldSet :: IdrisParser ([Name], SetOrUpdate)
         fieldSet :: IdrisParser ([Name], SetOrUpdate)
fieldSet = do ns <- StateT IState (WriterT FC (Parsec Void [Char])) [Name]
fieldGet
                       (do lchar '='
                           e <- expr syn
                           return (ns, FieldSet e))
                         <|> do symbol "$="
                                e <- expr syn
                                return (ns, FieldUpdate e)
                    IdrisParser ([Name], SetOrUpdate)
-> [Char] -> IdrisParser ([Name], SetOrUpdate)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"field setter"

         fieldGet :: IdrisParser [Name]
         fieldGet :: StateT IState (WriterT FC (Parsec Void [Char])) [Name]
fieldGet = StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) [Name]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 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])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"->")

         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet = IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
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 ([([Name], SetOrUpdate)] -> Either [([Name], SetOrUpdate)] [Name]
forall a b. a -> Either a b
Left ([([Name], SetOrUpdate)] -> Either [([Name], SetOrUpdate)] [Name])
-> StateT
     IState (WriterT FC (Parsec Void [Char])) [([Name], SetOrUpdate)]
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IdrisParser ([Name], SetOrUpdate)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT
     IState (WriterT FC (Parsec Void [Char])) [([Name], SetOrUpdate)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 IdrisParser ([Name], SetOrUpdate)
fieldSet (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
                     IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
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 f <- StateT IState (WriterT FC (Parsec Void [Char])) [Name]
fieldGet
                            return (Right f)

         applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
         applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [] PTerm
x = PTerm
x
         applyAll FC
fc (([Name]
ns, SetOrUpdate
e) : [([Name], SetOrUpdate)]
es) PTerm
x
            = FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
es (FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns SetOrUpdate
e PTerm
x)

         doUpdate :: FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns (FieldUpdate PTerm
e) PTerm
get
              = let get' :: PTerm
get' = FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
ns) PTerm
get in
                    FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns (PTerm -> SetOrUpdate
FieldSet (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
e [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
get'])) PTerm
get
         doUpdate FC
fc [Name
n] (FieldSet PTerm
e) PTerm
get
              = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> Name
mkType Name
n)) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
e, PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
get]
         doUpdate FC
fc (Name
n : [Name]
ns) SetOrUpdate
e PTerm
get
              = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> Name
mkType Name
n))
                  [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns SetOrUpdate
e (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
get])),
                   PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
get]

         getAll :: FC -> [Name] -> PTerm -> PTerm
         getAll :: FC -> [Name] -> PTerm -> PTerm
getAll FC
fc [Name
n] PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
e]
         getAll FC
fc (Name
n:[Name]
ns) PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc [Name]
ns PTerm
e)]


-- | Creates setters for record types on necessary functions
mkType :: Name -> Name
mkType :: Name -> Name
mkType (UN Text
n) = [Char] -> Name
sUN ([Char]
"set_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
str Text
n)
mkType (MN Int
0 Text
n) = Int -> [Char] -> Name
sMN Int
0 ([Char]
"set_" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
str Text
n)
mkType (NS Name
n [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
mkType Name
n) [Text]
s

{- | Parses a type signature
@
TypeSig ::=
  ':' Expr
  ;
@
@
TypeExpr ::= ConstraintList? Expr;
@
 -}
typeExpr :: SyntaxInfo -> IdrisParser PTerm
typeExpr :: SyntaxInfo -> IdrisParser PTerm
typeExpr SyntaxInfo
syn = do cs <- if SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn then SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn else [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                  sc <- expr (allowConstr syn)
                  return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount = r })) cs sc)
               IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"type signature"

{- | Parses a lambda expression
@
Lambda ::=
    '\\' TypeOptDeclList LambdaTail
  | '\\' SimpleExprList  LambdaTail
  ;
@
@
SimpleExprList ::=
  SimpleExpr
  | SimpleExpr ',' SimpleExprList
  ;
@
@
LambdaTail ::=
    Impossible
  | '=>' Expr
@
-}
lambda :: SyntaxInfo -> IdrisParser PTerm
lambda :: SyntaxInfo -> IdrisParser PTerm
lambda SyntaxInfo
syn = do 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
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"lambda expression"
                ((do xt <- IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 (IdrisParser [(RigCount, Name, FC, PTerm)]
 -> IdrisParser [(RigCount, Name, FC, PTerm)])
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                     (sc, fc) <- withExtent lambdaTail
                     return (bindList (\RigCount
r -> FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc) xt sc))
                 IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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 ps <- StateT IState (WriterT FC (Parsec Void [Char])) (FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [(FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (do (e, 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
simpleExpr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern = True }))
                                       return (fc, e))
                                   (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                     sc <- lambdaTail
                     return (pmList (zip [0..] ps) sc)))
                  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"lambda expression"
    where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
          pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList [] PTerm
sc = PTerm
sc
          pmList ((Int
i, (FC
fc, PTerm
x)) : [(Int, (FC, PTerm))]
xs) PTerm
sc
                = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> [Char] -> Name
sMN Int
i [Char]
"lamp") FC
NoFC PTerm
Placeholder
                        (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
i [Char]
"lamp"))
                                [(PTerm
x, [(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList [(Int, (FC, PTerm))]
xs PTerm
sc)])
          lambdaTail :: IdrisParser PTerm
          lambdaTail :: IdrisParser PTerm
lambdaTail = IdrisParser PTerm
impossible IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"=>" StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser PTerm -> IdrisParser PTerm
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn

{- | Parses a term rewrite expression
@
RewriteTerm ::=
  'rewrite' Expr ('==>' Expr)? 'in' Expr
  ;
@
-}
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
rewriteTerm SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"rewrite"
                     (prf, 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
expr SyntaxInfo
syn
                     giving <- optional (do symbol "==>"; expr' syn)
                     using <- optional (do reserved "using"
                                           n <- name
                                           return n)
                     keyword "in";  sc <- expr syn
                     return (PRewrite fc using prf sc giving)
                  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"term rewrite expression"

-- | Parse rig count for linear types
rigCount :: Parsing m => m RigCount
rigCount :: forall (m :: * -> *). Parsing m => m RigCount
rigCount = RigCount -> m RigCount -> m RigCount
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option RigCount
RigW (m RigCount -> m RigCount) -> m RigCount -> m RigCount
forall a b. (a -> b) -> a -> b
$ do Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'1'; RigCount -> m RigCount
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RigCount
Rig1
                       m RigCount -> m RigCount -> m RigCount
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'0'; RigCount -> m RigCount
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return RigCount
Rig0

{- |Parses a let binding
@
Let ::=
  'let' Name TypeSig'? '=' Expr  'in' Expr
| 'let' Expr'          '=' Expr' 'in' Expr

TypeSig' ::=
  ':' Expr'
  ;
@
 -}
let_ :: SyntaxInfo -> IdrisParser PTerm
let_ :: SyntaxInfo -> IdrisParser PTerm
let_ SyntaxInfo
syn = IdrisParser PTerm -> IdrisParser PTerm
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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                     ls <- IdrisParser (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
-> IdrisParser
     [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock (SyntaxInfo
-> IdrisParser
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding SyntaxInfo
syn)
                     keyword "in";  sc <- expr syn
                     return (buildLets ls sc))
           IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"let binding"
  where buildLets :: [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [] PTerm
sc = PTerm
sc
        buildLets ((FC
fc, RigCount
rc, PRef FC
nfc [FC]
_ Name
n, PTerm
ty, PTerm
v, []) : [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls) PTerm
sc
          = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v ([(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc)
        buildLets ((FC
fc, RigCount
_, PTerm
pat, PTerm
ty, PTerm
v, [(PTerm, PTerm)]
alts) : [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls) PTerm
sc
          = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
v ((PTerm
pat, [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)

let_binding :: SyntaxInfo
-> IdrisParser
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding SyntaxInfo
syn = do rc <- StateT IState (WriterT FC (Parsec Void [Char])) RigCount
forall (m :: * -> *). Parsing m => m RigCount
rigCount
                     (pat, fc) <- withExtent $ expr' (syn { inPattern = True })
                     ty <- P.option Placeholder (do lchar ':'; expr' syn)
                     lchar '='
                     v <- expr (syn { withAppAllowed = isVar pat })
                     ts <- P.option [] (do lchar '|'
                                           P.sepBy1 (do_alt syn) (lchar '|'))
                     return (fc,rc,pat,ty,v,ts)
   where isVar :: PTerm -> Bool
isVar (PRef FC
_ [FC]
_ Name
_) = Bool
True
         isVar PTerm
_ = Bool
False

{- | Parses a conditional expression
@
If ::= 'if' Expr 'then' Expr 'else' Expr
@

-}
if_ :: SyntaxInfo -> IdrisParser PTerm
if_ :: SyntaxInfo -> IdrisParser PTerm
if_ SyntaxInfo
syn = (do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"if"
              (c, 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
expr SyntaxInfo
syn
              keyword "then"
              t <- expr syn
              keyword "else"
              f <- expr syn
              return (PIfThenElse fc c t f))
          IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"conditional expression"


{- | Parses a quote goal

@
QuoteGoal ::=
  'quoteGoal' Name 'by' Expr 'in' Expr
  ;
@
 -}
quoteGoal :: SyntaxInfo -> IdrisParser PTerm
quoteGoal :: SyntaxInfo -> IdrisParser PTerm
quoteGoal SyntaxInfo
syn = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"quoteGoal"; n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name;
                   keyword "by"
                   r <- expr syn
                   keyword "in"
                   (sc, fc) <- withExtent $ expr syn
                   return (PGoal fc r n sc)
                IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"quote goal expression"

{- | Parses a dependent type signature

@
Pi ::= PiOpts Static? Pi'
@

@
Pi' ::=
    OpExpr ('->' Pi)?
  | '(' TypeDeclList           ')'            '->' Pi
  | '{' TypeDeclList           '}'            '->' Pi
  | '{' 'auto'    TypeDeclList '}'            '->' Pi
  | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
  ;
@
 -}

bindsymbol :: [ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st p
syn
     = do [Char] -> m ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"->"
          Plicity -> m Plicity
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp [ArgOpt]
opts Static
st Bool
False RigCount
RigW)

explicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
explicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn
   = do xt <- IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn IdrisParser [(RigCount, Name, FC, PTerm)]
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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])) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')')
        binder <- bindsymbol opts st syn
        sc <- expr (allowConstr syn)
        return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
binder { pcount = r })) xt sc)

autoImplicit :: p -> Static -> SyntaxInfo -> IdrisParser PTerm
autoImplicit p
opts Static
st SyntaxInfo
syn
   = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"auto"
        Bool
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Static
st Static -> Static -> Bool
forall a. Eq a => a -> a -> Bool
== Static
Static) (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"auto implicits can not be static"
        xt <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn
        lchar '}'
        symbol "->"
        sc <- expr (allowConstr syn)
        return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi
          ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [] Static
Dynamic ([PTactic] -> PTerm
PTactics [Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
True Bool
True Int
100 Maybe Name
forall a. Maybe a
Nothing [] []]) RigCount
r)) xt sc)

defaultImplicit :: p -> Static -> SyntaxInfo -> IdrisParser PTerm
defaultImplicit p
opts Static
st SyntaxInfo
syn = do
   [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"default"
   Bool
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Static
st Static -> Static -> Bool
forall a. Eq a => a -> a -> Bool
== Static
Static) (StateT IState (WriterT FC (Parsec Void [Char])) ()
 -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall a.
[Char] -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"default implicits can not be static"
   ist <- StateT IState (WriterT FC (Parsec Void [Char])) IState
forall s (m :: * -> *). MonadState s m => m s
get
   script' <- simpleExpr syn
   let script = SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ PTerm
script'
   xt <- typeDeclList syn
   lchar '}'
   symbol "->"
   sc <- expr (allowConstr syn)
   return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [] Static
Dynamic PTerm
script RigCount
r)) xt sc)

normalImplicit :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
normalImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn = do
   xt <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn IdrisParser [(RigCount, Name, FC, PTerm)]
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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])) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
   symbol "->"
   cs <- constraintList syn
   sc <- expr syn
   let (im,cl)
          = if implicitAllowed syn
               then (Imp opts st False (Just (Impl False True False)) True RigW,
                      constraint)
               else (Imp opts st False (Just (Impl False False False)) True RigW,
                     Imp opts st False (Just (Impl True False False)) True RigW)
   return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
im { pcount = r })) xt
           (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
cl { pcount = r })) cs sc))

constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
constraintPi [ArgOpt]
opts Static
st SyntaxInfo
syn =
   do cs <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn
      sc <- expr syn
      if implicitAllowed syn
         then return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint { pcount = r }) cs sc)
         else return (bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
st Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
True Bool
False Bool
False)) Bool
True RigCount
r))
                               cs sc)

implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
implicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn =
      [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
forall {p}. p -> Static -> SyntaxInfo -> IdrisParser PTerm
autoImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
forall {p}. p -> Static -> SyntaxInfo -> IdrisParser PTerm
defaultImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
          IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser 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
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
normalImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn

unboundPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPi [ArgOpt]
opts Static
st SyntaxInfo
syn = do
       x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do binder <- bindsymbol opts st syn
           sc <- expr syn
           return (PPi binder (sUN "__pi_arg") NoFC x sc))
              <|> return x

-- This is used when we need to disambiguate from a constraint list
unboundPiNoConstraint :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPiNoConstraint [ArgOpt]
opts Static
st SyntaxInfo
syn = do
       x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do binder <- bindsymbol opts st syn
           sc <- expr syn
           P.notFollowedBy $ reservedOp "=>"
           return (PPi binder (sUN "__pi_arg") NoFC x sc))
              <|> do P.notFollowedBy $ reservedOp "=>"
                     return x


pi :: SyntaxInfo -> IdrisParser PTerm
pi :: SyntaxInfo -> IdrisParser PTerm
pi SyntaxInfo
syn =
     do opts <- SyntaxInfo -> IdrisParser [ArgOpt]
piOpts SyntaxInfo
syn
        st   <- static
        explicitPi opts st syn
         <|> P.try (do lchar '{'; implicitPi opts st syn)
         <|> if constraintAllowed syn
                then P.try (unboundPiNoConstraint opts st syn)
                           <|> constraintPi opts st syn
                else unboundPi opts st syn
  IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"dependent type signature"

{- | Parses Possible Options for Pi Expressions
@
  PiOpts ::= '.'?
@
-}
piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
piOpts SyntaxInfo
syn | SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn =
        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
-> IdrisParser [ArgOpt] -> IdrisParser [ArgOpt]
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [ArgOpt] -> IdrisParser [ArgOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ArgOpt
InaccessibleArg]
    IdrisParser [ArgOpt]
-> IdrisParser [ArgOpt] -> IdrisParser [ArgOpt]
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
<|> [ArgOpt] -> IdrisParser [ArgOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
piOpts SyntaxInfo
syn = [ArgOpt] -> IdrisParser [ArgOpt]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

{- | Parses a type constraint list

@
ConstraintList ::=
    '(' Expr_List ')' '=>'
  | Expr              '=>'
  ;
@
-}
constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 (SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn)
                     IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, 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
<|> [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('
                                tys <- StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
nexpr (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                lchar ')'
                                reservedOp "=>"
                                return tys)
                  IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, 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
<|> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 t <- SyntaxInfo -> IdrisParser PTerm
opExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                                reservedOp "=>"
                                return [(RigW, defname, NoFC, t)])
                  IdrisParser [(RigCount, Name, FC, PTerm)]
-> [Char] -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"type constraint list"
  where nexpr :: StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
nexpr = StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (RigCount, Name, FC, PTerm)
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 (n, fc) <- 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
name; lchar ':'
                          e <- expr (disallowImp syn)
                          return (RigW, n, fc, e))
                StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (RigCount, 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
<|> do e <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                       return (RigW, defname, NoFC, e)
        defname :: Name
defname = Int -> [Char] -> Name
sMN Int
0 [Char]
"constraint"

{- | Parses a type declaration list
@
TypeDeclList ::=
    FunctionSignatureList
  | NameList TypeSig
  ;
@

@
FunctionSignatureList ::=
    Name TypeSig
  | Name TypeSig ',' FunctionSignatureList
  ;
@
-}
typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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]))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do rig <- StateT IState (WriterT FC (Parsec Void [Char])) RigCount
forall (m :: * -> *). Parsing m => m RigCount
rigCount
                                       (x, xfc) <- withExtent fnName
                                       lchar ':'
                                       t <- typeExpr (disallowImp syn)
                                       return (rig, x, xfc, t))
                             (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
                   IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, 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
<|> do ns <- StateT IState (WriterT FC (Parsec Void [Char])) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) [(Name, FC)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (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
name) (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                          lchar ':'
                          t <- typeExpr (disallowImp syn)
                          return (map (\(Name
x, FC
xfc) -> (RigCount
RigW, Name
x, FC
xfc, PTerm
t)) ns)
                   IdrisParser [(RigCount, Name, FC, PTerm)]
-> [Char] -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"type declaration list"

{- | Parses a type declaration list with optional parameters
@
TypeOptDeclList ::=
    NameOrPlaceholder TypeSig?
  | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
  ;
@

@
NameOrPlaceHolder ::= Name | '_';
@
-}
tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList SyntaxInfo
syn = StateT
  IState
  (WriterT FC (Parsec Void [Char]))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do (x, fc) <- 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
nameOrPlaceholder
                                 t <- P.option Placeholder (do lchar ':'
                                                               expr syn)
                                 return (RigW, x, fc, t))
                             (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    IdrisParser [(RigCount, Name, FC, PTerm)]
-> [Char] -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"type declaration list"
    where  nameOrPlaceholder :: IdrisParser Name
           nameOrPlaceholder :: StateT IState (WriterT FC (Parsec Void [Char])) Name
nameOrPlaceholder = StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                           StateT IState (WriterT FC (Parsec Void [Char])) Name
-> 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
-> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> [Char] -> Name
sMN Int
0 [Char]
"underscore" Name
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
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 ()
reservedOp [Char]
"_"
                           StateT IState (WriterT FC (Parsec Void [Char])) Name
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"name or placeholder"

{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
@
ListExpr ::=
     '[' ']'
  | '[' Expr '|' DoList ']'
  | '[' ExprList ']'
;
@
@
DoList ::=
    Do
  | Do ',' DoList
  ;
@
@
ExprList ::=
  Expr
  | Expr ',' ExprList
  ;
@
 -}
listExpr :: SyntaxInfo -> IdrisParser PTerm
listExpr :: SyntaxInfo -> IdrisParser PTerm
listExpr SyntaxInfo
syn = do (FC f (l, c) _) <- StateT IState (WriterT FC (Parsec Void [Char])) Char
-> StateT IState (WriterT FC (Parsec Void [Char])) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'[')
                  (do (FC _ _ (l', c')) <- extent (lchar ']') <?> "end of list expression"
                      return (mkNil (FC f (l, c) (l', c'))))
                   <|> (do (x, fc) <- withExtent (expr (syn { withAppAllowed = False })) <?> "expression"
                           (do P.try (lchar '|') <?> "list comprehension"
                               qs <- P.sepBy1 (do_ syn) (lchar ',')
                               lchar ']'
                               return (PDoBlock (map addGuard qs ++
                                          [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))
                                                       [pexp x])]))) <|>
                            (do xs <- many (do commaFC <- extent (lchar ',') <?> "list element"
                                               elt <- expr syn
                                               return (elt, commaFC))
                                rbrackFC <- extent (lchar ']') <?> "end of list expression"
                                return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))
                IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"list expression"
  where
    mkNil :: FC -> PTerm
    mkNil :: FC -> PTerm
mkNil FC
fc = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] ([Char] -> Name
sUN [Char]
"Nil")
    mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
    mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
mkList FC
errFC FC
nilFC [] = FC -> [FC] -> Name -> PTerm
PRef FC
nilFC [FC
nilFC] ([Char] -> Name
sUN [Char]
"Nil")
    mkList FC
errFC FC
nilFC ((PTerm
x, FC
fc) : [(PTerm, FC)]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
errFC (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] ([Char] -> Name
sUN [Char]
"::")) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
x, PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> FC -> [(PTerm, FC)] -> PTerm
mkList FC
errFC FC
nilFC [(PTerm, FC)]
xs)]
    addGuard :: PDo -> PDo
    addGuard :: PDo -> PDo
addGuard (DoExp FC
fc PTerm
e) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"guard"))
                                              [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
e])
    addGuard PDo
x = PDo
x

{- | Parses a do-block
@
Do' ::= Do KeepTerminator;
@

@
DoBlock ::=
  'do' OpenBlock Do'+ CloseBlock
  ;
@
 -}
doBlock :: SyntaxInfo -> IdrisParser PTerm
doBlock :: SyntaxInfo -> IdrisParser PTerm
doBlock SyntaxInfo
syn
    = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"do"
         [PDo] -> PTerm
PDoBlock ([PDo] -> PTerm)
-> StateT IState (WriterT FC (Parsec Void [Char])) [PDo]
-> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) [PDo]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PDo
do_ SyntaxInfo
syn)
      IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"do block"

{- | Parses an expression inside a do block
@
Do ::=
    'let' Name  TypeSig'?      '=' Expr
  | 'let' Expr'                '=' Expr
  | 'rewrite Expr
  | Name  '<-' Expr
  | Expr' '<-' Expr
  | Expr
  ;
@
-}
do_ :: SyntaxInfo -> IdrisParser PDo
do_ :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PDo
do_ SyntaxInfo
syn
     = StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                 (i, ifc) <- 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
name
                 ty' <- P.optional (do lchar ':'
                                       expr' syn)
                 reservedOp "="
                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })
                 -- If there is an explicit type, this can’t be a pattern-matching let, so do not parse alternatives
                 P.option (DoLet fc RigW i ifc (fromMaybe Placeholder ty') e)
                          (do lchar '|'
                              when (isJust ty') $ fail "a pattern-matching let may not have an explicit type annotation"
                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
                              return (DoLetP fc (PRef ifc [ifc] i) e ts)))
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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
<|> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                 i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 reservedOp "="
                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })
                 P.option (DoLetP fc i e [])
                          (do lchar '|'
                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
                              return (DoLetP fc i e ts)))
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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
<|> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 (sc, fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void [Char])) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent ([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"rewrite" StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser PTerm -> IdrisParser PTerm
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                 return (DoRewrite fc sc))
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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
<|> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 (i, ifc) <- 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
name
                 symbol "<-"
                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False });
                 P.option (DoBind fc i ifc e)
                          (do lchar '|'
                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
                              return (DoBindP fc (PRef ifc [ifc] i) e ts)))
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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
<|> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 symbol "<-"
                 (e, fc) <- withExtent $ expr (syn { withAppAllowed = False });
                 P.option (DoBindP fc i e [])
                          (do lchar '|'
                              ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
                              return (DoBindP fc i e ts)))
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> StateT IState (WriterT FC (Parsec Void [Char])) PDo
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 (e, 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
expr SyntaxInfo
syn
          return (DoExp fc e)
   StateT IState (WriterT FC (Parsec Void [Char])) PDo
-> [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) PDo
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"do block expression"

do_alt :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt SyntaxInfo
syn = do l <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                P.option (Placeholder, l)
                         (do symbol "=>"
                             r <- expr' syn
                             return (l, r))

{- | Parses an expression in idiom brackets
@
Idiom ::= '[|' Expr '|]';
@
-}
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom SyntaxInfo
syn
    = do [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"[|"
         (e, 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
expr (SyntaxInfo
syn { withAppAllowed = False })
         symbol "|]"
         return (PIdiom fc e)
      IdrisParser PTerm -> [Char] -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression in idiom brackets"

{- |Parses a constant or literal expression

@
Constant ::=
    'Integer'
  | 'Int'
  | 'Char'
  | 'Double'
  | 'String'
  | 'Bits8'
  | 'Bits16'
  | 'Bits32'
  | 'Bits64'
  | Float_t
  | Natural_t
  | VerbatimString_t
  | String_t
  | Char_t
  ;
@
-}

constants :: [(String, Idris.Core.TT.Const)]
constants :: [([Char], Const)]
constants =
  [ ([Char]
"Integer",            ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
  , ([Char]
"Int",                ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
  , ([Char]
"Char",               ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
  , ([Char]
"Double",             ArithTy -> Const
AType ArithTy
ATFloat)
  , ([Char]
"String",             Const
StrType)
  , ([Char]
"prim__WorldType",    Const
WorldType)
  , ([Char]
"prim__TheWorld",     Const
TheWorld)
  , ([Char]
"Bits8",              ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
  , ([Char]
"Bits16",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
  , ([Char]
"Bits32",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
  , ([Char]
"Bits64",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))
  ]

-- | Parse a constant and its source span
constant :: Parsing m => m Idris.Core.TT.Const
constant :: forall (m :: * -> *). Parsing m => m Const
constant = [m Const] -> m Const
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ Const
ty Const -> m () -> m Const
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> m ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
name | ([Char]
name, Const
ty) <- [([Char], Const)]
constants ]
       m Const -> m Const -> m Const
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Const -> m Const
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Double -> Const
Fl (Double -> Const) -> m Double -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Double
forall (m :: * -> *). Parsing m => m Double
float)
       m Const -> m Const -> m Const
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Const
BI (Integer -> Const) -> m Integer -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall (m :: * -> *). Parsing m => m Integer
natural
       m Const -> m Const -> m Const
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Const
Str ([Char] -> Const) -> m [Char] -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Char]
forall (m :: * -> *). Parsing m => m [Char]
verbatimStringLiteral
       m Const -> m Const -> m Const
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Const
Str ([Char] -> Const) -> m [Char] -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [Char]
forall (m :: * -> *). Parsing m => m [Char]
stringLiteral
       m Const -> m Const -> m Const
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Const -> m Const
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> Const
Ch (Char -> Const) -> m Char -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Char
forall (m :: * -> *). Parsing m => m Char
charLiteral) --Currently ambigous with symbols
       m Const -> [Char] -> m Const
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"constant or literal"

{- | Parses a verbatim multi-line string literal (triple-quoted)

@
VerbatimString_t ::=
  '\"\"\"' ~'\"\"\"' '\"'* '\"\"\"'
;
@
 -}
verbatimStringLiteral :: Parsing m => m String
verbatimStringLiteral :: forall (m :: * -> *). Parsing m => m [Char]
verbatimStringLiteral = m [Char] -> m [Char]
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m [Char] -> m [Char]) -> m [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ do m [Char] -> m [Char]
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m [Char] -> m [Char]) -> m [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> m [Char]
forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
"\"\"\""
                                   str <- m Char -> m [Char] -> m [Char]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.manyTill m Char
m (Token [Char])
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle (m [Char] -> m [Char]) -> m [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ m [Char] -> m [Char]
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([Char] -> m [Char]
forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
"\"\"\"")
                                   moreQuotes <- P.many $ P.char '"'
                                   return $ str ++ moreQuotes

{- | Parses a static modifier

@
Static ::=
  '%static'
;
@
-}
static :: IdrisParser Static
static :: IdrisParser Static
static =     Static
Static Static
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
-> IdrisParser Static
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]
"%static"
         IdrisParser Static -> IdrisParser Static -> IdrisParser Static
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
<|> Static -> IdrisParser Static
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Static
Dynamic
         IdrisParser Static -> [Char] -> IdrisParser Static
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"static modifier"

{- | Parses a tactic script

@
Tactic ::= 'intro' NameList?
       |   'intros'
       |   'refine'      Name Imp+
       |   'mrefine'     Name
       |   'rewrite'     Expr
       |   'induction'   Expr
       |   'equiv'       Expr
       |   'let'         Name ':' Expr' '=' Expr
       |   'let'         Name           '=' Expr
       |   'focus'       Name
       |   'exact'       Expr
       |   'applyTactic' Expr
       |   'reflect'     Expr
       |   'fill'        Expr
       |   'try'         Tactic '|' Tactic
       |   '{' TacticSeq '}'
       |   'compute'
       |   'trivial'
       |   'solve'
       |   'attack'
       |   'state'
       |   'term'
       |   'undo'
       |   'qed'
       |   'abandon'
       |   ':' 'q'
       ;

Imp ::= '?' | '_';

TacticSeq ::=
    Tactic ';' Tactic
  | Tactic ';' TacticSeq
  ;
@
-}

-- | A specification of the arguments that tactics can take
data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
               | ExprTArg
               | AltsTArg
               | StringLitTArg

-- The FIXMEs are Issue #1766 in the issue tracker.
--     https://github.com/idris-lang/Idris-dev/issues/1766
-- | A list of available tactics and their argument requirements
tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics :: [([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics =
  [ ([[Char]
"intro"], Maybe TacticArg
forall a. Maybe a
Nothing, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ -- FIXME syntax for intro (fresh name)
      do ns <- 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 sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced 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
','); return $ Intro ns)
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"intros"] PTactic
forall t. PTactic' t
Intros
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"unfocus"] PTactic
forall t. PTactic' t
Unfocus
  , ([[Char]
"refine"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          imps <- many imp
          return $ Refine n imps)
  , ([[Char]
"claim"], Maybe TacticArg
forall a. Maybe a
Nothing, \SyntaxInfo
syn ->
       do n <- StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
          goal <- indentGt *> expr syn
          return $ Claim n goal)
  , ([[Char]
"mrefine"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          return $ MatchRefine n)
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"rewrite"] PTerm -> PTactic
forall t. t -> PTactic' t
Rewrite
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"equiv"] PTerm -> PTactic
forall t. t -> PTactic' t
Equiv
  , ([[Char]
"let"], Maybe TacticArg
forall a. Maybe a
Nothing, \SyntaxInfo
syn -> -- FIXME syntax for let
       do n <- (StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void [Char])) ()
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name)
          (do indentGt *> lchar ':'
              ty <- indentGt *> expr' syn
              indentGt *> lchar '='
              t <- indentGt *> expr syn
              i <- get
              return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
            <|> (do indentGt *> lchar '='
                    t <- indentGt *> expr syn
                    i <- get
                    return $ LetTac n (desugar syn i t)))

  , ([[Char]
"focus"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do n <- StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
          return $ Focus n)
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"exact"] PTerm -> PTactic
forall t. t -> PTactic' t
Exact
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"applyTactic"] PTerm -> PTactic
forall t. t -> PTactic' t
ApplyTactic
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"byReflection"] PTerm -> PTactic
forall t. t -> PTactic' t
ByReflection
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"reflect"] PTerm -> PTactic
forall t. t -> PTactic' t
Reflect
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"fill"] PTerm -> PTactic
forall t. t -> PTactic' t
Fill
  , ([[Char]
"try"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
AltsTArg, \SyntaxInfo
syn ->
        do t <- IdrisParser PTactic -> IdrisParser PTactic
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
           lchar '|'
           t1 <- spaced (tactic syn)
           return $ Try t t1)
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"compute"] PTactic
forall t. PTactic' t
Compute
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"trivial"] PTactic
forall t. PTactic' t
Trivial
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"unify"] PTactic
forall t. PTactic' t
DoUnify
  , ([[Char]
"search"], Maybe TacticArg
forall a. Maybe a
Nothing, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
      do depth <- Integer
-> StateT IState (WriterT FC (Parsec Void [Char])) Integer
-> StateT IState (WriterT FC (Parsec Void [Char])) Integer
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Integer
10 StateT IState (WriterT FC (Parsec Void [Char])) Integer
forall (m :: * -> *). Parsing m => m Integer
natural
         return (ProofSearch True True (fromInteger depth) Nothing [] []))
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"implementation"] PTactic
forall t. PTactic' t
TCImplementation
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"solve"] PTactic
forall t. PTactic' t
Solve
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"attack"] PTactic
forall t. PTactic' t
Attack
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"state", [Char]
":state"] PTactic
forall t. PTactic' t
ProofState
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"term", [Char]
":term"] PTactic
forall t. PTactic' t
ProofTerm
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"undo", [Char]
":undo"] PTactic
forall t. PTactic' t
Undo
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"qed", [Char]
":qed"] PTactic
forall t. PTactic' t
Qed
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"abandon", [Char]
":q"] PTactic
forall t. PTactic' t
Abandon
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"skip"] PTactic
forall t. PTactic' t
Skip
  , [[Char]]
-> PTactic
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"sourceLocation"] PTactic
forall t. PTactic' t
SourceFC
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
":e", [Char]
":eval"] PTerm -> PTactic
forall t. t -> PTactic' t
TEval
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
":t", [Char]
":type"] PTerm -> PTactic
forall t. t -> PTactic' t
TCheck
  , [[Char]]
-> (PTerm -> PTactic)
-> ([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
":search"] PTerm -> PTactic
forall t. t -> PTactic' t
TSearch
  , ([[Char]
"fail"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
StringLitTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do msg <- StateT IState (WriterT FC (Parsec Void [Char])) [Char]
forall (m :: * -> *). Parsing m => m [Char]
stringLiteral
          return $ TFail [Idris.Core.TT.TextPart msg])
  , ([[Char]
":doc"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => m ()
whiteSpace
          doc <- (Const -> Either Name Const
forall a b. b -> Either a b
Right (Const -> Either Name Const)
-> StateT IState (WriterT FC (Parsec Void [Char])) Const
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Either Name Const)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) Const
forall (m :: * -> *). Parsing m => m Const
constant) StateT IState (WriterT FC (Parsec Void [Char])) (Either Name Const)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Either Name Const)
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Either Name Const)
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
<|> (Name -> Either Name Const
forall a b. a -> Either a b
Left (Name -> Either Name Const)
-> StateT IState (WriterT FC (Parsec Void [Char])) Name
-> StateT
     IState (WriterT FC (Parsec Void [Char])) (Either Name Const)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void [Char])) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
          P.eof
          return (TDocStr doc))
  ]
  where
  expressionTactic :: a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic a
names PTerm -> b
tactic = (a
names, TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, \SyntaxInfo
syn ->
     do t <- IdrisParser PTerm -> IdrisParser PTerm
forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced (SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
        i <- get
        return $ tactic (desugar syn i t))
  noArgs :: a -> a -> (a, Maybe a, b -> m a)
noArgs a
names a
tactic = (a
names, Maybe a
forall a. Maybe a
Nothing, m a -> b -> m a
forall a b. a -> b -> a
const (a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
tactic))
  spaced :: f b -> f b
spaced f b
parser = f ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt f () -> f b -> f b
forall a b. f a -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f b
parser
  imp :: IdrisParser Bool
  imp :: StateT IState (WriterT FC (Parsec Void [Char])) Bool
imp = do Char -> StateT IState (WriterT FC (Parsec Void [Char])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'?'; Bool -> StateT IState (WriterT FC (Parsec Void [Char])) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    StateT IState (WriterT FC (Parsec Void [Char])) Bool
-> StateT IState (WriterT FC (Parsec Void [Char])) Bool
-> StateT IState (WriterT FC (Parsec Void [Char])) Bool
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])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'_'; Bool -> StateT IState (WriterT FC (Parsec Void [Char])) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void [Char])) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True


tactic :: SyntaxInfo -> IdrisParser PTactic
tactic :: SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn = [IdrisParser PTactic] -> IdrisParser PTactic
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ do [StateT IState (WriterT FC (Parsec Void [Char])) ()]
-> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice (([Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ())
-> [[Char]] -> [StateT IState (WriterT FC (Parsec Void [Char])) ()]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> StateT IState (WriterT FC (Parsec Void [Char])) ()
forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [[Char]]
names); SyntaxInfo -> IdrisParser PTactic
parser SyntaxInfo
syn
                      | ([[Char]]
names, Maybe TacticArg
_, SyntaxInfo -> IdrisParser PTactic
parser) <- [([[Char]], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics ]
          IdrisParser PTactic -> IdrisParser PTactic -> IdrisParser PTactic
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])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
                 t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn;
                 lchar ';';
                 ts <- P.sepBy1 (tactic syn) (lchar ';')
                 lchar '}'
                 return $ TSeq t (mergeSeq ts)
          IdrisParser PTactic -> IdrisParser PTactic -> IdrisParser PTactic
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])) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':' StateT IState (WriterT FC (Parsec Void [Char])) Char
-> IdrisParser PTactic -> IdrisParser PTactic
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
>> IdrisParser PTactic
forall a. StateT IState (WriterT FC (Parsec Void [Char])) a
forall (f :: * -> *) a. Alternative f => f a
empty) IdrisParser PTactic -> [Char] -> IdrisParser PTactic
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"prover command")
          IdrisParser PTactic -> [Char] -> IdrisParser PTactic
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"tactic"
  where
    mergeSeq :: [PTactic] -> PTactic
    mergeSeq :: [PTactic] -> PTactic
mergeSeq [PTactic
t]    = PTactic
t
    mergeSeq (PTactic
t:[PTactic]
ts) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
t ([PTactic] -> PTactic
mergeSeq [PTactic]
ts)

-- | Parses a tactic as a whole
fullTactic :: SyntaxInfo -> IdrisParser PTactic
fullTactic :: SyntaxInfo -> IdrisParser PTactic
fullTactic SyntaxInfo
syn = do t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn
                    P.eof
                    return t