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

CHANGELOG+1

compare with master

unifiedsplit

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

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

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

10* 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

11

12

12Internal changes

13Internal changes

13

14

CONTRIBUTORS+1

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

11Google

12Cezar Ionescu

13Irene Knapp

14+Paul Koerbitz

14Shea Levy

15Shea Levy

15Mathnerd314

16Mathnerd314

16Hannes Mehnert

17Hannes Mehnert

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

main/Main.hs+1−1

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

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

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

102 "\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" ++

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

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

106 "\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)

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

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

285 | HNF PTerm

286 | TestInline PTerm

287 | Defn Name

288− | Info Name

289 | Missing Name

288 | Missing Name

290 | DynamicLink FilePath

289 | DynamicLink FilePath

291 | ListDynamic

290 | ListDynamic

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

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

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

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

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

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

484 | 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

487 | PClass Docstring SyntaxInfo FC

486 | PClass Docstring SyntaxInfo FC

488 [t] -- constraints

487 [t] -- constraints

489 Name

488 Name

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

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

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

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

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

571declared (PNamespace _ ds) = concatMap declared ds

570declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

575declared (PDSL n _) = [n]

574declared (PDSL n _) = [n]

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

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

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

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

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

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

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

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

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

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

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

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

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

589tldeclared (PParams _ _ ds) = []

588tldeclared (PParams _ _ ds) = []

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

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

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

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

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

606defined (PNamespace _ ds) = concatMap defined ds

605defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

610defined (PDSL n _) = [n]

609defined (PDSL n _) = [n]

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

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

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

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

27 [FunDoc] -- data constructor docs

28 | ClassDoc Name Docstring -- class docs

29 [FunDoc] -- method docs

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

31+ [PTerm] -- instances

30 deriving Show

32 deriving Show

31

33

32showDoc d | nullDocstring d = empty

34showDoc d | nullDocstring d = empty

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

66 showArgs [] _ = []

68 showArgs [] _ = []

67

69

68

70

69−

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

70pprintDocs imp (FunDoc d) = pprintFD imp d

72pprintDocs imp (FunDoc d) = pprintFD imp d

71pprintDocs imp (DataDoc t args)

73pprintDocs imp (DataDoc t args)

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

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

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

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

74 vsep (map (pprintFD imp) args))

76 vsep (map (pprintFD imp) args))

75−pprintDocs imp (ClassDoc n doc meths)

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

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

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 <$>

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

83 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))

79

112

80getDocs :: Name -> Idris Docs

113getDocs :: Name -> Idris Docs

81getDocs n

114getDocs n

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

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

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

97docClass n ci

130docClass n ci

98 = do i <- getIState

131 = do i <- getIState

132+ ctxt <- getContext

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

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

100− [str] -> fst str

101− _ -> emptyDocstring

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)

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

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

103− return (ClassDoc n docstr mdocs)

138+ return $ ClassDoc n docstr mdocs params instances

104

139

105docFun :: Name -> Idris FunDoc

140docFun :: Name -> Idris FunDoc

106docFun n

141docFun n

src/Idris/ElabDecls.hs+5−5

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

771

772

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

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

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

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

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

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

777 -- TODO think: something more in info?

778 cty' <- implicit info syn cn cty

779 i <- getIState

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

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

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

2344 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)

2346 | what /= ETypes

2347 = 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

2349 | otherwise

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

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

src/Idris/Help.hs−1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

159

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

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

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

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

162− names _ = []

162+ names _ = []

163

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

165filterName :: Name -- ^ Name to check

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

207 names = concatMap (extractPTermNames) ts

208 in S.map getNs $ S.fromList names

209

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

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

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

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

212− getFunDocs (ClassDoc _ _ fs) = fs

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

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

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

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

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

215

216

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

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

553 -> H.Html -- ^ Resulting HTML

554createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

555

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

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

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

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

559 H.span ! class_ "name type"

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

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

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

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

388 iPrintResult ""

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

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

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

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

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

392-- RmProof and AddProof not supported!

391-- RmProof and AddProof not supported!

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

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

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

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

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

692 iputStrLn (show cg')

691 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"

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

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

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

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

701process h fn (CaseSplitAt updatefile l n)

694process h fn (CaseSplitAt updatefile l n)

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

1103 Left err -> iPrintError err

1096 Left err -> iPrintError err

1104

1097

1105

1098

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−

1131showTotal :: Totality -> IState -> String

1099showTotal :: Totality -> IState -> String

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

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

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

1101 = 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)

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

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

61 <|> 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))

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

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

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

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

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

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

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