2e570a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'default-superclass-instances' of https://github.com/puffnfresh/Idris-dev into puffnfresh-default-superclass-instances

2e570a3Edwin Brady13 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

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

750data ClassInfo = CI { instanceName :: Name,

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

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

753+ class_default_superclasses :: [PDecl],

753 class_params :: [Name],

754 class_params :: [Name],

754 class_instances :: [Name] }

755 class_instances :: [Name] }

755 deriving Show

756 deriving Show

src/Idris/DeepSeq.hs+2−2

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

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

322

323instance NFData ClassInfo where

324− rnf (CI x1 x2 x3 x4 x5)

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

325 = rnf x1 `seq`

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

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

327

328instance NFData OptInfo where

329 rnf (Optimise x1 x2 x3 x4)

src/Idris/ElabDecls.hs+60−16

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

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

1543 -- build data declaration

1544 let mdecls = filter tydecl ds -- method declarations

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

1546+ mapM_ checkDefaultSuperclassInstance idecls

1545 let mnames = map getMName mdecls

1547 let mnames = map getMName mdecls

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

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

1547 ims <- mapM (tdecl mnames) mdecls

1549 ims <- mapM (tdecl mnames) mdecls

@@ -1550,7 +1552,7 @@ elabClass info syn doc fc constraints tn ps ds

1550 let (methods, imethods)

1552 let (methods, imethods)

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

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

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

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

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

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

1554 -- build instance constructor type

1556 -- build instance constructor type

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

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

1556 -- to elsewhere in the class declaration

1558 -- to elsewhere in the class declaration

@@ -1572,7 +1574,6 @@ elabClass info syn doc fc constraints tn ps ds

1572 mapM_ (elabDecl EAll info) (concat fns)

1574 mapM_ (elabDecl EAll info) (concat fns)

1573 -- add the default definitions

1575 -- add the default definitions

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

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

1575− i <- getIState

1576 addIBC (IBCClass tn)

1577 addIBC (IBCClass tn)

1577 where

1578 where

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

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

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

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

1584 mdec (NS x n) = NS (mdec x) n

1584 mdec x = x

1585 mdec x = x

1585

1586

1587+ -- TODO: probably should normalise

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

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

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

1591+ i <- getIState

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

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

1594+ when (not isConstrained) . tclift

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

1596+ return ()

1597+

1586 impbind [] x = x

1598 impbind [] x = x

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

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

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

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

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

1614

1626

1615 tydecl (PTy _ _ _ _ _ _) = True

1627 tydecl (PTy _ _ _ _ _ _) = True

1616 tydecl _ = False

1628 tydecl _ = False

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

1630+ instdecl _ = False

1617 clause (PClauses _ _ _ _) = True

1631 clause (PClauses _ _ _ _) = True

1618 clause _ = False

1632 clause _ = False

1619

1633

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

1699 [c] -> return c

1713 [c] -> return c

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

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

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

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

1702− let iname = case expn of

1716+ let iname = mkiname n ps expn

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

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

1705− Just nm -> nm

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

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

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

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

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

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

1709 case expn of

1720 case expn of

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

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

1711 (class_instances ci)

1722 (class_instances ci)

1712 addInstance intInst n iname

1723 addInstance intInst n iname

1713 Just _ -> addInstance intInst n iname

1724 Just _ -> addInstance intInst n iname

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

1721 PApp _ _ args -> getWParams args

1732 PApp _ _ args -> getWParams args

1722 _ -> return []) ps

1733 _ -> return []) ps

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

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

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

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

1737+ mapM_ (elabDecl EAll info) undefinedSuperclassInstances

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

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

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

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

1726 let t_in = substMatchesShadow ips pnames t

1740 let t_in = substMatchesShadow ips pnames t

@@ -1747,7 +1761,7 @@ elabInstance info syn fc cs n ps t expn ds

1747 let idecls = [PClauses fc [Dictionary] iname

1761 let idecls = [PClauses fc [Dictionary] iname

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

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

1749 iLOG (show idecls)

1763 iLOG (show idecls)

1750− mapM (elabDecl EAll info) idecls

1764+ mapM_ (elabDecl EAll info) idecls

1751 addIBC (IBCInstance intInst n iname)

1765 addIBC (IBCInstance intInst n iname)

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

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

1753-- logLvl 5 $ "Building functions"

1767-- logLvl 5 $ "Building functions"

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

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

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

1759 _ -> False

1773 _ -> False

1760

1774

1761− checkNotOverlapping i t n

1775+ mkiname n' ps' expn' =

1776+ case expn' of

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

1778+ Just nm -> nm

1779+

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

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

1782+

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

1784+ = case lookupCtxtName n (idris_classes i) of

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

1786+ case lookupTy iname (tt_ctxt i) of

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

1788+ (_:_) -> return True

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

1790+

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

1792+ elabFindOverlapping i ci iname syn t

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

1794+ ty' <- implicit syn iname ty'

1795+ let ty = addImpl i ty'

1796+ ctxt <- getContext

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

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

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

1800+ ctxt <- getContext

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

1802+ let nty = normalise ctxt [] cty

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

1804+

1805+ findOverlapping i t n

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

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

1763 | otherwise

1807 | otherwise

1764 = case lookupTy n (tt_ctxt i) of

1808 = case lookupTy n (tt_ctxt i) of

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

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

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

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

1767 case matchClause i tret' tret of

1811 case matchClause i tret' tret of

1768− Right ms -> overlapping tret tret'

1812+ Right ms -> Just tret'

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

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

1770− Right ms -> overlapping tret tret'

1814+ Right ms -> Just tret'

1771− Left _ -> return ()

1815+ Left _ -> Nothing

1772− _ -> return ()

1816+ _ -> Nothing

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

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

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

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

1775 getRetType (PPi _ _ _ sc) = getRetType sc

1819 getRetType (PPi _ _ _ sc) = getRetType sc

1776 getRetType t = t

1820 getRetType t = t

1777

1821

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+8−11

@@ -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

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

1752

1747

1753

1748

1754instance Binary ClassInfo where

1749instance Binary ClassInfo where

1755− put (CI x1 x2 x3 x4 _)

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

1756 = do put x1

1751 = do put x1

1757 put x2

1752 put x2

1758 put x3

1753 put x3

1759 put x4

1754 put x4

1755+ put x5

1760 get

1756 get

1761 = do x1 <- get

1757 = do x1 <- get

1762 x2 <- get

1758 x2 <- get

1763 x3 <- get

1759 x3 <- get

1764 x4 <- get

1760 x4 <- get

1761+ x5 <- get

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

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

1766

1763

1767instance Binary OptInfo where

1764instance Binary OptInfo where

1768 put (Optimise x1 x2 x3 x4)

1765 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