Test for idiom brackets and Applicative class

lib/prelude.idr

@@ -127,7 +127,7 @@ instance Functor List where {
 
 infixl 2 <$>;
 
-class Functor f => Applicative (f : Set -> Set) where {
+class Applicative (f : Set -> Set) where {
     pure  : a -> f a;
     (<$>) : f (a -> b) -> f a -> f b; 
 }

test/README

@@ -6,3 +6,4 @@ Tests:
 004: File operations
 005: Num class resolution [regression]; span & break; ad-hoc overloading
 006: Provisional definitions; class resolution in patterns
+007: Applicative and idiom brackets

test/test007/expected

@@ -0,0 +1,4 @@
+Just 8
+Just sssssssssO
+Just 42
+Nothing

test/test007/run

@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test007.idr -o test007
+./test007
+rm -f test007 test007.ibc

test/test007/test007.idr

@@ -0,0 +1,53 @@
+module main;
+
+instance Applicative Maybe where {
+  (Just f) <$> (Just a) = Just (f a);
+  Nothing  <$> Nothing  = Nothing;
+
+  pure x = Just x;
+}
+
+data Expr = Var String
+          | Val Int
+          | Add Expr Expr;
+
+
+data Eval : Set -> Set where
+   MkEval : (List (String, Int) -> Maybe a) -> Eval a;
+
+fetch : String -> Eval Int;
+fetch x = MkEval (\e => fetchVal e) where {
+    fetchVal : List (String, Int) -> Maybe Int;
+    fetchVal [] = Nothing;
+    fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
+}
+
+instance Applicative Eval where {
+    pure x = MkEval (\e => Just x);
+
+    (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where {
+       appAux : Maybe (a -> b) -> Maybe a -> Maybe b;
+       appAux (Just fx) (Just gx) = Just (fx gx);
+       appAux _         _         = Nothing;
+    }
+}
+
+eval : Expr -> Eval Int;
+eval (Var x)   = fetch x;
+eval (Val x)   = [| x |];
+eval (Add x y) = [| eval x + eval y |];
+
+runEval : List (String, Int) -> Expr -> Maybe Int;
+runEval env e with eval e {
+    | MkEval envFn = envFn env;
+}
+
+main : IO ();
+main = do { print [| (*2) (Just 4) |];
+            print [| plus (Just 4) (Just 5) |]; 
+            print (runEval [("x",21), ("y", 20)] (Add (Val 1) (Add (Var "x") (Var "y"))));
+            print (runEval [("x",21)] (Add (Val 1) (Add (Var "x") (Var "y"))));
+          };
+
+
+