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

git.iko.soy/Idris-dev

Overloading lists and syntactic sugar

commit6bef4f930d88bd6f31bcd7306c7ca9218d329eac authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 29 Nov 2011, 11:25 (15 years ago) parent598aca4

6 files changed+37−20

compare with master

unifiedsplit

lib/io.idr+12−5 lib/list.idr+11−9 lib/prelude.idr+3−3 samples/interp.idr+1−1 src/Idris/Parser.hs+9−1 test/test001/test001.idr+1−1

lib/io.idr+12−5

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

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

1515run__IO (prim__IO v) = prim__IO v;

1616

17+

1819

1920interpFTy : FTy -> Set;

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

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

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

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

30− mkForeign' Nil ty = ty;

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

31+ mkForeign' Nil ty = ty;

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

3233}

3334

35+namespace foreign {

36+

37+infixr 7 :: ;

38+

3439data FEnv : List FTy -> Set where

35− FEmpty : FEnv Nil

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

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

40+ Nil : FEnv Nil

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

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

3843

3944data Foreign : Set -> Set where

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

4146 Foreign (ForeignTy xs t);

4247

48+}

49+

4350mkForeign : Foreign x -> x;

4451-- mkForeign compiled as primitive

4552

lib/list.idr+11−9

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

33namespace list {

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

5+infixr 7 :: ;

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

79rev : List a -> List a;

810rev xs = revAcc Nil xs where {

911 revAcc : List a -> List a -> List a;

1012 revAcc acc Nil = acc;

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

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

1214}

1315

1416length : List a -> Int;

1517length Nil = 0;

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

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

1719

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

1921take 0 xs = Nil;

2022take 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;

2224

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

2426drop 0 xs = xs;

2527drop n Nil = Nil;

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

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

2729

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

2931map 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;

3133

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

3335filter pred Nil = Nil;

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

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

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

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

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

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

3739}

3840

3941}

lib/prelude.idr+3−3

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

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

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

4646 show' Nil = "";

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

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

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

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

4949 }

5050}

5151

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

106106---- some basic io

107107

108108putStr : String -> IO ();

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

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

110110

111111putStrLn : String -> IO ();

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

samples/interp.idr+1−1

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

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

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

3131

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

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

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

3434 interp env (Val x) = x;

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

src/Idris/Parser.hs+9−1

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

441441 return (PTactics ts)

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

443443 <|> try (pPair syn)

444+ <|> try (pList syn)

444445 <|> try (pAlt syn)

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

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

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

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

458459modifyConst syn fc x = x

459460

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+

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

461469 fc <- pfc

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

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

532540 sc <- pExpr syn

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

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

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

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

536544 t <- pExpr' syn

537545 symbol "->"

538546 sc <- pExpr syn

test/test001/test001.idr+1−1