Transfer: fixed Eq derivation to at least work for GF-generated Tree types.

src/Transfer/SyntaxToCore.hs

@@ -92,13 +92,10 @@ mergeDecls ds@(ValueDecl x p _ _:_)
          when (not (all ((== n) . length) pss))
               $ fail $ "Pattern count mismatch for " ++ printTree x
          vs <- freshIdents n
-         let cases = map (\ (ps,g,rhs) -> Case (mkPRec ps) g rhs) cs
+         let cases = map (\ (ps,g,rhs) -> Case (mkPTuple ps) g rhs) cs
-             c = ECase (mkERec (map EVar vs)) cases
+             c = ECase (mkETuple (map EVar vs)) cases
              f = foldr (EAbs . VVar) c vs
          return $ ValueDecl x [] GuardNo f
-  where mkRec r f = r . zipWith (\i e -> f (Ident ("p"++show i)) e) [0..]
-        mkPRec = mkRec PRec FieldPattern
-        mkERec = mkRec ERec FieldValue
 
 --
 -- * Derived function definitions
@@ -136,7 +133,7 @@ deriveCompos t@(Ident ts) k cs =
     cf <- deriveComposFold t k cs
     let [c] = argumentTypes k -- FIXME: what if there is not exactly one argument to t?
         d = Ident ("compos_"++ts)
-        dt = apply (EVar (Ident "Compos")) [c, EVar t]
+        dt = apply (var "Compos") [c, EVar t]
         r = ERec [FieldValue (Ident "composOp") co,
                   FieldValue (Ident "composFold") cf]
     return [TypeDecl d dt, ValueDecl d [] GuardNo r]
@@ -214,34 +211,39 @@ deriveShow t k cs = fail $ "derive Show not implemented"
 deriveEq :: Derivator
 deriveEq t@(Ident tn) k cs = 
     do
-    let ats = argumentTypes k
+    dt <- abstractType ats (EApp (var "Eq") . apply (EVar t))
-        d = Ident ("eq_"++tn)
+    f <- mkEq
-    dt <- abstractType ats (EApp (EVar (Ident "Eq")) . apply (EVar t))
+    r <- abstract (arity k) (\_ -> ERec [FieldValue (Ident "eq") f])
-    eq <- mkEq
-    r <- abstract (arity k) (\_ -> ERec [FieldValue (Ident "eq") eq])
     return [TypeDecl d dt, ValueDecl d [] GuardNo r]
   where
+  ats = argumentTypes k
+  d = Ident ("eq_"++tn)
   mkEq = do
          x <- freshIdent
+         y <- freshIdent
          cases <- mapM (uncurry mkEqCase) cs
-         return $ EAbs (VVar x) (ECase (EVar x) cases)
+         let fc = Case PWild gtrue false
+         abstract 2 (\es -> ECase (mkETuple es) (cases++[fc]))
   mkEqCase c ct = 
       do
       let n = arity ct
+          ts = argumentTypes ct
       vs1 <- freshIdents n
       vs2 <- freshIdents n
-      y <- freshIdent
+      let pr = mkPTuple [PCons c (map PVar vs1), PCons c (map PVar vs2)]
-      let p1 = PCons c (map PVar vs1)
+          eqs = concat $ zipWith3 child_eq ts vs1 vs2
-          p2 = PCons c (map PVar vs2)
+          rhs [] = true
-          es1 = map EVar vs1
+          rhs xs = foldr1 EAnd xs
-          es2 = map EVar vs2
+      return $ Case pr gtrue (rhs eqs)
-          tc | n == 0 = true
+  -- FIXME: hack: this returns a list to skip testing type arguments.
-               -- FIXME: using EEq doesn't work right now
+  child_eq EType _ _ = []
-             | otherwise = foldr1 EAnd (zipWith EEq es1 es2)
+  child_eq t x y = [apply (var "eq") [t,eq_dict t, EVar x, EVar y]]
-          c1 = Case p2 gtrue tc
+  -- FIXME: this is a hack to at least support Tree types
-          c2 = Case PWild gtrue false
+  eq_dict (EApp (EVar t') _) 
-      return $ Case p1 gtrue (EAbs (VVar y) (ECase (EVar y) [c1,c2]))
+      | t' == t = apply (EVar d) (replicate (arity k) EMeta)
-               
+  eq_dict (EVar (Ident x)) 
+      | x `elem` ["String","Integer","Double"] = var ("eq_"++x)
+  eq_dict _ = EMeta
 
 --
 -- * Deriving instances of Ord
@@ -569,6 +571,13 @@ false = var "False"
 gtrue :: Guard
 gtrue = GuardExp true
 
+
+mkETuple :: [Exp] -> Exp
+mkETuple = ERec . zipWith (\i -> FieldValue (Ident ("p"++show i))) [0..]
+
+mkPTuple :: [Pattern] -> Pattern
+mkPTuple = PRec . zipWith (\i -> FieldPattern (Ident ("p"++show i))) [0..]
+
 -- | Apply an expression to a list of arguments.
 apply :: Exp -> [Exp] -> Exp
 apply = foldl EApp

transfer/examples/stoneage.tr

@@ -1,3 +1,5 @@
+import prelude
+
 data Cat : Type where {
   CN : Cat ;
   NP : Cat ;
@@ -205,3 +207,4 @@ data Tree : (_ : Cat)-> Type where {
 
 derive Compos Tree
 
+derive Eq Tree