{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
-- Collections
------------------------------------------------------------------------{{{
-data CKind = CSet | CBag | CList
+data CKind = CBag | CList | CSet
data CTE (c :: CKind) e
data CollTy c where
- CTSet :: CollTy CSet
CTBag :: CollTy CBag
CTList :: CollTy CList
+ CTSet :: CollTy CSet
------------------------------------------------------------------------}}}
-- Effectables (XXX TODO)
VTCont :: VTy VKCont
-}
+data Ref a = Ref
+
------------------------------------------------------------------------}}}
-- Type System
------------------------------------------------------------------------{{{
{- TAddress | TTarget BaseTy -}
tPair :: r a -> r b -> r (a,b)
-
tMaybe :: r a -> r (Maybe a)
-
+ tRef :: r a -> r (Ref a)
tColl :: CollTy c -> r a -> r (CTE c a)
-
tFun :: r a -> r b -> r (a -> b)
-- | Existential typeclass wrapper for K3Ty
-newtype ExTyRepr (a :: *) = ETR { unETR :: forall r . (K3Ty r) => r a }
-instance K3Ty ExTyRepr where
- tAnn s (ETR t) = ETR$tAnn s t
- tBool = ETR tBool
- tByte = ETR tByte
- tFloat = ETR tFloat
- tInt = ETR tInt
- tString = ETR tString
- tUnit = ETR tUnit
- tUnk = ETR tUnk
-
- tPair (ETR a) (ETR b) = ETR$tPair a b
- tMaybe (ETR a) = ETR$tMaybe a
- tColl c (ETR a) = ETR$tColl c a
- tFun (ETR a) (ETR b) = ETR$tFun a b
+newtype UnivTyRepr (a :: *) = UTR { unUTR :: forall r . (K3Ty r) => r a }
+instance K3Ty UnivTyRepr where
+ tAnn s (UTR t) = UTR$tAnn s t
+ tBool = UTR tBool
+ tByte = UTR tByte
+ tFloat = UTR tFloat
+ tInt = UTR tInt
+ tString = UTR tString
+ tUnit = UTR tUnit
+ tUnk = UTR tUnk
+
+ tColl c (UTR a) = UTR$tColl c a
+ tFun (UTR a) (UTR b) = UTR$tFun a b
+ tMaybe (UTR a) = UTR$tMaybe a
+ tPair (UTR a) (UTR b) = UTR$tPair a b
+ tRef (UTR a) = UTR$tRef a
+
+ -- | 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 (CTE c a)
+instance (K3BaseTy a) => K3BaseTy (Maybe a)
+instance (K3BaseTy a) => K3BaseTy (Ref a)
+instance (K3BaseTy a, K3BaseTy b) => K3BaseTy (a,b)
------------------------------------------------------------------------}}}
-- Pattern System
--
-- Note that this is a closed class using the promoted
-- data PKind.
+ --
+ -- PatDa is needed for Render's function, since every
+ -- lambda needs an explicit type signature on its variable.
+ --
+ -- Essentially, these things determine where "r"s end up
+ -- in the lambda given to eLam. Compare and contrast:
+ -- eLam (PVar $ tMaybe tInt) :: (r (Maybe Int) -> _) -> _
+ -- eLam (PJust $ PVar tInt) :: (r Int -> _) -> _
+ --
+ -- eLam (PVar $ tPair tInt tInt) :: (r (Int, Int) -> _) -> _
+ -- eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _
+ --
class Pat (w :: PKind) where
-- | Any data this witness needs to carry around
data PatDa w :: *
- -- | The type this witness witnesses?
+ -- | The type this witness witnesses (i.e. the things matched against)
type PatTy w :: *
+ -- | The type this witness binds (i.e. after matching is done)
+ type PatBTy w :: *
-- | The type of this pattern.
type PatReprFn w (r :: * -> *) :: *
+
-- | Produce a data-level type representation for this witness
- patAsRepr :: PatDa w -> ExTyRepr (PatTy w)
+ -- patAsRepr :: PatDa w -> UnivTyRepr (PatTy w)
-instance Pat (PKVar (a :: *)) where
- -- | Pattern variables may be of any type, but we have to
- -- have a representation builder for it.
- data PatDa (PKVar a) = PVar { unPVar :: ExTyRepr a }
+instance (K3BaseTy a) => Pat (PKVar (a :: *)) where
+ data PatDa (PKVar a) = PVar { unPVar :: UnivTyRepr a }
type PatTy (PKVar a) = a
+ type PatBTy (PKVar a) = a
type PatReprFn (PKVar a) r = r a
- patAsRepr = unPVar
+ --patAsRepr = unPVar
instance (Pat w) => Pat (PKJust w) where
-- | Just patterns (fail on Nothing)
--
- -- Note the distinction between PatTy and PatReprFn here!
+ -- 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.
data PatDa (PKJust w) = PJust (PatDa w)
type PatTy (PKJust w) = Maybe (PatTy w)
+ type PatBTy (PKJust w) = PatBTy w
type PatReprFn (PKJust w) r = PatReprFn w r
- patAsRepr (PJust w') = ETR $ tMaybe $ unETR $ patAsRepr w'
+ --patAsRepr (PJust w') = UTR $ tMaybe $ unUTR $ patAsRepr w'
instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where
-- | Pair patterns
-- producing tuples.
data PatDa (PKPair wa wb) = PPair (PatDa wa) (PatDa wb)
type PatTy (PKPair wa wb) = (PatTy wa, PatTy wb)
+ type PatBTy (PKPair wa wb) = (PatBTy wa, PatBTy wb)
type PatReprFn (PKPair wa wb) r = (PatReprFn wa r, PatReprFn wb r)
- patAsRepr (PPair wa wb) = ETR $ tPair (unETR $ patAsRepr wa)
- (unETR $ patAsRepr wb)
+ --patAsRepr (PPair wa wb) = UTR $ tPair (unUTR $ patAsRepr wa)
+ -- (unUTR $ patAsRepr wb)
------------------------------------------------------------------------}}}
-- Slice System
-- | Kinds of slices permitted in K3
data SKind where
- SKVar :: k -> SKind
+ SKVar :: r -> k -> SKind
+ SKUnk :: k -> SKind
SKJust :: SKind -> SKind
SKPair :: SKind -> SKind -> SKind
-- | Witness of slice well-formedness
-class Slice (w :: SKind) where
+class Slice r (w :: SKind) where
data SliceDa w :: *
type SliceTy w :: *
- sliceAsRepr :: SliceDa w -> ExTyRepr (SliceTy w)
- -- Slice variables are VarIx and representation of K3 type
-instance Slice (SKVar (a :: *)) where
- data SliceDa (SKVar a) = SVar VarIx (ExTyRepr a)
- type SliceTy (SKVar a) = a
- sliceAsRepr (SVar _ ea) = ea
+ -- sliceAsRepr :: SliceDa w -> UnivTyRepr (SliceTy w)
+
+instance (K3BaseTy a, r0 ~ r) => Slice r0 (SKVar (r :: * -> *) (a :: *)) where
+ data SliceDa (SKVar r a) = SVar (r a)
+ type SliceTy (SKVar r a) = a
-instance (Slice s) => Slice (SKJust s) where
+ -- sliceAsRepr (SVar _ ea) = ea
+
+instance (K3BaseTy a) => Slice r (SKUnk (a :: *)) where
+ data SliceDa (SKUnk a) = SUnk
+ type SliceTy (SKUnk a) = a
+
+ -- sliceAsRepr (SUnk ea) = ea
+
+instance (Slice r s) => Slice r (SKJust s) where
data SliceDa (SKJust s) = SJust (SliceDa s)
type SliceTy (SKJust s) = Maybe (SliceTy s)
- sliceAsRepr (SJust a) = ETR $ tMaybe $ unETR $ sliceAsRepr a
-instance (Slice sa, Slice sb) => Slice (SKPair sa sb) where
+ -- sliceAsRepr (SJust a) = UTR $ tMaybe $ unUTR $ sliceAsRepr a
+
+instance (Slice r sa, Slice r sb) => Slice r (SKPair sa sb) where
data SliceDa (SKPair sa sb) = SPair (SliceDa sa) (SliceDa sb)
type SliceTy (SKPair sa sb) = (SliceTy sa, SliceTy sb)
- sliceAsRepr (SPair a b) = ETR $ tPair (unETR $ sliceAsRepr a)
- (unETR $ sliceAsRepr b)
+
+ -- sliceAsRepr (SPair a b) = UTR $ tPair (unUTR $ sliceAsRepr a)
+ -- (unUTR $ sliceAsRepr b)
------------------------------------------------------------------------}}}
-- Numeric Autocasting
------------------------------------------------------------------------{{{
+ -- XXX should we make these be constraints in the K3 class so that
+ -- different representations can make different choices?
+
-- | Unary numerics
class UnNum a where unneg :: a -> a
instance UnNum Bool where unneg = not
cAnn :: Ann -> r a -> r a
-- XXX An escape hatch
- cUnk :: r a
+ --
+ -- The K3 AST has this but uses it for wildcards in slices, which
+ -- we handle with SKUnk/SUnk.
+ -- cUnk :: r a
-- XXX cAddress :: AddrIx -> r AddrIx
cBool :: Bool -> r Bool
cString :: String -> r String
cUnit :: r ()
- -- XXX polymorphic type because the expression might be
- -- well-formed; we'll have to resolve it later.
- eVar :: VarIx -> r a
+ eVar :: VarIx -> UnivTyRepr a -> r a
ePair :: r a -> r b -> r (a,b)
eJust :: r a -> r (Maybe t)
eEmpty :: (K3AST_Coll_C r c) => r (CTE c e)
eSing :: (K3AST_Coll_C r c) => r e -> r (CTE c e)
- eComb :: r (CTE c e) -> r (CTE c e) -> r (CTE c e)
+ eCombine :: r (CTE c e) -> r (CTE c e) -> r (CTE c e)
eRange :: r Int -> r Int -> r Int -> r (CTE c Int)
eAdd :: (BiNum a b) => r a -> r b -> r (BNTF a b)
-- Unlike traditional lambdas, we require a witness
-- that the argument is admissible in K3.
- eLam :: (K3AST_Pat_C r w, Pat w)
+ eLam :: (K3AST_Pat_C r w, Pat w, K3BaseTy (PatTy w))
=> PatDa w -> (PatReprFn w r -> r b) -> r (PatTy w -> b)
eApp :: r (a -> b) -> r a -> r b
-- | Called Aggregate in K3's AST
eFold :: r ((t', t) -> t') -> r t' -> r (CTE c t) -> r t'
- eGBA :: r (t -> t'') -> r ((t',t) -> t') -> r t' -> r (CTE c t) -> r (CTE c (t'',t'))
-
- eSort :: r (CTE c t) -> r ((t,t) -> Bool) -> r (CTE 'CList 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 c t) -- ^ Input collection
+ -> r (CTE c (t'',t'))
+
+ eSort :: r (CTE c t) -- ^ Input collection
+ -> r ((t,t) -> Bool) -- ^ Less-or-equal
+ -> r (CTE 'CList t)
+
+ -- | Peek an element from a collection.
+ --
+ -- Fails on empty collections.
+ --
+ -- For lists, this returns the head; for sets and bags
+ -- it samples arbitrarily.
ePeek :: r (CTE c e) -> r e
-- | Slice out from a collection; the slice's type and
--
-- Rather like lambdas, except that the witness is also
-- a mandatory part of the definition of "slice" :)
- eSlice :: (K3AST_Slice_C r w, Slice w, SliceTy w ~ t)
+ eSlice :: (K3AST_Slice_C r w, Slice r w, SliceTy w ~ t)
=> SliceDa w -> r (CTE c t) -> r (CTE c t)
eInsert :: r (CTE c t) -> r t -> r ()
eDelete :: r (CTE c t) -> r t -> r ()
eUpdate :: r (CTE c t) -> r t -> r t -> r ()
- -- XXX eAssign
- -- XXX eDeref
+ eAssign :: r (Ref t) -> r t -> r ()
+ eDeref :: r (Ref t) -> r t
+
-- XXX eSend
------------------------------------------------------------------------}}}
--- /dev/null
+---------------------------------------------------------------------------
+-- 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 UndecidableInstances #-}
+
+module Dyna.BackendK3.Automation where
+
+import Data.Word
+import Text.PrettyPrint.Free
+
+import Dyna.BackendK3.AST
+import Dyna.BackendK3.Render
+
+ -- | Demote a collection type annotation (of kind CKind) to the
+ -- appropriate chunk of data for case analysis.
+ --
+ -- Note that this only works once the type has become monomorphic;
+ -- otherwise it imposes a constraint on the haskell tyvar.
+ -- (This is a total function)
+class K3AutoColl (c :: CKind) where autocoll :: CollTy c
+instance K3AutoColl CBag where autocoll = CTBag
+instance K3AutoColl CList where autocoll = CTList
+instance K3AutoColl CSet where autocoll = CTSet
+
+ -- | Attempt to automatically derive a universal type representation.
+ --
+ -- Note that this only works once the type has become monomorphic;
+ -- otherwise it imposes a constraint on the haskell tyvar.
+ -- (This is a total function)
+class K3AutoTy a where autoty :: UnivTyRepr a
+instance K3AutoTy Bool where autoty = tBool
+instance K3AutoTy Word8 where autoty = tByte
+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) => K3AutoTy (CTE c a) where
+ autoty = tColl autocoll autoty
+instance (K3AutoTy a) => K3AutoTy (Maybe a) where autoty = tMaybe autoty
+instance (K3AutoTy a) => K3AutoTy (Ref a) where autoty = tRef autoty
+instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a,b) where
+ autoty = tPair autoty autoty
+instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a -> b) where
+ autoty = tFun autoty autoty
+
+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 = ()
+ type K3AST_Pat_C VarsInK3 p = ()
+ type K3AST_Slice_C VarsInK3 s = ()
+
+ 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
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Dyna.BackendK3.Examples where
import Dyna.BackendK3.AST
+import Dyna.BackendK3.Automation
import Dyna.BackendK3.Render
------------------------------------------------------------------------}}}
--- Example cases
+-- Example cases: macros
------------------------------------------------------------------------{{{
-macro_caseMaybe :: (K3 r, K3AST_Pat_C r (PKJust (PKVar a)))
- => ExTyRepr a
+macro_caseMaybe :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKJust (PKVar a)))
+ => UnivTyRepr a
-> r (Maybe a)
-> r b
-> (r a -> r b)
-> r b
macro_caseMaybe w m n b = eITE (eEq m cNothing)
- n
- (eApp (eLam (PJust (PVar w)) b) m)
+ n
+ (eApp (eLam (PJust (PVar w)) b) m)
test_macroCM = Decl (Var "nocase")
(tInt)
- $Just $ macro_caseMaybe tInt (eVar (Var "test")) (cInt 0) (id)
+ $Just $ macro_caseMaybe tInt (eVar (Var "test") autoty) (cInt 0) (id)
+
+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 (CTE c1 a) -> r (CTE c2 b) -> r (a -> b -> Bool) -> r ()
+macro_simple_join2 c1 c2 p =
+ flip eIter c1 $ eLam (PVar autoty) $ \a -> flip eIter c2
+ $ eLam (PVar autoty) $ \b -> eITE (eApp (eApp p a) b) (cUnit) (cUnit)
+
+macro_emptyPeek :: (K3AST_Coll_C r c, K3AST_Pat_C r (PKVar a),
+ K3 r, K3BaseTy a, K3AutoTy a)
+ => r (CTE c a) -> r b -> (r a -> r b) -> r b
+macro_emptyPeek c e l = eITE (eEq c eEmpty)
+ e
+ (eApp (eLam (PVar autoty) l) $ ePeek c)
+
+------------------------------------------------------------------------}}}
+-- Example cases: misc
+------------------------------------------------------------------------{{{
+
testdecf = Decl (Var "f")
(tColl CTBag (tPair tInt tInt))
testmfn = Decl (Var "negAddOne")
(tFun tInt tInt)
- $Just (eLam (PVar $ ETR tInt) (\a -> eNeg $ eAdd a $ cInt 1))
+ $Just (eLam (PVar $ UTR tInt) (\a -> eNeg $ eAdd a $ cInt 1))
booli = Decl (Var "booli")
(tFun tBool tInt)
- $ Just (eLam (PVar (ETR tBool)) (\b -> eITE b (cInt 1) (cInt 0)))
+ $ Just (eLam (PVar (UTR tBool)) (\b -> eITE b (cInt 1) (cInt 0)))
testcfn = Decl (Var "cfn")
(tFun tInt $ tColl CTSet tInt)
(tFun (tPair tInt tBool) tInt)
$Just (eLam (PPair (PVar tInt) (PVar tBool)) (\(a,b) -> a))
-exslice = eSlice (SPair (SVar (Var "x") tInt)
- (SVar (Var "y") tInt))
- (eSing (ePair (cInt 3) (cInt 4)) `asColl` CTSet)
+lamslice = eLam (PVar autoty) $ \a ->
+ eSlice (SPair (SVar a) (SVar (cInt 4)))
+ (eSing (ePair (cInt 3) (cInt 4)) `asColl` CTSet)
+
+ -- XXX Man we need better tuple handling.
+project = eLam (PPair (PVar autoty) (PVar autoty))
+ $ \(x,c) -> eMap (eLam (PPair (PVar autoty)
+ (PPair (PVar autoty)
+ (PVar autoty)))
+ $ \(_,(y,z)) -> ePair y z)
+ (eSlice (SPair (SVar x) (SPair SUnk SUnk)) c)
+
+ -- Sum-Singleton case from M3ToK3 test
+ -- It is safe to leave off the top-level signature
+sumsing :: (K3 r, K3AutoColl c, K3AutoColl c',
+ K3AST_Coll_C r c,
+ K3AST_Coll_C r c',
+ K3AST_Pat_C r (PKVar (Int, (Int, Int))),
+ K3AST_Pat_C r (PKVar (CTE c (Int, (Int, Int)))),
+ K3AST_Pat_C r (PKVar (CTE c' (Int, (Int, Int)))),
+ K3AST_Pat_C r (PKPair (PKVar Int) (PKPair (PKVar Int) (PKVar Int))),
+ K3AST_Slice_C r (SKPair (SKVar r Int) (SKPair (SKVar r Int) (SKUnk Int)))
+ )
+ => r Int -> r Int
+ -> r (CTE c (Int, (Int,Int))) -> r (CTE c' (Int, (Int,Int)))
+ -> r Int
+sumsing (ix :: r Int) iy c1 c2 = eAdd (v c1) (v c2)
+ where
+ -- It is safe to eliminate this type signature
+ si :: SliceDa (SKPair (SKVar r Int) (SKPair (SKVar r Int) (SKUnk Int)))
+ si = SPair (SVar ix) (SPair (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 (PPair (PVar autoty)
+ (PPair (PVar autoty)
+ (PVar autoty)))
+ (\(_,(_,proj)) -> proj))
+ nec)))
+ (eSlice si c)
+
+------------------------------------------------------------------------}}}
+-- 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)
------------------------------------------------------------------------}}}
-- fin
------------------------------------------------------------------------{{{
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
- tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe " <> ta
+ tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> ta
tColl CTSet (AsK3Ty ta) = AsK3Ty$ braces ta
tColl CTBag (AsK3Ty ta) = AsK3Ty$ encBag ta
tColl CTList (AsK3Ty ta) = AsK3Ty$ brackets ta
- tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta <> " -> " <> tb
+ tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta <+> "->" <+> tb
+
+ tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
------------------------------------------------------------------------}}}
-- Collection handling
class (Pat w) => K3PFn w where
k3pfn :: Int -> PatDa w -> (Int, Doc e, PatReprFn w (AsK3 e))
-instance K3PFn (PKVar (a :: *)) where
+instance (K3BaseTy a) => K3PFn (PKVar (a :: *)) where
k3pfn n (PVar tr) = let sn = text $ "x" ++ show n in
(n+1
- ,sn <> colon <> unAsK3Ty (unETR tr)
+ ,sn <> colon <> unAsK3Ty (unUTR tr)
,AsK3$const$ sn)
instance (K3PFn w) => K3PFn (PKJust w) where
-- Slice handling
------------------------------------------------------------------------{{{
-class (Slice w) => K3SFn w where
- k3sfn :: SliceDa w -> Doc e
+class (Slice (AsK3 e) w) => K3SFn e w where
+ k3sfn :: SliceDa w -> AsK3 e (SliceTy w)
+
+instance (K3BaseTy a) => K3SFn e (SKVar (AsK3 e) (a :: *)) where
+ k3sfn (SVar r) = r
-instance K3SFn (SKVar (a :: *)) where
- k3sfn (SVar (Var v) _) = text v
+instance (K3BaseTy a) => K3SFn e (SKUnk (a :: *)) where
+ k3sfn SUnk = AsK3$ const$ text "_"
-instance (K3SFn s) => K3SFn (SKJust s) where
- k3sfn (SJust s) = "Just" <> parens (k3sfn s)
+instance (K3SFn e s) => K3SFn e (SKJust s) where
+ k3sfn (SJust s) = AsK3$ \n -> "Just" <> parens (unAsK3 (k3sfn s) n)
-instance (K3SFn sa, K3SFn sb) => K3SFn (SKPair sa sb) where
- k3sfn (SPair sa sb) = tupled [ k3sfn sa, k3sfn sb ]
+instance (K3SFn e sa, K3SFn e sb) => K3SFn e (SKPair sa sb) where
+ k3sfn (SPair sa sb) = AsK3$ \n -> tupled [ unAsK3 (k3sfn sa) n
+ , unAsK3 (k3sfn sb) n ]
------------------------------------------------------------------------}}}
-- Expression handling
instance K3 (AsK3 e) where
type K3AST_Coll_C (AsK3 e) c = K3CFn c
type K3AST_Pat_C (AsK3 e) p = K3PFn p
- type K3AST_Slice_C (AsK3 e) s = K3SFn s
+ type K3AST_Slice_C (AsK3 e) s = K3SFn e s
cAnn (Ann anns) (AsK3 e) = AsK3$ \n ->
parens (e n) <> " @ "
cString n = AsK3$const$ text$ show n
cNothing = AsK3$const$ "nothing"
cUnit = AsK3$const$ "unit"
- cUnk = AsK3$const$ "_"
- eVar (Var v) = AsK3$const$text v
+ eVar (Var v) _ = AsK3$const$text v
ePair (AsK3 a) (AsK3 b) = AsK3$ \n -> tupled [a n, b n]
eEmpty = k3cfn_empty
eSing = k3cfn_sing
- eComb (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> " ++ " <> parens (b n)
+ eCombine (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> " ++ " <> parens (b n)
eRange (AsK3 f) (AsK3 l) (AsK3 s) = builtin "range" [ f, l, s ]
- eAdd (AsK3 a) (AsK3 b) = AsK3$ \n -> a n <> "+" <> b n
- eMul (AsK3 a) (AsK3 b) = AsK3$ \n -> a n <> "*" <> b n
+ eAdd = binop "+"
+ eMul = binop "*"
eNeg (AsK3 b) = AsK3$ \n -> "-" <> parens (b n)
eEq = binop "=="
eNeq = binop "!="
eLam w f = AsK3$ \n -> let (n', pat, arg) = k3pfn n w
- in "\\" <> pat <> " -> " <> (unAsK3 (f arg) n')
+ in align ("\\" <> pat <+> "->" `above` unAsK3 (f arg) n')
eApp (AsK3 f) (AsK3 x) = AsK3$ \n ->
- parens (parens (f n) <> space <> parens (x n))
+ parens (parens (f n) `aboveBreak` parens (x n))
eBlock ss (AsK3 r) = AsK3$ \n ->
"do" <> (semiBraces (map ($ n) ((map unAsK3 ss) ++ [r])))
eIter (AsK3 f) (AsK3 c) = builtin "iterate" [ f, c ]
- eITE (AsK3 b) (AsK3 t) (AsK3 e) = AsK3$ \n -> "if " <> parens (b n)
- <> " then " <> parens (t n)
- <> " else " <> parens (e n)
+ eITE (AsK3 b) (AsK3 t) (AsK3 e) = AsK3$ \n ->
+ "if" <+> (align $ above (parens (b n))
+ ("then" <+> parens (t n) `aboveBreak`
+ "else" <+> parens (e n)))
eMap (AsK3 f) (AsK3 c) = builtin "map" [ f, c ]
eFiltMap (AsK3 f) (AsK3 m) (AsK3 c) = builtin "filtermap" [ f, m, c ]
eSort (AsK3 c) (AsK3 f) = builtin "sort" [ c, f ]
ePeek (AsK3 c) = builtin "peek" [ c ]
- eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (k3sfn w)
+ eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (k3sfn w) n)
eInsert (AsK3 c) (AsK3 e) = builtin "insert" [ c, e ]
eDelete (AsK3 c) (AsK3 e) = builtin "delete" [ c, e ]
eUpdate (AsK3 c) (AsK3 o) (AsK3 n) = builtin "update" [ c, o, n ]
+ eAssign = binop "<-"
+ eDeref (AsK3 r) = builtin "deref" [ r ]
+ -- XXX that doesn't seem to actually be right!
+
+
------------------------------------------------------------------------}}}
-- Miscellany
------------------------------------------------------------------------{{{
encBag :: Doc e -> Doc e
encBag = enclose "{|" "|}"
- -- Overly polymorphic; use only when correct
-binop :: Doc e -> AsK3 e a -> AsK3 e a -> AsK3 e b
-binop o (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> o <> parens (b n)
+ -- Overly polymorphic; use only when correct!
+binop :: Doc e -> AsK3 e a -> AsK3 e b -> AsK3 e c
+binop o (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (align $ a n)
+ </> o
+ </> parens (align $ b n)
- -- Overly polymorphic; use only when correct
+ -- Overly polymorphic; use only when correct!
builtin :: Doc e -> [ Int -> Doc e ] -> AsK3 e b
builtin fn as = AsK3$ \n -> fn <> tupled (map ($ n) as)
instance Show (AsK3 e a) where
show (AsK3 f) = show $ f 0
-sh :: AsK3 e a -> String
-sh = show
+sh :: AsK3 e a -> Doc e
+sh (AsK3 f) = f 0
instance Show (AsK3Ty e a) where
show (AsK3Ty f) = show f