+++ /dev/null
----------------------------------------------------------------------------
--- | An AST for K3.
---
--- 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.
---
--- 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 DataKinds #-}
-{-# 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.Backend.K3.AST (
- -- * Preliminaries
- VarIx(..), AddrIx(..), Target,
-
- -- * Numeric Autocasting
- BiNum(..), UnNum(..),
-
- -- * Collections
- CTE, CKind(..), CollTy(..), asColl,
-
-{- XXX k3ref
- -- * References
- Ref,
--}
-
- -- * Pattern System
- PKind(..), Pat(..), PDat(..),
- MapPatConst,
-
- -- * Annotations
- AnnT(..), AnnE(..), FunDepSpec(..),
-
- -- * Type System: Base constraints
- K3BaseTy,
-
- -- * Type System: Representations
- K3Ty(..), UnivTyRepr(..),
-
- -- * Expressions
- K3(..),
-
-{- XXX
- -- * Roles and Streams
- -- SFormat(..), Stream(..), K3RoleDesc(..),
--}
-
- -- * Declarations
- Decl(..), DBody(..), asR, asCollR, {- asRefR, -}
- mkCollDecl, mkRefDecl, mkTrigDecl, mkFuncDecl, -- unUDR,
-
- K3Proxied, K3Unproxy,
-
- -- * 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
-
-------------------------------------------------------------------------}}}
--- Preliminaries {{{
-
- -- XXX
-newtype VarIx = Var String
- deriving (Eq,Ord,Show)
-
- -- XXX (Hostname,Port)
-newtype AddrIx = Addr (String,Int)
- deriving (Eq,Show)
-
-------------------------------------------------------------------------}}}
--- Type System: Base Constraints {{{
-
--- | A constraint for /base/ types in K3. These are the things that can
--- be passed to lambdas. Essentially everything other than arrows.
-class K3BaseTy a
-instance K3BaseTy Bool
-instance K3BaseTy Word8
-instance K3BaseTy Float
-instance K3BaseTy Int
-instance K3BaseTy String
-instance K3BaseTy ()
-instance (K3BaseTy a) => K3BaseTy (Maybe a)
-instance K3BaseTy (HList '[])
-instance (K3BaseTy a, K3BaseTy (HList as)) => K3BaseTy (HList (a ': as))
--- See THSPLICE
-
-------------------------------------------------------------------------}}}
--- Type System: Proxified Representations {{{
-
--- XXX These will be a lot nicer once we get overlapping groups of type
--- families. Real Soon Now, I hope.
-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) = (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 {{{
-
--- | The 'r' representation of a target taking argument type 't'.
---
--- This is similar to @t -> ()@ except that it executes in a different
--- transaction and must be named. The only safe source of Targets is a
--- 'Decl', but being first class, they can be stored in collections for
--- dynamic dispatch.
-data family Target (r :: * -> *) t :: *
-
-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 = 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
- -- | 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)
-
-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.
---
--- Use as (eEmpty `asColl` CTSet)
-asColl :: r (CTE r c t) -> CollTy c -> r (CTE r c t)
-asColl = const
-
-------------------------------------------------------------------------}}}
--- References {{{
-
--- XXX k3ref At the moment K3 only supports global refs. This is enforced
--- in Haskell by allowing Refs to only be made as declarations; this will
--- change eventually.
-
--- | 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 {{{
-
--- | Kinds of patterns permitted in K3
-data PKind where
- -- | Variables in patterns (see 'PVar')
- PKVar :: r -> k -> PKind
-
- -- | Wildcards in patterns (see 'PUnk')
- PKUnk :: k -> PKind
-
- -- | Just patterns (see 'PJust')
- PKJust :: PKind -> PKind
-
- -- | Ref patterns (see 'PRef')
- PKRef :: PKind -> PKind
-
- -- | HList patterns
- PKHL :: [PKind] -> PKind
-
- -- | Product ("tuple") patterns
- --
- -- 'PatTy' and 'PatReprFn' both produce tuples.
- PKTup :: [PKind] -> PKind
-
--- | 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)
-
- -- | 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'.
---
--- Essentially, these things determine where 's's end up
--- in the lambda given to eLam. Compare and contrast:
---
--- > eLam (PVar $ tMaybe tInt) :: (s (Maybe Int) -> _) -> _
--- > eLam (PJust $ PVar tInt) :: (s 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.
---
-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)
- type PatBTy (s :: * -> *) w :: *
- -- | The type of this pattern.
- type PatReprFn (s :: * -> *) w :: *
-
-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
-
-instance (K3BaseTy a) => Pat (PKUnk (a :: *)) where
- type PatTy s (PKUnk a) = a
- type PatBTy s (PKUnk a) = ()
- type PatReprFn s (PKUnk a) = ()
-
-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
-
-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 TMapPatTy (s :: * -> *) (x :: [PKind]) :: *
--- see THSPLICE
-
-type family TMapPatBTy (s :: * -> *) (x :: [PKind]) :: *
--- see THSPLICE
-
-type family TMapPatReprFn (r :: * -> *) (x :: [PKind]) :: *
--- see THSPLICE
-
-type family MapPatConst (x :: [PKind]) :: Constraint
-type instance MapPatConst '[] = ()
-type instance MapPatConst (x ': xs) = (Pat x, MapPatConst xs)
-
-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 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 (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)
-
-------------------------------------------------------------------------}}}
--- 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'), 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)
-
--- | Annotations on 'K3Ty' types
-data AnnT a where
-
- -- | A functional dependency among elements of a collection.
- AFunDep :: (RTupled fs, RTR fs ~ FunDepSpec, RTE fs ~ a)
- => fs -> AnnT (CTE r t a)
-
- -- | Request an additional index on a collection
- AIndex :: (RTupled fs, RTR fs ~ FunDepSpec, RTE fs ~ a)
- => fs -> AnnT (CTE r t a)
-
- -- | An Exactly-One-Of annotation, used to convey variants (i.e. sums)
- -- to K3.
- AOneOf :: (RTupled mv, RTR mv ~ Maybe) => AnnT mv
-
- -- | 'AFunDep' for HList representations
- AFunDepHL :: HRList FunDepSpec a -> AnnT (CTE r t (HList a))
-
- -- | 'AIndex' for HList representations
- AIndexHL :: HRList FunDepSpec a -> AnnT (CTE r t (HList a))
-
- -- | '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 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.
- --
- -- 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)
- AEMisc :: String -> AnnE 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 -> [AnnT a] -> r a
-
- tAddress :: r AddrIx
- tBool :: r Bool
- tByte :: r Word8
- tFloat :: r Float
- tInt :: r Int
- tString :: r String
- tTarget :: r t -> r (Target r' t)
- tUnit :: r ()
-
- -- tPair :: r a -> r b -> r (a,b)
- tMaybe :: r a -> r (Maybe 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)
-
- -- 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
- tTarget (UTR t) = UTR $ tTarget t
- 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
- -- XXX k3ref
- -- 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 {{{
-
--- | 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
-class BiNum a b where
- type BNTF a b :: *
- biadd :: a -> b -> BNTF a b
- bimul :: a -> b -> BNTF a b
-
--- | And and Or are captured as binary numerics
-instance BiNum Bool Bool where
- type BNTF Bool Bool = Bool
- biadd = (||)
- bimul = (&&)
-
-instance BiNum Int Int where
- type BNTF Int Int = Int
- biadd = (+)
- bimul = (*)
-
-instance BiNum Int Float where
- type BNTF Int Float = Float
- biadd a b = ((fromIntegral a) + b)
- bimul a b = ((fromIntegral a) * b)
-
-instance BiNum Float Float where
- type BNTF Float Float = Float
- biadd = (+)
- bimul = (*)
-
-instance BiNum Float Int where
- type BNTF Float Int = Float
- biadd a b = (a + (fromIntegral b))
- bimul a b = (a * (fromIntegral b))
-
-------------------------------------------------------------------------}}}
--- Expressions {{{
-
--- | Data level representation of K3 expression, indexed by equivalent
--- type in Haskell.
-class K3 (r :: * -> *) where
-
- -- XXX To ensure uniqueness of declarations, we pull the ST trick with an
- -- existential skolem. Of course, that means that all of our
- -- representations have to be marked. We don't yet do this.
- --
- -- type K3ReprSrc r :: *
- --
- -- Once we have that, add (s ~ K3ReprSrc r) to declVar.
-
- -- | Reference a declaration by using its name. In emitted K3, this is
- -- just a variable. See "Dyna.BackendK3.CollectDecls" for an interpreter
- -- which gathers the transitive closure of declarations used in a program
- -- fragment.
- 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
- cAnn :: r a -> [AnnE a] -> r a
-
- cAddress :: AddrIx -> r AddrIx
- cBool :: Bool -> r Bool
- cByte :: Word8 -> r Word8
- cFloat :: Float -> r Float
- cInt :: Int -> r Int
- cNothing :: r (Maybe a)
- cString :: String -> r String
- cUnit :: r ()
-
- eJust :: r a -> r (Maybe a)
- -- XXX k3ref
- -- 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)
- eTuple5 :: (r a, r b, r c, r d, r e) -> r (a,b,c,d,e)
- -- eTuple :: K3RTuple r a -> r a
-
- eHL :: HRList r a -> r (HList a)
-
- 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)
-
- eAdd :: (BiNum a b) => r a -> r b -> r (BNTF a b)
- eMul :: (BiNum a b) => r a -> r b -> r (BNTF a b)
- eNeg :: (UnNum a) => r a -> r a
-
- -- XXX Constraints?
- eEq :: (K3BaseTy a) => r a -> r a -> r Bool
- eLt :: (K3BaseTy a) => r a -> r a -> r Bool
- eLeq :: (K3BaseTy a) => r a -> r a -> r Bool
- eNeq :: (K3BaseTy a) => r a -> r a -> r Bool
-
- -- | 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 :: (Pat w)
- => PDat UnivTyRepr 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')
- eFiltMap :: r (t -> Bool) -> r (t -> t') -> r (CTE r c t) -> r (CTE r c t')
-
- eFlatten :: r (CTE r c (CTE r c' t)) -> r (CTE r c' t)
-
- -- | 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.
- --
- -- 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 (CTE r c t) -- ^ Input collection
- -> r (CTE r c (t'',t'))
-
- -- | Sort a collection into a list.
- eSort :: r (CTE r c t) -- ^ Input collection
- -> r ((t,t) -> Bool) -- ^ Less-or-equal
- -> r (CTE r 'CKList t)
-
- -- | 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 r 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" :)
- 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)
-
- 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 ()
-
- -- | 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.
---
--- 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? [r t] ->
- DColl :: (pt ~ K3Proxied t)
- => UnivTyRepr (CTE r c t) -> DBody (CTE Proxy (c :: CKind) pt)
-
- -- | Global References, with initializer
- DRef :: UnivTyRepr pt
- -> (forall r . (K3 r) => r (K3Unproxy r pt))
- -> DBody (Ref Proxy pt)
-
- -- | Triggers, which execute in a different transaction than the caller
- --
- -- XXX does not support local variables
- DTrig :: (Pat w, pt ~ PatTy Proxy w)
- => PDat UnivTyRepr w
- -> (forall r . (K3 r) => PatReprFn r w -> r ())
- -> DBody (Target Proxy pt)
-
- -- | Functions, which execute in the same transaction as the caller
- DFunc :: (Pat w, pa ~ PatTy Proxy w, K3BaseTy pa, K3BaseTy pb)
- => UnivTyRepr pa
- -> UnivTyRepr pb
- -> PDat UnivTyRepr w
- -> (forall r . (K3 r) => PatReprFn r w -> r (K3Unproxy r pb))
- -> DBody (pa -> pb)
-
-{- XXX
- -- | Role declaration
- DRole :: (K3RoleDesc ro) => String -> ro Role -> DBody Role
--}
-
--- | A top-level declaration.
---
--- 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)
-
-newtype MkK3T m s a = MkK3T { unMkK3T :: StateT DeclIx m a }
- deriving (Monad, MonadState DeclIx)
-
--- | Define a collection
---
--- Note that this is polymorphic in r rather than using it as an
--- existential. This may seem rather odd, until one remembers that the only
--- ways of building UnivTyReprs are all polymorphic in r, too. Thus we
--- don't actually risk anything bad when we proxy and unproxy r out of the
--- way. In fact, the 'K3Unproxy' constraint is here only to ensure that we
--- get yelled at if we inadvertently write a collection that mixes
--- representations (or could mix representations using polymorphism); use
--- 'asCollR' and 'asR' and friends.
-mkCollDecl :: (Monad m, pt ~ K3Proxied t, t ~ K3Unproxy r pt)
- => String
- -> (Proxy r -> UnivTyRepr (CTE r c t))
- -> MkK3T m s (Decl s (CTE Proxy c pt))
-mkCollDecl n f = do
- (DeclIx uniq) <- incState
- let v = Var $ n ++ "_" ++ show uniq
- return $ Decl v $ DColl $ f Proxy
-
-mkRefDecl :: (Monad m)
- => String
- -> UnivTyRepr pt
- -> (forall r . (K3 r) => r (K3Unproxy r pt))
- -> MkK3T m s (Decl s (Ref Proxy pt))
-mkRefDecl n ty i = do
- (DeclIx uniq) <- incState
- let v = Var $ n ++ "_" ++ show uniq
- return $ Decl v (DRef ty i)
-
--- | Define a trigger
-mkTrigDecl :: (Monad m, K3BaseTy pt, Pat w, pt ~ PatTy Proxy w)
- => String
- -> PDat UnivTyRepr w
- -> (forall r . (K3 r) => PatReprFn r w -> r ())
- -> MkK3T m s (Decl s (Target Proxy pt))
-mkTrigDecl n p f = do
- (DeclIx uniq) <- incState
- let v = Var $ n ++ "_" ++ show uniq
- return $ Decl v (DTrig p f)
-
--- | Define a function
-mkFuncDecl :: (Monad m, Pat w, pa ~ PatTy Proxy w, K3BaseTy pa, K3BaseTy pb)
- => String
- -> UnivTyRepr pa
- -> UnivTyRepr pb
- -> PDat UnivTyRepr w
- -> (forall r . (K3 r) => PatReprFn r w -> r (K3Unproxy r pb))
- -> MkK3T m s (Decl s (pa -> pb))
-mkFuncDecl n ta tb pa f = do
- (DeclIx uniq) <- incState
- let v = Var $ n ++ "_" ++ show uniq
- return $ Decl v (DFunc ta tb pa f)
-
-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
---
--- 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) -> Proxy r -> s (CTE r c t)
-asCollR = const
-
-{-
- - XXX k3ref
--- | Ensure that the representation type of a ref matches
-asRefR :: s (Ref r t) -> Proxy r -> s (Ref r t)
-asRefR = const
--}
-
-------------------------------------------------------------------------}}}
--- Template Haskell splices (THSPLICE) {{{
-
-$(mkTupleRecInstances ''K3BaseTy [])
-$(mkTyMapFlat 1 ''TMapPatTy ''PatTy)
-$(mkTyMapFlat 1 ''TMapPatBTy ''PatBTy)
-$(mkTyMapFlat 1 ''TMapPatReprFn ''PatReprFn)
-
-------------------------------------------------------------------------}}}
+++ /dev/null
----------------------------------------------------------------------------
--- | Various automation assists for working with K3 ASTs
-
--- Header material {{{
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Dyna.Backend.K3.Automation (
- -- * Automated derivation of data from types, where possible
- K3AutoColl, autocoll, K3AutoTy, autoty,
-
- -- * Pattern handling
- autopv,
-
- -- * K3 macro library
- localVar, caseMaybe, emptyPeek, {- XXX k3ref deref, -} combMany, switchCase
-) where
-
-import Data.Word
-import Dyna.Backend.K3.AST
-import Dyna.XXX.HList
--- import Dyna.XXX.THTuple
-
-------------------------------------------------------------------------}}}
--- 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 should be a total function)
-class K3AutoColl (c :: CKind) where autocoll :: CollTy c
-instance K3AutoColl CKBag where autocoll = CBag
-instance K3AutoColl CKList where autocoll = CList
-instance K3AutoColl CKSet where autocoll = CSet
-
-------------------------------------------------------------------------}}}
--- 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 should be a total function)
-class K3AutoTy a where autoty :: UnivTyRepr a
-instance K3AutoTy Bool where autoty = tBool
-instance K3AutoTy Word8 where autoty = tByte
-instance K3AutoTy Float where autoty = tFloat
-instance K3AutoTy Int where autoty = tInt
-instance K3AutoTy String where autoty = tString
-instance K3AutoTy () where autoty = tUnit
-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
--- 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
- 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
- | ws -> a, a -> ws
- where autotytup :: K3RTuple UnivTyRepr a
-
-instance K3AutoTyTup '[] () where autotytup = K3RTNil
-
-instance (K3AutoTyTup was as, K3AutoTy a, wa ~ PKVar a, PatTy wa ~ a)
- => K3AutoTyTup (wa ': was) (a,as)
- where autotytup = K3RTCons autoty autotytup
-
-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
--- elimination patterns.
-
-{-
-
-type family UnPatReprFn (s :: * -> *) (pr :: *) :: PKind
-type instance UnPatReprFn s (s a) = PKVar UnivTyRepr a
-type instance UnPatReprFn s (HList '[]) = PKHL '[]
-
-class (Pat UnivTyRepr w) => K3AutoPat (w :: PKind) where
- autopat :: PatDa w
-
-instance (K3BaseTy a, K3AutoTy a) => K3AutoPat (PKVar UnivTyRepr a) where
- autopat = PVar autoty
-
-instance K3AutoPat (PKHL '[]) where
- autopat = HN
-
-instance (K3AutoPat (PKHL ws),
- K3AutoPat w,
- MapPatConst ws UnivTyRepr)
- => K3AutoPat (PKHL (w ': ws)) where
- autopat = autopat :+ autopat
-
-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 :: (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)
- => (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)
- => UnivTyRepr a
- -> (r a)
- -> (r a -> r b)
- -> r b
-localVar' w a b = eApp (eLam (PVar w) b) a
--}
-
--- | Case analyze a Maybe
-caseMaybe :: (K3 r, K3BaseTy 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
-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 autocoll)
- e
- (eApp (eLam (PVar autoty) l) $ ePeek c)
-
-{- XXX k3ref
--- | Dereference a value by using a Ref pattern on a lambda.
-deref :: (K3AutoTy a, K3BaseTy a, K3 r)
- => r (Ref r a) -> r a
-deref = eApp (eLam (PRef $ PVar autoty) id)
--}
-
--- | Combine many things
-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) {{{
-
-{-
-data ExVarTy = forall t . EVT VarIx (UnivTyRepr t)
-
-showEVT :: ExVarTy -> Doc e
-showEVT evt = case evt of EVT (Var vn) utr -> text vn
- <+> colon
- <+> unAsK3Ty (unUTR utr)
-
-newtype VarsInK3 a = VIK [ExVarTy]
-
-sVIK :: VarsInK3 t -> Doc e
-sVIK (VIK vs) = list $ map showEVT vs
-
-instance K3 VarsInK3 where
- type K3AST_Coll_C VarsInK3 c = ()
-
- cComment _ v = v
- cAnn _ a = a
-
- cBool _ = VIK []
- cByte _ = VIK []
- cFloat _ = VIK []
-
- eVar vi r = let x = VIK [EVT vi r] in x
-
- eIter (VIK f) (VIK c) = VIK $ f ++ c
-
- -- XXX etc
--}
-
-------------------------------------------------------------------------}}}
+++ /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.Backend.K3.CollectDecls where
-
-import qualified Data.Map as M
-
-import Dyna.Backend.K3.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 (PRef 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 (PRef 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]
-
- 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
-cdk (DRef _ i) = unC i
-cdk (DFunc _ _ p f) = unC (f $ mkpc p)
-cdk (DTrig p f) = unC (f $ mkpc p)
+++ /dev/null
----------------------------------------------------------------------------
--- Header material
-------------------------------------------------------------------------{{{
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-
-module Dyna.Backend.K3.Examples where
-
-import Dyna.BackendK3.AST
-import Dyna.BackendK3.Automation
-import Dyna.BackendK3.Render
-import Text.PrettyPrint.Free
-
-------------------------------------------------------------------------}}}
--- Example cases: misc
-------------------------------------------------------------------------{{{
-
-
- -- | Perform a simple join of two collections using a predicate and apply
- -- some function to rows that match.
- --
- -- This is intended to be sufficiently simple for K3 to chew on and
- -- do something useful with in its optimizer backend.
-macro_simple_join2 :: (K3 r, K3AutoTy a, K3BaseTy a, K3AST_Pat_C r (PKVar a),
- K3AutoTy b, K3BaseTy b, K3AST_Pat_C r (PKVar b))
- => r (a -> b -> Bool) -> r (a -> b -> ())
- -> r (CTE c1 a) -> r (CTE c2 b) -> r ()
-macro_simple_join2 p f c1 c2 =
- flip eIter c1 $ eLam (PVar autoty) $ \a ->
- flip eIter c2 $ eLam (PVar autoty) $ \b ->
- eITE (eApp (eApp p a) b) (eApp (eApp f a) b) (cUnit)
-
-
-testdecf = Decl (Var "f")
- (tColl CTBag (tTuple2 (tInt,tInt)))
- Nothing
-
-testmfn = Decl (Var "negAddOne")
- (tFun tInt tInt)
- $Just (eLam (PVar tInt) (\a -> eNeg $ eAdd a $ cInt 1))
-
-booli = Decl (Var "booli")
- (tFun tBool tInt)
- $ Just (eLam (PVar tBool) (\b -> eITE b (cInt 1) (cInt 0)))
-
-testcfn = Decl (Var "cfn")
- (tFun tInt $ tColl CTSet tInt)
- $Just (eLam (PVar tInt) (\x -> eSing x))
-
-testpairfn = Decl (Var "ibfst")
- (tFun (tTuple2 (tInt,tBool)) tInt)
- $Just (eLam (PTup (PVar tInt, PVar tBool)) (\(a,b) -> a))
-
-lamslice = eLam (PVar autoty) $ \a ->
- eSlice (STup (SVar a, SVar (cInt 4)))
- (eSing (eTuple2 (cInt 3, cInt 4)) `asColl` CTSet)
-
- -- XXX Man we need better tuple handling.
-project = eLam (PTup (PVar autoty, PVar autoty))
- $ \(x,c) -> eMap (eLam (PTup (PVar autoty
- ,PVar autoty
- ,PVar autoty))
- $ \(_,y,z) -> eTuple2 (y,z))
- (eSlice (STup (SVar x, SUnk, SUnk)) c)
-
-proj' = eLam (PTup (PVar tInt, PVar tInt, PVar tInt))
- $ \(a,b,c) -> b
-
- -- Sum-Singleton case from M3ToK3 test
- -- It is safe to leave off the top-level signature
-sumsing (ix :: r Int) (iy :: r Int) c1 c2 = eAdd (v c1) (v c2)
- where
- -- It is safe to eliminate this type signature
- si = STup (SVar ix,SVar iy,SUnk)
-
- -- XXX unfortunately, we have to be explicit about the forall c1 here;
- -- eliminating this type signature results in unified collection types
- -- for c1 and c2 above.
- v :: (K3AST_Pat_C r ('PKVar (CTE c1 (Int, Int, Int))),
- K3AST_Coll_C r c1, K3AutoColl c1)
- => r (CTE c1 (Int, Int, Int)) -> r Int
- v c = eApp (eLam (PVar autoty)
- (\cv -> macro_emptyPeek
- cv (cInt 0)
- (\nec -> eApp (eLam (PTup (PVar autoty
- ,PVar autoty
- ,PVar autoty))
- $ \(_,_,proj) -> proj)
- nec)))
- (eSlice si c)
-
- -- A very very complicated way of writing "3"
-testSumsing = sumsing (cInt 4) (cInt 5)
- (eSing (eTuple3 (cInt 4, cInt 5, cInt 1)) `asColl` CTSet)
- (eSing (eTuple3 (cInt 4, cInt 5, cInt 2)) `asColl` CTBag)
-
-testjoin2 c1 c2 =
- macro_simple_join2 pred c1 c2
- where p = PTup (PVar tInt, PVar tInt, PVar tInt)
- pred = (eLam p (\(k1a,k2a,_) ->
- eLam p (\(k1b,k2b,_) ->
- (eEq k1a k1b) `eAdd` (eEq k2a k2b))))
-
-
-testlocal = macro_localVar autoty
- (eEmpty `asColl` CTBag)
- (\x -> eInsert x $ eTuple2 (cInt 3, cInt 4))
-
-
-------------------------------------------------------------------------}}}
--- Example cases: misc badness
-------------------------------------------------------------------------{{{
-
--- We can write this with undefined, but it will induce a
--- constraint K3BaseTy (Bool -> b). Note that if b ever
--- became monomorphic, the search would fail; further,
--- trying to fill in the undefined will make it monomorphic. :)
---
--- That is, we are prevented from ever actually writing this thing out
--- to the K3 compiler.
-testHOF = eLam (PVar undefined) $ \x -> eApp x (cBool True)
-
-------------------------------------------------------------------------}}}
+++ /dev/null
----------------------------------------------------------------------------
--- | 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.
-
--- Header material {{{
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# OPTIONS_GHC -Wall -Werror #-}
-
-module Dyna.Backend.K3.Render (
- -- * K3 implementations
- AsK3Ty(..), AsK3E(..),
-
- -- * Utility functions
- sh, sht, shd, shk3
-) where
-
-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.Backend.K3.AST
-import Dyna.Backend.K3.CollectDecls
-import Dyna.XXX.HList
-import Dyna.XXX.MonadUtils
-import Dyna.XXX.THTuple
-import Dyna.XXX.PPrint
-
--- import qualified Language.Haskell.TH as TH
-
-------------------------------------------------------------------------}}}
--- Utilities {{{
-
--- | 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
--}
-
-{-
--- | 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
--}
-
-------------------------------------------------------------------------}}}
--- Collection handling {{{
-
-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$ "{| |}"
-
-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 {{{
-
-rec_k3pfn :: PDat UnivTyRepr w
- -> ReaderT (Doc e,Bool) (State Int) (Doc e, PatReprFn (AsK3E e) w)
-rec_k3pfn = local (\(a,_) -> (a,False)) . k3pfn
-
--- | 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 (Doc e,Bool) (State Int) (Doc e, PatReprFn (AsK3E e) w)
-k3pfn (PVar tr) = do
- n <- lift incState
- (pfx,_) <- ask
- let sn = pfx <> pretty n
- return (sn <> colon <> unAsK3Ty (unUTR tr)
- ,AsK3E$ const$ sn)
-k3pfn PUnk = return ("_", ())
-k3pfn (PJust w) = rec_k3pfn w >>= \(p,r) -> return ("just" <+> parens p, r)
-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 (\(a,_) -> (a,True)) $ k3pfn (PHL ws)
- p <- asks (\(_,f) -> (if f then (comma <>) else id) (pw <> ps))
- let r = rw :+ rs
- return (p,r)
-k3pfn (PT2 (a,b)) = do
- (pa,ra) <- k3pfn a
- (pb,rb) <- k3pfn b
- let p = sepBy comma [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 = sepBy comma [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 = sepBy comma [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 = sepBy comma [pa,pb,pc,pd,pe]
- let r = (ra,rb,rc,rd,re)
- return (p,r)
-
-run_k3pfn :: Doc e
- -> PDat UnivTyRepr w
- -> Int
- -> ((Doc e, PatReprFn (AsK3E e) w), Int)
-run_k3pfn pfx w n = runState (runReaderT (k3pfn w) (pfx,False)) n
-
-
-------------------------------------------------------------------------}}}
--- Slice handling {{{
-
-rec_k3sfn :: PDat (AsK3E e) w -> Reader Bool (AsK3E e (PatTy (AsK3E e) w))
-rec_k3sfn = local (const False) . k3sfn
-
--- | 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 $ AsK3E$ \n -> "just" <> parens (unAsK3E p n)
-k3sfn (PRef x) = do
- p <- rec_k3sfn x
- return $ phantom_ask3e p
-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]
-
-
-------------------------------------------------------------------------}}}
--- 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)
-
-{- XXX k3xref
-newtype K3RXref a = K3RXR { unK3RXR :: String }
-
-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
- (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
-
-instance (RXref w) => RXref (PKRef w) where
-
-instance (UnMapPatDa (HList (MapPatDa ws)) ~ ws,
- MapPatConst ws K3RXref,
- MapConstraint RXref ws)
- => RXref (PKHL '[]) where
- rxref_mk HN = return HN
-
-instance (RXref w, RXref (PKHL ws),
- MapPatConst ws K3RXref)
- => RXref (PKHL (w ': ws)) where
- rxref_mk (w :+ ws) = do
- pfx <- ask
- ix <- incState
- (rw,_) <- local (const $ pfx <> show ix) $ bracketState 0 $ rxref_mk w
- rs <- rxref_mk ws
- return (rw :+ rs)
--}
--}
-
-annTText :: AnnT a -> Doc e
-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"
-annEText ASingleton = "singleton"
-annEText (AEMisc s) = text s
-
-------------------------------------------------------------------------}}}
--- Type handling {{{
-
--- | Produce a textual representation of a K3 type
---
--- 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 }
-
-instance K3Ty (AsK3Ty e) where
- tAnn (AsK3Ty e) anns = AsK3Ty$ align $
- e </> "@" <+> (encloseSep lbrace rbrace comma $ map annTText anns)
-
- tAddress = AsK3Ty$ "address"
- tBool = AsK3Ty$ "bool"
- tByte = AsK3Ty$ "byte"
- tFloat = AsK3Ty$ "float"
- tInt = AsK3Ty$ "int"
- tString = AsK3Ty$ "string"
- tUnit = AsK3Ty$ "unit"
-
- -- XXX is that right?
- tTarget _ = AsK3Ty$ "target"
-
- -- tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
-
- tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> 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)
-
- -- XXX k3ref
- -- 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
-
-instance Show (AsK3Ty e a) where
- show (AsK3Ty f) = show f
-
-sht :: AsK3Ty e a -> Doc e
-sht = unAsK3Ty
-
-------------------------------------------------------------------------}}}
--- Expression handling {{{
-
-data Prec = PrecLowest
- | PrecITE
- | PrecBOComp
- | PrecBOAdd
- | PrecBOMul
- | PrecNeg
- | PrecApp
- deriving (Enum,Eq,Ord,Show)
-
--- | Produce a textual representation of a K3 expression
-newtype AsK3E e (a :: *) = AsK3E { unAsK3E :: (Int,Prec) -> Doc e }
-
-instance K3 (AsK3E e) where
- declVar (Decl (Var v) _) = AsK3E$ const$ text v
- unsafeVar (Var v) _ = AsK3E$ const$ text v
-
- cAnn (AsK3E e) anns = AsK3E$ \n -> align $
- parens (e n) <> " @ "
- <> (encloseSep lbrace rbrace comma $ map annEText anns)
-
- cComment str (AsK3E a) = AsK3E$ \n -> "\n// " <> text str <> "\n" <> a n
-
- cAddress (Addr (h,p)) = AsK3E$ const$ (text h <> ":" <> pretty p)
-
- 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$ "()"
-
-
- eJust (AsK3E a) = builtin "just" [ a ]
- -- XXX k3ref
- -- eRef (AsK3E a) = builtin "ref" [ a ]
-
- -- XXX TUPLES Note the similarity of these!
- 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 = AsK3E $ \(n,_) -> tupled $ hrlproj (flip unAsK3E (n,PrecLowest)) t
-
- eEmpty = k3cfn_empty
- eSing = k3cfn_sing
- 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 (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 = AsK3E$ \(n,_) -> let ((pat, arg),n') = run_k3pfn "x" w n
- in "\\" <> parens pat <+> "->" `above`
- indent 2 (unAsK3E (f arg) (n',PrecLowest))
-
- eApp (AsK3E f) (AsK3E x) = AsK3E$ \(n,_) ->
- parens (parens (f (n,PrecApp)) </> parens (x (n,PrecApp)))
-
- eBlock ss (AsK3E r) = AsK3E$ \(n,_) ->
- "do" <> (semiBraces (map ($ (n,PrecLowest)) ((map unAsK3E ss) ++ [r])))
-
- eIter (AsK3E f) (AsK3E c) = builtin "iterate" [ f, c ]
-
- 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 (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 (AsK3E c) = AsK3E$ \n -> c n <> brackets (unAsK3E (runReader (k3sfn w) False) 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 ":="
-
- eSend (AsK3E a) (AsK3E f) (AsK3E x) = builtin "send" [ a, f, x ]
-
-inist :: (Int,Prec)
-inist = (0,PrecLowest)
-
-encBag :: Doc e -> Doc e
-encBag = enclose "{|" "|}"
-
-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 -> 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)
-
-instance Show (AsK3E e a) where
- show (AsK3E f) = show $ f inist
-
-sh :: AsK3E e a -> Doc e
-sh f = unAsK3E f inist
-
-------------------------------------------------------------------------}}}
--- Declaration handling: data synthesis from types (XXX JUNK?) {{{
-
-{-
-
--- | Produce a textual representation of a K3 type
---
--- Unlike AsK3E below, we don't need to thread a variable counter
--- around since K3 doesn't have tyvars
-newtype AsK3TyDat e (a :: *) = AsK3TyDat { unAsK3TyDat :: State Int (AsK3E e a) }
-
-mkvar :: AsK3TyDat e a
-mkvar = AsK3TyDat$ incState >>= \n -> return $ AsK3E $ \_ -> text ("a" ++ (show n))
-
-instance K3Ty (AsK3TyDat e) where
- tAnn = const
-
- tAddress = mkvar
- tBool = mkvar
- tByte = mkvar
- tFloat = mkvar
- tInt = mkvar
- tString = mkvar
- tUnit = mkvar
- tTarget _ = mkvar
- tMaybe _ = mkvar
- tColl _ _ = mkvar
- tFun _ _ = mkvar
-
- -- XXX k3ref
- -- tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
-
- -- XXX TUPLES
- tTuple2 _ = mkvar
- tTuple3 _ = mkvar
- tTuple4 _ = mkvar
- tTuple5 _ = mkvar
-
- tHL _ = mkvar
--}
-
-------------------------------------------------------------------------}}}
--- Declaration handling: printout {{{
-
-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) -> colon <+> sht (unUTR ty)
- (DTrig p f) -> let ((pvs,args),_) = run_k3pfn "a" p 0
- in parens pvs
- <+> text "{}" -- XXX
- <+> equals
- <+> sh (f args)
-
- (DRef ty i) -> colon <+> sht (unUTR ty)
- <> renderBody i
- (DFunc ta tb p f) -> colon <+> sht (unUTR $ tFun ta tb)
- <> renderBody (eLam p f)
-
- where
- renderBody b = space <> equals `aboveBreak` (indent 2 $ sh b)
-
-shd :: Decl s t -> Doc e
-shd (Decl (Var name) {- tipe -} body) =
- declKeyword body
- <+> text name
- <+> align (shdk body)
- <> 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)
-
-{- XXX JUNK
- -
--- | Produce a textual representation of a K3 program, including all
--- referenced declarations.
-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 (XXX) {{{
-
-
-{-
-$(mkLRecInstances (''K3PFn,[]) 'PKTup
- ('k3pfn,'rec_k3pfn,Nothing,\ls -> TH.tupE [
- TH.appE (TH.varE 'tupled)
- $ TH.listE
- $ map (TH.appE (TH.varE 'fst)) ls
- , TH.tupE $ map (TH.appE (TH.varE 'snd)) ls
- ]
- ))
-$(do
- e <- liftM TH.varT $ TH.newName "e"
- n <- TH.newName "n"
- mkLRecInstances (''K3SFn,[e]) 'PKTup
- ('k3sfn,'rec_k3sfn,Nothing,\ls ->
- TH.appE (TH.conE 'AsK3)
- $ TH.lamE [TH.varP n]
- $ TH.appE (TH.varE 'tupled)
- $ TH.listE
- $ map (\l -> TH.appE (TH.appE (TH.varE 'unAsK3) l) (TH.varE n))
- $ ls
- ))
--}
-
-------------------------------------------------------------------------}}}
+++ /dev/null
----------------------------------------------------------------------------
--- Header material
-------------------------------------------------------------------------{{{
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-module Dyna.Backend.K3.Selftest where
-
-import Dyna.Backend.K3.AST
-import Dyna.Backend.K3.Automation
-import Dyna.Backend.K3.Render
-import Dyna.XXX.HList
-import qualified Test.Framework as TF
-import Test.Framework.Providers.HUnit
-import Test.Framework.TH
-import Test.HUnit
-import Text.PrettyPrint.Free
-
-------------------------------------------------------------------------}}}
--- Match some K3 to strings {{{
-
- -- | Produce a version of the Doc with minimal formatting
-displaySimple :: SimpleDoc e -> ShowS
-displaySimple (SEmpty ) = id
-displaySimple (SChar c d) = showChar c . displaySimple d
-displaySimple (SText _ s d) = showString s . displaySimple d
-displaySimple (SLine _ d) = showChar ' ' . displaySimple d
-displaySimple (SEffect _ d) = displaySimple d
-
-renderExp :: AsK3E e a -> String
-renderExp = despace . flip displaySimple [] . renderCompact . sh
- where
- despace [] = []
- despace [x] = [x]
- despace (' ':xs@(' ':_)) = despace xs
- despace (' ':xs) = ' ' : despace xs
- despace (x :xs) = x : despace xs
-
-------------------------------------------------------------------------}}}
--- Basic handling {{{
-
-case_mfn :: Assertion
-case_mfn = e @=? renderExp k3
- where
- e = "\\x0:int -> -(x0 + 1)"
- -- Note that we cannot automate the tInt here, since K3's math
- -- operators are overloaded, so there's no way to conclude
- -- the type of a from the occurrance of "a + Int".
- k3 = eLam (PVar tInt) (\a -> eNeg $ eAdd a $ cInt 1)
-
--- case_pairfn :: Assertion
--- case_pairfn = e @=? renderExp k3
--- where
--- 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 @=? renderExp k3
- where
- e = "if (test == nothing) then 0 "
- <> "else ((\\just (x0:int) -> x0) (test))"
- k3 = caseMaybe tInt (unsafeVar (Var "test") autoty) (cInt 0) (id)
-
-------------------------------------------------------------------------}}}
--- Harness toplevel {{{
-
-selftest :: TF.Test
-selftest = $(testGroupGenerator)
-
-main :: IO ()
-main = $(defaultMainGenerator)
-
-------------------------------------------------------------------------}}}
+++ /dev/null
-
-module Dyna.REPL where
-
-import Control.Applicative ((<*))
-import Control.Monad.Trans (liftIO)
-import System.Console.Haskeline
-import System.IO
-import System.Process
-import qualified Text.PrettyPrint.ANSI.Leijen as PPA
-import Text.Trifecta as T
-import Text.Trifecta.Result as TR
-
-import qualified Dyna.ParserHS.Parser as DP
--- import qualified Dyna.NormalizeParse as DNP
-import Dyna.XXX.Trifecta
-
-main :: IO ()
-main = do
- runInputT defaultSettings loop
- where
- loop = do
- maybeLine <- getInputLine "Dyna> "
- case maybeLine of
- Nothing -> return () -- ctrl-D
- Just l -> triInteract (DP.dline <* eof)
- promptCont
- success
- failure
- l
-
- -- Interaction interprets a ^D in nested context
- -- as an excuse to print out parsing errors
- -- (i.e. it why it rejected the line thus far);
- -- TODO is that what we want?
- promptCont = getInputLine " "
-
- success a = do
- outputStrLn $ "\nParsed: " ++ show a
- loop
-
- failure td = do
- liftIO $ PPA.hPutDoc stdout td
- loop
projects / dyna2 / commitdiff