75ab155 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -40,6 +40,8 @@ New in 0.9.18:

40 type classes. See the updated tutorial for details.

41* Records can be coinductive. Define coinductive records with the "corecord"

42 keyword.

43+* Type class constructors can be assigned user-accessible names. This is done

44+ using the same syntax as record constructors.

43* if ... then ... else ... is now built-in syntax instead of being defined in

45* if ... then ... else ... is now built-in syntax instead of being defined in

44 a library. It is shown in REPL output and error messages, rather than its

46 a library. It is shown in REPL output and error messages, rather than its

45 desugaring.

47 desugaring.

@@ -47,6 +49,7 @@ New in 0.9.18:

47 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and

49 boolElim. This is for consistency with GHC Haskell and scala-virtualized, and

48 to reflect that if-notation makes sense with non-Bool datatypes.

50 to reflect that if-notation makes sense with non-Bool datatypes.

49

51

52+

50New in 0.9.17:

53New in 0.9.17:

51--------------

54--------------

52* The --ideslave command line option has been replaced with a --ide-mode

55* The --ideslave command line option has been replaced with a --ide-mode

idris.cabal+5

@@ -357,6 +357,11 @@ Extra-source-files:

357 test/bignum002/*.idr

358 test/bignum002/expected

359

360+ test/classes001/*.idr

361+ test/classes001/run

362+ test/classes001/expected

363+ test/classes001/input

364+

360 test/corecords001/*.idr

365 test/corecords001/*.idr

361 test/corecords001/run

366 test/corecords001/run

362 test/corecords001/expected

367 test/corecords001/expected

src/Idris/AbsSyntax.hs+3−1

@@ -1101,7 +1101,7 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

1101-- (map (expandParamsD ist dec ps ns) pds)

1102expandParamsD rhs ist dec ps ns (PMutual f pds)

1103 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1104−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

1104+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls cn cd)

1105 = PClass doc info f

1106 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1107 n

@@ -1109,6 +1109,8 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

1109 pDocs

1110 fds

1111 (map (expandParamsD rhs ist dec ps ns) decls)

1112+ cn

1113+ cd

1112expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1114expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

1113 = PInstance doc argDocs info f

1115 = PInstance doc argDocs info f

1114 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

1116 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

src/Idris/AbsSyntaxTree.hs+9−7

@@ -612,13 +612,15 @@ data PDecl' t

612 -- ^ Record declaration

613 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

614 [(Name, t)] -- constraints

615− Name

615+ Name -- class name

616 [(Name, t)] -- parameters

617 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

618 [Name] -- determining parameters

619 [PDecl' t] -- declarations

620+ (Maybe Name) -- instance constructor name

621+ (Docstring (Either Err PTerm)) -- instance constructor docs

620 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

622 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

621− -- class name, parameters, method declarations

623+ -- class name, parameters, method declarations, optional constructor name

622 | PInstance

624 | PInstance

623 (Docstring (Either Err PTerm)) -- Instance docs

625 (Docstring (Either Err PTerm)) -- Instance docs

624 [(Name, Docstring (Either Err PTerm))] -- Parameter docs

626 [(Name, Docstring (Either Err PTerm))] -- Parameter docs

@@ -733,7 +735,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

733declared (PParams _ _ ds) = concatMap declared ds

735declared (PParams _ _ ds) = concatMap declared ds

734declared (PNamespace _ ds) = concatMap declared ds

736declared (PNamespace _ ds) = concatMap declared ds

735declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

737declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

736−declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms

738+declared (PClass _ _ _ _ n _ _ _ ms cn cd) = n : (maybeToList cn ++ concatMap declared ms)

737declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

739declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

738declared (PDSL n _) = [n]

740declared (PDSL n _) = [n]

739declared (PSyntax _ _) = []

741declared (PSyntax _ _) = []

@@ -753,7 +755,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

753tldeclared (PParams _ _ ds) = []

755tldeclared (PParams _ _ ds) = []

754tldeclared (PMutual _ ds) = concatMap tldeclared ds

756tldeclared (PMutual _ ds) = concatMap tldeclared ds

755tldeclared (PNamespace _ ds) = concatMap tldeclared ds

757tldeclared (PNamespace _ ds) = concatMap tldeclared ds

756−tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms

758+tldeclared (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap tldeclared ms)

757tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

759tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

758tldeclared _ = []

760tldeclared _ = []

759

761

@@ -769,7 +771,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

769defined (PParams _ _ ds) = concatMap defined ds

771defined (PParams _ _ ds) = concatMap defined ds

770defined (PNamespace _ ds) = concatMap defined ds

772defined (PNamespace _ ds) = concatMap defined ds

771defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

773defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

772−defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms

774+defined (PClass _ _ _ _ n _ _ _ ms cn _) = n : (maybeToList cn ++ concatMap defined ms)

773defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

775defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

774defined (PDSL n _) = [n]

776defined (PDSL n _) = [n]

775defined (PSyntax _ _) = []

777defined (PSyntax _ _) = []

@@ -1070,7 +1072,7 @@ highestFC (PQuoteName _) = Nothing

1070

1072

1071-- Type class data

1073-- Type class data

1072

1074

1073−data ClassInfo = CI { instanceName :: Name,

1075+data ClassInfo = CI { instanceCtorName :: Name,

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

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

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

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

1076 class_default_superclasses :: [PDecl],

1078 class_default_superclasses :: [PDecl],

@@ -1782,7 +1784,7 @@ showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1782showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1784showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1783showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1785showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1784showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1786showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1785−showDeclImp o (PClass _ _ _ cs n ps _ _ ds)

1787+showDeclImp o (PClass _ _ _ cs n ps _ _ ds _ _)

1786 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1788 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1787showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1789showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

1788 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1790 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

src/Idris/DeepSeq.hs+8−2

@@ -150,10 +150,16 @@ instance (NFData t) => NFData (PDecl' t) where

150 rnf x2 `seq`

151 rnf x3 `seq`

152 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

153− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)

153+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11)

154 = rnf x1 `seq`

155 rnf x2 `seq`

156− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

156+ rnf x3 `seq`

157+ rnf x4 `seq`

158+ rnf x5 `seq`

159+ rnf x6 `seq`

160+ rnf x7 `seq`

161+ rnf x8 `seq`

162+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

157 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

163 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

158 = rnf x1 `seq`

164 = rnf x1 `seq`

159 rnf x2 `seq`

165 rnf x2 `seq`

src/Idris/Docs.hs+13−1

@@ -40,6 +40,7 @@ data Docs' d = FunDoc (FunDoc' d)

40 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs

41 [PTerm] -- subclasses

42 [PTerm] -- superclasses

43+ (Maybe (FunDoc' d)) -- explicit constructor

43 | NamedInstanceDoc Name (FunDoc' d) -- name is class

44 | NamedInstanceDoc Name (FunDoc' d) -- name is class

44 | ModDoc [String] -- Module name

45 | ModDoc [String] -- Module name

45 d

46 d

@@ -95,7 +96,7 @@ pprintDocs ist (DataDoc t args)

95 if null args then text "No constructors."

96 if null args then text "No constructors."

96 else nest 4 (text "Constructors:" <> line <>

97 else nest 4 (text "Constructors:" <> line <>

97 vsep (map (pprintFD ist) args))

98 vsep (map (pprintFD ist) args))

98−pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

99+pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)

99 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

100 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

100 if nullDocstring doc

101 if nullDocstring doc

101 then empty

102 then empty

@@ -106,6 +107,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

106 nest 4 (text "Methods:" <$>

107 nest 4 (text "Methods:" <$>

107 vsep (map (pprintFD ist) meths))

108 vsep (map (pprintFD ist) meths))

108 <$>

109 <$>

110+ maybe empty

111+ ((<> line) . nest 4 .

112+ (text "Instance constructor:" <$>) .

113+ pprintFD ist)

114+ ctor

115+ <>

109 nest 4 (text "Instances:" <$>

116 nest 4 (text "Instances:" <$>

110 vsep (if null instances then [text "<no instances>"]

117 vsep (if null instances then [text "<no instances>"]

111 else map pprintInstance normalInstances))

118 else map pprintInstance normalInstances))

@@ -251,9 +258,14 @@ docClass n ci

251 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances

258 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances

252 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

253 mdocs <- mapM (docFun . fst) (class_methods ci)

260 mdocs <- mapM (docFun . fst) (class_methods ci)

261+ let ctorN = instanceCtorName ci

262+ ctorDocs <- case basename ctorN of

263+ SN _ -> return Nothing

264+ _ -> fmap Just $ docFun ctorN

254 return $ ClassDoc

265 return $ ClassDoc

255 n docstr mdocs params

266 n docstr mdocs params

256 instances' (map (\(_,tm,_) -> tm) subclasses) superclasses

267 instances' (map (\(_,tm,_) -> tm) subclasses) superclasses

268+ ctorDocs

257 where

269 where

258 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

270 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

259 namedInst n@(UN _) = Just n

271 namedInst n@(UN _) = Just n

src/Idris/Elab/Class.hs+17−5

@@ -54,10 +54,13 @@ data MArgTy = IA Name | EA Name | CA deriving Show

54

55elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

56 FC -> [(Name, PTerm)] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58− [Name] -> [PDecl] -> Idris ()

58+ [Name] -> [PDecl] ->

59+ Maybe Name {- ^ instance ctor name -} ->

60+ Docstring (Either Err PTerm) {- ^ instance ctor docs -} ->

61+ Idris ()

59−elabClass info syn_in doc fc constraints tn ps pDocs fds ds

62+elabClass info syn_in doc fc constraints tn ps pDocs fds ds mcn cd

60− = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

63+ = do let cn = fromMaybe (SN (InstanceCtorN tn)) mcn

61 let tty = pibind ps PType

64 let tty = pibind ps PType

62 let constraint = PApp fc (PRef fc tn)

65 let constraint = PApp fc (PRef fc tn)

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

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

@@ -80,7 +83,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

80 let cty = impbind ps $ conbind constraints

83 let cty = impbind ps $ conbind constraints

81 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

84 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

82 constraint

85 constraint

83− let cons = [(emptyDocstring, [], cn, cty, fc, [])]

86+ let cons = [(cd, pDocs ++ mapMaybe memberDocs ds, cn, cty, fc, [])]

84 let ddecl = PDatadecl tn tty cons

87 let ddecl = PDatadecl tn tty cons

85 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

88 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

86 -- Elaborate the data declaration

89 -- Elaborate the data declaration

@@ -243,6 +246,15 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

243 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

246 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

244 toExp ns e sc = sc

247 toExp ns e sc = sc

245

248

249+memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

250+memberDocs (PTy d _ _ _ _ n _) = Just (basename n, d)

251+memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

252+memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)

253+memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ ) = Just (basename n, d)

254+memberDocs (PClass d _ _ _ n _ _ _ _ _ _) = Just (basename n, d)

255+memberDocs _ = Nothing

256+

257+

246-- In a top level type for a method, expand all the method names namespaces

258-- In a top level type for a method, expand all the method names namespaces

247-- so that we don't have to disambiguate later

259-- so that we don't have to disambiguate later

248expandMethNS :: SyntaxInfo

260expandMethNS :: SyntaxInfo

src/Idris/Elab/Instance.hs+1−1

@@ -130,7 +130,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

130-- let lhs = PRef fc iname

131 let lhs = PApp fc (PRef fc iname)

132 (map (\n -> pimp n (PRef fc n) True) headVars)

133− let rhs = PApp fc (PRef fc (instanceName ci))

133+ let rhs = PApp fc (PRef fc (instanceCtorName ci))

134 (map (pexp . mkMethApp) mtys)

135

136 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

src/Idris/ElabDecls.hs+2−2

@@ -232,10 +232,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

232 ninfo = case namespace info of

233 Nothing -> info { namespace = Just [n] }

234 Just ns -> info { namespace = Just (n:ns) }

235−elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

235+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds cn cd)

236 | what /= EDefns

237 = do iLOG $ "Elaborating class " ++ show n

238− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

238+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds cn cd

239elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

240 = do iLOG $ "Elaborating instance " ++ show n

241 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/IBC.hs+6−2

@@ -1186,7 +1186,7 @@ instance (Binary t) => Binary (PDecl' t) where

1186 put x9

1187 put x10

1188 put x11

1189− PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

1189+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11

1190 -> do putWord8 7

1191 put x1

1192 put x2

@@ -1197,6 +1197,8 @@ instance (Binary t) => Binary (PDecl' t) where

1197 put x7

1198 put x8

1199 put x9

1200+ put x10

1201+ put x11

1200 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1202 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1201 do putWord8 8

1203 do putWord8 8

1202 put x1

1204 put x1

@@ -1299,7 +1301,9 @@ instance (Binary t) => Binary (PDecl' t) where

1299 x7 <- get

1301 x7 <- get

1300 x8 <- get

1302 x8 <- get

1301 x9 <- get

1303 x9 <- get

1304+ x10 <- get

1305+ x11 <- get

1302− return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

1306+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

1303 8 -> do x1 <- get

1307 8 -> do x1 <- get

1304 x2 <- get

1308 x2 <- get

1305 x3 <- get

1309 x3 <- get

src/Idris/IdrisDoc.hs+13−13

@@ -166,11 +166,11 @@ removeOrphans :: [NsItem] -- ^ List to remove orphans from

166 -> [NsItem] -- ^ Orphan-free list

167removeOrphans list =

168 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

169− in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

169+ in filter ((flip S.notMember children) . (\(n, _, _) -> n)) list

170

171− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

171+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

172− names (Just (ClassDoc _ _ fds _ _ _ _)) = map (\(FD n _ _ _ _) -> n) fds

172+ names (Just (ClassDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

173− names _ = []

173+ names _ = []

174

175-- | Whether a Name names something which should be documented

176filterName :: Name -- ^ Name to check

@@ -218,13 +218,13 @@ referredNss (n, Just d, _) =

218 names = concatMap (extractPTermNames) ts

219 in S.map getNs $ S.fromList names

220

221− where getFunDocs (FunDoc f) = [f]

221+ where getFunDocs (FunDoc f) = [f]

222− getFunDocs (DataDoc f fs) = f:fs

222+ getFunDocs (DataDoc f fs) = f:fs

223− getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs

223+ getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

224− getFunDocs (NamedInstanceDoc _ fd) = [fd]

224+ getFunDocs (NamedInstanceDoc _ fd) = [fd]

225− getFunDocs (ModDoc _ _) = []

225+ getFunDocs (ModDoc _ _) = []

226− types (FD _ _ args t _) = t:(map second args)

226+ types (FD _ _ args t _) = t:(map second args)

227− second (_, x, _, _) = x

227+ second (_, x, _, _) = x

228

229

230-- | Returns an NsDict of containing all known namespaces and their contents

@@ -579,7 +579,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

579 -> H.Html -- ^ Resulting HTML

580createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

581

582−createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

582+createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do

583 H.dt ! (A.id $ toValue $ show n) $ do

584 H.span ! class_ "word" $ do "class"; nbsp

585 H.span ! class_ "name type"

@@ -588,7 +588,7 @@ createOtherDoc ist (ClassDoc n docstring fds _ _ _ _) = do

588 H.span ! class_ "signature" $ nbsp

589 H.dd $ do

590 (if nullDocstring docstring then Empty else Docstrings.renderHtml docstring)

591− H.dl ! class_ "decls" $ forM_ fds (createFunDoc ist)

591+ H.dl ! class_ "decls" $ (forM_ (maybeToList c ++ fds) (createFunDoc ist))

592

593 where name (NS n ns) = show (NS (sUN $ name n) ns)

594 name n = let n' = show n

src/Idris/ParseData.hs+2−3

@@ -89,7 +89,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

89 fields <- many . indented $ field syn

90

91 return (fields, constructorName, constructorDoc')

92− where

92+ where

93 field :: SyntaxInfo -> IdrisParser ((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

94 field syn = do doc <- optional docComment

95 c <- optional $ lchar '{'

@@ -107,7 +107,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

107 return (n, p, t, doc')

108

109 constructor :: IdrisParser Name

110− constructor = (reserved "constructor") *> fnName

110+ constructor = reserved "constructor" *> fnName

111

112 endPlicity :: Maybe Char -> IdrisParser Plicity

113 endPlicity (Just _) = do lchar '}'

@@ -126,7 +126,6 @@ recordParameter syn =

126 <|>

127 (do (n, pt) <- onlyName syn

128 return (n, expl, pt))

129−

130 where

129 where

131 namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)

130 namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)

132 namedTy syn =

131 namedTy syn =

src/Idris/ParseHelpers.hs+2−2

@@ -584,8 +584,8 @@ collect (c@(PClauses _ o _ _) : ds)

584collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

585collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

586collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

587−collect (PClass doc f s cs n ps pdocs fds ds : ds')

587+collect (PClass doc f s cs n ps pdocs fds ds cn cd : ds')

588− = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

588+ = PClass doc f s cs n ps pdocs fds (collect ds) cn cd : collect ds'

589collect (PInstance doc argDocs f s cs n ps t en ds : ds')

590 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

591collect (d : ds) = d : collect ds

src/Idris/Parser.hs+19−5

@@ -624,18 +624,32 @@ MethodOrInstance ::=

624

625@

626ClassBlock ::=

627− 'where' OpenBlock MethodOrInstance* CloseBlock

627+ 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

628 ;

629@

630-}

631−classBlock :: SyntaxInfo -> IdrisParser [PDecl]

631+classBlock :: SyntaxInfo -> IdrisParser (Maybe Name, Docstring (Either Err PTerm), [PDecl])

632classBlock syn = do reserved "where"

633 openBlock

634+ (cn, cd) <- option (Nothing, emptyDocstring) $

635+ try (do (doc, _) <- option noDocs docComment

636+ n <- constructor

637+ return (Just n, doc))

638+ ist <- get

639+ let cd' = annotate syn ist cd

640+

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

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

635 closeBlock

642 closeBlock

636− return (concat ds)

643+ return (cn, cd', concat ds)

637 <?> "class block"

644 <?> "class block"

638

645

646+ where

647+ constructor :: IdrisParser Name

648+ constructor = reserved "constructor" *> fnName

649+

650+ annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

651+ annotate syn ist = annotCode $ tryFullExpr syn ist

652+

639{-| Parses a type class declaration

653{-| Parses a type class declaration

640

654

641@

655@

@@ -663,9 +677,9 @@ class_ syn = do (doc, argDocs, acc)

663 let n = expandNS syn n_in

677 let n = expandNS syn n_in

664 cs <- many carg

678 cs <- many carg

665 fds <- option (map fst cs) fundeps

679 fds <- option (map fst cs) fundeps

666− ds <- option [] (classBlock syn)

680+ (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)

667 accData acc n (concatMap declared ds)

681 accData acc n (concatMap declared ds)

668− return [PClass doc syn fc cons n cs argDocs fds ds]

682+ return [PClass doc syn fc cons n cs argDocs fds ds cn cd]

669 <?> "type-class declaration"

683 <?> "type-class declaration"

670 where

684 where

671 fundeps :: IdrisParser [Name]

685 fundeps :: IdrisParser [Name]

src/Idris/REPL.hs+1−1

@@ -791,7 +791,7 @@ process fn (NewDefn decls) = do

791 getName (PTy docs argdocs syn fc opts name ty) = Just name

792 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

793 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

794− getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

794+ getName (PClass doc syn fc constraints name parms parmdocs fds decls _ _) = Just name

795 getName _ = Nothing

796 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

797 getClauseName (PClause fc name whole with rhs whereBlock) = name

test/classes001/ClassName.idrnew file+49

@@ -0,0 +1,49 @@

1+module ClassName

2+

3+||| A fancy shower with a constructor

4+||| @ a the thing to be shown

5+class MyShow a where

6+ ||| Build a MyShow

7+ constructor MkMyShow

8+ ||| The shower

9+ ||| @ x will become a string

10+ myShow : (x : a) -> String

11+

12+twiceAString : MyShow a => a -> String

13+twiceAString x = myShow x ++ myShow x

14+

15+instance MyShow Integer where

16+ myShow x = show x

17+

18+badShow : MyShow Integer

19+badShow = MkMyShow (const "hej")

20+

21+test1 : twiceAString 2 = "22"

22+test1 = Refl

23+

24+test2 : twiceAString @{badShow} 2 = "hejhej"

25+test2 = Refl

26+

27+

28+||| Superclass fun

29+class MyMagma a where

30+ constructor MkMyMagma

31+ total op : a -> a -> a

32+

33+||| Semigroup

34+class MyMagma a => MySemigroup a where

35+ constructor MkMySemigroup

36+ total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z

37+

38+instance [addition] MyMagma Nat where

39+ op = plus

40+

41+additionS : MySemigroup Nat

42+additionS = MkMySemigroup @{addition} plusAssociative

43+

44+doIt : MySemigroup a => a -> List a -> a

45+doIt x [] = x

46+doIt x (y :: xs) = doIt (x `op` y) xs

47+

48+test : Nat

49+test = doIt @{additionS} 22 [1,2,3,4]

test/classes001/expectednew file+27

@@ -0,0 +1,27 @@

1+Type class MyShow

2+ A fancy shower with a constructor

3+

4+Parameters:

5+ a -- the thing to be shown

6+

7+Methods:

8+ myShow : MyShow a => (x : a) -> String

9+ The shower

10+

11+Instance constructor:

12+ MkMyShow : (myShow : a -> String) -> MyShow a

13+ Build a MyShow

14+ Arguments:

15+ (implicit) a : Type -- the thing to be shown

16+

17+ myShow : a -> String -- The shower

18+

19+Instances:

20+ MyShow Integer

21+MkMyShow : (myShow : a -> String) -> MyShow a

22+ Build a MyShow

23+ Arguments:

24+ (implicit) a : Type -- the thing to be shown

25+

26+ myShow : a -> String -- The shower

27+

test/classes001/inputnew file+2

@@ -0,0 +1,2 @@

1+:doc MyShow

2+:doc MkMyShow

test/classes001/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input

3+rm -f bounded001 *.ibc