From: Nathaniel Wesley Filardo Date: Mon, 3 Jun 2013 03:52:30 +0000 (-0400) Subject: Remove stale files X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=8cabac1f2df9bdfb5d61b990f6fede80db1cc36f;p=dyna2 Remove stale files --- diff --git a/src/Dyna/Backend/K3/AST.hs b/src/Dyna/Backend/K3/AST.hs deleted file mode 100644 index c218233..0000000 --- a/src/Dyna/Backend/K3/AST.hs +++ /dev/null @@ -1,942 +0,0 @@ ---------------------------------------------------------------------------- --- | 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) - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/K3/Automation.hs b/src/Dyna/Backend/K3/Automation.hs deleted file mode 100644 index b40cc1c..0000000 --- a/src/Dyna/Backend/K3/Automation.hs +++ /dev/null @@ -1,248 +0,0 @@ ---------------------------------------------------------------------------- --- | 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 --} - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/K3/CollectDecls.hs b/src/Dyna/Backend/K3/CollectDecls.hs deleted file mode 100644 index 72ed155..0000000 --- a/src/Dyna/Backend/K3/CollectDecls.hs +++ /dev/null @@ -1,152 +0,0 @@ ---------------------------------------------------------------------------- --- | 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) diff --git a/src/Dyna/Backend/K3/Examples.hs b/src/Dyna/Backend/K3/Examples.hs deleted file mode 100644 index 4cab237..0000000 --- a/src/Dyna/Backend/K3/Examples.hs +++ /dev/null @@ -1,134 +0,0 @@ ---------------------------------------------------------------------------- --- 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) - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/K3/Render.hs b/src/Dyna/Backend/K3/Render.hs deleted file mode 100644 index 96ec79b..0000000 --- a/src/Dyna/Backend/K3/Render.hs +++ /dev/null @@ -1,638 +0,0 @@ ---------------------------------------------------------------------------- --- | 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 - )) --} - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/Backend/K3/Selftest.hs b/src/Dyna/Backend/K3/Selftest.hs deleted file mode 100644 index 4c0636c..0000000 --- a/src/Dyna/Backend/K3/Selftest.hs +++ /dev/null @@ -1,77 +0,0 @@ ---------------------------------------------------------------------------- --- 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) - -------------------------------------------------------------------------}}} diff --git a/src/Dyna/REPL.hs b/src/Dyna/REPL.hs deleted file mode 100644 index ffa3866..0000000 --- a/src/Dyna/REPL.hs +++ /dev/null @@ -1,43 +0,0 @@ - -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