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

CHANGELOG+3

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

4040 type classes. See the updated tutorial for details.

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

4242 keyword.

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

44+ using the same syntax as record constructors.

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

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

4547 desugaring.

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

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

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

4951

52+

5053New in 0.9.17:

5154--------------

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

idris.cabal+5

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

357357 test/bignum002/*.idr

358358 test/bignum002/expected

359359

360+ test/classes001/*.idr

361+ test/classes001/run

362+ test/classes001/expected

363+ test/classes001/input

364+

360365 test/corecords001/*.idr

361366 test/corecords001/run

362367 test/corecords001/expected

src/Idris/AbsSyntax.hs+3−1

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

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

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

11031103 = 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)

11051105 = PClass doc info f

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

11071107 n

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

11091109 pDocs

11101110 fds

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

1112+ cn

1113+ cd

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

11131115 = PInstance doc argDocs info f

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

src/Idris/AbsSyntaxTree.hs+9−7

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

612612 -- ^ Record declaration

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

614614 [(Name, t)] -- constraints

615− Name

615+ Name -- class name

616616 [(Name, t)] -- parameters

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

618618 [Name] -- determining parameters

619619 [PDecl' t] -- declarations

620+ (Maybe Name) -- instance constructor name

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

620622 -- ^ 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

622624 | PInstance

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

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

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

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

734736declared (PNamespace _ ds) = concatMap declared ds

735737declared (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)

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

738740declared (PDSL n _) = [n]

739741declared (PSyntax _ _) = []

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

753755tldeclared (PParams _ _ ds) = []

754756tldeclared (PMutual _ ds) = concatMap tldeclared ds

755757tldeclared (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)

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

758760tldeclared _ = []

759761

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

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

770772defined (PNamespace _ ds) = concatMap defined ds

771773defined (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)

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

774776defined (PDSL n _) = [n]

775777defined (PSyntax _ _) = []

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

10701072

10711073-- Type class data

10721074

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

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

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

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

10761078 class_default_superclasses :: [PDecl],

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

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

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

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

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

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

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

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

17881790 = 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

150150 rnf x2 `seq`

151151 rnf x3 `seq`

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

154154 = rnf x1 `seq`

155155 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` ()

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

158164 = rnf x1 `seq`

159165 rnf x2 `seq`

src/Idris/Docs.hs+13−1

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

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

4141 [PTerm] -- subclasses

4242 [PTerm] -- superclasses

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

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

4445 | ModDoc [String] -- Module name

4546 d

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

9596 if null args then text "No constructors."

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

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

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

100101 if nullDocstring doc

101102 then empty

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

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

107108 vsep (map (pprintFD ist) meths))

108109 <$>

110+ maybe empty

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

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

113+ pprintFD ist)

114+ ctor

115+ <>

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

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

111118 else map pprintInstance normalInstances))

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

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

252259 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

253260 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

254265 return $ ClassDoc

255266 n docstr mdocs params

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

268+ ctorDocs

257269 where

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

259271 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

5454

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

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

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

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

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

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

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

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

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

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

61+ Idris ()

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

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

6164 let tty = pibind ps PType

6265 let constraint = PApp fc (PRef fc tn)

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

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

8083 let cty = impbind ps $ conbind constraints

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

8285 constraint

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

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

8487 let ddecl = PDatadecl tn tty cons

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

8689 -- Elaborate the data declaration

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

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

244247 toExp ns e sc = sc

245248

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+

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

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

248260expandMethNS :: 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

130130-- let lhs = PRef fc iname

131131 let lhs = PApp fc (PRef fc iname)

132132 (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))

134134 (map (pexp . mkMethApp) mtys)

135135

136136 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

232232 ninfo = case namespace info of

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

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

236236 | what /= EDefns

237237 = 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

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

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

241241 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

11861186 put x9

11871187 put x10

11881188 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

11901190 -> do putWord8 7

11911191 put x1

11921192 put x2

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

11971197 put x7

11981198 put x8

11991199 put x9

1200+ put x10

1201+ put x11

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

12011203 do putWord8 8

12021204 put x1

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

12991301 x7 <- get

13001302 x8 <- get

13011303 x9 <- get

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

1304+ x10 <- get

1305+ x11 <- get

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

13031307 8 -> do x1 <- get

13041308 x2 <- get

13051309 x3 <- get

src/Idris/IdrisDoc.hs+13−13

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

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

167167removeOrphans list =

168168 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

170170

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

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

173− names _ = []

171+ where names (Just (DataDoc _ 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 _ = []

174174

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

176176filterName :: Name -- ^ Name to check

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

218218 names = concatMap (extractPTermNames) ts

219219 in S.map getNs $ S.fromList names

220220

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

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

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

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

225− getFunDocs (ModDoc _ _) = []

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

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

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

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

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

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

225+ getFunDocs (ModDoc _ _) = []

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

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

228228

229229

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

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

579579 -> H.Html -- ^ Resulting HTML

580580createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

581581

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

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

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

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

585585 H.span ! class_ "name type"

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

588588 H.span ! class_ "signature" $ nbsp

589589 H.dd $ do

590590 (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))

592592

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

594594 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

8989 fields <- many . indented $ field syn

9090

9191 return (fields, constructorName, constructorDoc')

92− where

92+ where

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

9494 field syn = do doc <- optional docComment

9595 c <- optional $ lchar '{'

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

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

108108

109109 constructor :: IdrisParser Name

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

110+ constructor = reserved "constructor" *> fnName

111111

112112 endPlicity :: Maybe Char -> IdrisParser Plicity

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

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

126126 <|>

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

128128 return (n, expl, pt))

129−

130129 where

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

132131 namedTy syn =

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

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

588− = PClass doc f s cs n ps pdocs fds (collect ds) : collect 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) cn cd : collect ds'

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

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

591591collect (d : ds) = d : collect ds

src/Idris/Parser.hs+19−5

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

624624

625625@

626626ClassBlock ::=

627− 'where' OpenBlock MethodOrInstance* CloseBlock

627+ 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

628628 ;

629629@

630630-}

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

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

632632classBlock syn = do reserved "where"

633633 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+

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

635642 closeBlock

636− return (concat ds)

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

637644 <?> "class block"

638645

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+

639653{-| Parses a type class declaration

640654

641655@

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

663677 let n = expandNS syn n_in

664678 cs <- many carg

665679 fds <- option (map fst cs) fundeps

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

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

667681 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]

669683 <?> "type-class declaration"

670684 where

671685 fundeps :: IdrisParser [Name]

src/Idris/REPL.hs+1−1

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

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

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

793793 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

795795 getName _ = Nothing

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

797797 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