Variables_Test.hs

{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, 
  TypeOperators, FlexibleContexts, ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}

module Data.Comp.Variables_Test where


import Data.Comp.Variables
import Data.Comp.Derive
import Data.Comp.Sum
import Data.Comp.Term
import Data.Comp.Show ()

import qualified Data.Map as Map
import qualified Data.Set as Set

import Test.Framework
import Test.Framework.Providers.HUnit
import Test.HUnit



--------------------------------------------------------------------------------
-- Definitions
--------------------------------------------------------------------------------

data Var = X | Y | Z deriving (Eq,Ord,Show)


data Val e = Abs Var e
           | Var Var
           | Int Int
  deriving Functor

data Op e = App e e
          | Plus e e
  deriving Functor

data Let e = Let Var e e
  deriving Functor

data LetRec e = LetRec Var e e
  deriving Functor

type Sig = Op :+: Val

type SigLet = Let :+: Sig

type SigRec = LetRec :+: Sig

$(derive [makeTraversable, makeFoldable,
          makeEqF, makeShowF, smartConstructors]
         [''Op, ''Val, ''Let, ''LetRec])

instance HasVars Val Var where
    isVar (Var v) = Just v
    isVar _       = Nothing
    
    bindsVars (Abs v a) =  a |-> Set.singleton v
    bindsVars _         = empty

instance HasVars Op a where

instance HasVars Let Var where
    bindsVars (Let v _ a) = a |-> Set.singleton v

instance HasVars LetRec Var where
    bindsVars (LetRec v a b) = a |-> vs & b |-> vs
        where vs = Set.singleton v

-- let x = x + 1 in (\y. y + x) z
letExp, letExp' :: Term SigLet
letExp = iLet X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
letExp' = iLet X (iInt 1 `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)

-- letrec x = x + 1 in (\y. y + x) z
recExp, recExp' :: Term SigRec
recExp = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iVar Z)
recExp' = iLetRec X (iVar X `iPlus` iInt 1) (iAbs Y (iVar Y `iPlus` iVar X) `iApp` iInt 3)

subst :: (Val :<: f) => Subst f Var
subst = Map.fromList [(X, iInt 1), (Y, iInt 2), (Z, iInt 3)]

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

case_letFree = Set.fromList [Z,X] @=? variables letExp

case_recFree = Set.fromList [Z] @=? variables recExp

case_letSubst = letExp' @=? appSubst s letExp
    where s = subst :: Subst SigLet Var

case_recSubst = recExp' @=? appSubst s recExp
    where s = subst :: Subst SigRec Var

--------------------------------------------------------------------------------
-- Test Suits
--------------------------------------------------------------------------------

main = defaultMain [tests]

tests = testGroup "Variables" [
         testCase "case_letFree" case_letFree
        ,testCase "case_recFree" case_recFree
        ,testCase "case_letSubst" case_letSubst
        ,testCase "case_recSubst" case_recSubst
        ]