fa6f5fa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Refactored constraint syntax to use less lookahead

fa6f5faAhmad Salim Al-Sibahi13 years ago

src/Idris/Parser.hs+41−43

compare with master

unifiedsplit

@@ -1613,50 +1613,48 @@ Pi ::=

1613 | '{' 'static' '}' Expr' '->' Expr

1614 ;

1615 -}

1616+

1617+pi :: SyntaxInfo -> IdrisParser PTerm

1616pi syn =

1618pi syn =

1617− try (do lazy <- if implicitAllowed syn -- laziness is top level only

1619+ do lazy <- if implicitAllowed syn -- laziness is top level only

1618− then option False (do lchar '|'; return True)

1620+ then option False (do lchar '|'; return True)

1619− else return False

1621+ else return False

1620− st <- static

1622+ st <- static

1621− lchar '('; xt <- typeDeclList syn; lchar ')'

1623+ (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

1622− doc <- option "" (docComment '^')

1624+ doc <- option "" (docComment '^')

1623− symbol "->"

1625+ symbol "->"

1624− sc <- expr syn

1626+ sc <- expr syn

1625− return (bindList (PPi (Exp lazy st doc)) xt sc))

1627+ return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do

1626− <|> try (if implicitAllowed syn

1627− then do lazy <- option False (do lchar '|'

1628− return True)

1629− st <- static

1630− lchar '{'

1628+ lchar '{'

1631− xt <- typeDeclList syn

1629+ (do reserved "auto"

1632− lchar '}'

1630+ when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

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

1631+ xt <- typeDeclList syn

1640− lchar '}'

1632+ lchar '}'

1641− symbol "->"

1633+ symbol "->"

1642− sc <- expr syn

1634+ sc <- expr syn

1643− return (bindList (PPi

1635+ return (bindList (PPi

1644− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))

1636+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do

1645− <|> try (do lchar '{'

1637+ reserved "default"

1646− reserved "default"

1638+ when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

1647− script <- simpleExpr syn

1639+ script <- simpleExpr syn

1648− xt <- typeDeclList syn

1640+ xt <- typeDeclList syn

1649− lchar '}'

1641+ lchar '}'

1650− symbol "->"

1642+ symbol "->"

1651− sc <- expr syn

1643+ sc <- expr syn

1652− return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

1644+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do

1653− <|> do lchar '{'

1654− reserved "static"

1645+ reserved "static"

1655− lchar '}'

1646+ lchar '}'

1656− t <- expr' syn

1647+ t <- expr' syn

1657− symbol "->"

1648+ symbol "->"

1658− sc <- expr syn

1649+ sc <- expr syn

1659− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)

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"))

1660 <?> "dependent type signature"

1658 <?> "dependent type signature"

1661

1659

1662{- | Parses a type constraint list

1660{- | Parses a type constraint list