{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.DecisionDiagram.BDD.Internal.ItemOrder
-- Copyright   :  (c) Masahiro Sakai 2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
----------------------------------------------------------------------
module Data.DecisionDiagram.BDD.Internal.ItemOrder
  (
  -- * Item ordering
    ItemOrder (..)
  , AscOrder
  , DescOrder
  , withDefaultOrder
  , withAscOrder
  , withDescOrder
  , withCustomOrder

  -- * Ordered item
  , OrderedItem (..)

  -- * Level
  , Level (..)
  ) where

import Data.Proxy
import Data.Reflection

-- ------------------------------------------------------------------------

class ItemOrder a where
  compareItem :: proxy a -> Int -> Int -> Ordering

data AscOrder

data DescOrder

instance ItemOrder AscOrder where
  compareItem :: proxy AscOrder -> Int -> Int -> Ordering
compareItem proxy AscOrder
_ = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

instance ItemOrder DescOrder where
  compareItem :: proxy DescOrder -> Int -> Int -> Ordering
compareItem proxy DescOrder
_ = (Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

data CustomOrder a

instance Reifies s (Int -> Int -> Ordering) => ItemOrder (CustomOrder s) where
  compareItem :: proxy (CustomOrder s) -> Int -> Int -> Ordering
compareItem proxy (CustomOrder s)
_ = Proxy s -> Int -> Int -> Ordering
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s)

withAscOrder :: forall r. (Proxy AscOrder -> r) -> r
withAscOrder :: (Proxy AscOrder -> r) -> r
withAscOrder Proxy AscOrder -> r
k = Proxy AscOrder -> r
k Proxy AscOrder
forall k (t :: k). Proxy t
Proxy

withDescOrder :: forall r. (Proxy DescOrder -> r) -> r
withDescOrder :: (Proxy DescOrder -> r) -> r
withDescOrder Proxy DescOrder -> r
k = Proxy DescOrder -> r
k Proxy DescOrder
forall k (t :: k). Proxy t
Proxy

-- | Currently the default order is 'AscOrder'
withDefaultOrder :: forall r. (forall a. ItemOrder a => Proxy a -> r) -> r
withDefaultOrder :: (forall a. ItemOrder a => Proxy a -> r) -> r
withDefaultOrder forall a. ItemOrder a => Proxy a -> r
k = Proxy AscOrder -> r
forall a. ItemOrder a => Proxy a -> r
k (Proxy AscOrder
forall k (t :: k). Proxy t
Proxy :: Proxy AscOrder)

withCustomOrder :: forall r. (Int -> Int -> Ordering) -> (forall a. ItemOrder a => Proxy a -> r) -> r
withCustomOrder :: (Int -> Int -> Ordering)
-> (forall a. ItemOrder a => Proxy a -> r) -> r
withCustomOrder Int -> Int -> Ordering
cmp forall a. ItemOrder a => Proxy a -> r
k = (Int -> Int -> Ordering)
-> (forall s. Reifies s (Int -> Int -> Ordering) => Proxy s -> r)
-> r
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Int -> Int -> Ordering
cmp (\(Proxy s
_ :: Proxy s) -> Proxy (CustomOrder s) -> r
forall a. ItemOrder a => Proxy a -> r
k (Proxy (CustomOrder s)
forall k (t :: k). Proxy t
Proxy :: Proxy (CustomOrder s)))

-- ------------------------------------------------------------------------

newtype OrderedItem a = OrderedItem Int
  deriving (OrderedItem a -> OrderedItem a -> Bool
(OrderedItem a -> OrderedItem a -> Bool)
-> (OrderedItem a -> OrderedItem a -> Bool) -> Eq (OrderedItem a)
forall a. OrderedItem a -> OrderedItem a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OrderedItem a -> OrderedItem a -> Bool
$c/= :: forall a. OrderedItem a -> OrderedItem a -> Bool
== :: OrderedItem a -> OrderedItem a -> Bool
$c== :: forall a. OrderedItem a -> OrderedItem a -> Bool
Eq, Int -> OrderedItem a -> ShowS
[OrderedItem a] -> ShowS
OrderedItem a -> String
(Int -> OrderedItem a -> ShowS)
-> (OrderedItem a -> String)
-> ([OrderedItem a] -> ShowS)
-> Show (OrderedItem a)
forall a. Int -> OrderedItem a -> ShowS
forall a. [OrderedItem a] -> ShowS
forall a. OrderedItem a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OrderedItem a] -> ShowS
$cshowList :: forall a. [OrderedItem a] -> ShowS
show :: OrderedItem a -> String
$cshow :: forall a. OrderedItem a -> String
showsPrec :: Int -> OrderedItem a -> ShowS
$cshowsPrec :: forall a. Int -> OrderedItem a -> ShowS
Show)

instance ItemOrder a => Ord (OrderedItem a) where
  compare :: OrderedItem a -> OrderedItem a -> Ordering
compare (OrderedItem Int
x) (OrderedItem Int
y) = Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
x Int
y

-- ------------------------------------------------------------------------

data Level a
  = NonTerminal !Int
  | Terminal
  deriving (Level a -> Level a -> Bool
(Level a -> Level a -> Bool)
-> (Level a -> Level a -> Bool) -> Eq (Level a)
forall a. Level a -> Level a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Level a -> Level a -> Bool
$c/= :: forall a. Level a -> Level a -> Bool
== :: Level a -> Level a -> Bool
$c== :: forall a. Level a -> Level a -> Bool
Eq, Int -> Level a -> ShowS
[Level a] -> ShowS
Level a -> String
(Int -> Level a -> ShowS)
-> (Level a -> String) -> ([Level a] -> ShowS) -> Show (Level a)
forall a. Int -> Level a -> ShowS
forall a. [Level a] -> ShowS
forall a. Level a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Level a] -> ShowS
$cshowList :: forall a. [Level a] -> ShowS
show :: Level a -> String
$cshow :: forall a. Level a -> String
showsPrec :: Int -> Level a -> ShowS
$cshowsPrec :: forall a. Int -> Level a -> ShowS
Show)

instance ItemOrder a => Ord (Level a) where
  compare :: Level a -> Level a -> Ordering
compare (NonTerminal Int
x) (NonTerminal Int
y) = Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
x Int
y
  compare (NonTerminal Int
_) Level a
Terminal = Ordering
LT
  compare Level a
Terminal (NonTerminal Int
_) = Ordering
GT
  compare Level a
Terminal Level a
Terminal = Ordering
EQ

-- ------------------------------------------------------------------------