@@ -54,14 +54,22 @@ fullExpr syn = do x <- expr syn
5454 return $ debindApp syn (desugar syn i x)
5555
5656
57−{- |Parses an expression
57+{- | Parses an expression
5858@
59− Expr ::= Expr';
59+ Expr ::= Pi
6060@
61−-}
61+ -}
6262expr :: SyntaxInfo -> IdrisParser PTerm
63−expr syn = do i <- get
64− buildExpressionParser (table (idris_infixes i)) (expr' syn)
63+expr = pi
64+
65+{- | Parses an expression with possible operator applied
66+@
67+ OpExpr ::= {- Expression Parser with Operators based on Expr' -};
68+@
69+-}
70+opExpr :: SyntaxInfo -> IdrisParser PTerm
71+opExpr syn = do i <- get
72+ buildExpressionParser (table (idris_infixes i)) (expr' syn)
6573
6674{- | Parses either an internally defined expression or
6775 a user-defined one
@@ -70,16 +78,10 @@ Expr' ::= "External (User-defined) Syntax"
7078 | InternalExpr;
7179@
7280 -}
73−expr' syn = doexpr' syn
74−-- = do l <- restOfLine
75−-- f <- getFC
76−-- e <- trace (show (f, l)) $ doexpr' syn
77−-- return e
78−
79−doexpr' :: SyntaxInfo -> IdrisParser PTerm
80−doexpr' syn = try (externalExpr syn)
81− <|> internalExpr syn
82− <?> "expression"
81+expr' :: SyntaxInfo -> IdrisParser PTerm
82+expr' syn = try (externalExpr syn)
83+ <|> internalExpr syn
84+ <?> "expression"
8385
8486{- | Parses a user-defined expression -}
8587externalExpr :: SyntaxInfo -> IdrisParser PTerm
@@ -197,7 +199,6 @@ InternalExpr ::=
197199 | QuoteGoal
198200 | Let
199201 | RewriteTerm
200− | Pi
201202 | CaseExpr
202203 | DoBlock
203204 | App
@@ -214,7 +215,6 @@ internalExpr syn =
214215 <|> quoteGoal syn
215216 <|> let_ syn
216217 <|> rewriteTerm syn
217− <|> try (pi syn)
218218 <|> doBlock syn
219219 <|> caseExpr syn
220220 <|> app syn
@@ -363,7 +363,7 @@ bracketed' syn =
363363 return (PDPair fc TypeOrTerm (PRef fc ln) lty r))
364364 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
365365 -- No prefix operators! (bit of a hack here...)
366− if (o == "-" || o == "!")
366+ if (o == "-" || o == "!")
367367 then fail "minus not allowed in section"
368368 else return $ PLam (sMN 1000 "ARG") Placeholder
369369 (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),
@@ -754,11 +754,16 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;
754754{- | Parses a dependent type signature
755755
756756@
757−Pi ::=
758− '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
759− | '|'? Static? '{' TypeDeclList '}' '->' Expr
760− | '{' 'auto' TypeDeclList '}' '->' Expr
761− | '{' 'default' TypeDeclList '}' '->' Expr
757+Pi ::= PiOpts Static? Pi'
758+@
759+
760+@
761+Pi' ::=
762+ OpExpr ('->' Pi)?
763+ | '(' TypeDeclList ')' '->' Pi
764+ | '{' TypeDeclList '}' '->' Pi
765+ | '{' 'auto' TypeDeclList '}' '->' Pi
766+ | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
762767 ;
763768@
764769 -}
@@ -767,37 +772,44 @@ pi :: SyntaxInfo -> IdrisParser PTerm
767772pi syn =
768773 do opts <- piOpts syn
769774 st <- static
770− (do try (lchar '('); xt <- typeDeclList syn; lchar ')'
775+ (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
771776 symbol "->"
772777 sc <- expr syn
773778 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do
774− lchar '{'
775− (do reserved "auto"
779+ (do try (lchar '{' *> reserved "auto")
776780 when (st == Static) $ fail "auto type constraints can not be lazy or static"
777781 xt <- typeDeclList syn
778782 lchar '}'
779783 symbol "->"
780784 sc <- expr syn
781785 return (bindList (PPi
782− (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))
783− <|> (do
784− reserved "default"
786+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc)) <|> (do
787+ try (lchar '{' *> reserved "default")
785788 when (st == Static) $ fail "default tactic constraints can not be lazy or static"
786789 script <- simpleExpr syn
787790 xt <- typeDeclList syn
788791 lchar '}'
789792 symbol "->"
790793 sc <- expr syn
791− return (bindList (PPi (TacImp [] Dynamic script)) xt sc))
794+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))
792795 <|> (if implicitAllowed syn then do
793− xt <- typeDeclList syn
794− lchar '}'
796+ xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')
795797 symbol "->"
796798 sc <- expr syn
797799 return (bindList (PPi (Imp opts st False)) xt sc)
798800 else do fail "no implicit arguments allowed here"))
801+ <|> (do x <- opExpr syn
802+ (do symbol "->"
803+ sc <- expr syn
804+ return (PPi (Exp opts st False) (sMN 0 "__pi_arg") x sc))
805+ <|> return x)
799806 <?> "dependent type signature"
800807
808+{- | Parses Possible Options for Pi Expressions
809+@
810+ PiOpts ::= '.'?
811+@
812+-}
801813piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
802814piOpts syn | implicitAllowed syn =
803815 lchar '.' *> return [InaccessibleArg]
@@ -1079,7 +1091,7 @@ Static ::=
10791091@
10801092-}
10811093static :: IdrisParser Static
1082−static = do lchar '['; reserved "static"; lchar ']'; return Static
1094+static = do reserved "[static]"; return Static
10831095 <|> return Dynamic
10841096 <?> "static modifier"
10851097