From: Nathaniel Wesley Filardo Date: Tue, 23 Oct 2012 21:17:23 +0000 (-0400) Subject: A whole host of changes X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=fdf04e524ffb28c53d5b8baa9f7bb4d49a5a46df;p=dyna2 A whole host of changes Inspired by several days of hacking on the CKY example and thinking about how we're going to actually produce those ASTs. > Factors out HLists and pushes their utility through BackendK3. > Adds export annotations to BackendK3.AST and .Render > More documentation across the board --- diff --git a/dyna.cabal b/dyna.cabal index 4f74573..b2fd934 100644 --- a/dyna.cabal +++ b/dyna.cabal @@ -31,6 +31,8 @@ Library Dyna.BackendK3.Render Dyna.ParserHS.Parser, Dyna.NormalizeParse, + Dyna.XXX.HList, + Dyna.XXX.THTuple, Dyna.XXX.Trifecta Build-Depends: base >=4, diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs index 872b0fb..032cdc4 100644 --- a/src/Dyna/BackendK3/AST.hs +++ b/src/Dyna/BackendK3/AST.hs @@ -3,6 +3,14 @@ -- -- 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 #-} @@ -13,91 +21,61 @@ {-# 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 @@ -106,87 +84,63 @@ instance K3BaseTy Float 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 @@ -194,69 +148,103 @@ data PKind where -- 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) @@ -264,12 +252,165 @@ type family MapPatConst (x :: [PKind]) (r :: * -> *) :: Constraint 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 -} -- {{{ @@ -320,29 +461,15 @@ instance BiNum Float Int where ------------------------------------------------------------------------}}} {- * 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 @@ -352,18 +479,29 @@ class K3 (r :: * -> *) where 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) @@ -384,14 +522,20 @@ class K3 (r :: * -> *) where -- (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') @@ -399,7 +543,9 @@ class K3 (r :: * -> *) where 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. @@ -410,10 +556,11 @@ class K3 (r :: * -> *) where 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) @@ -430,30 +577,79 @@ class K3 (r :: * -> *) where -- -- 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 + ------------------------------------------------------------------------}}} diff --git a/src/Dyna/BackendK3/Automation.hs b/src/Dyna/BackendK3/Automation.hs index 28453e7..3252229 100644 --- a/src/Dyna/BackendK3/Automation.hs +++ b/src/Dyna/BackendK3/Automation.hs @@ -23,12 +23,16 @@ module Dyna.BackendK3.Automation ( -- * 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 {{{ @@ -38,7 +42,7 @@ import Dyna.BackendK3.AST -- -- 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 @@ -51,7 +55,7 @@ instance K3AutoColl CSet where autocoll = CTSet -- -- 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 @@ -63,15 +67,26 @@ instance (K3AutoColl c, K3AutoTy a, K3BaseTy a) => K3AutoTy (CTE r c a) where 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 @@ -88,39 +103,95 @@ instance (K3AutoTyTup (wa ': w) (a,b), K3AutoTyTup w b) => 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) {{{ diff --git a/src/Dyna/BackendK3/Render.hs b/src/Dyna/BackendK3/Render.hs index 440b8f1..a24acf7 100644 --- a/src/Dyna/BackendK3/Render.hs +++ b/src/Dyna/BackendK3/Render.hs @@ -2,6 +2,7 @@ -- | Provides the "AsK3" type and instances for the K3 AST. -- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -13,74 +14,30 @@ {-# 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 {{{ @@ -105,28 +62,58 @@ instance K3CFn CBag where -- 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 @@ -135,19 +122,111 @@ instance (K3BaseTy a) => K3SFn e (PKUnk (a :: *)) where 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) <> " @ " @@ -165,16 +244,19 @@ instance K3 (AsK3 e) where 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 @@ -190,7 +272,7 @@ instance K3 (AsK3 e) where 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 -> @@ -214,15 +296,13 @@ instance K3 (AsK3 e) where 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 ] @@ -246,13 +326,13 @@ instance Show (AsK3 e a) where 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) = @@ -268,7 +348,7 @@ 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 @@ -280,7 +360,7 @@ $(do 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) diff --git a/src/Dyna/BackendK3/Selftest.hs b/src/Dyna/BackendK3/Selftest.hs index 83a8157..6da9711 100644 --- a/src/Dyna/BackendK3/Selftest.hs +++ b/src/Dyna/BackendK3/Selftest.hs @@ -61,7 +61,7 @@ case_mcm = e @=? render k3 where e = "if ((test) == (nothing)) then (0) " <> "else (((\\just (x0:int) -> x0) (test)))" - k3 = macro_caseMaybe tInt (eVar (Var "test") autoty) (cInt 0) (id) + k3 = caseMaybe tInt (unsafeVar (Var "test") autoty) (cInt 0) (id) ------------------------------------------------------------------------}}} -- Harness toplevel {{{ diff --git a/src/Dyna/XXX/HList.hs b/src/Dyna/XXX/HList.hs new file mode 100644 index 0000000..401cacc --- /dev/null +++ b/src/Dyna/XXX/HList.hs @@ -0,0 +1,67 @@ +--------------------------------------------------------------------------- +-- | HLists using the GHC machinery new in 7.6. + +-- Header material {{{ + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} + +module Dyna.XXX.HList( + HList(..), MapStarConst, hlToHrl, HRList(..), hrlmap, hrlproj +) where + +import GHC.Prim (Constraint) + +------------------------------------------------------------------------}}} +-- Data-level HLists {{{ + +infixr 5 :+ + +-- | A heterogenous list +data HList a where + HN :: HList '[] + (:+) :: a -> HList b -> HList (a ': b) + +instance Show (HList '[]) where show _ = "HN" +instance (Show a, Show (HList as)) => Show (HList (a ': as)) where + show (a :+ as) = show a ++ " :+ " ++ show as + +hlToHrl :: (forall b . b -> r b) -> HList a -> HRList r a +hlToHrl _ HN = HRN +hlToHrl f (a:+as) = f a :++ (hlToHrl f as) + +type family MapStarConst (f :: * -> Constraint) (x :: [*]) :: Constraint +type instance MapStarConst f '[] = () +type instance MapStarConst f (x ': xs) = (f x, MapStarConst f xs) + +infixr 5 :++ + +-- | A heterogenous list in which every element is the image of some +-- type-function @r :: * -> *@. +data HRList r a where + HRN :: HRList r '[] + (:++) :: r a -> HRList r b -> HRList r (a ': b) + +instance Show (HRList r '[]) where show _ = "HRN" +instance (Show (r a), Show (HRList r as)) => Show (HRList r (a ': as)) where + show (a :++ as) = show a ++ " :+ " ++ show as + +-- | Shift the type-function of a HRList +hrlmap :: (forall a . r a -> s a) -> HRList r t -> HRList s t +hrlmap _ HRN = HRN +hrlmap f (a :++ as) = f a :++ (hrlmap f as) + +-- | Eliminate a HRList to a homogenous list +hrlproj :: (forall a . r a -> b) -> HRList r t -> [b] +hrlproj _ HRN = [] +hrlproj f (a :++ as) = f a : (hrlproj f as) + +------------------------------------------------------------------------}}} diff --git a/src/Dyna/XXX/THTuple.hs b/src/Dyna/XXX/THTuple.hs index d257931..f86af45 100644 --- a/src/Dyna/XXX/THTuple.hs +++ b/src/Dyna/XXX/THTuple.hs @@ -6,10 +6,12 @@ -- Header material {{{ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE Rank2Types #-} @@ -39,7 +41,9 @@ module Dyna.XXX.THTuple( mkLRecInstances ) where -import Dyna.XXX.THTupleInternals +import Dyna.XXX.HList +import Dyna.XXX.THTupleInternals +import GHC.Prim (Constraint) ------------------------------------------------------------------------}}} -- Type-level functions {{{ @@ -69,6 +73,12 @@ class (MKLT (TOL base) ~ base) => Tupled base where -- the inverse of MKLT (as asserted by class constraints). type TOL base :: [*] + -- | Send a tuple to an HList + tupleHL :: base -> HList (TOL base) + + -- | Send a HList to a Tuple + hlTuple :: HList (TOL base) -> base + -- | Shed a type constructor tupleopR :: (RTupled rbase, (RTR rbase) ~ r, (RTE rbase) ~ base) => (forall x . r x -> x) -> rbase -> base @@ -99,7 +109,10 @@ class (Tupled (RTE arred), -- Aaaand action {{{ -- Generate instances for Tupled -$(mkTupleInstances ''Tupled ''RTER ''TOL 'tupleopR 'tupleopRS) +$(mkTupleInstances + ''Tupled ''RTER + ''TOL '(:+) 'HN 'tupleHL 'hlTuple + 'tupleopR 'tupleopRS) -- Generate instances for RTupled $(mkRTupleInstances ''RTupled ''RTE ''RTR 'tupleopEL) diff --git a/src/Dyna/XXX/THTupleInternals.hs b/src/Dyna/XXX/THTupleInternals.hs index eb1b2fa..9cb4649 100644 --- a/src/Dyna/XXX/THTupleInternals.hs +++ b/src/Dyna/XXX/THTupleInternals.hs @@ -111,8 +111,7 @@ mkTyUnMap a b c d = foreachTupleSize (mkTyUnMapN a b c d) ------------------------------------------------------------------------}}} -- Make Tuple {{{ -mkTupleInstance :: Name -> Name -> Name -> Name -> Name -> Int -> Q Dec -mkTupleInstance _tc _rter _tol _opr _oprs n | n > 1 = do +mkTupleInstance _tc _rter _tol _hc _hn _thl _lth _opr _oprs n | n > 1 = do -- Build polymorphic variables names <- mkNames n @@ -127,15 +126,24 @@ mkTupleInstance _tc _rter _tol _opr _oprs n | n > 1 = do let fnames = map (appE (varE f) . varE) names let rpa = tupP $ map varP names let frpa = foldl appE (conE $ tupleDataName n) fnames + let lrpa = foldr (\e l -> (conE _hc) `appE` e `appE` l) + (conE _hn) + $ map varE names + let plpa = foldr (\e l -> conP _hc [e,l]) + (conP _hn []) + $ map varP names instanceD (cxt []) (appT (conT _tc) ty) -- where [tySynInstD _rter [ty, vr] $ mkRTy n vr names ,tySynInstD _tol [ty] $ promoteList $ map varT names + ,funD _thl [clause [rpa] (normalB $ lrpa) [] ] + ,funD _lth [clause [plpa] (normalB $ tupE $ map varE names) [] ] ,funD _opr [clause [varP f, rpa] (normalB $ frpa) [] ] ,funD _oprs [clause [varP f, rpa] (normalB $ frpa) [] ] ] -mkTupleInstances a b c d e = foreachTupleSize (mkTupleInstance a b c d e) +mkTupleInstances a b c d e f g h i = + foreachTupleSize (mkTupleInstance a b c d e f g h i) ------------------------------------------------------------------------}}} -- Make RTuple {{{ @@ -222,11 +230,12 @@ mkRecInstances a b c d e = foreachTupleSize (mkRecInstance a b c d e) mkLRecInstance :: (Name, [TypeQ]) -- ^ Class name and args -> Name - -> (Name, Maybe Name, [ExpQ] -> ExpQ) - -- ^ Function, data, and body + -> (Name, Name, Maybe Name, [ExpQ] -> ExpQ) + -- ^ Function, recursive + -- function, data, and body -> Int -- ^ Tuple size -> Q Dec -mkLRecInstance (_cname,_cargs) _tyf (_fn,_mfpn,fm) n = do +mkLRecInstance (_cname,_cargs) _tyf (_fn,_rfn,_mfpn,fm) n = do names <- mkNames n let context = cxt $ map (\na -> classP _cname $ _cargs ++ [varT na]) names let conarg = (appT (conT _tyf) $ promoteList $ map varT names)