From 4a95e619dd206f9f3578d420500ee3824a413b33 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 5 Aug 2016 01:24:28 +0200 Subject: Initial work on builtin constants --- events/src/Events/Spec.hs | 1 + events/src/Events/Spec/Eval.hs | 49 +++++++++++++++++++++++++++++++++-------- events/src/Events/Spec/Parse.hs | 2 +- events/src/Events/Spec/Types.hs | 11 +++++---- 4 files changed, 49 insertions(+), 14 deletions(-) diff --git a/events/src/Events/Spec.hs b/events/src/Events/Spec.hs index cfa75be..c2a84ac 100644 --- a/events/src/Events/Spec.hs +++ b/events/src/Events/Spec.hs @@ -4,6 +4,7 @@ module Events.Spec ( interpret , Spec, Cmnd(..), Expr(..), Elem(..) , module Events.Spec.Parse + , module Events.Spec.Eval ) where import Events.Spec.Types diff --git a/events/src/Events/Spec/Eval.hs b/events/src/Events/Spec/Eval.hs index 3a23e0b..24cfeb6 100644 --- a/events/src/Events/Spec/Eval.hs +++ b/events/src/Events/Spec/Eval.hs @@ -1,7 +1,10 @@ -{-# LANGUAGE GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE GADTs, DataKinds, TypeFamilies, TypeOperators, RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} +{-# LANGUAGE InstanceSigs #-} module Events.Spec.Eval ( evalExpr + , Bindable(..) ) where import Events.Spec.Types @@ -11,10 +14,11 @@ shift = shift' LZ where -- shift' :: forall ts1 ts2 t x. Length ts1 -> Expr (ts1 ++ ts2) x -> Expr (ts1 ++ t ': ts2) x shift' :: forall ts1 x. Length ts1 -> Expr m (ts1 ++ ts2) x -> Expr m (ts1 ++ t ': ts2) x - shift' _ (ELit x) = ELit x - shift' l (EVar v) = EVar $ shiftElem l v - shift' l (ELam b) = ELam $ shift' (LS l) b - shift' l (EApp f x) = EApp (shift' l f) (shift' l x) + shift' LZ (EPri f) = EPri $ const (EPri f) + shift' (LS l) (EPri f) = EPri $ shift' l . f + shift' l (EVar v) = EVar $ shiftElem l v + shift' l (ELam b) = ELam $ shift' (LS l) b + shift' l (EApp f x) = EApp (shift' l f) (shift' l x) shiftElem :: forall ts1 u. Length ts1 -> Elem u (ts1 ++ ts2) -> Elem u (ts1 ++ t ': ts2) shiftElem LZ e = ES e @@ -24,7 +28,8 @@ shift = shift' LZ beta = flip beta' LZ beta' :: forall m ts1 ts2 s t. Expr m ts2 s -> Length ts1 -> Expr m (ts1 ++ s ': ts2) t -> Expr m (ts1 ++ ts2) t -beta' _ _ (ELit x) = ELit x +beta' e LZ (EPri f) = EApp (ELam (EPri f)) e +beta' e (LS l) (EPri f) = EPri (beta' e l . f) beta' e LZ (EVar EZ ) = e beta' _ LZ (EVar (ES v)) = EVar v beta' _ (LS _) (EVar EZ ) = EVar EZ @@ -33,6 +38,32 @@ beta' e l (ELam b) = ELam $ beta' e (LS l) b beta' e l (EApp f a) = EApp (beta' e l f) (beta' e l a) evalExpr :: Expr m '[] t -> Val m t -evalExpr (ELit a) = a -evalExpr (ELam a) = a -evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) +evalExpr (EVal a) = a +evalExpr (ELam a) = a +evalExpr (EApp (ELam (EPri f)) a) = evalExpr . f $ evalExpr a +evalExpr (EApp f a) = evalExpr $ beta a (evalExpr f) + +-- liftE :: (Val m a -> Val m b) -> Expr m (a ': ctx) b +-- liftE = EPri . (EVal .) + +-- bindE :: (m a -> b) -> Expr m (a ': Ctx b) (Fin b) +-- bindE f = liftE $ bindE . f + +type family Ctx f where + Ctx (a -> b) = (a ': Ctx b) + Ctx a = '[] + +type family Fin f where + Fin (a -> b) = Fin b + Fin a = a + +class Bindable m b where + bindE :: (Val m a -> m b) -> Expr m (a ': Ctx b) (Fin b) + +instance {-# OVERLAPS #-} ((Val m b) ~ (m b), Applicative m, Bindable m c) => Bindable m (b -> c) where + bindE :: (Val m a -> m (b -> c)) -> Expr m (a ': b ': Ctx c) (Fin c) + bindE f = (EPri :: (Val m a -> Expr m (b ': Ctx c) (Fin c)) -> Expr m (a ': b ': Ctx c) (Fin c)) . ((bindE :: (Val m b -> m c) -> Expr m (b ': Ctx c) (Fin c)) . ) $ ((<*>) . f) + +instance (Val m b ~ m b, Ctx b ~ '[], Fin b ~ b) => Bindable m b where + bindE :: (Val m a -> Val m b) -> Expr m '[a] b + bindE = EPri . (EVal .) diff --git a/events/src/Events/Spec/Parse.hs b/events/src/Events/Spec/Parse.hs index 912a308..f3114f1 100644 --- a/events/src/Events/Spec/Parse.hs +++ b/events/src/Events/Spec/Parse.hs @@ -18,7 +18,7 @@ import Events.Spec.Types import Control.Monad.Catch (MonadThrow) parse :: MonadThrow m => Consumer Text m (Spec m) -parse = sinkParser $ (tokenize >>= pSpec) <* endOfInput +parse = sinkParser $ pSpec <* endOfInput pSpec :: Monad m => Parser (Spec m) pSpec = mzero diff --git a/events/src/Events/Spec/Types.hs b/events/src/Events/Spec/Types.hs index 5216f46..c7fd058 100644 --- a/events/src/Events/Spec/Types.hs +++ b/events/src/Events/Spec/Types.hs @@ -13,8 +13,11 @@ module Events.Spec.Types import Events.Types +-- | A functional language reminiscent of typed lambda calculus with monadic +-- side-effects and foreign primitives data Expr :: (* -> *) -> [*] -> * -> * where - ELit :: Val m a -> Expr m ctx a + EVal :: Val m a -> Expr m ctx a + EPri :: (Val m a -> Expr m ctx b) -> Expr m (a ': ctx) b EVar :: Elem a ctx -> Expr m ctx a ELam :: Expr m (arg ': ctx) res -> Expr m ctx (arg -> res) EApp :: Expr m ctx (arg -> a) -> Expr m ctx arg -> Expr m ctx a @@ -38,8 +41,8 @@ data Length :: [a] -> * where LZ :: Length '[] LS :: Length xs -> Length (x ': xs) -type family (xs :: [a]) ++ (ys :: [a]) :: [a] -type instance '[] ++ ys = ys -type instance (x ': xs) ++ ys = x ': (xs ++ ys) +type family (xs :: [a]) ++ (ys :: [a]) :: [a] where + '[] ++ ys = ys + (x ': xs) ++ ys = x ': (xs ++ ys) infixr 5 ++ -- cgit v1.2.3