6d9659c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'origin/master' into stylish-travis

commit6d9659c610adee1f0cd55f3861d4977d104d2aa6 authorEcho Nolan <echo@echonolan.net> dateWed 19 Oct 2016, 14:38 (10 years ago) parent0fec73c 284b90b

13 files changed+65−20

compare with master

unifiedsplit

CHANGELOG.md+2 src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Docs.hs+11−2 src/Idris/Elab/Interface.hs+1 src/Idris/IBC.hs+5−3 src/Idris/IdrisDoc.hs+10−10 src/Idris/Main.hs+3−1 test/TestData.hs+2−1 test/docs006/docs006.idr+7 test/docs006/expected+16 test/docs006/input+1 test/docs006/run+3

CHANGELOG.md+2

@@ -57,6 +57,8 @@

5757 * New flag `--docdir` provided to show default documentation installation location.

5858 * New environment variable `IDRIS_DOC_PATH` to allow specification of an alternative installation path for documentation.

5959* Semantic meaning behind several environment variables has been clarified in documentation and code. See compilation section of the reference manual for more details.

60+* Interface parameter constraints are now printed in the output of `:doc`. This

61+ is tested for in `docs006`.

6062

6163## Miscellaneous updates

6264

src/Idris/AbsSyntax.hs+3−3

@@ -444,10 +444,10 @@ addImplementation :: Bool -- ^ whether the name is an Integer implementation

444444addImplementation int res n i

445445 = do ist <- getIState

446446 case lookupCtxt n (idris_interfaces ist) of

447− [CI a b c d e f ins fds] ->

448− do let cs = addDef n (CI a b c d e f (addI i ins) fds) (idris_interfaces ist)

447+ [CI a b c d e f g ins fds] ->

448+ do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)

449449 putIState $ ist { idris_interfaces = cs }

450− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)

450+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)

451451 putIState $ ist { idris_interfaces = cs }

452452 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]

453453 addI i ins | int = (i, res) : ins

src/Idris/AbsSyntaxTree.hs+1

@@ -1401,6 +1401,7 @@ data InterfaceInfo = CI {

14011401 , interface_default_super_interfaces :: [PDecl]

14021402 , interface_impparams :: [Name]

14031403 , interface_params :: [Name]

1404+ , interface_constraints :: [PTerm]

14041405 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

14051406 , interface_determiners :: [Int]

14061407 } deriving (Show, Generic)

src/Idris/Docs.hs+11−2

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

4949 | InterfaceDoc Name d -- interface docs

5050 [FunDoc' d] -- method docs

5151 [(Name, Maybe d)] -- parameters and their docstrings

52+ [PTerm] -- parameter constraints

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

5354 [PTerm] -- sub interfaces

5455 [PTerm] -- super interfaces

@@ -140,13 +141,18 @@ pprintDocs ist (DataDoc t args)

140141 if null args then text "No constructors."

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

142143 vsep (map (pprintFDWithoutTotality ist False) args))

143−pprintDocs ist (InterfaceDoc n doc meths params implementations sub_interfaces super_interfaces ctor)

144+pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_interfaces super_interfaces ctor)

144145 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>

145146 if nullDocstring doc

146147 then empty

147148 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

148149 <> line <$>

149150 nest 4 (text "Parameters:" <$> prettyParameters)

151+

152+ <> (if null constraints

153+ then empty

154+ else line <$> nest 4 (text "Constraints:" <$> prettyConstraints))

155+

150156 <> line <$>

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

152158 vsep (map (pprintFDWithTotality ist False) meths))

@@ -233,6 +239,9 @@ pprintDocs ist (InterfaceDoc n doc meths params implementations sub_interfaces s

233239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

234240 isSubInterface _ = False

235241

242+ prettyConstraints =

243+ cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

244+

236245 prettyParameters =

237246 if any (isJust . snd) params

238247 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

@@ -336,7 +345,7 @@ docInterface n ci

336345 SN _ -> return Nothing

337346 _ -> fmap Just $ docFun ctorN

338347 return $ InterfaceDoc

339− n docstr mdocs params

348+ n docstr mdocs params (interface_constraints ci)

340349 implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

341350 ctorDocs

342351 where

src/Idris/Elab/Interface.hs+1

@@ -132,6 +132,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

132132 addInterface tn (CI cn (map nodoc imethods) defaults idecls

133133 (map (\(n, _, _) -> n) impps)

134134 (map (\(n, _, _) -> n) ps)

135+ (map snd constraints)

135136 [] dets)

136137

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

src/Idris/IBC.hs+5−3

@@ -47,7 +47,7 @@ import System.Directory

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 150

50+ibcVersion = 151

5151

5252-- | When IBC is being loaded - we'll load different things (and omit

5353-- different structures/definitions) depending on which phase we're in.

@@ -2354,7 +2354,7 @@ instance (Binary t) => Binary (PArg' t) where

23542354

23552355

23562356instance Binary InterfaceInfo where

2357− put (CI x1 x2 x3 x4 x5 x6 _ x7)

2357+ put (CI x1 x2 x3 x4 x5 x6 x7 _ x8)

23582358 = do put x1

23592359 put x2

23602360 put x3

@@ -2362,6 +2362,7 @@ instance Binary InterfaceInfo where

23622362 put x5

23632363 put x6

23642364 put x7

2365+ put x8

23652366 get

23662367 = do x1 <- get

23672368 x2 <- get

@@ -2370,7 +2371,8 @@ instance Binary InterfaceInfo where

23702371 x5 <- get

23712372 x6 <- get

23722373 x7 <- get

2373− return (CI x1 x2 x3 x4 x5 x6 [] x7)

2374+ x8 <- get

2375+ return (CI x1 x2 x3 x4 x5 x6 x7 [] x8)

23742376

23752377instance Binary RecordInfo where

23762378 put (RI x1 x2 x3)

src/Idris/IdrisDoc.hs+10−10

@@ -167,7 +167,7 @@ removeOrphans list =

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

168168

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

170− names (Just (InterfaceDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

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

171171 names _ = []

172172

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

@@ -215,14 +215,14 @@ referredNss (n, Just d, _) =

215215 names = concatMap (extractPTermNames) ts

216216 in S.map getNs $ S.fromList names

217217

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

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

220− getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs

221− getFunDocs (RecordDoc _ _ f fs _) = f:fs

222− getFunDocs (NamedImplementationDoc _ fd) = [fd]

223− getFunDocs (ModDoc _ _) = []

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

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

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

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

220+ getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _ _) = fs

221+ getFunDocs (RecordDoc _ _ f fs _) = f:fs

222+ getFunDocs (NamedImplementationDoc _ fd) = [fd]

223+ getFunDocs (ModDoc _ _) = []

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

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

226226

227227

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

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

576576 -> H.Html -- ^ Resulting HTML

577577createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

578578

579−createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ c) = do

579+createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ _ c) = do

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

581581 H.span ! class_ "word" $ do "interface"; nbsp

582582 H.span ! class_ "name type"

src/Idris/Main.hs+3−1

@@ -51,7 +51,9 @@ import Text.Trifecta.Result (ErrInfo(..), Result(..))

5151runMain :: Idris () -> IO ()

5252runMain prog = do res <- runExceptT $ execStateT prog idrisInit

5353 case res of

54− Left err -> putStrLn $ "Uncaught error: " ++ show err

54+ Left err -> do

55+ putStrLn $ "Uncaught error: " ++ show err

56+ exitFailure

5557 Right _ -> return ()

5658

5759

test/TestData.hs+2−1

@@ -91,7 +91,8 @@ testFamiliesData = [

9191 ( 2, ANY ),

9292 ( 3, ANY ),

9393 ( 4, ANY ),

94− ( 5, ANY )]),

94+ ( 5, ANY ),

95+ ( 6, ANY )]),

9596 ("dsl", "DSL",

9697 [ ( 1, ANY ),

9798 ( 2, C_CG ),

test/docs006/docs006.idrnew file+7

@@ -0,0 +1,7 @@

1+module docs006

3+||| interface

4+||| @ t some parameter

5+interface Eq t => Foo t where

6+ ||| member of interface

7+ m : t

test/docs006/expectednew file+16

@@ -0,0 +1,16 @@

1+Interface Foo

2+ interface

4+Parameters:

5+ t -- some parameter

7+Constraints:

8+ Eq t

10+Methods:

11+ m : Foo t => t

12+ member of interface

13+

14+ The function is Total

15+Implementations:

16+ <no implementations>

test/docs006/inputnew file+1

@@ -0,0 +1 @@

1+:doc Foo

test/docs006/runnew file+3

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

3+rm *.ibc