diff options
| author | bringert <bringert@cs.chalmers.se> | 2005-11-30 18:42:45 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2005-11-30 18:42:45 +0000 |
| commit | 12ca29b32b50fd924c5f69a30d204e4332dff4f9 (patch) | |
| tree | 0515af794def1a1737e1edf9fffad5becc5d73e7 /transfer/examples/numerals.tr | |
| parent | 01d1715994d2e7c58ef97fdd81dd7015a9118b17 (diff) | |
Transfer: derive instances, not functions.
Diffstat (limited to 'transfer/examples/numerals.tr')
| -rw-r--r-- | transfer/examples/numerals.tr | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/transfer/examples/numerals.tr b/transfer/examples/numerals.tr index 2b6628100..1a6e8d064 100644 --- a/transfer/examples/numerals.tr +++ b/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 + |