Don't write .ibc on error; add new test
commitb6456999e336c2ed895ce75b19ac6be88b9ee0b8
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateFri 9 Dec 2011, 07:54 (15 years ago)
parent215856d
samples/interp.idr+1−1
@@ -77,7 +77,7 @@ test : Int;
7777test = interp [] eProg 2 2;
7878
7979testFac : Int;
80−testFac = interp [] eFac 4;
80+testFac = interp [] eFac 5;
8181
8282main : IO ();
8383main = do { print testFac;
src/Idris/Error.hs+10
@@ -5,11 +5,21 @@ import Idris.Delaborate
55
66import Core.TT
77import Core.Typecheck
8+import Core.Constraints
89
910import Control.Monad.State
1011import System.IO.Error
1112import Data.Char
1213
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+
1323report :: IOError -> String
1424report e
1525 | isUserError e = ioeGetErrorString e
src/Idris/Parser.hs+5−2
@@ -88,8 +88,11 @@ loadSource f = do iLOG ("Reading " ++ f)
8888 mapM_ (elabDecl toplevel) ds
8989 iLOG ("Finished " ++ f)
9090 let ibc = dropExtension f ++ ".ibc"
91− idrisCatch (do writeIBC f ibc; clearIBC)
92− (\c -> return ()) -- failure is harmless
91+ iucheck
92+ ok <- noErrors
93+ when ok $
94+ idrisCatch (do writeIBC f ibc; clearIBC)
95+ (\c -> return ()) -- failure is harmless
9396 return ()
9497 where
9598 namespaces [] ds = ds
src/Idris/REPL.hs−9
@@ -43,15 +43,6 @@ repl orig mods
4343 Just mods -> repl orig mods
4444 Nothing -> return ()
4545
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−
5546mkPrompt [] = "Idris"
5647mkPrompt [x] = "*" ++ dropExtension x
5748mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs
src/Main.hs−1
@@ -55,7 +55,6 @@ runIdris opts =
5555 when runrepl $ iputStrLn banner
5656 ist <- get
5757 mods <- mapM loadModule inputs
58− iucheck
5958 ok <- noErrors
6059 when ok $ case output of
6160 [] -> 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+ -}