9993f3b · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -3,6 +3,8 @@ New in 0.9.14:

3* Support for running tests for a package with the tests section of .ipkg files and the

4 --testpkg command-line option

5* Clearly distinguish between type providers and postulate providers at the use site

6+* Allow dependent function syntax to be overridden in dsl blocks, similarly to

7+ functions and let. The keyword for this is "pi".

6

8

7New in 0.9.13:

9New in 0.9.13:

8--------------

10--------------

idris.cabal+3

@@ -289,6 +289,9 @@ Extra-source-files:

289 test/dsl002/test

290 test/dsl002/*.idr

291 test/dsl002/expected

292+ test/dsl003/run

293+ test/dsl003/*.idr

294+ test/dsl003/expected

292

295

293 test/effects001/run

296 test/effects001/run

294 test/effects001/*.idr

297 test/effects001/*.idr

src/Idris/AbsSyntaxTree.hs+3−1

@@ -904,7 +904,8 @@ data DSL' t = DSL { dsl_bind :: t,

904 index_first :: Maybe t,

905 index_next :: Maybe t,

906 dsl_lambda :: Maybe t,

907− dsl_let :: Maybe t

907+ dsl_let :: Maybe t,

908+ dsl_pi :: Maybe t

908 }

909 }

909 deriving (Show, Functor)

910 deriving (Show, Functor)

910{-!

911{-!

@@ -948,6 +949,7 @@ initDSL = DSL (PRef f (sUN ">>="))

948 Nothing

949 Nothing

950 Nothing

951 Nothing

952+ Nothing

951 where f = fileFC "(builtin)"

953 where f = fileFC "(builtin)"

952

954

953data Using = UImplicit Name PTerm

955data Using = UImplicit Name PTerm

src/Idris/DSL.hs+8−1

@@ -29,6 +29,10 @@ expandDo dsl (PLet n ty v tm)

29 = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

30 expandDo dsl sc

31expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

32+expandDo dsl (PPi p n ty tm)

33+ | Just pi <- dsl_pi dsl

34+ = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in

35+ expandDo dsl sc

32expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

36expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

33expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

37expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

34 (map (fmap (expandDo dsl)) args)

38 (map (fmap (expandDo dsl)) args)

@@ -88,7 +92,10 @@ var dsl n t i = v' i t where

88 | Nothing <- dsl_let dsl

92 | Nothing <- dsl_let dsl

89 = PLet n (v' i ty) (v' i val) (v' i sc)

93 = PLet n (v' i ty) (v' i val) (v' i sc)

90 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)

94 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)

95+ v' i (PPi p n ty sc)

96+ | Nothing <- dsl_pi dsl

91− v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc)

97+ = PPi p n (v' i ty) (v' i sc)

98+ | otherwise = PPi p n (v' i ty) (v' (i+1) sc)

92 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

99 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

93 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

94 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

src/Idris/DeepSeq.hs+3−2

@@ -291,12 +291,13 @@ instance NFData TypeInfo where

291 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

292

293instance (NFData t) => NFData (DSL' t) where

294− rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

294+ rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

295 = rnf x1 `seq`

296 rnf x2 `seq`

297 rnf x3 `seq`

298 rnf x4 `seq`

299+ rnf x5 `seq`

299− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

300+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

300

301

301instance NFData SynContext where

302instance NFData SynContext where

302 rnf PatternSyntax = ()

303 rnf PatternSyntax = ()

src/Idris/IBC.hs+4−2

@@ -2191,7 +2191,7 @@ instance Binary Syntax where

2191 return (Rule x1 x2 x3)

2192

2193instance (Binary t) => Binary (DSL' t) where

2194− put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2194+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2195 = do put x1

2196 put x2

2197 put x3

@@ -2201,6 +2201,7 @@ instance (Binary t) => Binary (DSL' t) where

2201 put x7

2202 put x8

2203 put x9

2204+ put x10

2204 get

2205 get

2205 = do x1 <- get

2206 = do x1 <- get

2206 x2 <- get

2207 x2 <- get

@@ -2211,7 +2212,8 @@ instance (Binary t) => Binary (DSL' t) where

2211 x7 <- get

2212 x7 <- get

2212 x8 <- get

2213 x8 <- get

2213 x9 <- get

2214 x9 <- get

2215+ x10 <- get

2214− return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)

2216+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

2215

2217

2216instance Binary SSymbol where

2218instance Binary SSymbol where

2217 put x

2219 put x

src/Idris/ParseData.hs+5−3

@@ -209,12 +209,14 @@ dsl syn = do reserved "dsl"

209 first = lookup "index_first" bs

210 next = lookup "index_next" bs

211 leto = lookup "let" bs

212− lambda = lookup "lambda" bs in

212+ lambda = lookup "lambda" bs

213+ pi = lookup "pi" bs in

213 initDSL { dsl_var = var,

214 initDSL { dsl_var = var,

214 index_first = first,

215 index_first = first,

215 index_next = next,

216 index_next = next,

216 dsl_lambda = lambda,

217 dsl_lambda = lambda,

217− dsl_let = leto }

218+ dsl_let = leto,

219+ dsl_pi = pi }

218

220

219{- | Checks DSL for errors -}

221{- | Checks DSL for errors -}

220-- FIXME: currently does nothing, check if DSL is really sane

222-- FIXME: currently does nothing, check if DSL is really sane

@@ -235,6 +237,6 @@ overload syn = do o <- identifier <|> do reserved "let"

235 t <- expr syn

237 t <- expr syn

236 return (o, t)

238 return (o, t)

237 <?> "dsl overload declaratioN"

239 <?> "dsl overload declaratioN"

238− where overloadable = ["let","lambda","index_first","index_next","variable"]

240+ where overloadable = ["let","lambda","pi","index_first","index_next","variable"]

239

241

240

242

test/dsl003/DSLPi.idrnew file+38

@@ -0,0 +1,38 @@

1+module DSLPi

2+

3+data Ty = BOOL | INT | UNIT | ARR Ty Ty

4+

5+dsl simple_type

6+ pi = ARR

7+

8+test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)

9+test1 = refl

10+

11+using (vars : Vect n Ty)

12+ infix 2 ===

13+

14+ data Expr : Vect n Ty -> Ty -> Type where

15+ Var : (i : Fin n) -> Expr vars (index i vars)

16+ (===) : Expr vars t -> Expr vars t -> Expr vars BOOL

17+

18+ data Spec : Vect n Ty -> Type where

19+ ForAll : (t : Ty) -> Spec (t :: vars) -> Spec vars

20+ ItHolds : Expr vars BOOL -> Spec vars

21+

22+ implicit exprSpec : Expr vars BOOL -> Spec vars

23+ exprSpec = ItHolds

24+

25+dsl specs

26+ pi = ForAll

27+ variable = Var

28+ index_first = fZ

29+ index_next = fS

30+

31+test2 : Spec []

32+test2 = specs ((x, y : INT) -> x === y)

33+

34+test3 : Spec []

35+test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ

36+

37+test4 : test2 = test3

38+test4 = refl

test/dsl003/expectednew file+2

@@ -0,0 +1,2 @@

1+ForAll INT (ForAll INT (ItHolds (Var (fS fZ) === Var fZ))) : Spec []

2+refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)

test/dsl003/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --nocolour --check DSLPi.idr -e test1 -e test2

3+rm -f *.ibc