Initial work on builtin constants

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 ++