import Dyna.XXX.THTuple
------------------------------------------------------------------------}}}
--- Preliminaries {{{
+{- * Preliminaries -} -- {{{
-- XXX
newtype VarIx = Var String
data Ann = Ann [String]
------------------------------------------------------------------------}}}
--- Collections {{{
+{- * Collections -} -- {{{
data CKind = CBag | CList | CSet
CTSet :: CollTy CSet
------------------------------------------------------------------------}}}
--- Effectables (XXX TODO) {{{
+{- * Effectables (XXX TODO) -} -- {{{
{-
data MKind = MKImmut | MKMut
data Ref a = Ref
------------------------------------------------------------------------}}}
--- Type System {{{
+{- * Type System -} -- {{{
-- | Data level representation of K3 types, indexed by equivalent type in
-- Haskell.
$(mkTupleRecInstances ''K3BaseTy [])
------------------------------------------------------------------------}}}
--- Pattern System {{{
+{- * Pattern System -} -- {{{
- -- | Kinds of patterns permitted in K3
+-- | Kinds of patterns permitted in K3
data PKind where
+ -- | Variables in patterns
PKVar :: k -> PKind
+ -- | Wildcards in patterns
+ PKUnk :: k -> PKind
+
-- | Just patterns (fail on Nothing)
--
-- Note the distinction between PatTy and (PatBTy and PatReprFn) here!
-- producing tuples.
PKTup :: [PKind] -> PKind
- -- | Provides witnesses that certain types may be used
- -- as arguments to K3 lambdas. Useful when building
- -- 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.
- --
- -- Essentially, these things determine where "r"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 $ tPair tInt tInt) :: (r (Int, Int) -> _) -> _
- -- eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _
- --
+-- | Provides witnesses that certain types may be used
+-- as arguments to K3 lambdas. Useful when building
+-- 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.
+--
+-- Essentially, these things determine where "r"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 $ tPair tInt tInt) :: (r (Int, Int) -> _) -> _
+-- eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _
+--
class (UnPatDa (PatDa w) ~ w) => Pat (w :: PKind) where
- -- | Any data this witness needs to carry around
+ -- | Any data this witness needs to carry around
data PatDa w :: *
- -- | The type this witness witnesses (i.e. the things matched against)
+ -- | The type this witness witnesses (i.e. the things matched against)
type PatTy w :: *
- -- | The type this witness binds (i.e. after matching is done)
+ -- | The type this witness binds (i.e. after matching is done)
type PatBTy w :: *
- -- | The type of this pattern.
+ -- | The type of this pattern.
type PatReprFn (r :: * -> *) w :: *
type family UnPatDa (pd :: *) :: PKind
type PatBTy (PKVar a) = a
type PatReprFn r (PKVar a) = r a
+instance (K3BaseTy a) => Pat (PKUnk (a :: *)) where
+ data PatDa (PKUnk a) = PUnk
+ type PatTy (PKUnk a) = a
+ type PatBTy (PKUnk a) = ()
+ type PatReprFn r (PKUnk a) = r ()
+
instance (Pat w) => Pat (PKJust w) where
data PatDa (PKJust w) = PJust (PatDa w)
type PatTy (PKJust w) = Maybe (PatTy w)
type PatReprFn r (PKTup ts) = MapPatReprFn r ts
------------------------------------------------------------------------}}}
--- Slice System {{{
+{- * Slice System -} -- {{{
- -- | Kinds of slices permitted in K3
+-- | Kinds of slices permitted in K3
data SKind where
SKVar :: r -> k -> SKind
SKUnk :: k -> SKind
SKTup :: [SKind] -> SKind
- -- | Witness of slice well-formedness
+-- | Witness of slice well-formedness
class Slice r (w :: SKind) where
data SliceDa w :: *
type SliceTy w :: *
data SliceDa (SKTup ts) = STup (MapSliceDa ts)
type SliceTy (SKTup ts) = MapSliceTy ts
-
------------------------------------------------------------------------}}}
--- Numeric Autocasting {{{
+{- * Numeric Autocasting -} -- {{{
-- XXX should we make these be constraints in the K3 class so that
-- different representations can make different choices?
- -- | Unary numerics
+-- | Unary numerics
class UnNum a where unneg :: a -> a
instance UnNum Bool where unneg = not
instance UnNum Int where unneg x = (-x)
instance UnNum Float where unneg x = (-x)
- -- | Binary numerics
+-- | Binary numerics
class BiNum a b where
type BNTF a b :: *
biadd :: a -> b -> BNTF a b
-- XXX More
------------------------------------------------------------------------}}}
--- Values and Expressions {{{
+{- * Values and Expressions -} -- {{{
class K3 (r :: * -> *) where
- -- | A representation-specific constraint for collections, on functions
- -- which need to dispatch on a type-tag in the output.
+ -- | 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.
+ -- | 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.
+ -- | A representation-specific constraint for slices, on eSlice.
type K3AST_Slice_C r (w :: SKind) :: Constraint
- -- | Add a comment to some part of the AST
+ -- | Add a comment to some part of the AST
cComment :: String -> r a -> r a
- -- | Add some annotations to some part of the AST
+ -- | Add some annotations to some part of the AST
cAnn :: Ann -> r a -> r a
-- XXX An escape hatch
eVar :: VarIx -> UnivTyRepr a -> r a
- eJust :: r a -> r (Maybe t)
+ eJust :: r a -> r (Maybe 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 (a,b,c)
+ eTuple4 :: (r a, r b, r c,r d) -> r (a,b,c,d)
-- eTuple :: K3RTuple r a -> r a
eEmpty :: (K3AST_Coll_C r c) => r (CTE c e)
eLeq :: r a -> r a -> r Bool
eNeq :: r a -> r a -> r Bool
- -- Unlike traditional lambdas, we require a witness
- -- that the argument is admissible in K3.
+ -- | A lambda application in K3.
+ --
+ -- Unlike traditional lambdas, we require some hints as to how to
+ -- destructure the argument (PatTy w) for the lambda; consider (\x -> x)
+ -- (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 w, K3BaseTy (PatTy w))
=> PatDa w -> (PatReprFn r w -> r b) -> r (PatTy w -> b)
eApp :: r (a -> b) -> r a -> r b
eFlatten :: r (CTE c (CTE c' t)) -> r (CTE c' t)
- -- | Called Aggregate in K3's AST
+ -- | Called Aggregate in K3's AST
eFold :: r ((t', t) -> t') -> r t' -> r (CTE c t) -> r t'
- -- | Group-By-Aggregate.
- --
- -- Note that the Fold argument is guaranteed to be called
- -- once per partition: any partitions that would be the Zero
- -- are not created by the Partitioner.
+ -- | Group-By-Aggregate.
+ --
+ -- Note that the Fold argument is guaranteed to be called
+ -- once per partition: any partitions that would be the Zero
+ -- are not created by the Partitioner.
eGBA :: r (t -> t'') -- ^ Partitioner
-> r ((t',t) -> t') -- ^ Folder
-> r t' -- ^ Zero for each partition
-> r ((t,t) -> Bool) -- ^ Less-or-equal
-> r (CTE 'CList t)
- -- | Peek an element from a collection.
- --
- -- Fails on empty collections.
- --
- -- For lists, this returns the head; for sets and bags
- -- it samples arbitrarily.
+ -- | Peek an element from a collection.
+ --
+ -- Fails on empty collections.
+ --
+ -- For lists, this returns the head; for sets and bags
+ -- it samples arbitrarily.
ePeek :: r (CTE c e) -> r e
- -- | Slice out from a collection; the slice's type and
- -- the type of elements of the collection must match.
- --
- -- Rather like lambdas, except that the witness is also
- -- a mandatory part of the definition of "slice" :)
+ -- | Slice out from a collection; the slice's type and
+ -- the type of elements of the collection must match.
+ --
+ -- Rather like lambdas, except that the witness is also
+ -- a mandatory part of the definition of "slice" :)
eSlice :: (K3AST_Slice_C r w, Slice r w, SliceTy w ~ t)
=> SliceDa w -> r (CTE c t) -> r (CTE c t)
-- XXX eSend
------------------------------------------------------------------------}}}
--- Miscellany {{{
+{- * 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 c t) -> CollTy c -> r (CTE c 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
------------------------------------------------------------------------}}}
) where
import Data.Word
-import Text.PrettyPrint.Free
-
import Dyna.BackendK3.AST
-import Dyna.BackendK3.Render
------------------------------------------------------------------------}}}
-- Automate collection type {{{
- -- | Demote a collection type annotation (of kind CKind) to the
- -- appropriate chunk of data for case analysis.
- --
- -- 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)
+-- | Demote a collection type annotation (of kind CKind) to the
+-- appropriate chunk of data for case analysis.
+--
+-- 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)
class K3AutoColl (c :: CKind) where autocoll :: CollTy c
instance K3AutoColl CBag where autocoll = CTBag
instance K3AutoColl CList where autocoll = CTList
------------------------------------------------------------------------}}}
-- Automate type {{{
- -- | Attempt to automatically derive a universal type representation.
- --
- -- 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)
+-- | Attempt to automatically derive a universal type representation.
+--
+-- 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)
class K3AutoTy a where autoty :: UnivTyRepr a
instance K3AutoTy Bool where autoty = tBool
instance K3AutoTy Word8 where autoty = tByte
------------------------------------------------------------------------}}}
-- K3 Macro Library (XXX WIP) {{{
- -- | Let as lambda
+-- | Let as lambda
macro_localVar :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKVar a))
=> UnivTyRepr a
-> (r a)
-> r b
macro_localVar w a b = eApp (eLam (PVar w) b) a
- -- | Case analyze a Maybe
+-- | Case analyze a Maybe
macro_caseMaybe :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKJust (PKVar a)))
=> UnivTyRepr a
-> r (Maybe a)
n
(eApp (eLam (PJust (PVar w)) b) m)
- -- | Case analyze a collection as either empty or a peeked element
+-- | Case analyze a collection as either empty or a peeked element
macro_emptyPeek :: (K3AST_Coll_C r c, K3AST_Pat_C r (PKVar a),
K3 r, K3BaseTy a, K3AutoTy a)
=> r (CTE c a) -> r b -> (r a -> r b) -> r b
-- | A parser for some chunk of the Dyna language, using Trifecta
--
-- Based in part on
--- https://github.com/ekmett/trifecta/blob/master/examples/RFC2616.hs
+-- <https://github.com/ekmett/trifecta/blob/master/examples/RFC2616.hs>
-- as well as the trifecta code itself
--
-- TODO:
--- We might want to use T.T.Literate, too, in the end.
--- Doesn't understand dynabase literals ("{ ... }")
--- Doesn't handle parenthesized aggregators
--- Doesn't handle shared subgoals ("whenever ... { ... }")
+--
+-- * We might want to use T.T.Literate, too, in the end.
+--
+-- * Doesn't understand dynabase literals ("{ ... }")
+--
+-- * Doesn't handle parenthesized aggregators
+--
+-- * Doesn't handle shared subgoals ("whenever ... { ... }")
-- Header material {{{
import Dyna.XXX.Trifecta (identNL)
------------------------------------------------------------------------}}}
--- Parsed output definition {{{
+{- * Parsed output definition -} -- {{{
data Annotation = AnnType (Spanned Term)
deriving (Eq,Ord,Show)
data Term = TFunctor {-# UNPACK #-} !B.ByteString ![Spanned Term]
| TAnnot Annotation !(Spanned Term)
| TVar {-# UNPACK #-} !B.ByteString
- -- | TDBLit XXX
+ -- TDBLit XXX
deriving (Eq,Ord,Show)
-- | Rules are not just terms because we want to make it very syntactically
------------------------------------------------------------------------}}}
--- Utilities {{{
+{- * Utilities -} -- {{{
bsf :: Functor f => f String -> f B.ByteString
bsf = fmap BU.fromString
------------------------------------------------------------------------}}}
--- Identifier Syles {{{
+{- * Identifier Syles -} -- {{{
usualpunct :: CS.CharSet
usualpunct = CS.fromList "!#$%&*+/<=>?@\\^|-~:."
------------------------------------------------------------------------}}}
--- Comment handling {{{
+{- * Comment handling -} -- {{{
dynaCommentStyle :: CommentStyle
dynaCommentStyle = CommentStyle
restOfLine = lift restOfLine
------------------------------------------------------------------------}}}
--- Atoms {{{
+{- * Atoms -} -- {{{
atom :: (Monad m, TokenParsing m) => m B.ByteString
atom = liftA BU.fromString stringLiteral
<|> (bsf $ ident dynaAtomStyle)
------------------------------------------------------------------------}}}
--- Terms and term expressions {{{
+{- * Terms and term expressions -} -- {{{
term :: DeltaParsing m => m (Spanned Term)
term = token $ choice
dtexpr = unDL texpr
------------------------------------------------------------------------}}}
--- Rules {{{
+{- * Rules -} -- {{{
-- | Grab the head (term!) and aggregation operator from a line that
-- we hope is a rule.
drule = spanned rule
------------------------------------------------------------------------}}}
--- Lines {{{
+{- * Lines -} -- {{{
progline :: DeltaParsing m => m (Spanned Line)
progline = spanned $ choice [ LRule <$> drule
module Dyna.XXX.THTuple(
-- * Promoted-kind type functions for tuples and rtuples
- MKLT(..),MKRLT(..),
+ MKLT,MKRLT,
-- * Classes on tuples and rtuples
Tupled(..),RTupled(..),
------------------------------------------------------------------------}}}
-- Exported classes {{{
- -- | Some type algebra on tuples full of constructed types
- -- which is invariant over the constructor in question
- --
- -- e.g. RTER (a,b) r = (r a, r b)
+-- | Some type algebra on tuples full of constructed types
+-- which is invariant over the constructor in question
+--
+-- e.g. RTER (a,b) r = (r a, r b)
class (MKLT (TOL base) ~ base) => Tupled base where
- -- | Apply r to each element of the tuple
+ -- | Apply r to each element of the tuple
type RTER base (r :: * -> *) :: *
-- | Go from the tuple representation to a promoted list;
-- the inverse of MKLT (as asserted by class constraints).
type TOL base :: [*]
- -- | Shed a type constructor
+ -- | Shed a type constructor
tupleopR :: (RTupled rbase, (RTR rbase) ~ r, (RTE rbase) ~ base)
=> (forall x . r x -> x) -> rbase -> base
- -- | Remap a type constructor
+ -- | Remap a type constructor
tupleopRS :: (RTupled rbase, (RTR rbase) ~ r, (RTE rbase) ~ base,
RTupled sbase, (RTR sbase) ~ s, (RTE sbase) ~ base)
=> (forall x . r x -> s x) -> rbase -> sbase
- -- | Recover the constructor and base type from r-full tuples.
- --
- -- e.g. RTR (r a, r b) = r, RTE (r a, r b) = (a, b)
- --
- -- This class further specifies some equivalence properties
- -- on RTER and MKRLT.
+-- | Recover the constructor and base type from r-full tuples.
+--
+-- e.g. RTR (r a, r b) = r, RTE (r a, r b) = (a, b)
+--
+-- This class further specifies some equivalence properties
+-- on RTER and MKRLT.
class (Tupled (RTE arred),
RTER (RTE arred) (RTR arred) ~ arred,
MKRLT (RTR arred) (TOL (RTE arred)) ~ arred
type RTR arred :: (* -> *)
type RTE arred :: *
- -- | Eliminate an rtuple out to a list.
+ -- | Eliminate an rtuple out to a list.
tupleopEL :: (RTR arred ~ r) => (forall x . r x -> a) -> arred -> [a]
------------------------------------------------------------------------}}}
projects / dyna2 / commitdiff