{-# OPTIONS -fglasgow-exts #-}

module Examples where

import Lift

examples   = 
    -- data Even = Zero | Double NonZero
    Kinded "Even" Star $
    Typed "Zero" (RestrictedConstructorType [] [] "Even" []) $
    Typed "Double" (RestrictedConstructorType [] [Name (Data "NonZero")] "Even" []) $
    -- data Odd = OneMore Even
    Kinded "Odd" Star $
    Typed "OneMore" (RestrictedConstructorType [] [Name (Data "Even")] "Odd" []) $
    -- data NonZero = NonZeroOdd Odd | DoubleNonZero Odd
    Kinded "NonZero" Star $
    Typed "NonZeroOdd" (RestrictedConstructorType [] [Name (Data "Odd")] "NonZero" []) $
    Typed "DoubleNonZero" (RestrictedConstructorType [] [Name (Data "Odd")] "NonZero" []) $
    -- data BinaryNumber = OddBinary Odd | EvenBinary Even
    Kinded "BinaryNumber" Star $
    Typed "OddBinary" (RestrictedConstructorType [] [Name (Data "Odd")] "BinaryNumber" []) $
    Typed "EvenBinary" (RestrictedConstructorType [] [Name (Data "Even")] "BinaryNumber" []) $
    {- 
       data LooksBad ab where
           LooksBadCons :: a -> LooksBad (a -> b)
     -}
    Kinded "LooksBad" (Star `KindArrow` Star) $
    Typed "LooksBadCons" (RestrictedConstructorType [(Variable "a", Star), (Variable "b", Star)]
                          [Var (Variable "a")]
                          "LooksBad"
                          [(Var (Variable "a")) `TypeArrow` (Var (Variable "b"))]) $
    {-
      data Good a where
          GoodCons :: Ok (One a) -> Good a
     -}
    Kinded "Good" (Star `KindArrow` Star) $
    Typed "GoodCons" (RestrictedConstructorType [(Variable "a", Star)]
                      [(Name (Data "Ok")) `TypeApply` ((Name (Data "One")) `TypeApply` (Var (Variable "a")))]
                      "Good"
                      [Var (Variable "a")]) $
    -- data One
    Kinded "One" (Star `KindArrow` Star) $
    {- 
       data Ok a where
           BadCons :: (a -> a) -> Ok (Two a)
     -}
    Kinded "Ok" (Star `KindArrow` Star) $
    Typed "BadCons" (RestrictedConstructorType [(Variable "a", Star)] 
                     [(Var (Variable "a")) `TypeArrow` (Var (Variable "a"))] 
                     "Ok" 
                     [(Name (Data "Two")) `TypeApply` (Var (Variable "a"))]) $
    -- data Two
    Kinded "Two" (Star `KindArrow` Star) $
    {- 
       data Useless a where
           UselessCons :: (forall f . f (f a)) -> Useless a
     -}
    Kinded "Useless" (Star `KindArrow` Star) $
    Typed "UselessCons" (RestrictedConstructorType 
                         [(Variable "a", Star)] 
                         [Forall (Variable "f") (Star `KindArrow` Star) 
                          ((Var (Variable "f")) `TypeApply` ((Var (Variable "f")) `TypeApply` (Var (Variable "a"))))] 
                         "Useless" [Var (Variable "a")]) $
    -- data Ping a = PingCons (Pong a)
    Kinded "Ping" (Star `KindArrow` Star) $
    Typed "PingCons" (RestrictedConstructorType 
                      [(Variable "a", Star)]
                      [Name (Data "Pong") `TypeApply` Var (Variable "a")]
                      "Ping"
                      [Var (Variable "a")]) $
    -- data Pong a = PongCons (Ping a)
    Kinded "Pong" (Star `KindArrow` Star) $
    Typed "PongCons" (RestrictedConstructorType 
                      [(Variable "a", Star)]
                      [Name (Data "Ping") `TypeApply` Var (Variable "a")]
                      "Pong"
                      [Var (Variable "a")]) $
    Empty