af3816e · Idris-dev · git.iko.soy

config.mk+1−1

compare with master

unifiedsplit

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

1−CC :=cc

1+CC ?=cc

2CABAL :=cabal

3CFLAGS :=-O2 -Wall $(CFLAGS)

4#CABALFLAGS :=

idris.cabal+5

@@ -339,12 +339,17 @@ Extra-source-files:

339 test/idrisdoc005/*.ipkg

340 test/idrisdoc006/run

341 test/idrisdoc006/expected

342+ test/idrisdoc006/A/fully/Qualified/NAME.idr

342 test/idrisdoc006/*.idr

343 test/idrisdoc006/*.idr

343 test/idrisdoc006/*.ipkg

344 test/idrisdoc006/*.ipkg

344 test/idrisdoc007/run

345 test/idrisdoc007/run

345 test/idrisdoc007/expected

346 test/idrisdoc007/expected

346 test/idrisdoc007/*.idr

347 test/idrisdoc007/*.idr

347 test/idrisdoc007/*.ipkg

348 test/idrisdoc007/*.ipkg

349+ test/idrisdoc008/run

350+ test/idrisdoc008/expected

351+ test/idrisdoc008/*.idr

352+ test/idrisdoc008/*.ipkg

348

353

349 test/interactive001/run

354 test/interactive001/run

350 test/interactive001/input

355 test/interactive001/input

libs/prelude/Prelude/Algebra.idr+21−21

@@ -21,7 +21,7 @@ class Semigroup a where

21 (<+>) : a -> a -> a

22

23class Semigroup a => VerifiedSemigroup a where

24− semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

24+ total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

25

26-- Sets equipped with a single binary operation that is associative, along with

27-- a neutral element for that binary operation. Must satisfy the following

@@ -35,8 +35,8 @@ class Semigroup a => Monoid a where

35 neutral : a

36

37class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

38− monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

38+ total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l

39− monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

39+ total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r

40

41-- Sets equipped with a single binary operation that is associative, along with

42-- a neutral element for that binary operation and inverses for all elements.

@@ -53,8 +53,8 @@ class Monoid a => Group a where

53 inverse : a -> a

54

55class (VerifiedMonoid a, Group a) => VerifiedGroup a where

56− groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral

56+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral

57− groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral

57+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral

58

59(<->) : Group a => a -> a -> a

60(<->) left right = left <+> (inverse right)

@@ -75,7 +75,7 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where

75class Group a => AbelianGroup a where { }

76

77class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

78− abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

78+ total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

79

80-- Sets equipped with two binary operations, one associative and commutative

81-- supplied with a neutral element, and the other associative, with

@@ -100,9 +100,9 @@ class AbelianGroup a => Ring a where

100 (<*>) : a -> a -> a

101

102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

103− ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

103+ total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

104− ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

104+ total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

105− ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

105+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)

106

107-- Sets equipped with two binary operations, one associative and commutative

108-- supplied with a neutral element, and the other associative supplied with a

@@ -130,8 +130,8 @@ class Ring a => RingWithUnity a where

130 unity : a

131

132class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

133− ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

133+ total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

134− ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

134+ total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

135

136-- Sets equipped with a binary operation that is commutative, associative and

137-- idempotent. Must satisfy the following laws:

@@ -146,9 +146,9 @@ class JoinSemilattice a where

146 join : a -> a -> a

147

148class JoinSemilattice a => VerifiedJoinSemilattice a where

149− joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r

149+ total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r

150− joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

150+ total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

151− joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

151+ total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

152

153-- Sets equipped with a binary operation that is commutative, associative and

154-- idempotent. Must satisfy the following laws:

@@ -163,9 +163,9 @@ class MeetSemilattice a where

163 meet : a -> a -> a

164

165class MeetSemilattice a => VerifiedMeetSemilattice a where

166− meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

166+ total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

167− meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

167+ total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

168− meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

168+ total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

169

170-- Sets equipped with a binary operation that is commutative, associative and

171-- idempotent and supplied with a neutral element. Must satisfy the following

@@ -184,7 +184,7 @@ class JoinSemilattice a => BoundedJoinSemilattice a where

184 bottom : a

185

186class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

187− boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

187+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom

188

189-- Sets equipped with a binary operation that is commutative, associative and

190-- idempotent and supplied with a neutral element. Must satisfy the following

@@ -203,7 +203,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where

203 top : a

204

205class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

206− boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

206+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top

207

208-- Sets equipped with two binary operations that are both commutative,

209-- associative and idempotent, along with absorbtion laws for relating the two

@@ -223,8 +223,8 @@ class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMe

223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

224

225class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

226− latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

226+ total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

227− latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

227+ total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

228

229-- Sets equipped with two binary operations that are both commutative,

230-- associative and idempotent and supplied with neutral elements, along with

src/Idris/AbsSyntax.hs+3−3

@@ -959,12 +959,12 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

959 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

960 econ (doc, argDocs, n, t, fc, fs)

961 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

962−expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

962+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)

963 = if tn `elem` ns

964 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

965− cdoc (dec cn) conty

965+ opts cdoc (dec cn) conty

966 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

967− cdoc (dec cn) conty

967+ opts cdoc (dec cn) conty

968 where conty = piBindp expl ps (expandParams dec ps ns [] cty)

969expandParamsD rhs ist dec ps ns (PParams f params pds)

970 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

src/Idris/AbsSyntaxTree.hs+6−6

@@ -482,7 +482,7 @@ data PDecl' t

482 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

483 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

484 | PNamespace String [PDecl' t] -- ^ New namespace

485− | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration

485+ | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration

486 | PClass Docstring SyntaxInfo FC

487 [t] -- constraints

488 Name

@@ -568,7 +568,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

568declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

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

570declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

574declared (PDSL n _) = [n]

@@ -582,7 +582,7 @@ tldeclared (PFix _ _ _) = []

582tldeclared (PTy _ _ _ _ _ n t) = [n]

583tldeclared (PPostulate _ _ _ _ n t) = [n]

584tldeclared (PClauses _ _ n _) = [] -- not a declaration

585−tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

585+tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]

586tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

587 where fstt (_, _, a, _, _, _) = a

588tldeclared (PParams _ _ ds) = []

@@ -603,7 +603,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

603defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

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

605defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

609defined (PDSL n _) = [n]

@@ -1619,8 +1619,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1619 where -- TODO THINK added niTacImp, but is it right?

1620 ni env (PRef _ n)

1621 | n `elem` vars && not (n `elem` env)

1622− = case lookupTy n (tt_ctxt ist) of

1622+ = case lookupDefExact n (tt_ctxt ist) of

1623− [] -> [n]

1623+ Nothing -> [n]

1624 _ -> []

1625 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1626 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

src/Idris/Core/CaseTree.hs+2

@@ -712,6 +712,8 @@ substSC n repl (Case n' alts)

712 | n == n' = Case repl (map (substAlt n repl) alts)

713 | otherwise = Case n' (map (substAlt n repl) alts)

714substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t

715+substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

716+substSC n repl ImpossibleCase = ImpossibleCase

715substSC n repl sc = error $ "unsupported in substSC: " ++ show sc

717substSC n repl sc = error $ "unsupported in substSC: " ++ show sc

716

718

717substAlt :: Name -> Name -> CaseAlt -> CaseAlt

719substAlt :: Name -> Name -> CaseAlt -> CaseAlt

src/Idris/Core/Elaborate.hs+1−1

@@ -64,7 +64,7 @@ loadState :: Elab' aux ()

64loadState = do (ES p s e) <- get

65 case e of

66 Just st -> put st

67− _ -> fail "Nothing to undo"

67+ _ -> lift $ Error . Msg $ "Nothing to undo"

68

69getNameFrom :: Name -> Elab' aux Name

70getNameFrom n = do (ES (p, a) s e) <- get

src/Idris/Core/Evaluate.hs+8−1

@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

15

16import Debug.Trace

17import Control.Applicative hiding (Const)

@@ -961,3 +961,10 @@ uniqueNameCtxt ctxt n hs

961 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

962 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

963 | otherwise = n

964+

965+uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name

966+uniqueBindersCtxt ctxt ns (Bind n b sc)

967+ = let n' = uniqueNameCtxt ctxt n ns in

968+ Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)

969+uniqueBindersCtxt ctxt ns (App f a) = App (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

970+uniqueBindersCtxt ctxt ns t = t

src/Idris/Core/ProofState.hs+3−3

@@ -15,7 +15,7 @@ import Idris.Core.Unify

15

16import Control.Monad.State.Strict

17import Control.Applicative hiding (empty)

18−import Control.Arrow (first)

18+import Control.Arrow ((***))

19import Data.List

20import Debug.Trace

21

@@ -666,7 +666,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

666 let scr = last $ tail args'

667 let indxnames = makeIndexNames indicies

668 prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

669− consargs' <- query (\ps -> map (first $ flip (uniqueNameCtxt (context ps)) (holes ps)) consargs)

669+ consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

670 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

671 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

672 action (\ps -> ps {holes = holes ps \\ [x]})

@@ -872,7 +872,7 @@ processTactic QED ps = case holes ps of

872 _ -> fail "Still holes to fill."

873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

874processTactic Undo ps = case previous ps of

875− Nothing -> fail "Nothing to undo."

875+ Nothing -> Error . Msg $ "Nothing to undo."

876 Just pold -> return (pold, "")

877processTactic EndUnify ps

878 = let (h, ns_in) = unified ps

src/Idris/Core/TT.hs+9

@@ -1223,3 +1223,12 @@ orderPats tm = op [] tm

1223 = (n', t') : insert n t ps

1224 | otherwise = (n,t):(n',t'):ps

1225

1226+allTTNames :: Eq n => TT n -> [n]

1227+allTTNames = nub . allNamesIn

1228+ where allNamesIn (P _ n _) = [n]

1229+ allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t

1230+ where nb (Let t v) = allNamesIn t ++ allNamesIn v

1231+ nb (Guess t v) = allNamesIn t ++ allNamesIn v

1232+ nb t = allNamesIn (binderTy t)

1233+ allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

1234+ allNamesIn _ = []

src/Idris/DeepSeq.hs+2−2

@@ -138,11 +138,11 @@ instance (NFData t) => NFData (PDecl' t) where

138 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

139 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

140 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

141− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

141+ rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

142 = rnf x1 `seq`

143 rnf x2 `seq`

144 rnf x3 `seq`

145− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `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)

147 = rnf x1 `seq`

148 rnf x2 `seq`

src/Idris/ElabDecls.hs+9−7

@@ -86,13 +86,14 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

86 ctxt <- getContext

87 i <- getIState

88

89− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

89+ logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'

90 ty' <- addUsingConstraints syn fc ty'

91 ty' <- implicit info syn n ty'

92

93 let ty = addImpl i ty'

94 inacc = inaccessibleArgs 0 ty

95+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

95− logLvl 3 $ show n ++ " type " ++ showTmImpls ty

96+ logLvl 5 $ show n ++ " type " ++ showTmImpls ty

96 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

97 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc

97

98

98 ((tyT, defer, is), log) <-

99 ((tyT, defer, is), log) <-

@@ -770,9 +771,9 @@ elabTransform info fc safe lhs_in rhs_in

770

771

772

772elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

773elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

773− PTerm -> Docstring -> Name -> PTerm -> Idris ()

774+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()

774−elabRecord info syn doc fc tyn ty cdoc cn cty

775+elabRecord info syn doc fc tyn ty opts cdoc cn cty

775− = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

776+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

776 -- TODO think: something more in info?

777 -- TODO think: something more in info?

777 cty' <- implicit info syn cn cty

778 cty' <- implicit info syn cn cty

778 i <- getIState

779 i <- getIState

@@ -1671,6 +1672,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1671 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1672 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

1672 addDeferred def''

1673 addDeferred def''

1673 mapM_ (elabCaseBlock info opts) is

1674 mapM_ (elabCaseBlock info opts) is

1675+ logLvl 5 ("Checked wval " ++ show wval')

1674 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1676 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

1675 let cwvaltyN = explicitNames cwvalty

1677 let cwvaltyN = explicitNames cwvalty

1676 let cwvalN = explicitNames cwval

1678 let cwvalN = explicitNames cwval

@@ -2318,10 +2320,10 @@ elabDecl' what info (PClass doc s f cs n ps ds)

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

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

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

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

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

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

2321−elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2323+elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

2322 | what /= ETypes

2324 | what /= ETypes

2323 = do iLOG $ "Elaborating record " ++ show tyn

2325 = do iLOG $ "Elaborating record " ++ show tyn

2324− elabRecord info s doc f tyn ty cdoc cn cty

2326+ elabRecord info s doc f tyn ty opts cdoc cn cty

2325 | otherwise

2327 | otherwise

2326 = do iLOG $ "Elaborating [type of] " ++ show tyn

2328 = do iLOG $ "Elaborating [type of] " ++ show tyn

2327 elabData info s doc [] f [] (PLaterdecl tyn ty)

2329 elabData info s doc [] f [] (PLaterdecl tyn ty)

src/Idris/IBC.hs+5−3

@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 67

33+ibcVersion = 68

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -1425,7 +1425,7 @@ instance (Binary t) => Binary (PDecl' t) where

1425 PNamespace x1 x2 -> do putWord8 5

1426 put x1

1427 put x2

1428− PRecord x1 x2 x3 x4 x5 x6 x7 x8 ->

1428+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->

1429 do putWord8 6

1430 put x1

1431 put x2

@@ -1435,6 +1435,7 @@ instance (Binary t) => Binary (PDecl' t) where

1435 put x6

1436 put x7

1437 put x8

1438+ put x9

1438 PClass x1 x2 x3 x4 x5 x6 x7

1439 PClass x1 x2 x3 x4 x5 x6 x7

1439 -> do putWord8 7

1440 -> do putWord8 7

1440 put x1

1441 put x1

@@ -1513,7 +1514,8 @@ instance (Binary t) => Binary (PDecl' t) where

1513 x6 <- get

1514 x6 <- get

1514 x7 <- get

1515 x7 <- get

1515 x8 <- get

1516 x8 <- get

1517+ x9 <- get

1516− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

1518+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

1517 7 -> do x1 <- get

1519 7 -> do x1 <- get

1518 x2 <- get

1520 x2 <- get

1519 x3 <- get

1521 x3 <- get

src/Idris/IdrisDoc.hs+26−10

@@ -77,10 +77,19 @@ generateDocs ist nss' out =

77

78-- ----------------------------------------------------------------- [ Types ]

79

80+-- | Either an error message or a result

80type Failable = Either String

81type Failable = Either String

82+

83+-- | Internal representation of a fully qualified namespace name

81type NsName = [T.Text]

84type NsName = [T.Text]

85+

86+-- | All information to be documented about a single namespace member

82type NsItem = (Name, Maybe Docs, Accessibility)

87type NsItem = (Name, Maybe Docs, Accessibility)

88+

89+-- | All information to be documented about a namespace

83type NsInfo = [NsItem]

90type NsInfo = [NsItem]

91+

92+-- | A map from namespace names to information about them

84type NsDict = M.Map NsName NsInfo

93type NsDict = M.Map NsName NsInfo

85

94

86-- --------------------------------------------------------------- [ Utility ]

95-- --------------------------------------------------------------- [ Utility ]

@@ -133,10 +142,11 @@ fetchInfo :: IState -- ^ IState to fetch info from

133fetchInfo ist nss =

142fetchInfo ist nss =

134 do let originNss = S.fromList nss

143 do let originNss = S.fromList nss

135 info <- nsDict ist

144 info <- nsDict ist

136− let info' = M.map (filter (filterName . (\(n, _, _) -> n))) info

145+ let info' = M.map (filter filterInclude) info

137 info'' = M.map removeOrphans info'

146 info'' = M.map removeOrphans info'

147+ info''' = M.filter (not . null) info''

138− reachedNss = traceNss info'' originNss S.empty

148+ reachedNss = traceNss info''' originNss S.empty

139− return $ M.filterWithKey (\k _ -> S.member k reachedNss) info''

149+ return $ M.filterWithKey (\k _ -> S.member k reachedNss) info'''

140

150

141

151

142-- | Removes loose class methods and data constructors,

152-- | Removes loose class methods and data constructors,

@@ -160,6 +170,16 @@ filterName (NS n _) = filterName n

160filterName _ = False

170filterName _ = False

161

171

162

172

173+-- | Whether a NsItem should be included in the documentation.

174+-- It must not be Hidden and filterName must return True for the name.

175+-- Also it must have Docs -- without Docs, nothing can be done.

176+filterInclude :: NsItem -- ^ Accessibility to check

177+ -> Bool -- ^ Predicate result

178+filterInclude (name, Just _, Public) | filterName name = True

179+filterInclude (name, Just _, Frozen) | filterName name = True

180+filterInclude _ = False

181+

182+

163-- | Finds all namespaces indirectly referred by a set of namespaces.

183-- | Finds all namespaces indirectly referred by a set of namespaces.

164-- The NsItems of the namespaces are searched for references.

184-- The NsItems of the namespaces are searched for references.

165traceNss :: NsDict -- ^ Mappings of namespaces and their contents

185traceNss :: NsDict -- ^ Mappings of namespaces and their contents

@@ -215,7 +235,7 @@ getAccess ist n =

215 let res = lookupDefAcc n False (tt_ctxt ist)

235 let res = lookupDefAcc n False (tt_ctxt ist)

216 in case res of

236 in case res of

217 [(_, acc)] -> acc

237 [(_, acc)] -> acc

218− _ -> Public

238+ _ -> Hidden

219

239

220-- | Simple predicate for whether an NsItem has Docs

240-- | Simple predicate for whether an NsItem has Docs

221hasDoc :: NsItem -- ^ The NsItem to test

241hasDoc :: NsItem -- ^ The NsItem to test

@@ -403,19 +423,15 @@ createNsDoc ist ns content out =

403 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

423 do let tpath = out </> "docs" </> (genRelNsPath ns "html")

404 dir = takeDirectory tpath

424 dir = takeDirectory tpath

405 file = takeFileName tpath

425 file = takeFileName tpath

406− visible (_, _, Hidden) = False

407− visible _ = True

408 haveDocs (_, Just d, _) = [d]

426 haveDocs (_, Just d, _) = [d]

409 haveDocs _ = []

427 haveDocs _ = []

410− -- Do not document private members

411− content' = filter visible content

412 -- We cannot do anything without a Doc

428 -- We cannot do anything without a Doc

413− content'' = concatMap haveDocs content'

429+ content' = concatMap haveDocs content

414 createDirectoryIfMissing True dir

430 createDirectoryIfMissing True dir

415 (path, h) <- openTempFile dir file

431 (path, h) <- openTempFile dir file

416 BS2.hPut h $ renderHtml $ wrapper (Just ns) $ do

432 BS2.hPut h $ renderHtml $ wrapper (Just ns) $ do

417 H.h1 $ toHtml (nsName2Str ns)

433 H.h1 $ toHtml (nsName2Str ns)

418− H.dl ! class_ "decls" $ forM_ content'' (createOtherDoc ist)

434+ H.dl ! class_ "decls" $ forM_ content' (createOtherDoc ist)

419 hClose h

435 hClose h

420 renameFile path tpath

436 renameFile path tpath

421

437

src/Idris/ParseData.hs+4−3

@@ -42,11 +42,12 @@ Record ::=

42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

43-}

44record :: SyntaxInfo -> IdrisParser PDecl

45−record syn = do (doc, acc) <- try (do

45+record syn = do (doc, acc, opts) <- try (do

46 doc <- option noDocs docComment

47 acc <- optional accessibility

48+ opts <- dataOpts []

48 reserved "record"

49 reserved "record"

49− return (doc, acc))

50+ return (doc, acc, opts))

50 fc <- getFC

51 fc <- getFC

51 tyn_in <- fnName

52 tyn_in <- fnName

52 lchar ':'

53 lchar ':'

@@ -59,7 +60,7 @@ record syn = do (doc, acc) <- try (do

59 syn_namespace syn }

60 syn_namespace syn }

60 let fns = getRecNames rsyn cty

61 let fns = getRecNames rsyn cty

61 mapM_ (\n -> addAcc n acc) fns

62 mapM_ (\n -> addAcc n acc) fns

62− return $ PRecord (fst doc) rsyn fc tyn ty cdoc cn cty

63+ return $ PRecord (fst doc) rsyn fc tyn ty opts cdoc cn cty

63 <?> "record type declaration"

64 <?> "record type declaration"

64 where

65 where

65 getRecNames :: SyntaxInfo -> PTerm -> [Name]

66 getRecNames :: SyntaxInfo -> PTerm -> [Name]

src/Idris/REPL.hs+4−2

@@ -1533,8 +1533,10 @@ getPkgCheck :: Opt -> Maybe String

1533getPkgCheck (PkgCheck str) = Just str

1534getPkgCheck _ = Nothing

1535

1536−-- IdrisDoc

1536+-- | Returns None if given an Opt which is not PkgMkDoc

1537+-- Otherwise returns Just x, where x is the contents of PkgMkDoc

1537−getPkgMkDoc :: Opt -> Maybe String

1538+getPkgMkDoc :: Opt -- ^ Opt to extract

1539+ -> Maybe String -- ^ Result

1538getPkgMkDoc (PkgMkDoc str) = Just str

1540getPkgMkDoc (PkgMkDoc str) = Just str

1539getPkgMkDoc _ = Nothing

1541getPkgMkDoc _ = Nothing

1540

1542

src/Pkg/PParser.hs+6−2

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

1+{-# LANGUAGE OverlappingInstances #-}

2+

1module Pkg.PParser where

3module Pkg.PParser where

2

4

3import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

5import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

@@ -27,6 +29,10 @@ data PkgDesc = PkgDesc { pkgname :: String,

27 }

29 }

28 deriving Show

30 deriving Show

29

31

32+instance TokenParsing PParser where

33+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

34+

35+

30defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

36defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing

31

37

32parseDesc :: FilePath -> IO PkgDesc

38parseDesc :: FilePath -> IO PkgDesc

@@ -78,6 +84,4 @@ pClause = do reserved "executable"; lchar '=';

78 mk <- iName []

84 mk <- iName []

79 st <- get

85 st <- get

80 put (st { makefile = Just (show mk) })

86 put (st { makefile = Just (show mk) })

81− <|> do string "--"; many (satisfy (not . isEol)) ; satisfy isEol

82− return ()

83

87

test/idrisdoc001/TestPrivate.idrnew file+5

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

1+module TestPrivate

2+

3+private

4+iAmPrivate : ()

5+iAmPrivate = ()

test/idrisdoc001/expected+2

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

1Type checking ./TestEmpty.idr

2+Type checking ./TestPrivate.idr

2Warning: Ignoring empty or non-existing namespace 'TestEmpty'

3Warning: Ignoring empty or non-existing namespace 'TestEmpty'

4+Warning: Ignoring empty or non-existing namespace 'TestPrivate'

3No namespaces to generate documentation for

5No namespaces to generate documentation for

test/idrisdoc001/run+1−1

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

1#!/usr/bin/env bash

2−# Tests that no documentation is built for empty namespaces

2+# Tests that no documentation is built for empty and/or private-only namespaces

3idris --mkdoc test_empty.ipkg

4rm -rf *.ibc *_doc

test/idrisdoc001/test_empty.ipkg+1−1

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

1package test_empty

2

3−modules = TestEmpty

3+modules = TestEmpty, TestPrivate

4

test/idrisdoc006/A.idr → test/idrisdoc006/A/fully/Qualified/NAME.idrrenamed+1−1

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

1−module A

1+module A.fully.Qualified.NAME

2

3||| This is another test

4data Test : Type where

test/idrisdoc006/expected+6−5

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

1−Type checking ./A.idr

1+Type checking ./A/fully/Qualified/NAME.idr

2+IdrisDoc file written

2Type checking ./B.idr

3Type checking ./B.idr

3−A: Check

4+A.fully.Qualified.NAME.html

4−B: Check

5+B.html

5−A

6+A.fully.Qualified.NAME is in the index

6−B

7+B is in the index

test/idrisdoc006/package_a.ipkg+1−1

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

1package test_merge

2

3−modules = A

3+modules = A.fully.Qualified.NAME

4

test/idrisdoc006/run+9−9

@@ -1,17 +1,17 @@

1#!/usr/bin/env bash

2−# Tests that documentation properly is merged with existing

2+# Tests that documentation properly is merged with existent.

3idris --mkdoc package_a.ipkg

4+[ -f test_merge_doc/IdrisDoc ] && echo "IdrisDoc file written"

4idris --mkdoc package_b.ipkg

5idris --mkdoc package_b.ipkg

5−[ -f test_merge_doc/docs/A.html ] && echo "A: Check"

6−[ -f test_merge_doc/docs/B.html ] && echo "B: Check"

6+ls -1p test_merge_doc/docs

7−if grep -q "href\\=\"docs/A\\.html\"" test_merge_doc/index.html; then

7+if grep -q "href\\=\"docs/A.fully.Qualified.NAME\\.html\"" test_merge_doc/index.html; then

8− echo A

8+ echo A.fully.Qualified.NAME is in the index

9else

10− echo A is not in the index

10+ echo A.fully.Qualified.NAME is NOT in the index

11fi

12if grep -q "href\\=\"docs/B\\.html\"" test_merge_doc/index.html; then

13− echo B

13+ echo B is in the index

14else

15− echo B is not in the index

15+ echo B is NOT in the index

16fi

17−rm -rf *.ibc *_doc

17+rm -rf *.ibc *_doc A/fully/Qualified/NAME.ibc

test/idrisdoc008/Abstract.idrnew file+5

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

1+module Abstract

2+

3+abstract

4+frozen : ()

5+frozen = ()

test/idrisdoc008/Visible.idrnew file+5

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

1+module Visible

2+

3+public

4+visible : ()

5+visible = ()

test/idrisdoc008/expectednew file+4

@@ -0,0 +1,4 @@

1+Type checking ./Abstract.idr

2+Type checking ./Visible.idr

3+Abstract members are documented

4+Public members are documented

test/idrisdoc008/runnew file+6

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

1+#!/usr/bin/env bash

2+# Tests that documentation is generated for both public and abstract members.

3+idris --mkdoc visibility.ipkg

4+[ -f visibility_doc/docs/Abstract.html ] && echo "Abstract members are documented"

5+[ -f visibility_doc/docs/Visible.html ] && echo "Public members are documented"

6+rm -rf *.ibc *_doc

test/idrisdoc008/visibility.ipkgnew file+4

@@ -0,0 +1,4 @@

1+package visibility

2+

3+modules = Abstract, Visible

4+