b0248ea · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Checking syntax declarations; also allow symbols

b0248eaEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+1

compare with master

unifiedsplit

@@ -203,6 +203,7 @@ data Syntax = Rule [SSymbol] PTerm

203 deriving Show

204

205data SSymbol = Keyword Name

206+ | Symbol String

206 | Expr Name

207 | Expr Name

207 deriving Show

208 deriving Show

208

209

src/Idris/Parser.hs+15−1

@@ -157,16 +157,27 @@ pSyntaxRule :: SyntaxInfo -> IParser Syntax

157pSyntaxRule syn

158 = do reserved "syntax"

159 syms <- many1 pSynSym

160+ when (all expr syms) $ fail "No keywords in syntax rule"

161+ let ns = mapMaybe name syms

162+ when (length ns /= length (nub ns))

163+ $ fail "Repeated variable in syntax rule"

160 lchar '='

164 lchar '='

161 tm <- pExpr syn

165 tm <- pExpr syn

162 lchar ';'

166 lchar ';'

163 return (Rule syms tm)

167 return (Rule syms tm)

168+ where

169+ expr (Expr _) = True

170+ expr _ = False

171+ name (Expr n) = Just n

172+ name _ = Nothing

164

173

165pSynSym :: IParser SSymbol

174pSynSym :: IParser SSymbol

166pSynSym = try (do lchar '['; n <- iName; lchar ']'

175pSynSym = try (do lchar '['; n <- iName; lchar ']'

167 return (Expr n))

176 return (Expr n))

168 <|> do n <- iName

177 <|> do n <- iName

169 return (Keyword n)

178 return (Keyword n)

179+ <|> do sym <- strlit

180+ return (Symbol sym)

170

181

171pFunDecl' :: SyntaxInfo -> IParser PDecl

182pFunDecl' :: SyntaxInfo -> IParser PDecl

172pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

183pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

@@ -238,11 +249,14 @@ pExtensions syn rules = choice (map (pExt syn) rules)

238pExt :: SyntaxInfo -> Syntax -> IParser PTerm

249pExt :: SyntaxInfo -> Syntax -> IParser PTerm

239pExt syn (Rule ssym ptm)

250pExt syn (Rule ssym ptm)

240 = do smap <- mapM pSymbol ssym

251 = do smap <- mapM pSymbol ssym

252+ let ns = mapMaybe id smap

241− return (update (mapMaybe id smap) ptm) -- updated with smap

253+ return (update ns ptm) -- updated with smap

242 where

254 where

243 pSymbol (Keyword n) = do reserved (show n); return Nothing

255 pSymbol (Keyword n) = do reserved (show n); return Nothing

244 pSymbol (Expr n) = do tm <- pSimpleExpr syn

256 pSymbol (Expr n) = do tm <- pSimpleExpr syn

245 return $ Just (n, tm)

257 return $ Just (n, tm)

258+ pSymbol (Symbol s) = do symbol s

259+ return Nothing

246 dropn n [] = []

260 dropn n [] = []

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

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

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

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