{-# OPTIONS -Wall #-}
{-# OPTIONS -Wno-compat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoOverloadedLists #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Data.Ordering (
type (>)
, type (>=)
, type (==)
, type (/=)
, type (<=)
, type (<)
, type (>~)
, type (>=~)
, type (==~)
, type (/=~)
, type (<=~)
, type (<~)
, Gt
, Ge
, Same
, Le
, Lt
, Ne
, type (==!)
, OrdP
, OrdA'
, OrdA
, OrdI
, type (===~)
, Cmp
, CmpI
, Asc
, Asc'
, Desc
, Desc'
, AllPositive
, Positive
, AllNegative
, Negative
, Ands
, Ors
) where
import Predicate.Core
import Predicate.Util
import Predicate.Data.Tuple (Pairs)
import Data.Proxy
import Data.Char
import Data.Function
import Data.Foldable (toList)
import Data.List (findIndex)
type Gt n = I > n
type Ge n = I >= n
type Same n = I == n
type Le n = I <= n
type Lt n = I < n
type Ne n = I /= n
data p > q
infix 4 >
instance P (Cmp 'CGt p q) x => P (p > q) x where
type PP (p > q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CGt p q))
data p >= q
infix 4 >=
instance P (Cmp 'CGe p q) x => P (p >= q) x where
type PP (p >= q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CGe p q))
data p == q
infix 4 ==
instance P (Cmp 'CEq p q) x => P (p == q) x where
type PP (p == q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CEq p q))
data p <= q
infix 4 <=
instance P (Cmp 'CLe p q) x => P (p <= q) x where
type PP (p <= q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CLe p q))
data p < q
infix 4 <
instance P (Cmp 'CLt p q) x => P (p < q) x where
type PP (p < q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CLt p q))
data p /= q
infix 4 /=
instance P (Cmp 'CNe p q) x => P (p /= q) x where
type PP (p /= q) x = Bool
eval _ = evalBool (Proxy @(Cmp 'CNe p q))
data p >~ q
infix 4 >~
instance P (CmpI 'CGt p q) x => P (p >~ q) x where
type PP (p >~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CGt p q))
data p >=~ q
infix 4 >=~
instance P (CmpI 'CGe p q) x => P (p >=~ q) x where
type PP (p >=~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CGe p q))
data p ==~ q
infix 4 ==~
instance P (CmpI 'CEq p q) x => P (p ==~ q) x where
type PP (p ==~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CEq p q))
data p <=~ q
infix 4 <=~
instance P (CmpI 'CLe p q) x => P (p <=~ q) x where
type PP (p <=~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CLe p q))
data p <~ q
infix 4 <~
instance P (CmpI 'CLt p q) x => P (p <~ q) x where
type PP (p <~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CLt p q))
data p /=~ q
infix 4 /=~
instance P (CmpI 'CNe p q) x => P (p /=~ q) x where
type PP (p /=~ q) x = Bool
eval _ = evalBool (Proxy @(CmpI 'CNe p q))
data p ==! q
infix 4 ==!
type OrdP p q = p ==! q
instance (Ord (PP p a)
, PP p a ~ PP q a
, P p a
, Show (PP q a)
, P q a
) => P (p ==! q) a where
type PP (p ==! q) a = Ordering
eval _ opts a = do
let msg0 = "(==!)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = compare p q
in mkNode opts (PresentT d) (msg0 <> " " <> showL opts p <> " " <> prettyOrd d <> " " <> showL opts q) [hh pp, hh qq]
data OrdA p
instance P (OrdA' p p) x => P (OrdA p) x where
type PP (OrdA p) x = PP (OrdA' p p) x
eval _ = eval (Proxy @(OrdA' p p))
data OrdA' p q
type OrdAT' p q = (Fst Id >> p) ==! (Snd Id >> q)
instance P (OrdAT' p q) x => P (OrdA' p q) x where
type PP (OrdA' p q) x = PP (OrdAT' p q) x
eval _ = eval (Proxy @(OrdAT' p q))
type OrdI p q = p ===~ q
data p ===~ q
infix 4 ===~
instance (PP p a ~ String
, PP p a ~ PP q a
, P p a
, P q a
) => P (p ===~ q) a where
type PP (p ===~ q) a = Ordering
eval _ opts a = do
let msg0 = "(===~)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = on compare (map toLower) p q
in mkNode opts (PresentT d) (msg0 <> " " <> p <> " " <> prettyOrd d <> " " <> q) [hh pp, hh qq]
data Cmp (o :: OrderingP) p q
instance (GetOrd o
, Ord (PP p a)
, Show (PP p a)
, PP p a ~ PP q a
, P p a
, P q a
) => P (Cmp o p q) a where
type PP (Cmp o p q) a = Bool
eval _ opts a = do
let (sfn, fn) = getOrd @o
lr <- runPQ sfn (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = fn p q
in mkNodeB opts b (showL opts p <> " " <> sfn <> " " <> showL opts q) [hh pp, hh qq]
data CmpI (o :: OrderingP) p q
instance (PP p a ~ String
, GetOrd o
, PP p a ~ PP q a
, P p a
, P q a
) => P (CmpI o p q) a where
type PP (CmpI o p q) a = Bool
eval _ opts a = do
let (sfn, fn) = getOrd @o
lr <- runPQ sfn (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let b = on fn (map toLower) p q
in mkNodeB opts b (p <> " " <> sfn <> "~ " <> q) [hh pp, hh qq]
data Asc
type AscT = All (Fst Id <= Snd Id) Pairs
instance P AscT x => P Asc x where
type PP Asc x = PP AscT x
eval _ = evalBool (Proxy @AscT)
data Asc'
type AscT' = All (Fst Id < Snd Id) Pairs
instance P AscT' x => P Asc' x where
type PP Asc' x = PP AscT' x
eval _ = evalBool (Proxy @AscT')
data Desc
type DescT = All (Fst Id >= Snd Id) Pairs
instance P DescT x => P Desc x where
type PP Desc x = PP DescT x
eval _ = evalBool (Proxy @DescT)
data Desc'
type DescT' = All (Fst Id > Snd Id) Pairs
instance P DescT' x => P Desc' x where
type PP Desc' x = PP DescT' x
eval _ = evalBool (Proxy @DescT')
data AllPositive
type AllPositiveT = All Positive Id
instance P AllPositiveT x => P AllPositive x where
type PP AllPositive x = PP AllPositiveT x
eval _ = evalBool (Proxy @AllPositiveT)
data AllNegative
type AllNegativeT = All Negative Id
instance P AllNegativeT x => P AllNegative x where
type PP AllNegative x = PP AllNegativeT x
eval _ = evalBool (Proxy @AllNegativeT)
type Positive = Gt 0
type Negative = Lt 0
data Ands p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t
, a ~ Bool
) => P (Ands p) x where
type PP (Ands p) x = Bool
eval _ opts x = do
let msg0 = "Ands"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let msg1 = msg0 ++ "(" ++ show (length p) ++ ")"
w = case findIndex not (toList p) of
Nothing -> ""
Just i -> " i="++show i
in mkNodeB opts (and p) (msg1 <> w <> showVerbose opts " | " p) [hh pp]
data Ors p
instance (PP p x ~ t a
, P p x
, Show (t a)
, Foldable t
, a ~ Bool
) => P (Ors p) x where
type PP (Ors p) x = Bool
eval _ opts x = do
let msg0 = "Ors"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let msg1 = msg0 ++ "(" ++ show (length p) ++ ")"
w = case findIndex id (toList p) of
Nothing -> ""
Just i -> " i="++show i
in mkNodeB opts (or p) (msg1 <> w <> showVerbose opts " | " p) [hh pp]