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

git.iko.soy/Idris-dev

Extension parsing, now deferring checks name is unique

commit71c1a0ec3c3540787ed53b727a7760eb5a03547b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 15 Nov 2011, 16:48 (15 years ago) parent4a1324c

2 files changed+9−7

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−1 src/Idris/Parser.hs+7−6

src/Core/Elaborate.hs+2−1

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

203203movelast n = processTactic' (MoveLast n)

204204

205205defer :: Name -> Elab ()

206−defer n = processTactic' (Defer n)

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

207+ processTactic' (Defer n')

207208

208209instanceArg :: Name -> Elab ()

209210instanceArg n = processTactic' (Instance n)

src/Idris/Parser.hs+7−6

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

333333

334334pSimpleExtExpr :: SyntaxInfo -> IParser PTerm

335335pSimpleExtExpr syn = do i <- getState

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

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

337337 where

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

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

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

342342 _ -> False

343343 simple _ = False

344344

345− valid (Rule _ _ AnySyntax) = True

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

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

348−

349345pNoExtExpr syn =

350346 try (pApp syn)

351347 <|> pSimpleExpr syn

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

355351 <|> pDoBlock syn

356352

357353pExtensions :: 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+

359360

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

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