1a87674 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improved type-directed name disambiguation

1a87674Edwin Brady14 years ago

CHANGELOG+6

compare with master

unifiedsplit

@@ -5,6 +5,12 @@ User visible changes:

6* Renamed EFF to EFFECT in Effect package

7* Experimental Java backend

8+* Tab completion in REPL

10+Internal changes:

11+

12+* Improved name disambiguation

13+* Various unification and totality checking bug fixes

9New in 0.9.7:

15New in 0.9.7:

10-------------

16-------------

src/Core/Elaborate.hs+25−16

@@ -516,9 +516,9 @@ try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

516try' t1 t2 proofSearch

517 = do s <- get

518 ps <- get_probs

519− case prunStateT ps t1 s of

519+ case prunStateT 999999 False ps t1 s of

520− OK (v, s') -> do put s'

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

521− return v

521+ return v

522 Error e1 -> if recoverableErr e1 then

523 do case runStateT t2 s of

524 OK (v, s') -> do put s'; return v

@@ -539,42 +539,51 @@ tryWhen False a b = a

539

540-- Try a selection of tactics. Exactly one must work, all others must fail

541tryAll :: [(Elab' aux a, String)] -> Elab' aux a

542−tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)

542+tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)

543 where

544 cantResolve :: Elab' aux a

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

546

547 tryAll' :: [Elab' aux a] -> -- successes

548+ Int -> -- most problems

548 (Elab' aux a, Int) -> -- smallest failure

549 (Elab' aux a, Int) -> -- smallest failure

549 [Elab' aux a] -> -- still to try

550 [Elab' aux a] -> -- still to try

550 Elab' aux a

551 Elab' aux a

551− tryAll' [res] _ [] = res

552+ tryAll' [res] pmax _ [] = res

552− tryAll' (_:_) _ [] = cantResolve

553+ tryAll' (_:_) pmax _ [] = cantResolve

553− tryAll' [] (f, _) [] = f

554+ tryAll' [] pmax (f, _) [] = f

554− tryAll' cs f (x:xs)

555+ tryAll' cs pmax f (x:xs)

555 = do s <- get

556 = do s <- get

556 ps <- get_probs

557 ps <- get_probs

557− case prunStateT ps x s of

558+ case prunStateT pmax True ps x s of

558− OK (v, s') -> tryAll' ((do put s'

559+ OK ((v, newps), s') ->

559− return v):cs) f xs

560+ do let cs' = if (newps < pmax)

561+ then [do put s'; return v]

562+ else (do put s'; return v) : cs

563+ tryAll' cs' newps f xs

560 Error err -> do put s

564 Error err -> do put s

561 if (score err) < 100

565 if (score err) < 100

562− then tryAll' cs (better err f) xs

566+ then tryAll' cs pmax (better err f) xs

563− else tryAll' [] (better err f) xs -- give up

567+ else tryAll' [] pmax (better err f) xs -- give up

564

568

565

569

566 better err (f, i) = let s = score err in

570 better err (f, i) = let s = score err in

567 if (s >= i) then (lift (tfail err), s)

571 if (s >= i) then (lift (tfail err), s)

568 else (f, i)

572 else (f, i)

569

573

570−prunStateT ps x s

574+prunStateT pmax zok ps x s

571 = case runStateT x s of

575 = case runStateT x s of

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

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

573− if (length (problems p) > length ps)

577+ let newps = length (problems p) - length ps

578+ newpmax = if newps < 0 then 0 else newps in

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

574 then case reverse (problems p) of

580 then case reverse (problems p) of

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

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

576− else OK (v, s')

582+ else OK ((v, newpmax), s')

577 Error e -> Error e

583 Error e -> Error e

578

584

585+qshow :: Fails -> String

586+qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

587+

579dumpprobs [] = ""

588dumpprobs [] = ""

580dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

589dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es

src/Core/Unify.hs+10

@@ -95,6 +95,10 @@ unify ctxt env topx topy dont holes =

95 = unifyFail topx topy

96 un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

97 = unifyFail topx topy

98+ un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

99+ = unifyFail topx topy

100+ un' fn names topx@(P (TCon _ _) x _) topy@(Constant _)

101+ = unifyFail topx topy

98 un' fn bnames tx@(P _ x _) ty@(P _ y _)

102 un' fn bnames tx@(P _ x _) ty@(P _ y _)

99 | (x,y) `elem` bnames || x == y = do sc 1; return []

103 | (x,y) `elem` bnames || x == y = do sc 1; return []

100 | injective tx && not (holeIn env y || y `elem` holes)

104 | injective tx && not (holeIn env y || y `elem` holes)

@@ -310,8 +314,14 @@ unify ctxt env topx topy dont holes =

310 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

314 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _)

311 | x == y = True

315 | x == y = True

312 | otherwise = False

316 | otherwise = False

317+ recoverable (Constant _) (P (DCon _ _) y _) = False

318+ recoverable (P (DCon _ _) x _) (Constant _) = False

319+ recoverable (Constant _) (P (TCon _ _) y _) = False

320+ recoverable (P (TCon _ _) x _) (Constant _) = False

313 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

321 recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

314 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

322 recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

323+ recoverable p@(Constant _) (App f a) = recoverable p f

324+ recoverable (App f a) p@(Constant _) = recoverable f p

315 recoverable p@(P _ n _) (App f a) = recoverable p f

325 recoverable p@(P _ n _) (App f a) = recoverable p f

316-- recoverable (App f a) p@(P _ _ _) = recoverable f p

326-- recoverable (App f a) p@(P _ _ _) = recoverable f p

317 recoverable (App f a) (App f' a')

327 recoverable (App f a) (App f' a')

test/reg014/expectednew file

No changes to the content.

test/reg014/reg014.idrnew file+12

@@ -0,0 +1,12 @@

1+module reg014

3+Matrix : Type -> Nat -> Nat -> Type

4+Matrix a n m = Vect (Vect a m) n

6+transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

7+transpose ((x:: []) :: []) = [[x]]

8+transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])

9+transpose (x :: y :: xs)

10+ = let tx = transpose [x] in

11+ let ux = transpose (y :: xs) in zipWith (++) tx ux

12+

test/reg014/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg014.idr --check

3+rm -f *.ibc

test/test020/test020a.idr−1

@@ -16,4 +16,3 @@ foo xs = reverse xs

16main : IO ()

17main = print (foo [1,2,3])

19−