555d58f · Idris-dev · git.iko.soy

CHANGELOG+1

@@ -8,6 +8,7 @@ New in 0.9.13:

88* Many more of the basic functions and datatypes are documented.

99* Removed javascript lib in favor of idris-hackers/iQuery

1010* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)

11+* Remove :info REPL command, subsume and enhance its functionality in the :doc command

1112

1213Internal changes

1314

CONTRIBUTORS+1

@@ -11,6 +11,7 @@ Simon Fowler

1111Google

1212Cezar Ionescu

1313Irene Knapp

14+Paul Koerbitz

1415Shea Levy

1516Mathnerd314

1617Hannes Mehnert

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

main/Main.hs+1−1

@@ -100,7 +100,7 @@ usagemsg = usagemsghdr ++ "\n" ++

100100 "\t --clean IPKG Clean package\n" ++

101101 "\t --build IPKG Build package\n" ++

102102 "\t --mkdoc IPKG Generate IdrisDoc for package\n" ++

103− "\t -e --eval EXPR Evaluate an expression without loading the REPL" ++

103+ "\t -e --eval EXPR Evaluate an expression without loading the REPL\n" ++

104104 "\t --exec EXPR Execute as idris\n" ++

105105 "\t --libdir Display library directory\n" ++

106106 "\t --link Display link flags\n" ++

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+4−5

@@ -285,7 +285,6 @@ data Command = Quit

285285 | HNF PTerm

286286 | TestInline PTerm

287287 | Defn Name

288− | Info Name

289288 | Missing Name

290289 | DynamicLink FilePath

291290 | ListDynamic

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

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

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

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

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

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

487486 | PClass Docstring SyntaxInfo FC

488487 [t] -- constraints

489488 Name

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

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

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

571570declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

575574declared (PDSL n _) = [n]

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

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

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

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

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

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

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

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

589588tldeclared (PParams _ _ ds) = []

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

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

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

606605defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

610609defined (PDSL n _) = [n]

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+2−2

@@ -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]})

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/Docs.hs+44−9

@@ -27,6 +27,8 @@ data Docs = FunDoc FunDoc

2727 [FunDoc] -- data constructor docs

2828 | ClassDoc Name Docstring -- class docs

2929 [FunDoc] -- method docs

30+ [(Name, Maybe Docstring)] -- parameters and their docstrings

31+ [PTerm] -- instances

3032 deriving Show

3133

3234showDoc d | nullDocstring d = empty

@@ -66,16 +68,47 @@ pprintFD imp (FD n doc args ty f)

6668 showArgs [] _ = []

6769

6870

69−

71+pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

7072pprintDocs imp (FunDoc d) = pprintFD imp d

7173pprintDocs imp (DataDoc t args)

7274 = text "Data type" <+> pprintFD imp t <$>

7375 nest 4 (text "Constructors:" <> line <>

7476 vsep (map (pprintFD imp) args))

75−pprintDocs imp (ClassDoc n doc meths)

76− = text "Type class" <+> prettyName imp [] n <$> -- parameters?

77+pprintDocs imp (ClassDoc n doc meths params instances)

78+ = nest 4 (text "Type class" <+> prettyName imp [] n <>

79+ if nullDocstring doc then empty else line <> renderDocstring doc)

80+ <> line <$>

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

82+ <> line <$>

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

78− vsep (map (pprintFD imp) meths))

84+ vsep (map (pprintFD imp) meths))

85+ <$>

86+ nest 4 (text "Instances:" <$>

87+ vsep (if null instances' then [text "<no instances>"]

88+ else map dumpInstance instances'))

89+ <>

90+ if null subclasses then empty

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

92+ vsep (map (dumpInstance . remConstraint) subclasses))

93+ where

94+ params' = map (\x -> (fst x, False)) params

95+

96+ dumpInstance :: PTerm -> Doc OutputAnnotation

97+ dumpInstance = pprintPTerm imp params' []

98+

99+ remConstraint (PPi (Constraint _ _) _ tm _) = tm

100+ remConstraint (PPi x y z pt) = PPi x y z (remConstraint pt)

101+ remConstraint p = p

102+

103+ hasConstraint (PPi (Constraint _ _) _ _ _) = True

104+ hasConstraint (PPi _ _ _ pt) = hasConstraint pt

105+ hasConstraint _ = False

106+

107+ (subclasses, instances') = partition hasConstraint instances

108+

109+ prettyParameters = if any (isJust . snd) params

110+ then vsep (map (\(n,md) -> prettyName False params' n <+> maybe empty showDoc md) params)

111+ else hsep (punctuate comma (map (prettyName False params' . fst) params))

79112

80113getDocs :: Name -> Idris Docs

81114getDocs n

@@ -96,11 +129,13 @@ docData n ti

96129docClass :: Name -> ClassInfo -> Idris Docs

97130docClass n ci

98131 = do i <- getIState

99− let docstr = case lookupCtxt n (idris_docstrings i) of

100− [str] -> fst str

101− _ -> emptyDocstring

102− mdocs <- mapM docFun (map fst (class_methods ci))

103− return (ClassDoc n docstr mdocs)

132+ ctxt <- getContext

133+ let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

134+ docstr = maybe emptyDocstring fst docStrings

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

136+ instances = map (delabTy i) (class_instances ci)

137+ mdocs <- mapM (docFun .fst) (class_methods ci)

138+ return $ ClassDoc n docstr mdocs params instances

104139

105140docFun :: Name -> Idris FunDoc

106141docFun n

src/Idris/ElabDecls.hs+5−5

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

771771

772772

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

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

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

776− = 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, [])])

777777 -- TODO think: something more in info?

778778 cty' <- implicit info syn cn cty

779779 i <- getIState

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

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

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

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

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

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

23462346 | what /= ETypes

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

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

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

23492349 | otherwise

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

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

src/Idris/Help.hs−1

@@ -35,7 +35,6 @@ help =

3535 ([":apropos"], NoArg, "Search names, types, and documentation"),

3636 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

3737 ([":callswho", ":cw"], NameArg, "List the callees of some name"),

38− ([":i", ":info"], NameArg, "Display information about a type class"),

3938 ([":total"], NameArg, "Check the totality of a name"),

4039 ([":r",":reload"], NoArg, "Reload current file"),

4140 ([":l",":load"], FileArg, "Load a new file"),

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+9−9

@@ -157,9 +157,9 @@ removeOrphans list =

157157 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

158158 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

159159

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

161− names (Just (ClassDoc _ _ fds)) = map (\(FD n _ _ _ _) -> n) fds

162− names _ = []

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

161+ names (Just (ClassDoc _ _ fds _ _)) = map (\(FD n _ _ _ _) -> n) fds

162+ names _ = []

163163

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

165165filterName :: Name -- ^ Name to check

@@ -207,11 +207,11 @@ referredNss (n, Just d, _) =

207207 names = concatMap (extractPTermNames) ts

208208 in S.map getNs $ S.fromList names

209209

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

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

212− getFunDocs (ClassDoc _ _ fs) = fs

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

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

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

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

212+ getFunDocs (ClassDoc _ _ fs _ _) = fs

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

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

215215

216216

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

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

553553 -> H.Html -- ^ Resulting HTML

554554createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

555555

556−createOtherDoc ist (ClassDoc n docstring fds) = do

556+createOtherDoc ist (ClassDoc n docstring fds _ _) = do

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

558558 H.span ! class_ "word" $ do "class"; nbsp

559559 H.span ! class_ "name type"

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−32

@@ -386,7 +386,6 @@ ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

386386ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

387387ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

388388 iPrintResult ""

389−ideslaveProcess fn (Info n) = process stdout fn (Info n)

390389ideslaveProcess fn (Search t) = process stdout fn (Search t)

391390ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

392391-- RmProof and AddProof not supported!

@@ -690,12 +689,6 @@ process h fn (DebugInfo n)

690689 iputStrLn $ "Size change: " ++ show sc

691690 when (not (null cg')) $ do iputStrLn "Call graph:\n"

692691 iputStrLn (show cg')

693−process h fn (Info n)

694− = do i <- getIState

695− case lookupCtxt n (idris_classes i) of

696− [c] -> do info <- classInfo c

697− ihRenderResult h info

698− _ -> iPrintError "Not a class"

699692process h fn (Search t) = iPrintError "Not implemented"

700693-- FIXME: There is far too much repetition in the cases below!

701694process h fn (CaseSplitAt updatefile l n)

@@ -1103,31 +1096,6 @@ process h fn (MakeDoc s) =

11031096 Left err -> iPrintError err

11041097

11051098

1106−classInfo :: ClassInfo -> Idris (Doc OutputAnnotation)

1107−classInfo ci = do ist <- getIState

1108− ctxt <- getContext

1109− return $

1110− text "Parameters:" <+>

1111− hsep (punctuate comma (map (prettyName False params') params)) <>

1112− line <> line <>

1113− text "Methods:" <> line <>

1114− indent 2 (vsep (map (dumpMethod ist) (class_methods ci))) <> line <> line <>

1115− text "Default superclass instances:" <>

1116− line <>

1117− indent 2 (vsep (map (dumpDefaultInstance ist) (class_default_superclasses ci))) <>

1118− line <>

1119− text "Instances:" <> line <>

1120− indent 2 (vsep (map (dumpInstance ist ctxt) (class_instances ci)))

1121− where dumpMethod :: IState -> (Name, (FnOpts, PTerm)) -> Doc OutputAnnotation

1122− dumpMethod ist (n, (_, t)) = prettyName False [] n <+> colon <+> pp ist t

1123− dumpDefaultInstance :: IState -> PDecl -> Doc OutputAnnotation

1124− dumpDefaultInstance ist (PInstance _ _ _ _ _ t _ _) = pp ist t

1125− dumpInstance :: IState -> Context -> Name -> Doc OutputAnnotation

1126− dumpInstance ist ctxt n = pp ist $ delabTy ist n

1127− params = class_params ci

1128− params' = zip params (repeat False)

1129− pp ist = pprintPTerm (opt_showimp (idris_options ist)) params' []

1130−

11311099showTotal :: Totality -> IState -> String

11321100showTotal t@(Partial (Other ns)) i

11331101 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

src/Idris/REPLParser.hs−1

@@ -59,7 +59,6 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

5959 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

6060 <|> try (do cmd ["u", "universes"]; eof; return Universes)

6161 <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

62− <|> try (do cmd ["i", "info"]; n <- P.fnName; eof; return (Info n))

6362 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

6463 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

6564 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

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