git.iko.soy/Idris-dev
on master help sign in
No need to qualify unambiguous names on :p
commitc30e6ced4c746e738e41686e7609c3eb2ac6d3a1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Aug 2012, 14:53 (14 years ago) parentd4861b2
4 files changed+21−8
compare with master
unifiedsplit
idris.cabal+1−1 src/Core/Evaluate.hs+6−1 src/Idris/Error.hs+1 src/Idris/REPL.hs+13−6
idris.cabal+1−1
@@ -73,7 +73,7 @@ Executable idris
7373
7474 Paths_idris
7575
76− Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
76+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline<0.7,
7777 containers, process, transformers, filepath, directory,
7878 binary, bytestring, epic>=0.9.3.1, pretty
7979
src/Core/Evaluate.hs+6−1
@@ -7,7 +7,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,
77 Context, initContext, ctxtAlist, uconstraints, next_tvar,
88 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,
99 addCasedef, addOperator,
10− lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
10+ lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
1111 lookupTyEnv, isConName, isFnName,
1212 Value(..)) where
1313
@@ -697,6 +697,11 @@ addOperator n ty a op uctxt
697697
698698tfst (a, _, _) = a
699699
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+
700705lookupTy :: Maybe [String] -> Name -> Context -> [Type]
701706lookupTy root n ctxt
702707 = do def <- lookupCtxt root n (definitions ctxt)
src/Idris/Error.hs+1
@@ -11,6 +11,7 @@ import Core.Typecheck
1111import Core.Constraints
1212
1313import System.Console.Haskeline
14+import System.Console.Haskeline.MonadException
1415import Control.Monad.State
1516import System.IO.Error(isUserError, ioeGetErrorString)
1617import Data.Char
src/Idris/REPL.hs+13−6
@@ -224,12 +224,19 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
224224 ist <- get
225225 let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
226226 iputStrLn (show (delab ist tm'))
227−process fn (Prove n) = do prover (lit fn) n
228− -- recheck totality
229− i <- get
230− totcheck (FC "(input)" 0, n)
231− mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
232− mapM_ checkDeclTotality (idris_totcheck i)
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
235+ -- recheck totality
236+ i <- get
237+ totcheck (FC "(input)" 0, n)
238+ mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
239+ mapM_ checkDeclTotality (idris_totcheck i)
233240process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
234241 ctxt <- getContext
235242 ist <- get