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

CHANGELOG.md+3

compare with master

unifiedsplit

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

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

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

22 ```

23+

24+## Library updates

25+

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

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

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

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

25

28

idris.cabal+3

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

580 test/interfaces005/*.idr

581 test/interfaces005/run

582 test/interfaces005/expected

583+ test/interfaces006/*.idr

584+ test/interfaces006/run

585+ test/interfaces006/expected

583

586

584 test/io001/run

587 test/io001/run

585 test/io001/*.idr

588 test/io001/*.idr

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

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

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

1059processTactic UnifyProblems ps

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

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

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

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

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

1064 previous = Just ps, plog = "",

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

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

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

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

1070+ orderUpdateSolved [] t = t

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

1070processTactic (MatchProblems all) ps

1072processTactic (MatchProblems all) ps

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

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

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

1074 (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

670 (do pbinds ist lhs_tm

671 -- proof search can use explicitly written names

672 mapM_ addPSname (allNamesIn lhs_in)

673+ ulog <- getUnifyLog

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

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

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

674 setNextName

676 setNextName

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

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

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

678 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

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

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

875 -- mark any type class arguments as injective

876+-- when (not pattern) $

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

877+ mapM_ checkIfInjective (map snd ns)

877 unifyProblems -- try again with the new information,

878 unifyProblems -- try again with the new information,

878 -- to help with disambiguation

879 -- to help with disambiguation

879 ulog <- getUnifyLog

880 ulog <- getUnifyLog

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

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

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

963 ulog <- getUnifyLog

964 ulog <- getUnifyLog

964 probs <- get_probs

965 probs <- get_probs

966+ inj <- get_inj

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

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

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

966 unifyProblems

969 unifyProblems

967 probs <- get_probs

970 probs <- get_probs

968 traceWhen ulog (qshow probs) $ return ()

971 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

2+

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

7+

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