be0ab25 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Display totality errors on type check failure

be0ab25Edwin Brady11 years ago

src/Idris/REPL.hs+10−9

compare with master

unifiedsplit

@@ -1620,15 +1620,16 @@ loadInputs inputs toline -- furthest line to read in input source files

1620 let tidata = idris_tyinfodata inew

1621 let patdefs = idris_patdefs inew

1622 ok <- noErrors

1623− when ok $

1623+ if ok then

1624− -- The $!! here prevents a space leak on reloading.

1624+ -- The $!! here prevents a space leak on reloading.

1625− -- This isn't a solution - but it's a temporary stopgap.

1625+ -- This isn't a solution - but it's a temporary stopgap.

1626− -- See issue #2386

1626+ -- See issue #2386

1627− do when (not keepstate) $ putIState $!! ist

1627+ do when (not keepstate) $ putIState $!! ist

1628− ist <- getIState

1628+ ist <- getIState

1629− putIState $!! ist { idris_tyinfodata = tidata,

1629+ putIState $!! ist { idris_tyinfodata = tidata,

1630− idris_patdefs = patdefs }

1630+ idris_patdefs = patdefs }

1631− tryLoad keepstate phase fs

1631+ tryLoad keepstate phase fs

1632+ else warnTotality

1632

1633

1633 ibc (IBC _ _) = True

1634 ibc (IBC _ _) = True

1634 ibc _ = False

1635 ibc _ = False

test/meta002/AgdaStyleReflection.idr+2−1

@@ -71,7 +71,7 @@ implementation Quotable Term Raw where

71 quote Ty = `(Ty)

74−implementation Show Term where

74+partial implementation Show Term where

75 showPrec d (Var k xs) = showCon d "Var" $ showArg k ++ showArg xs

76 showPrec d (Ctor n xs) = showCon d "Ctor" $ showArg n ++ showArg xs

77 showPrec d (TyCtor n xs) = showCon d "TyCtor" $ showArg n ++ showArg xs

@@ -330,3 +330,4 @@ baz = tactic trivial

330-- Local Variables:

331-- idris-load-packages: ("pruviloj")

332-- End:

333+