c30e6ce · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -73,7 +73,7 @@ Executable idris

73

74 Paths_idris

75

76− Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

76+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline<0.7,

77 containers, process, transformers, filepath, directory,

78 binary, bytestring, epic>=0.9.3.1, pretty

79

src/Core/Evaluate.hs+6−1

@@ -7,7 +7,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

9 addCasedef, addOperator,

10− lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

10+ lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11 lookupTyEnv, isConName, isFnName,

12 Value(..)) where

13

@@ -697,6 +697,11 @@ addOperator n ty a op uctxt

697

698tfst (a, _, _) = a

699

700+lookupNames :: Maybe [String] -> Name -> Context -> [Name]

701+lookupNames root n ctxt

702+ = let ns = lookupCtxtName root n (definitions ctxt) in

703+ map fst ns

704+

700lookupTy :: Maybe [String] -> Name -> Context -> [Type]

705lookupTy :: Maybe [String] -> Name -> Context -> [Type]

701lookupTy root n ctxt

706lookupTy root n ctxt

702 = do def <- lookupCtxt root n (definitions ctxt)

707 = do def <- lookupCtxt root n (definitions ctxt)

src/Idris/Error.hs+1

@@ -11,6 +11,7 @@ import Core.Typecheck

11import Core.Constraints

12

13import System.Console.Haskeline

14+import System.Console.Haskeline.MonadException

14import Control.Monad.State

15import Control.Monad.State

15import System.IO.Error(isUserError, ioeGetErrorString)

16import System.IO.Error(isUserError, ioeGetErrorString)

16import Data.Char

17import Data.Char

src/Idris/REPL.hs+13−6

@@ -224,12 +224,19 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

224 ist <- get

225 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm

226 iputStrLn (show (delab ist tm'))

227−process fn (Prove n) = do prover (lit fn) n

227+process fn (Prove n')

228+ = do ctxt <- getContext

229+ ist <- get

230+ n <- case lookupNames Nothing n' ctxt of

231+ [x] -> return x

232+ [] -> return n'

233+ ns -> fail $ pshow ist (CantResolveAlts (map show ns))

234+ prover (lit fn) n

228− -- recheck totality

235+ -- recheck totality

229− i <- get

236+ i <- get

230− totcheck (FC "(input)" 0, n)

237+ totcheck (FC "(input)" 0, n)

231− mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

238+ mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

232− mapM_ checkDeclTotality (idris_totcheck i)

239+ mapM_ checkDeclTotality (idris_totcheck i)

233process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

240process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

234 ctxt <- getContext

241 ctxt <- getContext

235 ist <- get

242 ist <- get