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

git.iko.soy/Idris-dev

on master help sign in

Better type class resolution

58bcd1eEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+21−1

compare with master

unifiedsplit

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

74 | IBCImp Name

75 | IBCStatic Name

76 | IBCClass Name

77+ | IBCInstance Name Name

77 | IBCDSL Name

78 | IBCDSL Name

78 | IBCData Name

79 | IBCData Name

79 | IBCOpt Name

80 | IBCOpt Name

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

147addToCG n ns = do i <- get

148addToCG n ns = do i <- get

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

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

149

150

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+

150addIBC :: IBCWrite -> Idris ()

169addIBC :: IBCWrite -> Idris ()

151addIBC ibc@(IBCDef n)

170addIBC ibc@(IBCDef n)

152 = do i <- get

171 = do i <- get

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

581data ClassInfo = CI { instanceName :: Name,

600data ClassInfo = CI { instanceName :: Name,

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

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

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

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

584− class_params :: [Name] }

603+ class_params :: [Name],

604+ class_instances :: [Name] }

585 deriving Show

605 deriving Show

586{-!

606{-!

587deriving instance Binary ClassInfo

607deriving instance Binary ClassInfo

src/Idris/ElabDecls.hs+13−2

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

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

553 i <- get

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

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

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

556− (idris_classes i) })

557 addIBC (IBCClass tn)

556 addIBC (IBCClass tn)

558 where

557 where

559 pibind [] x = x

558 pibind [] x = x

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

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

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

599 iLOG (showImp True ty)

598 iLOG (showImp True ty)

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

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

601 return [PTy syn fc [] cfn ty,

610 return [PTy syn fc [] cfn ty,

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

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

603

612

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

653 [c] -> return c

662 [c] -> return c

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

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

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

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

665+ addInstance n iname

656 elabType info syn fc [] iname t

666 elabType info syn fc [] iname t

657 let ips = zip (class_params ci) ps

667 let ips = zip (class_params ci) ps

658 let ns = case n of

668 let ns = case n of

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

683 [PClause fc iname lhs [] rhs wb]

693 [PClause fc iname lhs [] rhs wb]

684 iLOG (show idecl)

694 iLOG (show idecl)

685 elabDecl info idecl

695 elabDecl info idecl

696+ addIBC (IBCInstance n iname)

686 where

697 where

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

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

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

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

src/Idris/ElabTerm.hs+14−2

@@ -101,7 +101,9 @@ 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

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

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

106+ let insts = findInstances ist t

105 resolveTC 2 fn insts ist

107 resolveTC 2 fn insts ist

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

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

107 instanceArg c

109 instanceArg c

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

234 ivs' <- get_instances

236 ivs' <- get_instances

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

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

236 mapM_ (\n -> do focus n

238 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

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

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

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

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

240 tcArg _ = False

244 tcArg _ = False

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

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

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

345 (tryAll xs)

349 (tryAll xs)

346

350

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+

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

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

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

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

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

361resolveTC 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

21import Paths_idris

23ibcVersion :: Word8

24−ibcVersion = 15

24+ibcVersion = 16

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

@@ -30,6 +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_dsls :: [(Name, DSL)],

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

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

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

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

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

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

48!-}

49!-}

50initIBC :: IBCFile

51initIBC :: IBCFile

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

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

53loadIBC :: FilePath -> Idris ()

54loadIBC :: FilePath -> Idris ()

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

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

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

87 = case lookupCtxt Nothing n (idris_classes i) of

88 = case lookupCtxt Nothing n (idris_classes i) of

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

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

89 _ -> fail "IBC write failed"

90 _ -> fail "IBC write failed"

91+ibc i (IBCInstance n ins) f

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

90ibc i (IBCDSL n) f

93ibc i (IBCDSL n) f

91 = case lookupCtxt Nothing n (idris_dsls i) of

94 = case lookupCtxt Nothing n (idris_dsls i) of

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

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

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

128 pFixes (ibc_fixes i)

131 pFixes (ibc_fixes i)

129 pStatics (ibc_statics i)

132 pStatics (ibc_statics i)

130 pClasses (ibc_classes i)

133 pClasses (ibc_classes i)

134+ pInstances (ibc_instances i)

131 pDSLs (ibc_dsls i)

135 pDSLs (ibc_dsls i)

132 pDatatypes (ibc_datatypes i)

136 pDatatypes (ibc_datatypes i)

133 pOptimise (ibc_optimise i)

137 pOptimise (ibc_optimise i)

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

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

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

190 cs

194 cs

191

195

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

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

198+

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

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

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

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

194 do i <- getIState

201 do i <- getIState

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

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

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

643

650

644instance Binary IBCFile where

651instance 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)

646 = do put x1

653 = do put x1

647 put x2

654 put x2

648 put x3

655 put x3

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

663 put x18

670 put x18

664 put x19

671 put x19

665 put x20

672 put x20

673+ put x21

666 get

674 get

667 = do x1 <- get

675 = do x1 <- get

668 if x1 == ibcVersion then

676 if x1 == ibcVersion then

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

685 x18 <- get

693 x18 <- get

686 x19 <- get

694 x19 <- get

687 x20 <- get

695 x20 <- get

696+ x21 <- get

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

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

689 else return (initIBC { ver = x1 })

698 else return (initIBC { ver = x1 })

690

699

691instance Binary FnOpt where

700instance Binary FnOpt where

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

1068

1077

1069

1078

1070instance Binary ClassInfo where

1079instance Binary ClassInfo where

1071− put (CI x1 x2 x3 x4)

1080+ put (CI x1 x2 x3 x4 _)

1072 = do put x1

1081 = do put x1

1073 put x2

1082 put x2

1074 put x3

1083 put x3

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

1078 x2 <- get

1087 x2 <- get

1079 x3 <- get

1088 x3 <- get

1080 x4 <- get

1089 x4 <- get

1081− return (CI x1 x2 x3 x4)

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

1082

1091

1083instance Binary OptInfo where

1092instance Binary OptInfo where

1084 put (Optimise x1 x2 x3)

1093 put (Optimise x1 x2 x3)

tutorial/examples/theorems.idr+1−1

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

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

16acyclic O p = disjoint _ p

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

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

19empty1 : _|_

20empty1 = hd [] where