From 81aa1de717885b995cb8f1618a8f6f5a6a01148f Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Tue, 2 Oct 2012 01:22:15 -0400 Subject: [PATCH] Commit some incremental progress on the K3 AST This snapshots some crude attempts at getting generic tuples into the K3 AST. At the moment it isn't working (for somewhat annoying reasons involving universal quantification, I think) and the AST is wired up to have tuples 2-4 (though more are a simple matter of copy-paste-modify in a few places); some bits are automated, but many aren't. --- src/Dyna/BackendK3/AST.hs | 181 +++++++++++++++++++------------ src/Dyna/BackendK3/Automation.hs | 43 +++++++- src/Dyna/BackendK3/Examples.hs | 71 ++++++------ src/Dyna/BackendK3/Render.hs | 176 +++++++++++++++++++++--------- src/Dyna/XXX/MonadUtils.hs | 9 ++ src/Dyna/XXX/THTuple.hs | 64 +++++++++++ src/Dyna/XXX/THTupleInternals.hs | 143 ++++++++++++++++++++++++ 7 files changed, 526 insertions(+), 161 deletions(-) create mode 100644 src/Dyna/XXX/MonadUtils.hs create mode 100644 src/Dyna/XXX/THTuple.hs create mode 100644 src/Dyna/XXX/THTupleInternals.hs diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs index 92ab55e..7b46704 100644 --- a/src/Dyna/BackendK3/AST.hs +++ b/src/Dyna/BackendK3/AST.hs @@ -1,32 +1,33 @@ --------------------------------------------------------------------------- --- Header material -------------------------------------------------------------------------{{{ +-- | An AST for K3. +-- +-- To as large of an extent as possible, we wish to capture the static +-- semantics of K3 in the Haskell type system. + +-- 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 TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} - -- | An AST for K3. - -- - -- To as large of an extent as possible, we wish to capture the static - -- semantics of K3 in the Haskell type system. module Dyna.BackendK3.AST where import Data.Word import GHC.Prim (Constraint) +import Language.Haskell.TH (varT, mkName) + +import Dyna.XXX.THTuple ------------------------------------------------------------------------}}} --- Preliminaries -------------------------------------------------------------------------{{{ +-- Preliminaries {{{ newtype VarIx = Var String newtype AddrIx = Addr (String,Int) @@ -34,8 +35,7 @@ newtype AddrIx = Addr (String,Int) data Ann = Ann [String] ------------------------------------------------------------------------}}} --- Collections -------------------------------------------------------------------------{{{ +-- Collections {{{ data CKind = CBag | CList | CSet @@ -47,8 +47,7 @@ data CollTy c where CTSet :: CollTy CSet ------------------------------------------------------------------------}}} --- Effectables (XXX TODO) -------------------------------------------------------------------------{{{ +-- Effectables (XXX TODO) {{{ {- data MKind = MKImmut | MKMut @@ -67,8 +66,7 @@ data VTy v where data Ref a = Ref ------------------------------------------------------------------------}}} --- Type System -------------------------------------------------------------------------{{{ +-- Type System {{{ -- | Data level representation of K3 types, indexed by equivalent type in -- Haskell. @@ -86,16 +84,24 @@ class K3Ty (r :: * -> *) where {- TAddress | TTarget BaseTy -} - tPair :: r a -> r b -> r (a,b) + -- 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) + -- tTuple :: (RTupled rt, RTR rt ~ r) => rt -> r (RTE rt) + + -- XXX TUPLES + tTuple2 :: (r a, r b) -> r (a,b) + tTuple3 :: (r a, r b, r c) -> r (a,b,c) + tTuple4 :: (r a, r b, r c, r d) -> r (a,b,c,d) + -- | Existential typeclass wrapper for K3Ty newtype UnivTyRepr (a :: *) = UTR { unUTR :: forall r . (K3Ty r) => r a } + instance K3Ty UnivTyRepr where - tAnn s (UTR t) = UTR$tAnn s t + tAnn s (UTR t) = UTR $ tAnn s t tBool = UTR tBool tByte = UTR tByte tFloat = UTR tFloat @@ -104,11 +110,16 @@ instance K3Ty UnivTyRepr where 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 + 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 TUPLES + tTuple2 us = UTR $ tTuple2 $ tupleopRS unUTR us + tTuple3 us = UTR $ tTuple3 $ tupleopRS unUTR us + tTuple4 us = UTR $ tTuple4 $ tupleopRS unUTR us + -- | A constraint for "base" types in K3. These are the things that can -- be passed to lambdas. Essentially everything other than arrows. @@ -123,16 +134,21 @@ 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) +instance (K3BaseTy a, K3BaseTy b, K3BaseTy c) => K3BaseTy (a,b,c) ------------------------------------------------------------------------}}} --- Pattern System -------------------------------------------------------------------------{{{ +-- Pattern System {{{ -- | Kinds of patterns permitted in K3 data PKind where PKVar :: k -> PKind PKJust :: PKind -> PKind - PKPair :: PKind -> PKind -> PKind + + -- XXX TUPLES + PKTuple2 :: (PKind, PKind) -> PKind + PKTuple3 :: (PKind, PKind, PKind) -> PKind + PKTuple4 :: (PKind, PKind, PKind, PKind) -> PKind + -- PKTup :: [PKind] -> PKind -- | Provides witnesses that certain types may be used -- as arguments to K3 lambdas. Useful when building @@ -162,17 +178,12 @@ class Pat (w :: PKind) where -- | The type of this pattern. type PatReprFn w (r :: * -> *) :: * - -- | Produce a data-level type representation for this witness - -- patAsRepr :: PatDa w -> UnivTyRepr (PatTy w) - 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 + 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 - instance (Pat w) => Pat (PKJust w) where -- | Just patterns (fail on Nothing) -- @@ -184,67 +195,99 @@ instance (Pat w) => Pat (PKJust w) where type PatBTy (PKJust w) = PatBTy w type PatReprFn (PKJust w) r = PatReprFn w r - --patAsRepr (PJust w') = UTR $ tMaybe $ unUTR $ patAsRepr w' - -instance (Pat wa, Pat wb) => Pat (PKPair wa wb) where +{- +instance (Pat wa, Pat wb) => Pat (PKPair '(wa,wb)) where -- | Pair patterns -- -- Product patterns, on the other hand, have PatTy and PatReprFn both -- producing tuples. - data PatDa (PKPair wa wb) = PPair (PatDa wa) (PatDa wb) - type PatTy (PKPair wa wb) = (PatTy wa, PatTy wb) - type PatBTy (PKPair wa wb) = (PatBTy wa, PatBTy wb) - type PatReprFn (PKPair wa wb) r = (PatReprFn wa r, PatReprFn wb r) + 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) = UTR $ tPair (unUTR $ patAsRepr wa) - -- (unUTR $ patAsRepr wb) + -- XXX TUPLES +$( mapM (mkRecClass (''Pat,[]) (\n -> mkName $ "PKTuple" ++ show n) + [(''PatDa,\n -> mkName $ "PTuple" ++ show n )] + [''PatTy, ''PatBTy] [''PatReprFn]) + [2..4] + ) + +{- + -- Tragically patterns based on tuples are still represented + -- in Haskell as right-branching, unit-ending. +instance Pat (PKTup '[]) where + data PatDa (PKTup '[]) = PTupN + type PatTy (PKTup '[]) = () + type PatBTy (PKTup '[]) = () + type PatReprFn (PKTup '[]) r = r () + +instance Pat (PKTup as) => Pat (PKTup (a ': as)) where + data PatDa (PKTup (a ': as)) = PTupC (PatDa a) (PatDa (PKTup as)) + type PatTy (PKTup (a ': as)) = (PatTy a, PatTy (PKTup as)) + type PatBTy (PKTup (a ': as)) = (PatBTy a, PatBTy (PKTup as)) + type PatReprFn (PKTup (a ': as)) r = (PatReprFn a r, PatReprFn (PKTup as) r) +-} ------------------------------------------------------------------------}}} --- Slice System -------------------------------------------------------------------------{{{ +-- Slice System {{{ -- | Kinds of slices permitted in K3 data SKind where SKVar :: r -> k -> SKind SKUnk :: k -> SKind SKJust :: SKind -> SKind - SKPair :: SKind -> SKind -> SKind + + -- XXX TUPLES + SKTuple2 :: (SKind, SKind) -> SKind + SKTuple3 :: (SKind, SKind, SKind) -> SKind + SKTuple4 :: (SKind, SKind, SKind, SKind) -> SKind -- | Witness of slice well-formedness class Slice r (w :: SKind) where data SliceDa w :: * type SliceTy w :: * - -- 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 - -- 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) = UTR $ tMaybe $ unUTR $ sliceAsRepr a +{- +instance (Slice r sa, Slice r sb) => Slice r (SKTuple2 '(sa,sb)) where + data SliceDa (SKTuple2 '(sa,sb)) = STuple2 (SliceDa sa) (SliceDa sb) + type SliceTy (SKTuple2 '(sa,sb)) = (SliceTy sa, SliceTy sb) +-} -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) + -- XXX TUPLES +$( mapM (mkRecClass (''Slice, [varT $ mkName "r"]) + (\n -> mkName $ "SKTuple" ++ show n) + [(''SliceDa,\n -> mkName $ "STuple" ++ show n)] + [''SliceTy] []) + [2..4] ) - -- sliceAsRepr (SPair a b) = UTR $ tPair (unUTR $ sliceAsRepr a) - -- (unUTR $ sliceAsRepr b) + +{- +instance Slice r (SKTup '[]) where + data SliceDa (SKTup '[]) = STupN + type SliceTy (SKTup '[]) = () + +instance Slice r (SKTup as) => Slice r (SKTup (a ': as)) where + data SliceDa (SKTup (a ': as)) = STupC (SliceDa a) (SliceDa (SKTup as)) + type SliceTy (SKTup (a ': as)) = (SliceTy a, SliceTy (SKTup as)) + +-} ------------------------------------------------------------------------}}} --- Numeric Autocasting -------------------------------------------------------------------------{{{ +-- Numeric Autocasting {{{ -- XXX should we make these be constraints in the K3 class so that -- different representations can make different choices? @@ -279,8 +322,7 @@ instance BiNum Float Float where -- XXX More ------------------------------------------------------------------------}}} --- Values and Expressions -------------------------------------------------------------------------{{{ +-- Values and Expressions {{{ class K3 (r :: * -> *) where -- | A representation-specific constraint for collections, on functions @@ -316,9 +358,14 @@ class K3 (r :: * -> *) where eVar :: VarIx -> UnivTyRepr a -> r a - ePair :: r a -> r b -> r (a,b) eJust :: r a -> r (Maybe t) + -- XXX TUPLES + eTuple2 :: (r a, r b) -> r (a,b) + eTuple3 :: (r a, r b, r c) -> r (a,b,c) + eTuple4 :: (r a, r b, r c) -> r (a,b,c) + -- eTuple :: K3RTuple r a -> r a + eEmpty :: (K3AST_Coll_C r c) => r (CTE c e) eSing :: (K3AST_Coll_C r c) => r e -> r (CTE c e) eCombine :: r (CTE c e) -> r (CTE c e) -> r (CTE c e) @@ -395,8 +442,7 @@ class K3 (r :: * -> *) where -- XXX eSend ------------------------------------------------------------------------}}} --- Miscellanious -------------------------------------------------------------------------{{{ +-- Miscellany {{{ -- XXX does not enumerate local variables data Decl tr r t = Decl VarIx (tr t) (Maybe (r t)) @@ -406,7 +452,4 @@ data Decl tr r t = Decl VarIx (tr t) (Maybe (r t)) -- Use as (eEmpty `asColl` CTSet) asColl :: r (CTE c t) -> CollTy c -> r (CTE c t) asColl = const - ------------------------------------------------------------------------}}} --- fin ---------------------------------------------------------------------------- diff --git a/src/Dyna/BackendK3/Automation.hs b/src/Dyna/BackendK3/Automation.hs index ebfaf3d..2751c03 100644 --- a/src/Dyna/BackendK3/Automation.hs +++ b/src/Dyna/BackendK3/Automation.hs @@ -1,6 +1,7 @@ --------------------------------------------------------------------------- --- Header material -------------------------------------------------------------------------{{{ +-- | Various automation assists for working with K3 ASTs + +-- Header material {{{ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} @@ -15,6 +16,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Dyna.BackendK3.Automation where @@ -25,6 +27,9 @@ import Text.PrettyPrint.Free import Dyna.BackendK3.AST import Dyna.BackendK3.Render +------------------------------------------------------------------------}}} +-- Automate collection type {{{ + -- | Demote a collection type annotation (of kind CKind) to the -- appropriate chunk of data for case analysis. -- @@ -36,6 +41,9 @@ instance K3AutoColl CBag where autocoll = CTBag instance K3AutoColl CList where autocoll = CTList instance K3AutoColl CSet where autocoll = CTSet +------------------------------------------------------------------------}}} +-- Automate type {{{ + -- | Attempt to automatically derive a universal type representation. -- -- Note that this only works once the type has become monomorphic; @@ -52,11 +60,35 @@ 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 +instance (K3AutoTy a, K3AutoTy b) => K3AutoTy (a,b) + where autoty = tTuple2 (autoty, autoty) + +instance (K3AutoTy a, K3AutoTy b, K3AutoTy c) => K3AutoTy (a,b,c) + where autoty = tTuple3 (autoty, autoty, autoty) + +{- +class (Pat (PKTup ws), PatTy (PKTup ws) ~ a) => K3AutoTyTup ws a + | ws -> a, a -> ws + where autotytup :: K3RTuple UnivTyRepr a + +instance K3AutoTyTup '[] () where autotytup = K3RTNil + +instance (K3AutoTyTup was as, K3AutoTy a, wa ~ PKVar a, PatTy wa ~ a) + => K3AutoTyTup (wa ': was) (a,as) + where autotytup = K3RTCons autoty autotytup + +instance (K3AutoTyTup (wa ': w) (a,b), K3AutoTyTup w b) + => K3AutoTy (a,b) + where autoty = tTuple autotytup +-} + +------------------------------------------------------------------------}}} +-- Collect variables in a term (XXX TODO) {{{ + +{- data ExVarTy = forall t . EVT VarIx (UnivTyRepr t) showEVT :: ExVarTy -> Doc e @@ -86,3 +118,6 @@ instance K3 VarsInK3 where 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 6248e25..8ff29cd 100644 --- a/src/Dyna/BackendK3/Examples.hs +++ b/src/Dyna/BackendK3/Examples.hs @@ -42,8 +42,8 @@ test_macroCM = Decl (Var "nocase") 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 = + => r (a -> b -> Bool) -> r (CTE c1 a) -> r (CTE c2 b) -> r () +macro_simple_join2 p c1 c2 = flip eIter c1 $ eLam (PVar autoty) $ \a -> flip eIter c2 $ eLam (PVar autoty) $ \b -> eITE (eApp (eApp p a) b) (cUnit) (cUnit) @@ -60,7 +60,7 @@ macro_emptyPeek c e l = eITE (eEq c eEmpty) testdecf = Decl (Var "f") - (tColl CTBag (tPair tInt tInt)) + (tColl CTBag (tTuple2 (tInt,tInt))) Nothing testmfn = Decl (Var "negAddOne") @@ -77,57 +77,60 @@ testcfn = Decl (Var "cfn") testpairfn = Decl (Var "ibfst") - (tFun (tPair tInt tBool) tInt) - $Just (eLam (PPair (PVar tInt) (PVar tBool)) (\(a,b) -> a)) + (tFun (tTuple2 (tInt,tBool)) tInt) + $Just (eLam (PTuple2 (PVar tInt) (PVar tBool)) (\(a,b) -> a)) lamslice = eLam (PVar autoty) $ \a -> - eSlice (SPair (SVar a) (SVar (cInt 4))) - (eSing (ePair (cInt 3) (cInt 4)) `asColl` CTSet) + eSlice (STuple2 (SVar a) (SVar (cInt 4))) + (eSing (eTuple2 (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) +project = eLam (PTuple2 (PVar autoty) (PVar autoty)) + $ \(x,c) -> eMap (eLam (PTuple3 (PVar autoty) + (PVar autoty) + (PVar autoty)) + $ \(_,y,z) -> eTuple2 (y,z)) + (eSlice (STuple3 (SVar x) SUnk SUnk) c) + +proj' = eLam (PTuple3 (PVar tInt) (PVar tInt) (PVar tInt)) + $ \(a,b,c) -> b -- 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) +sumsing (ix :: r Int) (iy :: r Int) 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) + si = STuple3 (SVar ix) (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)))), + 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 + => 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 -> eApp (eLam (PTuple3 (PVar autoty) + (PVar autoty) + (PVar autoty)) + $ \(_,_,proj) -> proj) nec))) (eSlice si c) + -- A very very complicated way of writing "3" +testSumsing = sumsing (cInt 4) (cInt 5) + (eSing (eTuple3 (cInt 4, cInt 5, cInt 1)) `asColl` CTSet) + (eSing (eTuple3 (cInt 4, cInt 5, cInt 2)) `asColl` CTBag) + +testjoin2 c1 c2 = + macro_simple_join2 pred c1 c2 + where p = PTuple3 (PVar tInt) (PVar tInt) (PVar tInt) + pred = (eLam p (\(k1a,k2a,_) -> + eLam p (\(k1b,k2b,_) -> + (eEq k1a k1b) `eAdd` (eEq k2a k2b)))) + + ------------------------------------------------------------------------}}} -- Example cases: misc badness ------------------------------------------------------------------------{{{ diff --git a/src/Dyna/BackendK3/Render.hs b/src/Dyna/BackendK3/Render.hs index 0798b88..a11e949 100644 --- a/src/Dyna/BackendK3/Render.hs +++ b/src/Dyna/BackendK3/Render.hs @@ -1,7 +1,7 @@ --------------------------------------------------------------------------- --- Header material -------------------------------------------------------------------------{{{ -{-# LANGUAGE ConstraintKinds #-} +-- | Provides the "AsK3" type and instances for the K3 AST. + +-- Header material {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -10,19 +10,21 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} - -- | Provides the "AsK3" type and instances for the K3 AST. module Dyna.BackendK3.Render where +import Control.Monad.State import Text.PrettyPrint.Free import Dyna.BackendK3.AST +import Dyna.XXX.MonadUtils +import Dyna.XXX.THTuple ------------------------------------------------------------------------}}} --- Type handling -------------------------------------------------------------------------{{{ +-- Type handling {{{ -- | Unlike AsK3 below, we don't need to thread a variable counter -- around since K3 doesn't have tyvars @@ -41,7 +43,7 @@ instance K3Ty (AsK3Ty e) where tUnit = AsK3Ty$ "unit" tUnk = AsK3Ty$ "_" - tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ] + -- tPair (AsK3Ty ta) (AsK3Ty tb) = AsK3Ty$ tupled [ ta, tb ] tMaybe (AsK3Ty ta) = AsK3Ty$ "Maybe" <+> ta @@ -53,72 +55,135 @@ instance K3Ty (AsK3Ty e) where tRef (AsK3Ty ta) = AsK3Ty$ "ref" <+> ta + -- XXX TUPLES Note the similarities! + tTuple2 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us + tTuple3 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us + tTuple4 us = AsK3Ty $ tupled $ tupleopEL unAsK3Ty us + ------------------------------------------------------------------------}}} --- Collection handling -------------------------------------------------------------------------{{{ +-- Collection handling {{{ class K3CFn (c :: CKind) where k3cfn_empty :: AsK3 e (CTE c a) k3cfn_sing :: AsK3 e vma -> AsK3 e (CTE c vma) instance K3CFn CSet where - k3cfn_empty = AsK3$const$ "{ }" + k3cfn_empty = AsK3$ const$ "{ }" k3cfn_sing (AsK3 e) = AsK3$ braces . e instance K3CFn CList where - k3cfn_empty = AsK3$const$ "[ ]" + k3cfn_empty = AsK3$ const$ "[ ]" k3cfn_sing (AsK3 e) = AsK3$ brackets . e instance K3CFn CBag where - k3cfn_empty = AsK3$const$ "{| |}" + k3cfn_empty = AsK3$ const$ "{| |}" k3cfn_sing (AsK3 e) = AsK3$ encBag . e ------------------------------------------------------------------------}}} --- Pattern handling -------------------------------------------------------------------------{{{ +-- Pattern handling {{{ class (Pat w) => K3PFn w where - k3pfn :: Int -> PatDa w -> (Int, Doc e, PatReprFn w (AsK3 e)) + k3pfn :: Bool -> PatDa w -> State Int (Doc e, PatReprFn w (AsK3 e)) instance (K3BaseTy a) => K3PFn (PKVar (a :: *)) where - k3pfn n (PVar tr) = let sn = text $ "x" ++ show n in - (n+1 - ,sn <> colon <> unAsK3Ty (unUTR tr) - ,AsK3$const$ sn) + k3pfn _ (PVar tr) = do + n <- incState + let sn = text $ "x" ++ show n + return (sn <> colon <> unAsK3Ty (unUTR tr) + ,AsK3$ const$ sn) instance (K3PFn w) => K3PFn (PKJust w) where - k3pfn n (PJust w) = let (n', b, r) = k3pfn n w - in (n', "Just " <> parens b, r) - -instance (K3PFn wa, K3PFn wb) => K3PFn (PKPair wa wb) where - k3pfn n (PPair wa wb) = - let (n', ba, ra) = k3pfn n wa - (n'', bb, rb) = k3pfn n' wb - in (n'', tupled [ ba, bb ], (ra,rb)) + k3pfn _ (PJust w) = do + (p, r) <- k3pfn False w + return ("just " <> parens p, r) + + -- XXX TUPLES this should be automatically generated +instance (K3PFn wa, K3PFn wb) + => K3PFn (PKTuple2 '(wa,wb)) + where + k3pfn _ (PTuple2 wa wb) = do + (ba, ra) <- k3pfn False wa + (bb, rb) <- k3pfn False wb + return (tupled [ ba, bb ], (ra,rb)) + +instance (K3PFn wa, K3PFn wb, K3PFn wc) + => K3PFn (PKTuple3 '(wa,wb,wc)) + where + k3pfn _ (PTuple3 wa wb wc) = do + (ba, ra) <- k3pfn False wa + (bb, rb) <- k3pfn False wb + (bc, rc) <- k3pfn False wc + return (tupled [ ba, bb, bc ], (ra,rb,rc)) + +instance (K3PFn wa, K3PFn wb, K3PFn wc, K3PFn wd) + => K3PFn (PKTuple4 '(wa,wb,wc,wd)) + where + k3pfn _ (PTuple4 wa wb wc wd) = do + (ba, ra) <- k3pfn False wa + (bb, rb) <- k3pfn False wb + (bc, rc) <- k3pfn False wc + (bd, rd) <- k3pfn False wd + return (tupled [ ba, bb, bc, bd ], (ra,rb,rc,rd)) + +{- +instance K3PFn (PKTup '[]) where + k3pfn n _ PTupN = (n, rparen, AsK3$const$rparen) + +instance (Pat (PKTup as), K3PFn (PKTup as), K3PFn a) + => K3PFn (PKTup (a ': as)) where + k3pfn n b (PTupC a as) = let (n', pa, ra) = k3pfn n False a + (n'', ps, rs) = k3pfn n' True as + in (n'', extend pa ps, (ra,rs)) + where + left = if b then comma else lparen + extend pa ps = left <> pa <> ps +-} ------------------------------------------------------------------------}}} --- Slice handling -------------------------------------------------------------------------{{{ +-- Slice handling {{{ class (Slice (AsK3 e) w) => K3SFn e w where - k3sfn :: SliceDa w -> AsK3 e (SliceTy w) + k3sfn :: Bool -> SliceDa w -> AsK3 e (SliceTy w) instance (K3BaseTy a) => K3SFn e (SKVar (AsK3 e) (a :: *)) where - k3sfn (SVar r) = r + k3sfn _ (SVar r) = r instance (K3BaseTy a) => K3SFn e (SKUnk (a :: *)) where - k3sfn SUnk = AsK3$ const$ text "_" + k3sfn _ SUnk = AsK3$ const$ text "_" instance (K3SFn e s) => K3SFn e (SKJust s) where - k3sfn (SJust s) = AsK3$ \n -> "Just" <> parens (unAsK3 (k3sfn s) n) - -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 ] + k3sfn _ (SJust s) = AsK3$ \n -> "Just" <> parens (unAsK3 (k3sfn False s) n) + + -- XXX TUPLES this should be automatically generated +instance (K3SFn e sa, K3SFn e sb) + => K3SFn e (SKTuple2 '(sa,sb)) + where + k3sfn _ (STuple2 sa sb) = + AsK3$ \n -> tupled [ unAsK3 (k3sfn False sa) n + , unAsK3 (k3sfn False sb) n ] + +instance (K3SFn e sa, K3SFn e sb, K3SFn e sc) + => K3SFn e (SKTuple3 '(sa,sb,sc)) + where + k3sfn _ (STuple3 sa sb sc) = + AsK3$ \n -> tupled [ unAsK3 (k3sfn False sa) n + , unAsK3 (k3sfn False sb) n + , unAsK3 (k3sfn False sc) n ] + +{- +instance K3SFn e (SKTup '[]) where + k3sfn _ STupN = AsK3$const$rparen + +instance (Slice (AsK3 e) (SKTup as), K3SFn e (SKTup as), K3SFn e a) + => K3SFn e (SKTup (a ': as)) where + k3sfn b (STupC a as) = AsK3$ \n -> left <> unAsK3 (k3sfn False a) n + <> unAsK3 (k3sfn True as) n + where + left = if b then comma else lparen +-} ------------------------------------------------------------------------}}} --- Expression handling -------------------------------------------------------------------------{{{ +-- Expression handling {{{ newtype AsK3 e (a :: *) = AsK3 { unAsK3 :: Int -> Doc e } @@ -133,19 +198,24 @@ instance K3 (AsK3 e) where cComment str (AsK3 a) = AsK3$ \n -> "\n// " <> text str <> "\n" <> a n - cBool n = AsK3$const$ text$ show n - cByte n = AsK3$const$ text$ show n - cFloat n = AsK3$const$ text$ show n - cInt n = AsK3$const$ text$ show n - cString n = AsK3$const$ text$ show n - cNothing = AsK3$const$ "nothing" - cUnit = AsK3$const$ "unit" + 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" - 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] eJust (AsK3 a) = builtin "Just " [ a ] + -- ePair (AsK3 a) (AsK3 b) = AsK3$ \n -> tupled [a n, b n] + + -- XXX TUPLES Note the similarity of these! + eTuple2 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t + eTuple3 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t + eTuple4 t = AsK3 $ \n -> tupled $ tupleopEL (flip unAsK3 n) t eEmpty = k3cfn_empty eSing = k3cfn_sing @@ -161,7 +231,7 @@ instance K3 (AsK3 e) where eLeq = binop "<=" eNeq = binop "!=" - eLam w f = AsK3$ \n -> let (n', pat, arg) = k3pfn n w + eLam w f = AsK3$ \n -> let ((pat, arg),n') = runState (k3pfn False w) n in align ("\\" <> pat <+> "->" `above` unAsK3 (f arg) n') eApp (AsK3 f) (AsK3 x) = AsK3$ \n -> @@ -185,7 +255,7 @@ 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 (unAsK3 (k3sfn w) n) + eSlice w (AsK3 c) = AsK3$ \n -> c n <> brackets (unAsK3 (k3sfn False w) n) eInsert (AsK3 c) (AsK3 e) = builtin "insert" [ c, e ] eDelete (AsK3 c) (AsK3 e) = builtin "delete" [ c, e ] @@ -197,8 +267,7 @@ instance K3 (AsK3 e) where ------------------------------------------------------------------------}}} --- Miscellany -------------------------------------------------------------------------{{{ +-- Miscellany {{{ encBag :: Doc e -> Doc e encBag = enclose "{|" "|}" @@ -237,5 +306,4 @@ shd (Decl (Var name) tipe body) = <> semi ------------------------------------------------------------------------}}} --- fin ---------------------------------------------------------------------------- + diff --git a/src/Dyna/XXX/MonadUtils.hs b/src/Dyna/XXX/MonadUtils.hs new file mode 100644 index 0000000..857b71e --- /dev/null +++ b/src/Dyna/XXX/MonadUtils.hs @@ -0,0 +1,9 @@ +module Dyna.XXX.MonadUtils(incState) where + +import Control.Monad.State + +incState :: State Int Int +incState = do + s <- get + put $! (s+1) + return s diff --git a/src/Dyna/XXX/THTuple.hs b/src/Dyna/XXX/THTuple.hs new file mode 100644 index 0000000..526b473 --- /dev/null +++ b/src/Dyna/XXX/THTuple.hs @@ -0,0 +1,64 @@ +--------------------------------------------------------------------------- +-- | Template haskell for deriving tuple-handling functions +-- +-- I dearly wish I didn't have to do this kind of thing +-- (and even though I am, it doesn't quite work!) + +-- Header material {{{ + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +module Dyna.XXX.THTuple(Tupled(..),RTupled(..),mkRecClass + ) where + +import Dyna.XXX.THTupleInternals + +------------------------------------------------------------------------}}} +-- Exported classes {{{ + + -- | Some type algebra on tuples full of constructed types + -- which is invariant over the constructor in question + -- + -- e.g. RTER (a,b) r = (r a, r b) +class Tupled base where + -- | Apply r to each element of the tuple + type RTER base (r :: * -> *) :: * + + -- | Shed a type constructor + tupleopR :: (RTupled rbase, (RTR rbase) ~ r, (RTE rbase) ~ base) + => (forall x . r x -> x) -> rbase -> base + + -- | Remap a type constructor + tupleopRS :: (RTupled rbase, (RTR rbase) ~ r, (RTE rbase) ~ base, + RTupled sbase, (RTR sbase) ~ s, (RTE sbase) ~ base) + => (forall x . r x -> s x) -> rbase -> sbase + + -- | Recover the constructor and base type from r-full tuples. + -- + -- e.g. RTR (r a, r b) = r, RTE (r a, r b) = (a, b) +class (Tupled (RTE arred), + RTER (RTE arred) (RTR arred) ~ arred) + => RTupled arred where + type RTR arred :: (* -> *) + type RTE arred :: * + + -- | Eliminate an rtuple out to a list. + tupleopEL :: (RTR arred ~ r) => (forall x . r x -> a) -> arred -> [a] + +------------------------------------------------------------------------}}} +-- Aaaand action {{{ + + -- Generate instances for Tupled +$(mkTupleInstances ''Tupled ''RTER 'tupleopR 'tupleopRS) + + -- Generate instances for RTupled +$(mkRTupleInstances ''RTupled ''RTE ''RTR 'tupleopEL) +------------------------------------------------------------------------}}} + diff --git a/src/Dyna/XXX/THTupleInternals.hs b/src/Dyna/XXX/THTupleInternals.hs new file mode 100644 index 0000000..d389d94 --- /dev/null +++ b/src/Dyna/XXX/THTupleInternals.hs @@ -0,0 +1,143 @@ +--------------------------------------------------------------------------- +-- | Template haskell for deriving tuple-handling functions + +-- Header material {{{ + +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} + +module Dyna.XXX.THTupleInternals where + +import Control.Monad +import GHC.Exts (maxTupleSize) +import Language.Haskell.TH + +------------------------------------------------------------------------}}} +-- Utilities for tuple manipulation in TH land {{{ + + -- XXX +foreachTupleSize f = mapM f [2..10] -- maxTupleSize] + +mkNames n = mapM (newName . ("mti" ++) . show) [1..n] + +genMap app con var = foldl app con . map var + +mkTy n = genMap appT (conT $ tupleTypeName n) varT +mkDa n = genMap appE (conE $ tupleDataName n) varE +mkRTy n r = genMap appT (conT $ tupleTypeName n) (appT r . varT) +mkPTy n = genMap appT (promotedTupleT n) varT + +------------------------------------------------------------------------}}} +-- Make Tuple {{{ + +mkTupleInstance :: Name -> Name -> Name -> Name -> Int -> Q Dec +mkTupleInstance _tc _rter _opr _oprs n | n > 1 = do + -- Build polymorphic variables + names <- mkNames n + + -- Derive the tuple type and data forms + let ty = mkTy n names + + -- The constructor and function argument + vr <- liftM varT $ newName "r" + vf <- newName "f" + + -- Derive the rtuple type + let rty = mkRTy n vr names + + -- Patterns and expressions + let fnames = map (appE (varE vf) . varE) names + let rpa = tupP $ map varP names + let frpa = foldl appE (conE $ tupleDataName n) fnames + + instanceD (cxt []) (appT (conT _tc) ty) -- where + [tySynInstD _rter [ty, vr] rty + ,funD _opr [clause [varP vf, rpa] (normalB $ frpa) [] ] + ,funD _oprs [clause [varP vf, rpa] (normalB $ frpa) [] ] + ] + +mkTupleInstances a b c d = foreachTupleSize (mkTupleInstance a b c d) + +------------------------------------------------------------------------}}} +-- Make RTuple {{{ + +mkRTupleInstance :: Name -> Name -> Name -> Name -> Int -> Q Dec +mkRTupleInstance _tc _rte _rtr _opel n | n > 1 = do + names <- mkNames n + vr <- liftM varT $ newName "r" + vf <- newName "f" + let rty = mkRTy n vr names + + let fnames = map (appE (varE vf) . varE) names + let rpa = tupP $ map varP names + let lfrpa = listE fnames + instanceD (cxt []) (appT (conT _tc) rty) -- where + [tySynInstD _rtr [rty] vr + ,tySynInstD _rte [rty] $ mkTy n names + ,funD _opel [clause [varP vf, rpa] (normalB $ lfrpa) [] ] + ] + +mkRTupleInstances a b c d = foreachTupleSize (mkRTupleInstance a b c d) + +------------------------------------------------------------------------}}} +-- Make recursive type-math classes which walk tuple types {{{ + + -- XXX TUPLES Can't yet generate the closed lifted-ADTs we use + -- for class heads. + +mkRecClass :: (Name, [TypeQ]) -- ^ Class name and threaded arguments + -> (Int -> Name) -- ^ Class argument maker + -> [(Name,Int -> Name)] -- ^ Datas and constructor-maker + -> [Name] -- ^ Types + -> [Name] -- ^ Types with constructor argument + -> Int -- ^ Tuple size + -> Q Dec +mkRecClass (_cname,_cargs) _ntyf _dnames _tnames _trnames n = do + names <- mkNames n + let _tyf = _ntyf n + let context = cxt $ map (\na -> classP _cname $ _cargs ++ [varT na]) names + let conarg = (appT (conT _tyf) $ mkPTy n names) + + let datas :: [DecQ] + datas = map (\(tc,ndc) -> dataInstD (cxt []) tc [conarg] + [normalC (ndc n) $ map (strictType (return NotStrict) + . appT (conT tc) . varT) + names] + []) + $ _dnames + + let types = map (\tc -> tySynInstD tc [conarg] + $ genMap appT (conT $ tupleTypeName n) + (appT (conT tc) . varT) + names) + _tnames + + vr <- liftM varT $ newName "r" + let rtypes = map (\tc -> tySynInstD tc ([conarg] ++ [vr]) + $ genMap appT (conT $ tupleTypeName n) + (\na -> appT (appT (conT tc) (varT na)) vr) + names) + _trnames + + instanceD context + (genMap appT (conT _cname) (id) $ _cargs ++ [conarg]) + $ concat [datas,types,rtypes] + +------------------------------------------------------------------------}}} +-- Experimental detritus (XXX) {{{ + +{- +mkNpleFunction :: String -> TypeQ -> Int -> TypeQ +mkNpleFunction _pfx rt n = do + names <- mkNames n + let ty = mkTy n names + let rty = mkRty n names rt + +-} + +------------------------------------------------------------------------}}} + -- 2.50.1