git.iko.soy/Idris-dev
on master help sign in
Fix the broken 'Exact' versions of lookups

Instead of checking there's exactly one result, they must check that one of the (possibly many) results is the exact name they were looking for, since some things may be unqualified and will be returned anyway. Fixes #2271 (again; test for disambig001 and disambig002 added)

commit5b73dcbde118c10aee15e5a05f9fe9841ce937f5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 May 2015, 10:33 (11 years ago) parentad55342
10 files changed+35−11
compare with master
unifiedsplit
idris.cabal+7 src/Idris/Core/Evaluate.hs+3−6 src/Idris/Elab/Term.hs+5−4 test/disambig001/disambig001.idr+12 test/disambig001/expected+1 test/disambig001/run+4 test/reg064/reg064a.idr → test/disambig002/disambig002.idr test/disambig002/expected test/disambig002/run+3 test/reg064/run−1
idris.cabal+7
@@ -380,6 +380,13 @@ Extra-source-files:
380380 test/delab001/expected
381381 test/delab001/input
382382
383+ test/disambig001/run
384+ test/disambig001/*.idr
385+ test/disambig001/expected
386+ test/disambig002/run
387+ test/disambig002/*.idr
388+ test/disambig002/expected
389+
383390 test/dsl001/run
384391 test/dsl001/*.idr
385392 test/dsl001/expected
src/Idris/Core/Evaluate.hs+3−6
@@ -20,6 +20,7 @@ import Control.Applicative hiding (Const)
2020import Control.Monad.State -- not Strict!
2121import qualified Data.Binary as B
2222import Data.Binary hiding (get, put)
23+import Data.Maybe (listToMaybe)
2324
2425import Idris.Core.TT
2526import Idris.Core.CaseTree
@@ -952,9 +953,7 @@ lookupTyName n ctxt = do
952953
953954-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
954955lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
955−lookupTyNameExact n ctxt = case lookupTyName n ctxt of
956− [x] -> Just x
957− _ -> Nothing
956+lookupTyNameExact n ctxt = listToMaybe [ (nm, v) | (nm, v) <- lookupTyName n ctxt, nm == n ]
958957
959958-- | Get the types that match some name
960959lookupTy :: Name -> Context -> [Type]
@@ -962,9 +961,7 @@ lookupTy n ctxt = map snd (lookupTyName n ctxt)
962961
963962-- | Get the single type that matches some name precisely
964963lookupTyExact :: Name -> Context -> Maybe Type
965−lookupTyExact n ctxt = case lookupTy n ctxt of
966− [t] -> Just t
967− _ -> Nothing
964+lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)
968965
969966isConName :: Name -> Context -> Bool
970967isConName n ctxt = isTConName n ctxt || isDConName n ctxt
src/Idris/Elab/Term.hs+5−4
@@ -1378,7 +1378,7 @@ pruneByType env t c as
13781378
13791379pruneByType env (P _ n _) ctxt as
13801380-- if the goal type is polymorphic, keep e
1381− | [] <- lookupTy n ctxt = as
1381+ | Nothing <- lookupTyExact n ctxt = as
13821382 | otherwise
13831383 = let asV = filter (headIs True n) as
13841384 as' = filter (headIs False n) as in
@@ -1388,16 +1388,17 @@ pruneByType env (P _ n _) ctxt as
13881388 _ -> asV
13891389 _ -> as'
13901390 where
1391+ headIs var f (PRef _ f') = typeHead var f f'
13911392 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
13921393 headIs var f (PApp _ f' _) = headIs var f f'
13931394 headIs var f (PPi _ _ _ _ sc) = headIs var f sc
13941395 headIs var f (PHidden t) = headIs var f t
1395− headIs _ _ _ = True -- keep if it's not an application
1396+ headIs var f t = True -- keep if it's not an application
13961397
13971398 typeHead var f f'
13981399 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
1399− case lookupTy f' ctxt of
1400− [ty] -> case unApply (getRetTy ty) of
1400+ case lookupTyExact f' ctxt of
1401+ Just ty -> case unApply (getRetTy ty) of
14011402 (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
14021403 _ -> let ty' = normalise ctxt [] ty in
14031404 case unApply (getRetTy ty') of
test/disambig001/disambig001.idrnew file+12
@@ -0,0 +1,12 @@
1+module Main
2+
3+import Prelude.Monad
4+
5+import System
6+import Effect.System
7+
8+main : IO ()
9+main = do
10+ args <- System.getArgs
11+ putStrLn (concat args)
12+
test/disambig001/expectednew file+1
@@ -0,0 +1 @@
1+./disambig001foobar
test/disambig001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ disambig001.idr -p effects -o disambig001
3+./disambig001 foo bar
4+rm -f disambig001 *.ibc
test/reg064/reg064a.idr → test/disambig002/disambig002.idrrenamed

The content is the same.

test/disambig002/expectednew file

No changes to the content.

test/disambig002/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ disambig002.idr --check
3+rm -f *.ibc
test/reg064/run−1
@@ -1,4 +1,3 @@
11#!/usr/bin/env bash
22idris $@ reg064.idr --check
3−idris $@ reg064a.idr --check
43rm -f *.ibc