bfd5b51 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make sure names are not defined more than once

Fixes issue #124

commitbfd5b51fc865abc4d5263af023265d14e3fffc1a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 19 Dec 2012, 13:24 (14 years ago) parent496cf41

8 files changed+35−2

compare with master

unifiedsplit

CHANGELOG+4 src/Core/TT.hs+2−1 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+7−1 test/reg007/A.lidr+5 test/reg007/expected+1 test/reg007/reg007.lidr+12 test/reg007/run+3

CHANGELOG+4

@@ -12,6 +12,9 @@ User visible changes:

1212* 'mutual' blocks added

1313 - effect is to elaborate all types of declarations in the block before

1414 elaborating their definitions

15+ - allows inductive-recursive definitions

16+* Expression inspected by 'with' clause now abstracted from the goal

17+ - i.e. "magic" with

1518* Implicit arguments will be added automatically only if their initial

1619 letter is lower case, or they are in a using declaration

1720* Added documentation comments (Haddock style) and ':doc' REPL command

@@ -25,6 +28,7 @@ Internal changes:

2528* Separate inlining methods at compile-time and run-time

2629* Fixed nested parameters blocks

2730* Improve efficiency of elaborator by only normalising when necessary

31+* Better compilation of case trees

2832

2933New in 0.9.5:

3034-------------

src/Core/TT.hs+2−1

@@ -60,6 +60,7 @@ data Err = Msg String

6060 | ProgramLineComment

6161 | Inaccessible Name

6262 | NonCollapsiblePostulate Name

63+ | AlreadyDefined Name

6364 | At FC Err

6465 deriving Eq

6566

@@ -78,7 +79,7 @@ instance Sized Err where

7879 size UniverseError = 1

7980 size ProgramLineComment = 1

8081 size (At fc err) = size fc + size err

81− size (Inaccessible _) = 1

82+ size _ = 1

8283

8384score :: Err -> Int

8485score (CantUnify _ _ _ m _ s) = s + score m

src/Idris/Delaborate.hs+1

@@ -104,6 +104,7 @@ pshow i ProgramLineComment = "Program line next to comment"

104104pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

105105pshow i (NonCollapsiblePostulate n)

106106 = "The return type of postulate " ++ show n ++ " is not collapsible"

107+pshow i (AlreadyDefined n) = show n ++ " is already defined"

107108pshow i (At f e) = show f ++ ":" ++ pshow i e

108109

109110showSc i [] = ""

src/Idris/ElabDecls.hs+7−1

@@ -298,8 +298,9 @@ elabCon info syn tn codata (doc, n, t_in, fc)

298298elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

299299elabClauses info fc opts n_in cs = let n = liftname info n_in in

300300 do ctxt <- getContext

301− -- Check n actually exists

301+ -- Check n actually exists, with no definition yet

302302 let tys = lookupTy Nothing n ctxt

303+ checkUndefined n ctxt

303304 unless (length tys > 1) $ do

304305 fty <- case tys of

305306 [] -> -- TODO: turn into a CAF if there's no arguments

@@ -421,6 +422,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

421422 [] -> return ()

422423 return ()

423424 where

425+ checkUndefined n ctxt = case lookupDef Nothing n ctxt of

426+ [] -> return ()

427+ [TyDecl _ _] -> return ()

428+ _ -> tclift $ tfail (At fc (AlreadyDefined n))

429+

424430 debind (Right (x, y)) = let (vs, x') = depat [] x

425431 (_, y') = depat [] y in

426432 (vs, x', y')

test/reg007/A.lidrnew file+5

@@ -0,0 +1,5 @@

1+> module A

3+> n : Nat

4+> n = ?lala

test/reg007/expectednew file+1

@@ -0,0 +1 @@

1+reg007.lidr:8:A.n is already defined

test/reg007/reg007.lidrnew file+12

@@ -0,0 +1,12 @@

1+> module B

3+> import A

5+> isSame : A.n = A.lala

6+> isSame = refl

8+> A.n = O -- This is where it's at!

9+> A.lala = S O

10+

11+> hurrah : O = S O

12+> hurrah = isSame

test/reg007/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --check $@ reg007.lidr

3+rm -f *.ibc