728adb7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix a unification bug

Sometimes when revisiting unsolved unification problems, solutions which depend on other solutions arise, so we can't take the shortcut of instantiating everything at once (which doesn't really speed things up anyway...)

commit728adb7ea45437b6b7a1e0a1b019339b47e2395e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 5 Jul 2016, 13:52 (10 years ago) parent2e3b18b

8 files changed+39−4

compare with master

unifiedsplit

CHANGELOG.md+3 idris.cabal+3 src/Idris/Core/ProofState.hs+3−1 src/Idris/Elab/Clause.hs+3−1 src/Idris/Elab/Term.hs+5−2 test/interfaces006/expected test/interfaces006/interfaces006.idr+19 test/interfaces006/run+3

CHANGELOG.md+3

@@ -20,6 +20,9 @@

2020 correct st = record { score->correct $= (+1),

2121 score->attempted $= (+1) } st

2222 ```

23+

24+## Library updates

25+

2326* The File Effect has been updated to take into account changes in

2427 `Prelude.File` and to provide a 'better' API.

2528

idris.cabal+3

@@ -580,6 +580,9 @@ Extra-source-files:

580580 test/interfaces005/*.idr

581581 test/interfaces005/run

582582 test/interfaces005/expected

583+ test/interfaces006/*.idr

584+ test/interfaces006/run

585+ test/interfaces006/expected

583586

584587 test/io001/run

585588 test/io001/*.idr

src/Idris/Core/ProofState.hs+3−1

@@ -1058,7 +1058,7 @@ processTactic (ComputeLet n) ps

10581058 (getProofTerm (pterm ps)) }, "")

10591059processTactic UnifyProblems ps

10601060 = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))

1061− pterm' = updateSolved ns' (pterm ps)

1061+ pterm' = orderUpdateSolved ns' (pterm ps)

10621062 traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $

10631063 return (ps { pterm = pterm', solved = Nothing, problems = probs',

10641064 previous = Just ps, plog = "",

@@ -1067,6 +1067,8 @@ processTactic UnifyProblems ps

10671067 dotted = filter (notIn ns') (dotted ps),

10681068 holes = holes ps \\ (map fst ns') }, plog ps)

10691069 where notIn ns (h, _) = h `notElem` map fst ns

1070+ orderUpdateSolved [] t = t

1071+ orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)

10701072processTactic (MatchProblems all) ps

10711073 = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))

10721074 (ns'', probs'') = matchProblems all ps ns' probs'

src/Idris/Elab/Clause.hs+3−1

@@ -670,7 +670,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

670670 (do pbinds ist lhs_tm

671671 -- proof search can use explicitly written names

672672 mapM_ addPSname (allNamesIn lhs_in)

673− mapM_ setinj (nub (tcparams ++ inj))

673+ ulog <- getUnifyLog

674+ traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $

675+ mapM_ setinj (nub (tcparams ++ inj))

674676 setNextName

675677 (ElabResult _ _ is ctxt' newDecls highlights newGName) <-

676678 errAt "right hand side of " fname (Just clhsty)

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

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

873873 ns <- apply (Var f) (map isph args)

874874-- trace ("ns is " ++ show ns) $ return ()

875875 -- mark any type class arguments as injective

876− when (not pattern) $ mapM_ checkIfInjective (map snd ns)

876+-- when (not pattern) $

877+ mapM_ checkIfInjective (map snd ns)

877878 unifyProblems -- try again with the new information,

878879 -- to help with disambiguation

879880 ulog <- getUnifyLog

@@ -962,7 +963,9 @@ elab ist info emode opts fn tm

962963 -- maybe we can solve more things now...

963964 ulog <- getUnifyLog

964965 probs <- get_probs

965− traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $

966+ inj <- get_inj

967+ traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj

968+ ++ "\nProblems: " ++ qshow probs) $

966969 unifyProblems

967970 probs <- get_probs

968971 traceWhen ulog (qshow probs) $ return ()

test/interfaces006/expectednew file

No changes to the content.

test/interfaces006/interfaces006.idrnew file+19

@@ -0,0 +1,19 @@

1+module Categories

3+infixr 9 .

4+interface Category (c: k -> k -> Type) where

5+ id: c x x

6+ (.): c y z -> c x y -> c x z

8+interface Category c => Functor (c: k -> k -> Type) (f: k -> k) where

9+ map: c x y -> c (f x) (f y)

10+

11+infixr 1 =<<

12+interface Functor c m => Monad (c: k -> k -> Type) (m: k -> k) where

13+ return: c x (m x)

14+ join: c (m (m x)) (m x)

15+ (=<<) : c x (m y) -> c (m x) (m y)

16+

17+ join = (=<<) id

18+ (=<<) f = join . map f

19+

test/interfaces006/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces006.idr --noprelude --check

3+rm -rf *.ibc