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

commit2e570a38fea36b4f9ba18451addb285fbdb193d7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 12 Dec 2013, 10:04 (13 years ago) parent7cbf0cb 99beed8

8 files changed+108−54

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

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

750750data ClassInfo = CI { instanceName :: Name,

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

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

753+ class_default_superclasses :: [PDecl],

753754 class_params :: [Name],

754755 class_instances :: [Name] }

755756 deriving Show

src/Idris/DeepSeq.hs+2−2

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

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

322322

323323instance NFData ClassInfo where

324− rnf (CI x1 x2 x3 x4 x5)

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

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

327327

328328instance NFData OptInfo where

329329 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

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

15431543 -- build data declaration

15441544 let mdecls = filter tydecl ds -- method declarations

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

1546+ mapM_ checkDefaultSuperclassInstance idecls

15451547 let mnames = map getMName mdecls

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

15471549 ims <- mapM (tdecl mnames) mdecls

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

15501552 let (methods, imethods)

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

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

15541556 -- build instance constructor type

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

15561558 -- to elsewhere in the class declaration

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

15721574 mapM_ (elabDecl EAll info) (concat fns)

15731575 -- add the default definitions

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

1575− i <- getIState

15761577 addIBC (IBCClass tn)

15771578 where

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

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

15831584 mdec (NS x n) = NS (mdec x) n

15841585 mdec x = x

15851586

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+

15861598 impbind [] x = x

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

15881600 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

16141626

16151627 tydecl (PTy _ _ _ _ _ _) = True

16161628 tydecl _ = False

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

1630+ instdecl _ = False

16171631 clause (PClauses _ _ _ _) = True

16181632 clause _ = False

16191633

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

16991713 [c] -> return c

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

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

1702− let iname = case expn of

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

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

1705− Just nm -> nm

1716+ let iname = mkiname n ps expn

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

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

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

17091720 case expn of

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

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

17111722 (class_instances ci)

17121723 addInstance intInst n iname

17131724 Just _ -> addInstance intInst n iname

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

17211732 PApp _ _ args -> getWParams args

17221733 _ -> return []) ps

17231734 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

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

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

17261740 let t_in = substMatchesShadow ips pnames t

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

17471761 let idecls = [PClauses fc [Dictionary] iname

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

17491763 iLOG (show idecls)

1750− mapM (elabDecl EAll info) idecls

1764+ mapM_ (elabDecl EAll info) idecls

17511765 addIBC (IBCInstance intInst n iname)

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

17531767-- logLvl 5 $ "Building functions"

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

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

17591773 _ -> False

17601774

1761− checkNotOverlapping i t n

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

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

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

17631807 | otherwise

17641808 = case lookupTy n (tt_ctxt i) of

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

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

17671811 case matchClause i tret' tret of

1768− Right ms -> overlapping tret tret'

1812+ Right ms -> Just tret'

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

1770− Right ms -> overlapping tret tret'

1771− Left _ -> return ()

1772− _ -> return ()

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

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

1814+ Right ms -> Just tret'

1815+ Left _ -> Nothing

1816+ _ -> Nothing

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

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

17751819 getRetType (PPi _ _ _ sc) = getRetType sc

17761820 getRetType t = t

17771821

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

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

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

17521747

17531748

17541749instance Binary ClassInfo where

1755− put (CI x1 x2 x3 x4 _)

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

17561751 = do put x1

17571752 put x2

17581753 put x3

17591754 put x4

1755+ put x5

17601756 get

17611757 = do x1 <- get

17621758 x2 <- get

17631759 x3 <- get

17641760 x4 <- get

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

1761+ x5 <- get

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

17661763

17671764instance Binary OptInfo where

17681765 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