22556aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix for syntax extension parsing

When building applications, they should be flattened (i.e. take all arguments at once) since we assume that's what the parser does elsewhere.

commit22556aa30aaf0e4b9c4fad2e4f7d45c72c957e25 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 14 Jan 2014, 16:34 (13 years ago) parentc486513

1 file changed+5−1

unifiedsplit

src/Idris/ParseExpr.hs+5−1

@@ -114,7 +114,7 @@ extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm

114114extension syn (Rule ssym ptm _)

115115 = do smap <- mapM extensionSymbol ssym

116116 let ns = mapMaybe id smap

117− return (update ns ptm) -- updated with smap

117+ return (flatten (update ns ptm)) -- updated with smap

118118 where

119119 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

120120 extensionSymbol (Keyword n) = do reserved (show n); return Nothing

@@ -131,6 +131,10 @@ extension syn (Rule ssym ptm _)

131131 dropn n ((x,t) : xs) | n == x = xs

132132 | otherwise = (x,t):dropn n xs

133133

134+ flatten :: PTerm -> PTerm -- flatten application

135+ flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

136+ flatten t = t

137+

134138 updateB :: [(Name, SynMatch)] -> Name -> Name

135139 updateB ns n = case lookup n ns of

136140 Just (SynBind t) -> t