From: Nathaniel Wesley Filardo <nwf@cs.jhu.edu>
Date: Thu, 6 Dec 2012 01:16:41 +0000 (-0500)
Subject: WIP: towards a new spin on K3 backend
X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=5f7f80d5267a6d767418cf34bb0b99cd56c0e081;p=dyna2

WIP: towards a new spin on K3 backend
---

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