f9fb363 · Idris-dev · git.iko.soy

src/Core/ProofState.hs+4−4

compare with master

unifiedsplit

@@ -133,7 +133,7 @@ goal h tm = g [] tm where

133 | otherwise

134 = gb env b `mplus` g ((n, b):env) sc

135 g env (App f a) = g env f `mplus` g env a

136− g env t = Error "Can't find hole"

136+ g env t = fail "Can't find hole"

137

138 gb env (Let t v) = g env t `mplus` g env v

139 gb env (Guess t v) = g env t `mplus` g env v

@@ -323,10 +323,10 @@ processTactic QED ps = case holes ps of

323 (tm', ty') <- recheck (context ps) [] tm

324 return (ps { done = True, pterm = tm' },

325 "Proof complete: " ++ showEnv [] tm')

326− _ -> Error "Still holes to fill."

326+ _ -> fail "Still holes to fill."

327processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

328processTactic Undo ps = case previous ps of

329− Nothing -> Error "Nothing to undo."

329+ Nothing -> fail "Nothing to undo."

330 Just pold -> return (pold, "")

331processTactic EndUnify ps = let (h, ns) = unified ps

332 tm' = updateSolved ns (pterm ps) in

@@ -344,7 +344,7 @@ processTactic EndUnify ps = let (h, ns) = unified ps

344 updateSolved xs t = t

345processTactic t ps

346 = case holes ps of

347− [] -> Error "Nothing to fill in."

347+ [] -> fail "Nothing to fill in."

348 (h:_) -> do let n = nextname ps

349 ps' <- execStateT (process t h) ps

350 return (ps' { previous = Just ps, plog = "" }, plog ps')

src/Core/TT.hs+14−4

@@ -23,13 +23,20 @@ data Option = SetInSet

23 | CheckConv

24 deriving Eq

25

26+data Err = Msg String

27+ | CantUnify Term Term

28+ deriving Eq

29+

30+instance Show Err where

31+ show (Msg s) = s

32+

26data TC a = OK a

33data TC a = OK a

27− | Error String -- TMP! Make this an informative data structure

34+ | Error Err

28 deriving (Eq, Functor)

35 deriving (Eq, Functor)

29

36

30instance Show a => Show (TC a) where

37instance Show a => Show (TC a) where

31 show (OK x) = show x

38 show (OK x) = show x

32− show (Error str) = "Error: " ++ str

39+ show (Error str) = "Error: " ++ (show str)

33

40

34-- at some point, this instance should also carry type checking options

41-- at some point, this instance should also carry type checking options

35-- (e.g. Set:Set)

42-- (e.g. Set:Set)

@@ -39,10 +46,13 @@ instance Monad TC where

39 x >>= k = case x of

46 x >>= k = case x of

40 OK v -> k v

47 OK v -> k v

41 Error e -> Error e

48 Error e -> Error e

42− fail = Error

49+ fail e = Error (Msg e)

50+

51+tfail :: Err -> TC a

52+tfail e = Error e

43

53

44instance MonadPlus TC where

54instance MonadPlus TC where

45− mzero = Error "Unknown error"

55+ mzero = fail "Unknown error"

46 (OK x) `mplus` _ = OK x

56 (OK x) `mplus` _ = OK x

47 _ `mplus` (OK y) = OK y

57 _ `mplus` (OK y) = OK y

48 err `mplus` _ = err

58 err `mplus` _ = err

src/Core/Unify.hs+4−7

@@ -14,13 +14,10 @@ import Debug.Trace

14-- to help the rest of the unification

15

16unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

17−unify ctxt env x y

17+unify ctxt env topx topy

18− = --case un' [] x y of -- try without normalising first, for speed

19− -- OK v -> return v

20− -- _ ->

21− case un' [] (normalise ctxt env x) (normalise ctxt env y) of

18+ = case un' [] (normalise ctxt env topx) (normalise ctxt env topy) of

22− OK v -> return v

19+ OK v -> return v

23− _ -> fail $ "Can't unify " ++ showEnv env x ++ " and " ++ showEnv env y

20+ _ -> tfail $ CantUnify topx topy

24 where

21 where

25 un' bnames (P Bound x _) (P Bound y _)

22 un' bnames (P Bound x _) (P Bound y _)

26 | (x,y) `elem` bnames = return []

23 | (x,y) `elem` bnames = return []

src/Idris/AbsSyntax.hs−14

@@ -45,11 +45,6 @@ updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )

45iputStrLn :: String -> Idris ()

46iputStrLn = lift.putStrLn

47

48−tclift :: Show a => TC a -> Idris a

49−tclift tc = case tc of

50− OK v -> return v

51− err -> fail (show err)

52−

53setLogLevel :: Int -> Idris ()

48setLogLevel :: Int -> Idris ()

54setLogLevel l = do i <- get

49setLogLevel l = do i <- get

55 let opts = idris_options i

50 let opts = idris_options i

@@ -70,15 +65,6 @@ logLvl l str = do i <- get

70iLOG :: String -> Idris ()

65iLOG :: String -> Idris ()

71iLOG = logLvl 1

66iLOG = logLvl 1

72

67

73−-- Taken from the library source code - for ghc 6.12/7 compatibility

74−liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->

75− StateT s m a -> (e -> StateT s m a) -> StateT s m a

76−liftCatch catchError m h =

77− StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s

78−

79−idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

80−idrisCatch op handler = liftCatch catch op handler

81−

82-- Commands in the REPL

68-- Commands in the REPL

83

69

84data Command = Quit | Help | Eval PTerm

70data Command = Quit | Help | Eval PTerm

src/Idris/Error.hs+26

@@ -1,6 +1,12 @@

1module Idris.Error where

2

3import Idris.AbsSyntax

4+import Idris.Delaborate

5+

6+import Core.TT

7+import Core.Typecheck

8+

9+import Control.Monad.State

4import System.IO.Error

10import System.IO.Error

5

11

6report :: IOError -> String

12report :: IOError -> String

@@ -8,3 +14,23 @@ report e

8 | isUserError e = ioeGetErrorString e

14 | isUserError e = ioeGetErrorString e

9 | otherwise = show e

15 | otherwise = show e

10

16

17+-- Taken from the library source code - for ghc 6.12/7 compatibility

18+liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->

19+ StateT s m a -> (e -> StateT s m a) -> StateT s m a

20+liftCatch catchError m h =

21+ StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s

22+

23+idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

24+idrisCatch op handler = liftCatch catch op handler

25+

26+pshow :: IState -> Err -> String

27+pshow i (Msg s) = s

28+pshow i (CantUnify x y) = "Can't unify " ++ show (delab i x) ++

29+ " with " ++ show (delab i y)

30+

31+tclift :: Show a => TC a -> Idris a

32+tclift tc = case tc of

33+ OK v -> return v

34+ Error err -> do i <- get

35+ fail (pshow i err)

36+