739e0b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some error handling

commit739e0b537be0b8aaeb77e9a478eb4579b5dcbed3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 10 Oct 2011, 09:18 (15 years ago) parent22b4dc4

7 files changed+25−7

compare with master

unifiedsplit

miniidris.cabal+1−1 src/Core/ProofState.hs+1 src/Core/Unify.hs+3 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabDecls.hs+6−4 src/Idris/Error.hs+10 src/Idris/REPL.hs+3−1

miniidris.cabal+1−1

@@ -23,7 +23,7 @@ Executable miniidris

2323 Core.CaseTree,

2424

2525 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

26− Idris.REPLParser, Idris.ElabDecls

26+ Idris.REPLParser, Idris.ElabDecls, Idris.Error

2727

2828 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

2929 containers, process, transformers

src/Core/ProofState.hs+1

@@ -227,6 +227,7 @@ complete_fill ctxt env (Bind x (Guess ty val) sc) =

227227 let (uh, uns) = unified ps

228228 put (ps { unified = (uh, uns ++ ns) })

229229 return $ Bind x (Guess ty val) sc

230+complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

230231

231232solve :: RunTactic

232233solve ctxt env (Bind x (Guess ty val) sc)

src/Core/Unify.hs+3

@@ -11,6 +11,9 @@ import Control.Monad

1111-- which can be filled in, by matching one term's normal form against another.

1212-- Returns a list of hole names paired with the term which solves them.

1313

14+-- FIXME! Needs to be cleverer: when we solve a variable, fill it in and normalise

15+-- to help the rest of the unification

16+

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

1518unify ctxt env x y

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

src/Idris/AbsSyntax.hs+1−1

@@ -257,7 +257,7 @@ implicitise ist tm

257257 = do (decls, a, ns) <- get

258258 let isn = concatMap (namesIn ist) (map snd is)

259259 let esn = concatMap (namesIn ist) es

260− put (decls, a, nub (ns ++ ((isn ++ esn) \\ env)))

260+ put (decls, a, nub (ns ++ ((isn ++ esn) \\ (env ++ decls))))

261261 imps env (PPi Imp n ty sc)

262262 = do imps env ty

263263 (impdecls, a, ns) <- get

src/Idris/ElabDecls.hs+6−4

@@ -3,6 +3,7 @@

33module Idris.ElabDecls where

55import Idris.AbsSyntax

6+import Idris.Error

78import Core.TT

89import Core.Elaborate

@@ -63,6 +64,7 @@ elabVal tm

6364 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

6465 (build False (infTerm tm))

6566 let vtm = getInferTerm tm'

67+ iLOG (show vtm)

6668 tclift $ recheck ctxt [] vtm

6769

6870elabClause :: PClause -> Idris (Term, Term)

@@ -94,7 +96,7 @@ elabClause (PClause _ lhs rhs)

9496 psolve tm = return ()

9597

9698elabDecl :: PDecl -> Idris ()

97−elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (show e))

99+elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (report e))

98100

99101elabDecl' (PFix _ _) = return () -- nothing to elaborate

100102elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

@@ -149,11 +151,11 @@ elab pattern tm = do elab' tm

149151 elab' sc

150152 solve

151153 elab' (PApp (PRef f) imps args)

152− = try (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

154+ = try (do apply_elab f (map toElab imps ++ map (Just . elab') args)

155+ solve)

156+ (do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)

153157 solve

154158 elabArgs ns (map snd imps ++ args))

155− (do apply_elab f (map toElab imps ++ map (Just . elab') args)

156− solve)

157159 elab' (PApp f [] [arg])

158160 = do simple_app (elab' f) (elab' arg)

159161 solve

src/Idris/Error.hsnew file+10

@@ -0,0 +1,10 @@

1+module Idris.Error where

3+import Idris.AbsSyntax

4+import System.IO.Error

6+report :: IOError -> String

7+report e

8+ | isUserError e = ioeGetErrorString e

9+ | otherwise = show e

10+

src/Idris/REPL.hs+3−1

@@ -5,6 +5,7 @@ module Idris.REPL where

55import Idris.AbsSyntax

66import Idris.REPLParser

77import Idris.ElabDecls

8+import Idris.Error

910import Core.Evaluate

1011import Core.ProofShell

@@ -31,7 +32,8 @@ processInput cmd

3132 return True

3233 Right Quit -> do iputStrLn "Bye bye"

3334 return False

34− Right cmd -> do process cmd

35+ Right cmd -> do idrisCatch (process cmd)

36+ (\e -> iputStrLn (report e))

3537 return True

3638

3739process :: Command -> Idris ()