eba5123 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

Conflicts: CHANGELOG

commiteba512390d7c4cd8f89ca908198c60a388c6e9e7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 29 Jan 2016, 21:12 (11 years ago) parente3e35a5 c4c7802

12 files changed+31−31

compare with master

unifiedsplit

CHANGELOG+3 docs/conf.py+4−4 docs/reference/language-features.rst+1−1 idris-tutorial.pdf samples/tutorial/interp.idr+1−1 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/ParseData.hs+1−5 src/Idris/ParseExpr.hs+6−6 src/Idris/ParseHelpers.hs+9−1 src/Idris/Parser.hs+2−9 test/dsl001/test001.idr+1−1 test/dsl002/Resimp.idr+1−1

CHANGELOG+3

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

1414 directive as before.

1515* Exported types can only refer to other exported names

1616* 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+

1720

1821New in 0.10:

1922============

docs/conf.py+4−4

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

5959# built documents.

6060#

6161# The short X.Y version.

62−version = '0.9.19'

62+version = '0.10.1'

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

64−release = '0.9.19.1'

64+release = '0.10.1'

6565

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

6767# for a list of supported languages.

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

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

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

236236latex_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'),

239237 ('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'),

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

241241 ]

242242

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

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

4646 using the ``UniqueType`` universe.

4747- `Partial

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

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

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

5050- Error message reflection

5151- Eliminators

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

3333 Expr G c

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

3535

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

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

3737 interp env (Var i) = lookup i env

3838 interp env (Val x) = x

3939 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

17401740

17411741 st =

17421742 case s of

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

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

17441744 _ -> empty

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

17461746 | ppopt_impl ppo =

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

17511751 where

17521752 st =

17531753 case s of

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

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

17551755 _ -> empty

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

17571757 depth d . bracket p startPrec $

src/Idris/ParseData.hs+1−5

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

167167 <|> return opts

168168 <?> "data options"

169169 where warnElim fc =

170− do ist <- get

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 }

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

175171

176172{- | Parses a data type declaration

177173Data ::= 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 })

333333

334334warnTacticDeprecation :: FC -> IdrisParser ()

335335warnTacticDeprecation 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.")

341337

342338{- | Parses a proof block

343339@

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

13891385@

13901386-}

13911387static :: 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

13931393 <|> return Dynamic

13941394 <?> "static modifier"

13951395

src/Idris/ParseHelpers.hs+9−1

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

77import Prelude hiding (pi)

99import 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)

1111import Text.Parser.LookAhead

1212import Text.Parser.Expression

1313import qualified Text.Parser.Token as Tok

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

105105 parserWarnings ist)

106106 clearParserWarnings

107107

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+

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

109117

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

878878 classKeyword = reservedHL "interface"

879879 <|> do reservedHL "class"

880880 fc <- getFC

881− ist <- get

882− put ist { parserWarnings =

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

884− : parserWarnings ist }

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

885882

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

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

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

929926 instanceKeyword = reservedHL "implementation"

930927 <|> do reservedHL "instance"

931928 fc <- getFC

932− ist <- get

933− put ist { parserWarnings =

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

935− : parserWarnings ist }

936−

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

937930

938931-- | Parse a docstring

939932docstring :: SyntaxInfo

test/dsl001/test001.idr+1−1

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

4545 index_next = Pop

4646

4747 total

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

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

4949 interp env (Var i) = lookup i env

5050 interp env (Val x) = x

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

124124 ioret : a -> IO a

125125 ioret = return

126126

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

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

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

129129

130130 interp env (Let val scope) k