d8edff9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed type class resolution bug

commitd8edff9f41e7b7ef444b4ae9d4d8c7af14dbfdee authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 21 Dec 2011, 01:00 (15 years ago) parent00e21ca

6 files changed+51−38

compare with master

unifiedsplit

lib/Makefile+1−1 lib/builtins.idr+11−1 lib/prelude/nat.idr+7−7 lib/prelude/strings.idr+1 src/Idris/ElabDecls.hs+10−10 src/Idris/ElabTerm.hs+21−19

lib/Makefile+1−1

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

88recheck: clean check

10−install: check

10+install: recheck

1111 mkdir -p $(TARGET)/prelude

1212 install *.ibc $(TARGET)

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

lib/builtins.idr+11−1

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

153153 GT;

154154}

155155

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+

156162instance Ord Float where {

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

158164 if (boolOp prim__ltFloat x y) then LT else

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

171177 GT;

172178}

173179

174−class Eq a => Num a where {

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

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

176182 (-) : a -> a -> a;

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

178184

185+ abs : a -> a;

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

187+

179188 fromInteger : Int -> a;

180189}

181190

191+

182192instance Num Int where {

183193 (+) = prim__addInt;

184194 (-) = prim__subInt;

lib/prelude/nat.idr+7−7

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

3030 (S x) == O = False;

3131}

3232

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+

3340instance Num Nat where {

3441 (+) = plus;

3542 (-) = sub;

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

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

3946}

4047

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−

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

4949plusnO O = refl;

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

lib/prelude/strings.idr+1

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

4545

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

4747break 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

4242 let ty = addImpl i ty'

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

4444 ((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))

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

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

4848 let nty = normalise ctxt [] cty

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

5959 t_in <- implicit syn n t_in

6060 let t = addImpl i t_in

6161 ((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))

6363 def' <- checkDef fc defer

6464 addDeferred def'

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

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

7979 let t = addImpl i t_in

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

8181 ((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))

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

8484 def' <- checkDef fc defer

8585 addDeferred def'

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

129129 let tm = addImpl i tm_in

130130 logLvl 10 (showImp True tm)

131131 ((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))

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

134134 let vtm = getInferTerm tm'

135135 logLvl 2 (show vtm)

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

142142 let lhs = addImpl i lhs_in

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

144144 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

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

147147 Error _ -> return ()

148148 return Nothing

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

154154 let lhs = addImpl i lhs_in

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

156156 ((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)))

158158 let lhs_tm = orderPats (getInferTerm lhs')

159159 let lhs_ty = getInferType lhs'

160160 logLvl 3 (show lhs_tm)

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

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

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

181181 (do pbinds lhs_tm

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

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

183183 psolve lhs_tm

184184 tt <- get_term

185185 return $ runState (collectDeferred tt) [])

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

213213 let lhs = addImpl i lhs_in

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

215215 ((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)))

217217 let lhs_tm = orderPats (getInferTerm lhs')

218218 let lhs_ty = getInferType lhs'

219219 let ret_ty = getRetTy lhs_ty

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

229229 (bindTyArgs PVTy bargs infP)

230230 (do pbinds lhs_tm

231231 -- 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))

233233 psolve lhs_tm

234234 tt <- get_term

235235 return (tt, d))

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

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

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

266266 (do pbinds lhs_tm

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

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

268268 psolve lhs_tm

269269 tt <- get_term

270270 return (tt, d))

src/Idris/ElabTerm.hs+21−19

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

2929

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

3131

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

33−build ist info pattern tm

34− = do elab ist info pattern tm

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

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

34+build ist info pattern fn tm

35+ = do elab ist info pattern fn tm

3536 tt <- get_term

3637 return $ runState (collectDeferred tt) []

3738

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

39−elab ist info pattern tm

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

40+ Elab ()

41+elab ist info pattern fn tm

4042 = do elabE tm

4143 when pattern -- convert remaining holes to pattern vars

4244 mkPat

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

6971 (elab' (PRef fc unitTy))

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

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

72− = resolveTC 2 ist

74+ = resolveTC 2 fn ist

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

7476 instanceArg c

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

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

175177 ivs' <- get_instances

176178 when (not pattern) $

177179 mapM_ (\n -> do focus n

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

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

179181-- ivs <- get_instances

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

181183-- do t <- get_term

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

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

232234

233235trivial :: 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)))

235237 (do env <- get_env

236238 tryAll (map fst env))

237239 where

238240 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))

240242 (tryAll xs)

241243

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

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

244−resolveTC depth ist

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

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

246+resolveTC depth fn ist

245247 = try (trivial ist)

246248 (do t <- goal

247249 let (tc, ttypes) = unApply t

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

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

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

253255 where

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

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

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

256258

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

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

266268 boundVar _ = False

267269

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

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

270− (blunderbuss t ns)

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

272+ (blunderbuss t ns)

271273 | otherwise = blunderbuss t ns

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

273275 tcname (NS n _) = tcname n

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

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

283285 args <- apply (Var n) imps

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

285− resolveTC (depth - 1) ist)

287+ resolveTC (depth - 1) fn ist)

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

287289 solve

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

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

314316 bname (Bind n _ _) = Just n

315317 bname _ = Nothing

316318 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

318320 when autoSolve solveAll

319321 runT (Refine fn [])

320322 = 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

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

344346 letbind letn (Var tyn) (Var valn)

345347 focus valn

346− elab ist toplevel False tm

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

347349 rewrite (Var letn)

348350 when autoSolve solveAll

349351 runT (LetTac n tm)

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

355357 letn <- unique_hole n

356358 letbind letn (Var tyn) (Var valn)

357359 focus valn

358− elab ist toplevel False tm

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

359361 when autoSolve solveAll

360362 runT Compute = compute

361363 runT Trivial = do trivial ist; when autoSolve solveAll