{-|
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 :: Bool
implicitAllowed = Bool
True,
                     constraintAllowed :: Bool
constraintAllowed = Bool
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 :: Bool
implicitAllowed = Bool
False,
                      constraintAllowed :: Bool
constraintAllowed = Bool
False }

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

{-| Parses an expression as a whole
@
  FullExpr ::= Expr EOF_t;
@
 -}
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr SyntaxInfo
syn = do PTerm
x <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                  forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                  IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
x)

tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr :: SyntaxInfo -> IState -> [Char] -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
st = forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (forall t. [Char] -> Err' t
Msg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> Doc
parseErrorDoc) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
P.makeExprParser (SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn) ([FixDecl]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void [Char]))) PTerm]]
table (IState -> [FixDecl]
idris_infixes IState
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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
externalExpr SyntaxInfo
syn)
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
internalExpr SyntaxInfo
syn
            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 IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                      (PTerm
expr, outerFC :: FC
outerFC@(FC [Char]
fn (Int, Int)
_ (Int, Int)
_)) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions SyntaxInfo
syn (SyntaxRules -> [Syntax]
syntaxRulesList forall a b. (a -> b) -> a -> b
$ IState -> SyntaxRules
syntax_rules IState
i)
                      forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
mapPTermFC (FC -> FC -> FC
fixFC FC
outerFC) ([Char] -> FC -> FC -> FC
fixFCH [Char]
fn FC
outerFC) PTerm
expr)
                   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 IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                            SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions SyntaxInfo
syn (forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isSimple (SyntaxRules -> [Syntax]
syntaxRulesList forall a b. (a -> b) -> a -> b
$ IState -> SyntaxRules
syntax_rules IState
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 forall a. [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 [] (forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isValid [Syntax]
rules)
                       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]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SynMatch] -> ShowS
$cshowList :: [SynMatch] -> ShowS
show :: SynMatch -> [Char]
$cshow :: SynMatch -> [Char]
showsPrec :: Int -> SynMatch -> ShowS
$cshowsPrec :: Int -> 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 =
  forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall {a}. Eq a => [a] -> [a] -> Bool
ruleGroup forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Syntax -> [SSymbol]
syntaxSymbols) [Syntax]
rules) forall a b. (a -> b) -> a -> b
$ \[Syntax]
rs ->
    case forall a. [a] -> a
head [Syntax]
rs of -- can never be []
      Rule (SSymbol
symb:[SSymbol]
_) PTerm
_ SynContext
_ -> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
        Maybe (Name, SynMatch)
n <- SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol SSymbol
symb
        SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension SyntaxInfo
syn (Maybe (Name, SynMatch)
n forall a. a -> [a] -> [a]
: [Maybe (Name, SynMatch)]
ns) [[SSymbol] -> PTerm -> SynContext -> Syntax
Rule [SSymbol]
ss PTerm
t SynContext
ctx | (Rule (SSymbol
_:[SSymbol]
ss) PTerm
t SynContext
ctx) <- [Syntax]
rs]
      -- If we have more than one Rule in this bucket, our grammar is
      -- nondeterministic.
      Rule [] PTerm
ptm SynContext
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
flatten ([(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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 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)    = forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword (forall a. Show a => a -> [Char]
show Name
n)
    extensionSymbol (Expr Name
n)       = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extensionSymbol (SimpleExpr Name
n) = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extensionSymbol (Binding Name
n)    = do (Name
b, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, FC -> Name -> SynMatch
SynBind FC
fc Name
b)
    extensionSymbol (Symbol [Char]
s)     = forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (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 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 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 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) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PPatvar) 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 (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 (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 (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) (forall a b. (a -> b) -> [a] -> [b]
map (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) (forall a b. (a -> b) -> [a] -> [b]
map (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) (forall a b. (a -> b) -> [a] -> [b]
map (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) (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 (forall a b. (a, b) -> a
fst 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 (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 forall a b. (a -> b) -> a -> b
$ 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) = 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) = 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) = 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)
                    = 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)
                                 (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)
                    = 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)
                                (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) = 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 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) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PMetavar) 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 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 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 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) (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 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 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') = forall t. [Name] -> PTactic' t
Intro forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
ns'
    updTactic [(Name, SynMatch)]
ns (Focus Name
n) = forall t. Name -> PTactic' t
Focus forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst 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) = forall t. Name -> [Bool] -> PTactic' t
Refine (forall a b. (a, b) -> a
fst 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) = forall t. Name -> t -> PTactic' t
Claim (forall a b. (a, b) -> a
fst 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) = forall t. Name -> PTactic' t
MatchRefine (forall a b. (a, b) -> a
fst 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) = forall t. Name -> t -> PTactic' t
LetTac (forall a b. (a, b) -> a
fst 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) = forall t. Name -> t -> t -> PTactic' t
LetTacTy (forall a b. (a, b) -> a
fst 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) = forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
rec Bool
prover Int
depth
      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) Maybe Name
top) (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
psns) (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
hints)
    updTactic [(Name, SynMatch)]
ns (Try PTactic
l PTactic
r) = 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) = 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) = forall t. [Char] -> PTactic' t -> PTactic' t
GoalType [Char]
s 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)) = forall t. Either Name Const -> PTactic' t
TDocStr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst 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 = 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 forall a. Eq a => a -> a -> Bool
== Name
x = [(Name, a)]
xs
                         | Bool
otherwise = (Name
x,a
t)forall a. a -> [a] -> [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
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
runElab SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
disamb SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
noImplicits SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
recordType SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
if_ SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
lambda SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
quoteGoal SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
let_ SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
rewriteTerm SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
doBlock SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
caseExpr SyntaxInfo
syn
     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
app SyntaxInfo
syn
     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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"case"
                  (PTerm
scr, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                  forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"of"
                  [(PTerm, PTerm)]
opts <- forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption SyntaxInfo
syn)
                  forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
scr [(PTerm, PTerm)]
opts)
               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 PTerm
lhs <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True }))
                    PTerm
r <- IdrisParser PTerm
impossible forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"=>" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                    forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
lhs, PTerm
r)
                 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"case option"

warnTacticDeprecation :: FC -> IdrisParser ()
warnTacticDeprecation :: FC -> IdrisParser ()
warnTacticDeprecation FC
fc =
 FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning FC
fc (forall a. a -> Maybe a
Just Opt
NoOldTacticDeprecationWarnings) (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 FC
kw <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"proof"
                   [PTactic]
ts <- forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
                   FC -> IdrisParser ()
warnTacticDeprecation FC
kw
                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [PTactic] -> PTerm
PProof [PTactic]
ts
                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 FC
kw <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"tactics"
                     [PTactic]
ts <- forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
                     FC -> IdrisParser ()
warnTacticDeprecation FC
kw
                     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [PTactic] -> PTerm
PTactics [PTactic]
ts
                  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 =
            forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (Name
x, FC [Char]
f (Int
l, Int
c) (Int, Int)
end) <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'?' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name)
               forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> PTerm
PMetavar ([Char] -> (Int, Int) -> (Int, Int) -> FC
FC [Char]
f (Int
l, Int
cforall a. Num a => a -> a -> a
-Int
1) (Int, Int)
end) Name
x)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"implementation"; forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
PResolveTC FC
fc)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"instance"
               FC -> Maybe Opt -> Err -> IdrisParser ()
parserWarning FC
fc forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall t. [Char] -> Err' t
Msg [Char]
"The use of %instance is deprecated, use %implementation instead."
               forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
PResolveTC FC
fc)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
proofExpr SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
tacticsExpr SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"Type*"); forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
AllTypes)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"AnyType"; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
AllTypes
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FC -> PTerm
PType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"Type")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"UniqueType"; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
UniqueType
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"NullType"; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
NullType
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (Const
c, FC
cfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m Const
constant
               forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst SyntaxInfo
syn FC
cfc (FC -> Const -> PTerm
PConstant FC
cfc Const
c))
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"'"; (Name
str, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
               forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"Symbol_"))
                          [forall {t}. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC ([Char] -> Const
Str (forall a. Show a => a -> [Char]
show Name
str)))])
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (Name
x, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
               if SyntaxInfo -> Bool
inPattern SyntaxInfo
syn
                  then forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
x)
                                (do forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"@"
                                    (PTerm
s, FC
fcIn) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> PTerm -> PTerm
PAs FC
fcIn Name
x PTerm
s))
                  else forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
x)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
idiom SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
listExpr SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
alt SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"!"
               (PTerm
s, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
               forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc PTerm
s [])
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
bracketed (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
quasiquote SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
namequote SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
unquote SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'_'; forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
Placeholder
        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 [Char]
fn (Int
sl, Int
sc) (Int, Int)
_) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(') forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"parenthesized expression"
                   FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' ([Char] -> (Int, Int) -> (Int, Int) -> FC
FC [Char]
fn (Int
sl, Int
sc) (Int
sl, Int
scforall a. Num a => a -> a -> a
+Int
1)) (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
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
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). MonadWriter FC m => FC -> m ()
addExtent FC
open forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')')
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> PunInfo -> PTerm
PTrue FC
fc PunInfo
TypeOrTerm
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Name
opName, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName
                      Name -> IdrisParser ()
guardNotPrefix Name
opName

                      PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                      forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> [Char] -> Name
sMN Int
1000 [Char]
"ARG") FC
NoFC PTerm
Placeholder
                        (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
opName) [forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
1000 [Char]
"ARG")),
                                                      forall {t}. t -> PArg' t
pexp PTerm
e]))
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \PTerm
l ->
                     forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Name
opName, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
operatorName
                               forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> [Char] -> Name
sMN Int
1000 [Char]
"ARG") FC
NoFC PTerm
Placeholder
                                 (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
opName) [forall {t}. t -> PArg' t
pexp PTerm
l,
                                                               forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> [Char] -> Name
sMN Int
1000 [Char]
"ARG"))]))
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr SyntaxInfo
syn FC
open PTerm
l)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
l <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
               SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn) FC
open PTerm
l
  where
    justPrefix                          :: FixDecl -> Maybe Name
    justPrefix :: FixDecl -> Maybe Name
justPrefix (Fix (PrefixN Int
_) [Char]
opName) = forall a. a -> Maybe a
Just ([Char] -> Name
sUN [Char]
opName)
    justPrefix FixDecl
_                        = forall a. Maybe a
Nothing

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

      [FixDecl]
ops <- IState -> [FixDecl]
idris_infixes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
opName forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FixDecl -> Maybe Name
justPrefix forall a b. (a -> b) -> a -> b
$ [FixDecl]
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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PTerm, Maybe (FC, PTerm), FC)]
prev then
      IdrisParser PTerm
nametypePart forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart
  else
    case PunInfo
pun of
      PunInfo
IsType -> IdrisParser PTerm
nametypePart forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart 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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> IdrisParser PTerm
exprPart Bool
False
  where nametypePart :: IdrisParser PTerm
nametypePart = do
          (Name
ln, FC
lnfc, FC
colonFC) <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
            (Name
ln, FC
lnfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
            FC
colonFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':')
            forall (m :: * -> *) a. Monad m => a -> m a
return (Name
ln, FC
lnfc, FC
colonFC)
          PTerm
lty <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
          FC
starsFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"
          PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsType ((FC -> [FC] -> Name -> PTerm
PRef FC
lnfc [] Name
ln, forall a. a -> Maybe a
Just (FC
colonFC, PTerm
lty), FC
starsFC)forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
        namePart :: IdrisParser PTerm
namePart = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
          (Name
ln, FC
lnfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
          FC
starsFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"
          PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
pun ((FC -> [FC] -> Name -> PTerm
PRef FC
lnfc [] Name
ln, forall a. Maybe a
Nothing, FC
starsFC)forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
        exprPart :: Bool -> IdrisParser PTerm
exprPart Bool
isEnd = do
          PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          Either FC FC
sepFCE <-
            let stars :: StateT IState (WriterT FC (Parsec Void [Char])) (Either FC b)
stars = (forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"))
                ending :: StateT IState (WriterT FC (Parsec Void [Char])) (Either a FC)
ending = (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'))
            in if Bool
isEnd then forall {a}.
StateT IState (WriterT FC (Parsec Void [Char])) (Either a FC)
ending else forall {b}.
StateT IState (WriterT FC (Parsec Void [Char])) (Either FC b)
stars forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}.
StateT IState (WriterT FC (Parsec Void [Char])) (Either a FC)
ending
          case Either FC FC
sepFCE of
            Left FC
starsFC -> PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsTerm ((PTerm
e, forall a. Maybe a
Nothing, FC
starsFC)forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
            Right FC
closeFC ->
              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 (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] forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty forall a. [a] -> [a] -> [a]
++ [FC
starsFC, FC
closeFC] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<) (\(PTerm
_,Maybe (FC, PTerm)
cfclty,FC
sfc) -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty forall a. [a] -> [a] -> [a]
++ [FC
sfc]) [(PTerm, Maybe (FC, PTerm), FC)]
bnds)
                               PunInfo
pun PTerm
e (forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder forall a b. (a, b) -> b
snd Maybe (FC, PTerm)
cfclty) (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 (forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder 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 forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'; forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
e
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  do [(PTerm, FC)]
exprs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (do FC
comma <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                  PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
r, FC
comma))
                FC
closeParenFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')')
                let hilite :: [FC]
hilite = [FC
openParenFC, FC
closeParenFC] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PTerm, FC)]
exprs
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
openParenFC [FC]
hilite PunInfo
TypeOrTerm PTerm
e ([(PTerm, FC)] -> PTerm
mergePairs [(PTerm, FC)]
exprs)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  do FC
starsFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"**"
                PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsTerm [(PTerm
e, forall a. Maybe a
Nothing, FC
starsFC)] FC
openParenFC SyntaxInfo
syn
        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 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")) [forall {t}. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC (Integer -> Const
BI (forall a. Num a => Integer -> a
fromInteger Integer
x)))]
              forall a. a -> [a] -> [a]
: [PTerm]
consts)
    | Bool
otherwise = FC -> PTerm -> PTerm
PConstSugar FC
inFC 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 (forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word8 -> Const
B8 (forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word16 -> Const
B16 (forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word32 -> Const
B32 (forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word64 -> Const
B64 (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 forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"(|"; [PTerm]
alts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','); forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"|)"
             forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess [PTerm]
alts)

{- | Parses a possibly hidden simple expression
@
HSimpleExpr ::=
  '.' SimpleExpr
  | SimpleExpr
  ;
@
-}
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr SyntaxInfo
syn =
  do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'.'
     PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm
PHidden PTerm
e
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
  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 forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"unifyLog"
                  PTerm -> PTerm
PUnifyLog forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
               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 forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"runElab"
                 (PTerm
tm, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [[Char]] -> PTerm
PRunElab FC
fc PTerm
tm (SyntaxInfo -> [[Char]]
syn_namespace SyntaxInfo
syn)
              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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"with"
                [Name]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                forall (m :: * -> *) a. Monad m => a -> m a
return ([[Text]] -> PTerm -> PTerm
PDisamb (forall a b. (a -> b) -> [a] -> [b]
map Name -> [Text]
tons [Name]
ns) PTerm
tm)
               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 (forall a. Show a => a -> [Char]
show Name
n) forall a. a -> [a] -> [a]
: [Text]
s
        tons Name
n = [[Char] -> Text
txt (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 forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"noImplicits")
                     PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                     forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
PNoImplicits PTerm
tm)
                 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 = (forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent forall a b. (a -> b) -> a -> b
$ do
    PTerm
f <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
    (do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"<=="
        Name
ff <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
        forall (m :: * -> *) a. Monad m => a -> m a
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"))))
          forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"matching application expression") forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
      (do [PArg]
args <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do IdrisParser ()
notEndApp; SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
arg SyntaxInfo
syn)
          [PTerm]
wargs <- if SyntaxInfo -> Bool
withAppAllowed SyntaxInfo
syn Bool -> Bool -> Bool
&& Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
                     then forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do IdrisParser ()
notEndApp; forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"|"; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     else forall (m :: * -> *) a. Monad m => a -> m a
return []
          case [PArg]
args of
            [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \FC
fc -> PTerm
f
            [PArg]
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return 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)))
     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 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 forall a. Eq a => a -> a -> Bool
== [Char] -> Name
sUN [Char]
"fromInteger" = forall a. a -> Maybe a
Just PArg
a
    getFromInt (PTerm
_ : [PTerm]
xs) = [PTerm] -> Maybe PArg
getFromInt [PTerm]
xs
    getFromInt [PTerm]
_ = 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
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) PArg
constraintArg SyntaxInfo
syn
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall {t}. t -> PArg' t
pexp PTerm
e)
       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 forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
                     (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                     PTerm
v <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> [FC] -> Name -> PTerm
PRef FC
nfc [FC
nfc] Name
n) (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
                                                          SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                     forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
                     forall (m :: * -> *) a. Monad m => a -> m a
return (forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n PTerm
v Bool
True)
                  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 forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"@{"
                       PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                       forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"}"
                       forall (m :: * -> *) a. Monad m => a -> m a
return (forall {t}. t -> PArg' t
pconst PTerm
e)
                    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 = (forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote forall a b. (a -> b) -> a -> b
$ do
                    forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`("
                    PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn { syn_in_quasiquote :: Int
syn_in_quasiquote = (SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn) forall a. Num a => a -> a -> a
+ Int
1 ,
                                    inPattern :: Bool
inPattern = Bool
False }
                    Maybe PTerm
g <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional forall a b. (a -> b) -> a -> b
$
                           do forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
":"
                              SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
False } -- don't allow antiquotes
                    forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
")"
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe PTerm -> PTerm
PQuasiquote PTerm
e Maybe PTerm
g)
                  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 = (forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnAntiquote forall a b. (a -> b) -> a -> b
$ do
                 forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn forall a. Ord a => a -> a -> Bool
> Int
0)
                 forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"~"
                 PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn { syn_in_quasiquote :: Int
syn_in_quasiquote = SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn forall a. Num a => a -> a -> a
- Int
1 }
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm
PUnquote PTerm
e)
               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 = forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote ((forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
                     forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`{{"
                     (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                     forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"}}"
                     forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Bool -> FC -> PTerm
PQuoteName Name
n Bool
False FC
nfc))
                  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"`{"
                          (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                          forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"}"
                          forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Bool -> FC -> PTerm
PQuoteName Name
n Bool
True FC
nfc)))
                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 ((Either [([Name], SetOrUpdate)] [Name]
fgs, Maybe PTerm
rec), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
            forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"record"
            forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
            Either [([Name], SetOrUpdate)] [Name]
fgs <- IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet
            forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
            Maybe PTerm
rec <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do IdrisParser ()
notEndApp; SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Either [([Name], SetOrUpdate)] [Name]
fgs, Maybe PTerm
rec)
         case Either [([Name], SetOrUpdate)] [Name]
fgs of
              Left [([Name], SetOrUpdate)]
fields ->
                case Maybe PTerm
rec of
                   Maybe PTerm
Nothing ->
                       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 -> 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 ->
                       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 (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc (forall a. [a] -> [a]
reverse [Name]
fields) PTerm
v)

       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 [Name]
ns <- IdrisParser [Name]
fieldGet
                       (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
                           PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                           forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ns, PTerm -> SetOrUpdate
FieldSet PTerm
e))
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"$="
                                PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ns, PTerm -> SetOrUpdate
FieldUpdate PTerm
e)
                    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"field setter"

         fieldGet :: IdrisParser [Name]
         fieldGet :: IdrisParser [Name]
fieldGet = forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName (forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"->")

         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 IdrisParser ([Name], SetOrUpdate)
fieldSet (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
                     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Name]
f <- IdrisParser [Name]
fieldGet
                            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Name]
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 (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 [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)) [forall {t}. t -> PArg' t
pexp PTerm
e, 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))
                  [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) [forall {t}. t -> PArg' t
pexp PTerm
get])),
                   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) [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) [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_" forall a. [a] -> [a] -> [a]
++ Text -> [Char]
str Text
n)
mkType (MN Int
0 Text
n) = Int -> [Char] -> Name
sMN Int
0 ([Char]
"set_" 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 [(RigCount, Name, FC, PTerm)]
cs <- if SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn then SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn else forall (m :: * -> *) a. Monad m => a -> m a
return []
                  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
                  forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc)
               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 forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'\\' forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"lambda expression"
                ((do [(RigCount, Name, FC, PTerm)]
xt <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                     (PTerm
sc, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser PTerm
lambdaTail
                     forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\RigCount
r -> FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc))
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                 (do [(FC, PTerm)]
ps <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (do (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True }))
                                       forall (m :: * -> *) a. Monad m => a -> m a
return (FC
fc, PTerm
e))
                                   (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                     PTerm
sc <- IdrisParser PTerm
lambdaTail
                     forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(FC, PTerm)]
ps) PTerm
sc)))
                  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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"=>" 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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"rewrite"
                     (PTerm
prf, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     Maybe PTerm
giving <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"==>"; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     Maybe Name
using <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"using"
                                           Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                                           forall (m :: * -> *) a. Monad m => a -> m a
return Name
n)
                     forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"in";  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
using PTerm
prf PTerm
sc Maybe PTerm
giving)
                  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 = forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option RigCount
RigW forall a b. (a -> b) -> a -> b
$ do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'1'; forall (m :: * -> *) a. Monad m => a -> m a
return RigCount
Rig1
                       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'0'; 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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                     [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls <- forall a. IdrisParser a -> IdrisParser [a]
indentedBlock (SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding SyntaxInfo
syn)
                     forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"in";  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     forall (m :: * -> *) a. Monad m => a -> m a
return ([(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc))
           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) forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)

let_binding :: SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void [Char]))
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding SyntaxInfo
syn = do RigCount
rc <- forall (m :: * -> *). Parsing m => m RigCount
rigCount
                     (PTerm
pat, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True })
                     PTerm
ty <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
Placeholder (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
                     PTerm
v <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = PTerm -> Bool
isVar PTerm
pat })
                     [(PTerm, PTerm)]
ts <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
                                           forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt SyntaxInfo
syn) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'))
                     forall (m :: * -> *) a. Monad m => a -> m a
return (FC
fc,RigCount
rc,PTerm
pat,PTerm
ty,PTerm
v,[(PTerm, PTerm)]
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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"if"
              (PTerm
c, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"then"
              PTerm
t <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"else"
              PTerm
f <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f))
          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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"quoteGoal"; Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name;
                   forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"by"
                   PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"in"
                   (PTerm
sc, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc PTerm
r Name
n PTerm
sc)
                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 forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"->"
          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 [(RigCount, Name, FC, PTerm)]
xt <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')')
        Plicity
binder <- forall {m :: * -> *} {p}.
(MonadFail m, MonadParsec Void [Char] m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
        PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
        forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
binder { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc)

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

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

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

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

implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
implicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn =
      forall {p}. p -> Static -> SyntaxInfo -> IdrisParser PTerm
autoImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {p}. p -> Static -> SyntaxInfo -> IdrisParser PTerm
defaultImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
          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
       PTerm
x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do Plicity
binder <- forall {m :: * -> *} {p}.
(MonadFail m, MonadParsec Void [Char] m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
           PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
           forall (m :: * -> *) a. Monad m => a -> m a
return (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
binder ([Char] -> Name
sUN [Char]
"__pi_arg") FC
NoFC PTerm
x PTerm
sc))
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
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
       PTerm
x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do Plicity
binder <- forall {m :: * -> *} {p}.
(MonadFail m, MonadParsec Void [Char] m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
           PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
           forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=>"
           forall (m :: * -> *) a. Monad m => a -> m a
return (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
binder ([Char] -> Name
sUN [Char]
"__pi_arg") FC
NoFC PTerm
x PTerm
sc))
              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=>"
                     forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x


pi :: SyntaxInfo -> IdrisParser PTerm
pi :: SyntaxInfo -> IdrisParser PTerm
pi SyntaxInfo
syn =
     do [ArgOpt]
opts <- SyntaxInfo -> IdrisParser [ArgOpt]
piOpts SyntaxInfo
syn
        Static
st   <- IdrisParser Static
static
        [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
explicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'; [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
implicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn)
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> if SyntaxInfo -> Bool
constraintAllowed SyntaxInfo
syn
                then forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPiNoConstraint [ArgOpt]
opts Static
st SyntaxInfo
syn)
                           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
constraintPi [ArgOpt]
opts Static
st SyntaxInfo
syn
                else [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPi [ArgOpt]
opts Static
st SyntaxInfo
syn
  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 =
        forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'.' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. Monad m => a -> m a
return [ArgOpt
InaccessibleArg]
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []
piOpts SyntaxInfo
syn = 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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn)
                     forall (f :: * -> *) a. Alternative f => f a -> f a -> f 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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('
                                [(RigCount, Name, FC, PTerm)]
tys <- 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 (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
                                forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=>"
                                forall (m :: * -> *) a. Monad m => a -> m a
return [(RigCount, Name, FC, PTerm)]
tys)
                  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do PTerm
t <- SyntaxInfo -> IdrisParser PTerm
opExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                                forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"=>"
                                forall (m :: * -> *) a. Monad m => a -> m a
return [(RigCount
RigW, Name
defname, FC
NoFC, PTerm
t)])
                  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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Name
n, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                          PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                          forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
n, FC
fc, PTerm
e))
                forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                       forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
defname, FC
NoFC, PTerm
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 = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do RigCount
rig <- forall (m :: * -> *). Parsing m => m RigCount
rigCount
                                       (Name
x, FC
xfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                                       forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                                       PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                                       forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
rig, Name
x, FC
xfc, PTerm
t))
                             (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [(Name, FC)]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                          forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                          PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
x, FC
xfc) -> (RigCount
RigW, Name
x, FC
xfc, PTerm
t)) [(Name, FC)]
ns)
                   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 = forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do (Name
x, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void [Char])) Name
nameOrPlaceholder
                                 PTerm
t <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
Placeholder (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                                                               SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                                 forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
x, FC
fc, PTerm
t))
                             (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    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 = forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> [Char] -> Name
sMN Int
0 [Char]
"underscore" forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"_"
                           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 [Char]
f (Int
l, Int
c) (Int, Int)
_) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'[')
                  (do (FC [Char]
_ (Int, Int)
_ (Int
l', Int
c')) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']') forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"end of list expression"
                      forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
mkNil ([Char] -> (Int, Int) -> (Int, Int) -> FC
FC [Char]
f (Int
l, Int
c) (Int
l', Int
c'))))
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do (PTerm
x, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression"
                           (do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|') forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"list comprehension"
                               [PDo]
qs <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PDo
do_ SyntaxInfo
syn) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                               forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']'
                               forall (m :: * -> *) a. Monad m => a -> m a
return ([PDo] -> PTerm
PDoBlock (forall a b. (a -> b) -> [a] -> [b]
map PDo -> PDo
addGuard [PDo]
qs forall a. [a] -> [a] -> [a]
++
                                          [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]
"pure"))
                                                       [forall {t}. t -> PArg' t
pexp PTerm
x])]))) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                            (do [(PTerm, FC)]
xs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do FC
commaFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',') forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"list element"
                                               PTerm
elt <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                               forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
elt, FC
commaFC))
                                FC
rbrackFC <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']') forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"end of list expression"
                                forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> FC -> [(PTerm, FC)] -> PTerm
mkList FC
fc FC
rbrackFC ((PTerm
x, ([Char] -> (Int, Int) -> (Int, Int) -> FC
FC [Char]
f (Int
l, Int
c) (Int
l, Int
cforall a. Num a => a -> a -> a
+Int
1))) forall a. a -> [a] -> [a]
: [(PTerm, FC)]
xs))))
                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]
"::")) [forall {t}. t -> PArg' t
pexp PTerm
x, 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) = 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"))
                                              [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 forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"do"
         [PDo] -> PTerm
PDoBlock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser PDo
do_ SyntaxInfo
syn)
      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 -> IdrisParser PDo
do_ SyntaxInfo
syn
     = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                 (Name
i, FC
ifc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                 Maybe PTerm
ty' <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
P.optional (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                                       SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                 forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"="
                 (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
                 -- If there is an explicit type, this can’t be a pattern-matching let, so do not parse alternatives
                 forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
fc RigCount
RigW Name
i FC
ifc (forall a. a -> Maybe a -> a
fromMaybe PTerm
Placeholder Maybe PTerm
ty') PTerm
e)
                          (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
                              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isJust Maybe PTerm
ty') forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"a pattern-matching let may not have an explicit type annotation"
                              [(PTerm, PTerm)]
ts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|')
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
ifc [FC
ifc] Name
i) PTerm
e [(PTerm, PTerm)]
ts)))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"let"
                 PTerm
i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 forall (m :: * -> *). Parsing m => [Char] -> m ()
reservedOp [Char]
"="
                 (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
                 forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc PTerm
i PTerm
e [])
                          (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
                              [(PTerm, PTerm)]
ts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|')
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc PTerm
i PTerm
e [(PTerm, PTerm)]
ts)))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (PTerm
sc, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
[Char] -> m ()
keyword [Char]
"rewrite" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> PDo' t
DoRewrite FC
fc PTerm
sc))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Name
i, FC
ifc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                 forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"<-"
                 (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False });
                 forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
i FC
ifc PTerm
e)
                          (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
                              [(PTerm, PTerm)]
ts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|')
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
ifc [FC
ifc] Name
i) PTerm
e [(PTerm, PTerm)]
ts)))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do PTerm
i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"<-"
                 (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False });
                 forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc PTerm
i PTerm
e [])
                          (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
                              [(PTerm, PTerm)]
ts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|')
                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc PTerm
i PTerm
e [(PTerm, PTerm)]
ts)))
   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> t -> PDo' t
DoExp FC
fc PTerm
e)
   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 PTerm
l <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (PTerm
Placeholder, PTerm
l)
                         (do forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"=>"
                             PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                             forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
l, PTerm
r))

{- | Parses an expression in idiom brackets
@
Idiom ::= '[|' Expr '|]';
@
-}
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom SyntaxInfo
syn
    = do forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"[|"
         (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
         forall (m :: * -> *). Parsing m => [Char] -> m ()
symbol [Char]
"|]"
         forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm
PIdiom FC
fc PTerm
e)
      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 = forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ Const
ty forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
name | ([Char]
name, Const
ty) <- [([Char], Const)]
constants ]
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Double -> Const
Fl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Double
float)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Const
BI forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Integer
natural
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Const
Str forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m [Char]
verbatimStringLiteral
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Const
Str forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m [Char]
stringLiteral
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> Const
Ch forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Char
charLiteral) --Currently ambigous with symbols
       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 = forall (m :: * -> *) a. Parsing m => m a -> m a
token forall a b. (a -> b) -> a -> b
$ do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
"\"\"\""
                                   [Char]
str <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.manyTill forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => [Char] -> m [Char]
string [Char]
"\"\"\"")
                                   [Char]
moreQuotes <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Char
'"'
                                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char]
str forall a. [a] -> [a] -> [a]
++ [Char]
moreQuotes

{- | Parses a static modifier

@
Static ::=
  '%static'
;
@
-}
static :: IdrisParser Static
static :: IdrisParser Static
static =     Static
Static forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). Parsing m => [Char] -> m ()
reserved [Char]
"%static"
         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return Static
Dynamic
         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"], forall a. Maybe a
Nothing, forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ -- FIXME syntax for intro (fresh name)
      do [Name]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','); forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. [Name] -> PTactic' t
Intro [Name]
ns)
  , forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"intros"] forall t. PTactic' t
Intros
  , forall {m :: * -> *} {a} {a} {a} {b}.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs [[Char]
"unfocus"] forall t. PTactic' t
Unfocus
  , ([[Char]
"refine"], forall a. a -> Maybe a
Just TacticArg
ExprTArg, forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$
       do Name
n <- forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          [Bool]
imps <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many IdrisParser Bool
imp
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> [Bool] -> PTactic' t
Refine Name
n [Bool]
imps)
  , ([[Char]
"claim"], forall a. Maybe a
Nothing, \SyntaxInfo
syn ->
       do Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
          PTerm
goal <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> PTactic' t
Claim Name
n PTerm
goal)
  , ([[Char]
"mrefine"], forall a. a -> Maybe a
Just TacticArg
ExprTArg, forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$
       do Name
n <- forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void [Char] f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> PTactic' t
MatchRefine Name
n)
  , forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"rewrite"] forall t. t -> PTactic' t
Rewrite
  , forall {a} {b}.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void [Char])) b)
expressionTactic [[Char]
"equiv"] forall t. t -> PTactic' t
Equiv
  , ([[Char]
"let"], forall a. Maybe a
Nothing, \SyntaxInfo
syn -> -- FIXME syntax for let
       do Name
n <- (forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name)
          (do forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
              PTerm
ty <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
              forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
              PTerm
t <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> t -> PTactic' t
LetTacTy Name
n (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
ty) (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t))
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
                    PTerm
t <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                    IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Name -> t -> PTactic' t
LetTac Name
n (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t)))

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


tactic :: SyntaxInfo -> IdrisParser PTactic
tactic :: SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn = forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ do forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice (forall a b. (a -> b) -> [a] -> [b]
map 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 ]
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'
                 PTactic
t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn;
                 forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';';
                 [PTactic]
ts <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';')
                 forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
t ([PTactic] -> PTactic
mergeSeq [PTactic]
ts)
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Alternative f => f a
empty) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"prover command")
          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) = 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 PTactic
t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn
                    forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                    forall (m :: * -> *) a. Monad m => a -> m a
return PTactic
t