14b7025 · Idris-dev · git.iko.soy

README.md+1

@@ -1,6 +1,7 @@

1# Idris

2

3[![Build Status](https://travis-ci.org/idris-lang/Idris-dev.svg?branch=master)](https://travis-ci.org/idris-lang/Idris-dev)

4+[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)

4[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)

5[![Hackage](https://budueba.com/hackage/idris)](https://hackage.haskell.org/package/idris)

5

6

6Idris (http://idris-lang.org/) is a general-purpose functional programming

7Idris (http://idris-lang.org/) is a general-purpose functional programming

docs/effects/introduction.rst+6−4

@@ -63,6 +63,7 @@ library:

63

64 module Main

65

66+ import Effects

66 import Effect.StdIO

67 import Effect.StdIO

67

68

68 hello : [STDIO] Eff ()

69 hello : [STDIO] Eff ()

@@ -71,10 +72,11 @@ library:

71 main : IO ()

72 main : IO ()

72 main = run hello

73 main = run hello

73

74

74−As usual, the entry point is ``main``. All ``main`` has to do is

75+As usual, the entry point is ``main``. All ``main`` has to do is invoke the

75−invoke the ``hello`` function which supports the ``STDIO`` effect for

76+``hello`` function which supports the ``STDIO`` effect for console I/O, and

76−console I/O, and returns the unit value. The details of the ``Eff``

77+returns the unit value. All programs using the ``Effects`` library must

78+``import Effects``. The details of the ``Eff`` type will be presented in the

77−type will be presented in the remainder of this tutorial.

79+remainder of this tutorial.

78

80

79To compile and run this program, ``Idris`` needs to be told to include

81To compile and run this program, ``Idris`` needs to be told to include

80the ``Effects`` package, using the ``-p effects`` flag (this flag is

82the ``Effects`` package, using the ``-p effects`` flag (this flag is

docs/effects/state.rst+1

@@ -183,6 +183,7 @@ shown in Listing [introprog].

183

184 module Main

185

186+ import Effects

186 import Effect.State

187 import Effect.State

187

188

188 data BTree a = Leaf

189 data BTree a = Leaf

docs/index.rst+23−19

@@ -6,31 +6,21 @@

6Documentation for the Idris Language

7====================================

8

9− This work is licensed under the Creative Commons

9+.. note::

10− Attribution-ShareAlike 4.0 International License. To view a copy

10+

11− of this license, visit

11+ The documentation for Idris has been published under the Creative

12− http://creativecommons.org/licenses/by-sa/4.0/.

12+ Commons CC0 License. As such to the extent possible under law, /The

13+ Idris Community/ has waived all copyright and related or neighboring

14+ rights to Documentation for Idris.

15+

16+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

13

17

14−* :ref:`reference-index`

15* :ref:`tutorial-index`

18* :ref:`tutorial-index`

16* :ref:`eff-tutorial-index`

19* :ref:`eff-tutorial-index`

20+* :ref:`reference-index`

17* :ref:`guides-index`

21* :ref:`guides-index`

18

22

19

23

20−.. _reference:

21−

22−##################

23−Language Reference

24−##################

25−

26−.. toctree::

27− :maxdepth: 1

28−

29− reference/documenting

30− reference/uniqueness-types

31− reference/ffi

32− reference/erasure

33−

34.. _tutorial:

24.. _tutorial:

35

25

36###################

26###################

@@ -72,6 +62,20 @@ Learning Effects

72 effects/conclusions

62 effects/conclusions

73 effects/summary

63 effects/summary

74

64

65+.. _reference:

66+

67+##################

68+Language Reference

69+##################

70+

71+.. toctree::

72+ :maxdepth: 1

73+

74+ reference/documenting

75+ reference/uniqueness-types

76+ reference/ffi

77+ reference/erasure

78+

75.. _guides:

79.. _guides:

76

80

77############

81############

docs/tutorial/introduction.rst+3−3

@@ -1,8 +1,8 @@

1.. _sect-intro:

2

3−===========

3+============

4−Introducton

4+Introduction

5−===========

5+============

6

7In conventional programming languages, there is a clear distinction

8between *types* and *values*. For example, in `Haskell

idris.cabal+8−3

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.16

2+Version: 0.9.17

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -301,7 +301,9 @@ Extra-source-files:

301 test/reg060/run

302 test/reg060/*.idr

303 test/reg060/expected

304−

304+ test/reg061/run

305+ test/reg061/*.idr

306+ test/reg061/expected

305

307

306 test/basic001/run

308 test/basic001/run

307 test/basic001/*.idr

309 test/basic001/*.idr

@@ -632,7 +634,10 @@ Extra-source-files:

632 test/docs002/input

634 test/docs002/input

633 test/docs002/*.idr

635 test/docs002/*.idr

634 test/docs002/expected

636 test/docs002/expected

635−

637+ test/docs003/run

638+ test/docs003/input

639+ test/docs003/*.idr

640+ test/docs003/expected

636

641

637

642

638source-repository head

643source-repository head

mkpkg.sh+9

@@ -10,6 +10,15 @@ git tag v$VERSION -a

10

11cabal sdist

12

13+# Generate Idris library docs and put them in lib_docs.tar.gz in the root

14+make lib_doc

15+DOCDIR=`mktemp -d /tmp/docsXXXXX`

16+cp -r libs/base/base_doc "$DOCDIR"

17+cp -r libs/prelude/prelude_doc "$DOCDIR"

18+cp -r libs/effects/effects_doc "$DOCDIR"

19+cp -r libs/contrib/contrib_doc "$DOCDIR"

20+tar -czvf lib_docs.tar.gz -C "$DOCDIR" prelude_doc base_doc effects_doc contrib_doc

21+

13cabal configure --prefix=/usr/local

22cabal configure --prefix=/usr/local

14cabal build

23cabal build

15cabal copy --destdir=/tmp/idris-pkg/

24cabal copy --destdir=/tmp/idris-pkg/

src/Idris/AbsSyntax.hs+3−3

@@ -1685,9 +1685,9 @@ aiFn inpat expat qq imp_meths ist fc f ds as

1685 case find n imps [] of

1686 Just (tm, imps') ->

1687 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

1688− Nothing ->

1688+ Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in

1689− PImp p True l n Placeholder :

1689+ PImp p True l n ph :

1690− insImpAcc (M.insert n Placeholder pnas) ps given imps

1690+ insImpAcc (M.insert n ph pnas) ps given imps

1691 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1692 let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in

1693 case find n imps [] of

src/Idris/Core/Binary.hs+2−2

@@ -600,8 +600,8 @@ instance {- (Binary n) => -} Binary (TT Name) where

600 x2 <- getWord8

601 return (Proj x1 ((fromEnum x2)-1))

602 6 -> return Erased

603− 7 -> do x1 <- get

603+ 7 -> do _x1 <- get :: Get UExp

604− return (TType x1)

604+ return (TType (UVar (-1))) -- TODO: temp hack, make Edwin fix this!

605 8 -> return Impossible

606 9 -> do x1 <- get

607 return (V x1)

src/Idris/Core/Constraints.hs+152−59

@@ -1,71 +1,164 @@

1-- | Check universe constraints.

2−module Idris.Core.Constraints(ucheck) where

2+module Idris.Core.Constraints ( ucheck ) where

3

4−import Idris.Core.TT

4+import Idris.Core.TT ( TC(..), UExp(..), UConstraint(..), FC(..), Err'(..) )

5−import Idris.Core.Typecheck

6

5

7import Control.Applicative

6import Control.Applicative

8−import Control.Arrow

7+import Control.Monad.State.Strict

9−import Control.Monad.RWS

10−import Control.Monad.State

11−import qualified Data.Set as S

8+import Data.Function ( on )

12−import Data.List

9+import Data.List ( partition, nubBy )

13−import Data.Maybe

14import qualified Data.Map.Strict as M

10import qualified Data.Map.Strict as M

11+import qualified Data.Set as S

15

12

16−import Debug.Trace

17

13

18-- | Check that a list of universe constraints can be satisfied.

14-- | Check that a list of universe constraints can be satisfied.

19ucheck :: [(UConstraint, FC)] -> TC ()

15ucheck :: [(UConstraint, FC)] -> TC ()

20−ucheck cs = acyclic rels (map fst (M.toList rels))

16+ucheck = void . solve 10 . nubBy ((==) `on` fst) . filter (not . ignore)

21− where lhs (ULT l _) = l

17+ where

22− lhs (ULE l _) = l

18+ -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

23− cs' = S.toList (S.fromList cs)

19+ ignore (c,_) | any (== Var (-1)) (varsIn c) = True

24− rels = mkRels cs' M.empty

25−

26−type Relations = M.Map UExp [(UConstraint, FC)]

27−

28−mkRels :: [(UConstraint, FC)] -> Relations -> Relations

29−mkRels [] acc = acc

30−mkRels ((c, f) : cs) acc

31− | not (ignore c)

32− = case M.lookup (lhs c) acc of

33− Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)

34− Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)

35− | otherwise = mkRels cs acc

36− where lhs (ULT l _) = l

37− lhs (ULE l _) = l

38− ignore (ULE l r) = l == r

20+ ignore (ULE a b, _) = a == b

39 ignore _ = False

21 ignore _ = False

40

22

23+newtype Var = Var Int

24+ deriving (Eq, Ord, Show)

25+

26+data Domain = Domain {-# UNPACK #-} !Int

27+ {-# UNPACK #-} !Int

28+ deriving (Eq, Ord, Show)

29+

30+data SolverState =

31+ SolverState

32+ { queue :: Queue

33+ , domainStore :: M.Map Var ( Domain

34+ , S.Set (UConstraint, FC) -- constraints that effected this variable

35+ )

36+ }

37+

38+data Queue = Queue [(UConstraint, FC)] (S.Set UConstraint)

39+

40+

41+solve :: Int -> [(UConstraint, FC)] -> TC (M.Map Var Int)

42+solve maxUniverseLevel inpConstraints =

43+ evalStateT (propagate >> extractSolution) initSolverState

44+

45+ where

46+

47+ -- | initial solver state.

48+ -- the queue contains all constraints, the domain store contains the initial domains.

49+ initSolverState :: SolverState

50+ initSolverState =

51+ let

52+ (initUnaryQueue, initQueue) = partition (\ (c,_) -> length (varsIn c) == 1) inpConstraints

53+ in

54+ SolverState

55+ { queue = Queue (initUnaryQueue ++ initQueue) (S.fromList (map fst (initUnaryQueue ++ initQueue)))

56+ , domainStore = M.fromList

57+ [ (v, (Domain 0 maxUniverseLevel, S.empty))

58+ | v <- ordNub [ v

59+ | (c, _) <- inpConstraints

60+ , v <- varsIn c

61+ ]

62+ ]

63+ }

64+

65+ -- | a map from variables to the list of constraints the variable occurs in.

66+ constraints :: M.Map Var (S.Set (UConstraint, FC))

67+ constraints = M.fromListWith S.union

68+ [ (v, S.singleton (c,fc))

69+ | (c, fc) <- inpConstraints

70+ , let vars = varsIn c

71+ , length vars > 1 -- do not register unary constraints

72+ , v <- vars

73+ ]

74+

75+ -- | this is where the actual work is done.

76+ -- dequeue the first constraint,

77+ -- filter domains,

78+ -- update domains (possibly resulting in a domain wipe out),

79+ -- until the queue is empty.

80+ propagate :: StateT SolverState TC ()

81+ propagate = do

82+ mcons <- nextConstraint

83+ case mcons of

84+ Nothing -> return ()

85+ Just (cons, fc) -> do

86+ case cons of

87+ ULE a b -> do

88+ Domain lowerA upperA <- domainOf a

89+ Domain lowerB upperB <- domainOf b

90+ when (upperB < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB)

91+ when (lowerA > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA upperB)

92+ ULT a b -> do

93+ Domain lowerA upperA <- domainOf a

94+ Domain lowerB upperB <- domainOf b

95+ let upperB_pred = pred upperB

96+ let lowerA_succ = succ lowerA

97+ when (upperB_pred < upperA) $ updateDomainOf (cons, fc) a (Domain lowerA upperB_pred)

98+ when (lowerA_succ > lowerB) $ updateDomainOf (cons, fc) b (Domain lowerA_succ upperB)

99+ propagate

100+

101+ -- | extract a solution from the state.

102+ extractSolution :: (MonadState SolverState m, Functor m) => m (M.Map Var Int)

103+ extractSolution = M.map (extractValue . fst) <$> gets domainStore

104+

105+ extractValue :: Domain -> Int

106+ extractValue (Domain x _) = x

107+

108+ -- | dequeue the first constraint.

109+ nextConstraint :: MonadState SolverState m => m (Maybe (UConstraint, FC))

110+ nextConstraint = do

111+ Queue list set <- gets queue

112+ case list of

113+ [] -> return Nothing

114+ (q:qs) -> do

115+ modify $ \ st -> st { queue = Queue qs (S.delete (fst q) set) }

116+ return (Just q)

117+

118+ -- | look up the domain of a variable from the state.

119+ -- for convenience, this function also accepts UVal's and returns a singleton domain for them.

120+ domainOf :: MonadState SolverState m => UExp -> m Domain

121+ domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)

122+ domainOf (UVal val) = return (Domain val val)

123+

124+ -- | updates the domain of a variable.

125+ -- this function is also where we fail, inc ase of a domain wipe-out.

126+ updateDomainOf :: (UConstraint, FC) -> UExp -> Domain -> StateT SolverState TC ()

127+ updateDomainOf suspect (UVar var) newDom = do

128+ doms <- gets domainStore

129+ let (oldDom, suspects) = doms M.! Var var

130+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines

131+ $ "Universe inconsistency."

132+ : ("Working on: " ++ show (UVar var))

133+ : ("Old domain: " ++ show oldDom)

134+ : ("New domain: " ++ show newDom)

135+ : "Involved constraints: "

136+ : map (("\t"++) . show) (suspect : S.toList suspects)

137+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

138+ addToQueue (Var var)

139+ updateDomainOf _ UVal{} _ = return ()

140+

141+ -- | add all constraints related to a variable.

142+ addToQueue :: MonadState SolverState m => Var -> m ()

143+ addToQueue var =

144+ case M.lookup var constraints of

145+ Nothing -> return ()

146+ Just cs -> do

147+ Queue list set <- gets queue

148+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set ]

149+ if null newCons

150+ then return ()

151+ else modify $ \ st -> st { queue = Queue (list ++ newCons)

152+ (S.union set (S.fromList (map fst newCons))) }

153+

154+ -- | check if a domain is wiped out.

155+ wipeOut :: Domain -> Bool

156+ wipeOut (Domain l u) = l > u

157+

158+ordNub :: Ord a => [a] -> [a]

159+ordNub = S.toList . S.fromList

41

160

42−acyclic :: Relations -> [UExp] -> TC ()

161+-- | variables in a constraint

43−acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs

162+varsIn :: UConstraint -> [Var]

44− where

163+varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]

45− checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()

164+varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]

46− checkCycle fc r path inc [] = return ()

47− checkCycle fc r path inc (c : cs)

48− = do check fc r path inc c

49− -- Remove c from r since we know there's no cycles now

50− let r' = M.insert c [] r

51− checkCycle fc r' path inc cs

52−

53− check fc r path inc (UVar x) | x < 0 = return ()

54− check fc r path inc cv

55− | inc > 0 && cv `elem` map fst path

56− = Error $ At fc UniverseError

57− -- FIXME: Make informative

58− -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))

59− -- Issue #1725 on the issue tracker.

60− -- https://github.com/idris-lang/Idris-dev/issues/1725

61− -- if we reach a cycle but we're at the same universe level, it's

62− -- fine, because they must all be equal, so stop.

63− | inc == 0 && cv `elem` map fst path

64− = return ()

65− | otherwise

66− = case M.lookup cv r of

67− Nothing -> return ()

68− Just cs -> mapM_ (next r ((cv, fc):path) inc) cs

69−

70− next r path inc (ULT l x, fc) = check fc r path (inc + 1) x

71− next r path inc (ULE l x, fc) = check fc r path inc x

src/Idris/Delaborate.hs+1−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

3+module Idris.Delaborate (annName, bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

4

5-- Convert core TT back into high level syntax, primarily for display

6-- purposes.

src/Idris/Docs.hs+55−19

@@ -1,4 +1,5 @@

1−{-# LANGUAGE DeriveFunctor, PatternGuards #-}

1+{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

3module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

3

4

4import Idris.AbsSyntax

5import Idris.AbsSyntax

@@ -10,6 +11,8 @@ import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, rende

10

11

11import Util.Pretty

12import Util.Pretty

12

13

14+import Control.Arrow (first)

15+

13import Data.Maybe

16import Data.Maybe

14import Data.List

17import Data.List

15import qualified Data.Text as T

18import qualified Data.Text as T

@@ -32,9 +35,10 @@ data Docs' d = FunDoc (FunDoc' d)

32 | ClassDoc Name d -- class docs

35 | ClassDoc Name d -- class docs

33 [FunDoc' d] -- method docs

36 [FunDoc' d] -- method docs

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

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

35− [(PTerm, (d, [(Name, d)]))] -- instances

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

36 [PTerm] -- subclasses

39 [PTerm] -- subclasses

37 [PTerm] -- superclasses

40 [PTerm] -- superclasses

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

38 | ModDoc [String] -- Module name

42 | ModDoc [String] -- Module name

39 d

43 d

40 deriving Functor

44 deriving Functor

@@ -102,7 +106,11 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

102 <$>

106 <$>

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

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

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

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

105− else map pprintInstance instances))

109+ else map pprintInstance normalInstances))

110+ <>

111+ (if null namedInstances then empty

112+ else line <$> nest 4 (text "Named instances:" <$>

113+ vsep (map pprintInstance namedInstances)))

106 <>

114 <>

107 (if null subclasses then empty

115 (if null subclasses then empty

108 else line <$> nest 4 (text "Subclasses:" <$>

116 else line <$> nest 4 (text "Subclasses:" <$>

@@ -113,14 +121,17 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

113 vsep (map dumpInstance superclasses)))

121 vsep (map dumpInstance superclasses)))

114 where

122 where

115 params' = zip pNames (repeat False)

123 params' = zip pNames (repeat False)

124+

125+ (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)

126+ instances

116

127

117 pNames = map fst params

128 pNames = map fst params

118

129

119 ppo = ppOptionIst ist

130 ppo = ppOptionIst ist

120 infixes = idris_infixes ist

131 infixes = idris_infixes ist

121

132

122− pprintInstance (term, (doc, argDocs)) =

133+ pprintInstance (mname, term, (doc, argDocs)) =

123− nest 4 (dumpInstance term <>

134+ nest 4 (iname mname <> dumpInstance term <>

124 (if nullDocstring doc

135 (if nullDocstring doc

125 then empty

136 then empty

126 else line <>

137 else line <>

@@ -133,6 +144,10 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

133 then empty

144 then empty

134 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

145 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

135

146

147+

148+ iname Nothing = empty

149+ iname (Just n) = annName n <+> colon <> space

150+

136 prettyInstanceParam params (name, doc) =

151 prettyInstanceParam params (name, doc) =

137 if nullDocstring doc

152 if nullDocstring doc

138 then empty

153 then empty

@@ -170,6 +185,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

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

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

171 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

186 else hsep (punctuate comma (map (prettyName True False params' . fst) params))

172

187

188+pprintDocs ist (NamedInstanceDoc _cls doc)

189+ = nest 4 (text "Named instance:" <$> pprintFD ist doc)

190+

173pprintDocs ist (ModDoc mod docs)

191pprintDocs ist (ModDoc mod docs)

174 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

192 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

175 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

193 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs

@@ -190,13 +208,23 @@ getDocs n@(NS n' ns) w | n' == modDocName

190 " do not exist! This shouldn't have happened and is a bug."

208 " do not exist! This shouldn't have happened and is a bug."

191getDocs n w

209getDocs n w

192 = do i <- getIState

210 = do i <- getIState

193− docs <- case lookupCtxt n (idris_classes i) of

211+ docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)

194− [ci] -> docClass n ci

212+ -> docClass n ci

195− _ -> case lookupCtxt n (idris_datatypes i) of

213+ | Just ti <- lookupCtxtExact n (idris_datatypes i)

196− [ti] -> docData n ti

214+ -> docData n ti

215+ | Just class_ <- classNameForInst i n

216+ -> do fd <- docFun n

217+ return $ NamedInstanceDoc class_ fd

218+ | otherwise

197− _ -> do fd <- docFun n

219+ -> do fd <- docFun n

198− return (FunDoc fd)

220+ return (FunDoc fd)

199 return $ fmap (howMuch w) docs

221 return $ fmap (howMuch w) docs

222+ where classNameForInst :: IState -> Name -> Maybe Name

223+ classNameForInst ist n =

224+ listToMaybe [ cn

225+ | (cn, ci) <- toAlist (idris_classes ist)

226+ , n `elem` class_instances ci

227+ ]

200

228

201docData :: Name -> TypeInfo -> Idris Docs

229docData :: Name -> TypeInfo -> Idris Docs

202docData n ti

230docData n ti

@@ -209,19 +237,26 @@ docClass n ci

209 = do i <- getIState

237 = do i <- getIState

210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

238 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

211 docstr = maybe emptyDocstring fst docStrings

239 docstr = maybe emptyDocstring fst docStrings

212− params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)

240+ params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))

241+ (class_params ci)

213− instanceDocs = map (fromMaybe (emptyDocstring, []) .

242+ docsForInstance inst = fromMaybe (emptyDocstring, []) .

214− listToMaybe .

215− flip lookupCtxt (idris_docstrings i))

243+ flip lookupCtxtExact (idris_docstrings i) $

216− (class_instances ci)

244+ inst

245+ instances = map (\inst -> (namedInst inst,

246+ delabTy i inst,

247+ docsForInstance inst))

217− instances = zip (map (delabTy i) (class_instances ci)) instanceDocs

248+ (nub (class_instances ci))

218− (subclasses, instances') = partition (isSubclass . fst) instances

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

219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

250 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

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

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

221 return $ ClassDoc

252 return $ ClassDoc

222 n docstr mdocs params

253 n docstr mdocs params

223− instances' (map fst subclasses) superclasses

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

224 where

255 where

256+ namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

257+ namedInst n@(UN _) = Just n

258+ namedInst _ = Nothing

259+

225 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

260 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

226 getDInst _ = Nothing

261 getDInst _ = Nothing

227

262

@@ -250,6 +285,7 @@ docFun n

250 where funName :: Name -> String

285 where funName :: Name -> String

251 funName (UN n) = str n

286 funName (UN n) = str n

252 funName (NS n _) = funName n

287 funName (NS n _) = funName n

288+ funName n = show n

253

289

254getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]

290getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]

255getPArgNames (PPi plicity name ty body) ds =

291getPArgNames (PPi plicity name ty body) ds =

src/Idris/Elab/Class.hs+4−3

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

69 let idecls = filter instdecl ds -- default superclass instance declarations

70 mapM_ checkDefaultSuperclassInstance idecls

71 let mnames = map getMName mdecls

72− logLvl 2 $ "Building methods " ++ show mnames

72+ logLvl 1 $ "Building methods " ++ show mnames

73 ims <- mapM (tdecl mnames) mdecls

74 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

75 (filter clause ds)

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

94 mapM_ (rec_elabDecl info EAll info) (concat cfns)

95

96 -- for each method, build a top level function

97+ fns <- mapM (tfun cn constraint (syn { imp_methods = mnames })

97− fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

98+ (map fst imethods)) imethods

98 logLvl 5 $ "Functions " ++ show fns

99 logLvl 5 $ "Functions " ++ show fns

99 -- Elaborate the the top level methods

100 -- Elaborate the the top level methods

100 mapM_ (rec_elabDecl info EAll info) (concat fns)

101 mapM_ (rec_elabDecl info EAll info) (concat fns)

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

199 let anames = map (\x -> sMN x "arg") [0..]

200 let anames = map (\x -> sMN x "arg") [0..]

200 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

201 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

201 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

202 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

202− iLOG (showTmImpls ty)

203+ iLOG (showTmImpls ty')

203 iLOG (show (m, ty', capp, margs))

204 iLOG (show (m, ty', capp, margs))

204 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

205 iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

205 return [PTy doc [] syn fc o m ty',

206 return [PTy doc [] syn fc o m ty',

src/Idris/Elab/Instance.hs+25−3

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

88 -- where block

89 wparams <- mapM (\p -> case p of

90 PApp _ _ args -> getWParams (map getTm args)

91+ a@(PRef fc f) -> getWParams [a]

91 _ -> return []) ps

92 _ -> return []) ps

92 let pnames = map pname (concat (nub wparams))

93 let pnames = map pname (concat (nub wparams))

93 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

94 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

@@ -103,8 +104,11 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

103 op, coninsert cs t', t'))

104 op, coninsert cs t', t'))

104 (class_methods ci)

105 (class_methods ci)

105 logLvl 3 (show (mtys, ips))

106 logLvl 3 (show (mtys, ips))

107+ logLvl 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

106− let ds' = insertDefaults i iname (class_defaults ci) ns ds

108+ let ds_defs = insertDefaults i iname (class_defaults ci) ns ds

109+ logLvl 3 ("After defaults: " ++ show ds_defs ++ "\n")

110+ let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

107− iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci)

111+ iLOG ("Reordered: " ++ show ds' ++ "\n")

108 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

112 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

109 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

113 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

110 let wbTys = map mkTyDecl mtys

114 let wbTys = map mkTyDecl mtys

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

239 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

243 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

240 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

244 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

241

245

246+ mkTyDecl (n, op, t, _)

242− mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

247+ = PTy emptyDocstring [] syn fc op n

248+ (mkUniqueNames [] t)

243

249

244 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

250 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

245 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

251 conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

@@ -249,6 +255,22 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

249 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

255 coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

250 coninsert cs sc = conbind cs sc

256 coninsert cs sc = conbind cs sc

251

257

258+ -- Reorder declarations to be in the same order as defined in the

259+ -- class declaration (important so that we insert default definitions

260+ -- in the right place, and so that dependencies between methods are

261+ -- respected)

262+ reorderDefs :: [Name] -> [PDecl] -> [PDecl]

263+ reorderDefs ns [] = []

264+ reorderDefs [] ds = ds

265+ reorderDefs (n : ns) ds = case pick n [] ds of

266+ Just (def, ds') -> def : reorderDefs ns ds'

267+ Nothing -> reorderDefs ns ds

268+

269+ pick n acc [] = Nothing

270+ pick n acc (def@(PClauses _ _ cn cs) : ds)

271+ | nsroot n == nsroot cn = Just (def, acc ++ ds)

272+ pick n acc (d : ds) = pick n (acc ++ [d]) ds

273+

252 insertDefaults :: IState -> Name ->

274 insertDefaults :: IState -> Name ->

253 [(Name, (Name, PDecl))] -> [T.Text] ->

275 [(Name, (Name, PDecl))] -> [T.Text] ->

254 [PDecl] -> [PDecl]

276 [PDecl] -> [PDecl]

test/docs003/docs003.idrnew file+9

@@ -0,0 +1,9 @@

1+module docs003

2+

3+instance [mine] Functor List where

4+ map m [] = []

5+ map m (x :: xs) = m x :: map m xs

6+

7+||| More functors!

8+instance [another] Functor List where

9+ map f xs = map @{mine} f xs

test/docs003/expectednew file+37

@@ -0,0 +1,37 @@

1+Type checking ./docs003.idr

2+Type class Functor

3+ Functors

4+

5+Parameters:

6+ f -- the action of the functor on objects

7+

8+Methods:

9+ map : Functor f => (m : a -> b) -> f a -> f b

10+ The action of the functor on morphisms

11+

12+Instances:

13+ Functor List

14+ Functor Stream

15+ Functor Provider

16+ Functor Binder

17+ Functor PrimIO

18+ Functor (IO' ffi)

19+ Functor Maybe

20+ Functor (Either e)

21+

22+Named instances:

23+ docs003.mine : Functor List

24+ docs003.another : Functor List

25+ More functors!

26+

27+Subclasses:

28+ Traversable f

29+ Applicative f

30+Named instance:

31+ mine : Functor List

32+

33+

34+Named instance:

35+ another : Functor List

36+ More functors!

37+

test/docs003/inputnew file+3

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

1+:doc Functor

2+:doc mine

3+:doc another

test/docs003/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --consolewidth 80 --quiet --nocolor docs003.idr < input

3+rm *.ibc

test/error001/expected+10−1

@@ -1 +1,10 @@

1−test002.idr:5:6:Universe inconsistency

1+test002.idr:5:6:Universe inconsistency.

2+Working on: f2

3+Old domain: Domain 7 7

4+New domain: Domain 7 6

5+Involved constraints:

6+ (f2 <= i1,test002.idr:5:6)

7+ (e2 < f2,test002.idr:5:6)

8+ (j1 <= f2,test002.idr:5:6)

9+ (f2 <= i1,test002.idr:5:6)

10+

test/reg060/expectednew file

No changes to the content.

test/reg060/reg060.idrnew file+12

@@ -0,0 +1,12 @@

1+

2+class MyFunctor (f : Type -> Type) where

3+ mymap : (m : a -> b) -> f a -> f b

4+

5+data Foo x y = Bar y

6+

7+instance MyFunctor (Foo m) where

8+ mymap m x = ?wibble

9+

10+instance [foo] Functor m => MyFunctor m where

11+ mymap m x = map m x

12+

test/reg060/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg060.idr --check

3+rm -f *.ibc