8ab9f72 · Idris-dev · git.iko.soy

CHANGELOG+6−1

compare with master

unifiedsplit

@@ -14,7 +14,12 @@ New in 0.9.17:

14 been renamed to (<*) and (*>). The cascading effects of this rename

15 are that Algebra.(<*>) has been renamed to Algebra.(<.>) and

16 Matrix.(<.>) is now Matrix.(<:>).

17−

17+* Binding forms in DSL notation are now given an extra argument: a

18+ reflected representation of the name that the user chose.

19+ Specifically, the rewritten lambda, pi, and let binders will now get

20+ an extra argument of type TTName. This allows more understandable

21+ dynamic errors in DSL code and more readable code generation results.

22+

18New in 0.9.16:

23New in 0.9.16:

19--------------

24--------------

20* Inductive-inductive definitions are now supported (i.e. simultaneously

25* Inductive-inductive definitions are now supported (i.e. simultaneously

src/Idris/DSL.hs+28−6

@@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

17desugar syn i t = let t' = expandDo (dsl_info syn) t in

18 t' -- addImpl i t'

19

20+mkTTName :: FC -> Name -> PTerm

21+mkTTName fc n =

22+ let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])

23+ mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))

24+ [ pexp (stringC x)

25+ , pexp (mkList fc xs)]

26+ stringC = PConstant . Str . str

27+ intC = PConstant . I

28+ reflm n = sNS (sUN n) ["Reflection", "Language"]

29+ in case n of

30+ UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]

31+ NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)

32+ , pexp (mkList fc ns)]

33+ MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)

34+ , pexp (stringC nm)]

35+ otherwise -> PRef fc $ reflm "NErased"

36+

20expandDo :: DSL -> PTerm -> PTerm

37expandDo :: DSL -> PTerm -> PTerm

21expandDo dsl (PLam fc n ty tm)

38expandDo dsl (PLam fc n ty tm)

22 | Just lam <- dsl_lambda dsl

39 | Just lam <- dsl_lambda dsl

40+ = let sc = PApp fc lam [ pexp (mkTTName fc n)

23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in

41+ , pexp (var dsl n tm 0)]

24− expandDo dsl sc

42+ in expandDo dsl sc

25expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

43expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

26expandDo dsl (PLet fc n ty v tm)

44expandDo dsl (PLet fc n ty v tm)

27 | Just letb <- dsl_let dsl

45 | Just letb <- dsl_let dsl

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

46+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

47+ , pexp v

48+ , pexp (var dsl n tm 0)]

29− expandDo dsl sc

49+ in expandDo dsl sc

30expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

50expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

31expandDo dsl (PPi p n ty tm)

51expandDo dsl (PPi p n ty tm)

32 | Just pi <- dsl_pi dsl

52 | Just pi <- dsl_pi dsl

53+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

54+ , pexp ty

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

55+ , pexp (var dsl n tm 0)]

34− expandDo dsl sc

56+ in expandDo dsl sc

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

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

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

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

37 (map (fmap (expandDo dsl)) args)

59 (map (fmap (expandDo dsl)) args)

test/dsl001/test001.idr+4−1

@@ -35,8 +35,11 @@ using (G : Vect n Ty)

35 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

36 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b

37

38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)

39+ lam_ _ = Lam

40+

38 dsl expr

41 dsl expr

39− lambda = Lam

42+ lambda = lam_

40 variable = Var

43 variable = Var

41 index_first = stop

44 index_first = stop

42 index_next = pop

45 index_next = pop

test/dsl002/Resimp.idr+6−1

@@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

156 = interp env v (\env', v' => do n <- v'

157 interp env' (f n) k)

158

159+ let_ : _ -> Creator (interpTy a) ->

160+ Res (a :: gam) (Val () :: gam') (R t) ->

161+ Res gam gam' (R t)

162+ let_ _ = Let

163+

159-- run : {static} Res [] [] (R t) -> IO t

164-- run : {static} Res [] [] (R t) -> IO t

160-- run prog = interp [] prog (\env, res => res)

165-- run prog = interp [] prog (\env, res => res)

161

166

@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)

163

168

164dsl res

169dsl res

165 variable = id

170 variable = id

166− let = Let

171+ let = let_

167 index_first = stop

172 index_first = stop

168 index_next = pop

173 index_next = pop

169

174

test/dsl003/DSLPi.idr+8−2

@@ -5,8 +5,11 @@ import Data.Vect

5

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

7

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

9+arr_ _ = ARR

10+

8dsl simple_type

11dsl simple_type

9− pi = ARR

12+ pi = arr_

10

13

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

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

12test1 = Refl

15test1 = Refl

@@ -25,8 +28,11 @@ using (vars : Vect n Ty)

25 implicit exprSpec : Expr vars BOOL -> Spec vars

28 implicit exprSpec : Expr vars BOOL -> Spec vars

26 exprSpec = ItHolds

29 exprSpec = ItHolds

27

30

31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars

32+ forall_ _ = ForAll

33+

28dsl specs

34dsl specs

29− pi = ForAll

35+ pi = forall_

30 variable = Var

36 variable = Var

31 index_first = FZ

37 index_first = FZ

32 index_next = FS

38 index_next = FS

test/sourceLocation001/SourceLoc.idr+3−1

@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)

54 run (App f x) env = !(run f env) !(run x env)

55 run (Die {loc}) _ = Left loc

56

57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

58+ lam_ _ = Lam

57

59

58exec : Tm [] t -> IO ()

60exec : Tm [] t -> IO ()

59exec tm = case run tm [] of

61exec tm = case run tm [] of

@@ -64,7 +66,7 @@ dsl lang

64 variable = Var

66 variable = Var

65 index_first = FZ

67 index_first = FZ

66 index_next = FS

68 index_next = FS

67− lambda = Lam

69+ lambda = lam_

68

70

69testTerm1 : Tm [] (Arr U U)

71testTerm1 : Tm [] (Arr U U)

70testTerm1 = lang (\x=>Die)

72testTerm1 = lang (\x=>Die)

test/sourceLocation001/expected+2−2

@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)

3Testing using inline tactics

4FileLoc "SourceLoc.idr" (20, 17) (20, 17)

5Testing using metavariable with later definition

6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)

6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)

7-----------------------

8Success!

9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)

9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)

10Success!

11Success!