BackendK3: Eliminate Slices as distinct objects from Patterns

diff --git a/src/Dyna/BackendK3/AST.hs b/src/Dyna/BackendK3/AST.hs
index 53cc1ed6911c36cb0bc2c733a146b13c5f8e970e..872b0fb304067c6fa7a6b936d091f7ae13e9890f 100644 (file)
--- 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 82c076490378b90f617a8fc9ae4337050b55fd9c..28453e700343d15ef9a4bbbbf171861b2faba674 100644 (file)
--- 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 fbb19f7ca78ed1752a754175a7d1def3c5e743ae..440b8f1a2247c839f3a9c431bdda240bd8e3bf6c 100644 (file)
--- 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]