5047cc5 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

@@ -793,7 +793,7 @@ data PArg' t = PImp { priority :: Int,

793 getTm :: t }

794 deriving (Show, Eq, Functor)

795

796−data ArgOpt = Lazy | HideDisplay

796+data ArgOpt = Lazy | HideDisplay | ErasedArg

797 deriving (Show, Eq)

798

799lazyarg :: PArg' t -> Bool

src/Idris/IBC.hs+2

@@ -1319,11 +1319,13 @@ instance Binary ArgOpt where

1319 = case x of

1320 Lazy -> putWord8 0

1321 HideDisplay -> putWord8 1

1322+ ErasedArg -> putWord8 2

1322 get

1323 get

1323 = do i <- getWord8

1324 = do i <- getWord8

1324 case i of

1325 case i of

1325 0 -> return Lazy

1326 0 -> return Lazy

1326 1 -> return HideDisplay

1327 1 -> return HideDisplay

1328+ 2 -> return ErasedArg

1327 _ -> error "Corrupted binary data for Static"

1329 _ -> error "Corrupted binary data for Static"

1328

1330

1329instance Binary Static where

1331instance Binary Static where

src/Idris/ParseExpr.hs+9−5

@@ -797,13 +797,11 @@ Pi ::=

797@

798 -}

799

800+pi :: SyntaxInfo -> IdrisParser PTerm

800pi :: SyntaxInfo -> IdrisParser PTerm

801pi :: SyntaxInfo -> IdrisParser PTerm

801pi syn =

802pi syn =

802− do opts <- -- if implicitAllowed syn -- laziness is top level only

803+ do opts <- piOpts syn

803− -- then option [] (do lchar '|'; return [Lazy])

804− -- else return []

805− return []

806− st <- static

804+ st <- static

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

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

808 symbol "->"

806 symbol "->"

809 sc <- expr syn

807 sc <- expr syn

@@ -835,6 +833,12 @@ pi syn =

835 else do fail "no implicit arguments allowed here"))

833 else do fail "no implicit arguments allowed here"))

836 <?> "dependent type signature"

834 <?> "dependent type signature"

837

835

836+piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

837+piOpts syn | implicitAllowed syn =

838+ lchar '.' *> return [ErasedArg]

839+ <|> return []

840+piOpts syn = return []

841+

838{- | Parses a type constraint list

842{- | Parses a type constraint list

839

843

840@

844@