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

git.iko.soy/Idris-dev

Default superclass intances

This allows code like: data Identity i = Id i class Functor (f : Type -> Type) where map : (a -> b) -> f a -> f b class Functor f => Applicative (f : Type -> Type) where instance Functor f where map f fa = ap (pure f) fa pure : a -> f a ap : f (a -> b) -> f a -> f b instance Applicative Identity where pure = Id ap (Id f) (Id a) = Id (f a) data Nat = Z | S Nat x : Identity Nat x = map S (Id Z) Note the default Functor instance defined as part of the Applicative class. This allows the Identity data type to omit an explicit Functor instance and one gets defined from the Applicative instance. This feature is largely copied from the approach done in She: https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/superclass.html It basically does macro expansion of each default superclass instance (e.g. Functor) when the containing class (e.g. Applicative) gets an instance defined. Currently, default superclass instance definitions are not type-checked, only their macro expansions are. Default superclass instances are limited to being defined for types which are syntactically equal to one of the superclass constraints.

commit99beed88c0963a8d3c7bbc313ffee4876b2bc2f1 authorBrian McKenna <brian@brianmckenna.org> dateTue 10 Dec 2013, 20:18 (13 years ago) parent2f52264

8 files changed+109−55

compare with master

unifiedsplit

src/Core/Evaluate.hs−7 src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+1 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+60−16 src/Idris/ElabTerm.hs+1−1 src/Idris/IBC.hs+9−12 src/Idris/Parser.hs+33−14

src/Core/Evaluate.hs−7

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

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

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

634634

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−

642635-------

643636

644637-- Frozen => doesn't reduce

src/Idris/AbsSyntax.hs+3−3

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

197197addInstance int n i

198198 = do ist <- getIState

199199 case lookupCtxt n (idris_classes ist) of

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

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

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

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

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

204204 putIState $ ist { idris_classes = cs }

205205 where addI i ins | int = i : ins

206206 | chaser n = ins ++ [i]

src/Idris/AbsSyntaxTree.hs+1

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

748748data ClassInfo = CI { instanceName :: Name,

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

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

751+ class_default_superclasses :: [PDecl],

751752 class_params :: [Name],

752753 class_instances :: [Name] }

753754 deriving Show

src/Idris/DeepSeq.hs+2−2

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

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

321321

322322instance NFData ClassInfo where

323− rnf (CI x1 x2 x3 x4 x5)

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

324324 = 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` ()

326326

327327instance NFData OptInfo where

328328 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

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

15421542 -- build data declaration

15431543 let mdecls = filter tydecl ds -- method declarations

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

1545+ mapM_ checkDefaultSuperclassInstance idecls

15441546 let mnames = map getMName mdecls

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

15461548 ims <- mapM (tdecl mnames) mdecls

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

15491551 let (methods, imethods)

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

15511553 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) [])

15531555 -- build instance constructor type

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

15551557 -- to elsewhere in the class declaration

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

15711573 mapM_ (elabDecl EAll info) (concat fns)

15721574 -- add the default definitions

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

1574− i <- getIState

15751576 addIBC (IBCClass tn)

15761577 where

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

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

15821583 mdec (NS x n) = NS (mdec x) n

15831584 mdec x = x

15841585

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+

15851597 impbind [] x = x

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

15871599 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

16131625

16141626 tydecl (PTy _ _ _ _ _ _) = True

16151627 tydecl _ = False

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

1629+ instdecl _ = False

16161630 clause (PClauses _ _ _ _) = True

16171631 clause _ = False

16181632

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

16981712 [c] -> return c

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

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

1701− let iname = case expn of

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

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

1704− Just nm -> nm

1715+ let iname = mkiname n ps expn

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

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

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

17081719 case expn of

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

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

17101721 (class_instances ci)

17111722 addInstance intInst n iname

17121723 Just _ -> addInstance intInst n iname

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

17201731 PApp _ _ args -> getWParams args

17211732 _ -> return []) ps

17221733 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

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

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

17251739 let t_in = substMatchesShadow ips pnames t

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

17461760 let idecls = [PClauses fc [Dictionary] iname

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

17481762 iLOG (show idecls)

1749− mapM (elabDecl EAll info) idecls

1763+ mapM_ (elabDecl EAll info) idecls

17501764 addIBC (IBCInstance intInst n iname)

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

17521766-- logLvl 5 $ "Building functions"

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

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

17581772 _ -> False

17591773

1760− checkNotOverlapping i t n

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

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

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

17621806 | otherwise

17631807 = case lookupTy n (tt_ctxt i) of

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

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

17661810 case matchClause i tret' tret of

1767− Right ms -> overlapping tret tret'

1811+ Right ms -> Just tret'

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

1769− Right ms -> overlapping tret tret'

1770− Left _ -> return ()

1771− _ -> return ()

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

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

1813+ Right ms -> Just tret'

1814+ Left _ -> Nothing

1815+ _ -> Nothing

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

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

17741818 getRetType (PPi _ _ _ sc) = getRetType sc

17751819 getRetType t = t

17761820

src/Idris/ElabTerm.hs+1−1

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

641641findInstances ist t

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

643643 = case lookupCtxt n (idris_classes ist) of

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

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

645645 _ -> []

646646 | otherwise = []

647647

src/Idris/IBC.hs+9−12

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

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 46

26+ibcVersion = 47

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

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

226226 -- could have loaded in any order

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

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

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

229229 _ -> []

230230 let c' = c { class_instances =

231231 class_instances c ++ is }

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

807807 1 -> do x1 <- get

808808 x2 <- get

809809 return (TyDecl x1 x2)

810− 2 -> do x1 <- get

811− x2 <- get

812− x3 <- get

813− return (Operator x1 x2 x3)

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

814811 3 -> do x1 <- get

815812 x2 <- get

816813 x3 <- get

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

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

12471244

12481245instance Binary SyntaxInfo where

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

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

12501247 = do put x1

12511248 put x2

12521249 put x3

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

12541251 put x5

12551252 put x6

12561253 put x7

1257− put x8

12581254 get

12591255 = do x1 <- get

12601256 x2 <- get

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

12631259 x5 <- get

12641260 x6 <- get

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

12681263

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

12701265 put x

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

17481743

17491744

17501745instance Binary ClassInfo where

1751− put (CI x1 x2 x3 x4 _)

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

17521747 = do put x1

17531748 put x2

17541749 put x3

17551750 put x4

1751+ put x5

17561752 get

17571753 = do x1 <- get

17581754 x2 <- get

17591755 x3 <- get

17601756 x4 <- get

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

1757+ x5 <- get

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

17621759

17631760instance Binary OptInfo where

17641761 put (Optimise x1 x2 x3 x4)

src/Idris/Parser.hs+33−14

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

437437 return [PNamespace n (concat ds)]

438438 <?> "namespace declaration"

439439

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

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

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

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

442442 -}

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

444−methodsBlock syn = do reserved "where"

445− openBlock

446− ds <- many (fnDecl syn)

447− closeBlock

448− return (concat ds)

449− <?> "methods block"

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

444+instanceBlock syn = do reserved "where"

445+ openBlock

446+ ds <- many (fnDecl syn)

447+ closeBlock

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)

468+ <?> "class block"

450469

451470{- |Parses a type class declaration

452471

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

456475 ;

457476

458477Class ::=

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

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

460479 ;

461480-}

462481class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

468487 let n = expandNS syn n_in

469488 cs <- many carg

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

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

471490 accData acc n (concatMap declared ds)

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

473492 <?> "type-class declaration"

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

481500{- |Parses a type class instance declaration

482501

483502 Instance ::=

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

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

485504 ;

486505

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

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

494513 args <- many (simpleExpr syn)

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

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

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

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

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

499− <?> "instance declaratioN"

518+ <?> "instance declaration"

500519 where instanceName :: IdrisParser Name

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

502521 let n = expandNS syn n_in