58bcd1e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better type class resolution

commit58bcd1eea5bf36732ae5dd23cc5aa8c3ff250aca authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 2 Feb 2012, 14:21 (15 years ago) parent33baa44

5 files changed+64−12

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+21−1 src/Idris/ElabDecls.hs+13−2 src/Idris/ElabTerm.hs+14−2 src/Idris/IBC.hs+15−6 tutorial/examples/theorems.idr+1−1

src/Idris/AbsSyntax.hs+21−1

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

7474 | IBCImp Name

7575 | IBCStatic Name

7676 | IBCClass Name

77+ | IBCInstance Name Name

7778 | IBCDSL Name

7879 | IBCData Name

7980 | IBCOpt Name

@@ -147,6 +148,24 @@ addToCG :: Name -> [Name] -> Idris ()

147148addToCG n ns = do i <- get

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

149150

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

152+addInstance n i

153+ = do ist <- get

154+ case lookupCtxt Nothing n (idris_classes ist) of

155+ [CI a b c d ins] ->

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

157+ put (ist { idris_classes = cs })

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

159+ put (ist { idris_classes = cs })

160+

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

162+addClass n i

163+ = do ist <- get

164+ let i' = case lookupCtxt Nothing n (idris_classes ist) of

165+ [c] -> c { class_instances = class_instances i }

166+ _ -> i

167+ put (ist { idris_classes = addDef n i' (idris_classes ist) })

168+

150169addIBC :: IBCWrite -> Idris ()

151170addIBC ibc@(IBCDef n)

152171 = do i <- get

@@ -581,7 +600,8 @@ type PArg = PArg' PTerm

581600data ClassInfo = CI { instanceName :: Name,

582601 class_methods :: [(Name, (FnOpts, PTerm))],

583602 class_defaults :: [(Name, Name)], -- method name -> default impl

584− class_params :: [Name] }

603+ class_params :: [Name],

604+ class_instances :: [Name] }

585605 deriving Show

586606{-!

587607deriving instance Binary ClassInfo

src/Idris/ElabDecls.hs+13−2

@@ -552,8 +552,7 @@ elabClass info syn fc constraints tn ps ds

552552 mapM_ (elabDecl info) (concat (map (snd.snd) defs))

553553 i <- get

554554 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

555− put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps))

556− (idris_classes i) })

555+ addClass tn (CI cn imethods defaults (map fst ps) [])

557556 addIBC (IBCClass tn)

558557 where

559558 pibind [] x = x

@@ -598,6 +597,16 @@ elabClass info syn fc constraints tn ps ds

598597 let ty = PPi constraint (MN 0 "pc") c con

599598 iLOG (showImp True ty)

600599 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

600+ i <- get

601+ let conn = case con of

602+ PRef _ n -> n

603+ PApp _ (PRef _ n) _ -> n

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

605+ [(n, _)] -> n

606+ _ -> conn

607+ addInstance conn' cfn

608+ addIBC (IBCInstance conn' cfn)

609+-- iputStrLn ("Added " ++ show (conn, cfn))

601610 return [PTy syn fc [] cfn ty,

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

603612

@@ -653,6 +662,7 @@ elabInstance info syn fc cs n ps t ds

653662 [c] -> return c

654663 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

655664 let iname = UN ('@':show n ++ "$" ++ show ps)

665+ addInstance n iname

656666 elabType info syn fc [] iname t

657667 let ips = zip (class_params ci) ps

658668 let ns = case n of

@@ -683,6 +693,7 @@ elabInstance info syn fc cs n ps t ds

683693 [PClause fc iname lhs [] rhs wb]

684694 iLOG (show idecl)

685695 elabDecl info idecl

696+ addIBC (IBCInstance n iname)

686697 where

687698 mkMethApp (n, _, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

688699 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

src/Idris/ElabTerm.hs+14−2

@@ -101,7 +101,9 @@ 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 let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))

104+ = do t <- goal

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

106+ let insts = findInstances ist t

105107 resolveTC 2 fn insts ist

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

107109 instanceArg c

@@ -234,7 +236,9 @@ elab ist info pattern tcgen fn tm

234236 ivs' <- get_instances

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

236238 mapM_ (\n -> do focus n

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

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

240+ t <- goal

241+ let insts = findInstances ist t

238242 resolveTC 7 fn insts ist) (ivs' \\ ivs)

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

240244 tcArg _ = False

@@ -344,6 +348,14 @@ trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf

344348 (MN 0 "tac") (PRef (FC "prf" 0) x))

345349 (tryAll xs)

346350

351+findInstances :: IState -> Term -> [Name]

352+findInstances ist t

353+ | (P _ n _, _) <- unApply t

354+ = case lookupCtxt Nothing n (idris_classes ist) of

355+ [CI _ _ _ _ ins] -> ins

356+ _ -> []

357+ | otherwise = []

358+

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

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

349361resolveTC 1 fn insts ist = try (trivial ist) (resolveTC 0 fn insts ist)

src/Idris/IBC.hs+15−6

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

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 15

24+ibcVersion = 16

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -30,6 +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)],

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

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

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

@@ -48,7 +49,7 @@ deriving instance Binary IBCFile

4849!-}

4950

5051initIBC :: IBCFile

51−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

52+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

5253

5354loadIBC :: FilePath -> Idris ()

5455loadIBC fp = do iLOG $ "Loading ibc " ++ fp

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

8788 = case lookupCtxt Nothing n (idris_classes i) of

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

8990 _ -> fail "IBC write failed"

91+ibc i (IBCInstance n ins) f

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

9093ibc i (IBCDSL n) f

9194 = case lookupCtxt Nothing n (idris_dsls i) of

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

@@ -128,6 +131,7 @@ process i fn

128131 pFixes (ibc_fixes i)

129132 pStatics (ibc_statics i)

130133 pClasses (ibc_classes i)

134+ pInstances (ibc_instances i)

131135 pDSLs (ibc_dsls i)

132136 pDatatypes (ibc_datatypes i)

133137 pOptimise (ibc_optimise i)

@@ -189,6 +193,9 @@ pClasses cs = mapM_ (\ (n, c) ->

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

190194 cs

191195

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

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

198+

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

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

194201 do i <- getIState

@@ -642,7 +649,7 @@ instance Binary Totality where

642649 _ -> error "Corrupted binary data for Totality"

643650

644651instance Binary IBCFile where

645− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20)

652+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21)

646653 = do put x1

647654 put x2

648655 put x3

@@ -663,6 +670,7 @@ instance Binary IBCFile where

663670 put x18

664671 put x19

665672 put x20

673+ put x21

666674 get

667675 = do x1 <- get

668676 if x1 == ibcVersion then

@@ -685,7 +693,8 @@ instance Binary IBCFile where

685693 x18 <- get

686694 x19 <- get

687695 x20 <- get

688− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20)

696+ x21 <- get

697+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21)

689698 else return (initIBC { ver = x1 })

690699

691700instance Binary FnOpt where

@@ -1068,7 +1077,7 @@ instance (Binary t) => Binary (PArg' t) where

10681077

10691078

10701079instance Binary ClassInfo where

1071− put (CI x1 x2 x3 x4)

1080+ put (CI x1 x2 x3 x4 _)

10721081 = do put x1

10731082 put x2

10741083 put x3

@@ -1078,7 +1087,7 @@ instance Binary ClassInfo where

10781087 x2 <- get

10791088 x3 <- get

10801089 x4 <- get

1081− return (CI x1 x2 x3 x4)

1090+ return (CI x1 x2 x3 x4 [])

10821091

10831092instance Binary OptInfo where

10841093 put (Optimise x1 x2 x3)

tutorial/examples/theorems.idr+1−1

@@ -14,7 +14,7 @@ disjoint n p = replace {P = disjointTy} p ()

1414

1515total acyclic : (n : Nat) -> n = S n -> _|_

1616acyclic O p = disjoint _ p

17−acyclic (S k) p = acyclic k _ -- (succInjective _ _ p)

17+acyclic (S k) p = acyclic k (succInjective _ _ p)

1818

1919empty1 : _|_

2020empty1 = hd [] where