c55f8c2 · Idris-dev · git.iko.soy

src/Core/ProofState.hs+3−3

compare with master

unifiedsplit

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

176unify' ctxt env topx topy =

177 do ps <- get

178 let dont = dontunify ps

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

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

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

181 traceWhen (unifylog ps)

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

183 " in " ++ show env ++

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

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

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

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

186-- ++ show (pterm ps)

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

188 case fails of

src/Core/Unify.hs+6−1

@@ -154,6 +154,9 @@ unify ctxt env topx topy dont holes =

154 sc i = do UI s f <- get

155 put (UI (s+i) f)

156

157+ errors = do UI s f <- get

158+ return (not (null f))

159+

157 uplus u1 u2 = do UI s f <- get

160 uplus u1 u2 = do UI s f <- get

158 r <- u1

161 r <- u1

159 UI s f' <- get

162 UI s f' <- get

@@ -290,7 +293,9 @@ unify ctxt env topx topy dont holes =

290 then

293 then

291-- (notFn headx && notFn heady))) then

294-- (notFn headx && notFn heady))) then

292 do uf <- un' True bnames headx heady

295 do uf <- un' True bnames headx heady

296+ failed <- errors

293− unArgs uf argsx argsy

297+ if (not failed) then unArgs uf argsx argsy

298+ else return []

294 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

299 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

295 unifyTmpFail appx appy)

300 unifyTmpFail appx appy)

296 (unifyTmpFail appx appy) -- whole application fails

301 (unifyTmpFail appx appy) -- whole application fails

src/Idris/AbsSyntaxTree.hs+3−3

@@ -1098,6 +1098,9 @@ showImp ist impl colour tm = se 10 [] tm where

1098 se p bnd (PQuote r) = "![" ++ show r ++ "]"

1099 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n

1100 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1101+ se p bnd e

1102+ | Just str <- slist p bnd e = str

1103+ | Just num <- snat p e = perhapsColourise colouriseData (show num)

1101 se p bnd (PRef fc n) = showName ist bnd impl colour n

1104 se p bnd (PRef fc n) = showName ist bnd impl colour n

1102 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

1105 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

1103 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

1106 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

@@ -1130,9 +1133,6 @@ showImp ist impl colour tm = se 10 [] tm where

1130 = bracket p 2 $

1133 = bracket p 2 $

1131 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1134 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1132 se 10 ((n, False):bnd) sc

1135 se 10 ((n, False):bnd) sc

1133− se p bnd e

1134− | Just str <- slist p bnd e = str

1135− | Just num <- snat p e = perhapsColourise colouriseData (show num)

1136 se p bnd (PMatchApp _ f) = "match " ++ show f

1137 se p bnd (PApp _ hd@(PRef _ f) [])

1138 | not impl = se p bnd hd

src/Idris/Parser.hs+2−2

@@ -147,8 +147,8 @@ loadSource lidr f

147 -- build size change graph from simplified definitions

148 iLOG "Totality checking"

149 i <- getIState

150−-- mapM_ buildSCG (idris_totcheck i)

150+ mapM_ buildSCG (idris_totcheck i)

151−-- mapM_ checkDeclTotality (idris_totcheck i)

151+ mapM_ checkDeclTotality (idris_totcheck i)

152 iLOG ("Finished " ++ f)

153 ibcsd <- valIBCSubDir i

154 iLOG "Universe checking"