Safe Haskell | None |
---|---|
Language | Haskell2010 |
Usage example with template haskell support.
- data Rose a
- value1 :: Rose Int
- value2 :: Rose Int
- value3 :: Rose Int
- value4 :: Rose Int
- type FamRoseInt = '[Rose Int, [Rose Int]]
- type CodesRoseInt = '['['[K KInt, I (S Z)], '[K KInt]], '['[], '[I Z, I (S Z)]]]
- pattern ListRoseInt_Ifx1 :: phi Z -> phi (S Z) -> View kon phi (Lkup (S Z) CodesRoseInt)
- pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt)
- pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt)
- pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt)
- pattern IdxListRoseInt :: forall (a :: Nat). () => forall (n :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n Z) => SNat a
- pattern IdxRoseInt :: forall (a :: Nat). () => (~#) Nat Nat a Z => SNat a
- tyInfo_1 :: [Char]
- tyInfo_0 :: [Char]
- testEq :: Bool
- normalize :: Rose Int -> Rose Int
- sumTree :: Rose Int -> Int
- testSum :: Bool
Defining the datatype
First, we will start off defining a variant of your standard Rose trees.
The Leaf
constructor adds some redundancy on purpose, so we can
later use the combinators in the library to remove that redundancy.
Rose trees with redundancy.
pattern ListRoseInt_Ifx0 :: View kon phi (Lkup (S Z) CodesRoseInt) Source #
pattern RoseIntLeaf_ :: kon KInt -> View kon phi (Lkup Z CodesRoseInt) Source #
pattern RoseInt_Ifx0 :: kon KInt -> phi (S Z) -> View kon phi (Lkup Z CodesRoseInt) Source #
pattern IdxListRoseInt :: forall (a :: Nat). () => forall (n :: Nat). ((~#) Nat Nat a (S n), (~#) Nat Nat n Z) => SNat a Source #
Eq Instance
Compos test
Crush test
The sum of a tree should be the same as the sum of a normalized tree;
This should return True
.