db96d75 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

160 test/reg020/run

161 test/reg020/*.idr

162 test/reg020/expected

163+ test/reg021/run

164+ test/reg021/*.idr

165+ test/reg021/expected

163 test/test001/run

166 test/test001/run

164 test/test001/*.idr

167 test/test001/*.idr

165 test/test001/expected

168 test/test001/expected

src/Core/ProofState.hs+6−4

@@ -176,13 +176,15 @@ unify' :: Context -> Env -> TT Name -> TT Name ->

176unify' ctxt env topx topy =

177 do ps <- get

178 let dont = dontunify ps

179− (u, fails) <- traceWhen (unifylog ps) ("Trying " ++ show (topx, topy)) $

179+ (u, fails) <- traceWhen (unifylog ps)

180+ ("Trying " ++ show (topx, topy) ++

181+ " in " ++ show env ++

182+ "\nHoles: " ++ show (holes ps) ++ "\n") $

180 lift $ unify ctxt env topx topy dont (holes ps)

183 lift $ unify ctxt env topx topy dont (holes ps)

181 traceWhen (unifylog ps)

184 traceWhen (unifylog ps)

182 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

185 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

183− " in " ++ show env ++

184− "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails ++ "\nCurrent problems:\n"

186+ "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails

185− ++ qshow (problems ps) ++ "\nHoles: " ++ show (holes ps) ++ "\n"

187+ ++ "\nCurrent problems:\n" ++ qshow (problems ps)

186-- ++ show (pterm ps)

188-- ++ show (pterm ps)

187 ++ "\n----------") $

189 ++ "\n----------") $

188 case fails of

190 case fails of

src/Idris/ElabTerm.hs+1−1

@@ -97,6 +97,7 @@ elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->

97elab ist info pattern tcgen fn tm

98 = do let loglvl = opt_logLevel (idris_options ist)

99 when (loglvl > 5) $ unifyLog True

100+ compute -- expand type synonyms, etc

100 elabE (False, False) tm -- (in argument, guarded)

101 elabE (False, False) tm -- (in argument, guarded)

101 end_unify

102 end_unify

102 when pattern -- convert remaining holes to pattern vars

103 when pattern -- convert remaining holes to pattern vars

@@ -493,7 +494,6 @@ elab ist info pattern tcgen fn tm

493 (caseBlock fc cname' (reverse args) opts)

494 (caseBlock fc cname' (reverse args) opts)

494 -- elaborate case

495 -- elaborate case

495 env <- get_env

496 env <- get_env

496− g <- goal

497 updateAux (newdef : )

498 -- if we haven't got the type yet, hopefully we'll get it later!

499 movelast tyn

test/reg022/expectednew file

No changes to the content.

test/reg022/reg022.idrnew file+18

@@ -0,0 +1,18 @@

1+module reg022

2+

3+data Result str a = Success str a | Failure String

4+

5+instance Functor (Result str) where

6+ map f (Success s x) = Success s (f x)

7+ map f (Failure e ) = Failure e

8+

9+ParserT : (Type -> Type) -> Type -> Type -> Type

10+ParserT m str a = str -> m (Result str a)

11+

12+ap : Monad m => ParserT m str (a -> b) -> ParserT m str a ->

13+ ParserT m str b

14+ap f x = \s => do f' <- f s

15+ case f' of

16+ Failure e => (pure (Failure e))

17+ Success s' g => x s' >>= pure . map g

18+

test/reg022/runnew file+3

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

1+#!/bin/bash

2+idris $@ reg022.idr --check

3+rm -f *.ibc