From 8efcc43800e8129e5308e9f11f4a8cde8d131c83 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Wed, 26 Sep 2012 03:22:23 -0400 Subject: [PATCH] Snapshotting before I try to replace pairs with tuples --- src/Dyna/BackendK3/AST.hs | 177 +++++++++++++++++++++---------- src/Dyna/BackendK3/Automation.hs | 88 +++++++++++++++ src/Dyna/BackendK3/Examples.hs | 100 +++++++++++++++-- src/Dyna/BackendK3/Render.hs | 75 +++++++------ 4 files changed, 343 insertions(+), 97 deletions(-) create mode 100644 src/Dyna/BackendK3/Automation.hs diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs index 16a9c91..92ab55e 100644 --- a/src/Dyna/BackendK3/AST.hs +++ b/src/Dyna/BackendK3/AST.hs @@ -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 r (w :: SKind) where data SliceDa w :: * type SliceTy w :: * - sliceAsRepr :: SliceDa w -> ExTyRepr (SliceTy w) - -- Slice variables are VarIx and representation of K3 type -instance Slice (SKVar (a :: *)) where - data SliceDa (SKVar a) = SVar VarIx (ExTyRepr a) - type SliceTy (SKVar a) = a - sliceAsRepr (SVar _ ea) = ea + -- sliceAsRepr :: SliceDa w -> UnivTyRepr (SliceTy w) + +instance (K3BaseTy a, r0 ~ r) => Slice r0 (SKVar (r :: * -> *) (a :: *)) where + data SliceDa (SKVar r a) = SVar (r a) + type SliceTy (SKVar r a) = a -instance (Slice s) => Slice (SKJust s) where + -- sliceAsRepr (SVar _ ea) = ea + +instance (K3BaseTy a) => Slice r (SKUnk (a :: *)) where + data SliceDa (SKUnk a) = SUnk + type SliceTy (SKUnk a) = a + + -- sliceAsRepr (SUnk ea) = ea + +instance (Slice r s) => Slice r (SKJust s) where data SliceDa (SKJust s) = SJust (SliceDa s) type SliceTy (SKJust s) = Maybe (SliceTy s) - sliceAsRepr (SJust a) = ETR $ tMaybe $ unETR $ sliceAsRepr a -instance (Slice sa, Slice sb) => Slice (SKPair sa sb) where + -- sliceAsRepr (SJust a) = UTR $ tMaybe $ unUTR $ sliceAsRepr a + +instance (Slice r sa, Slice r sb) => Slice r (SKPair sa sb) where data SliceDa (SKPair sa sb) = SPair (SliceDa sa) (SliceDa sb) type SliceTy (SKPair sa sb) = (SliceTy sa, SliceTy sb) - sliceAsRepr (SPair a b) = ETR $ tPair (unETR $ sliceAsRepr a) - (unETR $ sliceAsRepr b) + + -- sliceAsRepr (SPair a b) = UTR $ tPair (unUTR $ sliceAsRepr a) + -- (unUTR $ sliceAsRepr b) ------------------------------------------------------------------------}}} -- Numeric Autocasting ------------------------------------------------------------------------{{{ + -- XXX should we make these be constraints in the K3 class so that + -- different representations can make different choices? + -- | Unary numerics class UnNum a where unneg :: a -> a instance UnNum Bool where unneg = not @@ -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 r w, SliceTy w ~ t) => SliceDa w -> r (CTE c t) -> r (CTE c t) eInsert :: r (CTE c t) -> r t -> r () eDelete :: r (CTE c t) -> r t -> r () eUpdate :: r (CTE c t) -> r t -> r t -> r () - -- XXX eAssign - -- XXX eDeref + eAssign :: r (Ref t) -> r t -> r () + eDeref :: r (Ref t) -> r t + -- XXX eSend ------------------------------------------------------------------------}}} diff --git a/src/Dyna/BackendK3/Automation.hs b/src/Dyna/BackendK3/Automation.hs new file mode 100644 index 0000000..ebfaf3d --- /dev/null +++ b/src/Dyna/BackendK3/Automation.hs @@ -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 diff --git a/src/Dyna/BackendK3/Examples.hs b/src/Dyna/BackendK3/Examples.hs index 209cc0f..6248e25 100644 --- a/src/Dyna/BackendK3/Examples.hs +++ b/src/Dyna/BackendK3/Examples.hs @@ -12,31 +12,52 @@ {-# 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 diff --git a/src/Dyna/BackendK3/Render.hs b/src/Dyna/BackendK3/Render.hs index e6ea815..0798b88 100644 --- a/src/Dyna/BackendK3/Render.hs +++ b/src/Dyna/BackendK3/Render.hs @@ -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 e 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 -- 2.50.1