6bef4f9 · Idris-dev · git.iko.soy

lib/io.idr+12−5

compare with master

unifiedsplit

@@ -14,6 +14,7 @@ io_return = prim__IO;

14run__IO : IO () -> IO ();

15run__IO (prim__IO v) = prim__IO v;

16

17+

18

19

19interpFTy : FTy -> Set;

20interpFTy : FTy -> Set;

@@ -27,19 +28,25 @@ interpFTy FUnit = ();

27ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

28ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

28ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {

29ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {

29 mkForeign' : List FTy -> Set -> Set;

30 mkForeign' : List FTy -> Set -> Set;

30− mkForeign' Nil ty = ty;

31+ mkForeign' Nil ty = ty;

31− mkForeign' (Cons s ss) ty = mkForeign' ss (interpFTy s -> ty);

32+ mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty);

32}

33}

33

34

35+namespace foreign {

36+

37+infixr 7 :: ;

38+

34data FEnv : List FTy -> Set where

39data FEnv : List FTy -> Set where

35− FEmpty : FEnv Nil

40+ Nil : FEnv Nil

36− | FCons : {xs:List FTy} ->

41+ | (::) : {xs:List FTy} ->

37− interpFTy x -> FEnv xs -> FEnv (Cons x xs);

42+ interpFTy x -> FEnv xs -> FEnv (x ::xs);

38

43

39data Foreign : Set -> Set where

44data Foreign : Set -> Set where

40 FFun : String -> (xs:List FTy) -> (t:FTy) ->

45 FFun : String -> (xs:List FTy) -> (t:FTy) ->

41 Foreign (ForeignTy xs t);

46 Foreign (ForeignTy xs t);

42

47

48+}

49+

43mkForeign : Foreign x -> x;

50mkForeign : Foreign x -> x;

44-- mkForeign compiled as primitive

51-- mkForeign compiled as primitive

45

52

lib/list.idr+11−9

@@ -2,38 +2,40 @@ import builtins;

2

3namespace list {

4

5+infixr 7 :: ;

6+

5−data List a = Nil | Cons a (List a);

7+data List a = Nil | (::) a (List a);

6

8

7rev : List a -> List a;

9rev : List a -> List a;

8rev xs = revAcc Nil xs where {

10rev xs = revAcc Nil xs where {

9 revAcc : List a -> List a -> List a;

11 revAcc : List a -> List a -> List a;

10 revAcc acc Nil = acc;

12 revAcc acc Nil = acc;

11− revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

13+ revAcc acc (x :: xs) = revAcc (x :: acc) xs;

12}

14}

13

15

14length : List a -> Int;

16length : List a -> Int;

15length Nil = 0;

17length Nil = 0;

16−length (Cons x xs) = 1 + length xs;

18+length (x :: xs) = 1 + length xs;

17

19

18take : Int -> List a -> List a;

20take : Int -> List a -> List a;

19take 0 xs = Nil;

21take 0 xs = Nil;

20take n Nil = Nil;

22take n Nil = Nil;

21−take n (Cons x xs) = Cons x (take (n-1) xs);

23+take n (x :: xs) = x :: take (n-1) xs;

22

24

23drop : Int -> List a -> List a;

25drop : Int -> List a -> List a;

24drop 0 xs = xs;

26drop 0 xs = xs;

25drop n Nil = Nil;

27drop n Nil = Nil;

26−drop n (Cons x xs) = drop (n-1) xs;

28+drop n (x :: xs) = drop (n-1) xs;

27

29

28map : (a -> b) -> List a -> List b;

30map : (a -> b) -> List a -> List b;

29map f Nil = Nil;

31map f Nil = Nil;

30−map f (Cons x xs) = Cons (f x) (map f xs);

32+map f (x :: xs) = f x :: map f xs;

31

33

32filter : (y -> Bool) -> List y -> List y;

34filter : (y -> Bool) -> List y -> List y;

33filter pred Nil = Nil;

35filter pred Nil = Nil;

34−filter pred (Cons x xs) with (pred x, filter pred xs) {

36+filter pred (x :: xs) with (pred x, filter pred xs) {

35− filter pred (Cons x xs) | (True, fxs) = Cons x fxs;

37+ filter pred (x :: xs) | (True, fxs) = x :: fxs;

36− filter pred (Cons x xs) | (False, fxs) = fxs;

38+ filter pred (x :: xs) | (False, fxs) = fxs;

37}

39}

38

40

39}

41}

lib/prelude.idr+3−3

@@ -44,8 +44,8 @@ instance Show a => Show (List a) where {

44 show xs = "[" ++ show' xs ++ "]" where {

45 show' : Show a => List a -> String;

46 show' Nil = "";

47− show' (Cons x Nil) = show x;

47+ show' (x :: Nil) = show x;

48− show' (Cons x xs) = show x ++ ", " ++ show' xs;

48+ show' (x :: xs) = show x ++ ", " ++ show' xs;

49 }

50}

51

@@ -106,7 +106,7 @@ log x = prim__floatLog x;

106---- some basic io

107

108putStr : String -> IO ();

109−putStr x = mkForeign (FFun "putStr" (Cons FString Nil) FUnit) x;

109+putStr x = mkForeign (FFun "putStr" (FString :: Nil) FUnit) x;

110

111putStrLn : String -> IO ();

112putStrLn x = putStr (x ++ "\n");

samples/interp.idr+1−1

@@ -29,7 +29,7 @@ using (G : Vect Ty n) {

29 | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

30 | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

31

32− interp : Env G -> [static] Expr G t -> interpTy t;

32+ interp : Env G -> {static} Expr G t -> interpTy t;

33 interp env (Var i) = envLookup i env;

34 interp env (Val x) = x;

35 interp env (Lam sc) = \x => interp (x :: env) sc;

src/Idris/Parser.hs+9−1

@@ -441,6 +441,7 @@ pSimpleExpr syn =

441 return (PTactics ts)

442 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))

443 <|> try (pPair syn)

444+ <|> try (pList syn)

444 <|> try (pAlt syn)

445 <|> try (pAlt syn)

445 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

446 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

446 <|> try (do c <- pConstant; fc <- pfc

447 <|> try (do c <- pConstant; fc <- pfc

@@ -457,6 +458,13 @@ modifyConst syn fc (PConstant (I x))

457 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]

458 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]

458modifyConst syn fc x = x

459modifyConst syn fc x = x

459

460

461+pList syn = do lchar '['; fc <- pfc

462+ xs <- sepBy (pExpr syn) (lchar ','); lchar ']'

463+ return (mkList fc xs)

464+ where

465+ mkList fc [] = PRef fc (UN "Nil")

466+ mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]

467+

460pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp

468pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp

461 fc <- pfc

469 fc <- pfc

462 r <- pExpr syn; lchar ')';

470 r <- pExpr syn; lchar ')';

@@ -532,7 +540,7 @@ pPi syn =

532 sc <- pExpr syn

540 sc <- pExpr syn

533 return (bindList (PPi (Imp lazy st)) xt sc))

541 return (bindList (PPi (Imp lazy st)) xt sc))

534 <|> do --lazy <- option False (do lchar '|'; return True)

542 <|> do --lazy <- option False (do lchar '|'; return True)

535− lchar '['; reserved "static"; lchar ']'

543+ lchar '{'; reserved "static"; lchar '}'

536 t <- pExpr' syn

544 t <- pExpr' syn

537 symbol "->"

545 symbol "->"

538 sc <- pExpr syn

546 sc <- pExpr syn

test/test001/test001.idr+1−1