git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/test/tutorial003/tutorial003.idr
38 lines 1.0 kB history raw
1module idiom
3data Expr = Var String
4 | Val Int
5 | Add Expr Expr
7data Eval : Type -> Type where
8 MkEval : (List (String, Int) -> Maybe a) -> Eval a
10fetch : String -> Eval Int
11fetch x = MkEval (\e => fetchVal e) where
12 fetchVal : List (String, Int) -> Maybe Int
13 fetchVal [] = Nothing
14 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)
16instance Functor Eval where
17 map f (MkEval g) = MkEval (\e => map f (g e))
19instance Applicative Eval where
20 pure x = MkEval (\e => Just x)
22 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
23 app : Maybe (a -> b) -> Maybe a -> Maybe b
24 app (Just fx) (Just gx) = Just (fx gx)
25 app _ _ = Nothing
27eval : Expr -> Eval Int
28eval (Var x) = fetch x
29eval (Val x) = [| x |]
30eval (Add x y) = [| eval x + eval y |]
32runEval : List (String, Int) -> Expr -> Maybe Int
33runEval env e = case eval e of
34 MkEval envFn => envFn env
36m_add' : Maybe Int -> Maybe Int -> Maybe Int
37m_add' x y = [| x + y |]