From: Nathaniel Wesley Filardo Date: Thu, 18 Oct 2012 08:09:14 +0000 (-0400) Subject: BackendK3: Eliminate Slices as distinct objects from Patterns X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=8819e85449a86672ddaed5aa48e9412e2c66dcf9;p=dyna2 BackendK3: Eliminate Slices as distinct objects from Patterns --- diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs index 53cc1ed..872b0fb 100644 --- a/src/Dyna/BackendK3/AST.hs +++ b/src/Dyna/BackendK3/AST.hs @@ -171,7 +171,7 @@ instance K3Ty UnivTyRepr where -- | Kinds of patterns permitted in K3 data PKind where -- | Variables in patterns - PKVar :: k -> PKind + PKVar :: r -> k -> PKind -- | Wildcards in patterns PKUnk :: k -> PKind @@ -207,7 +207,7 @@ data PKind where -- eLam (PVar $ tPair tInt tInt) :: (r (Int, Int) -> _) -> _ -- eLam (PPair (PVar tInt) (PVar tInt)) :: ((r Int, r Int) -> _) -> _ -- -class (UnPatDa (PatDa w) ~ w) => Pat (w :: PKind) where +class (UnPatDa (PatDa w) ~ w) => Pat (r :: * -> *) (w :: PKind) where -- | Any data this witness needs to carry around type PatDa w :: * -- | The type this witness witnesses (i.e. the things matched against) @@ -215,33 +215,33 @@ class (UnPatDa (PatDa w) ~ w) => Pat (w :: PKind) where -- | The type this witness binds (i.e. after matching is done) type PatBTy w :: * -- | The type of this pattern. - type PatReprFn (r :: * -> *) w :: * + type PatReprFn (s :: * -> *) w :: * type family UnPatDa (pd :: *) :: PKind -data PVar a = PVar (UnivTyRepr a) -type instance UnPatDa (PVar a) = PKVar a -instance (K3BaseTy a) => Pat (PKVar (a :: *)) where - type PatDa (PKVar a) = PVar a - type PatTy (PKVar a) = a - type PatBTy (PKVar a) = a - type PatReprFn r (PKVar a) = r a +data 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 + type PatTy (PKVar r a) = a + type PatBTy (PKVar r a) = a + type PatReprFn s (PKVar r a) = s a data PUnk a = PUnk type instance UnPatDa (PUnk a) = PKUnk a -instance (K3BaseTy a) => Pat (PKUnk (a :: *)) where +instance (K3BaseTy a) => Pat r (PKUnk (a :: *)) where type PatDa (PKUnk a) = PUnk a type PatTy (PKUnk a) = a type PatBTy (PKUnk a) = () - type PatReprFn r (PKUnk a) = r () + type PatReprFn s (PKUnk a) = s () data PJust a = PJust { unPJust :: a } type instance UnPatDa (PJust a) = PKJust (UnPatDa a) -instance (Pat w) => Pat (PKJust w) where +instance (Pat r w) => Pat r (PKJust w) where type PatDa (PKJust w) = PJust (PatDa w) type PatTy (PKJust w) = Maybe (PatTy w) type PatBTy (PKJust w) = PatBTy w - type PatReprFn r (PKJust w) = PatReprFn r w + type PatReprFn s (PKJust w) = PatReprFn s w type family MapPatDa (x :: [PKind]) :: * $(mkTyMapFlat 0 ''MapPatDa ''PatDa) @@ -260,71 +260,16 @@ $(mkTyMapFlat 1 ''MapPatReprFn ''PatReprFn) $(mkTyUnMap (Just 'PKTup) 0 ''UnPatDa ''UnPatDa) -instance (UnPatDa (MapPatDa ts) ~ 'PKTup ts) - => Pat (PKTup (ts :: [PKind])) where +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 (MapPatDa ts) ~ 'PKTup ts, MapPatConst ts r) + => Pat r (PKTup (ts :: [PKind])) where type PatDa (PKTup ts) = MapPatDa ts type PatTy (PKTup ts) = MapPatTy ts type PatBTy (PKTup ts) = MapPatBTy ts - type PatReprFn r (PKTup ts) = MapPatReprFn r ts - -------------------------------------------------------------------------}}} -{- * Slice System -} -- {{{ - --- | Kinds of slices permitted in K3 -data SKind where - SKVar :: r -> k -> SKind - SKUnk :: k -> SKind - SKJust :: SKind -> SKind - - SKTup :: [SKind] -> SKind - --- | Witness of slice well-formedness -class (UnSliceDa (SliceDa w) ~ w) => Slice r (w :: SKind) where - type SliceDa w :: * - type SliceTy w :: * - -type family UnSliceDa (pd :: *) :: SKind - -data SVar r a = SVar (r a) -type instance UnSliceDa (SVar r a) = SKVar r a -instance (K3BaseTy a, r0 ~ r) => Slice r0 (SKVar (r :: * -> *) (a :: *)) where - type SliceDa (SKVar r a) = SVar r a - type SliceTy (SKVar r a) = a - -data SUnk a = SUnk -type instance UnSliceDa (SUnk a) = SKUnk a -instance (K3BaseTy a) => Slice r (SKUnk (a :: *)) where - type SliceDa (SKUnk a) = SUnk a - type SliceTy (SKUnk a) = a - -data SJust a = SJust { unSJust :: a } -type instance UnSliceDa (SJust a) = SKJust (UnSliceDa a) -instance (Slice r s) => Slice r (SKJust s) where - type SliceDa (SKJust s) = SJust (SliceDa s) - type SliceTy (SKJust s) = Maybe (SliceTy s) - -type family SliceConst (x :: SKind) (r :: * -> *) :: Constraint -type instance SliceConst x r = Slice r x - -type family MapSliceConst (x :: [SKind]) (r :: * -> *) :: Constraint -type instance MapSliceConst '[] r = () -type instance MapSliceConst (x ': xs) r = (SliceConst x r, MapSliceConst xs r) - -type family MapSliceDa (x :: [SKind]) :: * -$(mkTyMapFlat 0 ''MapSliceDa ''SliceDa) - -type family UnMapSliceDa (x :: *) :: [SKind] -$(mkTyUnMap Nothing 0 ''UnMapSliceDa ''UnSliceDa) - -type family MapSliceTy (x :: [SKind]) :: * -$(mkTyMapFlat 0 ''MapSliceTy ''SliceTy) - -$(mkTyUnMap (Just 'SKTup) 0 ''UnSliceDa ''UnSliceDa) - -instance (UnSliceDa (MapSliceDa ts) ~ 'SKTup ts, MapSliceConst ts r) - => Slice r (SKTup (ts :: [SKind])) where - type SliceDa (SKTup ts) = MapSliceDa ts - type SliceTy (SKTup ts) = MapSliceTy ts + type PatReprFn s (PKTup ts) = MapPatReprFn s ts ------------------------------------------------------------------------}}} {- * Numeric Autocasting -} -- {{{ @@ -385,7 +330,7 @@ class K3 (r :: * -> *) where type K3AST_Pat_C r (w :: PKind) :: Constraint -- | A representation-specific constraint for slices, on eSlice. - type K3AST_Slice_C r (w :: SKind) :: Constraint + type K3AST_Slice_C r (w :: PKind) :: Constraint -- | Add a comment to some part of the AST cComment :: String -> r a -> r a @@ -439,7 +384,7 @@ 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 :: (K3AST_Pat_C r w, Pat w, K3BaseTy (PatTy w)) + eLam :: (K3AST_Pat_C r w, Pat UnivTyRepr w, K3BaseTy (PatTy w)) => PatDa w -> (PatReprFn r w -> r b) -> r (PatTy w -> b) eApp :: r (a -> b) -> r a -> r b @@ -485,8 +430,8 @@ 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 r w, SliceTy w ~ t) - => SliceDa w -- ^ Slice specification + eSlice :: (K3AST_Slice_C r w, Pat r w, PatTy w ~ t) + => PatDa w -- ^ Slice specification -> r (CTE r c t) -- ^ Input collection -> r (CTE r c t) diff --git a/src/Dyna/BackendK3/Automation.hs b/src/Dyna/BackendK3/Automation.hs index 82c0764..28453e7 100644 --- a/src/Dyna/BackendK3/Automation.hs +++ b/src/Dyna/BackendK3/Automation.hs @@ -93,7 +93,7 @@ instance (K3AutoTyTup (wa ': w) (a,b), K3AutoTyTup w b) -- K3 Macro Library (XXX WIP) {{{ -- | Let as lambda -macro_localVar :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKVar a)) +macro_localVar :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKVar UnivTyRepr a)) => UnivTyRepr a -> (r a) -> (r a -> r b) @@ -101,7 +101,8 @@ macro_localVar :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKVar a)) macro_localVar w a b = eApp (eLam (PVar w) b) a -- | Case analyze a Maybe -macro_caseMaybe :: (K3 r, K3BaseTy a, K3AST_Pat_C r (PKJust (PKVar a))) +macro_caseMaybe :: (K3 r, K3BaseTy a, + K3AST_Pat_C r (PKJust (PKVar UnivTyRepr a))) => UnivTyRepr a -> r (Maybe a) -> r b @@ -112,7 +113,8 @@ macro_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 -macro_emptyPeek :: (K3AST_Coll_C r c, K3AST_Pat_C r (PKVar a), +macro_emptyPeek :: (K3AST_Coll_C r c, + K3AST_Pat_C r (PKVar UnivTyRepr a), K3 r, K3BaseTy a, K3AutoTy a) => r (CTE r c a) -> r b -> (r a -> r b) -> r b macro_emptyPeek c e l = eITE (eEq c eEmpty) diff --git a/src/Dyna/BackendK3/Render.hs b/src/Dyna/BackendK3/Render.hs index fbb19f7..440b8f1 100644 --- a/src/Dyna/BackendK3/Render.hs +++ b/src/Dyna/BackendK3/Render.hs @@ -10,6 +10,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} @@ -103,11 +104,11 @@ instance K3CFn CBag where ------------------------------------------------------------------------}}} -- Pattern handling {{{ -class (Pat w) => K3PFn w where +class (Pat UnivTyRepr w) => K3PFn w where k3pfn :: PatDa w -> State Int (Doc e, PatReprFn (AsK3 e) w) -instance (K3BaseTy a) => K3PFn (PKVar (a :: *)) where - k3pfn (PVar tr) = do +instance (K3BaseTy a) => K3PFn (PKVar UnivTyRepr (a :: *)) where + k3pfn (PVar (tr :: UnivTyRepr a)) = do n <- incState let sn = text $ "x" ++ show n return (sn <> colon <> unAsK3Ty (unUTR tr) @@ -124,17 +125,17 @@ instance (K3BaseTy a) => K3PFn (PKUnk (a :: *)) where ------------------------------------------------------------------------}}} -- Slice handling {{{ -class (Slice (AsK3 e) w) => K3SFn e w where - k3sfn :: SliceDa w -> Identity (AsK3 e (SliceTy w)) +class (Pat (AsK3 e) w) => K3SFn e w where + k3sfn :: PatDa w -> Identity (AsK3 e (PatTy w)) -instance (K3BaseTy a) => K3SFn e (SKVar (AsK3 e) (a :: *)) where - k3sfn (SVar r) = return r +instance (K3BaseTy a) => K3SFn e (PKVar (AsK3 e) (a :: *)) where + k3sfn (PVar r) = return r -instance (K3BaseTy a) => K3SFn e (SKUnk (a :: *)) where - k3sfn SUnk = return $ AsK3$ const$ text "_" +instance (K3BaseTy a) => K3SFn e (PKUnk (a :: *)) where + k3sfn PUnk = return $ AsK3$ const$ text "_" -instance (K3SFn e s) => K3SFn e (SKJust s) where - k3sfn (SJust s) = return $ AsK3$ \n -> "Just" +instance (K3SFn e s) => K3SFn e (PKJust s) where + k3sfn (PJust s) = return $ AsK3$ \n -> "Just" <> parens (unAsK3 (runIdentity $ k3sfn s) n) @@ -278,7 +279,7 @@ $(mkLRecInstances (''K3PFn,[]) 'PKTup $(do e <- liftM TH.varT $ TH.newName "e" n <- TH.newName "n" - mkLRecInstances (''K3SFn,[e]) 'SKTup + mkLRecInstances (''K3SFn,[e]) 'PKTup ('k3sfn,Nothing,\ls -> TH.appE (TH.conE 'AsK3) $ TH.lamE [TH.varP n]