git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into fix/1047-repl-doc-for-typeclasses
commitaf3816ec445bf49fb82ab0d989602172e7362165 authorPaul Koerbitz <paul.koerbitz@theppro.com> dateThu 1 May 2014, 16:20 (12 years ago) parentf5705eb8f8a40f
30 files changed+165−83
compare with master
unifiedsplit
config.mk+1−1 idris.cabal+5 libs/prelude/Prelude/Algebra.idr+21−21 src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+6−6 src/Idris/Core/CaseTree.hs+2 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/Evaluate.hs+8−1 src/Idris/Core/ProofState.hs+3−3 src/Idris/Core/TT.hs+9 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+9−7 src/Idris/IBC.hs+5−3 src/Idris/IdrisDoc.hs+26−10 src/Idris/ParseData.hs+4−3 src/Idris/REPL.hs+4−2 src/Pkg/PParser.hs+6−2 test/idrisdoc001/TestPrivate.idr+5 test/idrisdoc001/expected+2 test/idrisdoc001/run+1−1 test/idrisdoc001/test_empty.ipkg+1−1 test/idrisdoc006/A.idr → test/idrisdoc006/A/fully/Qualified/NAME.idr+1−1 test/idrisdoc006/expected+6−5 test/idrisdoc006/package_a.ipkg+1−1 test/idrisdoc006/run+9−9 test/idrisdoc008/Abstract.idr+5 test/idrisdoc008/Visible.idr+5 test/idrisdoc008/expected+4 test/idrisdoc008/run+6 test/idrisdoc008/visibility.ipkg+4
config.mk+1−1
@@ -1,4 +1,4 @@
1−CC :=cc
1+CC ?=cc
22CABAL :=cabal
33CFLAGS :=-O2 -Wall $(CFLAGS)
44#CABALFLAGS :=
idris.cabal+5
@@ -339,12 +339,17 @@ Extra-source-files:
339339 test/idrisdoc005/*.ipkg
340340 test/idrisdoc006/run
341341 test/idrisdoc006/expected
342+ test/idrisdoc006/A/fully/Qualified/NAME.idr
342343 test/idrisdoc006/*.idr
343344 test/idrisdoc006/*.ipkg
344345 test/idrisdoc007/run
345346 test/idrisdoc007/expected
346347 test/idrisdoc007/*.idr
347348 test/idrisdoc007/*.ipkg
349+ test/idrisdoc008/run
350+ test/idrisdoc008/expected
351+ test/idrisdoc008/*.idr
352+ test/idrisdoc008/*.ipkg
348353
349354 test/interactive001/run
350355 test/interactive001/input
libs/prelude/Prelude/Algebra.idr+21−21
@@ -21,7 +21,7 @@ class Semigroup a where
2121 (<+>) : a -> a -> a
2222
2323class 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
2525
2626-- Sets equipped with a single binary operation that is associative, along with
2727-- a neutral element for that binary operation. Must satisfy the following
@@ -35,8 +35,8 @@ class Semigroup a => Monoid a where
3535 neutral : a
3636
3737class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38− monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39− monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
38+ total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39+ total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
4040
4141-- Sets equipped with a single binary operation that is associative, along with
4242-- a neutral element for that binary operation and inverses for all elements.
@@ -53,8 +53,8 @@ class Monoid a => Group a where
5353 inverse : a -> a
5454
5555class (VerifiedMonoid a, Group a) => VerifiedGroup a where
56− groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57− groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
56+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
5858
5959(<->) : Group a => a -> a -> a
6060(<->) left right = left <+> (inverse right)
@@ -75,7 +75,7 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where
7575class Group a => AbelianGroup a where { }
7676
7777class (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
7979
8080-- Sets equipped with two binary operations, one associative and commutative
8181-- supplied with a neutral element, and the other associative, with
@@ -100,9 +100,9 @@ class AbelianGroup a => Ring a where
100100 (<*>) : a -> a -> a
101101
102102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
103− ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104− 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)
103+ total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104+ total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
106106
107107-- Sets equipped with two binary operations, one associative and commutative
108108-- supplied with a neutral element, and the other associative supplied with a
@@ -130,8 +130,8 @@ class Ring a => RingWithUnity a where
130130 unity : a
131131
132132class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
133− ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134− ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
133+ total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134+ total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
135135
136136-- Sets equipped with a binary operation that is commutative, associative and
137137-- idempotent. Must satisfy the following laws:
@@ -146,9 +146,9 @@ class JoinSemilattice a where
146146 join : a -> a -> a
147147
148148class JoinSemilattice a => VerifiedJoinSemilattice a where
149− 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
151− joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
149+ total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
150+ total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151+ total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
152152
153153-- Sets equipped with a binary operation that is commutative, associative and
154154-- idempotent. Must satisfy the following laws:
@@ -163,9 +163,9 @@ class MeetSemilattice a where
163163 meet : a -> a -> a
164164
165165class MeetSemilattice a => VerifiedMeetSemilattice a where
166− 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
168− meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
166+ total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167+ total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168+ total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
169169
170170-- Sets equipped with a binary operation that is commutative, associative and
171171-- idempotent and supplied with a neutral element. Must satisfy the following
@@ -184,7 +184,7 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
184184 bottom : a
185185
186186class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
187− boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
187+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
188188
189189-- Sets equipped with a binary operation that is commutative, associative and
190190-- idempotent and supplied with a neutral element. Must satisfy the following
@@ -203,7 +203,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
203203 top : a
204204
205205class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
206− boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
206+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
207207
208208-- Sets equipped with two binary operations that are both commutative,
209209-- associative and idempotent, along with absorbtion laws for relating the two
@@ -223,8 +223,8 @@ class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMe
223223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
224224
225225class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
226− latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227− latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
226+ total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227+ total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
228228
229229-- Sets equipped with two binary operations that are both commutative,
230230-- 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)
959959 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
960960 econ (doc, argDocs, n, t, fc, fs)
961961 = (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)
963963 = if tn `elem` ns
964964 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
966966 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
967− cdoc (dec cn) conty
967+ opts cdoc (dec cn) conty
968968 where conty = piBindp expl ps (expandParams dec ps ns [] cty)
969969expandParamsD rhs ist dec ps ns (PParams f params pds)
970970 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
src/Idris/AbsSyntaxTree.hs+6−6
@@ -482,7 +482,7 @@ data PDecl' t
482482 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
483483 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
484484 | 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
486486 | PClass Docstring SyntaxInfo FC
487487 [t] -- constraints
488488 Name
@@ -568,7 +568,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
568568declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
569569declared (PParams _ _ ds) = concatMap declared ds
570570declared (PNamespace _ ds) = concatMap declared ds
571−declared (PRecord _ _ _ n _ _ c _) = [n, c]
571+declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
572572declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms
573573declared (PInstance _ _ _ _ _ _ _ _) = []
574574declared (PDSL n _) = [n]
@@ -582,7 +582,7 @@ tldeclared (PFix _ _ _) = []
582582tldeclared (PTy _ _ _ _ _ n t) = [n]
583583tldeclared (PPostulate _ _ _ _ n t) = [n]
584584tldeclared (PClauses _ _ n _) = [] -- not a declaration
585−tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]
585+tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
586586tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
587587 where fstt (_, _, a, _, _, _) = a
588588tldeclared (PParams _ _ ds) = []
@@ -603,7 +603,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
603603defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
604604defined (PParams _ _ ds) = concatMap defined ds
605605defined (PNamespace _ ds) = concatMap defined ds
606−defined (PRecord _ _ _ n _ _ c _) = [n, c]
606+defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
607607defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms
608608defined (PInstance _ _ _ _ _ _ _ _) = []
609609defined (PDSL n _) = [n]
@@ -1619,8 +1619,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm
16191619 where -- TODO THINK added niTacImp, but is it right?
16201620 ni env (PRef _ n)
16211621 | n `elem` vars && not (n `elem` env)
1622− = case lookupTy n (tt_ctxt ist) of
1623− [] -> [n]
1622+ = case lookupDefExact n (tt_ctxt ist) of
1623+ Nothing -> [n]
16241624 _ -> []
16251625 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
16261626 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)
712712 | n == n' = Case repl (map (substAlt n repl) alts)
713713 | otherwise = Case n' (map (substAlt n repl) alts)
714714substSC 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
715717substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
716718
717719substAlt :: Name -> Name -> CaseAlt -> CaseAlt
src/Idris/Core/Elaborate.hs+1−1
@@ -64,7 +64,7 @@ loadState :: Elab' aux ()
6464loadState = do (ES p s e) <- get
6565 case e of
6666 Just st -> put st
67− _ -> fail "Nothing to undo"
67+ _ -> lift $ Error . Msg $ "Nothing to undo"
6868
6969getNameFrom :: Name -> Elab' aux Name
7070getNameFrom 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,
1111 lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
14− Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
14+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where
1515
1616import Debug.Trace
1717import Control.Applicative hiding (Const)
@@ -961,3 +961,10 @@ uniqueNameCtxt ctxt n hs
961961 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
962962 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs
963963 | 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
1515
1616import Control.Monad.State.Strict
1717import Control.Applicative hiding (empty)
18−import Control.Arrow (first)
18+import Control.Arrow ((***))
1919import Data.List
2020import Debug.Trace
2121
@@ -666,7 +666,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
666666 let scr = last $ tail args'
667667 let indxnames = makeIndexNames indicies
668668 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)
670670 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))
671671 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
672672 action (\ps -> ps {holes = holes ps \\ [x]})
@@ -872,7 +872,7 @@ processTactic QED ps = case holes ps of
872872 _ -> fail "Still holes to fill."
873873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
874874processTactic Undo ps = case previous ps of
875− Nothing -> fail "Nothing to undo."
875+ Nothing -> Error . Msg $ "Nothing to undo."
876876 Just pold -> return (pold, "")
877877processTactic EndUnify ps
878878 = let (h, ns_in) = unified ps
src/Idris/Core/TT.hs+9
@@ -1223,3 +1223,12 @@ orderPats tm = op [] tm
12231223 = (n', t') : insert n t ps
12241224 | otherwise = (n,t):(n',t'):ps
12251225
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
138138 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
139139 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
140140 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)
142142 = rnf x1 `seq`
143143 rnf x2 `seq`
144144 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` ()
146146 rnf (PClass x1 x2 x3 x4 x5 x6 x7)
147147 = rnf x1 `seq`
148148 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
8686 ctxt <- getContext
8787 i <- getIState
8888
89− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
89+ logLvl 5 $ show n ++ " pre-type " ++ showTmImpls ty'
9090 ty' <- addUsingConstraints syn fc ty'
9191 ty' <- implicit info syn n ty'
9292
9393 let ty = addImpl i ty'
9494 inacc = inaccessibleArgs 0 ty
95− logLvl 3 $ show n ++ " type " ++ showTmImpls ty
95+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
96+ logLvl 5 $ show n ++ " type " ++ showTmImpls ty
9697 logLvl 3 $ show n ++ ": inaccessible arguments: " ++ show inacc
9798
9899 ((tyT, defer, is), log) <-
@@ -770,9 +771,9 @@ elabTransform info fc safe lhs_in rhs_in
770771
771772
772773elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
773− PTerm -> Docstring -> Name -> PTerm -> Idris ()
774−elabRecord info syn doc fc tyn ty cdoc cn cty
775− = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
774+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
775+elabRecord info syn doc fc tyn ty opts cdoc cn cty
776+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
776777 -- TODO think: something more in info?
777778 cty' <- implicit info syn cn cty
778779 i <- getIState
@@ -1671,6 +1672,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
16711672 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
16721673 addDeferred def''
16731674 mapM_ (elabCaseBlock info opts) is
1675+ logLvl 5 ("Checked wval " ++ show wval')
16741676 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
16751677 let cwvaltyN = explicitNames cwvalty
16761678 let cwvalN = explicitNames cwval
@@ -2318,10 +2320,10 @@ elabDecl' what info (PClass doc s f cs n ps ds)
23182320elabDecl' what info (PInstance s f cs n ps t expn ds)
23192321 = do iLOG $ "Elaborating instance " ++ show n
23202322 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)
23222324 | what /= ETypes
23232325 = 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
23252327 | otherwise
23262328 = do iLOG $ "Elaborating [type of] " ++ show tyn
23272329 elabData info s doc [] f [] (PLaterdecl tyn ty)
src/Idris/IBC.hs+5−3
@@ -30,7 +30,7 @@ import Codec.Compression.Zlib (compress)
3030import Util.Zlib (decompressEither)
3131
3232ibcVersion :: Word8
33−ibcVersion = 67
33+ibcVersion = 68
3434
3535data IBCFile = IBCFile { ver :: Word8,
3636 sourcefile :: FilePath,
@@ -1425,7 +1425,7 @@ instance (Binary t) => Binary (PDecl' t) where
14251425 PNamespace x1 x2 -> do putWord8 5
14261426 put x1
14271427 put x2
1428− PRecord x1 x2 x3 x4 x5 x6 x7 x8 ->
1428+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->
14291429 do putWord8 6
14301430 put x1
14311431 put x2
@@ -1435,6 +1435,7 @@ instance (Binary t) => Binary (PDecl' t) where
14351435 put x6
14361436 put x7
14371437 put x8
1438+ put x9
14381439 PClass x1 x2 x3 x4 x5 x6 x7
14391440 -> do putWord8 7
14401441 put x1
@@ -1513,7 +1514,8 @@ instance (Binary t) => Binary (PDecl' t) where
15131514 x6 <- get
15141515 x7 <- get
15151516 x8 <- get
1516− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8)
1517+ x9 <- get
1518+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)
15171519 7 -> do x1 <- get
15181520 x2 <- get
15191521 x3 <- get
src/Idris/IdrisDoc.hs+26−10
@@ -77,10 +77,19 @@ generateDocs ist nss' out =
7777
7878-- ----------------------------------------------------------------- [ Types ]
7979
80+-- | Either an error message or a result
8081type Failable = Either String
82+
83+-- | Internal representation of a fully qualified namespace name
8184type NsName = [T.Text]
85+
86+-- | All information to be documented about a single namespace member
8287type NsItem = (Name, Maybe Docs, Accessibility)
88+
89+-- | All information to be documented about a namespace
8390type NsInfo = [NsItem]
91+
92+-- | A map from namespace names to information about them
8493type NsDict = M.Map NsName NsInfo
8594
8695-- --------------------------------------------------------------- [ Utility ]
@@ -133,10 +142,11 @@ fetchInfo :: IState -- ^ IState to fetch info from
133142fetchInfo ist nss =
134143 do let originNss = S.fromList nss
135144 info <- nsDict ist
136− let info' = M.map (filter (filterName . (\(n, _, _) -> n))) info
145+ let info' = M.map (filter filterInclude) info
137146 info'' = M.map removeOrphans info'
138− reachedNss = traceNss info'' originNss S.empty
139− return $ M.filterWithKey (\k _ -> S.member k reachedNss) info''
147+ info''' = M.filter (not . null) info''
148+ reachedNss = traceNss info''' originNss S.empty
149+ return $ M.filterWithKey (\k _ -> S.member k reachedNss) info'''
140150
141151
142152-- | Removes loose class methods and data constructors,
@@ -160,6 +170,16 @@ filterName (NS n _) = filterName n
160170filterName _ = False
161171
162172
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+
163183-- | Finds all namespaces indirectly referred by a set of namespaces.
164184-- The NsItems of the namespaces are searched for references.
165185traceNss :: NsDict -- ^ Mappings of namespaces and their contents
@@ -215,7 +235,7 @@ getAccess ist n =
215235 let res = lookupDefAcc n False (tt_ctxt ist)
216236 in case res of
217237 [(_, acc)] -> acc
218− _ -> Public
238+ _ -> Hidden
219239
220240-- | Simple predicate for whether an NsItem has Docs
221241hasDoc :: NsItem -- ^ The NsItem to test
@@ -403,19 +423,15 @@ createNsDoc ist ns content out =
403423 do let tpath = out </> "docs" </> (genRelNsPath ns "html")
404424 dir = takeDirectory tpath
405425 file = takeFileName tpath
406− visible (_, _, Hidden) = False
407− visible _ = True
408426 haveDocs (_, Just d, _) = [d]
409427 haveDocs _ = []
410− -- Do not document private members
411− content' = filter visible content
412428 -- We cannot do anything without a Doc
413− content'' = concatMap haveDocs content'
429+ content' = concatMap haveDocs content
414430 createDirectoryIfMissing True dir
415431 (path, h) <- openTempFile dir file
416432 BS2.hPut h $ renderHtml $ wrapper (Just ns) $ do
417433 H.h1 $ toHtml (nsName2Str ns)
418− H.dl ! class_ "decls" $ forM_ content'' (createOtherDoc ist)
434+ H.dl ! class_ "decls" $ forM_ content' (createOtherDoc ist)
419435 hClose h
420436 renameFile path tpath
421437
src/Idris/ParseData.hs+4−3
@@ -42,11 +42,12 @@ Record ::=
4242 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
4343-}
4444record :: SyntaxInfo -> IdrisParser PDecl
45−record syn = do (doc, acc) <- try (do
45+record syn = do (doc, acc, opts) <- try (do
4646 doc <- option noDocs docComment
4747 acc <- optional accessibility
48+ opts <- dataOpts []
4849 reserved "record"
49− return (doc, acc))
50+ return (doc, acc, opts))
5051 fc <- getFC
5152 tyn_in <- fnName
5253 lchar ':'
@@ -59,7 +60,7 @@ record syn = do (doc, acc) <- try (do
5960 syn_namespace syn }
6061 let fns = getRecNames rsyn cty
6162 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
6364 <?> "record type declaration"
6465 where
6566 getRecNames :: SyntaxInfo -> PTerm -> [Name]
src/Idris/REPL.hs+4−2
@@ -1533,8 +1533,10 @@ getPkgCheck :: Opt -> Maybe String
15331533getPkgCheck (PkgCheck str) = Just str
15341534getPkgCheck _ = Nothing
15351535
1536−-- IdrisDoc
1537−getPkgMkDoc :: Opt -> Maybe String
1536+-- | Returns None if given an Opt which is not PkgMkDoc
1537+-- Otherwise returns Just x, where x is the contents of PkgMkDoc
1538+getPkgMkDoc :: Opt -- ^ Opt to extract
1539+ -> Maybe String -- ^ Result
15381540getPkgMkDoc (PkgMkDoc str) = Just str
15391541getPkgMkDoc _ = Nothing
15401542
src/Pkg/PParser.hs+6−2
@@ -1,3 +1,5 @@
1+{-# LANGUAGE OverlappingInstances #-}
2+
13module Pkg.PParser where
24
35import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
@@ -27,6 +29,10 @@ data PkgDesc = PkgDesc { pkgname :: String,
2729 }
2830 deriving Show
2931
32+instance TokenParsing PParser where
33+ someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
34+
35+
3036defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (sUN "") Nothing
3137
3238parseDesc :: FilePath -> IO PkgDesc
@@ -78,6 +84,4 @@ pClause = do reserved "executable"; lchar '=';
7884 mk <- iName []
7985 st <- get
8086 put (st { makefile = Just (show mk) })
81− <|> do string "--"; many (satisfy (not . isEol)) ; satisfy isEol
82− return ()
8387
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 @@
11Type checking ./TestEmpty.idr
2+Type checking ./TestPrivate.idr
23Warning: Ignoring empty or non-existing namespace 'TestEmpty'
4+Warning: Ignoring empty or non-existing namespace 'TestPrivate'
35No namespaces to generate documentation for
test/idrisdoc001/run+1−1
@@ -1,4 +1,4 @@
11#!/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
33idris --mkdoc test_empty.ipkg
44rm -rf *.ibc *_doc
test/idrisdoc001/test_empty.ipkg+1−1
@@ -1,4 +1,4 @@
11package test_empty
22
3−modules = TestEmpty
3+modules = TestEmpty, TestPrivate
44
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
22
33||| This is another test
44data 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
23Type checking ./B.idr
3−A: Check
4−B: Check
5−A
6−B
4+A.fully.Qualified.NAME.html
5+B.html
6+A.fully.Qualified.NAME is in the index
7+B is in the index
test/idrisdoc006/package_a.ipkg+1−1
@@ -1,4 +1,4 @@
11package test_merge
22
3−modules = A
3+modules = A.fully.Qualified.NAME
44
test/idrisdoc006/run+9−9
@@ -1,17 +1,17 @@
11#!/usr/bin/env bash
2−# Tests that documentation properly is merged with existing
2+# Tests that documentation properly is merged with existent.
33idris --mkdoc package_a.ipkg
4+[ -f test_merge_doc/IdrisDoc ] && echo "IdrisDoc file written"
45idris --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"
7−if grep -q "href\\=\"docs/A\\.html\"" test_merge_doc/index.html; then
8− echo A
6+ls -1p test_merge_doc/docs
7+if grep -q "href\\=\"docs/A.fully.Qualified.NAME\\.html\"" test_merge_doc/index.html; then
8+ echo A.fully.Qualified.NAME is in the index
99else
10− echo A is not in the index
10+ echo A.fully.Qualified.NAME is NOT in the index
1111fi
1212if grep -q "href\\=\"docs/B\\.html\"" test_merge_doc/index.html; then
13− echo B
13+ echo B is in the index
1414else
15− echo B is not in the index
15+ echo B is NOT in the index
1616fi
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+