@@ -1613,50 +1613,48 @@ Pi ::=
16131613 | '{' 'static' '}' Expr' '->' Expr
16141614 ;
16151615 -}
1616+
1617+pi :: SyntaxInfo -> IdrisParser PTerm
16161618pi syn =
1617− try (do lazy <- if implicitAllowed syn -- laziness is top level only
1618− then option False (do lchar '|'; return True)
1619− else return False
1620− st <- static
1621− lchar '('; xt <- typeDeclList syn; lchar ')'
1622− doc <- option "" (docComment '^')
1623− symbol "->"
1624− sc <- expr syn
1625− return (bindList (PPi (Exp lazy st doc)) xt sc))
1626− <|> try (if implicitAllowed syn
1627− then do lazy <- option False (do lchar '|'
1628− return True)
1629− st <- static
1630− lchar '{'
1631− xt <- typeDeclList syn
1632− lchar '}'
1633− symbol "->"
1634− sc <- expr syn
1635− return (bindList (PPi (Imp lazy st "")) xt sc)
1636− else fail "no implicit arguments allowed here")
1637− <|> try (do lchar '{'
1638− reserved "auto"
1639− xt <- typeDeclList syn
1640− lchar '}'
1641− symbol "->"
1642− sc <- expr syn
1643− return (bindList (PPi
1644− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
1645− <|> try (do lchar '{'
1646− reserved "default"
1647− script <- simpleExpr syn
1648− xt <- typeDeclList syn
1649− lchar '}'
1650− symbol "->"
1651− sc <- expr syn
1652− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
1653− <|> do lchar '{'
1654− reserved "static"
1655− lchar '}'
1656− t <- expr' syn
1657− symbol "->"
1658− sc <- expr syn
1659− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
1619+ do lazy <- if implicitAllowed syn -- laziness is top level only
1620+ then option False (do lchar '|'; return True)
1621+ else return False
1622+ st <- static
1623+ (do try(lchar '('); xt <- typeDeclList syn; lchar ')'
1624+ doc <- option "" (docComment '^')
1625+ symbol "->"
1626+ sc <- expr syn
1627+ return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do
1628+ lchar '{'
1629+ (do reserved "auto"
1630+ when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"
1631+ xt <- typeDeclList syn
1632+ lchar '}'
1633+ symbol "->"
1634+ sc <- expr syn
1635+ return (bindList (PPi
1636+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do
1637+ reserved "default"
1638+ when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"
1639+ script <- simpleExpr syn
1640+ xt <- typeDeclList syn
1641+ lchar '}'
1642+ symbol "->"
1643+ sc <- expr syn
1644+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do
1645+ reserved "static"
1646+ lchar '}'
1647+ t <- expr' syn
1648+ symbol "->"
1649+ sc <- expr syn
1650+ return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (
1651+ if implicitAllowed syn then do
1652+ xt <- typeDeclList syn
1653+ lchar '}'
1654+ symbol "->"
1655+ sc <- expr syn
1656+ return (bindList (PPi (Imp lazy st "")) xt sc)
1657+ else do fail "no implicit arguments allowed here"))
16601658 <?> "dependent type signature"
16611659
16621660{- | Parses a type constraint list