Constraints(but mostly vectors)

Constraint.hs

{-# LANGUAGE DataKinds, GADTs, StandaloneDeriving, FlexibleInstances, FlexibleContexts #-}

import Data.Foldable hiding (foldl)
import Data.Traversable
import Data.Monoid
import Control.Applicative

-- vector stuff --
data Nat = Z | S Nat

infixr :|
data Vec n a where
  Nil :: Vec Z a
  (:|) :: a -> Vec n a -> Vec (S n) a

instance Show (Vec Z a) where
  show Nil = "Nil"
  
instance (Show a, Show (Vec n a)) => Show (Vec (S n) a) where
  show (a :| v) = show a ++ " :| " ++ show v
  
instance Functor (Vec n) where
  fmap f Nil = Nil
  fmap f (a :| v) = f a :| fmap f v
  
instance Foldable (Vec n) where
  fold Nil = mempty
  fold (a :| v) = a `mappend` fold v
  
instance Traversable (Vec n) where
  sequenceA Nil = pure Nil
  sequenceA (fa :| v) = (:|) <$> fa <*> sequenceA v
  
-- solving stuff --
solve :: Vec n Integer -> [(Vec n Integer -> Bool)] -> [Vec n Integer]
solve bounds preds = foldl (flip filter) universe preds
  where universe = enumerate bounds

enumerate :: Vec n Integer -> [Vec n Integer]
enumerate v = traverse (\n -> [1..n]) v


--example--

pairify :: Vec (S(S(Z))) a -> (a, a)
pairify (a :| b :| Nil) = (a, b)

diff (a, b) = a /= b

domain = (2 :| 2 :| Nil)

test1 = solve domain [(diff . pairify), ((==2) . fst . pairify)] -- [2 :| 1 :| Nil]
test2 = solve domain [(diff . pairify)]                          -- [1 :| 2 :| Nil, 2 :| 1 :| Nil]
test3 = solve domain [(==2) . fst . pairify]                     -- [2 :| 1 :| Nil , 2 :| 2 :| Nil]