Transfer: derive instances, not functions.

src/Transfer/SyntaxToCore.hs

@@ -111,23 +111,31 @@ type Derivator = Ident -> Exp -> [(Ident,Exp)] -> C [Decl]
 
 derivators :: [(String, Derivator)]
 derivators = [
-              ("composOp", deriveComposOp),
-              ("composFold", deriveComposFold),
-              ("show", deriveShow),
-              ("eq", deriveEq),
-              ("ord", deriveOrd)
+              ("Compos", deriveCompos),
+              ("Show", deriveShow),
+              ("Eq", deriveEq),
+              ("Ord", deriveOrd)
              ]
 
-deriveComposOp :: Derivator
+deriveCompos :: Derivator
+deriveCompos t@(Ident ts) k cs = 
+    do
+    co <- deriveComposOp t 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]
+        r = ERec [FieldValue (Ident "composOp") co,
+                  FieldValue (Ident "composFold") cf]
+    return [TypeDecl d dt, ValueDecl d [] r]
+
+deriveComposOp :: Ident -> Exp -> [(Ident,Exp)] -> C Exp
 deriveComposOp t k cs = 
     do
     f <- freshIdent
     x <- freshIdent
-    let co = Ident ("composOp_" ++ printTree t)
-        e = EVar
+    let e = EVar
         pv = VVar
-        infixr 3 -->
-        (-->) = EPiNoVar
         infixr 3 \->
         (\->) = EAbs
         mkCase ci ct = 
@@ -141,28 +149,20 @@ deriveComposOp t k cs =
                                    _ -> e v
                 calls = zipWith rec vars (argumentTypes ct)
             return $ Case (PCons ci (map PVar vars)) (apply (e ci) calls)
-    ift <- abstractType (argumentTypes k) (\vs -> 
-             let tc = apply (EVar t) vs in tc --> tc)
-    ft <- abstractType (argumentTypes k) (\vs -> 
-             let tc = apply (EVar t) vs in ift --> tc --> tc)
     cases <- mapM (uncurry mkCase) cs
     let cases' = cases ++ [Case PWild (e x)]
     fb <- abstract (arity k) $ const $ pv f \-> pv x \-> ECase (e x) cases'
-    return $ [TypeDecl co ft,
-              ValueDecl co [] fb]
+    return fb
 
-deriveComposFold :: Derivator
+deriveComposFold :: Ident -> Exp -> [(Ident,Exp)] -> C Exp
 deriveComposFold t k cs = 
     do
     f <- freshIdent
     x <- freshIdent
     b <- freshIdent
     r <- freshIdent
-    let co = Ident ("composFold_" ++ printTree t)
-        e = EVar
+    let e = EVar
         pv = VVar
-        infixr 3 -->
-        (-->) = EPiNoVar
         infixr 3 \->
         (\->) = EAbs
         mkCase ci ct = 
@@ -175,29 +175,24 @@ deriveComposFold t k cs =
                                    EApp (EVar t') c | t' == t -> apply (e f) [c, e v]
                                    _ -> e v
                 calls = zipWith rec vars (argumentTypes ct)
-                z = EProj (e r) (Ident "zero")
-                p = EProj (e r) (Ident "plus")
+                z = EProj (e r) (Ident "mzero")
+                p = EProj (e r) (Ident "mplus")
                 joinCalls [] = z
                 joinCalls cs = foldr1 (\x y -> apply p [x,y]) cs
             return $ Case (PCons ci (map PVar vars)) (joinCalls calls)
-    let rt = ERecType [FieldType (Ident "zero") (e b), 
-                       FieldType (Ident "plus") (e b --> e b --> e b)]
-    ift <- abstractType (argumentTypes k) (\vs -> apply (EVar t) vs --> e b)
-    ft <- abstractType (argumentTypes k) (\vs -> ift --> apply (EVar t) vs --> e b)
     cases <- mapM (uncurry mkCase) cs
     let cases' = cases ++ [Case PWild (e x)]
     fb <- abstract (arity k) $ const $ pv f \-> pv x \-> ECase (e x) cases'
-    return $ [TypeDecl co $ EPi (VVar b) EType $ rt --> ft,
-              ValueDecl co [] $ VWild \-> pv r \-> fb]
+    return $ VWild \-> pv r \-> fb
 
 deriveShow :: Derivator
-deriveShow t k cs = fail $ "derive show not implemented"
+deriveShow t k cs = fail $ "derive Show not implemented"
 
 deriveEq :: Derivator
-deriveEq t k cs = fail $ "derive eq not implemented"
+deriveEq t k cs = fail $ "derive Eq not implemented"
 
 deriveOrd :: Derivator
-deriveOrd t k cs = fail $ "derive ord not implemented"
+deriveOrd t k cs = fail $ "derive Ord not implemented"
 
 --
 -- * Constructor patterns and applications.

transfer/examples/exp.tr

@@ -1,3 +1,5 @@
+import prelude
+
 data Cat : Type where
   Stm : Cat
   Exp : Cat
@@ -20,11 +22,12 @@ data Tree : Cat -> Type where
   NilStm  : Tree ListStm
   ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm
 
-derive composOp Tree
+derive Compos Tree
 
 rename : (String -> String) -> (C : Type) -> Tree C -> Tree C
 rename f C t = case t of
 		   V x -> V (f x)
-		   _ -> composOp_Tree C (rename f) t
+		   _ -> composOp ? ? compos_Tree C (rename f) t
 
 
+main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2)))

transfer/examples/numerals.tr

@@ -33,9 +33,15 @@ data Tree : (_ : Cat)-> Type where {
   pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000
 }
 
+derive Compos Tree
 
-num2int : (A : Cat) -> Tree A -> Integer
-num2int _ n = case n of
+monoid_plus_Int : Monoid Integer
+monoid_plus_Int = rec mzero = 0
+		      mplus = (\x -> \y -> x + y)
+
+
+num2int : (C : Cat) -> Tree C -> Integer
+num2int C n = case n of
 		n2 -> 2
 		n3 -> 3
 		n4 -> 4
@@ -44,14 +50,10 @@ num2int _ n = case n of
 		n7 -> 7
 		n8 -> 8
 		n9 -> 9
-		num x -> num2int ? x
-		pot0 x -> num2int ? x
 		pot01 -> 1
-		pot0as1 x -> num2int ? x
 		pot1 x -> 10 * num2int ? x
 		pot110 -> 10
 		pot111 -> 11
-		pot1as2 x -> num2int ? x
 		pot1plus x y -> 10 * num2int ? x + num2int ? y
 		pot1to19 x -> 10 + num2int ? x
 		pot2 x -> 100 * num2int ? x
@@ -59,3 +61,5 @@ num2int _ n = case n of
 		pot2plus x y -> 100 * num2int ? x + num2int ? y
 		pot3 x -> 1000 * num2int ? x
 		pot3plus x y -> 1000 * num2int ? x + num2int ? y
+                _ -> composFold ? ? compos_Tree ? monoid_plus_Int C num2int n
+

transfer/examples/stoneage.tr

@@ -203,5 +203,5 @@ data Tree : (_ : Cat)-> Type where {
   You_One : Tree NP
 }
 
-derive composOp Tree
-derive composFold Tree
+derive Compos Tree
+

transfer/examples/test.tr

@@ -1,3 +1 @@
-import nat
-
-main = natToInt (intToNat 100)
+main = ?

transfer/examples/widesnake.tr

@@ -9,11 +9,11 @@ monoid_Bool = rec
 isSnake : (A : Tree) -> Tree A -> Bool
 isSnake _ x = case x of
 		Snake -> True
-		_ -> composFold_Tree Bool monoid_Bool ? isSnake x
+		_ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x
 
 wideSnake : (A : Cat) -> Tree A -> Tree A
 wideSnake _ x = case x of
 		    Wide y -> let y' : CN = wideSnake ? y
                                in if isSnake CN y' then Thick y' else Wide y'
-		    _ -> composOp_Tree ? wideSnake x
+		    _ -> composOp ? ? compos_Tree ? wideSnake x