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

lib/Makefile+1−1

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

2020 rm -f control/monad/*.ibc

2121

2222linecount: .PHONY

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

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

2424

2525.PHONY:

src/Idris/AbsSyntax.hs+9−4

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

7474 | IBCImp Name

7575 | IBCStatic Name

7676 | IBCClass Name

77− | IBCInstance Name Name

77+ | IBCInstance Bool Name Name

7878 | IBCDSL Name

7979 | IBCData Name

8080 | IBCOpt Name

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

148148addToCG n ns = do i <- get

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

150150

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

152−addInstance n i

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

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

153+

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

155+addInstance int n i

153156 = do ist <- get

154157 case lookupCtxt Nothing n (idris_classes ist) of

155158 [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)

157160 put (ist { idris_classes = cs })

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

159162 put (ist { idris_classes = cs })

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

164+ | otherwise = ins ++ [i]

160165

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

162167addClass n i

src/Idris/ElabDecls.hs+14−7

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

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

609609 [(n, _)] -> n

610610 _ -> conn

611− addInstance conn' cfn

612− addIBC (IBCInstance conn' cfn)

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

611+ addInstance False conn' cfn

612+ addIBC (IBCInstance False conn' cfn)

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

614614 return [PTy syn fc [] cfn ty,

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

616616

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

658658 toExp ns e sc = sc

659659

660660elabInstance :: ElabInfo -> SyntaxInfo ->

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

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

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

662+ Name -> -- the class

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

664+ PTerm -> -- full instance type

665+ [PDecl] -> Idris ()

663666elabInstance info syn fc cs n ps t ds

664667 = do i <- get

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

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

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

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

671674 mapM_ (checkNotOverlapping i t) (class_instances ci)

672− addInstance n iname

675+ addInstance intInst n iname

673676 elabType info syn fc [] iname t

674677 let ips = zip (class_params ci) ps

675678 let ns = case n of

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

700703 [PClause fc iname lhs [] rhs wb]

701704 iLOG (show idecl)

702705 elabDecl info idecl

703− addIBC (IBCInstance n iname)

706+ addIBC (IBCInstance intInst n iname)

704707 where

708+ intInst = case ps of

709+ [PConstant IType] -> True

710+ _ -> False

711+

705712 checkNotOverlapping i t n

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

707714 | otherwise

src/Idris/ElabTerm.hs+13−17

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

101101 (elab' ina (PRef fc unitTy))

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

103103 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

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

109106 instanceArg c

110107 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

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

241238 mapM_ (\n -> do focus n

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

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

247242 tcArg _ = False

248243

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

359354 _ -> []

360355 | otherwise = []

361356

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

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

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

365−resolveTC depth fn insts ist

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

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

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

360+resolveTC depth fn ist

366361 = try (trivial ist)

367362 (do t <- goal

363+ let insts = findInstances ist t

368364 let (tc, ttypes) = unApply t

369365 scopeOnly <- needsDefault t tc ttypes

370366 tm <- get_term

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

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

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

378374

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

380− = do focus a

381− fill (RConstant IType) -- default Int

382− solve

383− return False

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

376+-- = do focus a

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

378+-- solve

379+-- return False

384380 needsDefault t f as

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

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

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

408404 args <- apply (Var n) imps

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

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

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

407+ resolveTC (depth - 1) fn ist)

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

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

414410 solve

src/Idris/IBC.hs+6−6

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

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 16

24+ibcVersion = 17

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

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

3030 ibc_fixes :: [FixDecl],

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

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

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

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

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

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

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

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

8888 = case lookupCtxt Nothing n (idris_classes i) of

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

9090 _ -> fail "IBC write failed"

91−ibc i (IBCInstance n ins) f

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

91+ibc i (IBCInstance int n ins) f

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

9393ibc i (IBCDSL n) f

9494 = case lookupCtxt Nothing n (idris_dsls i) of

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

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

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

194194 cs

195195

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

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

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

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

198198

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

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

src/Idris/Parser.hs+2−2

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

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

480480 cs <- many1 carg

481481 reserved "where"; open_block

482− ds <- many1 $ pFunDecl syn

482+ ds <- many $ pFunDecl syn

483483 close_block

484484 let allDs = concat ds

485485 accData acc n (concatMap declared allDs)

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

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

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

501501 reserved "where"; open_block

502− ds <- many1 $ pFunDecl syn

502+ ds <- many $ pFunDecl syn

503503 close_block

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

505505