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

git.iko.soy/Idris-dev

Hide more features behind %language pragmas

These are the features which should not be considered stable: ElabReflection, DSLNotation, UniquenessTypes and FirstClassReflection, in addition to the existing TypeProviders and ErrorReflection

commit58c3bb760a8930a48848d82ad42c0bffa795dc44 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 7 Dec 2016, 19:38 (10 years ago) parentd89f3fa

44 files changed+118−42

compare with master

unifiedsplit

CHANGELOG.md+14 libs/contrib/CFFI/Types.idr+3−1 libs/prelude/Builtins.idr+1 libs/prelude/Prelude.idr+2 src/Idris/AbsSyntax.hs+4−8 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Elab/Clause.hs+2 src/Idris/Elab/Term.hs+8−3 src/Idris/ElabDecls.hs+6−1 src/Idris/Parser.hs+4 test/dsl001/test001.idr+2 test/dsl002/Resimp.idr+1 test/dsl003/DSLPi.idr+2 test/dsl004/Door0.idr+3−1 test/dsl004/Door1.idr+2 test/dsl004/Door2.idr+2 test/dsl004/Door3.idr+2 test/dsl004/IOu.idr+2 test/meta001/Finite.idr+2 test/meta002/AgdaStyleReflection.idr+1−1 test/meta002/DataDef.idr+2 test/meta002/Deriving.idr+2 test/meta002/Tacs.idr+1 test/meta002/expected+2−2 test/meta003/BadDef.idr+2 test/meta003/expected+1−1 test/meta004/expected+1−1 test/meta004/meta004.idr+2 test/proof002/Reflect.idr+1 test/proof002/expected+3−3 test/pruviloj001/pruviloj001.idr+1 test/sourceLocation001/SourceLoc.idr+1 test/sourceLocation001/expected+8−8 test/tactics001/Tactics.idr+1−1 test/unique001/unique001.idr+2 test/unique004/expected+10−10 test/unique004/unique001a.idr+2 test/unique004/unique001b.idr+2 test/unique004/unique001c.idr+1 test/unique004/unique001d.idr+1 test/unique004/unique001e.idr+1 test/unique004/unique002.idr+2 test/unique004/unique002a.idr+2 test/unique004/unique003.idr+2

CHANGELOG.md+14

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

1+# New in 0.99.1:

3+## Language updates

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+

115# New in 0.99:

216

317## Language updates

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

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

126126 offsets' [] acc _ = reverse acc

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

128128

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

130+

129131private

130132indexOrFail : Nat -> List a -> a

131133indexOrFail i xs = case index' i xs of

132134 Just x => x

133135 Nothing => error "Out of bounds access"

134136

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

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

136138export

137139offset : Composite -> Nat -> Int

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

libs/prelude/Builtins.idr+1

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

33%access public export

44%default total

5+%language UniquenessTypes

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

78||| true proposition.

libs/prelude/Prelude.idr+2

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

3737%access public export

3838%default total

3939

40+%language ElabReflection

41+

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

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

4244-- for explanation of this definition's location

src/Idris/AbsSyntax.hs+4−8

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

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

143143

144144addLangExt :: 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

150− putIState $ i {

151− idris_language_extensions = ErrorReflection : idris_language_extensions i

152− }

145+addLangExt e = do i <- getIState

146+ putIState $ i {

147+ idris_language_extensions = e : idris_language_extensions i

148+ }

153149

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

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

src/Idris/AbsSyntaxTree.hs+2−1

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

184184ppOptionIst :: IState -> PPOption

185185ppOptionIst = ppOption . idris_options

186186

187−data LanguageExt = TypeProviders | ErrorReflection

187+data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes

188+ | DSLNotation | ElabReflection | FCReflection

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

189190

190191-- | The output mode in use

src/Idris/Elab/Clause.hs+2

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

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

7676 let tys = lookupTy n ctxt

7777 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")

7880 checkUndefined n ctxt

7981 unless (length tys > 1) $ do

8082 fty <- case tys of

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

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

295295

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

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

299299 -- typically

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

301301 elabE ina fc' t =

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

372372 solve

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

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

375− do apply (RUType 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")

378+ apply (RUType u) []

376379 solve

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

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

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

12781281 dotterm

12791282 elab' ina fc t

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

1281− do attack

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

1286+ attack

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

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

12841289 ["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

284284-}

285285elabDecl' _ info (PDSL n dsl)

286286 = 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"

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

288290 addIBC (IBCDSL n)

289291elabDecl' what info (PDirective i)

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

296298 = do elabTransform info fc safety old new

297299 return ()

298300elabDecl' what info (PRunElabDecl fc script ns)

299− = do elabRunElab info 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")

304+ elabRunElab info fc script ns

300305 return ()

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

src/Idris/Parser.hs+4

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

14291429pLangExt :: IdrisParser LanguageExt

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

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

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

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

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

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

14321436

14331437{-| Parses a totality

14341438

test/dsl001/test001.idr+2

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

33import Data.Vect

44import Data.Fin

6+%language DSLNotation

68data Ty = TyInt | TyBool| TyFun Ty Ty

810interpTy : Ty -> Type

test/dsl002/Resimp.idr+1

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

33import public Data.Vect

44import public Data.Fin

6+%language DSLNotation

67%access public export

89-- IO operations which read a resource

test/dsl003/DSLPi.idr+2

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

33import Data.Fin

44import Data.Vect

6+%language DSLNotation

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

810arr_ : _ -> Ty -> Ty -> Ty

test/dsl004/Door0.idr+3−1

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

11import IOu

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

3+%language UniquenessTypes

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

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

test/dsl004/Door1.idr+2

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

33import Data.Vect

5+%language UniquenessTypes

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

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

test/dsl004/Door2.idr+2

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

11import IOu

3+%language UniquenessTypes

35data DoorState = OPEN | CLOSED

57data DoorH : DoorState -> UniqueType where

test/dsl004/Door3.idr+2

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

11import IOu

3+%language UniquenessTypes

35data DoorState = OPEN | CLOSED

57data DoorH : DoorState -> UniqueType where

test/dsl004/IOu.idr+2

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

11module IOu

3+%language UniquenessTypes

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

57data IOu : AnyType -> AnyType where

test/meta001/Finite.idr+2

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

44import Language.Reflection.Elab

55import Language.Reflection.Utils

7+%language ElabReflection

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

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

911

test/meta002/AgdaStyleReflection.idr+1−1

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

1313import Pruviloj

1414

1515%default total

16−

16+%language ElabReflection

1717

1818

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

test/meta002/DataDef.idr+2

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

11module DataDef

3+%language ElabReflection

35foo : Elab ()

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

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

test/meta002/Deriving.idr+2

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

11||| Test some deriving features

22module Deriving

4+%language ElabReflection

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

68import Pruviloj

test/meta002/Tacs.idr+1

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

1616import Pruviloj.Core

1717

1818%default total

19+%language ElabReflection

1920

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

2122

test/meta002/expected+2−2

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

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

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

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

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

4−Tacs.idr:298:15:

4+Tacs.idr:299:15:

55When checking right hand side of testElab3 with expected type

66 DPair Ty (Tm [])

test/meta003/BadDef.idr+2

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

33import Language.Reflection.Elab

5+%language ElabReflection

57mkN : String -> TTName

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

test/meta003/expected+1−1

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

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

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

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

33Type mismatch between

44 ()

test/meta004/expected+1−1

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

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

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

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

33Not an impossible case

test/meta004/meta004.idr+2

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

22import Language.Reflection.Utils

33import Pruviloj.Core

5+%language ElabReflection

57rename : TTName -> TTName -> Raw -> Raw

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

79rename 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

55%access public export

66%default total

7+%language FirstClassReflection

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

910

test/proof002/expected+3−3

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

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

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

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

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

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

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

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

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

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

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

88When checking right hand side of testReflect1 with expected type

test/pruviloj001/pruviloj001.idr+1

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

55import Pruviloj.Induction

77%default total

8+%language ElabReflection

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

1011||| solve the goal

test/sourceLocation001/SourceLoc.idr+1

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

66import Language.Reflection.Utils

88%default total

9+%language DSLNotation

910

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

1112getLoc : {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:

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

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

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

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

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

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

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

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

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

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

99Testing using definition

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

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

1111Testing using inline tactics

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

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

1313Testing using metavariable with later definition

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

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

1515-----------------------

1616Success!

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

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

1818Success!

1919Success!

test/tactics001/Tactics.idr+1−1

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

55import Data.Vect

7−

7+%language ElabReflection

88%default total

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

test/unique001/unique001.idr+2

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

11module Main

3+%language UniquenessTypes

35data UList : Type -> UniqueType where

46 Nil : UList a

57 (::) : 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

22 Int -> String

33and

44 UniqueType (Int -> String)

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

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

66 Int -> String

77and

88 UniqueType (Int -> String)

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

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

1010 UniqueType (Int -> String)

1111and

1212 Int -> String

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

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

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

16−unique001e.idr:3:10:

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

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

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

16+unique001e.idr:4:10:

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

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

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

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

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

2020 Int -> String

2121and

2222 UniqueType (Int -> String)

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

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

2424 Int -> String

2525and

2626 UniqueType (Int -> String)

test/unique004/unique001a.idr+2

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

11module Main

3+%language UniquenessTypes

35data UList : Type -> UniqueType where

46 Nil : UList a

57 (::) : a -> UList a -> UList a

test/unique004/unique001b.idr+2

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

11module Main

3+%language UniquenessTypes

35data UList : Type -> UniqueType where

46 Nil : UList a

57 (::) : a -> UList a -> UList a

test/unique004/unique001c.idr+1

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

1+%language UniquenessTypes

23data UList : Type -> UniqueType where

34 UNil : UList a

test/unique004/unique001d.idr+1

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

1+%language UniquenessTypes

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

34steal (Read x) = x

test/unique004/unique001e.idr+1

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

1+%language UniquenessTypes

23data BadList : UniqueType -> Type where

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

test/unique004/unique002.idr+2

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

1+%language UniquenessTypes

13data UList : Type -> UniqueType where

24 Nil : UList a

35 (::) : a -> UList a -> UList a

test/unique004/unique002a.idr+2

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

1+%language UniquenessTypes

13data UList : Type -> UniqueType where

24 Nil : UList a

35 (::) : a -> UList a -> UList a

test/unique004/unique003.idr+2

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

11module Main

3+%language UniquenessTypes

35data UList : Type -> UniqueType where

46 Nil : UList a

57 (::) : a -> UList a -> UList a