58c3bb7 · Idris-dev · git.iko.soy

CHANGELOG.md+14

compare with master

unifiedsplit

@@ -1,3 +1,17 @@

1+# New in 0.99.1:

2+

3+## Language updates

4+

5+* New language extensions, in addition to the existing `TypeProviders` and

6+ `ErrorReflection`:

7+ + `ElabReflection`, which must be enabled to use `%runElab`

8+ + `UniquenessTypes`, which must be enabled to use `UniqueType`

9+ + `DSLNotation`, which must be enabled to define a `dsl` block

10+ + `FirstClassReflection`, which must be enabled to define a `%reflection`

11+ function

12+

13+

14+

1# New in 0.99:

15# New in 0.99:

2

16

3## Language updates

17## Language updates

libs/contrib/CFFI/Types.idr+3−1

@@ -126,13 +126,15 @@ offsetsPacked xs = offsets' xs [] 0

126 offsets' [] acc _ = reverse acc

127 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)

128

129+%language ElabReflection -- needed for 'error', which finds a line number

130+

129private

131private

130indexOrFail : Nat -> List a -> a

132indexOrFail : Nat -> List a -> a

131indexOrFail i xs = case index' i xs of

133indexOrFail i xs = case index' i xs of

132 Just x => x

134 Just x => x

133 Nothing => error "Out of bounds access"

135 Nothing => error "Out of bounds access"

134

136

135−||| The offset of a firld in a composite type

137+||| The offset of a field in a composite type

136export

138export

137offset : Composite -> Nat -> Int

139offset : Composite -> Nat -> Int

138offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

140offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)

libs/prelude/Builtins.idr+1

@@ -2,6 +2,7 @@

2

3%access public export

4%default total

5+%language UniquenessTypes

5

6

6||| The canonical single-element type, also known as the trivially

7||| The canonical single-element type, also known as the trivially

7||| true proposition.

8||| true proposition.

libs/prelude/Prelude.idr+2

@@ -37,6 +37,8 @@ import public Language.Reflection.Errors

37%access public export

38%default total

39

40+%language ElabReflection

41+

40-- Things that can't be elsewhere for import cycle reasons

42-- Things that can't be elsewhere for import cycle reasons

41-- See comment after declaration of void in Builtins.idr

43-- See comment after declaration of void in Builtins.idr

42-- for explanation of this definition's location

44-- for explanation of this definition's location

src/Idris/AbsSyntax.hs+4−8

@@ -142,14 +142,10 @@ addImported pub f

142 putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

143

144addLangExt :: LanguageExt -> Idris ()

145−addLangExt TypeProviders = do i <- getIState

146− putIState $ i {

147− idris_language_extensions = TypeProviders : idris_language_extensions i

148− }

149−addLangExt ErrorReflection = do i <- getIState

145+addLangExt e = do i <- getIState

150− putIState $ i {

146+ putIState $ i {

151− idris_language_extensions = ErrorReflection : idris_language_extensions i

147+ idris_language_extensions = e : idris_language_extensions i

152− }

148+ }

153

149

154-- | Transforms are organised by the function being applied on the lhs

150-- | Transforms are organised by the function being applied on the lhs

155-- of the transform, to make looking up appropriate transforms quicker

151-- of the transform, to make looking up appropriate transforms quicker

src/Idris/AbsSyntaxTree.hs+2−1

@@ -184,7 +184,8 @@ ppOption opt = PPOption {

184ppOptionIst :: IState -> PPOption

185ppOptionIst = ppOption . idris_options

186

187−data LanguageExt = TypeProviders | ErrorReflection

187+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

188+ | DSLNotation | ElabReflection | FCReflection

188 deriving (Show, Eq, Read, Ord, Generic)

189 deriving (Show, Eq, Read, Ord, Generic)

189

190

190-- | The output mode in use

191-- | The output mode in use

src/Idris/Elab/Clause.hs+2

@@ -75,6 +75,8 @@ elabClauses info' fc opts n_in cs =

75 -- Check n actually exists, with no definition yet

76 let tys = lookupTy n ctxt

77 let reflect = Reflection `elem` opts

78+ when (reflect && FCReflection `notElem` idris_language_extensions ist) $

79+ ierror $ At fc (Msg "You must turn on the FirstClassReflection extension to use %reflection")

78 checkUndefined n ctxt

80 checkUndefined n ctxt

79 unless (length tys > 1) $ do

81 unless (length tys > 1) $ do

80 fty <- case tys of

82 fty <- case tys of

src/Idris/Elab/Term.hs+8−3

@@ -295,7 +295,7 @@ elab ist info emode opts fn tm

295

296 -- | elabE elaborates an expression, possibly wrapping implicit coercions

297 -- and forces/delays. If you make a recursive call in elab', it is

298− -- normally correct to call elabE - the ones that don't are desugarings

298+ -- normally correct to call elabE - the ones that don't are `desugarings

299 -- typically

300 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()

301 elabE ina fc' t =

@@ -372,7 +372,10 @@ elab ist info emode opts fn tm

372 solve

373 highlightSource fc' (AnnType "Type" "The type of types")

374 elab' ina fc (PUniverse fc' u) =

375+ do unless (UniquenessTypes `elem` idris_language_extensions ist

376+ || e_qq ina) $

377+ lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")

375− do apply (RUType u) []

378+ apply (RUType u) []

376 solve

379 solve

377 highlightSource fc' (AnnType (show u) "The type of unique types")

380 highlightSource fc' (AnnType (show u) "The type of unique types")

378-- elab' (_,_,inty) (PConstant c)

381-- elab' (_,_,inty) (PConstant c)

@@ -1278,7 +1281,9 @@ elab ist info emode opts fn tm

1278 dotterm

1281 dotterm

1279 elab' ina fc t

1282 elab' ina fc t

1280 elab' ina fc (PRunElab fc' tm ns) =

1283 elab' ina fc (PRunElab fc' tm ns) =

1284+ do unless (ElabReflection `elem` idris_language_extensions ist) $

1285+ lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")

1281− do attack

1286+ attack

1282 n <- getNameFrom (sMN 0 "tacticScript")

1287 n <- getNameFrom (sMN 0 "tacticScript")

1283 let scriptTy = RApp (Var (sNS (sUN "Elab")

1288 let scriptTy = RApp (Var (sNS (sUN "Elab")

1284 ["Elab", "Reflection", "Language"]))

1289 ["Elab", "Reflection", "Language"]))

src/Idris/ElabDecls.hs+6−1

@@ -284,6 +284,8 @@ elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc cs

284-}

285elabDecl' _ info (PDSL n dsl)

286 = do i <- getIState

287+ unless (DSLNotation `elem` idris_language_extensions i) $

288+ ifail "You must turn on the DSLNotation extension to use a dsl block"

287 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

289 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

288 addIBC (IBCDSL n)

290 addIBC (IBCDSL n)

289elabDecl' what info (PDirective i)

291elabDecl' what info (PDirective i)

@@ -296,6 +298,9 @@ elabDecl' what info (PTransform fc safety old new)

296 = do elabTransform info fc safety old new

298 = do elabTransform info fc safety old new

297 return ()

299 return ()

298elabDecl' what info (PRunElabDecl fc script ns)

300elabDecl' what info (PRunElabDecl fc script ns)

301+ = do i <- getIState

302+ unless (ElabReflection `elem` idris_language_extensions i) $

303+ ierror $ At fc (Msg "You must turn on the ElabReflection extension to use %runElab")

299− = do elabRunElab info fc script ns

304+ elabRunElab info fc script ns

300 return ()

305 return ()

301elabDecl' _ _ _ = return () -- skipped this time

306elabDecl' _ _ _ = return () -- skipped this time

src/Idris/Parser.hs+4

@@ -1429,6 +1429,10 @@ directive syn = do try (lchar '%' *> reserved "lib")

1429pLangExt :: IdrisParser LanguageExt

1430pLangExt = (reserved "TypeProviders" >> return TypeProviders)

1431 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1432+ <|> (reserved "UniquenessTypes" >> return UniquenessTypes)

1433+ <|> (reserved "DSLNotation" >> return DSLNotation)

1434+ <|> (reserved "ElabReflection" >> return ElabReflection)

1435+ <|> (reserved "FirstClassReflection" >> return FCReflection)

1432

1436

1433{-| Parses a totality

1437{-| Parses a totality

1434

1438

test/dsl001/test001.idr+2

@@ -3,6 +3,8 @@ module Main

3import Data.Vect

4import Data.Fin

5

6+%language DSLNotation

7+

6data Ty = TyInt | TyBool| TyFun Ty Ty

8data Ty = TyInt | TyBool| TyFun Ty Ty

7

9

8interpTy : Ty -> Type

10interpTy : Ty -> Type

test/dsl002/Resimp.idr+1

@@ -3,6 +3,7 @@ module Resimp

3import public Data.Vect

4import public Data.Fin

5

6+%language DSLNotation

6%access public export

7%access public export

7

8

8-- IO operations which read a resource

9-- IO operations which read a resource

test/dsl003/DSLPi.idr+2

@@ -3,6 +3,8 @@ module DSLPi

3import Data.Fin

4import Data.Vect

5

6+%language DSLNotation

7+

6data Ty = BOOL | INT | UNIT | ARR Ty Ty

8data Ty = BOOL | INT | UNIT | ARR Ty Ty

7

9

8arr_ : _ -> Ty -> Ty -> Ty

10arr_ : _ -> Ty -> Ty -> Ty

test/dsl004/Door0.idr+3−1

@@ -1,6 +1,8 @@

1import IOu

2

3+%language UniquenessTypes

4+

3−data Result : (a : Type) -> (a -> Type) -> Type* where

5+data Result : (a : Type) -> (a -> Type) -> AnyType where

4 Res : {k : a -> Type} -> (val : a) -> k val -> Result a k

6 Res : {k : a -> Type} -> (val : a) -> k val -> Result a k

5

7

6

8

test/dsl004/Door1.idr+2

@@ -2,6 +2,8 @@ import IOu

2

3import Data.Vect

4

5+%language UniquenessTypes

6+

5data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where

7data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where

6 Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k

8 Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k

7

9

test/dsl004/Door2.idr+2

@@ -1,5 +1,7 @@

1import IOu

2

3+%language UniquenessTypes

4+

3data DoorState = OPEN | CLOSED

5data DoorState = OPEN | CLOSED

4

6

5data DoorH : DoorState -> UniqueType where

7data DoorH : DoorState -> UniqueType where

test/dsl004/Door3.idr+2

@@ -1,5 +1,7 @@

1import IOu

2

3+%language UniquenessTypes

4+

3data DoorState = OPEN | CLOSED

5data DoorState = OPEN | CLOSED

4

6

5data DoorH : DoorState -> UniqueType where

7data DoorH : DoorState -> UniqueType where

test/dsl004/IOu.idr+2

@@ -1,5 +1,7 @@

1module IOu

2

3+%language UniquenessTypes

4+

3-------- An IO type supporting possibly unique values

5-------- An IO type supporting possibly unique values

4

6

5data IOu : AnyType -> AnyType where

7data IOu : AnyType -> AnyType where

test/meta001/Finite.idr+2

@@ -4,6 +4,8 @@ import Data.Fin

4import Language.Reflection.Elab

5import Language.Reflection.Utils

6

7+%language ElabReflection

8+

7-- Test various features of reflected elaboration, including looking

9-- Test various features of reflected elaboration, including looking

8-- up datatypes, defining functions, and totality checking

10-- up datatypes, defining functions, and totality checking

9

11

test/meta002/AgdaStyleReflection.idr+1−1

@@ -13,7 +13,7 @@ import Language.Reflection.Utils

13import Pruviloj

14

15%default total

16−

16+%language ElabReflection

17

18

19||| Function arguments as provided at the application site

test/meta002/DataDef.idr+2

@@ -1,5 +1,7 @@

1module DataDef

2

3+%language ElabReflection

4+

3foo : Elab ()

5foo : Elab ()

4foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)

6foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)

5 defineDatatype $ DefineDatatype `{{DataDef.N}} [

7 defineDatatype $ DefineDatatype `{{DataDef.N}} [

test/meta002/Deriving.idr+2

@@ -1,6 +1,8 @@

1||| Test some deriving features

2module Deriving

3

4+%language ElabReflection

5+

4-- NB: test disabled due to excess memory consumption

6-- NB: test disabled due to excess memory consumption

5

7

6import Pruviloj

8import Pruviloj

test/meta002/Tacs.idr+1

@@ -16,6 +16,7 @@ import Language.Reflection.Utils

16import Pruviloj.Core

17

18%default total

19+%language ElabReflection

19

20

20-- Tactics can now query the elaborator and bind variables

21-- Tactics can now query the elaborator and bind variables

21

22

test/meta002/expected+2−2

@@ -1,7 +1,7 @@

1−DataDef.idr:72:1-9:

1+DataDef.idr:74:1-9:

2While running an elaboration script, the following error occurred:

3Prelude.Either.Either is already defined as a datatype.

4−Tacs.idr:298:15:

4+Tacs.idr:299:15:

5When checking right hand side of testElab3 with expected type

6 DPair Ty (Tm [])

7

test/meta003/BadDef.idr+2

@@ -2,6 +2,8 @@ module BadDef

2

3import Language.Reflection.Elab

4

5+%language ElabReflection

6+

5mkN : String -> TTName

7mkN : String -> TTName

6mkN n = NS (UN n) ["BadDef"]

8mkN n = NS (UN n) ["BadDef"]

7

9

test/meta003/expected+1−1

@@ -1,4 +1,4 @@

1−BadDef.idr:12:1-9:

1+BadDef.idr:14:1-9:

2While running an elaboration script, the following error occurred:

3Type mismatch between

4 ()

test/meta004/expected+1−1

@@ -1,3 +1,3 @@

1−meta004.idr:48:1-9:

1+meta004.idr:50:1-9:

2While running an elaboration script, the following error occurred:

3Not an impossible case

test/meta004/meta004.idr+2

@@ -2,6 +2,8 @@ import Data.Fin

2import Language.Reflection.Utils

3import Pruviloj.Core

4

5+%language ElabReflection

6+

5rename : TTName -> TTName -> Raw -> Raw

7rename : TTName -> TTName -> Raw -> Raw

6rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)

8rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)

7rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)

9rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)

test/proof002/Reflect.idr+1

@@ -4,6 +4,7 @@ import Decidable.Equality

4

5%access public export

6%default total

7+%language FirstClassReflection

7

8

8using (xs : List a, ys : List a, G : List (List a))

9using (xs : List a, ys : List a, G : List (List a))

9

10

test/proof002/expected+3−3

@@ -1,8 +1,8 @@

1−Reflect.idr:174:21-26:

1+Reflect.idr:175:21-26:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−Reflect.idr:183:21-26:

3+Reflect.idr:184:21-26:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5−Reflect.idr:191:15-20:

5+Reflect.idr:192:15-20:

6This style of tactic proof is deprecated. See %runElab for the replacement.

7test030a.idr:12:26-14:1:

8When checking right hand side of testReflect1 with expected type

test/pruviloj001/pruviloj001.idr+1

@@ -5,6 +5,7 @@ import Pruviloj

5import Pruviloj.Induction

6

7%default total

8+%language ElabReflection

8

9

9||| Try some simplification and rewriting heuristics, then attempt to

10||| Try some simplification and rewriting heuristics, then attempt to

10||| solve the goal

11||| solve the goal

test/sourceLocation001/SourceLoc.idr+1

@@ -6,6 +6,7 @@ import Language.Reflection

6import Language.Reflection.Utils

7

8%default total

9+%language DSLNotation

9

10

10||| A "function" that returns where it is called in the source

11||| A "function" that returns where it is called in the source

11getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

12getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

test/sourceLocation001/expected+8−8

@@ -1,19 +1,19 @@

1−SourceLoc.idr:11:19-26:

1+SourceLoc.idr:12:19-26:

2This style of tactic proof is deprecated. See %runElab for the replacement.

3−SourceLoc.idr:20:19-24:

3+SourceLoc.idr:21:19-24:

4This style of tactic proof is deprecated. See %runElab for the replacement.

5−SourceLoc.idr:40:20-27:

5+SourceLoc.idr:41:20-27:

6This style of tactic proof is deprecated. See %runElab for the replacement.

7−SourceLoc.idr:98:18-23:

7+SourceLoc.idr:99:18-23:

8This style of tactic proof is deprecated. See %runElab for the replacement.

9Testing using definition

10−FileLoc "SourceLoc.idr" (16, 11) (16, 17)

10+FileLoc "SourceLoc.idr" (17, 11) (17, 17)

11Testing using inline tactics

12−FileLoc "SourceLoc.idr" (20, 17) (20, 17)

12+FileLoc "SourceLoc.idr" (21, 17) (21, 17)

13Testing using metavariable with later definition

14−FileLoc "SourceLoc.idr" (98, 16) (98, 16)

14+FileLoc "SourceLoc.idr" (99, 16) (99, 16)

15-----------------------

16Success!

17−Error at FileLoc "SourceLoc.idr" (72, 23) (72, 26)

17+Error at FileLoc "SourceLoc.idr" (73, 23) (73, 26)

18Success!

19Success!

test/tactics001/Tactics.idr+1−1

@@ -4,7 +4,7 @@ import Language.Reflection.Elab

4

5import Data.Vect

6

7−

7+%language ElabReflection

8%default total

9

10-- Test that basic proofs with new-style tactics work

test/unique001/unique001.idr+2

@@ -1,5 +1,7 @@

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/expected+10−10

@@ -1,26 +1,26 @@

1−unique001a.idr:33:11:Type mismatch between

1+unique001a.idr:35:11:Type mismatch between

2 Int -> String

3and

4 UniqueType (Int -> String)

5−unique001a.idr:44:12:Type mismatch between

5+unique001a.idr:46:12:Type mismatch between

6 Int -> String

7and

8 UniqueType (Int -> String)

9−unique001a.idr:55:12:Type mismatch between

9+unique001a.idr:57:12:Type mismatch between

10 UniqueType (Int -> String)

11and

12 Int -> String

13−unique001b.idr:16:7:Borrowed name xs must not be used on RHS

13+unique001b.idr:18:7:Borrowed name xs must not be used on RHS

14−unique001c.idr:46:6:Unique name f is used more than once

14+unique001c.idr:47:6:Unique name f is used more than once

15−unique001d.idr:3:7:Borrowed name x must not be used on RHS

15+unique001d.idr:4:7:Borrowed name x must not be used on RHS

16−unique001e.idr:3:10:

16+unique001e.idr:4:10:

17Constructor Main.Nil has a UniqueType, but the data type does not

18−unique002.idr:15:5:Unique name xs is used more than once

18+unique002.idr:17:5:Unique name xs is used more than once

19−unique002a.idr:15:5:Type mismatch between

19+unique002a.idr:17:5:Type mismatch between

20 Int -> String

21and

22 UniqueType (Int -> String)

23−unique003.idr:18:5:Type mismatch between

23+unique003.idr:20:5:Type mismatch between

24 Int -> String

25and

26 UniqueType (Int -> String)

test/unique004/unique001a.idr+2

@@ -1,5 +1,7 @@

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/unique001b.idr+2

@@ -1,5 +1,7 @@

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a

test/unique004/unique001c.idr+1

@@ -1,3 +1,4 @@

1+%language UniquenessTypes

1

2

2data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

3 UNil : UList a

4 UNil : UList a

test/unique004/unique001d.idr+1

@@ -1,3 +1,4 @@

1+%language UniquenessTypes

1

2

2steal : {a : UniqueType} -> Borrowed a -> a

3steal : {a : UniqueType} -> Borrowed a -> a

3steal (Read x) = x

4steal (Read x) = x

test/unique004/unique001e.idr+1

@@ -1,3 +1,4 @@

1+%language UniquenessTypes

1

2

2data BadList : UniqueType -> Type where

3data BadList : UniqueType -> Type where

3 Nil : {a : UniqueType} -> BadList a

4 Nil : {a : UniqueType} -> BadList a

test/unique004/unique002.idr+2

@@ -1,3 +1,5 @@

1+%language UniquenessTypes

2+

1data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

2 Nil : UList a

4 Nil : UList a

3 (::) : a -> UList a -> UList a

5 (::) : a -> UList a -> UList a

test/unique004/unique002a.idr+2

@@ -1,3 +1,5 @@

1+%language UniquenessTypes

2+

1data UList : Type -> UniqueType where

3data UList : Type -> UniqueType where

2 Nil : UList a

4 Nil : UList a

3 (::) : a -> UList a -> UList a

5 (::) : a -> UList a -> UList a

test/unique004/unique003.idr+2

@@ -1,5 +1,7 @@

1module Main

2

3+%language UniquenessTypes

4+

3data UList : Type -> UniqueType where

5data UList : Type -> UniqueType where

4 Nil : UList a

6 Nil : UList a

5 (::) : a -> UList a -> UList a

7 (::) : a -> UList a -> UList a