No need to qualify unambiguous names on :p

edwinb · Aug 4, 2012 · c30e6ce · c30e6ce
1 parent d4861b2
commit c30e6ce
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 8 deletions.
diff --git a/idris.cabal b/idris.cabal
@@ -73,7 +73,7 @@ Executable     idris
 
                               Paths_idris
 
-               Build-depends:   base>=4 && <5, parsec, mtl, Cabal, haskeline,
+               Build-depends:   base>=4 && <5, parsec, mtl, Cabal, haskeline<0.7,
                                 containers, process, transformers, filepath, directory,
                                 binary, bytestring, epic>=0.9.3.1, pretty
 

diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs
@@ -7,7 +7,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,
                 Context, initContext, ctxtAlist, uconstraints, next_tvar,
                 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype, 
                 addCasedef, addOperator,
-                lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
+                lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
                 lookupTyEnv, isConName, isFnName,
                 Value(..)) where
 
@@ -697,6 +697,11 @@ addOperator n ty a op uctxt
 
 tfst (a, _, _) = a
 
+lookupNames :: Maybe [String] -> Name -> Context -> [Name]
+lookupNames root n ctxt
+                = let ns = lookupCtxtName root n (definitions ctxt) in
+                      map fst ns
+
 lookupTy :: Maybe [String] -> Name -> Context -> [Type]
 lookupTy root n ctxt 
                 = do def <- lookupCtxt root n (definitions ctxt)

diff --git a/src/Idris/Error.hs b/src/Idris/Error.hs
@@ -11,6 +11,7 @@ import Core.Typecheck
 import Core.Constraints
 
 import System.Console.Haskeline
+import System.Console.Haskeline.MonadException
 import Control.Monad.State
 import System.IO.Error(isUserError, ioeGetErrorString)
 import Data.Char

diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
@@ -224,12 +224,19 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
                          ist <- get
                          let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm
                          iputStrLn (show (delab ist tm'))
-process fn (Prove n) = do prover (lit fn) n
-                          -- recheck totality
-                          i <- get
-                          totcheck (FC "(input)" 0, n)
-                          mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
-                          mapM_ checkDeclTotality (idris_totcheck i)
+process fn (Prove n') 
+     = do ctxt <- getContext
+          ist <- get
+          n <- case lookupNames Nothing n' ctxt of
+                    [x] -> return x
+                    [] -> return n'
+                    ns -> fail $ pshow ist (CantResolveAlts (map show ns)) 
+          prover (lit fn) n
+          -- recheck totality
+          i <- get
+          totcheck (FC "(input)" 0, n)
+          mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
+          mapM_ checkDeclTotality (idris_totcheck i)
 process fn (HNF t)  = do (tm, ty) <- elabVal toplevel False t
                          ctxt <- getContext
                          ist <- get