99beed8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Default superclass intances

99beed8Brian McKenna13 years ago

src/Core/Evaluate.hs−7

compare with master

unifiedsplit

@@ -632,13 +632,6 @@ instance Show Def where

632 show ns' ++ " " ++ show sc' ++ "\n\n" ++

633 if inlc then "Inlinable\n" else "Not inlinable\n"

634

635−-- We need this for serialising Def. Fortunately, it never gets used because

636−-- we'll never serialise a primitive operator

637−

638−instance Binary (a -> b) where

639− put x = return ()

640− get = error "Getting a function"

641−

642-------

635-------

643

636

644-- Frozen => doesn't reduce

637-- Frozen => doesn't reduce

src/Idris/AbsSyntax.hs+3−3

@@ -197,10 +197,10 @@ addInstance :: Bool -> Name -> Name -> Idris ()

197addInstance int n i

198 = do ist <- getIState

199 case lookupCtxt n (idris_classes ist) of

200− [CI a b c d ins] ->

200+ [CI a b c d e ins] ->

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

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

202 putIState $ ist { idris_classes = cs }

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

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

204 putIState $ ist { idris_classes = cs }

205 where addI i ins | int = i : ins

206 | chaser n = ins ++ [i]

src/Idris/AbsSyntaxTree.hs+1

@@ -748,6 +748,7 @@ type PArg = PArg' PTerm

748data ClassInfo = CI { instanceName :: Name,

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

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

751+ class_default_superclasses :: [PDecl],

751 class_params :: [Name],

752 class_params :: [Name],

752 class_instances :: [Name] }

753 class_instances :: [Name] }

753 deriving Show

754 deriving Show

src/Idris/DeepSeq.hs+2−2

@@ -320,9 +320,9 @@ instance (NFData t) => NFData (PArg' t) where

320 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

321

322instance NFData ClassInfo where

323− rnf (CI x1 x2 x3 x4 x5)

323+ rnf (CI x1 x2 x3 x4 x5 x6)

324 = rnf x1 `seq`

325− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

325+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

326

327instance NFData OptInfo where

328 rnf (Optimise x1 x2 x3 x4)

src/Idris/ElabDecls.hs+60−16

@@ -1541,6 +1541,8 @@ elabClass info syn doc fc constraints tn ps ds

1541 (map (pexp . PRef fc) (map fst ps))

1542 -- build data declaration

1543 let mdecls = filter tydecl ds -- method declarations

1544+ let idecls = filter instdecl ds -- default superclass instance declarations

1545+ mapM_ checkDefaultSuperclassInstance idecls

1544 let mnames = map getMName mdecls

1546 let mnames = map getMName mdecls

1545 logLvl 2 $ "Building methods " ++ show mnames

1547 logLvl 2 $ "Building methods " ++ show mnames

1546 ims <- mapM (tdecl mnames) mdecls

1548 ims <- mapM (tdecl mnames) mdecls

@@ -1549,7 +1551,7 @@ elabClass info syn doc fc constraints tn ps ds

1549 let (methods, imethods)

1551 let (methods, imethods)

1550 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

1552 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

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

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

1552− addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])

1554+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])

1553 -- build instance constructor type

1555 -- build instance constructor type

1554 -- decorate names of functions to ensure they can't be referred

1556 -- decorate names of functions to ensure they can't be referred

1555 -- to elsewhere in the class declaration

1557 -- to elsewhere in the class declaration

@@ -1571,7 +1573,6 @@ elabClass info syn doc fc constraints tn ps ds

1571 mapM_ (elabDecl EAll info) (concat fns)

1573 mapM_ (elabDecl EAll info) (concat fns)

1572 -- add the default definitions

1574 -- add the default definitions

1573 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

1575 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))

1574− i <- getIState

1575 addIBC (IBCClass tn)

1576 addIBC (IBCClass tn)

1576 where

1577 where

1577 nodoc (n, (_, o, t)) = (n, (o, t))

1578 nodoc (n, (_, o, t)) = (n, (o, t))

@@ -1582,6 +1583,17 @@ elabClass info syn doc fc constraints tn ps ds

1582 mdec (NS x n) = NS (mdec x) n

1583 mdec (NS x n) = NS (mdec x) n

1583 mdec x = x

1584 mdec x = x

1584

1585

1586+ -- TODO: probably should normalise

1587+ checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)

1588+ = do when (not $ null cs) . tclift

1589+ $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

1590+ i <- getIState

1591+ let t = PApp fc (PRef fc n) (map pexp ps)

1592+ let isConstrained = any (== t) constraints

1593+ when (not isConstrained) . tclift

1594+ $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

1595+ return ()

1596+

1585 impbind [] x = x

1597 impbind [] x = x

1586 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

1598 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

1587 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1599 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

@@ -1613,6 +1625,8 @@ elabClass info syn doc fc constraints tn ps ds

1613

1625

1614 tydecl (PTy _ _ _ _ _ _) = True

1626 tydecl (PTy _ _ _ _ _ _) = True

1615 tydecl _ = False

1627 tydecl _ = False

1628+ instdecl (PInstance _ _ _ _ _ _ _ _) = True

1629+ instdecl _ = False

1616 clause (PClauses _ _ _ _) = True

1630 clause (PClauses _ _ _ _) = True

1617 clause _ = False

1631 clause _ = False

1618

1632

@@ -1698,15 +1712,12 @@ elabInstance info syn fc cs n ps t expn ds

1698 [c] -> return c

1712 [c] -> return c

1699 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

1713 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

1700 let constraint = PApp fc (PRef fc n) (map pexp ps)

1714 let constraint = PApp fc (PRef fc n) (map pexp ps)

1701− let iname = case expn of

1715+ let iname = mkiname n ps expn

1702− Nothing -> SN (InstanceN n (map show ps))

1703− -- UN ('@':show n ++ "$" ++ show ps)

1704− Just nm -> nm

1705 nty <- elabType' True info syn "" fc [] iname t

1716 nty <- elabType' True info syn "" fc [] iname t

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

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

1707 -- and it's not a named instance, then it's overlapping, so report an error

1718 -- and it's not a named instance, then it's overlapping, so report an error

1708 case expn of

1719 case expn of

1709− Nothing -> do mapM_ (checkNotOverlapping i (delab i nty))

1720+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))

1710 (class_instances ci)

1721 (class_instances ci)

1711 addInstance intInst n iname

1722 addInstance intInst n iname

1712 Just _ -> addInstance intInst n iname

1723 Just _ -> addInstance intInst n iname

@@ -1720,6 +1731,9 @@ elabInstance info syn fc cs n ps t expn ds

1720 PApp _ _ args -> getWParams args

1731 PApp _ _ args -> getWParams args

1721 _ -> return []) ps

1732 _ -> return []) ps

1722 let pnames = map pname (concat (nub wparams))

1733 let pnames = map pname (concat (nub wparams))

1734+ let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

1735+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances

1736+ mapM_ (elabDecl EAll info) undefinedSuperclassInstances

1723 let all_meths = map (nsroot . fst) (class_methods ci)

1737 let all_meths = map (nsroot . fst) (class_methods ci)

1724 let mtys = map (\ (n, (op, t)) ->

1738 let mtys = map (\ (n, (op, t)) ->

1725 let t_in = substMatchesShadow ips pnames t

1739 let t_in = substMatchesShadow ips pnames t

@@ -1746,7 +1760,7 @@ elabInstance info syn fc cs n ps t expn ds

1746 let idecls = [PClauses fc [Dictionary] iname

1760 let idecls = [PClauses fc [Dictionary] iname

1747 [PClause fc iname lhs [] rhs wb]]

1761 [PClause fc iname lhs [] rhs wb]]

1748 iLOG (show idecls)

1762 iLOG (show idecls)

1749− mapM (elabDecl EAll info) idecls

1763+ mapM_ (elabDecl EAll info) idecls

1750 addIBC (IBCInstance intInst n iname)

1764 addIBC (IBCInstance intInst n iname)

1751-- -- for each constraint, build a top level function to chase it

1765-- -- for each constraint, build a top level function to chase it

1752-- logLvl 5 $ "Building functions"

1766-- logLvl 5 $ "Building functions"

@@ -1757,20 +1771,50 @@ elabInstance info syn fc cs n ps t expn ds

1757 [PConstant (AType (ATInt ITNative))] -> True

1771 [PConstant (AType (ATInt ITNative))] -> True

1758 _ -> False

1772 _ -> False

1759

1773

1760− checkNotOverlapping i t n

1774+ mkiname n' ps' expn' =

1775+ case expn' of

1776+ Nothing -> SN (InstanceN n' (map show ps'))

1777+ Just nm -> nm

1778+

1779+ substInstance ips pnames (PInstance syn _ cs n ps t expn ds)

1780+ = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

1781+

1782+ isOverlapping i (PInstance syn _ _ n ps t expn _)

1783+ = case lookupCtxtName n (idris_classes i) of

1784+ [(n, ci)] -> let iname = (mkiname n ps expn) in

1785+ case lookupTy iname (tt_ctxt i) of

1786+ [] -> elabFindOverlapping i ci iname syn t

1787+ (_:_) -> return True

1788+ _ -> return False -- couldn't find class, just let elabInstance fail later

1789+

1790+ -- TODO: largely based upon elabType' - should try to abstract

1791+ elabFindOverlapping i ci iname syn t

1792+ = do ty' <- addUsingConstraints syn fc t

1793+ ty' <- implicit syn iname ty'

1794+ let ty = addImpl i ty'

1795+ ctxt <- getContext

1796+ ((tyT, _, _), _) <-

1797+ tclift $ elaborate ctxt iname (TType (UVal 0)) []

1798+ (errAt "type of " iname (erun fc (build i info False iname ty)))

1799+ ctxt <- getContext

1800+ (cty, _) <- recheckC fc [] tyT

1801+ let nty = normalise ctxt [] cty

1802+ return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)

1803+

1804+ findOverlapping i t n

1761− | take 2 (show n) == "@@" = return ()

1805+ | take 2 (show n) == "@@" = Nothing

1762 | otherwise

1806 | otherwise

1763 = case lookupTy n (tt_ctxt i) of

1807 = case lookupTy n (tt_ctxt i) of

1764 [t'] -> let tret = getRetType t

1808 [t'] -> let tret = getRetType t

1765 tret' = getRetType (delab i t') in

1809 tret' = getRetType (delab i t') in

1766 case matchClause i tret' tret of

1810 case matchClause i tret' tret of

1767− Right ms -> overlapping tret tret'

1811+ Right ms -> Just tret'

1768 Left _ -> case matchClause i tret tret' of

1812 Left _ -> case matchClause i tret tret' of

1769− Right ms -> overlapping tret tret'

1813+ Right ms -> Just tret'

1770− Left _ -> return ()

1814+ Left _ -> Nothing

1771− _ -> return ()

1815+ _ -> Nothing

1772− overlapping t t' = tclift $ tfail (At fc (Msg $

1816+ overlapping t' = tclift $ tfail (At fc (Msg $

1773− "Overlapping instance: " ++ show t' ++ " already defined"))

1817+ "Overlapping instance: " ++ show t' ++ " already defined"))

1774 getRetType (PPi _ _ _ sc) = getRetType sc

1818 getRetType (PPi _ _ _ sc) = getRetType sc

1775 getRetType t = t

1819 getRetType t = t

1776

1820

src/Idris/ElabTerm.hs+1−1

@@ -641,7 +641,7 @@ findInstances :: IState -> Term -> [Name]

641findInstances ist t

642 | (P _ n _, _) <- unApply t

643 = case lookupCtxt n (idris_classes ist) of

644− [CI _ _ _ _ ins] -> ins

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

645 _ -> []

646 | otherwise = []

647

src/Idris/IBC.hs+9−12

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 46

26+ibcVersion = 47

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -225,7 +225,7 @@ pClasses cs = mapM_ (\ (n, c) ->

225 -- Don't lose instances from previous IBCs, which

226 -- could have loaded in any order

227 let is = case lookupCtxt n (idris_classes i) of

228− [CI _ _ _ _ ins] -> ins

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

229 _ -> []

230 let c' = c { class_instances =

231 class_instances c ++ is }

@@ -807,10 +807,7 @@ instance Binary Def where

807 1 -> do x1 <- get

808 x2 <- get

809 return (TyDecl x1 x2)

810− 2 -> do x1 <- get

810+ -- Operator isn't written, don't read

811− x2 <- get

812− x3 <- get

813− return (Operator x1 x2 x3)

814 3 -> do x1 <- get

811 3 -> do x1 <- get

815 x2 <- get

812 x2 <- get

816 x3 <- get

813 x3 <- get

@@ -1246,7 +1243,7 @@ instance Binary Using where

1246 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1243 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

1247

1244

1248instance Binary SyntaxInfo where

1245instance Binary SyntaxInfo where

1249− put (Syn x1 x2 x3 x4 x5 x6 x7 x8)

1246+ put (Syn x1 x2 x3 x4 _ x5 x6 x7)

1250 = do put x1

1247 = do put x1

1251 put x2

1248 put x2

1252 put x3

1249 put x3

@@ -1254,7 +1251,6 @@ instance Binary SyntaxInfo where

1254 put x5

1251 put x5

1255 put x6

1252 put x6

1256 put x7

1253 put x7

1257− put x8

1258 get

1254 get

1259 = do x1 <- get

1255 = do x1 <- get

1260 x2 <- get

1256 x2 <- get

@@ -1263,8 +1259,7 @@ instance Binary SyntaxInfo where

1263 x5 <- get

1259 x5 <- get

1264 x6 <- get

1260 x6 <- get

1265 x7 <- get

1261 x7 <- get

1266− x8 <- get

1267− return (Syn x1 x2 x3 x4 x5 x6 x7 x8)

1262+ return (Syn x1 x2 x3 x4 id x5 x6 x7)

1268

1263

1269instance (Binary t) => Binary (PClause' t) where

1264instance (Binary t) => Binary (PClause' t) where

1270 put x

1265 put x

@@ -1748,17 +1743,19 @@ instance (Binary t) => Binary (PArg' t) where

1748

1743

1749

1744

1750instance Binary ClassInfo where

1745instance Binary ClassInfo where

1751− put (CI x1 x2 x3 x4 _)

1746+ put (CI x1 x2 x3 x4 x5 _)

1752 = do put x1

1747 = do put x1

1753 put x2

1748 put x2

1754 put x3

1749 put x3

1755 put x4

1750 put x4

1751+ put x5

1756 get

1752 get

1757 = do x1 <- get

1753 = do x1 <- get

1758 x2 <- get

1754 x2 <- get

1759 x3 <- get

1755 x3 <- get

1760 x4 <- get

1756 x4 <- get

1757+ x5 <- get

1761− return (CI x1 x2 x3 x4 [])

1758+ return (CI x1 x2 x3 x4 x5 [])

1762

1759

1763instance Binary OptInfo where

1760instance Binary OptInfo where

1764 put (Optimise x1 x2 x3 x4)

1761 put (Optimise x1 x2 x3 x4)

src/Idris/Parser.hs+33−14

@@ -437,16 +437,35 @@ namespace syn =

437 return [PNamespace n (concat ds)]

438 <?> "namespace declaration"

439

440−{- |Parses a methods block (for type classes and instances)

440+{- |Parses a methods block (for instances)

441− MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock

441+ InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

442 -}

443−methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]

443+instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

444−methodsBlock syn = do reserved "where"

444+instanceBlock syn = do reserved "where"

445− openBlock

445+ openBlock

446− ds <- many (fnDecl syn)

446+ ds <- many (fnDecl syn)

447− closeBlock

447+ closeBlock

448− return (concat ds)

448+ return (concat ds)

449+ <?> "instance block"

450+

451+{- |Parses a methods and instances block (for type classes)

452+

453+MethodOrInstance ::=

454+ FnDecl

455+ | Instance

456+ ;

457+

458+ClassBlock ::=

459+ 'where' OpenBlock MethodOrInstance* CloseBlock

460+ ;

461+-}

462+classBlock :: SyntaxInfo -> IdrisParser [PDecl]

463+classBlock syn = do reserved "where"

464+ openBlock

465+ ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)

466+ closeBlock

467+ return (concat ds)

449− <?> "methods block"

468+ <?> "class block"

450

469

451{- |Parses a type class declaration

470{- |Parses a type class declaration

452

471

@@ -456,7 +475,7 @@ ClassArgument ::=

456 ;

475 ;

457

476

458Class ::=

477Class ::=

459− DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?

478+ DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?

460 ;

479 ;

461-}

480-}

462class_ :: SyntaxInfo -> IdrisParser [PDecl]

481class_ :: SyntaxInfo -> IdrisParser [PDecl]

@@ -467,7 +486,7 @@ class_ syn = do (doc, acc) <- try (do

467 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name

486 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name

468 let n = expandNS syn n_in

487 let n = expandNS syn n_in

469 cs <- many carg

488 cs <- many carg

470− ds <- option [] (methodsBlock syn)

489+ ds <- option [] (classBlock syn)

471 accData acc n (concatMap declared ds)

490 accData acc n (concatMap declared ds)

472 return [PClass doc syn fc cons n cs ds]

491 return [PClass doc syn fc cons n cs ds]

473 <?> "type-class declaration"

492 <?> "type-class declaration"

@@ -481,7 +500,7 @@ class_ syn = do (doc, acc) <- try (do

481{- |Parses a type class instance declaration

500{- |Parses a type class instance declaration

482

501

483 Instance ::=

502 Instance ::=

484− 'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?

503+ 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

485 ;

504 ;

486

505

487 InstanceName ::= '[' Name ']';

506 InstanceName ::= '[' Name ']';

@@ -494,9 +513,9 @@ instance_ syn = do reserved "instance"; fc <- getFC

494 args <- many (simpleExpr syn)

513 args <- many (simpleExpr syn)

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

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

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

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

497− ds <- option [] (methodsBlock syn)

516+ ds <- option [] (instanceBlock syn)

498 return [PInstance syn fc cs cn args t en ds]

517 return [PInstance syn fc cs cn args t en ds]

499− <?> "instance declaratioN"

518+ <?> "instance declaration"

500 where instanceName :: IdrisParser Name

519 where instanceName :: IdrisParser Name

501 instanceName = do lchar '['; n_in <- fnName; lchar ']'

520 instanceName = do lchar '['; n_in <- fnName; lchar ']'

502 let n = expandNS syn n_in

521 let n = expandNS syn n_in