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

git.iko.soy/Idris-dev

Add pi to overridable syntax in DSL blocks

commit9993f3bd80e428ba3749fc79d407cc90101d0e4f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 9 Jun 2014, 23:36 (12 years ago) parent590140a

10 files changed+71−9

compare with master

unifiedsplit

CHANGELOG+2 idris.cabal+3 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/DSL.hs+8−1 src/Idris/DeepSeq.hs+3−2 src/Idris/IBC.hs+4−2 src/Idris/ParseData.hs+5−3 test/dsl003/DSLPi.idr+38 test/dsl003/expected+2 test/dsl003/run+3

CHANGELOG+2

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

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

44 --testpkg command-line option

55* 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".

79New in 0.9.13:

810--------------

idris.cabal+3

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

289289 test/dsl002/test

290290 test/dsl002/*.idr

291291 test/dsl002/expected

292+ test/dsl003/run

293+ test/dsl003/*.idr

294+ test/dsl003/expected

292295

293296 test/effects001/run

294297 test/effects001/*.idr

src/Idris/AbsSyntaxTree.hs+3−1

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

904904 index_first :: Maybe t,

905905 index_next :: Maybe t,

906906 dsl_lambda :: Maybe t,

907− dsl_let :: Maybe t

907+ dsl_let :: Maybe t,

908+ dsl_pi :: Maybe t

908909 }

909910 deriving (Show, Functor)

910911{-!

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

948949 Nothing

949950 Nothing

950951 Nothing

952+ Nothing

951953 where f = fileFC "(builtin)"

952954

953955data Using = UImplicit Name PTerm

src/Idris/DSL.hs+8−1

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

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

3030 expandDo dsl sc

3131expandDo 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

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

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

3438 (map (fmap (expandDo dsl)) args)

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

8892 | Nothing <- dsl_let dsl

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

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

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

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

96+ | Nothing <- dsl_pi dsl

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

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

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

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

94101 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

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

292292

293293instance (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)

295295 = rnf x1 `seq`

296296 rnf x2 `seq`

297297 rnf x3 `seq`

298298 rnf x4 `seq`

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

299+ rnf x5 `seq`

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

300301

301302instance NFData SynContext where

302303 rnf PatternSyntax = ()

src/Idris/IBC.hs+4−2

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

21912191 return (Rule x1 x2 x3)

21922192

21932193instance (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)

21952195 = do put x1

21962196 put x2

21972197 put x3

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

22012201 put x7

22022202 put x8

22032203 put x9

2204+ put x10

22042205 get

22052206 = do x1 <- get

22062207 x2 <- get

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

22112212 x7 <- get

22122213 x8 <- get

22132214 x9 <- get

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

2215+ x10 <- get

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

22152217

22162218instance Binary SSymbol where

22172219 put x

src/Idris/ParseData.hs+5−3

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

209209 first = lookup "index_first" bs

210210 next = lookup "index_next" bs

211211 leto = lookup "let" bs

212− lambda = lookup "lambda" bs in

212+ lambda = lookup "lambda" bs

213+ pi = lookup "pi" bs in

213214 initDSL { dsl_var = var,

214215 index_first = first,

215216 index_next = next,

216217 dsl_lambda = lambda,

217− dsl_let = leto }

218+ dsl_let = leto,

219+ dsl_pi = pi }

218220

219221{- | Checks DSL for errors -}

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

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

235237 t <- expr syn

236238 return (o, t)

237239 <?> "dsl overload declaratioN"

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

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

239241

240242

test/dsl003/DSLPi.idrnew file+38

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

1+module DSLPi

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

5+dsl simple_type

6+ pi = ARR

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