bfd5b51 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

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

12* 'mutual' blocks added

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

14 elaborating their definitions

15+ - allows inductive-recursive definitions

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

17+ - i.e. "magic" with

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

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

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

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

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

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

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

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

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

26* Fixed nested parameters blocks

29* Fixed nested parameters blocks

27* Improve efficiency of elaborator by only normalising when necessary

30* Improve efficiency of elaborator by only normalising when necessary

31+* Better compilation of case trees

28

32

29New in 0.9.5:

33New in 0.9.5:

30-------------

34-------------

src/Core/TT.hs+2−1

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

60 | ProgramLineComment

61 | Inaccessible Name

62 | NonCollapsiblePostulate Name

63+ | AlreadyDefined Name

63 | At FC Err

64 | At FC Err

64 deriving Eq

65 deriving Eq

65

66

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

78 size UniverseError = 1

79 size UniverseError = 1

79 size ProgramLineComment = 1

80 size ProgramLineComment = 1

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

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

81− size (Inaccessible _) = 1

82+ size _ = 1

82

83

83score :: Err -> Int

84score :: Err -> Int

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

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

src/Idris/Delaborate.hs+1

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

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

105pshow i (NonCollapsiblePostulate n)

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

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

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

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

108

109

109showSc i [] = ""

110showSc i [] = ""

src/Idris/ElabDecls.hs+7−1

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

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

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

300 do ctxt <- getContext

301− -- Check n actually exists

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

302 let tys = lookupTy Nothing n ctxt

303+ checkUndefined n ctxt

303 unless (length tys > 1) $ do

304 unless (length tys > 1) $ do

304 fty <- case tys of

305 fty <- case tys of

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

306 [] -> -- 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

421 [] -> return ()

422 [] -> return ()

422 return ()

423 return ()

423 where

424 where

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

426+ [] -> return ()

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

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

429+

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

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

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

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

426 (vs, x', y')

432 (vs, x', y')

test/reg007/A.lidrnew file+5

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

1+> module A

2+

3+> n : Nat

4+> n = ?lala

5+

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

2+

3+> import A

4+

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

6+> isSame = refl

7+

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