6eaf933 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Disambiguation tweak

6eaf933Edwin Brady11 years ago

src/Idris/Core/Elaborate.hs+29−17

compare with master

unifiedsplit

@@ -863,7 +863,7 @@ try' t1 t2 proofSearch

863 ps <- get_probs

864 ulog <- getUnifyLog

865 ivs <- get_instances

866− case prunStateT 999999 False ps t1 s of

866+ case prunStateT 999999 False ps Nothing t1 s of

867 OK ((v, _, _), s') -> do put s'

868 return $! v

869 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

@@ -906,8 +906,11 @@ tryWhen False a b = a

906-- Bool says whether it's okay to create new unification problems. If set

907-- to False, then the whole tactic fails if there are any new problems

908tryAll :: [(Elab' aux a, Name)] -> Elab' aux a

909−tryAll [(x, _)] = x

909+tryAll = tryAll' True

910+

911+tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a

912+tryAll' _ [(x, _)] = x

910−tryAll xs = tryAll' [] 999999 xs

913+tryAll' constrok xs = doAll [] 999999 xs

911 where

914 where

912 cantResolve :: Elab' aux a

915 cantResolve :: Elab' aux a

913 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

916 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

@@ -915,44 +918,53 @@ tryAll xs = tryAll' [] 999999 xs

915 noneValid :: Elab' aux a

918 noneValid :: Elab' aux a

916 noneValid = lift $ tfail $ NoValidAlts (map snd xs)

919 noneValid = lift $ tfail $ NoValidAlts (map snd xs)

917

920

918− tryAll' :: [Elab' aux a] -> -- successes

921+ doAll :: [Elab' aux a] -> -- successes

919− Int -> -- most problems

922+ Int -> -- most problems

920− [(Elab' aux a, Name)] -> -- still to try

923+ [(Elab' aux a, Name)] -> -- still to try

921− Elab' aux a

924+ Elab' aux a

922− tryAll' [res] pmax [] = res

925+ doAll [res] pmax [] = res

923− tryAll' (_:_) pmax [] = cantResolve

926+ doAll (_:_) pmax [] = cantResolve

924− tryAll' [] pmax [] = noneValid

927+ doAll [] pmax [] = noneValid

925− tryAll' cs pmax ((x, msg):xs)

928+ doAll cs pmax ((x, msg):xs)

926 = do s <- get

929 = do s <- get

927 ps <- get_probs

930 ps <- get_probs

931+ ivs <- get_instances

928− case prunStateT pmax True ps x s of

932+ case prunStateT pmax True ps (if constrok then Nothing

933+ else Just ivs) x s of

929 OK ((v, newps, probs), s') ->

934 OK ((v, newps, probs), s') ->

930 do let cs' = if (newps < pmax)

935 do let cs' = if (newps < pmax)

931 then [do put s'; return $! v]

936 then [do put s'; return $! v]

932 else (do put s'; return $! v) : cs

937 else (do put s'; return $! v) : cs

933− tryAll' cs' newps xs

938+ doAll cs' newps xs

934 Error err -> do put s

939 Error err -> do put s

935− tryAll' cs pmax xs

940+ doAll cs pmax xs

936

941

937−-- Run an elaborator, and fail if any problems are introduced

942+-- Run an elaborator, and fail if any problems or constraints are introduced

938prunStateT

943prunStateT

939 :: Int

944 :: Int

940 -> Bool

945 -> Bool

941 -> [a]

946 -> [a]

947+ -> Maybe [b] -- constraints left, if we're interested

942 -> Control.Monad.State.Strict.StateT

948 -> Control.Monad.State.Strict.StateT

943 (ElabState t) TC t1

949 (ElabState t) TC t1

944 -> ElabState t

950 -> ElabState t

945 -> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)

951 -> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)

946−prunStateT pmax zok ps x s

952+prunStateT pmax zok ps ivs x s

947 = case runStateT x s of

953 = case runStateT x s of

948 OK (v, s'@(ES (p, _) _ _)) ->

954 OK (v, s'@(ES (p, _) _ _)) ->

949 let newps = length (problems p) - length ps

955 let newps = length (problems p) - length ps

956+ ibad = badInstances (instances p) ivs

950 newpmax = if newps < 0 then 0 else newps in

957 newpmax = if newps < 0 then 0 else newps in

951 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

958 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

952 then case reverse (problems p) of

959 then case reverse (problems p) of

953 ((_,_,_,_,e,_,_):_) -> Error e

960 ((_,_,_,_,e,_,_):_) -> Error e

961+ else if ibad

962+ then Error (InternalMsg "Constraint introduced in disambiguation")

954− else OK ((v, newpmax, problems p), s')

963+ else OK ((v, newpmax, problems p), s')

955 Error e -> Error e

964 Error e -> Error e

965+ where

966+ badInstances _ Nothing = False

967+ badInstances inow (Just ithen) = length inow > length ithen

956

968

957debugElaborator :: [ErrorReportPart] -> Elab' aux a

969debugElaborator :: [ErrorReportPart] -> Elab' aux a

958debugElaborator msg = do ps <- fmap proof get

970debugElaborator msg = do ps <- fmap proof get

src/Idris/Elab/Term.hs+2−2

@@ -464,8 +464,8 @@ elab ist info emode opts fn tm

464 case as'' of

465 [x] -> elab' ina fc x

466 _ -> do hds <- mapM showHd as''

467− tryAll (zip (map (elab' ina fc) as'')

467+ tryAll' False (zip (map (elab' ina fc) as'')

468− hds))

468+ hds))

469 where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])

470 | l == txt "Delay" = showHd (getTm arg)

471 showHd (PApp _ (PRef _ _ n) _) = return n

src/Idris/Interactive.hs+5−1

@@ -400,10 +400,14 @@ makeLemma fn updatefile l n

400 = n : guessImps ist ctxt sc

401 | isClass ist ty

402 = n : guessImps ist ctxt sc

403− | TType _ <- ty = n : guessImps ist ctxt sc

403+ | paramty ty = n : guessImps ist ctxt sc

404 | ignoreName n = n : guessImps ist ctxt sc

405 | otherwise = guessImps ist ctxt sc

406 guessImps ist ctxt _ = []

407+

408+ paramty (TType _) = True

409+ paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc

410+ paramty _ = False

407

411

408 -- TMP HACK unusable name so don't lift

412 -- TMP HACK unusable name so don't lift

409 ignoreName n = case show n of

413 ignoreName n = case show n of

test/interactive010/expected+4−7

@@ -1,15 +1,12 @@

1Prelude.List.(++) : List a -> List a -> List a

2Prelude.Strings.(++) : String -> String -> String

3−Prelude.Classes./ Double

3+a is not an implicit argument of Prelude.Classes./

4− Prelude.Classes.Double implementation of Prelude.Classes.Fractional : (__pi_arg : Double) →

5− (__pi_arg3 : Double) →

6− Double

7Usage is :doc <functionname>

4Usage is :doc <functionname>

8Usage is :wc <functionname>

5Usage is :wc <functionname>

9Usage is :printdef <functionname>

6Usage is :printdef <functionname>

10−pat {a504} : Type u. pat {__class505} : Prelude.Classes.Fractional {a504}. Prelude.Classes./ {a504} {__class505}

7+pat {ty504} : Type u. pat {__class505} : Prelude.Classes.Fractional {ty504}. Prelude.Classes./ {ty504} {__class505}

12− : pty {a504} : Type u. pty {__class505} : Prelude.Classes.Fractional {a504}. {a504} -> {a504} -> {a504}

9+ : pty {ty504} : Type u. pty {__class505} : Prelude.Classes.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

13(input):1:1: error: expected: ":",

10(input):1:1: error: expected: ":",

14 dependent type signature,

11 dependent type signature,

15 end of input

12 end of input

@@ -20,4 +17,4 @@ pat {a504} : Type u. pat {__class505} : Prelude.Classes.Fractional {a504}. Prelu

20 end of input

17 end of input

21++<EOF>

18++<EOF>

22^

19^

23−Can't resolve type class Fractional a

20+Can't resolve type class Fractional ty