4035b5d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add a field for parameter docstrings in the PClass constructor of PDecl'

4035b5dPaul Koerbitz12 years ago

src/Idris/AbsSyntaxTree.hs+6−5

compare with master

unifiedsplit

@@ -487,6 +487,7 @@ data PDecl' t

487 [t] -- constraints

488 Name

489 [(Name, t)] -- parameters

490+ [(Name, Docstring)] -- parameter docstrings

490 [PDecl' t] -- declarations

491 [PDecl' t] -- declarations

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

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

492 -- class name, parameters, method declarations

493 -- class name, parameters, method declarations

@@ -569,7 +570,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

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

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

570declared (PNamespace _ ds) = concatMap declared ds

571declared (PNamespace _ ds) = concatMap declared ds

571declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

572declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

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

573+declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

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

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

574declared (PDSL n _) = [n]

575declared (PDSL n _) = [n]

575declared (PSyntax _ _) = []

576declared (PSyntax _ _) = []

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

588tldeclared (PParams _ _ ds) = []

589tldeclared (PParams _ _ ds) = []

589tldeclared (PMutual _ ds) = concatMap tldeclared ds

590tldeclared (PMutual _ ds) = concatMap tldeclared ds

590tldeclared (PNamespace _ ds) = concatMap tldeclared ds

591tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

592+tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

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

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

593tldeclared _ = []

594tldeclared _ = []

594

595

@@ -604,7 +605,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

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

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

605defined (PNamespace _ ds) = concatMap defined ds

606defined (PNamespace _ ds) = concatMap defined ds

606defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

607defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

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

608+defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

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

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

609defined (PDSL n _) = [n]

610defined (PDSL n _) = [n]

610defined (PSyntax _ _) = []

611defined (PSyntax _ _) = []

@@ -1065,7 +1066,7 @@ eqOpts = []

1065elimName = sUN "__Elim"

1066elimName = sUN "__Elim"

1066elimMethElimTy = sUN "__elimTy"

1067elimMethElimTy = sUN "__elimTy"

1067elimMethElim = sUN "elim"

1068elimMethElim = sUN "elim"

1068−elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]

1069+elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []

1069 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1070 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,

1070 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1071 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

1071

1072

@@ -1419,7 +1420,7 @@ showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

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

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

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

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

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

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

1422−showDeclImp i (PClass _ _ _ cs n ps ds)

1423+showDeclImp i (PClass _ _ _ cs n ps _ ds)

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

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

1424showDeclImp i (PInstance _ _ cs n _ t _ ds)

1425showDeclImp i (PInstance _ _ cs n _ t _ ds)

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

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

src/Idris/DeepSeq.hs+2−2

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

143 rnf x2 `seq`

144 rnf x3 `seq`

145 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

146− rnf (PClass x1 x2 x3 x4 x5 x6 x7)

146+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)

147 = rnf x1 `seq`

148 rnf x2 `seq`

149− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

149+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

150 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8)

151 = rnf x1 `seq`

152 rnf x2 `seq`

src/Idris/ElabDecls.hs+5−5

@@ -1834,8 +1834,8 @@ data MArgTy = IA | EA | CA deriving Show

1834

1835elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

1836 FC -> [PTerm] ->

1837− Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1837+ Name -> [(Name, PTerm)] -> [(Name, Docstring)] -> [PDecl] -> Idris ()

1838−elabClass info syn doc fc constraints tn ps ds

1838+elabClass info syn doc fc constraints tn ps pDocs ds

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

1840 let tty = pibind ps PType

1841 let constraint = PApp fc (PRef fc tn)

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

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

1863 let ddecl = PDatadecl tn tty cons

1864 logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1865− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc [] fc [] ddecl

1865+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

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

1867 logLvl 5 $ "Building functions"

1868 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

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

2344 ninfo = case namespace info of

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

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

2347−elabDecl' what info (PClass doc s f cs n ps ds)

2347+elabDecl' what info (PClass doc s f cs n ps pdocs ds)

2348 | what /= EDefns

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

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

2350+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

2351elabDecl' what info (PInstance s f cs n ps t expn ds)

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

2353 elabInstance info s what f cs n ps t expn ds

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

569−collect (PClass doc f s cs n ps ds : ds')

569+collect (PClass doc f s cs n ps pdocs ds : ds')

570− = PClass doc f s cs n ps (collect ds) : collect ds'

570+ = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

571collect (PInstance f s cs n ps t en ds : ds')

572 = PInstance f s cs n ps t en (collect ds) : collect ds'

573collect (d : ds) = d : collect ds

src/Idris/Parser.hs+2−2

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

574 cs <- many carg

575 ds <- option [] (classBlock syn)

576 accData acc n (concatMap declared ds)

577− return [PClass (fst doc) syn fc cons n cs ds]

577+ return [PClass (fst doc) syn fc cons n cs (snd doc) ds]

578 <?> "type-class declaration"

579 where

580 carg :: IdrisParser (Name, PTerm)

@@ -1309,7 +1309,7 @@ loadSource h lidr f

1309 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1310 case x of

1311 PClauses _ _ _ _ -> r

1312− PClass _ _ _ _ _ _ _ -> r

1312+ PClass _ _ _ _ _ _ _ _ -> r

1313 PInstance _ _ _ _ _ _ _ _ -> r

1314 _ -> x

1315