]> hydra-www.ietfng.org Git - dyna2/commitdiff
Snapshotting before I try to replace pairs with tuples
authorNathaniel Wesley Filardo <nwf@cs.jhu.edu>
Wed, 26 Sep 2012 07:22:23 +0000 (03:22 -0400)
committerNathaniel Wesley Filardo <nwf@cs.jhu.edu>
Wed, 26 Sep 2012 07:22:23 +0000 (03:22 -0400)
src/Dyna/BackendK3/AST.hs
src/Dyna/BackendK3/Automation.hs [new file with mode: 0644]
src/Dyna/BackendK3/Examples.hs
src/Dyna/BackendK3/Render.hs

index 16a9c91d0425f77c54b63252af76a468299974a5..92ab55e4fd62e1a7605d5d6c1a93fab9ae06f269 100644 (file)
@@ -5,6 +5,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
@@ -36,14 +37,14 @@ data Ann = Ann [String]
 -- Collections
 ------------------------------------------------------------------------{{{
 
-data CKind = CSet | CBag | CList
+data CKind = CBag | CList | CSet
 
 data CTE (c :: CKind) e
 
 data CollTy c where
-  CTSet  :: CollTy CSet
   CTBag  :: CollTy CBag
   CTList :: CollTy CList
+  CTSet  :: CollTy CSet
 
 ------------------------------------------------------------------------}}}
 -- Effectables (XXX TODO)
@@ -63,6 +64,8 @@ data VTy v where
   VTCont :: VTy VKCont
 -}
 
+data Ref a = Ref
+
 ------------------------------------------------------------------------}}}
 -- Type System
 ------------------------------------------------------------------------{{{
@@ -84,29 +87,42 @@ class K3Ty (r :: * -> *) where
 {- TAddress | TTarget BaseTy -}
 
   tPair   :: r a -> r b -> r (a,b)
-
   tMaybe  :: r a -> r (Maybe a)
-
+  tRef    :: r a -> r (Ref a)
   tColl   :: CollTy c -> r a -> r (CTE c a)
-
   tFun    :: r a -> r b -> r (a -> b)
 
   -- | Existential typeclass wrapper for K3Ty
-newtype ExTyRepr (a :: *) = ETR { unETR :: forall r . (K3Ty r) => r a }
-instance K3Ty ExTyRepr where
-  tAnn   s (ETR t)               = ETR$tAnn s t
-  tBool                          = ETR tBool
-  tByte                          = ETR tByte
-  tFloat                         = ETR tFloat
-  tInt                           = ETR tInt
-  tString                        = ETR tString
-  tUnit                          = ETR tUnit
-  tUnk                           = ETR tUnk
-
-  tPair  (ETR a) (ETR b) = ETR$tPair a b
-  tMaybe (ETR a)         = ETR$tMaybe a
-  tColl  c (ETR a)       = ETR$tColl c a
-  tFun   (ETR a) (ETR b) = ETR$tFun a b
+newtype UnivTyRepr (a :: *) = UTR { unUTR :: forall r . (K3Ty r) => r a }
+instance K3Ty UnivTyRepr where
+  tAnn   s (UTR t)               = UTR$tAnn s t
+  tBool                          = UTR tBool
+  tByte                          = UTR tByte
+  tFloat                         = UTR tFloat
+  tInt                           = UTR tInt
+  tString                        = UTR tString
+  tUnit                          = UTR tUnit
+  tUnk                           = UTR tUnk
+
+  tColl  c (UTR a)       = UTR$tColl c a
+  tFun   (UTR a) (UTR b) = UTR$tFun a b
+  tMaybe (UTR a)         = UTR$tMaybe a
+  tPair  (UTR a) (UTR b) = UTR$tPair a b
+  tRef   (UTR a)         = UTR$tRef a
+
+  -- | A constraint for "base" types in K3.  These are the things that can
+  -- be passed to lambdas.  Essentially everything other than arrows.
+class    K3BaseTy a
+instance K3BaseTy Bool
+instance K3BaseTy Word8
+instance K3BaseTy Float
+instance K3BaseTy Int
+instance K3BaseTy String
+instance K3BaseTy ()
+instance (K3BaseTy a) => K3BaseTy (CTE c a)
+instance (K3BaseTy a) => K3BaseTy (Maybe a)
+instance (K3BaseTy a) => K3BaseTy (Ref a)
+instance (K3BaseTy a, K3BaseTy b) => K3BaseTy (a,b)
 
 ------------------------------------------------------------------------}}}
 -- Pattern System
@@ -124,36 +140,51 @@ data PKind where
   --
   --   Note that this is a closed class using the promoted
   --   data PKind.
+  --
+  --   PatDa is needed for Render's function, since every
+  --   lambda needs an explicit type signature on its variable.
+  --
+  --   Essentially, these things determine where "r"s end up
+  --   in the lambda given to eLam.  Compare and contrast:
+  --     eLam (PVar $ tMaybe tInt)            :: (r (Maybe Int)  -> _) -> _
+  --     eLam (PJust $ PVar tInt)             :: (r Int          -> _) -> _
+  --
+  --     eLam (PVar $ tPair tInt tInt)        :: (r (Int, Int)   -> _) -> _
+  --     eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _
+  --
 class Pat (w :: PKind) where
     -- | Any data this witness needs to carry around
   data PatDa w :: *
-    -- | The type this witness witnesses?
+    -- | The type this witness witnesses (i.e. the things matched against)
   type PatTy w :: *
+    -- | The type this witness binds (i.e. after matching is done)
+  type PatBTy w :: *
     -- | The type of this pattern.
   type PatReprFn w (r :: * -> *) :: *
+
     -- | Produce a data-level type representation for this witness
-  patAsRepr :: PatDa w -> ExTyRepr (PatTy w)
+  -- patAsRepr :: PatDa w -> UnivTyRepr (PatTy w)
 
-instance Pat (PKVar (a :: *)) where
-  -- | Pattern variables may be of any type, but we have to
-  --   have a representation builder for it.
-  data PatDa (PKVar a) = PVar { unPVar :: ExTyRepr a }
+instance (K3BaseTy a) => Pat (PKVar (a :: *)) where
+  data PatDa (PKVar a) = PVar { unPVar :: UnivTyRepr a }
   type PatTy (PKVar a) = a
+  type PatBTy (PKVar a) = a
   type PatReprFn (PKVar a) r = r a
 
-  patAsRepr = unPVar
+  --patAsRepr = unPVar
 
 instance (Pat w) => Pat (PKJust w) where
   -- | Just patterns (fail on Nothing)
   --
-  -- Note the distinction between PatTy and PatReprFn here!
+  -- Note the distinction between PatTy and (PatBTy and PatReprFn) here!
   -- This pattern witnesses a type "Maybe a" but binds a variable of type
   -- "a".  This will in general be true of any variant (i.e. sum) pattern.
   data PatDa (PKJust w)       = PJust (PatDa w)
   type PatTy (PKJust w)       = Maybe (PatTy w)
+  type PatBTy (PKJust w)      = PatBTy w
   type PatReprFn (PKJust w) r = PatReprFn w r
 
-  patAsRepr (PJust w') = ETR $ tMaybe $ unETR $ patAsRepr w'
+  --patAsRepr (PJust w') = UTR $ tMaybe $ unUTR $ patAsRepr w'
 
 instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where
   -- | Pair patterns
@@ -162,10 +193,11 @@ instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where
   -- producing tuples.
   data PatDa (PKPair wa wb)       = PPair (PatDa wa) (PatDa wb)
   type PatTy (PKPair wa wb)       = (PatTy wa, PatTy wb)
+  type PatBTy (PKPair wa wb)      = (PatBTy wa, PatBTy wb)
   type PatReprFn (PKPair wa wb) r = (PatReprFn wa r, PatReprFn wb r)
 
-  patAsRepr (PPair wa wb) = ETR $ tPair (unETR $ patAsRepr wa)
-                                        (unETR $ patAsRepr wb)
+  --patAsRepr (PPair wa wb) = UTR $ tPair (unUTR $ patAsRepr wa)
+  --                                      (unUTR $ patAsRepr wb)
 
 ------------------------------------------------------------------------}}}
 -- Slice System
@@ -173,37 +205,50 @@ instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where
 
   -- | Kinds of slices permitted in K3
 data SKind where
-  SKVar  :: k -> SKind
+  SKVar  :: r -> k -> SKind
+  SKUnk  :: k -> SKind
   SKJust :: SKind -> SKind
   SKPair :: SKind -> SKind -> SKind
 
   -- | Witness of slice well-formedness
-class Slice (w :: SKind) where
+class Slice (w :: SKind) where
   data SliceDa w :: *
   type SliceTy w :: *
-  sliceAsRepr :: SliceDa w -> ExTyRepr (SliceTy w)
 
-  -- Slice variables are VarIx and representation of K3 type
-instance Slice (SKVar (a :: *)) where
-  data SliceDa (SKVar a) = SVar VarIx (ExTyRepr a)
-  type SliceTy (SKVar a) = a
-  sliceAsRepr (SVar _ ea) = ea
+  -- sliceAsRepr :: SliceDa w -> UnivTyRepr (SliceTy w)
+
+instance (K3BaseTy a, r0 ~ r) => Slice r0 (SKVar (r :: * -> *) (a :: *)) where
+  data SliceDa (SKVar r a) = SVar (r a)
+  type SliceTy (SKVar r a) = a
 
-instance (Slice s) => Slice (SKJust s) where
+  -- sliceAsRepr (SVar _ ea) = ea
+
+instance (K3BaseTy a) => Slice r (SKUnk (a :: *)) where
+  data SliceDa (SKUnk a) = SUnk
+  type SliceTy (SKUnk a) = a
+
+  -- sliceAsRepr (SUnk ea) = ea
+
+instance (Slice r s) => Slice r (SKJust s) where
   data SliceDa (SKJust s) = SJust (SliceDa s)
   type SliceTy (SKJust s) = Maybe (SliceTy s)
-  sliceAsRepr (SJust a) = ETR $ tMaybe $ unETR $ sliceAsRepr a
 
-instance (Slice sa, Slice sb) => Slice (SKPair sa sb) where
+  -- sliceAsRepr (SJust a) = UTR $ tMaybe $ unUTR $ sliceAsRepr a
+
+instance (Slice r sa, Slice r sb) => Slice r (SKPair sa sb) where
   data SliceDa (SKPair sa sb) = SPair (SliceDa sa) (SliceDa sb)
   type SliceTy (SKPair sa sb) = (SliceTy sa, SliceTy sb)
-  sliceAsRepr (SPair a b) = ETR $ tPair (unETR $ sliceAsRepr a)
-                                        (unETR $ sliceAsRepr b)
+
+  -- sliceAsRepr (SPair a b) = UTR $ tPair (unUTR $ sliceAsRepr a)
+  --                                       (unUTR $ sliceAsRepr b)
 
 ------------------------------------------------------------------------}}}
 -- Numeric Autocasting
 ------------------------------------------------------------------------{{{
 
+  -- XXX should we make these be constraints in the K3 class so that
+  -- different representations can make different choices?
+
   -- | Unary numerics
 class UnNum a where unneg :: a -> a
 instance UnNum Bool  where unneg = not
@@ -255,7 +300,10 @@ class K3 (r :: * -> *) where
   cAnn      :: Ann -> r a -> r a
 
     -- XXX An escape hatch
-  cUnk      :: r a 
+    --
+    -- The K3 AST has this but uses it for wildcards in slices, which
+    -- we handle with SKUnk/SUnk.
+  -- cUnk      :: r a 
 
     -- XXX cAddress  :: AddrIx -> r AddrIx
   cBool     :: Bool -> r Bool
@@ -266,16 +314,14 @@ class K3 (r :: * -> *) where
   cString   :: String -> r String
   cUnit     :: r ()
 
-    -- XXX polymorphic type because the expression might be
-    -- well-formed; we'll have to resolve it later.
-  eVar      :: VarIx -> r a
+  eVar      :: VarIx -> UnivTyRepr a -> r a
 
   ePair     :: r a -> r b -> r (a,b)
   eJust     :: r a -> r (Maybe t)
 
   eEmpty    :: (K3AST_Coll_C r c) => r (CTE c e)
   eSing     :: (K3AST_Coll_C r c) => r e -> r (CTE c e)
-  eComb     :: r (CTE c e) -> r (CTE c e) -> r (CTE c e)
+  eCombine  :: r (CTE c e) -> r (CTE c e) -> r (CTE c e)
   eRange    :: r Int -> r Int -> r Int -> r (CTE c Int)
 
   eAdd      :: (BiNum a b) => r a -> r b -> r (BNTF a b)
@@ -290,7 +336,7 @@ class K3 (r :: * -> *) where
 
     -- Unlike traditional lambdas, we require a witness
     -- that the argument is admissible in K3.
-  eLam      :: (K3AST_Pat_C r w, Pat w)
+  eLam      :: (K3AST_Pat_C r w, Pat w, K3BaseTy (PatTy w))
             => PatDa w -> (PatReprFn w r -> r b) -> r (PatTy w -> b)
   eApp      :: r (a -> b) -> r a -> r b
 
@@ -307,10 +353,28 @@ class K3 (r :: * -> *) where
 
     -- | Called Aggregate in K3's AST
   eFold     :: r ((t', t) -> t') -> r t' -> r (CTE c t) -> r t'
-  eGBA      :: r (t -> t'') -> r ((t',t) -> t') -> r t' -> r (CTE c t) -> r (CTE c (t'',t'))
-
-  eSort     :: r (CTE c t) -> r ((t,t) -> Bool) -> r (CTE 'CList t)
 
+    -- | Group-By-Aggregate.
+    --
+    -- Note that the Fold argument is guaranteed to be called
+    -- once per partition: any partitions that would be the Zero
+    -- are not created by the Partitioner.
+  eGBA      :: r (t -> t'')       -- ^ Partitioner
+            -> r ((t',t) -> t')   -- ^ Folder
+            -> r t'               -- ^ Zero for each partition
+            -> r (CTE c t)        -- ^ Input collection
+            -> r (CTE c (t'',t'))
+
+  eSort     :: r (CTE c t)        -- ^ Input collection
+            -> r ((t,t) -> Bool)  -- ^ Less-or-equal
+            -> r (CTE 'CList t)
+
+    -- | Peek an element from a collection.
+    --
+    -- Fails on empty collections.
+    --
+    -- For lists, this returns the head; for sets and bags
+    -- it samples arbitrarily.
   ePeek     :: r (CTE c e) -> r e
 
     -- | Slice out from a collection; the slice's type and
@@ -318,15 +382,16 @@ class K3 (r :: * -> *) where
     --
     -- Rather like lambdas, except that the witness is also
     -- a mandatory part of the definition of "slice" :)
-  eSlice    :: (K3AST_Slice_C r w, Slice w, SliceTy w ~ t)
+  eSlice    :: (K3AST_Slice_C r w, Slice w, SliceTy w ~ t)
             => SliceDa w -> r (CTE c t) -> r (CTE c t)
 
   eInsert   :: r (CTE c t) -> r t -> r ()
   eDelete   :: r (CTE c t) -> r t -> r ()
   eUpdate   :: r (CTE c t) -> r t -> r t -> r ()
 
-  -- XXX eAssign
-  -- XXX eDeref
+  eAssign   :: r (Ref t) -> r t -> r ()
+  eDeref    :: r (Ref t) -> r t
+
   -- XXX eSend
 
 ------------------------------------------------------------------------}}}
diff --git a/src/Dyna/BackendK3/Automation.hs b/src/Dyna/BackendK3/Automation.hs
new file mode 100644 (file)
index 0000000..ebfaf3d
--- /dev/null
@@ -0,0 +1,88 @@
+---------------------------------------------------------------------------
+-- Header material
+------------------------------------------------------------------------{{{
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Dyna.BackendK3.Automation where
+
+import           Data.Word
+import           Text.PrettyPrint.Free
+
+import           Dyna.BackendK3.AST
+import           Dyna.BackendK3.Render
+
+  -- | Demote a collection type annotation (of kind CKind) to the
+  -- appropriate chunk of data for case analysis.
+  --
+  -- Note that this only works once the type has become monomorphic;
+  -- otherwise it imposes a constraint on the haskell tyvar.
+  -- (This is a total function)
+class K3AutoColl (c :: CKind) where autocoll :: CollTy c
+instance K3AutoColl CBag where autocoll = CTBag
+instance K3AutoColl CList where autocoll = CTList
+instance K3AutoColl CSet where autocoll = CTSet
+
+  -- | Attempt to automatically derive a universal type representation.
+  --
+  -- Note that this only works once the type has become monomorphic;
+  -- otherwise it imposes a constraint on the haskell tyvar.
+  -- (This is a total function)
+class    K3AutoTy a      where autoty :: UnivTyRepr a
+instance K3AutoTy Bool   where autoty = tBool
+instance K3AutoTy Word8  where autoty = tByte
+instance K3AutoTy Float  where autoty = tFloat
+instance K3AutoTy Int    where autoty = tInt
+instance K3AutoTy String where autoty = tString
+instance K3AutoTy ()     where autoty = tUnit
+instance (K3AutoColl c, K3AutoTy a) => K3AutoTy (CTE c a) where
+  autoty = tColl autocoll autoty
+instance (K3AutoTy a) => K3AutoTy (Maybe a) where autoty = tMaybe autoty
+instance (K3AutoTy a) => K3AutoTy (Ref a) where autoty = tRef autoty
+instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a,b) where
+  autoty = tPair autoty autoty
+instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a -> b) where
+  autoty = tFun autoty autoty
+
+data ExVarTy = forall t . EVT VarIx (UnivTyRepr t)
+
+showEVT :: ExVarTy -> Doc e
+showEVT evt = case evt of EVT (Var vn) utr ->     text vn
+                                              <+> colon
+                                              <+> unAsK3Ty (unUTR utr)
+
+newtype VarsInK3 a = VIK [ExVarTy]
+
+sVIK :: VarsInK3 t -> Doc e
+sVIK (VIK vs) = list $ map showEVT vs
+
+instance K3 VarsInK3 where
+  type K3AST_Coll_C VarsInK3 c = ()
+  type K3AST_Pat_C VarsInK3 p = ()
+  type K3AST_Slice_C VarsInK3 s = ()
+
+  cComment _ v = v
+  cAnn _ a = a
+
+  cBool  _ = VIK []
+  cByte  _ = VIK []
+  cFloat _ = VIK []
+
+  eVar vi r = let x = VIK [EVT vi r] in x
+
+  eIter (VIK f) (VIK c) = VIK $ f ++ c
+
+  -- XXX etc
index 209cc0f1634440adb36d9f91a55dbf800cdd7213..6248e252c35a45bc81ec74746a3acfff735bf9aa 100644 (file)
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 
 
 module Dyna.BackendK3.Examples where
 
 import           Dyna.BackendK3.AST
+import           Dyna.BackendK3.Automation
 import           Dyna.BackendK3.Render
 
 ------------------------------------------------------------------------}}}
--- Example cases
+-- Example cases: macros
 ------------------------------------------------------------------------{{{
 
-macro_caseMaybe :: (K3 r, K3AST_Pat_C r (PKJust (PKVar a)))
-                => ExTyRepr a
+macro_caseMaybe :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKJust (PKVar a)))
+                => UnivTyRepr a
                 -> r (Maybe a)
                 -> r b
                 -> (r a -> r b)
                 -> r b
 macro_caseMaybe w m n b = eITE (eEq m cNothing)
-                                n
-                                (eApp (eLam (PJust (PVar w)) b) m)
+                               n
+                               (eApp (eLam (PJust (PVar w)) b) m)
 
 test_macroCM = Decl (Var "nocase")
                     (tInt)
-                    $Just $ macro_caseMaybe tInt (eVar (Var "test")) (cInt 0) (id)
+                    $Just $ macro_caseMaybe tInt (eVar (Var "test") autoty) (cInt 0) (id)
+
+macro_simple_join2 :: (K3 r, K3AutoTy a, K3BaseTy a, K3AST_Pat_C r (PKVar a),
+                             K3AutoTy b, K3BaseTy b, K3AST_Pat_C r (PKVar b))
+                   => r (CTE c1 a) -> r (CTE c2 b) -> r (a -> b -> Bool) -> r ()
+macro_simple_join2 c1 c2 p =
+    flip eIter c1 $ eLam (PVar autoty) $ \a -> flip eIter c2
+                  $ eLam (PVar autoty) $ \b -> eITE (eApp (eApp p a) b) (cUnit) (cUnit)
+
+macro_emptyPeek :: (K3AST_Coll_C r c, K3AST_Pat_C r (PKVar a),
+                    K3 r, K3BaseTy a, K3AutoTy a)
+                => r (CTE c a) -> r b -> (r a -> r b) -> r b
+macro_emptyPeek c e l = eITE (eEq c eEmpty)
+                             e
+                             (eApp (eLam (PVar autoty) l) $ ePeek c)
+
+------------------------------------------------------------------------}}}
+-- Example cases: misc
+------------------------------------------------------------------------{{{
+
 
 testdecf = Decl (Var "f")
                 (tColl CTBag (tPair tInt tInt))
@@ -44,11 +65,11 @@ testdecf = Decl (Var "f")
 
 testmfn = Decl (Var "negAddOne")
                (tFun tInt tInt)
-               $Just (eLam (PVar $ ETR tInt) (\a -> eNeg $ eAdd a $ cInt 1))
+               $Just (eLam (PVar $ UTR tInt) (\a -> eNeg $ eAdd a $ cInt 1))
 
 booli = Decl (Var "booli")
              (tFun tBool tInt)
-             $ Just (eLam (PVar (ETR tBool)) (\b -> eITE b (cInt 1) (cInt 0)))
+             $ Just (eLam (PVar (UTR tBool)) (\b -> eITE b (cInt 1) (cInt 0)))
 
 testcfn = Decl (Var "cfn")
                (tFun tInt $ tColl CTSet tInt)
@@ -59,9 +80,66 @@ 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)
+lamslice = eLam (PVar autoty) $ \a ->
+             eSlice (SPair (SVar a) (SVar (cInt 4)))
+                    (eSing (ePair (cInt 3) (cInt 4)) `asColl` CTSet)
+
+    -- XXX Man we need better tuple handling.
+project = eLam (PPair (PVar autoty) (PVar autoty))
+               $ \(x,c) -> eMap (eLam (PPair (PVar autoty)
+                                      (PPair (PVar autoty)
+                                             (PVar autoty)))
+                                      $ \(_,(y,z)) -> ePair y z)
+                                (eSlice (SPair (SVar x) (SPair SUnk SUnk)) c)
+
+    -- Sum-Singleton case from M3ToK3 test
+    -- It is safe to leave off the top-level signature
+sumsing :: (K3 r, K3AutoColl c, K3AutoColl c',
+           K3AST_Coll_C r c,
+           K3AST_Coll_C r c',
+           K3AST_Pat_C r (PKVar (Int, (Int, Int))),
+           K3AST_Pat_C r (PKVar (CTE c (Int, (Int, Int)))),
+           K3AST_Pat_C r (PKVar (CTE c' (Int, (Int, Int)))),
+           K3AST_Pat_C r (PKPair (PKVar Int) (PKPair (PKVar Int) (PKVar Int))),
+           K3AST_Slice_C r (SKPair (SKVar r Int) (SKPair (SKVar r Int) (SKUnk Int)))
+           )
+        => r Int -> r Int
+        -> r (CTE c (Int, (Int,Int))) -> r (CTE c' (Int, (Int,Int)))
+        -> r Int
+sumsing (ix :: r Int) iy c1 c2 = eAdd (v c1) (v c2)
+ where
+    -- It is safe to eliminate this type signature
+  si :: SliceDa (SKPair (SKVar r Int) (SKPair (SKVar r Int) (SKUnk Int)))
+  si = SPair (SVar ix) (SPair (SVar iy) SUnk)
+
+    -- XXX unfortunately, we have to be explicit about the forall c1 here;
+    -- eliminating this type signature results in unified collection types
+    -- for c1 and c2 above.
+  v :: (K3AST_Pat_C r ('PKVar (CTE c1 (Int, (Int, Int)))),
+       K3AST_Coll_C r c1, K3AutoColl c1)
+    => r (CTE c1 (Int, (Int, Int))) -> r Int
+  v c = eApp (eLam (PVar autoty)
+                   (\cv -> macro_emptyPeek
+                             cv (cInt 0)
+                             (\nec -> eApp (eLam (PPair (PVar autoty)
+                                                 (PPair (PVar autoty)
+                                                        (PVar autoty)))
+                                           (\(_,(_,proj)) -> proj))
+                                         nec)))
+            (eSlice si c)
+
+------------------------------------------------------------------------}}}
+-- Example cases: misc badness
+------------------------------------------------------------------------{{{
+
+-- We can write this with undefined, but it will induce a
+-- constraint K3BaseTy (Bool -> b).  Note that if b ever
+-- became monomorphic, the search would fail; further,
+-- trying to fill in the undefined will make it monomorphic. :)
+--
+-- That is, we are prevented from ever actually writing this thing out
+-- to the K3 compiler.
+testHOF = eLam (PVar undefined) $ \x -> eApp x (cBool True)
 
 ------------------------------------------------------------------------}}}
 -- fin
index e6ea815151e526697d887237138ed4aea36ef79d..0798b88a2db9831d42b578ecf9a953acfda5f5f7 100644 (file)
@@ -3,8 +3,10 @@
 ------------------------------------------------------------------------{{{
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE Rank2Types #-}
@@ -41,13 +43,15 @@ instance K3Ty (AsK3Ty e) where
 
   tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ]
 
-  tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe " <> ta
+  tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> ta
 
   tColl CTSet  (AsK3Ty ta) = AsK3Ty$ braces   ta
   tColl CTBag  (AsK3Ty ta) = AsK3Ty$ encBag   ta
   tColl CTList (AsK3Ty ta) = AsK3Ty$ brackets ta
 
-  tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta <> " -> " <> tb
+  tFun (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ ta <+> "->" <+> tb
+
+  tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta
 
 ------------------------------------------------------------------------}}}
 -- Collection handling
@@ -76,10 +80,10 @@ instance K3CFn CBag where
 class (Pat w) => K3PFn w where
   k3pfn :: Int -> PatDa w -> (Int, Doc e, PatReprFn w (AsK3 e))
 
-instance K3PFn (PKVar (a :: *)) where
+instance (K3BaseTy a) => K3PFn (PKVar (a :: *)) where
   k3pfn n (PVar tr) = let sn = text $ "x" ++ show n in
                       (n+1
-                      ,sn <> colon <> unAsK3Ty (unETR tr)
+                      ,sn <> colon <> unAsK3Ty (unUTR tr)
                       ,AsK3$const$ sn)
 
 instance (K3PFn w) => K3PFn (PKJust w) where
@@ -96,17 +100,21 @@ instance (K3PFn wa, K3PFn wb) => K3PFn (PKPair wa wb) where
 -- Slice handling
 ------------------------------------------------------------------------{{{
 
-class (Slice w) => K3SFn w where
-  k3sfn :: SliceDa w -> Doc e
+class (Slice (AsK3 e) w) => K3SFn e w where
+  k3sfn :: SliceDa w -> AsK3 e (SliceTy w)
+
+instance (K3BaseTy a) => K3SFn e (SKVar (AsK3 e) (a :: *)) where
+  k3sfn (SVar r) = r
 
-instance K3SFn (SKVar (a :: *)) where
-  k3sfn (SVar (Var v) _) = text v
+instance (K3BaseTy a) => K3SFn e (SKUnk (a :: *)) where
+  k3sfn SUnk = AsK3$ const$ text "_"
 
-instance (K3SFn s) => K3SFn (SKJust s) where
-  k3sfn (SJust s) = "Just" <> parens (k3sfn s)
+instance (K3SFn e s) => K3SFn e (SKJust s) where
+  k3sfn (SJust s) = AsK3$ \n -> "Just" <> parens (unAsK3 (k3sfn s) n)
 
-instance (K3SFn sa, K3SFn sb) => K3SFn (SKPair sa sb) where
-  k3sfn (SPair sa sb) = tupled [ k3sfn sa, k3sfn sb ]
+instance (K3SFn e sa, K3SFn e sb) => K3SFn e (SKPair sa sb) where
+  k3sfn (SPair sa sb) = AsK3$ \n -> tupled [ unAsK3 (k3sfn sa) n
+                                           , unAsK3 (k3sfn sb) n ]
 
 ------------------------------------------------------------------------}}}
 -- Expression handling
@@ -117,7 +125,7 @@ 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
+  type K3AST_Slice_C (AsK3 e) s = K3SFn s
 
   cAnn (Ann anns) (AsK3 e) = AsK3$ \n ->
        parens (e n) <> " @ "
@@ -132,9 +140,8 @@ instance K3 (AsK3 e) where
   cString n     = AsK3$const$ text$ show n
   cNothing      = AsK3$const$ "nothing"
   cUnit         = AsK3$const$ "unit"
-  cUnk          = AsK3$const$ "_"
 
-  eVar (Var v) = AsK3$const$text v
+  eVar (Var v) = AsK3$const$text v
 
 
   ePair (AsK3 a) (AsK3 b) = AsK3$ \n -> tupled [a n, b n]
@@ -142,11 +149,11 @@ instance K3 (AsK3 e) where
 
   eEmpty = k3cfn_empty
   eSing  = k3cfn_sing
-  eComb (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> " ++ " <> parens (b n)
+  eCombine (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> " ++ " <> parens (b n)
   eRange (AsK3 f) (AsK3 l) (AsK3 s) = builtin "range" [ f, l, s ]
   
-  eAdd (AsK3 a) (AsK3 b) = AsK3$ \n -> a n <> "+" <> b n
-  eMul (AsK3 a) (AsK3 b) = AsK3$ \n -> a n <> "*" <> b n
+  eAdd = binop "+"
+  eMul = binop "*"
   eNeg (AsK3 b) = AsK3$ \n -> "-" <> parens (b n)
 
   eEq  = binop "=="
@@ -155,19 +162,20 @@ instance K3 (AsK3 e) where
   eNeq = binop "!="
 
   eLam w f = AsK3$ \n -> let (n', pat, arg) = k3pfn n w
-                         in "\\" <> pat <> " -> " <> (unAsK3 (f arg) n')
+                         in align ("\\" <> pat <+> "->" `above` unAsK3 (f arg) n')
 
   eApp (AsK3 f) (AsK3 x) = AsK3$ \n ->
-    parens (parens (f n) <> space <> parens (x n))
+    parens (parens (f n) `aboveBreak` parens (x n))
 
   eBlock ss (AsK3 r) = AsK3$ \n -> 
     "do" <> (semiBraces (map ($ n) ((map unAsK3 ss) ++ [r])))
 
   eIter (AsK3 f) (AsK3 c) = builtin "iterate" [ f, c ]
 
-  eITE (AsK3 b) (AsK3 t) (AsK3 e) = AsK3$ \n ->    "if "     <> parens (b n)
-                                                <> " then "  <> parens (t n)
-                                                <> " else "  <> parens (e n)
+  eITE (AsK3 b) (AsK3 t) (AsK3 e) = AsK3$ \n ->
+    "if" <+> (align $ above (parens (b n))
+                            ("then" <+> parens (t n) `aboveBreak`
+                             "else"  <+> parens (e n)))
 
   eMap     (AsK3 f) (AsK3 c)                   = builtin "map"       [ f, c    ]
   eFiltMap (AsK3 f) (AsK3 m) (AsK3 c)          = builtin "filtermap" [ f, m, c ]
@@ -177,12 +185,17 @@ instance K3 (AsK3 e) where
   eSort    (AsK3 c) (AsK3 f)                   = builtin "sort"      [ c, f ]
   ePeek    (AsK3 c)                            = builtin "peek"      [ c ]
 
-  eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (k3sfn w)
+  eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (k3sfn w) n)
 
   eInsert (AsK3 c) (AsK3 e)          = builtin "insert" [ c, e ]
   eDelete (AsK3 c) (AsK3 e)          = builtin "delete" [ c, e ]
   eUpdate (AsK3 c) (AsK3 o) (AsK3 n) = builtin "update" [ c, o, n ]
 
+  eAssign          = binop "<-" 
+  eDeref  (AsK3 r) = builtin "deref" [ r ]
+    -- XXX that doesn't seem to actually be right!
+   
+
 ------------------------------------------------------------------------}}}
 -- Miscellany
 ------------------------------------------------------------------------{{{
@@ -190,19 +203,21 @@ instance K3 (AsK3 e) where
 encBag :: Doc e -> Doc e
 encBag = enclose "{|" "|}"
 
-    -- Overly polymorphic; use only when correct
-binop :: Doc e -> AsK3 e a -> AsK3 e a -> AsK3 e b
-binop o (AsK3 a) (AsK3 b) = AsK3$ \n -> parens (a n) <> o <> parens (b n)
+    -- Overly polymorphic; use only when correct!
+binop :: Doc e -> AsK3 e a -> AsK3 e b -> AsK3 e c
+binop o (AsK3 a) (AsK3 b) = AsK3$ \n ->     parens (align $ a n)
+                                        </> o
+                                        </> parens (align $ b n)
 
-    -- Overly polymorphic; use only when correct
+    -- Overly polymorphic; use only when correct!
 builtin :: Doc e -> [ Int -> Doc e ] -> AsK3 e b
 builtin fn as = AsK3$ \n -> fn <> tupled (map ($ n) as)
 
 instance Show (AsK3 e a) where
   show (AsK3 f) = show $ f 0
 
-sh :: AsK3 e a -> String
-sh = show
+sh :: AsK3 e a -> Doc e
+sh (AsK3 f) = f 0
 
 instance Show (AsK3Ty e a) where
   show (AsK3Ty f) = show f