content: {-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
  module TestShiftEmbed (test_shiftEmbed) where
  
  import Prelude hiding (pi)
  
  import Data.Typeable (Typeable)
  import GHC.Generics (Generic)
  import Unbound.Generics.LocallyNameless
  import qualified Unbound.Generics.PermM as PermM
  
  import AlphaAssertions
  
  import Test.Tasty
  import Test.Tasty.HUnit
  
  type Var = Name Term
  
  data Term
    = V Var
    | Pi (Bind (Var, Embed Term) Term)
    | LetRec (Bind (Rec Decl) Term)
      deriving (Show, Generic, Typeable)
  
  data Decl =
    -- a recursive declaration  x : A = m
    -- where x may occur in m but not in A
    Decl {
      declVar :: Var
      , declClass :: Shift (Embed Term)
      , declVal :: Embed Term
      }
    deriving (Show, Generic, Typeable)
  
  instance Alpha Term
  instance Alpha Decl
  
  x, y, z :: Var
  x = s2n "x"
  y = s2n "y"
  z = s2n "z"
  
  pi :: Var -> Term -> Term -> Term
  pi v a b = Pi $ bind (v, embed a) b
  
  letrec :: Decl -> Term -> Term
  letrec d e = LetRec $ bind (rec d) e
  
  decl :: Var -> Term -> Term -> Decl
  decl v klass e = Decl v (embed klass) (embed e)
  
  
  test_shiftEmbed =
    testGroup "Embedded and Shifted terms"
    [
      testGroup "Embed"
      [
        testCase "(pi x:x . x) = (pi y:x . y)" $ let m1 = pi x (V x) (V x)
                                                     m2 = pi y (V x) (V y)
                                                 in assertAeq m1 m2
      , testCase "(letrec x : x = x in x) = (letrec y : x = y in y)"
        $ let m1 = letrec (decl x (V x) (V x)) (V x)
              m2 = letrec (decl y (V x) (V y)) (V y)
          in assertAeq m1 m2
      , testCase "pi x : z . (letrec x : x = x in x) = pi y : z . (letrec x : y = x in x)"
        $ let m1 = pi x (V z) $ letrec (decl x (V x) (V x)) (V x)
              m2 = pi y (V z) $ letrec (decl x (V y) (V x)) (V x)
          in assertAeq m1 m2
      ]
    ]
  