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

git.iko.soy/Idris-dev

Add ErasedArg to PiOpts.

commit5047cc5b748a24331de6221143ec430899127b18 authorMatus Tejiscak <ziman@functor.sk> dateTue 11 Feb 2014, 11:04 (13 years ago) parentfe0e037

3 files changed+12−6

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/IBC.hs+2 src/Idris/ParseExpr.hs+9−5

src/Idris/AbsSyntaxTree.hs+1−1

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

793793 getTm :: t }

794794 deriving (Show, Eq, Functor)

795795

796−data ArgOpt = Lazy | HideDisplay

796+data ArgOpt = Lazy | HideDisplay | ErasedArg

797797 deriving (Show, Eq)

798798

799799lazyarg :: PArg' t -> Bool

src/Idris/IBC.hs+2

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

13191319 = case x of

13201320 Lazy -> putWord8 0

13211321 HideDisplay -> putWord8 1

1322+ ErasedArg -> putWord8 2

13221323 get

13231324 = do i <- getWord8

13241325 case i of

13251326 0 -> return Lazy

13261327 1 -> return HideDisplay

1328+ 2 -> return ErasedArg

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

13281330

13291331instance Binary Static where

src/Idris/ParseExpr.hs+9−5

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

797797@

798798 -}

799799

800+pi :: SyntaxInfo -> IdrisParser PTerm

800801pi :: SyntaxInfo -> IdrisParser PTerm

801802pi syn =

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

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

804− -- else return []

805− return []

806− st <- static

803+ do opts <- piOpts syn

804+ st <- static

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

808806 symbol "->"

809807 sc <- expr syn

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

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

836834 <?> "dependent type signature"

837835

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

837+piOpts syn | implicitAllowed syn =

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

839+ <|> return []

840+piOpts syn = return []

841+

838842{- | Parses a type constraint list

839843

840844@