71c1a0e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Extension parsing, now deferring checks name is unique

71c1a0eEdwin Brady15 years ago

src/Core/Elaborate.hs+2−1

compare with master

unifiedsplit

@@ -203,7 +203,8 @@ movelast :: Name -> Elab ()

203movelast n = processTactic' (MoveLast n)

204

205defer :: Name -> Elab ()

206+defer n = do n' <- unique_hole n

206−defer n = processTactic' (Defer n)

207+ processTactic' (Defer n')

207

208

208instanceArg :: Name -> Elab ()

209instanceArg :: Name -> Elab ()

209instanceArg n = processTactic' (Instance n)

210instanceArg n = processTactic' (Instance n)

src/Idris/Parser.hs+7−6

@@ -333,7 +333,7 @@ pExtExpr syn = do i <- getState

333

334pSimpleExtExpr :: SyntaxInfo -> IParser PTerm

335pSimpleExtExpr syn = do i <- getState

336− pExtensions syn (filter valid (filter simple (syntax_rules i)))

336+ pExtensions syn (filter simple (syntax_rules i))

337 where

338 simple (Rule (Expr x:xs) _ _) = False

339 simple (Rule (_:xs) _ _) = case (last xs) of

@@ -342,10 +342,6 @@ pSimpleExtExpr syn = do i <- getState

342 _ -> False

343 simple _ = False

344

345− valid (Rule _ _ AnySyntax) = True

346− valid (Rule _ _ PatternSyntax) = inPattern syn

347− valid (Rule _ _ TermSyntax) = not (inPattern syn)

348−

349pNoExtExpr syn =

345pNoExtExpr syn =

350 try (pApp syn)

346 try (pApp syn)

351 <|> pSimpleExpr syn

347 <|> pSimpleExpr syn

@@ -355,7 +351,12 @@ pNoExtExpr syn =

355 <|> pDoBlock syn

351 <|> pDoBlock syn

356

352

357pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

353pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

358−pExtensions syn rules = choice (map (\x -> try (pExt syn x)) rules)

354+pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))

355+ where

356+ valid (Rule _ _ AnySyntax) = True

357+ valid (Rule _ _ PatternSyntax) = inPattern syn

358+ valid (Rule _ _ TermSyntax) = not (inPattern syn)

359+

359

360

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

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

361pExt syn (Rule (s:ssym) ptm _)

362pExt syn (Rule (s:ssym) ptm _)