Support the simplest kind of recursive data type
authorJoachim Breitner <mail@joachim-breitner.de>
Thu, 11 Jul 2013 12:31:11 +0000 (14:31 +0200)
committerJoachim Breitner <mail@joachim-breitner.de>
Thu, 11 Jul 2013 12:31:11 +0000 (14:31 +0200)
GHC/NT/Plugin.hs
test.hs

index 3637c4a..b58ca9f 100644 (file)
@@ -194,8 +194,9 @@ checkInScope env n = case lookupGRE_Name env n of
 deriveNT :: GlobalRdrEnv -> TyCon -> [Coercion] -> [TyCon] -> Type -> Type -> CoreM Coercion
 deriveNT env nttc cos seen t1 t2
     | t1 `eqType` t2 = do
-        putMsg $ text "done, types are equal" <+> ppr t1
         return $ Refl t1
+    | Just usable <- findCoercion t1 t2 cos = do
+        return usable
     | Just (tc1,tyArgs1) <- splitTyConApp_maybe t1,
       Just (tc2,tyArgs2) <- splitTyConApp_maybe t2,
       tc1 == tc2,
@@ -204,18 +205,18 @@ deriveNT env nttc cos seen t1 t2
     | Just (tc1,tyArgs1) <- splitTyConApp_maybe t1,
       Just (tc2,tyArgs2) <- splitTyConApp_maybe t2,
       tc1 == tc2 = do
-        putMsg $ text "checking tc" <+> ppr tc1 <+> text "params" <+> ppr (tyArgs1, tyArgs2)
         -- First we check if the data constructors are in scope
         checkDataConsInScope env tc1
-        -- And then that we have witnesses for the equality of all their parameters
-        -- TODO: Prevent looping!
+        -- Then we generate the witness for this type
+        c <- TyConAppCo tc1 <$>
+            sequence (zipWith (deriveNT env nttc cos seen) tyArgs1 tyArgs2)
+        -- And finally see if the coercion of the arguments is justified. We
+        -- inclue the generated witness in the list of known coercions, to
+        -- support simple recursive types.
         forM_ (tyConDataCons tc1) $ \dc -> do
-            putMsg $ text "checking" <+> ppr dc <+> text "using" <+> ppr (map coercionKind cos)
             forM_ (zip (dataConInstArgTys dc tyArgs1) (dataConInstArgTys dc tyArgs2)) $ \(t1,t2) -> do
-                putMsg $ text "comparing" <+> ppr t1 <+> ppr t2
-                deriveNT env nttc cos (tc1:seen) t1 t2
-        TyConAppCo tc1 <$>
-            sequence (zipWith (deriveNT env nttc cos seen) tyArgs1 tyArgs2)
+                deriveNT env nttc (c:cos) (tc1:seen) t1 t2
+        return c
     | Just (tc,tyArgs) <- splitTyConApp_maybe t1 = do
         case unwrapNewTyCon_maybe tc of
             Just (tyVars, tyExpanded, coAxiom) -> do
@@ -226,9 +227,6 @@ deriveNT env nttc cos seen t1 t2
                   then return $ mkAxInstCo coAxiom tyArgs
                   else err_wrong_newtype rhs
             Nothing -> err_not_newtype
-    | Just usable <- findCoercion t1 t2 cos = do
-        putMsg $ text "done, found" <+> ppr (coercionKind usable)
-        return usable
     | otherwise = err_no_idea_what_to_do
   where
     err_wrong_newtype rhs =
diff --git a/test.hs b/test.hs
index b16b5b0..e5066fc 100644 (file)
--- a/test.hs
+++ b/test.hs
@@ -9,6 +9,9 @@ listNT = deriveThisNT
 tupleNT :: NT a b -> NT (a,c) (b,c)
 tupleNT = deriveThisNT
 
+nestedNT :: NT a a' -> NT ((a,b),c) ((a',b),c)
+nestedNT = deriveThisNT
+
 newtype Age = Age Int deriving Show
 
 ageNT :: NT Age Int
@@ -50,11 +53,21 @@ fNT = deriveThisNT
 
 
 badNT :: NT a b -> NT (Abs1 a) (Abs1 b)
-badNT = deriveThisNT
+badNT = deriveThisNT -- rejected 
 
-data WrappedBad a = WrappedBad (Abs1 a)
+data WrappedBad a = WrappedBad (Abs1 a) deriving Show
 wrappedBadNT :: NT a b -> NT (WrappedBad a) (WrappedBad b)
-wrappedBadNT = deriveThisNT
+wrappedBadNT = deriveThisNT -- rejected
+
+data WrappedAbstract a = WrappedAbstract (Abs2 a) deriving Show
+wrappedAbstactBadNT :: NT a b -> NT (WrappedAbstract a) (WrappedAbstract b)
+wrappedAbstactBadNT = deriveThisNT -- rejected
+
+wrappedAbstactNTRaw :: NT a b -> NT (Abs2 a) (Abs2 b) -> NT (WrappedAbstract a) (WrappedAbstract b)
+wrappedAbstactNTRaw = deriveThisNT -- accepted
+
+wrappedAbstactNT :: NT a b -> NT (WrappedAbstract a) (WrappedAbstract b)
+wrappedAbstactNT nt = wrappedAbstactNTRaw nt (abs2NT nt)
 
 main = do
     let n = 1 :: Int
@@ -71,8 +84,14 @@ main = do
     print $ coerce (fNT (sym ageNT)) (F 1 2 3)
     tree'NT `seq` tree'NT' `seq` tupleNT `seq` return ()
     -- badNT `seq` return ()
-    wrappedBadNT `seq` return ()
-    --let t1 = T 1 []
-    --print $ coerce (trans (sym tree'NT) (sym (tree'NT' ageNT))) t1
-    --print $ coerce (trans (treeNT (sym ageNT)) (sym tree'NT)) t1
+    -- wrappedBadNT `seq` return ()
+    -- wrappedAbstactBadNT `seq` return ()
+    wrappedAbstactNT `seq` return ()
+    let wa = WrappedAbstract abs2
+    print wa
+    print $ coerce (sym (wrappedAbstactNT ageNT)) wa
+    let t1 = T 1 []
+    print $ coerce (trans (sym tree'NT) (sym (tree'NT' ageNT))) t1
+    print $ coerce (trans (treeNT (sym ageNT)) (sym tree'NT)) t1
+    -- nestedNT `seq` return ()