From: Nathaniel Wesley Filardo <nwf@pf.priv.oc.ietfng.org>
Date: Sat, 22 Sep 2012 03:11:45 +0000 (-0400)
Subject: Some initial progress towards a K3 backend: AST, renderer, and examples
X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=f2d58e05a75eb7d8100bba2d11b67125415bc0a5;p=dyna2

Some initial progress towards a K3 backend: AST, renderer, and examples
---

diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs
new file mode 100644
index 0000000..16a9c91
--- /dev/null
+++ b/src/Dyna/BackendK3/AST.hs
@@ -0,0 +1,347 @@
+---------------------------------------------------------------------------
+-- 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 TypeFamilies #-}
+
+  -- | 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.
+module Dyna.BackendK3.AST where
+
+import           Data.Word
+import           GHC.Prim (Constraint)
+
+------------------------------------------------------------------------}}}
+-- Preliminaries
+------------------------------------------------------------------------{{{
+
+newtype VarIx  = Var String
+newtype AddrIx = Addr (String,Int)
+
+data Ann = Ann [String]
+
+------------------------------------------------------------------------}}}
+-- Collections
+------------------------------------------------------------------------{{{
+
+data CKind = CSet | CBag | CList
+
+data CTE (c :: CKind) e
+
+data CollTy c where
+  CTSet  :: CollTy CSet
+  CTBag  :: CollTy CBag
+  CTList :: CollTy CList
+
+------------------------------------------------------------------------}}}
+-- Effectables (XXX TODO)
+------------------------------------------------------------------------{{{
+
+{-
+data MKind = MKImmut | MKMut
+
+data MTy m where
+  MTImmut :: MTy MKImmut
+  MTMut   :: MTy MKMut
+
+data VKind = VKIsol | VKCont
+
+data VTy v where
+  VTIsol :: VTy VKIsol
+  VTCont :: VTy VKCont
+-}
+
+------------------------------------------------------------------------}}}
+-- 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    :: Ann -> r a -> r a
+
+  tBool   :: r Bool
+  tByte   :: r Word8
+  tFloat  :: r Float
+  tInt    :: r Int
+  tString :: r String
+  tUnit   :: r ()
+  tUnk    :: r a
+
+{- TAddress | TTarget BaseTy -}
+
+  tPair   :: r a -> r b -> r (a,b)
+
+  tMaybe  :: r a -> r (Maybe 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
+
+------------------------------------------------------------------------}}}
+-- Pattern System
+------------------------------------------------------------------------{{{
+
+  -- | Kinds of patterns permitted in K3
+data PKind where
+  PKVar  :: k -> PKind
+  PKJust :: PKind -> PKind
+  PKPair :: PKind -> PKind -> PKind
+
+  -- | Provides witnesses that certain types may be used
+  --   as arguments to K3 lambdas.  Useful when building
+  --   up type signatures and pattern matches in lambdas.
+  --
+  --   Note that this is a closed class using the promoted
+  --   data PKind.
+class Pat (w :: PKind) where
+    -- | Any data this witness needs to carry around
+  data PatDa w :: *
+    -- | The type this witness witnesses?
+  type PatTy 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)
+
+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 }
+  type PatTy (PKVar a) = a
+  type PatReprFn (PKVar a) r = r a
+
+  patAsRepr = unPVar
+
+instance (Pat w) => Pat (PKJust w) where
+  -- | Just patterns (fail on Nothing)
+  --
+  -- Note the distinction between PatTy 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 PatReprFn (PKJust w) r = PatReprFn w r
+
+  patAsRepr (PJust w') = ETR $ tMaybe $ unETR $ patAsRepr w'
+
+instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where
+  -- | Pair patterns
+  --
+  -- Product patterns, on the other hand, have PatTy and PatReprFn both
+  -- producing tuples.
+  data PatDa (PKPair wa wb)       = PPair (PatDa wa) (PatDa wb)
+  type PatTy (PKPair wa wb)       = (PatTy wa, PatTy 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)
+
+------------------------------------------------------------------------}}}
+-- Slice System
+------------------------------------------------------------------------{{{
+
+  -- | Kinds of slices permitted in K3
+data SKind where
+  SKVar  :: k -> SKind
+  SKJust :: SKind -> SKind
+  SKPair :: SKind -> SKind -> SKind
+
+  -- | Witness of slice well-formedness
+class Slice (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
+
+instance (Slice s) => Slice (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
+  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)
+
+------------------------------------------------------------------------}}}
+-- 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
+
+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 Float Float where
+  type BNTF Float Float = Float
+  biadd = (+)
+  bimul = (*)
+
+  -- XXX More
+
+------------------------------------------------------------------------}}}
+-- Values and Expressions
+------------------------------------------------------------------------{{{
+
+class K3 (r :: * -> *) where
+    -- | A representation-specific constraint for collections, on functions
+    -- which need to dispatch on a type-tag in the output.
+  type K3AST_Coll_C r (c :: CKind) :: Constraint
+
+    -- | A representation-specific constraint on handling patterns, on any
+    -- function which uses patterns.
+  type K3AST_Pat_C r (w :: PKind) :: Constraint
+
+    -- | A representation-specific constraint for slices, on eSlice.
+  type K3AST_Slice_C r (w :: SKind) :: Constraint
+
+    -- | 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      :: Ann -> r a -> r a
+
+    -- XXX An escape hatch
+  cUnk      :: r a 
+
+    -- XXX 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 ()
+
+    -- XXX polymorphic type because the expression might be
+    -- well-formed; we'll have to resolve it later.
+  eVar      :: VarIx -> 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)
+  eRange    :: r Int -> r Int -> r Int -> r (CTE 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       :: r a -> r a -> r Bool
+  eLt       :: r a -> r a -> r Bool
+  eLeq      :: r a -> r a -> r Bool
+  eNeq      :: r a -> r a -> r Bool
+
+    -- Unlike traditional lambdas, we require a witness
+    -- that the argument is admissible in K3.
+  eLam      :: (K3AST_Pat_C r w, Pat w)
+            => PatDa w -> (PatReprFn w r -> r b) -> r (PatTy w -> b)
+  eApp      :: r (a -> b) -> r a -> r b
+
+  eBlock    :: [r ()] -> r a -> r a
+
+  eIter     :: r (t -> ()) -> r (CTE c t) -> r ()
+
+  eITE      :: r Bool -> r a -> r a -> r a
+
+  eMap      :: r (t -> t') -> r (CTE c t) -> r (CTE c t')
+  eFiltMap  :: r (t -> Bool) -> r (t -> t') -> r (CTE c t) -> r (CTE c t')
+
+  eFlatten  :: r (CTE c (CTE c' t)) -> r (CTE c' t)
+
+    -- | 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)
+
+  ePeek     :: r (CTE c e) -> r e
+
+    -- | Slice out from a collection; the slice's type and
+    -- the type of elements of the collection must match.
+    --
+    -- Rather like lambdas, except that the witness is also
+    -- a mandatory part of the definition of "slice" :)
+  eSlice    :: (K3AST_Slice_C r w, Slice 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
+  -- XXX eSend
+
+------------------------------------------------------------------------}}}
+-- Miscellanious
+------------------------------------------------------------------------{{{
+
+  -- XXX does not enumerate local variables
+data Decl tr r t = Decl VarIx (tr t) (Maybe (r t))
+
+  -- | A convenience function for setting the type of a collection.
+  --
+  -- Use as (eEmpty `asColl` CTSet)
+asColl :: r (CTE c t) -> CollTy c -> r (CTE c t)
+asColl = const
+
+------------------------------------------------------------------------}}}
+-- fin
+---------------------------------------------------------------------------
diff --git a/src/Dyna/BackendK3/Examples.hs b/src/Dyna/BackendK3/Examples.hs
new file mode 100644
index 0000000..209cc0f
--- /dev/null
+++ b/src/Dyna/BackendK3/Examples.hs
@@ -0,0 +1,68 @@
+---------------------------------------------------------------------------
+-- 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 TypeFamilies #-}
+
+
+module Dyna.BackendK3.Examples where
+
+import           Dyna.BackendK3.AST
+import           Dyna.BackendK3.Render
+
+------------------------------------------------------------------------}}}
+-- Example cases
+------------------------------------------------------------------------{{{
+
+macro_caseMaybe :: (K3 r, K3AST_Pat_C r (PKJust (PKVar a)))
+                => ExTyRepr 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)
+
+test_macroCM = Decl (Var "nocase")
+                    (tInt)
+                    $Just $ macro_caseMaybe tInt (eVar (Var "test")) (cInt 0) (id)
+
+testdecf = Decl (Var "f")
+                (tColl CTBag (tPair tInt tInt))
+                Nothing
+
+testmfn = Decl (Var "negAddOne")
+               (tFun tInt tInt)
+               $Just (eLam (PVar $ ETR 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)))
+
+testcfn = Decl (Var "cfn")
+               (tFun tInt $ tColl CTSet tInt)
+               $Just (eLam (PVar tInt) (\x -> eSing x))
+
+
+testpairfn = Decl (Var "ibfst")
+                  (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)
+
+------------------------------------------------------------------------}}}
+-- fin
+---------------------------------------------------------------------------
diff --git a/src/Dyna/BackendK3/Render.hs b/src/Dyna/BackendK3/Render.hs
new file mode 100644
index 0000000..e6ea815
--- /dev/null
+++ b/src/Dyna/BackendK3/Render.hs
@@ -0,0 +1,226 @@
+---------------------------------------------------------------------------
+-- Header material
+------------------------------------------------------------------------{{{
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TypeFamilies #-}
+
+    -- | Provides the "AsK3" type and instances for the K3 AST.
+module Dyna.BackendK3.Render where
+
+import           Text.PrettyPrint.Free
+
+import           Dyna.BackendK3.AST
+
+
+------------------------------------------------------------------------}}}
+-- Type handling
+------------------------------------------------------------------------{{{
+
+    -- | Unlike AsK3 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 (Ann anns) (AsK3Ty e) = AsK3Ty$ 
+       parens e <> " @ "
+    <> (encloseSep lbrace rbrace comma $ map text anns)
+
+  tBool   = AsK3Ty$ "bool"
+  tByte   = AsK3Ty$ "byte"
+  tFloat  = AsK3Ty$ "float"
+  tInt    = AsK3Ty$ "int"
+  tString = AsK3Ty$ "string"
+  tUnit   = AsK3Ty$ "unit"
+  tUnk    = AsK3Ty$ "_"
+
+  tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
+
+  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
+
+------------------------------------------------------------------------}}}
+-- Collection handling
+------------------------------------------------------------------------{{{
+
+class K3CFn (c :: CKind) where
+  k3cfn_empty :: AsK3 e (CTE c a)
+  k3cfn_sing  :: AsK3 e vma -> AsK3 e (CTE c vma)
+
+instance K3CFn CSet where
+  k3cfn_empty = AsK3$const$ "{ }"
+  k3cfn_sing (AsK3 e) = AsK3$ braces . e
+
+instance K3CFn CList where
+  k3cfn_empty = AsK3$const$ "[ ]"
+  k3cfn_sing (AsK3 e) = AsK3$ brackets . e
+
+instance K3CFn CBag where
+  k3cfn_empty = AsK3$const$ "{| |}"
+  k3cfn_sing (AsK3 e) = AsK3$ encBag . e
+
+------------------------------------------------------------------------}}}
+-- Pattern handling
+------------------------------------------------------------------------{{{
+
+class (Pat w) => K3PFn w where
+  k3pfn :: Int -> PatDa w -> (Int, Doc e, PatReprFn w (AsK3 e))
+
+instance K3PFn (PKVar (a :: *)) where
+  k3pfn n (PVar tr) = let sn = text $ "x" ++ show n in
+                      (n+1
+                      ,sn <> colon <> unAsK3Ty (unETR tr)
+                      ,AsK3$const$ sn)
+
+instance (K3PFn w) => K3PFn (PKJust w) where
+  k3pfn n (PJust w) = let (n', b, r) = k3pfn n w
+                      in (n', "Just " <> parens b, r)
+
+instance (K3PFn wa, K3PFn wb) => K3PFn (PKPair wa wb) where
+  k3pfn n (PPair wa wb) =
+    let (n', ba, ra) = k3pfn n wa
+        (n'', bb, rb) = k3pfn n' wb
+    in (n'', tupled [ ba, bb ], (ra,rb))
+
+------------------------------------------------------------------------}}}
+-- Slice handling
+------------------------------------------------------------------------{{{
+
+class (Slice w) => K3SFn w where
+  k3sfn :: SliceDa w -> Doc e
+
+instance K3SFn (SKVar (a :: *)) where
+  k3sfn (SVar (Var v) _) = text v
+
+instance (K3SFn s) => K3SFn (SKJust s) where
+  k3sfn (SJust s) = "Just" <> parens (k3sfn s)
+
+instance (K3SFn sa, K3SFn sb) => K3SFn (SKPair sa sb) where
+  k3sfn (SPair sa sb) = tupled [ k3sfn sa, k3sfn sb ]
+
+------------------------------------------------------------------------}}}
+-- Expression handling
+------------------------------------------------------------------------{{{
+
+newtype AsK3 e (a :: *) = AsK3 { unAsK3 :: Int -> Doc e }
+
+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
+
+  cAnn (Ann anns) (AsK3 e) = AsK3$ \n ->
+       parens (e n) <> " @ "
+    <> (encloseSep lbrace rbrace comma $ map text anns)
+
+  cComment str (AsK3 a) = AsK3$ \n -> "\n// " <> text str <> "\n" <> a n
+
+  cBool   n     = AsK3$const$ text$ show n
+  cByte   n     = AsK3$const$ text$ show n
+  cFloat  n     = AsK3$const$ text$ show n
+  cInt    n     = AsK3$const$ text$ show n
+  cString n     = AsK3$const$ text$ show n
+  cNothing      = AsK3$const$ "nothing"
+  cUnit         = AsK3$const$ "unit"
+  cUnk          = AsK3$const$ "_"
+
+  eVar (Var v) = AsK3$const$text v
+
+
+  ePair (AsK3 a) (AsK3 b) = AsK3$ \n -> tupled [a n, b n]
+  eJust (AsK3 a)          = builtin "Just " [ a ]
+
+  eEmpty = k3cfn_empty
+  eSing  = k3cfn_sing
+  eComb (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
+  eNeg (AsK3 b) = AsK3$ \n -> "-" <> parens (b n)
+
+  eEq  = binop "=="
+  eLt  = binop "<"
+  eLeq = binop "<="
+  eNeq = binop "!="
+
+  eLam w f = AsK3$ \n -> let (n', pat, arg) = k3pfn n w
+                         in "\\" <> pat <> " -> " <> (unAsK3 (f arg) n')
+
+  eApp (AsK3 f) (AsK3 x) = AsK3$ \n ->
+    parens (parens (f n) <> space <> 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)
+
+  eMap     (AsK3 f) (AsK3 c)                   = builtin "map"       [ f, c    ]
+  eFiltMap (AsK3 f) (AsK3 m) (AsK3 c)          = builtin "filtermap" [ f, m, c ]
+  eFlatten (AsK3 c)                            = builtin "flatten"   [ c ]
+  eFold    (AsK3 f) (AsK3 z) (AsK3 c)          = builtin "fold"      [ f, z, c ]
+  eGBA     (AsK3 p) (AsK3 f) (AsK3 z) (AsK3 c) = builtin "groupby"   [ p, f, z, c ]
+  eSort    (AsK3 c) (AsK3 f)                   = builtin "sort"      [ c, f ]
+  ePeek    (AsK3 c)                            = builtin "peek"      [ c ]
+
+  eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (k3sfn w)
+
+  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 ]
+
+------------------------------------------------------------------------}}}
+-- 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
+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
+
+instance Show (AsK3Ty e a) where
+  show (AsK3Ty f) = show f
+
+sht :: AsK3Ty e a -> String
+sht = show
+
+shd :: Decl (AsK3Ty e) (AsK3 e) t -> Doc e
+shd (Decl (Var name) tipe body) =
+     "declare "
+  <> text name
+  <> space <> colon <> space
+  <> unAsK3Ty tipe
+  <> case body of
+       Nothing -> empty
+       Just b  -> space <> equals <> space <> unAsK3 b 0
+  <> semi
+
+------------------------------------------------------------------------}}}
+-- fin
+---------------------------------------------------------------------------