From c30e6ced4c746e738e41686e7609c3eb2ac6d3a1 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 4 Aug 2012 14:53:53 +0100
Subject: [PATCH] No need to qualify unambiguous names on :p

---
 idris.cabal          |  2 +-
 src/Core/Evaluate.hs |  7 ++++++-
 src/Idris/Error.hs   |  1 +
 src/Idris/REPL.hs    | 19 +++++++++++++------
 4 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/idris.cabal b/idris.cabal
index 758a0276a7..5d22775fdb 100644
--- 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
index b75816bd08..5d16094ace 100644
--- 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
index c625f9ec11..587457bdc7 100644
--- 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
index c7ff1bc1fc..bfbdd2ccbe 100644
--- 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