--
-- To as large of an extent as possible, we wish to capture the static
-- semantics of K3 in the Haskell type system.
+--
+-- This file uses some rather exciting extensions and as such is in a
+-- Haskell-friendly definition order, rather than the cleanest
+-- human-friendly ordering. Sorry about that.
+--
+-- XXX Currently does not have any mechanism for declaring local variables
+-- The K3 Way -- right now the only way to do that is let-as-lambda.
+--
-- Header material {{{
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-module Dyna.BackendK3.AST where
-
-import Data.Word
-import GHC.Prim (Constraint)
-import Language.Haskell.TH (varT, mkName)
-
-import Dyna.XXX.THTuple
+module Dyna.BackendK3.AST (
+ HList(..), HRList(..),
-------------------------------------------------------------------------}}}
-{- * Preliminaries -} -- {{{
+ VarIx(..), AddrIx(..),
- -- XXX
-newtype VarIx = Var String
- -- XXX (Hostname,Port)
-newtype AddrIx = Addr (String,Int)
- deriving (Eq,Show)
+ BiNum(..), UnNum(..),
- -- XXX This has a phantom type only so that we can use it as an r
- -- in RTupled. We'd rather not (see .Render's need to use fdscast)
-data FunDepSpec a = FDIrr | FDDom | FDCod
- deriving (Eq,Show)
+ CTE, CKind(..), CollTy(..),
- -- XXX should really do something smarter
-data Ann a where
+ Ref,
- -- | Decorate an expression as atomic.
- AAtomic :: Ann a
+ PKind(..), Pat(..),
+ PVar(..), PUnk(..), PJust(..), PRef(..),
+ MapPatConst,
- -- | A functional dependency among elements of a collection.
- AFunDep :: (RTupled fs, RTE fs ~ a, RTR fs ~ FunDepSpec)
- => fs -> Ann (CTE r t a)
+ Ann(..), FunDepSpec(..),
- -- XXX Declare an additional index
- -- AIndex :: (RTupled fs, RTE fs ~ a, RTR fs ~ FunDepSpec)
- -- => fs -> Ann (CTE r t a)
+ K3BaseTy,
- -- | An "Exactly-One-Of" annotation, used to convey variants (i.e. sums)
- -- to K3.
- AOneOf :: (RTupled mv, RTR mv ~ Maybe) => Ann mv
+ K3Ty(..), UnivTyRepr(..),
- -- | An escape hatch! (XXX)
- AMisc :: String -> Ann a
+ K3(..), K3_Pat_C, K3_Coll_C, K3_Slice_C,
-------------------------------------------------------------------------}}}
-{- * Collections -} -- {{{
+ asColl,
-data CKind = CBag | CList | CSet
+ Decl(..), mkdecl, mkfdecl, asCollR, asRefR
+) where
-data family CTE (r :: * -> *) (c :: CKind) e
+import Data.Word
+import GHC.Prim (Constraint)
+-- import Language.Haskell.TH (varT, mkName)
-data CollTy c where
- CTBag :: CollTy CBag
- CTList :: CollTy CList
- CTSet :: CollTy CSet
+import Dyna.XXX.HList
+import Dyna.XXX.THTuple
------------------------------------------------------------------------}}}
-{- * Effectables (XXX TODO) -} -- {{{
-
-{-
-data MKind = MKImmut | MKMut
-
-data MTy m where
- MTImmut :: MTy MKImmut
- MTMut :: MTy MKMut
-
-data VKind = VKIsol | VKCont
-
-data VTy v where
- VTIsol :: VTy VKIsol
- VTCont :: VTy VKCont
--}
+{- * Preliminaries -} -- {{{
-data family Ref (r :: * -> *) a
+ -- XXX
+newtype VarIx = Var String
+ -- XXX (Hostname,Port)
+newtype AddrIx = Addr (String,Int)
+ deriving (Eq,Show)
------------------------------------------------------------------------}}}
-{- * Type System -} -- {{{
+{- * Type System: Base Constraints -} -- {{{
--- | A constraint for "base" types in K3. These are the things that can
+-- | A constraint for /base/ types in K3. These are the things that can
-- be passed to lambdas. Essentially everything other than arrows.
class K3BaseTy a
instance K3BaseTy Bool
instance K3BaseTy Int
instance K3BaseTy String
instance K3BaseTy ()
-instance (K3BaseTy a) => K3BaseTy (CTE r c a)
instance (K3BaseTy a) => K3BaseTy (Maybe a)
-instance (K3BaseTy a) => K3BaseTy (Ref r a)
+instance K3BaseTy (HList '[])
+instance (K3BaseTy a, K3BaseTy (HList as)) => K3BaseTy (HList (a ': as))
$(mkTupleRecInstances ''K3BaseTy [])
--- | Data level representation of K3 types, indexed by equivalent type in
--- Haskell.
-class K3Ty (r :: * -> *) where
- -- | Attach an annotation to a type
- tAnn :: r a -> [Ann a] -> r a
-
- tAddress :: r AddrIx
- tBool :: r Bool
- tByte :: r Word8
- tFloat :: r Float
- tInt :: r Int
- tString :: r String
- tUnit :: r ()
+------------------------------------------------------------------------}}}
+{- * Collections -} -- {{{
- -- tPair :: r a -> r b -> r (a,b)
- tMaybe :: r a -> r (Maybe a)
- tRef :: r a -> r (Ref r' a)
- tColl :: (K3BaseTy a) => CollTy c -> r a -> r (CTE r' c a)
- tFun :: r a -> r b -> r (a -> b)
+-- | Reflect 'CollTy' at the type level.
+data CKind = CBag | CList | CSet
- -- XXX TUPLES
- -- tTuple :: (RTupled rt, RTR rt ~ r, RTE rt ~ t) => rt -> r t
- tTuple2 :: (r a, r b) -> r (a,b)
- tTuple3 :: (r a, r b, r c) -> r (a,b,c)
- tTuple4 :: (r a, r b, r c, r d) -> r (a,b,c,d)
- tTuple5 :: (r a, r b, r c, r d, r e) -> r (a,b,c,d,e)
+-- | The 'r' representation of a collection of kind 'c' of elements 'e'.
+data family CTE (r :: * -> *) (c :: CKind) e
--- | Universal typeclass wrapper for K3Ty
-newtype UnivTyRepr (a :: *) = UTR { unUTR :: forall r . (K3Ty r) => r a }
+-- | Data-level specification of collection kinds
+data CollTy c where
+ CTBag :: CollTy CBag
+ CTList :: CollTy CList
+ CTSet :: CollTy CSet
-instance K3Ty UnivTyRepr where
- tAnn (UTR t) s = UTR $ tAnn t s
+instance (K3BaseTy a) => K3BaseTy (CTE r c a)
- tAddress = UTR tAddress
- tBool = UTR tBool
- tByte = UTR tByte
- tFloat = UTR tFloat
- tInt = UTR tInt
- tString = UTR tString
- tUnit = UTR tUnit
+-- | A representation-specific constraint for collections, on functions
+-- which need to dispatch on a type-tag in the output.
+type family K3_Coll_C (r :: * -> *) (c :: CKind) :: Constraint
- tColl c (UTR a) = UTR $ tColl c a
- tFun (UTR a) (UTR b) = UTR $ tFun a b
- tMaybe (UTR a) = UTR $ tMaybe a
- tRef (UTR a) = UTR $ tRef a
+------------------------------------------------------------------------}}}
+{- * References -} -- {{{
- -- XXX TUPLES
- -- tTuple us = UTR $ tTuple $ tupleopRS unUTR us
- tTuple2 us = UTR $ tTuple2 $ tupleopRS unUTR us
- tTuple3 us = UTR $ tTuple3 $ tupleopRS unUTR us
- tTuple4 us = UTR $ tTuple4 $ tupleopRS unUTR us
- tTuple5 us = UTR $ tTuple5 $ tupleopRS unUTR us
+-- | The 'r' representation of references of elements of type 'a'
+data family Ref (r :: * -> *) a
+instance (K3BaseTy a) => K3BaseTy (Ref r a)
------------------------------------------------------------------------}}}
{- * Pattern System -} -- {{{
-- | Kinds of patterns permitted in K3
data PKind where
- -- | Variables in patterns
+ -- | Variables in patterns (see 'PVar')
PKVar :: r -> k -> PKind
- -- | Wildcards in patterns
+ -- | Wildcards in patterns (see 'PUnk')
PKUnk :: k -> PKind
- -- | Just patterns (fail on Nothing)
- --
- -- Note the distinction between PatTy and (PatBTy and PatReprFn) here!
- -- This pattern witnesses a type "Maybe a" but binds a variable of type
- -- "a". This will in general be true of any variant (i.e. sum) pattern.
+ -- | Just patterns (see 'PJust')
PKJust :: PKind -> PKind
+ -- | Ref patterns (see 'PRef')
+ PKRef :: PKind -> PKind
+
+ -- | HList patterns
+ PKHL :: [PKind] -> PKind
+
-- | Product ("tuple") patterns
--
- -- Product patterns, on the other hand, have PatTy and PatReprFn both
- -- producing tuples.
+ -- 'PatTy' and 'PatReprFn' both produce tuples.
PKTup :: [PKind] -> PKind
-- | Provides witnesses that certain types may be used
-- up type signatures and pattern matches in lambdas.
--
-- Note that this is a closed class using the promoted
--- data PKind.
---
--- PatDa is needed for Render's function, since every
--- lambda needs an explicit type signature on its variable.
+-- data 'PKind'.
--
--- Essentially, these things determine where "r"s end up
+-- Essentially, these things determine where 's's end up
-- in the lambda given to eLam. Compare and contrast:
--- eLam (PVar $ tMaybe tInt) :: (r (Maybe Int) -> _) -> _
--- eLam (PJust $ PVar tInt) :: (r Int -> _) -> _
+--
+-- > eLam (PVar $ tMaybe tInt) :: (s (Maybe Int) -> _) -> _
+-- > eLam (PJust $ PVar tInt) :: (s Int -> _) -> _
--
--- eLam (PVar $ tPair tInt tInt) :: (r (Int, Int) -> _) -> _
--- eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _
+-- > eLam (PVar $ tPair tInt tInt) :: (s (Int, Int) -> _) -> _
+-- > eLam (PPair (PVar tInt) (PVar tInt)) :: ((s Int, s Int) -> _) -> _
+--
+-- The 's' parameter on 'PatTy', 'PatBTy', and 'PatReprFn' is the
+-- underlying representation being manipulated, as above. It is notably
+-- used to constrain the representation of 'Ref's to be consistent across
+-- a pattern.
+--
+-- The 'r' class parameter (also on 'PVar') is the representation of
+-- components of the pattern itself, and is used to constrain
+-- representation of variables. When being used as slices, @r ~ s@; when
+-- being used as patterns for lambdas, @r ~ UnivTyRepr@ and 's' is a 'K3'.
+-- In this latter case, 'PatDa' is needed for "Dyna.BackendK3.Render"'s
+-- function, since every lambda needs an explicit type signature on its
+-- variable.
--
class (UnPatDa (PatDa w) ~ w) => Pat (r :: * -> *) (w :: PKind) where
-- | Any data this witness needs to carry around
type PatDa w :: *
-- | The type this witness witnesses (i.e. the things matched against)
- type PatTy w :: *
+ type PatTy (s :: * -> *) w :: *
-- | The type this witness binds (i.e. after matching is done)
- type PatBTy w :: *
+ type PatBTy (s :: * -> *) w :: *
-- | The type of this pattern.
type PatReprFn (s :: * -> *) w :: *
+-- | Given a chunk of pattern data, recover the PKind.
type family UnPatDa (pd :: *) :: PKind
-data PVar r a = PVar (r a)
+-- | A variable used literally in a pattern
+newtype PVar r a = PVar (r a)
type instance UnPatDa (PVar r a) = PKVar r a
instance (K3BaseTy a, r ~ r') => Pat r' (PKVar (r :: * -> *) (a :: *)) where
- type PatDa (PKVar r a) = PVar r a
- type PatTy (PKVar r a) = a
- type PatBTy (PKVar r a) = a
+ type PatDa (PKVar r a) = PVar r a
+ type PatTy s (PKVar r a) = a
+ type PatBTy s (PKVar r a) = a
type PatReprFn s (PKVar r a) = s a
+-- | A pattern wildcard.
+--
+-- Note that 'PatReprFn s (PUnk a) ~ ()', which should prohibit even
+-- accidental use as part of a 'K3' expression or type.
data PUnk a = PUnk
type instance UnPatDa (PUnk a) = PKUnk a
instance (K3BaseTy a) => Pat r (PKUnk (a :: *)) where
- type PatDa (PKUnk a) = PUnk a
- type PatTy (PKUnk a) = a
- type PatBTy (PKUnk a) = ()
- type PatReprFn s (PKUnk a) = s ()
+ type PatDa (PKUnk a) = PUnk a
+ type PatTy s (PKUnk a) = a
+ type PatBTy s (PKUnk a) = ()
+ type PatReprFn s (PKUnk a) = ()
-data PJust a = PJust { unPJust :: a }
-type instance UnPatDa (PJust a) = PKJust (UnPatDa a)
+-- | A /Just/ pattern. Eliminates a Just constructor, and causes the
+-- trigger to abort on a Nothing.
+--
+-- Note the distinction between PatTy and (PatBTy and PatReprFn) here!
+-- This pattern witnesses a type "Maybe a" but binds a variable of type
+-- "a". This will in general be true of any variant (i.e. sum) pattern.
+newtype PJust w = PJust { unPJust :: PatDa w }
+type instance UnPatDa (PJust w) = PKJust w
instance (Pat r w) => Pat r (PKJust w) where
- type PatDa (PKJust w) = PJust (PatDa w)
- type PatTy (PKJust w) = Maybe (PatTy w)
- type PatBTy (PKJust w) = PatBTy w
+ type PatDa (PKJust w) = PJust w
+ type PatTy s (PKJust w) = Maybe (PatTy s w)
+ type PatBTy s (PKJust w) = PatBTy s w
type PatReprFn s (PKJust w) = PatReprFn s w
-type family MapPatDa (x :: [PKind]) :: *
-$(mkTyMapFlat 0 ''MapPatDa ''PatDa)
+-- | A /Ref/ pattern; dereferences the provided reference.
+newtype PRef w = PRef { unPRef :: PatDa w }
+type instance UnPatDa (PRef w) = PKRef w
+instance (Pat r w) => Pat r (PKRef w) where
+ type PatDa (PKRef w) = PRef w
+ type PatTy s (PKRef w) = Ref s (PatTy s w)
+ type PatBTy s (PKRef w) = PatBTy s w
+ type PatReprFn s (PKRef w) = PatReprFn s w
+
+-- ** Tuples
+
+type family TMapPatDa (x :: [PKind]) :: *
+$(mkTyMapFlat 0 ''TMapPatDa ''PatDa)
type family UnMapPatDa (x :: *) :: [PKind]
$(mkTyUnMap Nothing 0 ''UnMapPatDa ''UnPatDa)
-type family MapPatTy (x :: [PKind]) :: *
-$(mkTyMapFlat 0 ''MapPatTy ''PatTy)
+type family TMapPatTy (s :: * -> *) (x :: [PKind]) :: *
+$(mkTyMapFlat 1 ''TMapPatTy ''PatTy)
-type family MapPatBTy (x :: [PKind]) :: *
-$(mkTyMapFlat 0 ''MapPatBTy ''PatBTy)
+type family TMapPatBTy (s :: * -> *) (x :: [PKind]) :: *
+$(mkTyMapFlat 1 ''TMapPatBTy ''PatBTy)
-type family MapPatReprFn (r :: * -> *) (x :: [PKind]) :: *
-$(mkTyMapFlat 1 ''MapPatReprFn ''PatReprFn)
+type family TMapPatReprFn (r :: * -> *) (x :: [PKind]) :: *
+$(mkTyMapFlat 1 ''TMapPatReprFn ''PatReprFn)
$(mkTyUnMap (Just 'PKTup) 0 ''UnPatDa ''UnPatDa)
type instance MapPatConst '[] r = ()
type instance MapPatConst (x ': xs) r = (Pat r x, MapPatConst xs r)
-instance (UnPatDa (MapPatDa ts) ~ 'PKTup ts, MapPatConst ts r)
+instance (UnPatDa (TMapPatDa ts) ~ PKTup ts, MapPatConst ts r)
=> Pat r (PKTup (ts :: [PKind])) where
- type PatDa (PKTup ts) = MapPatDa ts
- type PatTy (PKTup ts) = MapPatTy ts
- type PatBTy (PKTup ts) = MapPatBTy ts
- type PatReprFn s (PKTup ts) = MapPatReprFn s ts
+ type PatDa (PKTup ts) = TMapPatDa ts
+ type PatTy s (PKTup ts) = TMapPatTy s ts
+ type PatBTy s (PKTup ts) = TMapPatBTy s ts
+ type PatReprFn s (PKTup ts) = TMapPatReprFn s ts
+
+-- ** HLists
+
+type instance UnMapPatDa (HList '[]) = '[]
+type instance UnMapPatDa (HList (a ': as)) = UnPatDa a ': (UnMapPatDa (HList as))
+type instance UnPatDa (HList x) = PKHL (UnMapPatDa (HList x))
+
+type family MapPatDa (x :: [PKind]) :: [*]
+type instance MapPatDa ('[]) = '[]
+type instance MapPatDa (w ': ws) = PatDa w ': (MapPatDa ws)
+
+type family MapPatTy (r :: * -> *) (x :: [PKind]) :: [*]
+type instance MapPatTy r ('[]) = '[]
+type instance MapPatTy r (w ': ws) = PatTy r w ': (MapPatTy r ws)
+
+type family MapPatBTy (r :: * -> *) (x :: [PKind]) :: [*]
+type instance MapPatBTy r ('[]) = '[]
+type instance MapPatBTy r (w ': ws) = PatBTy r w ': (MapPatBTy r ws)
+
+type family MapPatReprFn (r :: * -> *) (x :: [PKind]) :: [*]
+type instance MapPatReprFn r '[] = '[]
+type instance MapPatReprFn r (w ': ws) = PatReprFn r w ': (MapPatReprFn r ws)
+
+instance (UnPatDa (HList (MapPatDa ts)) ~ PKHL ts, MapPatConst ts r)
+ => Pat r (PKHL (ts :: [PKind])) where
+ type PatDa (PKHL ts) = HList (MapPatDa ts)
+ type PatTy s (PKHL ts) = HList (MapPatTy s ts)
+ type PatBTy s (PKHL ts) = HList (MapPatBTy s ts)
+ type PatReprFn s (PKHL ts) = HList (MapPatReprFn s ts)
+
+-- | A representation-specific constraint on handling patterns, on 'eLam'.
+type family K3_Pat_C (r :: * -> *) (w :: PKind) :: Constraint
+
+-- | A representation-specific constraint for slices, on 'eSlice'.
+type family K3_Slice_C (r :: * -> *) (w :: PKind) :: Constraint
+
+------------------------------------------------------------------------}}}
+{- * Annotations -} -- {{{
+
+-- | Specification for functional dependencies within a collection.
+--
+-- XXX This has a phantom type only so that we can use it as an r
+-- in RTupled. We'd rather not (see "Dyna.BackendK3.Render"'s
+-- need to use fdscast)
+data FunDepSpec a = FDIrr -- ^ /Irr/elevant to a fundep
+ | FDDom -- ^ In the /Dom/ain of a fundep
+ | FDCod -- ^ In the /Cod/omain of a fundep
+ deriving (Eq,Show)
+
+-- | Annotations on 'K3' expressions or 'K3Ty' types.
+--
+-- XXX should really do something smarter
+data Ann a where
+
+ -- | Decorate an expression as atomic.
+ AAtomic :: Ann a
+
+ -- | A functional dependency among elements of a collection.
+ AFunDep :: (RTupled fs, RTR fs ~ FunDepSpec, RTE fs ~ a)
+ => fs -> Ann (CTE r t a)
+
+ -- | Request an additional index on a collection
+ AIndex :: (RTupled fs, RTR fs ~ FunDepSpec, RTE fs ~ a)
+ => fs -> Ann (CTE r t a)
+
+ -- | An Exactly-One-Of annotation, used to convey variants (i.e. sums)
+ -- to K3.
+ AOneOf :: (RTupled mv, RTR mv ~ Maybe) => Ann mv
+
+ -- | 'AFunDep' for HList representations
+ AFunDepHL :: HRList FunDepSpec a -> Ann (CTE r t (HList a))
+
+ -- | 'AIndex' for HList representations
+ AIndexHL :: HRList FunDepSpec a -> Ann (CTE r t (HList a))
+
+ -- | 'AOneOf' for HList representations
+ --
+ -- XXX Constraints by analogy to AOneOf
+ AOneOfHL :: Ann (HList mv)
+
+{-
+ - XXX
+ -- | A cross-reference between collections
+ AXref :: r' (CTE rf tf af)
+ -> ???
+ -> Ann (CTE rt tt at)
+-}
+
+ -- | An escape hatch! (XXX)
+ AMisc :: String -> Ann a
+
+------------------------------------------------------------------------}}}
+{- * Type System -} -- {{{
+
+-- | Data level representation of K3 types, indexed by equivalent type in
+-- Haskell.
+class K3Ty (r :: * -> *) where
+ -- | Attach an annotation to a type
+ tAnn :: r a -> [Ann a] -> r a
+
+ tAddress :: r AddrIx
+ tBool :: r Bool
+ tByte :: r Word8
+ tFloat :: r Float
+ tInt :: r Int
+ tString :: r String
+ tUnit :: r ()
+
+ -- tPair :: r a -> r b -> r (a,b)
+ tMaybe :: r a -> r (Maybe a)
+ tRef :: r a -> r (Ref r' a)
+ tColl :: (K3BaseTy a) => CollTy c -> r a -> r (CTE r' c a)
+ tFun :: (K3BaseTy a, K3BaseTy b) => r a -> r b -> r (a -> b)
+
+ -- XXX TUPLES
+ -- tTuple :: (RTupled rt, RTR rt ~ r, RTE rt ~ t) => rt -> r t
+ tTuple2 :: (r a, r b) -> r (a,b)
+ tTuple3 :: (r a, r b, r c) -> r (a,b,c)
+ tTuple4 :: (r a, r b, r c, r d) -> r (a,b,c,d)
+ tTuple5 :: (r a, r b, r c, r d, r e) -> r (a,b,c,d,e)
+
+ tHL :: HRList r a -> r (HList a)
+
+-- | Universal typeclass wrapper for K3Ty
+--
+-- Often, especially in 'eLam', we need some representation-agnostic proof
+-- of type, so we use this.
+newtype UnivTyRepr (a :: *) = UTR { unUTR :: forall r . (K3Ty r) => r a }
+
+instance K3Ty UnivTyRepr where
+ tAnn (UTR t) s = UTR $ tAnn t s
+
+ tAddress = UTR tAddress
+ tBool = UTR tBool
+ tByte = UTR tByte
+ tFloat = UTR tFloat
+ tInt = UTR tInt
+ tString = UTR tString
+ tUnit = UTR tUnit
+
+ tColl c (UTR a) = UTR $ tColl c a
+ tFun (UTR a) (UTR b) = UTR $ tFun a b
+ tMaybe (UTR a) = UTR $ tMaybe a
+ tRef (UTR a) = UTR $ tRef a
+
+ -- XXX TUPLES
+ -- tTuple us = UTR $ tTuple $ tupleopRS unUTR us
+ tTuple2 us = UTR $ tTuple2 $ tupleopRS unUTR us
+ tTuple3 us = UTR $ tTuple3 $ tupleopRS unUTR us
+ tTuple4 us = UTR $ tTuple4 $ tupleopRS unUTR us
+ tTuple5 us = UTR $ tTuple5 $ tupleopRS unUTR us
+
+ tHL us = UTR $ tHL $ hrlmap unUTR us
------------------------------------------------------------------------}}}
{- * Numeric Autocasting -} -- {{{
------------------------------------------------------------------------}}}
{- * Values and Expressions -} -- {{{
+-- | Data level representation of K3 expression, indexed by equivalent
+-- type in Haskell.
class K3 (r :: * -> *) where
- -- | A representation-specific constraint for collections, on functions
- -- which need to dispatch on a type-tag in the output.
- type K3AST_Coll_C r (c :: CKind) :: Constraint
-
- -- | A representation-specific constraint on handling patterns, on any
- -- function which uses patterns.
- type K3AST_Pat_C r (w :: PKind) :: Constraint
-
- -- | A representation-specific constraint for slices, on eSlice.
- type K3AST_Slice_C r (w :: PKind) :: Constraint
-- | Add a comment to some part of the AST
cComment :: String -> r a -> r a
-- | Add some annotations to some part of the AST
cAnn :: r a -> [Ann a] -> r a
- -- XXX An escape hatch
- --
- -- The K3 AST has this but uses it for wildcards in slices, which
- -- we handle with SKUnk/SUnk.
- -- cUnk :: r a
-
cAddress :: AddrIx -> r AddrIx
cBool :: Bool -> r Bool
cByte :: Word8 -> r Word8
cString :: String -> r String
cUnit :: r ()
- eVar :: VarIx -> UnivTyRepr a -> r a
+ -- | Reference the given variable (and promise that it has type 'a')
+ --
+ -- XXX replace with something more like declvar so that, in theory, a
+ -- sufficiently smart "r" might know what to do about it?
+ --
+ -- We might also want an eLocalVar :: VarIx -> UnivTyRepr a -> r (Ref a)
+ -- to get something like "The K3 Way" of doing local variables?
+ unsafeVar :: VarIx -> UnivTyRepr a -> r a
eJust :: r a -> r (Maybe a)
+ eRef :: r a -> r (Ref r a)
-- XXX TUPLES
eTuple2 :: (r a, r b) -> r (a,b)
eTuple3 :: (r a, r b, r c) -> r (a,b,c)
- eTuple4 :: (r a, r b, r c,r d) -> r (a,b,c,d)
+ eTuple4 :: (r a, r b, r c, r d) -> r (a,b,c,d)
+ eTuple5 :: (r a, r b, r c, r d, r e) -> r (a,b,c,d,e)
-- eTuple :: K3RTuple r a -> r a
- eEmpty :: (K3AST_Coll_C r c) => r (CTE r c e)
- eSing :: (K3AST_Coll_C r c) => r e -> r (CTE r c e)
+ eHL :: HRList r a -> r (HList a)
+
+ eEmpty :: (K3_Coll_C r c) => r (CTE r c e)
+ eSing :: (K3_Coll_C r c) => r e -> r (CTE r c e)
eCombine :: r (CTE r c e) -> r (CTE r c e) -> r (CTE r c e)
eRange :: r Int -> r Int -> r Int -> r (CTE r c Int)
-- (1,2) vs (\(x,y) -> eTuple2 (x,y)) (1,2): the former has a HOAS lambda
-- of type (r (a,b) -> r (a,b)) while the latter has ((r a, r b) -> r
-- (a,b)).
- eLam :: (K3AST_Pat_C r w, Pat UnivTyRepr w, K3BaseTy (PatTy w))
- => PatDa w -> (PatReprFn r w -> r b) -> r (PatTy w -> b)
+ eLam :: (K3_Pat_C r w, Pat UnivTyRepr w, K3BaseTy (PatTy r w))
+ => PatDa w -> (PatReprFn r w -> r b) -> r (PatTy r w -> b)
+
+ -- | Apply
eApp :: r (a -> b) -> r a -> r b
+ -- | Sequence a series of side-effectful statements. Compare 'sequence_'
eBlock :: [r ()] -> r a -> r a
+ -- | Apply a side-effecting function for each element of a collection.
+ -- Compare 'mapM_'
eIter :: r (t -> ()) -> r (CTE r c t) -> r ()
+ -- | If-Then-Else
eITE :: r Bool -> r a -> r a -> r a
eMap :: r (t -> t') -> r (CTE r c t) -> r (CTE r c t')
eFlatten :: r (CTE r c (CTE r c' t)) -> r (CTE r c' t)
- -- | Called Aggregate in K3's AST
+ -- | Fold over a collection. Note that collection ordering is not
+ -- always well-defined; this should probably be used only with associative
+ -- and commutative reducers.
eFold :: r ((t', t) -> t') -> r t' -> r (CTE r c t) -> r t'
-- | Group-By-Aggregate.
eGBA :: r (t -> t'') -- ^ Partitioner
-> r ((t',t) -> t') -- ^ Folder
-> r t' -- ^ Zero for each partition
- -> r (CTE r c t) -- ^ Input collection
+ -> r (CTE r c t) -- ^ Input collection
-> r (CTE r c (t'',t'))
- eSort :: r (CTE r c t) -- ^ Input collection
+ -- | Sort a collection into a list.
+ eSort :: r (CTE r c t) -- ^ Input collection
-> r ((t,t) -> Bool) -- ^ Less-or-equal
-> r (CTE r 'CList t)
--
-- Rather like lambdas, except that the witness is also
-- a mandatory part of the definition of "slice" :)
- eSlice :: (K3AST_Slice_C r w, Pat r w, PatTy w ~ t)
+ eSlice :: (K3_Slice_C r w, Pat r w, PatTy r w ~ t)
=> PatDa w -- ^ Slice specification
-> r (CTE r c t) -- ^ Input collection
-> r (CTE r c t)
eInsert :: r (CTE r c t) -> r t -> r ()
eDelete :: r (CTE r c t) -> r t -> r ()
+
+ -- | Replace an element with another in a collection.
+ --
+ -- XXX What does this do on 'CTBag'?
eUpdate :: r (CTE r c t) -> r t -> r t -> r ()
+ -- | Assign to a reference.
+ --
+ -- Note that dereference is done by a lambda pattern. See Automation's
+ -- 'deref'.
eAssign :: r (Ref r t) -> r t -> r ()
- eDeref :: r (Ref r t) -> r t
+ -- | Send a function and data to another node.
+ --
+ -- XXX Is there any way to refer to "self" as an addrix?
+ --
+ -- XXX Are there restrictions on the functions that can be sent (do they
+ -- have to be declarations)? If so, can we expose that by the type
+ -- system?
eSend :: r AddrIx -> r (a -> ()) -> r a -> r ()
------------------------------------------------------------------------}}}
{- * Miscellany -} -- {{{
- -- XXX does not enumerate local variables
-data Decl tr r t = Decl VarIx (tr t) (Maybe (r t))
-
-- | A convenience function for setting the type of a collection.
--
-- Use as (eEmpty `asColl` CTSet)
asColl :: r (CTE r c t) -> CollTy c -> r (CTE r c t)
asColl = const
+-- | A top-level declaration.
+--
+-- XXX does not enumerate local variables
+data Decl tr r t = Decl VarIx (tr t) (Maybe (r t))
+
+-- | Capture a type-constructor as data.
+data RCons (r :: * -> *) = RCons
+
+-- | A utility for setting the type of sub-components of a declaration, by
+-- constraining polymorphism. Use the 'asCollR' and 'asRefR' combinators
+-- to avail yourself of the RCons passed in.
+mkdecl :: (RCons r -> Decl tr r t) -> Decl tr r t
+mkdecl f = f RCons
+
+-- | Define a fixed-point declaration. Like mkdecl, it continues to assist
+-- in constraining polymorphism, but also yields a representation of the
+-- declaration being made.
+--
+-- Note that this relies on laziness in Haskell it pulls out the name and
+-- type fields of the Decl being built to construct a K3 AST variable to
+-- refer to the current definition.
+mkfdecl :: (K3 r, K3Ty trx)
+ => (RCons r -> r t -> (forall tr . (K3Ty tr) => Decl tr r t))
+ -> Decl trx r t
+mkfdecl f = let self = (\(Decl n tr _) -> unsafeVar n tr) (f RCons self)
+ in f RCons self
+
+-- | Ensure that the representation type of a collection matches
+--
+-- This is probably most useful when s is a K3Ty and r is a K3, but this may
+-- be more generally applicable.
+asCollR :: s (CTE r c t) -> RCons r -> s (CTE r c t)
+asCollR = const
+
+-- | Ensure that the representation type of a ref matches
+asRefR :: r' (Ref r t) -> RCons r -> r' (Ref r t)
+asRefR = const
+
------------------------------------------------------------------------}}}
-- * Automated derivation of data from types, where possible
K3AutoColl, autocoll, K3AutoTy, autoty,
+ -- * Pattern handling
+ autopv,
+
-- * K3 macro library
- macro_localVar, macro_caseMaybe, macro_emptyPeek
+ localVar, caseMaybe, emptyPeek, deref, combMany
) where
import Data.Word
import Dyna.BackendK3.AST
+import Dyna.XXX.THTuple
------------------------------------------------------------------------}}}
-- Automate collection type {{{
--
-- Note that this only works once the type has become monomorphic;
-- otherwise it imposes a constraint on the haskell tyvar.
--- (This is a total function)
+-- (This should be a total function)
class K3AutoColl (c :: CKind) where autocoll :: CollTy c
instance K3AutoColl CBag where autocoll = CTBag
instance K3AutoColl CList where autocoll = CTList
--
-- Note that this only works once the type has become monomorphic;
-- otherwise it imposes a constraint on the haskell tyvar.
--- (This is a total function)
+-- (This should be a total function)
class K3AutoTy a where autoty :: UnivTyRepr a
instance K3AutoTy Bool where autoty = tBool
instance K3AutoTy Word8 where autoty = tByte
autoty = tColl autocoll autoty
instance (K3AutoTy a) => K3AutoTy (Maybe a) where autoty = tMaybe autoty
instance (K3AutoTy a) => K3AutoTy (Ref r a) where autoty = tRef autoty
-instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a -> b) where
+instance (K3AutoTy a, K3BaseTy a, K3AutoTy b, K3BaseTy b)
+ => K3AutoTy (a -> b) where
autoty = tFun autoty autoty
+ -- HList derivation
+class K3AutoTyHL (a :: [*]) where autotyhl :: HRList UnivTyRepr a
+instance K3AutoTyHL '[] where autotyhl = HRN
+instance (K3AutoTy a, K3AutoTyHL as)
+ => K3AutoTyHL (a ': as) where autotyhl = autoty :++ autotyhl
+
+instance K3AutoTyHL a
+ => K3AutoTy (HList a) where autoty = tHL autotyhl
+
-- XXX TUPLES
instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a,b)
where autoty = tTuple2 (autoty, autoty)
-
instance (K3AutoTy a, K3AutoTy b, K3AutoTy c) => K3AutoTy (a,b,c)
where autoty = tTuple3 (autoty, autoty, autoty)
+instance (K3AutoTy a, K3AutoTy b, K3AutoTy c, K3AutoTy d) => K3AutoTy (a,b,c,d)
+ where autoty = tTuple4 (autoty, autoty, autoty, autoty)
{-
class (Pat (PKTup ws), PatTy (PKTup ws) ~ a) => K3AutoTyTup ws a
=> K3AutoTy (a,b)
where autoty = tTuple autotytup
-}
-
+
+------------------------------------------------------------------------}}}
+{- * Automate pattern -} -- XXX {{{
+
+{-
+-- | Automatically derive a pattern, for use with eLam.
+-- Note that this is only useful for the (common) case of not using Just
+-- patterns.
+
+class (Pat UnivTyRepr w) => K3AutoPat (w :: PKind) where
+ autopat :: PatDa w
+
+instance (K3BaseTy a, K3AutoTy a) => K3AutoPat (PKVar UnivTyRepr a) where
+ autopat = PVar autoty
+
+class UFAP (w :: [PKind]) where unfoldautopat :: HList (MapPatDa w)
+instance UFAP '[] where unfoldautopat = HN
+
+instance (UnPatDa (PatDa a) ~ a, K3AutoPat a,
+ UFAP as, MapPatDa (a ': as) ~ (PatDa a ': (MapPatDa as))
+ )
+ => UFAP (a ': as) where unfoldautopat = (autopat :: PatDa a)
+ :+ (unfoldautopat :: HList (MapPatDa as))
+
+instance (UnPatDa (PatDa a) ~ a, K3AutoPat a,
+ UnPatDa (PatDa b) ~ b, K3AutoPat b)
+ => UFAP '[a,b] where unfoldautopat = (autopat :: PatDa a)
+ :+ (autopat :: PatDa b)
+ :+ HN
+instance (K3AutoTy a, UFAP ts)
+ => K3AutoPat (PKTup ts) where
+ autopat = hlTuple $ unfoldautopat
+
+-}
+
+autopv :: (K3AutoTy a) => PatDa (PKVar UnivTyRepr a)
+autopv = PVar autoty
+
------------------------------------------------------------------------}}}
-- K3 Macro Library (XXX WIP) {{{
-- | Let as lambda
-macro_localVar :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKVar UnivTyRepr a))
- => UnivTyRepr a
- -> (r a)
- -> (r a -> r b)
- -> r b
-macro_localVar w a b = eApp (eLam (PVar w) b) a
+localVar :: (K3 r, K3AutoTy a, K3BaseTy a, K3_Pat_C r (PKVar UnivTyRepr a))
+ => (r a)
+ -> (r a -> r b)
+ -> r b
+localVar a b = eApp (eLam autopv b) a
+
+{-
+-- | Let as lambda with explicit type variable
+localVar' :: (K3 r, K3BaseTy a, K3_Pat_C r (PKVar UnivTyRepr a))
+ => UnivTyRepr a
+ -> (r a)
+ -> (r a -> r b)
+ -> r b
+localVar' w a b = eApp (eLam (PVar w) b) a
+-}
-- | Case analyze a Maybe
-macro_caseMaybe :: (K3 r, K3BaseTy a,
- K3AST_Pat_C r (PKJust (PKVar UnivTyRepr a)))
- => UnivTyRepr a
- -> r (Maybe a)
- -> r b
- -> (r a -> r b)
- -> r b
-macro_caseMaybe w m n b = eITE (eEq m cNothing)
+caseMaybe :: (K3 r, K3BaseTy a,
+ K3_Pat_C r (PKJust (PKVar UnivTyRepr a)))
+ => UnivTyRepr a
+ -> r (Maybe a)
+ -> r b
+ -> (r a -> r b)
+ -> r b
+caseMaybe w m n b = eITE (eEq m cNothing)
n
(eApp (eLam (PJust (PVar w)) b) m)
-- | Case analyze a collection as either empty or a peeked element
-macro_emptyPeek :: (K3AST_Coll_C r c,
- K3AST_Pat_C r (PKVar UnivTyRepr a),
- K3 r, K3BaseTy a, K3AutoTy a)
- => r (CTE r c a) -> r b -> (r a -> r b) -> r b
-macro_emptyPeek c e l = eITE (eEq c eEmpty)
+emptyPeek :: (K3_Coll_C r c,
+ K3_Pat_C r (PKVar UnivTyRepr a),
+ K3 r, K3BaseTy a, K3AutoTy a)
+ => r (CTE r c a) -> r b -> (r a -> r b) -> r b
+emptyPeek c e l = eITE (eEq c eEmpty)
e
(eApp (eLam (PVar autoty) l) $ ePeek c)
+-- | Dereference a value by using a Ref pattern on a lambda.
+deref :: (K3_Pat_C r (PKRef (PKVar UnivTyRepr a)),
+ K3AutoTy a, K3BaseTy a, K3 r)
+ => r (Ref r a) -> r a
+deref = eApp (eLam (PRef $ PVar autoty) id)
+
+-- | Combine many things
+combMany :: (K3_Coll_C r c, K3 r) => [r a] -> r (CTE r c a)
+combMany = foldr (\e c -> eCombine c (eSing e)) eEmpty
+
------------------------------------------------------------------------}}}
-- Collect variables in a term (XXX TODO) {{{
-- | Provides the "AsK3" type and instances for the K3 AST.
-- Header material {{{
+{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
-module Dyna.BackendK3.Render where
+module Dyna.BackendK3.Render (
+ -- * K3 implementations
+ AsK3Ty(..), AsK3(..),
+
+ -- * Utility functions
+ sh, sht, shd
+) where
import Control.Monad.Identity
+import Control.Monad.Reader
import Control.Monad.State
import qualified Data.List as DL
import Text.PrettyPrint.Free
import Dyna.BackendK3.AST
+import Dyna.XXX.HList
import Dyna.XXX.MonadUtils
import Dyna.XXX.THTuple
import qualified Language.Haskell.TH as TH
-------------------------------------------------------------------------}}}
-{- * Annotations -} -- {{{
-
-annText :: Ann a -> Doc e
-annText AAtomic = "atomic"
-annText AOneOf = "oneof"
-annText (AMisc s) = text s
-annText (AFunDep fs) = let x = tupleopEL (fdscast) fs
- in let (dom,cod) = (DL.elemIndices FDDom x
- ,DL.elemIndices FDCod x)
- in (tupled $ map pretty dom)
- <+> "->"
- <+> (tupled $ map pretty cod)
- where
- fdscast FDIrr = FDIrr
- fdscast FDDom = FDDom
- fdscast FDCod = FDCod
-
-------------------------------------------------------------------------}}}
-{- * Type handling -} -- {{{
-
--- | Unlike AsK3 below, we don't need to thread a variable counter
--- around since K3 doesn't have tyvars
-newtype AsK3Ty e (a :: *) = AsK3Ty { unAsK3Ty :: Doc e }
-
-instance K3Ty (AsK3Ty e) where
- tAnn (AsK3Ty e) anns = AsK3Ty$ align $
- e </> "@" <+> (encloseSep lbrace rbrace comma $ map annText anns)
-
- tAddress = AsK3Ty$ "address"
- tBool = AsK3Ty$ "bool"
- tByte = AsK3Ty$ "byte"
- tFloat = AsK3Ty$ "float"
- tInt = AsK3Ty$ "int"
- tString = AsK3Ty$ "string"
- tUnit = AsK3Ty$ "unit"
-
- -- tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
-
- tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> ta
-
- tColl CTSet (AsK3Ty ta) = AsK3Ty$ braces ta
- tColl CTBag (AsK3Ty ta) = AsK3Ty$ encBag ta
- tColl CTList (AsK3Ty ta) = AsK3Ty$ brackets ta
-
- tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta `above` ("->" <+> tb)
-
- tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
-
- -- XXX TUPLES Note the similarities!
- tTuple2 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
- tTuple3 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
- tTuple4 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
- tTuple5 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
------------------------------------------------------------------------}}}
-- Collection handling {{{
-- Pattern handling {{{
class (Pat UnivTyRepr w) => K3PFn w where
- k3pfn :: PatDa w -> State Int (Doc e, PatReprFn (AsK3 e) w)
+ -- | Turn a pattern into two parts: the string to be placed after the
+ -- \ in the K3 code and the constitutent pieces to be passed into the
+ -- HOAS function given to eLam
+ k3pfn :: PatDa w -> ReaderT Bool (State Int) (Doc e, PatReprFn (AsK3 e) w)
+
+rec_k3pfn :: (K3PFn w)
+ => PatDa w
+ -> ReaderT Bool (State Int) (Doc e, PatReprFn (AsK3 e) w)
+rec_k3pfn = local (const False) . k3pfn
instance (K3BaseTy a) => K3PFn (PKVar UnivTyRepr (a :: *)) where
k3pfn (PVar (tr :: UnivTyRepr a)) = do
- n <- incState
+ n <- lift incState
let sn = text $ "x" ++ show n
return (sn <> colon <> unAsK3Ty (unUTR tr)
,AsK3$ const$ sn)
+instance (K3BaseTy a) => K3PFn (PKUnk (a :: *)) where
+ k3pfn PUnk = return ("_", ())
+
instance (K3PFn w) => K3PFn (PKJust w) where
k3pfn (PJust w) = do
- (p, r) <- k3pfn w
- return ("just " <> parens p, r)
+ (p,r) <- rec_k3pfn w
+ return ("just" <+> parens p, r)
+
+instance (K3PFn w) => K3PFn (PKRef w) where
+ k3pfn (PRef w) = rec_k3pfn w
+
+instance K3PFn (PKHL '[]) where
+ k3pfn HN = ask >>= \f -> return (if f then "" else "()", HN)
+
+instance (K3PFn w, K3PFn (PKHL ws), MapPatConst ws UnivTyRepr)
+ => K3PFn (PKHL (w ': ws)) where
+ k3pfn (w :+ ws) = do
+ (pw,rw) <- k3pfn w
+ (ps,rs) <- local (const True) $ k3pfn ws
+ p <- asks (\f -> (if f then (comma <>) else parens) (pw <> ps))
+ let r = rw :+ rs
+ return (p,r)
-instance (K3BaseTy a) => K3PFn (PKUnk (a :: *)) where
- k3pfn PUnk = return ("_", cUnit)
------------------------------------------------------------------------}}}
-- Slice handling {{{
class (Pat (AsK3 e) w) => K3SFn e w where
- k3sfn :: PatDa w -> Identity (AsK3 e (PatTy w))
+ -- | Print a pattern
+ k3sfn :: PatDa w -> Reader Bool (AsK3 e (PatTy (AsK3 e) w))
+
+rec_k3sfn :: (K3SFn e w)
+ => PatDa w
+ -> Reader Bool (AsK3 e (PatTy (AsK3 e) w))
+rec_k3sfn = local (const False) . k3sfn
instance (K3BaseTy a) => K3SFn e (PKVar (AsK3 e) (a :: *)) where
k3sfn (PVar r) = return r
k3sfn PUnk = return $ AsK3$ const$ text "_"
instance (K3SFn e s) => K3SFn e (PKJust s) where
- k3sfn (PJust s) = return $ AsK3$ \n -> "Just"
- <> parens (unAsK3 (runIdentity $ k3sfn s) n)
+ k3sfn (PJust s) = do
+ p <- rec_k3sfn s
+ return $ AsK3$ \n -> "just" <> parens (unAsK3 p n)
+
+instance K3SFn e (PKHL '[]) where
+ k3sfn HN = asks (\f -> AsK3$ const$ if f then "" else "()")
+
+instance (K3SFn e w, K3SFn e (PKHL ws), MapPatConst ws (AsK3 e))
+ => K3SFn e (PKHL (w ': ws)) where
+ k3sfn (w :+ ws) = do
+ pw <- k3sfn w
+ ps <- local (const True) $ k3sfn ws
+ fn <- asks (\f -> (if f then (comma <>) else parens))
+ return$ AsK3$ \n -> fn $ (unAsK3 pw n) <> (unAsK3 ps n)
+
+------------------------------------------------------------------------}}}
+{- * Annotations -} -- {{{
+
+fdscast :: FunDepSpec a -> FunDepSpec b
+fdscast FDIrr = FDIrr
+fdscast FDDom = FDDom
+fdscast FDCod = FDCod
+
+annfds :: (RTupled fs, RTR fs ~ FunDepSpec)
+ => Doc e -> fs -> Doc e
+annfds op fs =
+ let x = tupleopEL (fdscast) fs
+ (dom,cod) = (DL.elemIndices FDDom x
+ ,DL.elemIndices FDCod x)
+ in (tupled $ map pretty dom)
+ <+> op
+ <+> (tupled $ map pretty cod)
+
+annfdshl :: Doc e -> HRList FunDepSpec a -> Doc e
+annfdshl op fs =
+ let x = hrlproj (fdscast) fs
+ (dom,cod) = (DL.elemIndices FDDom x
+ ,DL.elemIndices FDCod x)
+ in (tupled $ map pretty dom)
+ <+> op
+ <+> (tupled $ map pretty cod)
+
+
+annText :: Ann a -> Doc e
+annText AAtomic = "atomic"
+annText (AFunDep fs) = annfds "->" fs
+annText (AFunDepHL fs) = annfdshl "->" fs
+annText (AIndex fs) = annfds "=>" fs
+annText (AIndexHL fs) = annfdshl "=>" fs
+annText AOneOf = "oneof"
+annText AOneOfHL = "oneof"
+annText (AMisc s) = text s
+
+------------------------------------------------------------------------}}}
+{- * Type handling -} -- {{{
+
+-- | Produce a textual representation of a K3 type
+--
+-- Unlike AsK3 below, we don't need to thread a variable counter
+-- around since K3 doesn't have tyvars
+newtype AsK3Ty e (a :: *) = AsK3Ty { unAsK3Ty :: Doc e }
+
+instance K3Ty (AsK3Ty e) where
+ tAnn (AsK3Ty e) anns = AsK3Ty$ align $
+ e </> "@" <+> (encloseSep lbrace rbrace comma $ map annText anns)
+
+ tAddress = AsK3Ty$ "address"
+ tBool = AsK3Ty$ "bool"
+ tByte = AsK3Ty$ "byte"
+ tFloat = AsK3Ty$ "float"
+ tInt = AsK3Ty$ "int"
+ tString = AsK3Ty$ "string"
+ tUnit = AsK3Ty$ "unit"
+
+ -- tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
+
+ tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> ta
+
+ tColl CTSet (AsK3Ty ta) = AsK3Ty$ braces ta
+ tColl CTBag (AsK3Ty ta) = AsK3Ty$ encBag ta
+ tColl CTList (AsK3Ty ta) = AsK3Ty$ brackets ta
+ tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta `above` ("->" <+> tb)
+
+ tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
+
+ -- XXX TUPLES Note the similarities!
+ tTuple2 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
+ tTuple3 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
+ tTuple4 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
+ tTuple5 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
+
+ tHL us = AsK3Ty $ tupled $ hrlproj unAsK3Ty us
------------------------------------------------------------------------}}}
-- Expression handling {{{
+-- | Produce a textual representation of a K3 expression
newtype AsK3 e (a :: *) = AsK3 { unAsK3 :: Int -> Doc e }
+type instance K3_Coll_C (AsK3 e) c = K3CFn c
+type instance K3_Pat_C (AsK3 e) p = K3PFn p
+type instance K3_Slice_C (AsK3 e) s = K3SFn e s
+
instance K3 (AsK3 e) where
- type K3AST_Coll_C (AsK3 e) c = K3CFn c
- type K3AST_Pat_C (AsK3 e) p = K3PFn p
- type K3AST_Slice_C (AsK3 e) s = K3SFn e s
cAnn (AsK3 e) anns = AsK3$ \n -> align $
parens (e n) <> " @ "
cNothing = AsK3$ const$ "nothing"
cUnit = AsK3$ const$ "unit"
- eVar (Var v) _ = AsK3$ const$ text v
+ unsafeVar (Var v) _ = AsK3$ const$ text v
- eJust (AsK3 a) = builtin "Just " [ a ]
- -- ePair (AsK3 a) (AsK3 b) = AsK3$ \n -> tupled [a n, b n]
+ eJust (AsK3 a) = builtin "just" [ a ]
+ eRef (AsK3 a) = builtin "ref" [ a ]
-- XXX TUPLES Note the similarity of these!
eTuple2 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t
eTuple3 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t
eTuple4 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t
+ eTuple5 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t
+
+ eHL t = AsK3 $ \n -> tupled $ hrlproj (flip unAsK3 n) t
eEmpty = k3cfn_empty
eSing = k3cfn_sing
eLeq = binop "<="
eNeq = binop "!="
- eLam w f = AsK3$ \n -> let ((pat, arg),n') = runState (k3pfn w) n
+ eLam w f = AsK3$ \n -> let ((pat, arg),n') = runState (runReaderT (k3pfn w) False) n
in "\\" <> pat <+> "->" `above` indent 2 (unAsK3 (f arg) n')
eApp (AsK3 f) (AsK3 x) = AsK3$ \n ->
eSort (AsK3 c) (AsK3 f) = builtin "sort" [ c, f ]
ePeek (AsK3 c) = builtin "peek" [ c ]
- eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (runIdentity $ k3sfn w) n)
+ eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (runReader (k3sfn w) False) n)
eInsert (AsK3 c) (AsK3 e) = builtin "insert" [ c, e ]
eDelete (AsK3 c) (AsK3 e) = builtin "delete" [ c, e ]
eUpdate (AsK3 c) (AsK3 o) (AsK3 n) = builtin "update" [ c, o, n ]
eAssign = binop "<-"
- eDeref (AsK3 r) = builtin "deref" [ r ]
- -- XXX that doesn't seem to actually be right!
eSend (AsK3 a) (AsK3 f) (AsK3 x) = builtin "send" [ a, f, x ]
show (AsK3 f) = show $ f 0
sh :: AsK3 e a -> Doc e
-sh (AsK3 f) = f 0
+sh f = unAsK3 f 0
instance Show (AsK3Ty e a) where
show (AsK3Ty f) = show f
-sht :: AsK3Ty e a -> String
-sht = show
+sht :: AsK3Ty e a -> Doc e
+sht = unAsK3Ty
shd :: Decl (AsK3Ty e) (AsK3 e) t -> Doc e
shd (Decl (Var name) tipe body) =
-- Template Haskell splices {{{
$(mkLRecInstances (''K3PFn,[]) 'PKTup
- ('k3pfn,Nothing,\ls -> TH.tupE [
+ ('k3pfn,'rec_k3pfn,Nothing,\ls -> TH.tupE [
TH.appE (TH.varE 'tupled)
$ TH.listE
$ map (TH.appE (TH.varE 'fst)) ls
e <- liftM TH.varT $ TH.newName "e"
n <- TH.newName "n"
mkLRecInstances (''K3SFn,[e]) 'PKTup
- ('k3sfn,Nothing,\ls ->
+ ('k3sfn,'rec_k3sfn,Nothing,\ls ->
TH.appE (TH.conE 'AsK3)
$ TH.lamE [TH.varP n]
$ TH.appE (TH.varE 'tupled)
projects / dyna2 / commitdiff