{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Rank1 where

import Numeric.Natural
import Numeric.Natural.QuickCheck ()
import Data.Typeable

import Data.Name
import Data.Prop

data Rank1 p a = Forall [a] (p a) deriving (Eq, Ord, Show, Read, Functor)
instance Typeable1 p => Typeable1 (Rank1 p) where
    typeOf1 _ = mkTyConApp (mkTyCon3 "" "Data.Rank1" "Rank1") [typeOf1 (undefined :: p ())]

type Rank1PropS = Rank1 Prop Name
type Rank1PropI = Rank1 Prop Natural

alphaReduce :: (Eq a, Eq (p a), Functor p) => a -> a -> Rank1 p a -> Rank1 p a
alphaReduce a b = fmap (\ x -> if x == a then b else x)

readRank1PropS :: String -> Rank1PropS
readRank1PropS = read
readRank1PropI :: String -> Rank1PropI
readRank1PropI = read

cutDangling :: Eq a => Rank1 Prop a -> Rank1 Prop a
cutDangling (Forall xs p) = Forall (filter (`elem` atoms p) xs) p
