eba5123 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -14,6 +14,9 @@ Updated export rules

14 directive as before.

15* Exported types can only refer to other exported names

16* Publicly exported definitions can only refer to publicly exported names

17+* The '[static]' annotation is changed to '%static' to be consistent with the

18+other annotations.

19+

17

20

18New in 0.10:

21New in 0.10:

19============

22============

docs/conf.py+4−4

@@ -59,9 +59,9 @@ author = u'The Idris Community'

59# built documents.

60#

61# The short X.Y version.

62−version = '0.9.19'

62+version = '0.10.1'

63# The full version, including alpha/beta/rc tags.

64−release = '0.9.19.1'

64+release = '0.10.1'

65

66# The language for content autogenerated by Sphinx. Refer to documentation

67# for a list of supported languages.

@@ -234,9 +234,9 @@ latex_elements = {

234# (source start file, target name, title,

235# author, documentclass [howto, manual, or own class]).

236latex_documents = [

237− ('guides/index', 'idris-guides.tex', u'Idris Tutorial Series', u'The Idris Community', 'manual'),

238− ('reference/index', 'idris-reference.tex', u'The Idris Reference', u'The Idris Community', 'manual'),

239 ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'manual'),

237 ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'manual'),

238+ ('guides/index', 'idris-guides.tex', u'Idris Tutorial Series', u'The Idris Community', 'manual'),

239+# ('reference/index', 'idris-reference.tex', u'The Idris Reference', u'The Idris Community', 'manual'),

240 ('effects/index', 'eff-tutorial.tex', u'The Effects Tutorial', u'The Idris Community', 'manual')

241 ]

242

docs/reference/language-features.rst+1−1

@@ -46,7 +46,7 @@ Core Language Features

46 using the ``UniqueType`` universe.

47- `Partial

48 evaluation <https://github.com/idris-lang/Idris-dev/wiki/Static-Arguments-and-Partial-Evaluation>`__

49− by ``[static]`` argument annotations.

49+ by ``%static`` argument annotations.

50- Error message reflection

51- Eliminators

52- Label types ``'name``

idris-tutorial.pdf

Binary file not shown.

samples/tutorial/interp.idr+1−1

@@ -33,7 +33,7 @@ using (G : Vect n Ty)

33 Expr G c

34 If : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

35

36− interp : Env G -> [static] (e : Expr G t) -> interpTy t

36+ interp : Env G -> %static (e : Expr G t) -> interpTy t

37 interp env (Var i) = lookup i env

38 interp env (Val x) = x

39 interp env (Lam sc) = \x => interp (x :: env) sc

src/Idris/AbsSyntaxTree.hs+2−2

@@ -1740,7 +1740,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1740

1741 st =

1742 case s of

1743− Static -> text "[static]" <> space

1743+ Static -> text "%static" <> space

1744 _ -> empty

1745 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)

1746 | ppopt_impl ppo =

@@ -1751,7 +1751,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1751 where

1752 st =

1753 case s of

1754− Static -> text "[static]" <> space

1754+ Static -> text "%static" <> space

1755 _ -> empty

1756 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =

1757 depth d . bracket p startPrec $

src/Idris/ParseData.hs+1−5

@@ -167,11 +167,7 @@ dataOpts opts

167 <|> return opts

168 <?> "data options"

169 where warnElim fc =

170− do ist <- get

170+ parserWarning fc (Just NoElimDeprecationWarnings) (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

171− let cmdline = opt_cmdline (idris_options ist)

172− unless (NoElimDeprecationWarnings `elem` cmdline) $

173− put ist { parserWarnings =

174− (fc, Msg "Eliminator generation is deprecated. Use an eliminator generator in a library instead.") : parserWarnings ist }

175

171

176{- | Parses a data type declaration

172{- | Parses a data type declaration

177Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

173Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

src/Idris/ParseExpr.hs+6−6

@@ -333,11 +333,7 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })

333

334warnTacticDeprecation :: FC -> IdrisParser ()

335warnTacticDeprecation fc =

336− do ist <- get

337− let cmdline = opt_cmdline (idris_options ist)

338− unless (NoOldTacticDeprecationWarnings `elem` cmdline) $

339− put ist { parserWarnings =

340− (fc, Msg "This style of tactic proof is deprecated. See %runElab for the replacement.") : parserWarnings ist }

336+ parserWarning fc (Just NoOldTacticDeprecationWarnings) (Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")

341

337

342{- | Parses a proof block

338{- | Parses a proof block

343@

339@

@@ -1389,7 +1385,11 @@ Static ::=

1389@

1385@

1390-}

1386-}

1391static :: IdrisParser Static

1387static :: IdrisParser Static

1392−static = do reserved "[static]"; return Static

1388+static = do reserved "%static"; return Static

1389+ <|> do reserved "[static]"

1390+ fc <- getFC

1391+ parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")

1392+ return Static

1393 <|> return Dynamic

1394 <?> "static modifier"

1395

src/Idris/ParseHelpers.hs+9−1

@@ -7,7 +7,7 @@ module Idris.ParseHelpers where

7import Prelude hiding (pi)

8

9import Text.Trifecta.Delta

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

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

11import Text.Parser.LookAhead

12import Text.Parser.Expression

13import qualified Text.Parser.Token as Tok

@@ -105,6 +105,14 @@ reportParserWarnings = do ist <- getIState

105 parserWarnings ist)

106 clearParserWarnings

107

108+

109+parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()

110+parserWarning fc warnOpt warnErr = do

111+ ist <- get

112+ let cmdline = opt_cmdline (idris_options ist)

113+ unless (maybe False (`elem` cmdline) warnOpt) $

114+ put ist { parserWarnings = (fc, warnErr) : parserWarnings ist }

115+

108{- * Space, comments and literals (token/lexing like parsers) -}

116{- * Space, comments and literals (token/lexing like parsers) -}

109

117

110-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

118-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

src/Idris/Parser.hs+2−9

@@ -878,10 +878,7 @@ class_ syn = do (doc, argDocs, acc)

878 classKeyword = reservedHL "interface"

879 <|> do reservedHL "class"

880 fc <- getFC

881− ist <- get

882− put ist { parserWarnings =

883− (fc, Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

881+ parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

884− : parserWarnings ist }

885

882

886 carg :: IdrisParser (Name, FC, PTerm)

883 carg :: IdrisParser (Name, FC, PTerm)

887 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'

884 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'

@@ -929,11 +926,7 @@ instance_ kwopt syn

929 instanceKeyword = reservedHL "implementation"

926 instanceKeyword = reservedHL "implementation"

930 <|> do reservedHL "instance"

927 <|> do reservedHL "instance"

931 fc <- getFC

928 fc <- getFC

932− ist <- get

933− put ist { parserWarnings =

934− (fc, Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

929+ parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

935− : parserWarnings ist }

936−

937

930

938-- | Parse a docstring

931-- | Parse a docstring

939docstring :: SyntaxInfo

932docstring :: SyntaxInfo

test/dsl001/test001.idr+1−1

@@ -45,7 +45,7 @@ using (G : Vect n Ty)

45 index_next = Pop

46

47 total

48− interp : Env G -> [static] (e : Expr G t) -> interpTy t

48+ interp : Env G -> %static (e : Expr G t) -> interpTy t

49 interp env (Var i) = lookup i env

50 interp env (Val x) = x

51 interp env (Lam sc) = \x => interp (x :: env) sc

test/dsl002/Resimp.idr+1−1

@@ -124,7 +124,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

124 ioret : a -> IO a

125 ioret = return

126

127− interp : Env gam -> [static] (e : Res gam gam' t) ->

127+ interp : Env gam -> %static (e : Res gam gam' t) ->

128 (Env gam' -> interpTy t -> IO u) -> IO u

129

130 interp env (Let val scope) k