b645699 · Idris-dev · git.iko.soy

samples/interp.idr+1−1

compare with master

unifiedsplit

@@ -77,7 +77,7 @@ test : Int;

77test = interp [] eProg 2 2;

78

79testFac : Int;

80−testFac = interp [] eFac 4;

80+testFac = interp [] eFac 5;

81

82main : IO ();

83main = do { print testFac;

src/Idris/Error.hs+10

@@ -5,11 +5,21 @@ import Idris.Delaborate

5

6import Core.TT

7import Core.Typecheck

8+import Core.Constraints

8

9

9import Control.Monad.State

10import Control.Monad.State

10import System.IO.Error

11import System.IO.Error

11import Data.Char

12import Data.Char

12

13

14+iucheck :: Idris ()

15+iucheck = do tit <- typeInType

16+ when (not tit) $

17+ do ist <- get

18+ idrisCatch (tclift $ ucheck (idris_constraints ist))

19+ (\e -> do let msg = report e

20+ setErrLine (getErrLine msg)

21+ iputStrLn msg)

22+

13report :: IOError -> String

23report :: IOError -> String

14report e

24report e

15 | isUserError e = ioeGetErrorString e

25 | isUserError e = ioeGetErrorString e

src/Idris/Parser.hs+5−2

@@ -88,8 +88,11 @@ loadSource f = do iLOG ("Reading " ++ f)

88 mapM_ (elabDecl toplevel) ds

89 iLOG ("Finished " ++ f)

90 let ibc = dropExtension f ++ ".ibc"

91+ iucheck

92+ ok <- noErrors

93+ when ok $

91− idrisCatch (do writeIBC f ibc; clearIBC)

94+ idrisCatch (do writeIBC f ibc; clearIBC)

92− (\c -> return ()) -- failure is harmless

95+ (\c -> return ()) -- failure is harmless

93 return ()

96 return ()

94 where

97 where

95 namespaces [] ds = ds

98 namespaces [] ds = ds

src/Idris/REPL.hs−9

@@ -43,15 +43,6 @@ repl orig mods

43 Just mods -> repl orig mods

44 Nothing -> return ()

45

46−iucheck :: Idris ()

47−iucheck = do tit <- typeInType

48− when (not tit) $

49− do ist <- get

50− idrisCatch (tclift $ ucheck (idris_constraints ist))

51− (\e -> do let msg = report e

52− setErrLine (getErrLine msg)

53− iputStrLn msg)

54−

55mkPrompt [] = "Idris"

46mkPrompt [] = "Idris"

56mkPrompt [x] = "*" ++ dropExtension x

47mkPrompt [x] = "*" ++ dropExtension x

57mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

48mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

src/Main.hs−1

@@ -55,7 +55,6 @@ runIdris opts =

55 when runrepl $ iputStrLn banner

56 ist <- get

57 mods <- mapM loadModule inputs

58− iucheck

59 ok <- noErrors

58 ok <- noErrors

60 when ok $ case output of

59 when ok $ case output of

61 [] -> return ()

60 [] -> return ()

test/test002/expectednew file+1

@@ -0,0 +1 @@

1+test002.idr:7:Universe inconsistency

test/test002/runnew file+3

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

1+#!/bin/bash

2+idris test002.idr --check --noprelude

3+

test/test002/test002.idrnew file+29

@@ -0,0 +1,29 @@

1+myid : a -> a;

2+myid x = x;

3+

4+idid : (a : Set) -> a -> a;

5+idid = myid ![myid];

6+

7+app : (a -> b) -> a -> b;

8+app f x = f x;

9+

10+foo : a -> b -> c -> d -> e -> e;

11+foo a b c d e = e;

12+

13+doapp : a -> a;

14+doapp x = app myid x;

15+

16+{-

17+

18+id : (b : Set k) -> b -> b : Set l, k < l

19+

20+foo = id ((a : Set k) -> a -> a) id

21+ Set m, k < m

22+

23+So we have k < m, k < l, m <= k

24+

25+ when converting Set m against Set n, we must have m <= n

26+ if we can reach m from n, we have an inconsistency

27+

28+

29+ -}