Dyna.BackendK3.AST,
Dyna.BackendK3.Automation,
Dyna.BackendK3.Render,
- Dyna.BackendK3.Stdlib,
Dyna.ParserHS.Parser,
Dyna.XXX.HList,
Dyna.XXX.THTuple,
-- 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.
--
+-- XXX k3ref K3 does not yet support references. This string is littered
+-- through the codebase from a previous, incomplete attempt at handling
+-- references which has been commented out to prevent the overly ambitious
+-- from attempting to make use of it.
+--
+-- XXX k3xref K3 does not yet support foreign key constraints.
-- Header material {{{
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
module Dyna.BackendK3.AST (
-- * Preliminaries
BiNum(..), UnNum(..),
-- * Collections
- CTE, CKind(..), CollTy(..), K3_Coll_C, asColl,
+ CTE, CKind(..), CollTy(..), asColl,
+{- XXX k3ref
-- * References
Ref,
+-}
-- * Pattern System
- PKind(..), Pat(..),
- PVar(..), PUnk(..), PJust(..), PRef(..),
- UnPatDa,
- MapPatDa, UnMapPatDa, MapPatTy,
- MapPatConst, K3_Pat_C, K3_Slice_C,
+ PKind(..), Pat(..), PDat(..),
+ MapPatConst,
-- * Annotations
- AnnT(..), AnnE(..), FunDepSpec(..), K3_Xref_C,
+ AnnT(..), AnnE(..), FunDepSpec(..),
-- * Type System: Base constraints
K3BaseTy,
-- * Expressions
K3(..),
+{- XXX
+ -- * Roles and Streams
+ -- SFormat(..), Stream(..), K3RoleDesc(..),
+-}
+
-- * Declarations
- Decl(..), DKind(..), mkdecl, mkfdecl, asCollR, asRefR
+ Decl(..), DBody(..), asR, asCollR, {- asRefR, -}
+ mkCollDecl, mkTrigDecl, -- unUDR,
+
+ -- * Programs
+ mkK3, mkK3T, MkK3T, Prog(..)
) where
+import Control.Monad.Identity
+import Control.Monad.State
import Data.Proxy
import Data.Word
import GHC.Prim (Constraint)
-- import Language.Haskell.TH (varT, mkName)
import Dyna.XXX.HList
+import Dyna.XXX.MonadUtils
import Dyna.XXX.THTuple
------------------------------------------------------------------------}}}
-- XXX
newtype VarIx = Var String
+ deriving (Eq,Ord,Show)
+
-- XXX (Hostname,Port)
newtype AddrIx = Addr (String,Int)
deriving (Eq,Show)
instance (K3BaseTy a, K3BaseTy (HList as)) => K3BaseTy (HList (a ': as))
$(mkTupleRecInstances ''K3BaseTy [])
+------------------------------------------------------------------------}}}
+-- Type System: Proxified Representations {{{
+
+type family K3Proxied (a :: *) :: *
+type family K3Unproxy (r :: * -> *) (a :: *) :: *
+
+type instance K3Proxied Bool = Bool
+type instance K3Unproxy r Bool = Bool
+
+type instance K3Proxied Word8 = Word8
+type instance K3Unproxy r Word8 = Word8
+
+type instance K3Proxied Float = Float
+type instance K3Unproxy r Float = Float
+
+type instance K3Proxied Int = Int
+type instance K3Unproxy r Int = Int
+
+type instance K3Proxied String = String
+type instance K3Unproxy r String = String
+
+type instance K3Proxied () = ()
+type instance K3Unproxy r () = ()
+
+type instance K3Proxied (Maybe a) = Maybe (K3Proxied a)
+type instance K3Unproxy r (Maybe a) = Maybe (K3Unproxy r a)
+
+type family MapK3Proxied (a :: [*]) :: [*]
+type instance MapK3Proxied '[] = '[]
+type instance MapK3Proxied (a ': as) = K3Proxied a ': (MapK3Proxied as)
+
+type family MapK3Unproxy (r :: * -> *) (a :: [*]) :: [*]
+type instance MapK3Unproxy r '[] = '[]
+type instance MapK3Unproxy r (a ': as) = K3Unproxy r a ': (MapK3Unproxy r as)
+
+type instance K3Proxied (HList a) = HList (MapK3Proxied a)
+type instance K3Unproxy r (HList a) = HList (MapK3Unproxy r a)
+
+type instance K3Proxied (a,b) = (K3Proxied a, K3Proxied b)
+type instance K3Unproxy r (a,b) = (K3Unproxy r a, K3Unproxy r b)
+
+type instance K3Proxied (a,b,c) = (K3Proxied a, K3Proxied b,
+ K3Proxied c)
+type instance K3Unproxy r (a,b,c) = (K3Unproxy r a, K3Unproxy r b,
+ K3Unproxy r c)
+
+type instance K3Proxied (a,b,c,d) = (K3Proxied a, K3Proxied b,
+ K3Proxied c, K3Proxied d)
+type instance K3Unproxy r (a,b,c,d) = (K3Unproxy r a, K3Unproxy r b,
+ K3Unproxy r c, K3Unproxy r d)
+
+type instance K3Proxied (a,b,c,d,e) = (K3Proxied a, K3Proxied b,
+ K3Proxied c, K3Proxied d,
+ K3Proxied e)
+type instance K3Unproxy r (a,b,c,d,e) = (K3Unproxy r a, K3Unproxy r b,
+ K3Unproxy r c, K3Unproxy r d,
+ K3Unproxy r e)
+
------------------------------------------------------------------------}}}
-- Targets {{{
instance (K3BaseTy a) => K3BaseTy (Target r a)
+type instance K3Proxied (Target r a) = Target Proxy (K3Proxied a)
+type instance K3Unproxy r (Target Proxy a) = Target r (K3Unproxy r a)
+
------------------------------------------------------------------------}}}
-- Collections {{{
-- | Reflect 'CollTy' at the type level.
-data CKind = CBag | CList | CSet
+data CKind = CKBag | CKList | CKSet
-- | The 'r' representation of a collection of kind 'c' of elements 'e'.
data family CTE (r :: * -> *) (c :: CKind) e
-- | Data-level specification of collection kinds
data CollTy c where
- CTBag :: CollTy CBag
- CTList :: CollTy CList
- CTSet :: CollTy CSet
+ -- | Bags are unordered collections of elements which may have duplicates.
+ CBag :: CollTy CKBag
+ -- | Lists are linearly ordered collecitons of elements in the usual
+ -- mu-recursive style.
+ CList :: CollTy CKList
+ -- | Sets are unordered collections of elements with no duplicates.
+ CSet :: CollTy CKSet
instance (K3BaseTy a) => K3BaseTy (CTE r c a)
--- | 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
+type instance K3Proxied (CTE r c a) = CTE Proxy c (K3Proxied a)
+type instance K3Unproxy r (CTE Proxy c a) = CTE r c (K3Unproxy r a)
-- | A convenience function for setting the type of a collection.
--
------------------------------------------------------------------------}}}
-- References {{{
+{- XXX k3ref
-- | The 'r' representation of references of elements of type 'a'
data family Ref (r :: * -> *) a
instance (K3BaseTy a) => K3BaseTy (Ref r a)
+type instance K3Proxied (Ref r a) = Ref Proxy (K3Proxied a)
+type instance K3Unproxy r (Ref Proxy a) = Ref r (K3Unproxy r a)
+ -}
+
------------------------------------------------------------------------}}}
-- Pattern System {{{
-- | Just patterns (see 'PJust')
PKJust :: PKind -> PKind
+{- XXX k3ref
-- | Ref patterns (see 'PRef')
PKRef :: PKind -> PKind
+ -}
-- | HList patterns
PKHL :: [PKind] -> PKind
-- 'PatTy' and 'PatReprFn' both produce 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.
+-- | Data-representation of patterns in K3.
+--
+-- The 'r' parameter is the representation of components of the pattern
+-- itself, and is used to constrain representation of variables. When
+-- being used as slices, @r@ will be the same as @s@ given to the type
+-- functions in the 'Pat' class below; when being used as patterns for
+-- lambdas, @r ~ UnivTyRepr@ and 's' is a 'K3'. In this latter case,
+-- the 'UnivTyRepr' is needed for "Dyna.BackendK3.Render"'s function,
+-- since every lambda needs an explicit type signature on its pattern.
+data PDat (r :: * -> *) (k :: PKind) where
+ -- | A variable used literally in a pattern
+ PVar :: r a -> PDat r (PKVar r (a :: *))
+
+ -- | A pattern wildcard.
+ --
+ -- Note that 'PatReprFn s (PUnk a) ~ ()', which should prohibit even
+ -- accidental use as part of a 'K3' expression or type.
+ PUnk :: PDat r (PKUnk (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.
+ PJust :: PDat r w -> PDat r (PKJust w)
+
+{- XXX k3ref
+ -- | A /Ref/ pattern; dereferences the provided reference.
+ PRef :: PDat r w -> PDat r (PKRef w)
+-}
+
+ -- | A HList-style product pattern
+ PHL :: HRList (PDat r) ws -> PDat r (PKHL ws)
+
+ PT2 :: (PDat r w1, PDat r w2) -> PDat r (PKTup [w1,w2])
+ PT3 :: (PDat r w1, PDat r w2, PDat r w3) -> PDat r (PKTup [w1,w2,w3])
+ PT4 :: (PDat r w1, PDat r w2, PDat r w3, PDat r w4)
+ -> PDat r (PKTup [w1,w2,w3,w4])
+ PT5 :: (PDat r w1, PDat r w2, PDat r w3, PDat r w4, PDat r w5)
+ -> PDat r (PKTup [w1,w2,w3,w4,w5])
+
+
+-- | Provides type functions on patterns. Useful when building up type
+-- signatures and pattern matches in lambdas.
--
-- Note that this is a closed class using the promoted
-- data 'PKind'.
-- 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 :: *
+class Pat (w :: PKind) where
-- | The type this witness witnesses (i.e. the things matched against)
type PatTy (s :: * -> *) w :: *
-- | The type this witness binds (i.e. after matching is done)
-- | The type of this pattern.
type PatReprFn (s :: * -> *) w :: *
--- | Given a chunk of pattern data, recover the PKind.
-type family UnPatDa (pd :: *) :: PKind
-
--- | Given a PatReprFn output and type constructor input, recover the PKind
-type family UnPatReprFn (s :: * -> *) (prf :: *) :: PKind
-
--- | 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
+instance (K3BaseTy a) => Pat (PKVar (r :: * -> *) (a :: *)) where
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
+instance (K3BaseTy a) => Pat (PKUnk (a :: *)) where
type PatTy s (PKUnk a) = a
type PatBTy s (PKUnk a) = ()
type PatReprFn s (PKUnk 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 w
+instance (Pat w) => Pat (PKJust w) where
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
--- | 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
+{- XXX k3ref
+instance (Pat w) => Pat (PKRef w) where
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 TMapPatTy (s :: * -> *) (x :: [PKind]) :: *
$(mkTyMapFlat 1 ''TMapPatTy ''PatTy)
type family TMapPatReprFn (r :: * -> *) (x :: [PKind]) :: *
$(mkTyMapFlat 1 ''TMapPatReprFn ''PatReprFn)
-$(mkTyUnMap (Just 'PKTup) 0 ''UnPatDa ''UnPatDa)
+type family MapPatConst (x :: [PKind]) :: Constraint
+type instance MapPatConst '[] = ()
+type instance MapPatConst (x ': xs) = (Pat x, MapPatConst xs)
-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 (TMapPatDa ts) ~ PKTup ts, MapPatConst ts r)
- => Pat r (PKTup (ts :: [PKind])) where
- type PatDa (PKTup ts) = TMapPatDa ts
+instance (MapPatConst ts)
+ => Pat (PKTup (ts :: [PKind])) where
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 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)
+instance (MapPatConst ts)
+ => Pat (PKHL (ts :: [PKind])) where
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 {{{
--
-- 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)
+-- need to use 'fdscast'), but the alternative of, e.g. Tagged, is not that
+-- great either!
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)
--- | A representation-specific constraint for cross-references
-type family K3_Xref_C (r :: * -> *) (w :: PKind) :: Constraint
-
-- | Annotations on 'K3Ty' types
data AnnT a where
-- | 'AOneOf' for HList representations
AOneOfHL :: (HLR Maybe v mv) => AnnT (HList mv)
+{- XXX k3xref
-- | A cross-reference within this collection
+ --
+ -- Note that the AST supports the use of arbitrary expressions here, which
+ -- is not likely the case of the actual K3 system! Please don't do
+ -- something silly.
--
- -- XXX this is not actually implemented anywhere and has yet to be
- -- demonstrated as being implementable
- AXref :: (PatTy r w ~ t, w ~ UnPatDa (PatDa w))
- => PatDa w -> (forall p . PatReprFn p w -> p x)
- -- Foreign projection
- -> PatDa w -> (forall p . PatReprFn p w -> p x)
+ -- XXX The need to specify a Proxy is annoying.
+ AXref :: (Pat w, PatTy r w ~ t, Pat w', PatTy r w' ~ t)
+ => Proxy x
+ -> PDat r w -> (forall p . PatReprFn p w -> p x)
+ -> PDat r w' -> (forall p . PatReprFn p w' -> p x)
-> AnnT (CTE r c' t)
-- | A cross-reference to a declared collection.
--
- -- XXX this is not actually implemented anywhere and has yet to be
- -- demonstrated as being implementable
- AXrefF :: (Pat p w, Pat p w', PatTy p w ~ t, PatTy p w' ~ t')
- => Decl UnivTyRepr r' (CTE r' c t) -- Foreign collection
- -> PatDa w
- -> (PatReprFn p w -> p x) -- Foreign projection
- -> PatDa w'
- -> (PatReprFn p w' -> p x) -- Local projection
- -> AnnT (CTE r c' t')
+ -- See the notes for 'AXref'
+ AXrefF :: (Pat w, Pat w', PatTy r w ~ t, PatTy r w' ~ t')
+ => Proxy x
+ -> Decl s (CTE Proxy c' t') -- Foreign collection
+ -> PDat UnivTyRepr w' -> (forall p . PatReprFn p w' -> p x)
+ -> PDat UnivTyRepr w -> (forall p . PatReprFn p w -> p x)
+ -> AnnT (CTE r c t)
+-}
-- | An escape hatch! (XXX)
ATMisc :: String -> AnnT a
+ -- XXX Missing: INDEX, UNIQUE, ORDERED, SORTED
-- | Annotations on 'K3' expressions
data AnnE a where
-- | Decorate an expression as atomic.
AAtomic :: AnnE a
- -- |
+ -- | Flag that a collection (or collection expression) ought to be a
+ -- singleton. K3's type system is not so deeply embedded into Haskell
+ -- that we can check this.
ASingleton :: AnnE (CTE r t a)
-- | An escape hatch! (XXX)
-- tPair :: r a -> r b -> r (a,b)
tMaybe :: r a -> r (Maybe a)
- tRef :: r a -> r (Ref r' a)
+ -- XXX k3ref
+ -- 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)
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 k3ref
+ -- tRef (UTR a) = UTR $ tRef a
-- XXX TUPLES
-- tTuple us = UTR $ tTuple $ tupleopRS unUTR us
------------------------------------------------------------------------}}}
-- Numeric Autocasting {{{
- -- XXX should we make these be constraints in the K3 class so that
- -- different representations can make different choices?
-
-- | Unary numerics
class UnNum a where unneg :: a -> a
instance UnNum Bool where unneg = not
biadd a b = (a + (fromIntegral b))
bimul a b = (a * (fromIntegral b))
-
- -- XXX More
-
------------------------------------------------------------------------}}}
-- Expressions {{{
-- type in Haskell.
class K3 (r :: * -> *) where
+ declVar :: (pt ~ K3Proxied t, t ~ K3Unproxy r pt)
+ => Decl s pt -> r t
+
+ -- | Reference the given variable (and promise that it has type 'a')
+ --
+ -- Note that this is, for example, the only way of producing Targets.
+ --
+ -- 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
+
-- | Add a comment to some part of the AST
cComment :: String -> r a -> r a
-- | Add some annotations to some part of the AST
cString :: String -> r String
cUnit :: r ()
- -- | Reference the given variable (and promise that it has type 'a')
- --
- -- Note that this is, for example, the only way of producing Targets.
- --
- -- 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
-
- declVar :: Decl UnivTyRepr r a -> r a
-
eJust :: r a -> r (Maybe a)
- eRef :: r a -> r (Ref r a)
+ -- XXX k3ref
+ -- eRef :: r a -> r (Ref r a)
-- XXX TUPLES
eTuple2 :: (r a, r b) -> r (a,b)
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)
+ eEmpty :: CollTy c -> r (CTE r c e)
+ eSing :: CollTy 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 :: (K3_Pat_C r w, Pat UnivTyRepr w, K3BaseTy (PatTy r w))
- => PatDa w -> (PatReprFn r w -> r b) -> r (PatTy r w -> b)
+ eLam :: (Pat w)
+ => PDat UnivTyRepr w -> (PatReprFn r w -> r b) -> r (PatTy r w -> b)
-- | Apply
eApp :: r (a -> b) -> r a -> r b
-- | 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)
+ -> r (CTE r 'CKList t)
-- | Peek an element from a collection.
--
--
-- Rather like lambdas, except that the witness is also
-- a mandatory part of the definition of "slice" :)
- eSlice :: (K3_Slice_C r w, Pat r w, PatTy r w ~ t)
- => PatDa w -- ^ Slice specification
+ eSlice :: (Pat w, PatTy r w ~ t, K3BaseTy t)
+ => PDat r w -- ^ Slice specification
-> r (CTE r c t) -- ^ Input collection
-> r (CTE r c t)
--
-- Note that dereference is done by a lambda pattern. See Automation's
-- 'deref'.
- eAssign :: r (Ref r t) -> r t -> r ()
+ -- XXX k3ref
+ -- eAssign :: r (Ref r t) -> r t -> r ()
-- | Send a function and data to another node.
--
-- XXX Is there any way to refer to "self" as an addrix?
eSend :: r AddrIx -> r (Target r a) -> r a -> r ()
+------------------------------------------------------------------------}}}
+-- Roles and Streams {{{
+
+{- XXX UNTESTED!
+
+data Role = Role
+data SFormat = CSV | JSON
+data Stream t = StreamFile SFormat String
+
+-- | Describe the information flow through a K3 program. K3 calls these
+-- "roles".
+--
+-- XXX Doesn't do anything with "patterns" at the moment.
+class K3RoleDesc (r :: * -> *) where
+ type K3RD_M r :: * -> * -> *
+
+ -- | Finalize a role description. Since we force sources to be made
+ -- inside some @Monad@, we'll need a way out which seals the
+ -- universe. This is the ST Monad trick over again.
+ mkRole :: (m ~ K3RD_M r)
+ => (forall s . (Monad (m s) => m s (r ())))
+ -> r Role
+
+ -- | Create a source for this role.
+ rSource :: (K3BaseTy t, m ~ K3RD_M r, Monad (m s))
+ => UnivTyRepr t -> Stream t -> m s (r t)
+
+ -- | Bind a source to a trigger
+ rBind :: (K3BaseTy t)
+ => r t -> (Decl s t) -> r ()
+
+ -- | Consume
+ rConsume :: r t -> r ()
+
+ -- | Many terminal role descriptions group together
+ -- to form a terminal role description.
+ rBlock :: [r ()] -> r ()
+-}
+
------------------------------------------------------------------------}}}
-- Declarations {{{
--- | K3 supports a few kinds of delcarations at the top level:
-data DKind r dt where
+-- | K3 supports a few kinds of delcarations at the top level.
+--
+-- Those with actual structural content are required to be universal in the
+-- underlying representation. The types exposed here are all 'K3Proxied' so
+-- that universally quantified variables do not escape (all references to
+-- representation are replaced with 'Proxy').
+data DBody dt where
-- | Collections
--
- -- XXX No initializers? [t] ->
- DKColl :: DKind r (CTE r (c :: CKind) t)
+ -- XXX No initializers? [r t] ->
+ DColl :: (pt ~ K3Proxied t)
+ => UnivTyRepr (CTE r c t) -> DBody (CTE Proxy (c :: CKind) pt)
+{-
+ - XXX K3ref
-- | Global References
- DKRef :: DKind r (Ref r t)
+ DRef :: DBody (Ref Proxy (K3Proxied t))
+-}
+
+ -- | Triggers, which execute in a different transaction than the caller
+ --
+ -- XXX does not support local variables
+ DTrig :: (forall r . (K3 r) => r (t -> ())) -> DBody (Target Proxy (K3Proxied t))
-- | Functions, which execute in the same transaction as the caller
- DKFunc :: r (a -> b) -> DKind r (a -> b)
+ DFunc :: (forall r . (K3 r) => r (a -> b)) -> DBody (K3Proxied (a -> b))
- -- | Triggers, which execute in a different transaction than the caller
- DKTrig :: r (t -> ()) -> DKind r (Target r t)
+{- XXX
+ -- | Role declaration
+ DRole :: (K3RoleDesc ro) => String -> ro Role -> DBody Role
+-}
-- | A top-level declaration.
--
--- XXX does not enumerate local variables
-data Decl tr r t = Decl VarIx (tr t) (DKind r t)
-
--- | 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 Proxy passed in.
-mkdecl :: (Proxy r -> Decl tr r t) -> Decl tr r t
-mkdecl f = f Proxy
-
--- | 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)
- => (Proxy 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 Proxy self)
- in f Proxy self
+-- Contains the name ultimately used in the K3 program and the body of the
+-- declaration.
+data Decl s t = Decl VarIx (DBody t)
+
+-- XXX This really can't quite be right; in the end a K3 program is a set of
+-- role declarations!
+data Prog = forall s t . Prog (Decl s t)
+
+newtype DeclIx = DeclIx Int
+ deriving (Num,Show)
+
+mkCollDecl :: (Monad m)
+ => String
+ -> (forall r . Proxy r -> UnivTyRepr (CTE r c t))
+ -> MkK3T m s (Decl s (CTE Proxy c (K3Proxied t)))
+mkCollDecl n f = do
+ (DeclIx uniq) <- incState
+ let v = Var $ n ++ "_" ++ show uniq
+ return $ Decl v $ DColl (f Proxy)
+
+-- | Define a fixed-point declaration, with an assist in constraining
+-- polymorphism.
+mkTrigDecl :: (Monad m)
+ => String
+ -> (forall r . Proxy r -> UnivTyRepr t)
+ -> (forall r . (K3 r) => r t -> r (t -> ()))
+ -> MkK3T m s (Decl s (Target Proxy (K3Proxied t)))
+mkTrigDecl n ty mk = do
+ (DeclIx uniq) <- incState
+ let v = Var $ n ++ "_" ++ show uniq
+ return $ Decl v (DTrig $ mk (unsafeVar v (ty Proxy)))
+
+newtype MkK3T m s a = MkK3T { unMkK3T :: StateT DeclIx m a }
+ deriving (Monad, MonadState DeclIx)
+
+mkK3T :: (Functor m, Monad m)
+ => (forall s . MkK3T m s (Decl s a))
+ -> m Prog
+mkK3T a = Prog `fmap` evalStateT (unMkK3T a) (DeclIx 0)
+
+mkK3 :: (forall s . MkK3T Identity s (Decl s a))
+ -> Prog
+mkK3 = runIdentity . mkK3T
+
+------------------------------------------------------------------------}}}
+-- Utilities for AST work {{{
+
+asR :: r a -> Proxy r -> r a
+asR = const
-- | Ensure that the representation type of a collection matches
--
asCollR :: s (CTE r c t) -> Proxy r -> s (CTE r c t)
asCollR = const
+{-
+ - XXX k3ref
-- | Ensure that the representation type of a ref matches
-asRefR :: r' (Ref r t) -> Proxy r -> r' (Ref r t)
+asRefR :: s (Ref r t) -> Proxy r -> s (Ref r t)
asRefR = const
+-}
------------------------------------------------------------------------}}}
autopv,
-- * K3 macro library
- localVar, caseMaybe, emptyPeek, deref, combMany
+ localVar, caseMaybe, emptyPeek, {- XXX k3ref deref, -} combMany, switchCase
) where
import Data.Word
import Dyna.BackendK3.AST
import Dyna.XXX.HList
-import Dyna.XXX.THTuple
+-- import Dyna.XXX.THTuple
------------------------------------------------------------------------}}}
-- Automate collection type {{{
-- otherwise it imposes a constraint on the haskell tyvar.
-- (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
-instance K3AutoColl CSet where autocoll = CTSet
+instance K3AutoColl CKBag where autocoll = CBag
+instance K3AutoColl CKList where autocoll = CList
+instance K3AutoColl CKSet where autocoll = CSet
------------------------------------------------------------------------}}}
-- Automate type {{{
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
+-- XXX k3ref
+-- instance (K3AutoTy a) => K3AutoTy (Ref r a) where autoty = tRef autoty
instance (K3AutoTy a) => K3AutoTy (Target r a) where autoty = tTarget autoty
instance (K3AutoTy a, K3BaseTy a, K3AutoTy b, K3BaseTy b)
=> K3AutoTy (a -> b) where
-}
-autopv :: (K3AutoTy a) => PatDa (PKVar UnivTyRepr a)
+autopv :: (K3BaseTy a, K3AutoTy a) => PDat UnivTyRepr (PKVar UnivTyRepr a)
autopv = PVar autoty
------------------------------------------------------------------------}}}
-- K3 Macro Library (XXX WIP) {{{
-- | Let as lambda
-localVar :: (K3 r, K3AutoTy a, K3BaseTy a, K3_Pat_C r (PKVar UnivTyRepr a))
+localVar :: (K3 r, K3AutoTy a, K3BaseTy a)
=> (r a)
-> (r a -> r b)
-> r b
{-
-- | Let as lambda with explicit type variable
-localVar' :: (K3 r, K3BaseTy a, K3_Pat_C r (PKVar UnivTyRepr a))
+localVar' :: (K3 r, K3BaseTy a)
=> UnivTyRepr a
-> (r a)
-> (r a -> r b)
-}
-- | Case analyze a Maybe
-caseMaybe :: (K3 r, K3BaseTy a,
- K3_Pat_C r (PKJust (PKVar UnivTyRepr a)))
+caseMaybe :: (K3 r, K3BaseTy a)
=> UnivTyRepr a
-> r (Maybe a)
-> r b
(eApp (eLam (PJust (PVar w)) b) m)
-- | Case analyze a collection as either empty or a peeked element
-emptyPeek :: (K3_Coll_C r c,
- K3_Pat_C r (PKVar UnivTyRepr a),
- K3 r, K3BaseTy a, K3AutoTy a)
+emptyPeek :: (K3 r, K3BaseTy a, K3AutoTy a, K3AutoColl c)
=> r (CTE r c a) -> r b -> (r a -> r b) -> r b
-emptyPeek c e l = eITE (eEq c eEmpty)
+emptyPeek c e l = eITE (eEq c $ eEmpty autocoll)
e
(eApp (eLam (PVar autoty) l) $ ePeek c)
+{- XXX k3ref
-- | 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)
+deref :: (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
+combMany :: (K3AutoColl c, K3 r) => [r a] -> r (CTE r c a)
+combMany = foldr (\e c -> eCombine c (eSing autocoll e)) $ eEmpty autocoll
+
+switchCase :: (K3 r, K3AutoTy s, K3BaseTy s)
+ => [(r s, r a)] -> r a -> r (s -> a)
+switchCase arms def = eLam autopv
+ (\s -> foldl (\c (s',a) -> eITE (eEq s s') a c) def arms)
------------------------------------------------------------------------}}}
-- Collect variables in a term (XXX TODO) {{{
instance K3 VarsInK3 where
type K3AST_Coll_C VarsInK3 c = ()
- type K3AST_Pat_C VarsInK3 p = ()
- type K3AST_Slice_C VarsInK3 s = ()
cComment _ v = v
cAnn _ a = a
--- /dev/null
+---------------------------------------------------------------------------
+-- | Collect the declarations used inside a K3 expression.
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Dyna.BackendK3.CollectDecls where
+
+import qualified Data.Map as M
+
+import Dyna.BackendK3.AST
+import Dyna.XXX.HList
+
+data ExDecl = forall a s . Ex (Decl s a)
+
+newtype C (a :: *) = C { unC :: M.Map VarIx ExDecl }
+
+pC :: C a -> C b
+pC (C x) = C x
+
+eC :: C a
+eC = C M.empty
+
+uC :: C a -> C b -> C c
+uC (C a) (C b) = C $ M.union a b
+
+mkpc :: PDat UnivTyRepr w -> (PatReprFn C w)
+mkpc (PVar _) = eC
+mkpc PUnk = ()
+mkpc (PHL HRN) = HN
+mkpc (PHL (w :++ ws)) = mkpc w :+ mkpc (PHL ws)
+mkpc (PJust x) = mkpc x
+mkpc (PT2 (a,b)) = (mkpc a, mkpc b)
+mkpc (PT3 (a,b,c)) = (mkpc a, mkpc b, mkpc c)
+mkpc (PT4 (a,b,c,d)) = (mkpc a, mkpc b, mkpc c, mkpc d)
+mkpc (PT5 (a,b,c,d,e)) = (mkpc a, mkpc b, mkpc c, mkpc d, mkpc e)
+-- XXX k3ref
+-- mkpc (PRef w) = mkpc w
+
+cslice :: PDat C w -> C (PatTy C w)
+cslice (PVar x) = x
+cslice (PUnk) = eC
+cslice (PJust x) = pC $ cslice x
+cslice (PHL xs) = C $ M.unions $ hrlproj (unC . cslice) xs
+cslice (PT2 (a,b)) = uC (cslice a) (cslice b)
+cslice (PT3 (a,b,c)) = C $ M.unions [ unC $ cslice a
+ , unC $ cslice b
+ , unC $ cslice c
+ ]
+cslice (PT4 (a,b,c,d)) = C $ M.unions [ unC $ cslice a
+ , unC $ cslice b
+ , unC $ cslice c
+ , unC $ cslice d
+ ]
+cslice (PT5 (a,b,c,d,e)) = C $ M.unions [ unC $ cslice a
+ , unC $ cslice b
+ , unC $ cslice c
+ , unC $ cslice d
+ , unC $ cslice e
+ ]
+
+instance K3 C where
+
+ declVar d@(Decl v b) = C $ M.union (cdk b) (M.singleton v (Ex d))
+ unsafeVar _ _ = eC
+
+ cComment _ x = x
+ cAnn x _ = x
+
+ cAddress _ = eC
+ cBool _ = eC
+ cByte _ = eC
+ cFloat _ = eC
+ cInt _ = eC
+ cNothing = eC
+ cString _ = eC
+ cUnit = eC
+
+ eJust c = pC c
+ -- XXX k3ref
+ -- eRef c = pC c
+
+ eTuple2 (a,b) = C $ M.unions [unC a, unC b]
+ eTuple3 (a,b,c) = C $ M.unions [unC a, unC b, unC c]
+ eTuple4 (a,b,c,d) = C $ M.unions [unC a, unC b, unC c, unC d]
+ eTuple5 (a,b,c,d,e) = C $ M.unions [unC a, unC b, unC c, unC d, unC e]
+
+ eHL HRN = eC
+ eHL (a:++b) = uC a (eHL b)
+
+ eEmpty _ = eC
+ eSing _ c = pC c
+ eCombine a b = uC a b
+ eRange a b c = C $ M.unions [unC a, unC b, unC c]
+
+ eAdd a b = uC a b
+ eMul a b = uC a b
+ eNeg a = pC a
+
+ eEq a b = uC a b
+ eLt a b = uC a b
+ eLeq a b = uC a b
+ eNeq a b = uC a b
+
+ eLam p fn = let cs = unC $ fn (mkpc p) in C cs
+ eApp f x = uC f x
+
+ eBlock cs c = C $ M.unions (unC c : map unC cs)
+ eIter f c = uC f c
+ eITE i t e = C $ M.unions [unC i, unC t, unC e]
+
+ eMap f c = uC f c
+ eFiltMap p f c = C $ M.unions [unC p, unC f, unC c]
+
+ eFlatten c = pC c
+
+ eFold s z c = C $ M.unions [unC s, unC z, unC c]
+
+ eGBA p f z i = C $ M.unions [unC p, unC f, unC z, unC i]
+
+ eSort i c = uC i c
+
+ ePeek c = pC c
+ eSlice s c = uC (cslice s) c
+
+ eInsert a b = uC a b
+ eDelete a b = uC a b
+ eUpdate a b c = C $ M.unions [unC a, unC b, unC c]
+
+ -- XXX k3ref
+ -- eAssign r v = C $ M.union (unC r) (unC v)
+
+ eSend a t m = C $ M.unions [unC a, unC t, unC m]
+
+cdk :: DBody t -> M.Map VarIx ExDecl
+cdk (DColl _) = M.empty
+-- XXX k3ref
+-- cdk DRef = M.empty
+cdk (DFunc b) = unC b
+cdk (DTrig b) = unC b
---------------------------------------------------------------------------
--- | Print a K3 AST or Type in a way that the K3 compiler understands.
+-- | Print a K3 AST or Type in a way that the K3 compiler understands.
--
--- XXX Note that the output is currently hideously ugly. We really should
--- fix that.
+-- XXX Note that the output is currently hideously ugly. We really should
+-- fix that.
-- Header material {{{
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
module Dyna.BackendK3.Render (
-- * K3 implementations
- AsK3Ty(..), AsK3(..),
+ AsK3Ty(..), AsK3E(..),
-- * Utility functions
- sh, sht, shd
+ sh, sht, shd, shk3
) where
-import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.List as DL
+import qualified Data.Map as M
import Text.PrettyPrint.Free
import Dyna.BackendK3.AST
-import Dyna.BackendK3.Automation
+import Dyna.BackendK3.CollectDecls
import Dyna.XXX.HList
import Dyna.XXX.MonadUtils
import Dyna.XXX.THTuple
-import qualified Language.Haskell.TH as TH
+-- import qualified Language.Haskell.TH as TH
------------------------------------------------------------------------}}}
-- Collection handling {{{
-class K3CFn (c :: CKind) where
- k3cfn_empty :: AsK3 e (CTE (AsK3 e) c a)
- k3cfn_sing :: AsK3 e vma -> AsK3 e (CTE (AsK3 e) c vma)
+k3cfn_empty :: CollTy c -> AsK3E e (CTE (AsK3E e) c a)
+k3cfn_empty CSet = AsK3E$ const$ "{ }"
+k3cfn_empty CList = AsK3E$ const$ "[ ]"
+k3cfn_empty CBag = AsK3E$ const$ "{| |}"
-instance K3CFn CSet where
- k3cfn_empty = AsK3$ const$ "{ }"
- k3cfn_sing (AsK3 e) = AsK3$ braces . e
-
-instance K3CFn CList where
- k3cfn_empty = AsK3$ const$ "[ ]"
- k3cfn_sing (AsK3 e) = AsK3$ brackets . e
-
-instance K3CFn CBag where
- k3cfn_empty = AsK3$ const$ "{| |}"
- k3cfn_sing (AsK3 e) = AsK3$ encBag . e
+k3cfn_sing :: CollTy c -> AsK3E e vma -> AsK3E e (CTE (AsK3E e) c vma)
+k3cfn_sing CSet (AsK3E e) = AsK3E$ braces . e
+k3cfn_sing CList (AsK3E e) = AsK3E$ brackets . e
+k3cfn_sing CBag (AsK3E e) = AsK3E$ encBag . e
------------------------------------------------------------------------}}}
-- Pattern handling {{{
-class (Pat UnivTyRepr w) => K3PFn w where
- -- | 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 :: PDat UnivTyRepr w
+ -> ReaderT Bool (State Int) (Doc e, PatReprFn (AsK3E e) w)
rec_k3pfn = local (const False) . k3pfn
-instance (K3BaseTy a) => K3PFn (PKVar UnivTyRepr (a :: *)) where
- k3pfn (PVar (tr :: UnivTyRepr a)) = do
+-- | 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 :: PDat UnivTyRepr w -> ReaderT Bool (State Int) (Doc e, PatReprFn (AsK3E e) w)
+k3pfn (PVar tr) = do
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) <- 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)
+ ,AsK3E$ const$ sn)
+k3pfn PUnk = return ("_", ())
+k3pfn (PJust w) = rec_k3pfn w >>= \(p,r) -> return ("just" <+> parens p, r)
+-- XXX k3ref
+-- k3pfn (PRef w) = rec_k3pfn w
+k3pfn (PHL HRN) = ask >>= \f -> return (if f then "" else "()", HN)
+k3pfn (PHL (w :++ ws)) = do
+ (pw,rw) <- k3pfn w
+ (ps,rs) <- local (const True) $ k3pfn (PHL ws)
+ p <- asks (\f -> (if f then (comma <>) else parens) (pw <> ps))
+ let r = rw :+ rs
+ return (p,r)
+k3pfn (PT2 (a,b)) = do
+ (pa,ra) <- k3pfn a
+ (pb,rb) <- k3pfn b
+ let p = tupled [pa,pb]
+ let r = (ra,rb)
+ return (p,r)
+k3pfn (PT3 (a,b,c)) = do
+ (pa,ra) <- k3pfn a
+ (pb,rb) <- k3pfn b
+ (pc,rc) <- k3pfn c
+ let p = tupled [pa,pb,pc]
+ let r = (ra,rb,rc)
+ return (p,r)
+k3pfn (PT4 (a,b,c,d)) = do
+ (pa,ra) <- k3pfn a
+ (pb,rb) <- k3pfn b
+ (pc,rc) <- k3pfn c
+ (pd,rd) <- k3pfn d
+ let p = tupled [pa,pb,pc,pd]
+ let r = (ra,rb,rc,rd)
+ return (p,r)
+k3pfn (PT5 (a,b,c,d,e)) = do
+ (pa,ra) <- k3pfn a
+ (pb,rb) <- k3pfn b
+ (pc,rc) <- k3pfn c
+ (pd,rd) <- k3pfn d
+ (pe,re) <- k3pfn e
+ let p = tupled [pa,pb,pc,pd,pe]
+ let r = (ra,rb,rc,rd,re)
+ return (p,r)
------------------------------------------------------------------------}}}
-- Slice handling {{{
-class (Pat (AsK3 e) w) => K3SFn e w where
- -- | 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 :: PDat (AsK3E e) w -> Reader Bool (AsK3E e (PatTy (AsK3E e) w))
rec_k3sfn = local (const False) . k3sfn
-instance (K3BaseTy a) => K3SFn e (PKVar (AsK3 e) (a :: *)) where
- k3sfn (PVar r) = return r
-
-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) = do
+-- | Print a pattern
+k3sfn :: PDat (AsK3E e) w -> Reader Bool (AsK3E e (PatTy (AsK3E e) w))
+k3sfn (PVar r) = return r
+k3sfn PUnk = return $ AsK3E$ const$ text "_"
+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 "()")
+ return $ AsK3E$ \n -> "just" <> parens (unAsK3E p n)
+{- XXX k3ref
+k3sfn (PRef x) = do
+ p <- rec_k3sfn x
+ return $ AsK3E$ unAsK3E p -- coerce
+-}
+k3sfn (PHL HRN) = asks (\f -> AsK3E$ const$ if f then "" else "()")
+k3sfn (PHL (w :++ ws)) = do
+ pw <- k3sfn w
+ ps <- local (const True) $ k3sfn (PHL ws)
+ fn <- asks (\f -> (if f then (comma <>) else parens))
+ return$ AsK3E$ \n -> fn $ (unAsK3E pw n) <> (unAsK3E ps n)
+k3sfn (PT2 (a,b)) = do
+ pa <- k3sfn a
+ pb <- k3sfn b
+ return$ AsK3E$ \n -> tupled [unAsK3E pa n, unAsK3E pb n]
+k3sfn (PT3 (a,b,c)) = do
+ pa <- k3sfn a
+ pb <- k3sfn b
+ pc <- k3sfn c
+ return$ AsK3E$ \n -> tupled [unAsK3E pa n, unAsK3E pb n, unAsK3E pc n]
+k3sfn (PT4 (a,b,c,d)) = do
+ pa <- k3sfn a
+ pb <- k3sfn b
+ pc <- k3sfn c
+ pd <- k3sfn d
+ return$ AsK3E$ \n -> tupled [unAsK3E pa n, unAsK3E pb n
+ ,unAsK3E pc n, unAsK3E pd n]
+k3sfn (PT5 (a,b,c,d,e)) = do
+ pa <- k3sfn a
+ pb <- k3sfn b
+ pc <- k3sfn c
+ pd <- k3sfn d
+ pe <- k3sfn e
+ return$ AsK3E$ \n -> tupled [unAsK3E pa n, unAsK3E pb n
+ ,unAsK3E pc n, unAsK3E pd n
+ ,unAsK3E pe n]
-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 {{{
<+> op
<+> (tupled $ map pretty cod)
-{-
+{- XXX k3xref
newtype K3RXref a = K3RXR { unK3RXR :: String }
-class (UnPatDa (PatDa w) ~ w) => RXref (w :: PKind) where
- rxref_mk :: PatDa w -> ReaderT String (State Int) (PatReprFn K3RXref w)
-instance (K3BaseTy a) => RXref (PKVar (K3RXref :: * -> *) (a :: *)) where
- rxref_mk _ = do
+rxref_mk :: PDat r w -> ReaderT String (State Int) (PatReprFn K3RXref w)
+rxref_mk (PVar _) = ask >>= \p -> get >>= \i -> return $ K3RXR (p <> show i)
+rxref_mk PUnk = return ()
+{- XXX k3ref
+rxref_mk (PRef w) = do
pfx <- ask
ix <- get
- return $ K3RXR (pfx <> show ix)
+ (r,_) <- local (const $ pfx <> show ix) $ bracketState 0 $ rxref_mk w
+ return r
+
+-- test (AXref pd fn _ _) = unK3RXR $ fn (evalState (runReaderT (rxref_mk pd) "x") 0)
+-}
+
+{-
+ - Some older code for doing this; this has obsolesced but may be useful in
+ - writing the above.
+class (UnPatDa (PatDa w) ~ w) => RXref (w :: PKind) where
+
+instance (K3BaseTy a) => RXref (PKVar (r :: * -> *) (a :: *)) where
instance (K3BaseTy a) => RXref (PKUnk (a :: *)) where
- rxref_mk _ = return ()
instance (RXref w) => RXref (PKRef w) where
- rxref_mk w = do
- pfx <- ask
- ix <- get
- (r,_) <- local (const $ pfx <> show ix) $ bracketState 0 $ rxref_mk w
- return r
instance (UnMapPatDa (HList (MapPatDa ws)) ~ ws,
MapPatConst ws K3RXref,
(rw,_) <- local (const $ pfx <> show ix) $ bracketState 0 $ rxref_mk w
rs <- rxref_mk ws
return (rw :+ rs)
-
-type instance K3_Xref_C K3RXref w = RXref w
+-}
-}
annTText :: AnnT a -> Doc e
-annTText (AFunDep fs) = annfds "->" fs
-annTText (AFunDepHL fs) = annfdshl "->" fs
-annTText (AIndex fs) = annfds "=>" fs
-annTText (AIndexHL fs) = annfdshl "=>" fs
-annTText AOneOf = "oneof"
-annTText AOneOfHL = "oneof"
-annTText (AXref _ _ _ _) = "" -- XXX
-annTText (AXrefF _ _ _ _ _) = "" -- XXX
-annTText (ATMisc s) = text s
+annTText (AFunDep fs) = annfds "->" fs
+annTText (AFunDepHL fs) = annfdshl "->" fs
+annTText (AIndex _) = "" -- XXX not yet supported annfds "=>" fs
+annTText (AIndexHL _) = "" -- XXX not yet supported annfdshl "=>" fs
+annTText AOneOf = "" -- XXX not yet supported "oneof"
+annTText AOneOfHL = "" -- XXX not yet supported "oneof"
+annTText (ATMisc s) = text s
+-- XXX k3xref
+-- annTText (AXref _ _ _ _ _) = "" -- XXX
+-- annTText (AXrefF _ _ _ _ _ _) = "" -- XXX
annEText :: AnnE a -> Doc e
annEText AAtomic = "atomic"
-- | Produce a textual representation of a K3 type
--
--- Unlike AsK3 below, we don't need to thread a variable counter
+-- Unlike AsK3E 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 }
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
+ tColl CSet (AsK3Ty ta) = AsK3Ty$ braces ta
+ tColl CBag (AsK3Ty ta) = AsK3Ty$ encBag ta
+ tColl CList (AsK3Ty ta) = AsK3Ty$ brackets ta
tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta `above` ("->" <+> tb)
- tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
+ -- XXX k3ref
+ -- tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
-- XXX TUPLES Note the similarities!
tTuple2 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us
deriving (Enum,Eq,Ord,Show)
-- | Produce a textual representation of a K3 expression
-newtype AsK3 e (a :: *) = AsK3 { unAsK3 :: (Int,Prec) -> Doc e }
+newtype AsK3E e (a :: *) = AsK3E { unAsK3E :: (Int,Prec) -> 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 (AsK3E e) where
+ declVar (Decl (Var v) _) = AsK3E$ const$ text v
+ unsafeVar (Var v) _ = AsK3E$ const$ text v
-instance K3 (AsK3 e) where
-
- cAnn (AsK3 e) anns = AsK3$ \n -> align $
+ cAnn (AsK3E e) anns = AsK3E$ \n -> align $
parens (e n) <> " @ "
<> (encloseSep lbrace rbrace comma $ map annEText anns)
- cComment str (AsK3 a) = AsK3$ \n -> "\n// " <> text str <> "\n" <> a n
+ cComment str (AsK3E a) = AsK3E$ \n -> "\n// " <> text str <> "\n" <> a n
- cAddress (Addr (h,p)) = AsK3$ const$ (text h <> ":" <> pretty p)
+ cAddress (Addr (h,p)) = AsK3E$ const$ (text h <> ":" <> pretty p)
- cBool n = AsK3$ const$ text$ show n
- cByte n = AsK3$ const$ text$ show n
- cFloat n = AsK3$ const$ text$ show n
- cInt n = AsK3$ const$ text$ show n
- cString n = AsK3$ const$ text$ show n
- cNothing = AsK3$ const$ "nothing"
- cUnit = AsK3$ const$ "unit"
+ cBool n = AsK3E$ const$ text$ show n
+ cByte n = AsK3E$ const$ text$ show n
+ cFloat n = AsK3E$ const$ text$ show n
+ cInt n = AsK3E$ const$ text$ show n
+ cString n = AsK3E$ const$ text$ show n
+ cNothing = AsK3E$ const$ "nothing"
+ cUnit = AsK3E$ const$ "unit"
- unsafeVar (Var v) _ = AsK3$ const$ text v
- declVar (Decl (Var v) _ _) = AsK3$ const$ text v
- eJust (AsK3 a) = builtin "just" [ a ]
- eRef (AsK3 a) = builtin "ref" [ a ]
+ eJust (AsK3E a) = builtin "just" [ a ]
+ -- XXX k3ref
+ -- eRef (AsK3E a) = builtin "ref" [ a ]
-- XXX TUPLES Note the similarity of these!
- eTuple2 t = AsK3 $ \(n,_) -> tupled $ tupleopEL (flip unAsK3 (n,PrecLowest)) t
- eTuple3 t = AsK3 $ \(n,_) -> tupled $ tupleopEL (flip unAsK3 (n,PrecLowest)) t
- eTuple4 t = AsK3 $ \(n,_) -> tupled $ tupleopEL (flip unAsK3 (n,PrecLowest)) t
- eTuple5 t = AsK3 $ \(n,_) -> tupled $ tupleopEL (flip unAsK3 (n,PrecLowest)) t
+ eTuple2 t = AsK3E $ \(n,_) -> tupled $ tupleopEL (flip unAsK3E (n,PrecLowest)) t
+ eTuple3 t = AsK3E $ \(n,_) -> tupled $ tupleopEL (flip unAsK3E (n,PrecLowest)) t
+ eTuple4 t = AsK3E $ \(n,_) -> tupled $ tupleopEL (flip unAsK3E (n,PrecLowest)) t
+ eTuple5 t = AsK3E $ \(n,_) -> tupled $ tupleopEL (flip unAsK3E (n,PrecLowest)) t
- eHL t = AsK3 $ \(n,_) -> tupled $ hrlproj (flip unAsK3 (n,PrecLowest)) t
+ eHL t = AsK3E $ \(n,_) -> tupled $ hrlproj (flip unAsK3E (n,PrecLowest)) t
eEmpty = k3cfn_empty
eSing = k3cfn_sing
- eCombine (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> " ++ " <> parens (b n)
- eRange (AsK3 f) (AsK3 l) (AsK3 s) = builtin "range" [ f, l, s ]
+ eCombine (AsK3E a) (AsK3E b) = AsK3E$ \n -> parens (a n) <> " ++ " <> parens (b n)
+ eRange (AsK3E f) (AsK3E l) (AsK3E s) = builtin "range" [ f, l, s ]
eAdd = binop PrecBOAdd "+"
eMul = binop PrecBOMul "*"
- eNeg (AsK3 b) = AsK3$ \(n,p) -> np p PrecNeg $ "-" <> (b (n,PrecNeg))
+ eNeg (AsK3E b) = AsK3E$ \(n,p) -> np p PrecNeg $ "-" <> (b (n,PrecNeg))
eEq = binop PrecBOComp "=="
eLt = binop PrecBOComp "<"
eLeq = binop PrecBOComp "<="
eNeq = binop PrecBOComp "!="
- eLam w f = AsK3$ \(n,p) -> let ((pat, arg),n') = runState (runReaderT (k3pfn w) False) n
- in "\\" <> pat <+> "->" `above` indent 2 (unAsK3 (f arg) (n',p))
+ eLam w f = AsK3E$ \(n,_) -> let ((pat, arg),n') = runState (runReaderT (k3pfn w) False) n
+ in "\\" <> pat <+> "->" `above` indent 2 (unAsK3E (f arg) (n',PrecLowest))
- eApp (AsK3 f) (AsK3 x) = AsK3$ \n ->
+ eApp (AsK3E f) (AsK3E x) = AsK3E$ \n ->
parens (parens (f n) </> parens (x n))
- eBlock ss (AsK3 r) = AsK3$ \(n,_) ->
- "do" <> (semiBraces (map ($ (n,PrecLowest)) ((map unAsK3 ss) ++ [r])))
+ eBlock ss (AsK3E r) = AsK3E$ \(n,_) ->
+ "do" <> (semiBraces (map ($ (n,PrecLowest)) ((map unAsK3E ss) ++ [r])))
- eIter (AsK3 f) (AsK3 c) = builtin "iterate" [ f, c ]
+ eIter (AsK3E f) (AsK3E c) = builtin "iterate" [ f, c ]
- eITE (AsK3 b) (AsK3 t) (AsK3 e) = AsK3$ \(n,p) -> np p PrecITE $
+ eITE (AsK3E b) (AsK3E t) (AsK3E e) = AsK3E$ \(n,p) -> np p PrecITE $
"if" <+> (align $ above (parens (b (n,PrecLowest)))
("then" <+> t (n,PrecLowest) `aboveBreak`
"else" <+> e (n,PrecLowest)))
- eMap (AsK3 f) (AsK3 c) = builtin "map" [ f, c ]
- eFiltMap (AsK3 f) (AsK3 m) (AsK3 c) = builtin "filtermap" [ f, m, c ]
- eFlatten (AsK3 c) = builtin "flatten" [ c ]
- eFold (AsK3 f) (AsK3 z) (AsK3 c) = builtin "fold" [ f, z, c ]
- eGBA (AsK3 p) (AsK3 f) (AsK3 z) (AsK3 c) = builtin "groupby" [ p, f, z, c ]
- eSort (AsK3 c) (AsK3 f) = builtin "sort" [ c, f ]
- ePeek (AsK3 c) = builtin "peek" [ c ]
+ eMap (AsK3E f) (AsK3E c) = builtin "map" [ f, c ]
+ eFiltMap (AsK3E f) (AsK3E m) (AsK3E c) = builtin "filtermap" [ f, m, c ]
+ eFlatten (AsK3E c) = builtin "flatten" [ c ]
+ eFold (AsK3E f) (AsK3E z) (AsK3E c) = builtin "fold" [ f, z, c ]
+ eGBA (AsK3E p) (AsK3E f) (AsK3E z) (AsK3E c) = builtin "groupby" [ p, f, z, c ]
+ eSort (AsK3E c) (AsK3E f) = builtin "sort" [ c, f ]
+ ePeek (AsK3E c) = builtin "peek" [ c ]
- eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (runReader (k3sfn w) False) n)
+ eSlice w (AsK3E c) = AsK3E$ \n -> c n <> brackets (unAsK3E (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 ]
+ eInsert (AsK3E c) (AsK3E e) = builtin "insert" [ c, e ]
+ eDelete (AsK3E c) (AsK3E e) = builtin "delete" [ c, e ]
+ eUpdate (AsK3E c) (AsK3E o) (AsK3E n) = builtin "update" [ c, o, n ]
- eAssign = binop PrecBOComp "<-"
+ -- XXX k3ref
+ -- eAssign = binop PrecBOComp "<-"
- eSend (AsK3 a) (AsK3 f) (AsK3 x) = builtin "send" [ a, f, x ]
-
-------------------------------------------------------------------------}}}
--- Miscellany {{{
+ eSend (AsK3E a) (AsK3E f) (AsK3E x) = builtin "send" [ a, f, x ]
inist :: (Int,Prec)
inist = (0,PrecLowest)
np :: forall a e. Ord a => a -> a -> Doc e -> Doc e
np p p' = (if p > p' then parens else id)
- -- Overly polymorphic; use only when correct!
-binop :: Prec -> Doc e -> AsK3 e a -> AsK3 e b -> AsK3 e c
-binop p' o (AsK3 a) (AsK3 b) =
- AsK3$ \(n,p) -> np p p' $ (align $ a (n,p')) </> o <+> (align $ b (n,succ p'))
+-- Overly polymorphic; use only when correct!
+binop :: Prec -> Doc e -> AsK3E e a -> AsK3E e b -> AsK3E e c
+binop p' o (AsK3E a) (AsK3E b) =
+ AsK3E$ \(n,p) -> np p p' $ (align $ a (n,p')) </> o <+> (align $ b (n,succ p'))
+
+-- Overly polymorphic; use only when correct!
+builtin :: Doc e -> [ (Int,Prec) -> Doc e ] -> AsK3E e b
+builtin fn as = AsK3E$ \(n,_) -> fn <> tupled (map ($ (n,PrecLowest)) as)
+
+{-
+-- | Since the entire type of an AsK3 is phantom, we can, of course, alter
+-- it at a moment's notice. Note that this is generally probably unwise.
+phantom_ask3e :: forall t e a. AsK3E e t -> AsK3E e a
+phantom_ask3e (AsK3E f) = AsK3E f
+
+{- XXX k3ref
+-- | Shift the phantom type for a reference inside AsK3E's interpretation
+phantom_ref :: AsK3E e (Ref (AsK3E e) a) -> AsK3E e (Ref r a)
+phantom_ref = phantom_ask3e
+-}
- -- Overly polymorphic; use only when correct!
-builtin :: Doc e -> [ (Int,Prec) -> Doc e ] -> AsK3 e b
-builtin fn as = AsK3$ \(n,_) -> fn <> tupled (map ($ (n,PrecLowest)) as)
+-- | Shift the phantom type for a collection inside AsK3E's interpretation
+phantom_coll :: AsK3E e (CTE (AsK3E e) c a) -> AsK3E e (CTE r c a)
+phantom_coll = phantom_ask3e
+-}
-instance Show (AsK3 e a) where
- show (AsK3 f) = show $ f inist
+instance Show (AsK3E e a) where
+ show (AsK3E f) = show $ f inist
-sh :: AsK3 e a -> Doc e
-sh f = unAsK3 f inist
+sh :: AsK3E e a -> Doc e
+sh f = unAsK3E f inist
instance Show (AsK3Ty e a) where
show (AsK3Ty f) = show f
sht :: AsK3Ty e a -> Doc e
sht = unAsK3Ty
-shd :: Decl (AsK3Ty e) (AsK3 e) t -> Doc e
-shd (Decl (Var name) tipe body) =
- keyword
- <+> text name
- <+> align (colon <+> unAsK3Ty tipe)
- <> case body of
- DKColl -> empty
- DKRef -> empty
- (DKFunc b) -> renderBody b
- (DKTrig b) -> renderBody b
- <> semi
+declKeyword :: DBody t -> Doc e
+declKeyword (DColl _) = "declare"
+declKeyword (DTrig _) = "trigger"
+-- declKeyword DRef = "declare"
+declKeyword (DFunc _) = "declare"
+
+shdk :: DBody t -> Doc e
+shdk d = case d of
+ (DColl ty) -> align (colon <+> sht (unUTR ty))
+ (DTrig b) -> renderBody b
+ -- XXX k3ref
+ -- shdk DRef = empty
+ (DFunc b) -> renderBody b
where
- keyword = case body of
- DKColl -> "declare"
- DKRef -> "declare"
- (DKFunc _) -> "declare"
- (DKTrig _) -> "trigger"
+ renderBody b = space <> equals `aboveBreak`
+ (indent 2 $ unAsK3E b inist)
- renderBody b = space <> equals `aboveBreak` (indent 2 $ unAsK3 b inist)
+shd :: Decl s t -> Doc e
+shd (Decl (Var name) {- tipe -} body) =
+ declKeyword body
+ <+> text name
+ <+> shdk body
+ <> semi
+ <> line
+
+------------------------------------------------------------------------}}}
+-- Program handling {{{
+
+shex :: ExDecl -> Doc e
+shex (Ex d) = shd d
+
+shk3 :: Prog -> (Doc e, [Doc e])
+shk3 r = (case r of (Prog d) -> shd d,
+ case r of (Prog (Decl _ b)) -> map shex $ M.elems $ cdk b)
+
+{-
+-- | Produce a textual representation of a K3 program, including all
+-- referenced declarations.
+--
+-- XXX I would rather do this differently, if I can, but for the moment,
+-- this suffices.
+data AsK3P e (a :: *) = AsK3P { ask3p_exp :: AsK3E e a
+ , ask3p_decls :: M.Map VarIx (Doc e)
+ }
+
+phantom_pat_prf :: PDat UnivTyRepr w
+ -> PatReprFn (AsK3P e) w
+ -> PatReprFn (AsK3E e) w
+phantom_pat_prf (PVar _) (AsK3P e _) = e
+
+phantom_lam :: PDat UnivTyRepr w
+ -> AsK3E e (PatTy (AsK3E e) w -> b)
+ -> AsK3E e (PatTy (AsK3P e) w -> b)
+phantom_lam _ = phantom_ask3e
+
+mkpc :: Proxy e -> PDat UnivTyRepr w -> PatReprFn (AsK3P e) w
+mkpc _ (PVar _) = AsK3P (AsK3E $ const empty) M.empty
+mkpc _ PUnk = ()
+mkpc p (PJust w) = mkpc p w
+-- XXX k3ref
+-- mkpc p (PRef w) = mkpc p w
+mkpc _ (PHL HRN) = HN
+mkpc p (PHL (w :++ ws)) = mkpc p w :+ mkpc p (PHL ws)
+
+instance K3 (AsK3P e) where
+
+ type K3_M (AsK3P e) = K3_M (AsK3E e)
+
+ cComment = flip const
+ cAnn = const
+
+ cAddress a = AsK3P (cAddress a) M.empty
+ cBool a = AsK3P (cBool a) M.empty
+ -- XXX
+
+ eJust (AsK3P e d) = AsK3P (eJust e) d
+ -- XXX k3ref
+ -- eRef (AsK3P e d) = AsK3P (phantom_ref $ eRef e) d
+
+ eTuple2 (AsK3P e1 d1, AsK3P e2 d2)
+ = AsK3P (eTuple2 (e1,e2))
+ (M.union d1 d2)
+ eTuple3 (AsK3P e1 d1, AsK3P e2 d2, AsK3P e3 d3)
+ = AsK3P (eTuple3 (e1,e2,e3))
+ (M.union d1 $ M.union d2 d3)
+ eTuple4 (AsK3P e1 d1, AsK3P e2 d2, AsK3P e3 d3, AsK3P e4 d4)
+ = AsK3P (eTuple4 (e1,e2,e3,e4))
+ (M.union (M.union d1 d2) (M.union d3 d4))
+ eTuple5 (AsK3P e1 d1, AsK3P e2 d2, AsK3P e3 d3, AsK3P e4 d4, AsK3P e5 d5)
+ = AsK3P (eTuple5 (e1,e2,e3,e4,e5))
+ (M.union d1 $ M.union (M.union d2 d3)
+ (M.union d4 d5))
+
+ eHL xs = AsK3P (eHL $ hrlmap ask3p_exp xs)
+ (M.unions $ hrlproj ask3p_decls xs)
+
+ eEmpty c = AsK3P (phantom_coll $ eEmpty c) M.empty
+ eSing c (AsK3P e d) = AsK3P (phantom_coll $ eSing c e) d
+
+ eLam p f =
+ undefined
+{-
+ let earg x = phantom_pat_prf p x
+ eres x = ask3p_exp (f (earg x))
+
+ in AsK3P (phantom_lam p $ eLam p eres) undefined
+-}
+-}
------------------------------------------------------------------------}}}
-- Template Haskell splices {{{
+
+{-
$(mkLRecInstances (''K3PFn,[]) 'PKTup
('k3pfn,'rec_k3pfn,Nothing,\ls -> TH.tupE [
TH.appE (TH.varE 'tupled)
, TH.tupE $ map (TH.appE (TH.varE 'snd)) ls
]
))
-
$(do
e <- liftM TH.varT $ TH.newName "e"
n <- TH.newName "n"
$ map (\l -> TH.appE (TH.appE (TH.varE 'unAsK3) l) (TH.varE n))
$ ls
))
+-}
---------------------------------------------------------------------------
-- Header material
------------------------------------------------------------------------{{{
+{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TemplateHaskell #-}
import Dyna.BackendK3.AST
import Dyna.BackendK3.Automation
import Dyna.BackendK3.Render
+import Dyna.XXX.HList
import qualified Test.Framework as TF
import Test.Framework.Providers.HUnit
import Test.Framework.TH
displaySimple (SLine _ d) = showChar ' ' . displaySimple d
displaySimple (SEffect _ d) = displaySimple d
-render :: AsK3 e a -> String
-render = despace . flip displaySimple [] . renderCompact . sh
+renderExp :: AsK3E e a -> String
+renderExp = despace . flip displaySimple [] . renderCompact . sh
where
despace [] = []
despace [x] = [x]
-- Basic handling {{{
case_mfn :: Assertion
-case_mfn = e @=? render k3
+case_mfn = e @=? renderExp k3
where
e = "\\x0:int -> -(x0 + 1)"
-- Note that we cannot automate the tInt here, since K3's math
k3 = eLam (PVar tInt) (\a -> eNeg $ eAdd a $ cInt 1)
case_pairfn :: Assertion
-case_pairfn = e @=? render k3
+case_pairfn = e @=? renderExp k3
where
- e = "\\(x0:int ,x1:bool) -> x0"
- k3 = eLam (PVar tInt, PVar tBool) (\(a,_) -> a)
+ e = "\\(x0:int,x1:bool) -> x0"
+ k3 = eLam (PHL $ PVar tInt :++ PVar tBool :++ HRN) (\(a:+_:+_) -> a)
------------------------------------------------------------------------}}}
-- Macro expansion test cases {{{
case_mcm :: Assertion
-case_mcm = e @=? render k3
+case_mcm = e @=? renderExp k3
where
- e = "if (test == nothing) then (0) "
- <> "else (((\\just (x0:int) -> x0) (test)))"
+ e = "if (test == nothing) then 0 "
+ <> "else ((\\just (x0:int) -> x0) (test))"
k3 = caseMaybe tInt (unsafeVar (Var "test") autoty) (cInt 0) (id)
------------------------------------------------------------------------}}}
+++ /dev/null
----------------------------------------------------------------------------
--- | A standard library for the K3 backend. A collection of canned
--- routines.
---
--- Unlike Dyna.BackendK3.Automation, this is intended specifically for the
--- purpose of implementing Dyna-on-K3.
-
--- Header material {{{
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-
-module Dyna.BackendK3.Stdlib (
- -- * Generic term storage
- -- ** Haskell type level
- TermIx, ArgIx, FAIx, TXRef, IndTy, IndTyRow, IndTyRowSet,
-
- -- ** K3 type level
- ttermix, targix, tfaix, txref, indty,
-
- -- ** K3 data representation
- fatab, faixCtr, heap,
-
- -- ** K3 representation mathematics
- foldMath, foldMathSum, foldMathProd,
-
- -- ** K3 heap utilities
- allocTermixHelper, allocTermix, allocFaix, findFaix, initHeapRow,
-
- -- ** Metaprogramming term representation utilities
- -- *** Data Injections
- indterm, indint, indflt, indstr,
- -- *** Slice Injections
- sindterm, sindint, sindflt, sindstr,
- -- *** Projectors
- proterm, proint, proflt, prostr,
-
- -- ** Metaprogramming heap utilities
- hproindr, hpropara, hproeval
-
-) where
-
-import Control.Monad.State
-import Dyna.BackendK3.AST
-import Dyna.BackendK3.Automation
-import Dyna.XXX.HList
-import Dyna.XXX.MonadUtils
-import Dyna.XXX.THTuple
-
-------------------------------------------------------------------------}}}
--- Generic term storage, Haskell type level {{{
-
-type TermIx = Int
-type ArgIx = Int
-type FAIx = Int
-type TXRef = (FAIx, TermIx)
-type IndTy = HList '[Maybe TXRef, Maybe Int, Maybe Float, Maybe String]
-type IndTyRow = (Int, Int, IndTy)
-type IndTyRowSet r = CTE r CSet IndTyRow
-
-------------------------------------------------------------------------}}}
--- Generic term storage, K3 type level {{{
---
--- The type-annotations here serve to make the Haskell toolchain's output
--- prettier; being type aliases, though, there is no semantic difference
--- between these and the inferred types.
-
--- | TERM IndeX
-ttermix :: (K3Ty r) => r TermIx
-ttermix = tInt
-
--- | ARGument IndeX
-targix :: (K3Ty r) => r ArgIx
-targix = tInt
-
--- | Functor and Arity IndeX
-tfaix :: (K3Ty r) => r FAIx
-tfaix = tInt
-
--- | Term crossreference
-txref = tTuple2 $ (tfaix, ttermix)
-
--- | A node in a recursive term structure
---
--- This needs more base-cases.
-indty :: K3Ty r => r IndTy
-indty = tHL
- ( tMaybe txref -- Term xref
- :++ tMaybe tInt -- Base int
- :++ tMaybe tFloat -- Base float
- :++ tMaybe tString -- Base string
- :++ HRN
- )
- `tAnn` [AOneOfHL]
-
-------------------------------------------------------------------------}}}
--- Generic term storage, K3 data representation {{{
-
--- | For each pair of functor and arity, what is the name we've given?
---
--- Used when we don't know static assignments
-fatab = flip (Decl $ Var "fatab") DKColl $
- tColl CTSet (tTuple3 (tfaix, tString, tInt))
- `tAnn` [ AFunDep (FDDom,FDCod,FDCod)
- , AFunDep (FDCod,FDDom,FDDom)
- ]
-
--- | A counter for dynamic allocation of faixes
-faixCtr = mkdecl $ \r -> Decl (Var "faixCtr") (tRef tfaix `asRefR` r) DKRef
-
--- | The place we store all our terms, partitioned globally by functor-arity
--- values. For each faix, we store
---
--- * a counter for the next possibly-free termix,
---
--- * a table of arguments
---
--- * a table of parasitic functors (which should be thought of as Dyna's
--- version of newtypes: top-level f/1 which are eliminated from
--- evaluations at compile time.)
---
--- * a table of evaluations (including parasitic evaluations)
-heap = mkdecl $ \r -> flip (Decl $ Var "heap") DKColl $
- (tColl CTSet $
- tHL ( tfaix
- :++ tRef ttermix `asRefR` r
-
- -- Indirection
- :++ tRef ((tColl CTSet $ tTuple3 (ttermix, targix, indty))
- `tAnn` [AFunDep (FDDom,FDDom,FDCod)]
- `asCollR` r) `asRefR` r
-
- -- Parasitism (used when we don't statically know the parasitic
- -- storage "offset")
- :++ tRef ((tColl CTSet $ tTuple2 (tString, tInt))
- `tAnn` [AFunDep (FDDom,FDCod)]
- `asCollR` r) `asRefR` r
-
- -- Evaluation (including parasitism)
- :++ tRef ((tColl CTSet $ tTuple3 (ttermix, tInt, indty))
- `tAnn` [AFunDep (FDDom,FDDom,FDCod)]
- `asCollR` r) `asRefR` r
-
- :++ HRN
- ))
- `tAnn` [AFunDepHL (FDDom :++ FDCod :++ FDCod :++ FDCod :++ FDCod :++ HRN)
- , AXrefF fatab
- (autopv, PUnk, PUnk)
- (\(x,_,_) -> x)
- (PVar autoty:+PUnk:+PUnk:+PUnk:+PUnk:+HN)
- (\(x:+_) -> x)
- ]
- `asCollR` r
-
-------------------------------------------------------------------------}}}
--- Generic term storage, term representation mathematics {{{
-
-foldMath (s,fn :: forall a b . (BiNum a b) => r a -> r b -> r (BNTF a b))
- = Decl (Var $ "foldMath" ++ s) (tFun (tTuple2 (indty, indty)) indty) $ DKFunc $
- eLam (PVar indty, PVar indty) $ \(a,b) ->
- localVar (pronum a) $ \aif ->
- localVar (pronum b) $ \bif ->
- eITE (aif `eEq` eTuple2 (cNothing, cNothing)) (indstr $ cString "Error") $
- eITE (bif `eEq` eTuple2 (cNothing, cNothing)) (indstr $ cString "Error") $
- eApp (eLam (PVar $ tMaybe tInt, PVar $ tMaybe tFloat) $ \(mai,maf) ->
- caseMaybe tInt mai (eApp (eLam (PJust $ PVar tFloat)
- $ \a -> commonB a indflt bif
- ) maf)
- $ \a -> commonB a indint bif
- ) aif
- where
- commonB :: (K3 r, BiNum a Float, BNTF a Float ~ Float, BiNum a Int)
- => r a
- -> (r (BNTF a Int) -> r IndTy)
- -> r (Maybe Int, Maybe Float)
- -> r IndTy
- commonB a f bif =
- eApp (eLam (PVar $ tMaybe tInt, PVar $ tMaybe tFloat) $ \(mbi,mbf) ->
- caseMaybe tInt mbi
- (eApp (eLam (PJust $ PVar tFloat) $ \b -> indflt $ a `fn` b) mbf)
- (\b -> f $ a `fn` b)
- ) bif
-
-
-foldMathSum = foldMath ("sum" , eAdd)
-foldMathProd = foldMath ("prod", eMul)
-
-------------------------------------------------------------------------}}}
--- Generic term storage, metaprogramming term representation {{{
-
-indterm :: K3 r => r TXRef -> r IndTy
-indterm x = eHL (eJust x :++ cNothing :++ cNothing :++ cNothing :++ HRN)
-
-indint :: K3 r => r Int -> r IndTy
-indint x = eHL (cNothing :++ eJust x :++ cNothing :++ cNothing :++ HRN)
-
-indflt :: K3 r => r Float -> r IndTy
-indflt x = eHL (cNothing :++ cNothing :++ eJust x :++ cNothing :++ HRN)
-
-indstr :: K3 r => r String -> r IndTy
-indstr x = eHL (cNothing :++ cNothing :++ cNothing :++ eJust x :++ HRN)
-
-sindterm :: (K3 r, PatDa w ~ PVar r TXRef)
- => r TXRef
- -> HList [PJust w, PVar r (Maybe Int), PVar r (Maybe Float), PVar r (Maybe String)]
-sindterm x = (PJust (PVar x) :+ PVar cNothing :+ PVar cNothing :+ PVar cNothing :+ HN)
-
-sindint x = (PVar cNothing :+ PJust (PVar x) :+ PVar cNothing :+ PVar cNothing :+ HN)
-sindflt x = (PVar cNothing :+ PVar cNothing :+ PJust (PVar x) :+ PVar cNothing :+ HN)
-sindstr x = (PVar cNothing :+ PVar cNothing :+ PVar cNothing :+ PJust (PVar x) :+ HN)
-
-proterm (x :: r IndTy) =
- flip eApp x $ eLam (PJust (PVar $ tTuple2 (tfaix,ttermix)) :+ PUnk :+ PUnk :+ PUnk :+ HN)
- (\(i:+_:+_:+_:+HN) -> i)
-proint (x :: r IndTy) =
- flip eApp x $ eLam (PUnk :+ PJust (PVar tInt) :+ PUnk :+ PUnk :+ HN)
- (\(_:+i:+_:+_:+HN) -> i)
-proflt (x :: r IndTy) =
- flip eApp x $ eLam (PUnk :+ PUnk :+ PJust (PVar tFloat) :+ PUnk :+ HN)
- (\(_:+_:+i:+_:+HN) -> i)
-prostr (x :: r IndTy) =
- flip eApp x $ eLam (PUnk :+ PUnk :+ PUnk :+ PJust (PVar tString) :+ HN)
- (\(_:+_:+_:+i:+HN) -> i)
-
-pronum (x :: r IndTy) =
- flip eApp x $ eLam (PUnk :+ PVar (tMaybe tInt) :+ PVar (tMaybe tFloat) :+ PUnk :+ HN)
- (\(_:+i:+j:+_:+HN) -> eTuple2 (i,j))
-
-------------------------------------------------------------------------}}}
--- Generic term storage, heap utility functions {{{
-
--- | Set up a new faix on the heap
-initHeapRow = Decl (Var "initHeapRow") (tFun tfaix tUnit) $ DKFunc $
- eLam autopv (\faix -> eInsert (declVar heap)
- $ eHL $ faix
- :++ eRef (cInt 0)
- :++ eRef eEmpty
- :++ eRef eEmpty
- :++ eRef eEmpty
- :++ HRN)
-
-
-
-
--- | Find us a free faix, starting at (deref faixCtr)
-allocFaix = mkfdecl $ \_ s -> Decl (Var "allocFaix") (tFun tUnit tfaix) $ DKFunc $
- eLam PUnk $ \_ ->
- eApp (eLam (PRef $ PVar tfaix)
- (\fa -> eBlock [ eAssign cr (fa `eAdd` cInt 1) ]
- $ eITE (eEmpty `eEq` eSlice (PVar fa,PUnk,PUnk)
- (declVar fatab))
- (fa)
- (eApp s cUnit)))
- cr
- where cr = declVar faixCtr
-
-findFaix = mkdecl $ \_ -> Decl (Var "findFaix") (tFun (tTuple2 (tString, tInt)) tfaix) $ DKFunc $
- eLam (autopv, autopv) $ \(f,n) -> localVar (search f n) (\sr -> emptyPeek sr (create f n) id)
- where
- search f n = eMap (eLam (PVar tfaix,PUnk,PUnk) (\(x,_,_) -> x))
- $ eSlice (PUnk, PVar f, PVar n) (declVar fatab)
- create f n = localVar (eApp (declVar allocFaix) cUnit)
- (\i -> eBlock [eInsert (declVar fatab) (eTuple3 (i,f,n))] i)
-
-
-allocTermixHelper = mkfdecl $ \_ s ->
- Decl (Var "allocTermixHelper")
- (tFun (tTuple2 (tRef ttermix, tColl CTSet $ tTuple3 (ttermix, targix, indty)))
- ttermix)
- $ DKFunc $
- eLam (autopv,autopv) $ \(tr,ts) -> localVar (deref tr)
- $ \ti -> eBlock [ eAssign tr (ti `eAdd` cInt 1) ]
- $ eITE (eEmpty `eEq` eSlice (PVar ti, PUnk, PUnk) ts)
- ti
- (eApp s $ eTuple2 (tr,ts))
-
--- | Find us a free termix in a given faix
-allocTermix = mkfdecl $ \_ s -> Decl (Var "allocTermix") (tFun tfaix ttermix) $ DKFunc $
- eLam autopv $ \fa ->
- eApp (declVar allocTermixHelper)
- (ePeek $ eMap (eLam (PUnk :+ PVar (tRef ttermix) :+ PVar autoty :+ PUnk :+ PUnk :+ HN) $ \(_:+r:+s:+_) -> eTuple2 (r,deref s))
- $ eSlice (PVar fa:+PUnk:+PUnk:+PUnk:+PUnk:+HN) (declVar heap))
-
-------------------------------------------------------------------------}}}
--- Generic term storage, metaprogramming heap utility functions {{{
-
--- | Extract the indirection table for a given faix
-hproindr faix = localVar $ ePeek $
- eMap (eLam (PUnk :+ PUnk :+ PVar autoty :+ PUnk :+ PUnk :+ HN)
- (\(_:+_:+ts:+_:+_:+HN) -> ts))
- $ eSlice (PVar faix :+ PUnk :+ PUnk :+ PUnk :+ PUnk :+ HN)
- (declVar heap)
-
--- | Extract the parasitism table for a given faix
-hpropara faix = localVar $ ePeek $
- eMap (eLam (PUnk :+ PUnk :+ PUnk :+ PVar autoty :+ PUnk :+ HN)
- (\(_:+_:+_:+ps:+_:+HN) -> ps))
- $ eSlice (PVar faix :+ PUnk :+ PUnk :+ PUnk :+ PUnk :+ HN)
- (declVar heap)
-
--- | Extract the evaluation table for a given faix
-hproeval faix = localVar $ ePeek $
- eMap (eLam (PUnk :+ PUnk :+ PUnk :+ PUnk :+ PVar autoty :+ HN)
- (\(_:+_:+_:+_:+es:+HN) -> es))
- $ eSlice (PVar faix :+ PUnk :+ PUnk :+ PUnk :+ PUnk :+ HN)
- (declVar heap)
-
-
-------------------------------------------------------------------------}}}
projects / dyna2 / commitdiff