2 files changed, 120 insertions, 0 deletions
diff --git a/html-test/src/BundledPatterns.hs b/html-test/src/BundledPatterns.hs
new file mode 100644
index 00000000..443e64fa
--- /dev/null
+++ b/html-test/src/BundledPatterns.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, PatternSynonyms, TypeOperators,
+             ViewPatterns #-}
+module BundledPatterns (Vec(Nil,(:>)), RTree (LR,BR)) where
+
+import GHC.TypeLits
+import Prelude hiding (head, tail)
+import Unsafe.Coerce
+
+-- | Fixed size vectors.
+--
+-- * Lists with their length encoded in their type
+-- * 'Vec'tor elements have an __ASCENDING__ subscript starting from 0 and
+--   ending at @'length' - 1@.
+data Vec :: Nat -> * -> * where
+  Nil  :: Vec 0 a
+  Cons :: a -> Vec n a -> Vec (n + 1) a
+
+infixr 5 `Cons`
+
+-- | Add an element to the head of a vector.
+--
+-- >>> 3:>4:>5:>Nil
+-- <3,4,5>
+-- >>> let x = 3:>4:>5:>Nil
+-- >>> :t x
+-- x :: Num a => Vec 3 a
+--
+-- Can be used as a pattern:
+--
+-- >>> let f (x :> y :> _) = x + y
+-- >>> :t f
+-- f :: Num a => Vec ((n + 1) + 1) a -> a
+-- >>> f (3:>4:>5:>6:>7:>Nil)
+-- 7
+--
+-- Also in conjunctions with (':<'):
+--
+-- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
+-- >>> :t g
+-- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
+-- >>> g (1:>2:>3:>4:>5:>Nil)
+-- 12
+pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
+pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
+  where
+    (:>) x xs = Cons x xs
+
+infixr 5 :>
+
+head :: Vec (n + 1) a -> a
+head (x `Cons` _) = x
+
+tail :: Vec (n + 1) a -> Vec n a
+tail (_ `Cons` xs) = unsafeCoerce xs
+
+-- | Perfect depth binary tree.
+--
+-- * Only has elements at the leaf of the tree
+-- * A tree of depth /d/ has /2^d/ elements.
+data RTree :: Nat -> * -> * where
+  LR_ :: a -> RTree 0 a
+  BR_ :: RTree d a -> RTree d a -> RTree (d+1) a
+
+textract :: RTree 0 a -> a
+textract (LR_ x) = x
+{-# NOINLINE textract #-}
+
+tsplit :: RTree (d+1) a -> (RTree d a,RTree d a)
+tsplit (BR_ l r) = (unsafeCoerce l, unsafeCoerce r)
+{-# NOINLINE tsplit #-}
+
+-- | Leaf of a perfect depth tree
+--
+-- >>> LR 1
+-- 1
+-- >>> let x = LR 1
+-- >>> :t x
+-- x :: Num a => RTree 0 a
+--
+-- Can be used as a pattern:
+--
+-- >>> let f (LR a) (LR b) = a + b
+-- >>> :t f
+-- f :: Num a => RTree 0 a -> RTree 0 a -> a
+-- >>> f (LR 1) (LR 2)
+-- 3
+pattern LR :: a -> RTree 0 a
+pattern LR x <- (textract -> x)
+  where
+    LR x = LR_ x
+
+-- | Branch of a perfect depth tree
+--
+-- >>> BR (LR 1) (LR 2)
+-- <1,2>
+-- >>> let x = BR (LR 1) (LR 2)
+-- >>> :t x
+-- x :: Num a => RTree 1 a
+--
+-- Case be used a pattern:
+--
+-- >>> let f (BR (LR a) (LR b)) = LR (a + b)
+-- >>> :t f
+-- f :: Num a => RTree 1 a -> RTree 0 a
+-- >>> f (BR (LR 1) (LR 2))
+-- 3
+pattern BR :: RTree d a -> RTree d a -> RTree (d+1) a
+pattern BR l r <- ((\t -> (tsplit t)) -> (l,r))
+  where
+    BR l r = BR_ l r
diff --git a/html-test/src/BundledPatterns2.hs b/html-test/src/BundledPatterns2.hs
new file mode 100644
index 00000000..5e9a83a7
--- /dev/null
+++ b/html-test/src/BundledPatterns2.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds, GADTs, KindSignatures, PatternSynonyms, TypeOperators,
+             ViewPatterns #-}
+module BundledPatterns2 (Vec((:>), Empty), RTree(..)) where
+
+import GHC.TypeLits
+
+import BundledPatterns
+
+pattern Empty :: Vec 0 a
+pattern Empty <- Nil