Permalink
Browse files

No need to qualify unambiguous names on :p

  • Loading branch information...
1 parent d4861b2 commit c30e6ced4c746e738e41686e7609c3eb2ac6d3a1 @edwinb edwinb committed Aug 4, 2012
Showing with 21 additions and 8 deletions.
  1. +1 −1 idris.cabal
  2. +6 −1 src/Core/Evaluate.hs
  3. +1 −0 src/Idris/Error.hs
  4. +13 −6 src/Idris/REPL.hs
View
2 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
View
7 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)
View
1 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
View
19 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

0 comments on commit c30e6ce

Please sign in to comment.