3b13341 · Idris-dev · git.iko.soy

Makefile+4

compare with master

unifiedsplit

@@ -14,6 +14,10 @@ configure: .PHONY

14test : .PHONY

15 make -C test

16

17+relib: .PHONY

18+ make -C lib clean

19+ make -C lib BINDIR=../dist/build/idris

20+

17linecount : .PHONY

21linecount : .PHONY

18 wc -l src/Idris/*.hs src/Core/*.hs

22 wc -l src/Idris/*.hs src/Core/*.hs

19

23

idris.cabal+1−1

@@ -61,7 +61,7 @@ Executable idris

61 Idris.Delaborate, Idris.Primitives, Idris.Imports,

62 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

63 Idris.Coverage, Idris.IBC, Idris.Unlit,

64− Idris.DataOpts, Idris.Transforms,

64+ Idris.DataOpts, Idris.Transforms,

65

66 Paths_idris

67

lib/prelude/strings.idr+1−1

@@ -21,7 +21,7 @@ strTail' x p = prim__strTail x

21

22strM : (x : String) -> StrM x

23strM x with (choose (not (x == "")))

24− strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p))

24+ strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)

25 strM x | (Right p) = believe_me StrNil

26

27unpack : String -> List Char

src/Core/TT.hs+2

@@ -40,6 +40,7 @@ instance Show FC where

40data Err = Msg String

41 | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify

42 | NotInjective Term Term Term

43+ | CantResolve Term

43 | IncompleteTerm Term

44 | IncompleteTerm Term

44 | UniverseError

45 | UniverseError

45 | ProgramLineComment

46 | ProgramLineComment

@@ -48,6 +49,7 @@ data Err = Msg String

48

49

49score :: Err -> Int

50score :: Err -> Int

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

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

52+score (CantResolve _) = 20

51score _ = 0

53score _ = 0

52

54

53instance Show Err where

55instance Show Err where

src/Idris/Delaborate.hs+1

@@ -70,6 +70,7 @@ pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)

70pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

71 " when unifying " ++ show (delab i x) ++ " and " ++

72 show (delab i y)

73+pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

73pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

74pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

74pshow i UniverseError = "Universe inconsistency"

75pshow i UniverseError = "Universe inconsistency"

75pshow i ProgramLineComment = "Program line next to comment"

76pshow i ProgramLineComment = "Program line next to comment"

src/Idris/ElabTerm.hs+1−1

@@ -341,7 +341,7 @@ resolveTC depth fn ist

341 boundVar (P Bound _ _) = True

342 boundVar _ = False

343

344− blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

344+ blunderbuss t [] = lift $ tfail $ CantResolve t

345 blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

346 (blunderbuss t ns)

347 | otherwise = blunderbuss t ns

src/Idris/Parser.hs−1

@@ -313,7 +313,6 @@ pDecl syn = do notEndBlock

313 <|> pDirective

314 <|> try (do reserved "import"

315 fp <- identifier

316− lchar ';'

317 fail "imports must be at the top of file")

316 fail "imports must be at the top of file")

318

317

319pFunDecl :: SyntaxInfo -> IParser [PDecl]

318pFunDecl :: SyntaxInfo -> IParser [PDecl]

tutorial/typesfuns.tex+1−1

@@ -38,7 +38,7 @@ in each module each have their own namespace, as we will discuss in Section

38\ref{sect:namespaces}) and a

39collection of declarations and definitions. Each definition must have a type

40declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).

41−Indentation is significant --- a new declaration begins at the same leve

41+Indentation is significant --- a new declaration begins at the same level

42of indentation as the preceding declaration. Alternatively, declarations

43may be terminated with a semicolon.

44