463e62a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some type class bug fixes

463e62aEdwin Brady15 years ago

lib/Makefile+1−1

compare with master

unifiedsplit

@@ -20,6 +20,6 @@ clean: .PHONY

20 rm -f control/monad/*.ibc

22linecount: .PHONY

23− wc -l *.idr network/*.idr prelude/*.idr

23+ wc -l *.idr network/*.idr prelude/*.idr control/monad/*.idr

25.PHONY:

src/Idris/AbsSyntax.hs+9−4

@@ -74,7 +74,7 @@ data IBCWrite = IBCFix FixDecl

74 | IBCImp Name

75 | IBCStatic Name

76 | IBCClass Name

77− | IBCInstance Name Name

77+ | IBCInstance Bool Name Name

78 | IBCDSL Name

79 | IBCData Name

80 | IBCOpt Name

@@ -148,15 +148,20 @@ addToCG :: Name -> [Name] -> Idris ()

148addToCG n ns = do i <- get

149 put (i { idris_callgraph = addDef n ns (idris_callgraph i) })

150

151+-- Add a class instance function. Dodgy hack: Put integer instances first in the

152+-- list so they are resolved by default.

153+

151−addInstance :: Name -> Name -> Idris ()

154+addInstance :: Bool -> Name -> Name -> Idris ()

152−addInstance n i

155+addInstance int n i

153 = do ist <- get

156 = do ist <- get

154 case lookupCtxt Nothing n (idris_classes ist) of

157 case lookupCtxt Nothing n (idris_classes ist) of

155 [CI a b c d ins] ->

158 [CI a b c d ins] ->

156− do let cs = addDef n (CI a b c d (i : ins)) (idris_classes ist)

159+ do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)

157 put (ist { idris_classes = cs })

160 put (ist { idris_classes = cs })

158 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)

161 _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)

159 put (ist { idris_classes = cs })

162 put (ist { idris_classes = cs })

163+ where addI i ins | int = i : ins

164+ | otherwise = ins ++ [i]

160

165

161addClass :: Name -> ClassInfo -> Idris ()

166addClass :: Name -> ClassInfo -> Idris ()

162addClass n i

167addClass n i

src/Idris/ElabDecls.hs+14−7

@@ -608,9 +608,9 @@ elabClass info syn fc constraints tn ps ds

608 let conn' = case lookupCtxtName Nothing conn (idris_classes i) of

609 [(n, _)] -> n

610 _ -> conn

611− addInstance conn' cfn

611+ addInstance False conn' cfn

612− addIBC (IBCInstance conn' cfn)

612+ addIBC (IBCInstance False conn' cfn)

613−-- iputStrLn ("Added " ++ show (conn, cfn))

613+-- iputStrLn ("Added " ++ show (conn, cfn, ty))

614 return [PTy syn fc [] cfn ty,

615 PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

616

@@ -658,8 +658,11 @@ elabClass info syn fc constraints tn ps ds

658 toExp ns e sc = sc

659

660elabInstance :: ElabInfo -> SyntaxInfo ->

661− FC -> [PTerm] -> Name ->

661+ FC -> [PTerm] -> -- constraints

662+ Name -> -- the class

663+ [PTerm] -> -- class parameters (i.e. instance)

664+ PTerm -> -- full instance type

662− [PTerm] -> PTerm -> [PDecl] -> Idris ()

665+ [PDecl] -> Idris ()

663elabInstance info syn fc cs n ps t ds

666elabInstance info syn fc cs n ps t ds

664 = do i <- get

667 = do i <- get

665 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

668 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

@@ -669,7 +672,7 @@ elabInstance info syn fc cs n ps t ds

669 -- if the instance type matches any of the instances we have already,

672 -- if the instance type matches any of the instances we have already,

670 -- then it's overlapping, so report an error

673 -- then it's overlapping, so report an error

671 mapM_ (checkNotOverlapping i t) (class_instances ci)

674 mapM_ (checkNotOverlapping i t) (class_instances ci)

672− addInstance n iname

675+ addInstance intInst n iname

673 elabType info syn fc [] iname t

676 elabType info syn fc [] iname t

674 let ips = zip (class_params ci) ps

677 let ips = zip (class_params ci) ps

675 let ns = case n of

678 let ns = case n of

@@ -700,8 +703,12 @@ elabInstance info syn fc cs n ps t ds

700 [PClause fc iname lhs [] rhs wb]

703 [PClause fc iname lhs [] rhs wb]

701 iLOG (show idecl)

704 iLOG (show idecl)

702 elabDecl info idecl

705 elabDecl info idecl

703− addIBC (IBCInstance n iname)

706+ addIBC (IBCInstance intInst n iname)

704 where

707 where

708+ intInst = case ps of

709+ [PConstant IType] -> True

710+ _ -> False

711+

705 checkNotOverlapping i t n

712 checkNotOverlapping i t n

706 | take 2 (show n) == "@@" = return ()

713 | take 2 (show n) == "@@" = return ()

707 | otherwise

714 | otherwise

src/Idris/ElabTerm.hs+13−17

@@ -101,10 +101,7 @@ elab ist info pattern tcgen fn tm

101 (elab' ina (PRef fc unitTy))

102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

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

104− = do t <- goal

105− -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

106− let insts = findInstances ist t

107− resolveTC 2 fn insts ist

104+ = resolveTC 2 fn ist

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

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

109 instanceArg c

106 instanceArg c

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

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

@@ -240,9 +237,7 @@ elab ist info pattern tcgen fn tm

240 when (not pattern || (ina && not tcgen)) $

237 when (not pattern || (ina && not tcgen)) $

241 mapM_ (\n -> do focus n

238 mapM_ (\n -> do focus n

242 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

239 -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

243− t <- goal

244− let insts = findInstances ist t

245− resolveTC 7 fn insts ist) (ivs' \\ ivs)

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

246 where tcArg (n, PConstraint _ _ Placeholder) = True

241 where tcArg (n, PConstraint _ _ Placeholder) = True

247 tcArg _ = False

242 tcArg _ = False

248

243

@@ -359,12 +354,13 @@ findInstances ist t

359 _ -> []

354 _ -> []

360 | otherwise = []

355 | otherwise = []

361

356

362−resolveTC :: Int -> Name -> [Name] -> IState -> ElabD ()

357+resolveTC :: Int -> Name -> IState -> ElabD ()

363−resolveTC 0 fn insts ist = fail $ "Can't resolve type class"

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

364−resolveTC 1 fn insts ist = try (trivial ist) (resolveTC 0 fn insts ist)

359+resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

365−resolveTC depth fn insts ist

360+resolveTC depth fn ist

366 = try (trivial ist)

361 = try (trivial ist)

367 (do t <- goal

362 (do t <- goal

363+ let insts = findInstances ist t

368 let (tc, ttypes) = unApply t

364 let (tc, ttypes) = unApply t

369 scopeOnly <- needsDefault t tc ttypes

365 scopeOnly <- needsDefault t tc ttypes

370 tm <- get_term

366 tm <- get_term

@@ -376,11 +372,11 @@ resolveTC depth fn insts ist

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

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

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

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

378

374

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

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

380− = do focus a

376+-- = do focus a

381− fill (RConstant IType) -- default Int

377+-- fill (RConstant IType) -- default Int

382− solve

378+-- solve

383− return False

379+-- return False

384 needsDefault t f as

380 needsDefault t f as

385 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

381 | all boundVar as = return True -- fail $ "Can't resolve " ++ show t

386 needsDefault t f a = return False -- trace (show t) $ return ()

382 needsDefault t f a = return False -- trace (show t) $ return ()

@@ -408,7 +404,7 @@ resolveTC depth fn insts ist

408 args <- apply (Var n) imps

404 args <- apply (Var n) imps

409-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

405-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

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

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

411− resolveTC (depth - 1) fn insts ist)

407+ resolveTC (depth - 1) fn ist)

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

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

413 -- if there's any arguments left, we've failed to resolve

409 -- if there's any arguments left, we've failed to resolve

414 solve

410 solve

src/Idris/IBC.hs+6−6

@@ -21,7 +21,7 @@ import System.Directory

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 16

24+ibcVersion = 17

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -30,7 +30,7 @@ data IBCFile = IBCFile { ver :: Word8,

30 ibc_fixes :: [FixDecl],

31 ibc_statics :: [(Name, [Bool])],

32 ibc_classes :: [(Name, ClassInfo)],

33− ibc_instances :: [(Name, Name)],

33+ ibc_instances :: [(Bool, Name, Name)],

34 ibc_dsls :: [(Name, DSL)],

35 ibc_datatypes :: [(Name, TypeInfo)],

36 ibc_optimise :: [(Name, OptInfo)],

@@ -88,8 +88,8 @@ ibc i (IBCClass n) f

88 = case lookupCtxt Nothing n (idris_classes i) of

89 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

90 _ -> fail "IBC write failed"

91−ibc i (IBCInstance n ins) f

91+ibc i (IBCInstance int n ins) f

92− = return f { ibc_instances = (n,ins): ibc_instances f }

92+ = return f { ibc_instances = (int,n,ins): ibc_instances f }

93ibc i (IBCDSL n) f

94 = case lookupCtxt Nothing n (idris_dsls i) of

95 [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }

@@ -193,8 +193,8 @@ pClasses cs = mapM_ (\ (n, c) ->

193 = addDef n c (idris_classes i) }))

194 cs

195

196−pInstances :: [(Name, Name)] -> Idris ()

196+pInstances :: [(Bool, Name, Name)] -> Idris ()

197−pInstances cs = mapM_ (\ (n, ins) -> addInstance n ins) cs

197+pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs

198

199pDSLs :: [(Name, DSL)] -> Idris ()

200pDSLs cs = mapM_ (\ (n, c) ->

src/Idris/Parser.hs+2−2

@@ -479,7 +479,7 @@ pClass syn = do acc <- pAccessibility

479 n_in <- pName; let n = expandNS syn n_in

480 cs <- many1 carg

481 reserved "where"; open_block

482− ds <- many1 $ pFunDecl syn

482+ ds <- many $ pFunDecl syn

483 close_block

484 let allDs = concat ds

485 accData acc n (concatMap declared allDs)

@@ -499,7 +499,7 @@ pInstance syn = do reserved "instance"

499 let sc = PApp fc (PRef fc cn) (map pexp args)

500 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc

501 reserved "where"; open_block

502− ds <- many1 $ pFunDecl syn

502+ ds <- many $ pFunDecl syn

503 close_block

504 return [PInstance syn fc cs cn args t (concat ds)]

505