5b73dcb · Idris-dev · git.iko.soy

idris.cabal+7

compare with master

unifiedsplit

@@ -380,6 +380,13 @@ Extra-source-files:

380 test/delab001/expected

381 test/delab001/input

382

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+

383 test/dsl001/run

390 test/dsl001/run

384 test/dsl001/*.idr

391 test/dsl001/*.idr

385 test/dsl001/expected

392 test/dsl001/expected

src/Idris/Core/Evaluate.hs+3−6

@@ -20,6 +20,7 @@ import Control.Applicative hiding (Const)

20import Control.Monad.State -- not Strict!

21import qualified Data.Binary as B

22import Data.Binary hiding (get, put)

23+import Data.Maybe (listToMaybe)

23

24

24import Idris.Core.TT

25import Idris.Core.TT

25import Idris.Core.CaseTree

26import Idris.Core.CaseTree

@@ -952,9 +953,7 @@ lookupTyName n ctxt = do

952

953

953-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

954-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.

954lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)

955lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)

955−lookupTyNameExact n ctxt = case lookupTyName n ctxt of

956+lookupTyNameExact n ctxt = listToMaybe [ (nm, v) | (nm, v) <- lookupTyName n ctxt, nm == n ]

956− [x] -> Just x

957− _ -> Nothing

958

957

959-- | Get the types that match some name

958-- | Get the types that match some name

960lookupTy :: Name -> Context -> [Type]

959lookupTy :: Name -> Context -> [Type]

@@ -962,9 +961,7 @@ lookupTy n ctxt = map snd (lookupTyName n ctxt)

962

961

963-- | Get the single type that matches some name precisely

962-- | Get the single type that matches some name precisely

964lookupTyExact :: Name -> Context -> Maybe Type

963lookupTyExact :: Name -> Context -> Maybe Type

965−lookupTyExact n ctxt = case lookupTy n ctxt of

964+lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)

966− [t] -> Just t

967− _ -> Nothing

968

965

969isConName :: Name -> Context -> Bool

966isConName :: Name -> Context -> Bool

970isConName n ctxt = isTConName n ctxt || isDConName n ctxt

967isConName n ctxt = isTConName n ctxt || isDConName n ctxt

src/Idris/Elab/Term.hs+5−4

@@ -1378,7 +1378,7 @@ pruneByType env t c as

1378

1379pruneByType env (P _ n _) ctxt as

1380-- if the goal type is polymorphic, keep e

1381− | [] <- lookupTy n ctxt = as

1381+ | Nothing <- lookupTyExact n ctxt = as

1382 | otherwise

1383 = let asV = filter (headIs True n) as

1384 as' = filter (headIs False n) as in

@@ -1388,16 +1388,17 @@ pruneByType env (P _ n _) ctxt as

1388 _ -> asV

1389 _ -> as'

1390 where

1391+ headIs var f (PRef _ f') = typeHead var f f'

1391 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1392 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1392 headIs var f (PApp _ f' _) = headIs var f f'

1393 headIs var f (PApp _ f' _) = headIs var f f'

1393 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1394 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1394 headIs var f (PHidden t) = headIs var f t

1395 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

1396

1397

1397 typeHead var f f'

1398 typeHead var f f'

1398 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1399 = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $

1399− case lookupTy f' ctxt of

1400+ case lookupTyExact f' ctxt of

1400− [ty] -> case unApply (getRetTy ty) of

1401+ Just ty -> case unApply (getRetTy ty) of

1401 (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f

1402 (P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f

1402 _ -> let ty' = normalise ctxt [] ty in

1403 _ -> let ty' = normalise ctxt [] ty in

1403 case unApply (getRetTy ty') of

1404 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 @@

1#!/usr/bin/env bash

2idris $@ reg064.idr --check

3−idris $@ reg064a.idr --check

4rm -f *.ibc

3rm -f *.ibc