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

git.iko.soy/Idris-dev

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

commit4035b5d1d90ba7d126da262556b34aef5448ca78 authorPaul Koerbitz <paul.koerbitz@theppro.com> dateFri 2 May 2014, 00:34 (12 years ago) parent9b1b1f1

5 files changed+17−16

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+6−5 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+5−5 src/Idris/ParseHelpers.hs+2−2 src/Idris/Parser.hs+2−2

src/Idris/AbsSyntaxTree.hs+6−5

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

487487 [t] -- constraints

488488 Name

489489 [(Name, t)] -- parameters

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

490491 [PDecl' t] -- declarations

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

492493 -- class name, parameters, method declarations

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

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

570571declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

574575declared (PDSL n _) = [n]

575576declared (PSyntax _ _) = []

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

588589tldeclared (PParams _ _ ds) = []

589590tldeclared (PMutual _ ds) = concatMap tldeclared ds

590591tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

593594tldeclared _ = []

594595

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

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

605606defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

609610defined (PDSL n _) = [n]

610611defined (PSyntax _ _) = []

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

10651066elimName = sUN "__Elim"

10661067elimMethElimTy = sUN "__elimTy"

10671068elimMethElim = 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)] []

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

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

10711072

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

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

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

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

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

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

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

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

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

143143 rnf x2 `seq`

144144 rnf x3 `seq`

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

147147 = rnf x1 `seq`

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

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

151151 = rnf x1 `seq`

152152 rnf x2 `seq`

src/Idris/ElabDecls.hs+5−5

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

18341834

18351835elabClass :: ElabInfo -> SyntaxInfo -> Docstring ->

18361836 FC -> [PTerm] ->

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

1838−elabClass info syn doc fc constraints tn ps ds

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

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

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

18401840 let tty = pibind ps PType

18411841 let constraint = PApp fc (PRef fc tn)

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

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

18631863 let ddecl = PDatadecl tn tty cons

18641864 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

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

18671867 logLvl 5 $ "Building functions"

18681868 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

23442344 ninfo = case namespace info of

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

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

23482348 | what /= EDefns

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

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

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

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

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

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

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

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

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

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

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

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

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

573573collect (d : ds) = d : collect ds

src/Idris/Parser.hs+2−2

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

574574 cs <- many carg

575575 ds <- option [] (classBlock syn)

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

578578 <?> "type-class declaration"

579579 where

580580 carg :: IdrisParser (Name, PTerm)

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

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

13101310 case x of

13111311 PClauses _ _ _ _ -> r

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

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

13131313 PInstance _ _ _ _ _ _ _ _ -> r

13141314 _ -> x

13151315