d8edff9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed type class resolution bug

d8edff9Edwin Brady15 years ago

lib/Makefile+1−1

compare with master

unifiedsplit

@@ -7,7 +7,7 @@ check: .PHONY

8recheck: clean check

10−install: check

10+install: recheck

11 mkdir -p $(TARGET)/prelude

12 install *.ibc $(TARGET)

13 install prelude/*.ibc $(TARGET)/prelude

lib/builtins.idr+11−1

@@ -153,6 +153,12 @@ instance Ord Int where {

153 GT;

154}

155

156+instance Ord Integer where {

157+ compare x y = if (x == y) then EQ else

158+ if (boolOp prim__ltBigInt x y) then LT else

159+ GT;

160+}

161+

156instance Ord Float where {

162instance Ord Float where {

157 compare x y = if (x == y) then EQ else

163 compare x y = if (x == y) then EQ else

158 if (boolOp prim__ltFloat x y) then LT else

164 if (boolOp prim__ltFloat x y) then LT else

@@ -171,14 +177,18 @@ instance Ord String where {

171 GT;

177 GT;

172}

178}

173

179

174−class Eq a => Num a where {

180+class (Eq a, Ord a) => Num a where {

175 (+) : a -> a -> a;

181 (+) : a -> a -> a;

176 (-) : a -> a -> a;

182 (-) : a -> a -> a;

177 (*) : a -> a -> a;

183 (*) : a -> a -> a;

178

184

185+ abs : a -> a;

186+ abs x = if (x < 0) then (-x) else x;

187+

179 fromInteger : Int -> a;

188 fromInteger : Int -> a;

180}

189}

181

190

191+

182instance Num Int where {

192instance Num Int where {

183 (+) = prim__addInt;

193 (+) = prim__addInt;

184 (-) = prim__subInt;

194 (-) = prim__subInt;

lib/prelude/nat.idr+7−7

@@ -30,6 +30,13 @@ instance Eq Nat where {

30 (S x) == O = False;

31}

33+instance Ord Nat where {

34+ compare O O = EQ;

35+ compare O (S k) = LT;

36+ compare (S k) O = GT;

37+ compare (S x) (S y) = compare x y;

38+}

39+

33instance Num Nat where {

40instance Num Nat where {

34 (+) = plus;

41 (+) = plus;

35 (-) = sub;

42 (-) = sub;

@@ -38,13 +45,6 @@ instance Num Nat where {

38 fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;

45 fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;

39}

46}

41−instance Ord Nat where {

42− compare O O = EQ;

43− compare O (S k) = LT;

44− compare (S k) O = GT;

45− compare (S x) (S y) = compare x y;

46−}

47−

48plusnO : (m : Nat) -> m + O = m;

49plusnO O = refl;

50plusnO (S k) = eqRespS (plusnO k);

lib/prelude/strings.idr+1

@@ -45,3 +45,4 @@ span p s with strM s {

46break : (Char -> Bool) -> String -> (String, String);

47break p = span (not . p);

48+

src/Idris/ElabDecls.hs+10−10

@@ -42,7 +42,7 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

42 let ty = addImpl i ty'

43 logLvl 2 $ show n ++ " type " ++ showImp True ty

44 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

45− (erun fc (build i info False ty))

45+ (erun fc (build i info False n ty))

46 (cty, _) <- recheckC ctxt fc [] ty'

47 logLvl 2 $ "---> " ++ show cty

48 let nty = normalise ctxt [] cty

@@ -59,7 +59,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

59 t_in <- implicit syn n t_in

60 let t = addImpl i t_in

61 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

62− (erun fc (build i info False t))

62+ (erun fc (build i info False n t))

63 def' <- checkDef fc defer

64 addDeferred def'

65 (cty, _) <- recheckC ctxt fc [] t'

@@ -79,7 +79,7 @@ elabCon info syn (n, t_in, fc)

79 let t = addImpl i t_in

80 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

81 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))

82− (erun fc (build i info False t))

82+ (erun fc (build i info False n t))

83 logLvl 2 $ "Rechecking " ++ show t'

84 def' <- checkDef fc defer

85 addDeferred def'

@@ -129,7 +129,7 @@ elabVal info aspat tm_in

129 let tm = addImpl i tm_in

130 logLvl 10 (showImp True tm)

131 ((tm', defer), _) <- tclift $ elaborate ctxt (MN 0 "val") infP

132− (build i info aspat (infTerm tm))

132+ (build i info aspat (MN 0 "val") (infTerm tm))

133 logLvl 3 ("Value: " ++ show tm')

134 let vtm = getInferTerm tm'

135 logLvl 2 (show vtm)

@@ -142,7 +142,7 @@ elabClause info fc (PClause fname lhs_in [] PImpossible [])

142 let lhs = addImpl i lhs_in

143 -- if the LHS type checks, it is possible, so report an error

144 case elaborate ctxt (MN 0 "patLHS") infP

145− (erun fc (build i info True (infTerm lhs))) of

145+ (erun fc (build i info True fname (infTerm lhs))) of

146 OK _ -> fail $ show fc ++ ":" ++ show lhs ++ " is a possible case"

147 Error _ -> return ()

148 return Nothing

@@ -154,7 +154,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

154 let lhs = addImpl i lhs_in

155 logLvl 5 ("LHS: " ++ showImp True lhs)

156 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

157− (erun fc (build i info True (infTerm lhs)))

157+ (erun fc (build i info True fname (infTerm lhs)))

158 let lhs_tm = orderPats (getInferTerm lhs')

159 let lhs_ty = getInferType lhs'

160 logLvl 3 (show lhs_tm)

@@ -179,7 +179,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)

179 ((rhs', defer), _) <-

180 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

181 (do pbinds lhs_tm

182− (_, _) <- erun fc (build i info False rhs)

182+ (_, _) <- erun fc (build i info False fname rhs)

183 psolve lhs_tm

184 tt <- get_term

185 return $ runState (collectDeferred tt) [])

@@ -213,7 +213,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

213 let lhs = addImpl i lhs_in

214 logLvl 5 ("LHS: " ++ showImp True lhs)

215 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

216− (erun fc (build i info True (infTerm lhs)))

216+ (erun fc (build i info True fname (infTerm lhs)))

217 let lhs_tm = orderPats (getInferTerm lhs')

218 let lhs_ty = getInferType lhs'

219 let ret_ty = getRetTy lhs_ty

@@ -229,7 +229,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

229 (bindTyArgs PVTy bargs infP)

230 (do pbinds lhs_tm

231 -- TODO: may want where here - see winfo abpve

232− (_', d) <- erun fc (build i info False (infTerm wval))

232+ (_', d) <- erun fc (build i info False fname (infTerm wval))

233 psolve lhs_tm

234 tt <- get_term

235 return (tt, d))

@@ -264,7 +264,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

264 ((rhs', defer), _) <-

265 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty

266 (do pbinds lhs_tm

267− (_, d) <- erun fc (build i info False rhs)

267+ (_, d) <- erun fc (build i info False fname rhs)

268 psolve lhs_tm

269 tt <- get_term

270 return (tt, d))

src/Idris/ElabTerm.hs+21−19

@@ -29,14 +29,16 @@ toplevel = EInfo [] emptyContext id Nothing

30-- Also find deferred names in the term and their types

32−build :: IState -> ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])

32+build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

33+ Elab (Term, [(Name, Type)])

33−build ist info pattern tm

34+build ist info pattern fn tm

34− = do elab ist info pattern tm

35+ = do elab ist info pattern fn tm

35 tt <- get_term

36 tt <- get_term

36 return $ runState (collectDeferred tt) []

37 return $ runState (collectDeferred tt) []

38−elab :: IState -> ElabInfo -> Bool -> PTerm -> Elab ()

39+elab :: IState -> ElabInfo -> Bool -> Name -> PTerm ->

40+ Elab ()

39−elab ist info pattern tm

41+elab ist info pattern fn tm

40 = do elabE tm

42 = do elabE tm

41 when pattern -- convert remaining holes to pattern vars

43 when pattern -- convert remaining holes to pattern vars

42 mkPat

44 mkPat

@@ -69,7 +71,7 @@ elab ist info pattern tm

69 (elab' (PRef fc unitTy))

71 (elab' (PRef fc unitTy))

70 elab' (PFalse fc) = elab' (PRef fc falseTy)

72 elab' (PFalse fc) = elab' (PRef fc falseTy)

71 elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes

73 elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes

72− = resolveTC 2 ist

74+ = resolveTC 2 fn ist

73 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

75 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")

74 instanceArg c

76 instanceArg c

75 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

77 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

@@ -175,7 +177,7 @@ elab ist info pattern tm

175 ivs' <- get_instances

177 ivs' <- get_instances

176 when (not pattern) $

178 when (not pattern) $

177 mapM_ (\n -> do focus n

179 mapM_ (\n -> do focus n

178− resolveTC 7 ist) (ivs' \\ ivs)

180+ resolveTC 7 fn ist) (ivs' \\ ivs)

179-- ivs <- get_instances

181-- ivs <- get_instances

180-- when (not (null ivs)) $

182-- when (not (null ivs)) $

181-- do t <- get_term

183-- do t <- get_term

@@ -231,17 +233,17 @@ pruneAlt xs = map prune xs

231 headIs f _ = True -- keep if it's not an application

233 headIs f _ = True -- keep if it's not an application

232

234

233trivial :: IState -> Elab ()

235trivial :: IState -> Elab ()

234−trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))

236+trivial ist = try (elab ist toplevel False (MN 0 "tac") (PRefl (FC "prf" 0)))

235 (do env <- get_env

237 (do env <- get_env

236 tryAll (map fst env))

238 tryAll (map fst env))

237 where

239 where

238 tryAll [] = fail "No trivial solution"

240 tryAll [] = fail "No trivial solution"

239− tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))

241+ tryAll (x:xs) = try (elab ist toplevel False (MN 0 "tac") (PRef (FC "prf" 0) x))

240 (tryAll xs)

242 (tryAll xs)

241

243

242−resolveTC :: Int -> IState -> Elab ()

244+resolveTC :: Int -> Name -> IState -> Elab ()

243−resolveTC 0 ist = fail $ "Can't resolve type class"

245+resolveTC 0 fn ist = fail $ "Can't resolve type class"

244−resolveTC depth ist

246+resolveTC depth fn ist

245 = try (trivial ist)

247 = try (trivial ist)

246 (do t <- goal

248 (do t <- goal

247 let (tc, ttypes) = unApply t

249 let (tc, ttypes) = unApply t

@@ -251,7 +253,7 @@ resolveTC depth ist

251-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

253-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))

252 blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

254 blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))

253 where

255 where

254− elabTC n | tcname n = (resolve n depth, show n)

256+ elabTC n | n /= fn && tcname n = (resolve n depth, show n)

255 | otherwise = (fail "Can't resolve", show n)

257 | otherwise = (fail "Can't resolve", show n)

256

258

257 needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]

259 needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]

@@ -266,8 +268,8 @@ resolveTC depth ist

266 boundVar _ = False

268 boundVar _ = False

267

269

268 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

270 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t

269− blunderbuss t (n:ns) | tcname n = try (resolve n depth)

271+ blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)

270− (blunderbuss t ns)

272+ (blunderbuss t ns)

271 | otherwise = blunderbuss t ns

273 | otherwise = blunderbuss t ns

272 tcname (UN ('@':_)) = True

274 tcname (UN ('@':_)) = True

273 tcname (NS n _) = tcname n

275 tcname (NS n _) = tcname n

@@ -282,7 +284,7 @@ resolveTC depth ist

282 [args] -> map isImp (snd args) -- won't be overloaded!

284 [args] -> map isImp (snd args) -- won't be overloaded!

283 args <- apply (Var n) imps

285 args <- apply (Var n) imps

284 mapM_ (\ (_,n) -> do focus n

286 mapM_ (\ (_,n) -> do focus n

285− resolveTC (depth - 1) ist)

287+ resolveTC (depth - 1) fn ist)

286 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

288 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

287 solve

289 solve

288 where isImp (PImp p _ _ _) = (True, p)

290 where isImp (PImp p _ _ _) = (True, p)

@@ -314,7 +316,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

314 bname (Bind n _ _) = Just n

316 bname (Bind n _ _) = Just n

315 bname _ = Nothing

317 bname _ = Nothing

316 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

318 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs

317− runT (Exact tm) = do elab ist toplevel False tm

319+ runT (Exact tm) = do elab ist toplevel False (MN 0 "tac") tm

318 when autoSolve solveAll

320 when autoSolve solveAll

319 runT (Refine fn [])

321 runT (Refine fn [])

320 = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

322 = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

@@ -343,7 +345,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

343 letn <- unique_hole (MN 0 "rewrite_rule")

345 letn <- unique_hole (MN 0 "rewrite_rule")

344 letbind letn (Var tyn) (Var valn)

346 letbind letn (Var tyn) (Var valn)

345 focus valn

347 focus valn

346− elab ist toplevel False tm

348+ elab ist toplevel False (MN 0 "tac") tm

347 rewrite (Var letn)

349 rewrite (Var letn)

348 when autoSolve solveAll

350 when autoSolve solveAll

349 runT (LetTac n tm)

351 runT (LetTac n tm)

@@ -355,7 +357,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where

355 letn <- unique_hole n

357 letn <- unique_hole n

356 letbind letn (Var tyn) (Var valn)

358 letbind letn (Var tyn) (Var valn)

357 focus valn

359 focus valn

358− elab ist toplevel False tm

360+ elab ist toplevel False (MN 0 "tac") tm

359 when autoSolve solveAll

361 when autoSolve solveAll

360 runT Compute = compute

362 runT Compute = compute

361 runT Trivial = do trivial ist; when autoSolve solveAll

363 runT Trivial = do trivial ist; when autoSolve solveAll