1a12cc3 · Idris-dev · git.iko.soy

lib/prelude.idr+1−1

compare with master

unifiedsplit

@@ -127,7 +127,7 @@ instance Functor List where {

127

128infixl 2 <$>;

129

130−class Functor f => Applicative (f : Set -> Set) where {

130+class Applicative (f : Set -> Set) where {

131 pure : a -> f a;

132 (<$>) : f (a -> b) -> f a -> f b;

133}

test/README+1

@@ -6,3 +6,4 @@ Tests:

6004: File operations

7005: Num class resolution [regression]; span & break; ad-hoc overloading

8006: Provisional definitions; class resolution in patterns

9+007: Applicative and idiom brackets

test/test007/expectednew file+4

@@ -0,0 +1,4 @@

1+Just 8

2+Just sssssssssO

3+Just 42

4+Nothing

test/test007/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris test007.idr -o test007

3+./test007

4+rm -f test007 test007.ibc

test/test007/test007.idrnew file+53

@@ -0,0 +1,53 @@

1+module main;

2+

3+instance Applicative Maybe where {

4+ (Just f) <$> (Just a) = Just (f a);

5+ Nothing <$> Nothing = Nothing;

6+

7+ pure x = Just x;

8+}

9+

10+data Expr = Var String

11+ | Val Int

12+ | Add Expr Expr;

13+

14+

15+data Eval : Set -> Set where

16+ MkEval : (List (String, Int) -> Maybe a) -> Eval a;

17+

18+fetch : String -> Eval Int;

19+fetch x = MkEval (\e => fetchVal e) where {

20+ fetchVal : List (String, Int) -> Maybe Int;

21+ fetchVal [] = Nothing;

22+ fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);

23+}

24+

25+instance Applicative Eval where {

26+ pure x = MkEval (\e => Just x);

27+

28+ (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {

29+ appAux : Maybe (a -> b) -> Maybe a -> Maybe b;

30+ appAux (Just fx) (Just gx) = Just (fx gx);

31+ appAux _ _ = Nothing;

32+ }

33+}

34+

35+eval : Expr -> Eval Int;

36+eval (Var x) = fetch x;

37+eval (Val x) = [| x |];

38+eval (Add x y) = [| eval x + eval y |];

39+

40+runEval : List (String, Int) -> Expr -> Maybe Int;

41+runEval env e with eval e {

42+ | MkEval envFn = envFn env;

43+}

44+

45+main : IO ();

46+main = do { print [| (*2) (Just 4) |];

47+ print [| plus (Just 4) (Just 5) |];

48+ print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))));

49+ print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))));

50+ };

51+

52+

53+