{-# 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.Enum (
type (...)
, EnumFromTo
, EnumFromThenTo
, FromEnum
, SuccB
, SuccB'
, PredB
, PredB'
, ToEnumBDef
, ToEnumBDef'
, ToEnumBFail
, Succ
, SuccN
, Pred
, ToEnum
, ToEnum'
) where
import Predicate.Core
import Predicate.Util
import Safe (succMay, predMay, toEnumMay)
import Data.Proxy
import qualified Control.Exception as E
import Data.Kind (Type)
instance (PP q x ~ a
, P q x
, P p (Proxy a)
, PP p (Proxy a) ~ a
, Show a
, Eq a
, Bounded a
, Enum a
) => P (SuccB p q) x where
type PP (SuccB p q) x = PP q x
eval _ opts x = do
let msg0 = "SuccB"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case succMay q of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @p) opts (Proxy @a)
pure $ case getValueLR opts msg1 pp [hh qq] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) msg1 [hh qq, hh pp]
Just n -> pure $ mkNode opts (PresentT n) (show01 opts msg0 n q) [hh qq]
data SuccB p q
data SuccB' q
type SuccBT' q = SuccB (Failp "Succ bounded") q
instance P (SuccBT' q) x => P (SuccB' q) x where
type PP (SuccB' q) x = PP (SuccBT' q) x
eval _ = eval (Proxy @(SuccBT' q))
data PredB' q
type PredBT' q = PredB (Failp "Pred bounded") q
instance (PP q x ~ a
, P q x
, P p (Proxy a)
, PP p (Proxy a) ~ a
, Show a
, Eq a
, Bounded a
, Enum a
) => P (PredB p q) x where
type PP (PredB p q) x = PP q x
eval _ opts x = do
let msg0 = "PredB"
qq <- eval (Proxy @q) opts x
case getValueLR opts msg0 qq [] of
Left e -> pure e
Right q ->
case predMay q of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @p) opts (Proxy @a)
pure $ case getValueLR opts msg1 pp [hh qq] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) msg1 [hh qq, hh pp]
Just n -> pure $ mkNode opts (PresentT n) (show01 opts msg0 n q) [hh qq]
data Succ p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (Succ p) x where
type PP (Succ p) x = PP p x
eval _ opts x = do
let msg0 = "Succ"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (succ p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) (showL opts p) [hh pp]
Right n -> mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
data SuccN n p
instance (Show a
, Enum a
, Integral (PP n x)
, P n x
, PP p x ~ a
, P p x
) => P (SuccN n p) x where
type PP (SuccN n p) x = PP p x
eval _ opts x = do
let msg0 = "SuccN"
lr <- runPQ msg0 (Proxy @n) (Proxy @p) opts x []
case lr of
Left e -> pure e
Right (n,p,nn,pp) -> do
lr1 <- catchit @_ @E.SomeException (toEnum (fromEnum p + fromIntegral n))
pure $ case lr1 of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) (litL opts (msg0 <> " " <> show (fromIntegral @_ @Integer n) <> " " <> show p)) [hh nn, hh pp]
Right r -> mkNode opts (PresentT r) (litL opts (msg0 <> " " <> show (fromIntegral @_ @Integer n) <> " " <> show p)) [hh nn, hh pp]
data Pred p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (Pred p) x where
type PP (Pred p) x = PP p x
eval _ opts x = do
let msg0 = "Pred"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (pred p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) (showL opts p) [hh pp]
Right n -> mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
data PredB p q
instance P (PredBT' q) x => P (PredB' q) x where
type PP (PredB' q) x = PP (PredBT' q) x
eval _ = eval (Proxy @(PredBT' q))
data FromEnum p
instance (Show a
, Enum a
, PP p x ~ a
, P p x
) => P (FromEnum p) x where
type PP (FromEnum p) x = Int
eval _ opts x = do
let msg0 = "FromEnum"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let n = fromEnum p
in mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
data ToEnum' t p
instance (PP p x ~ a
, P p x
, Show a
, Enum (PP t x)
, Show (PP t x)
, Integral a
) => P (ToEnum' t p) x where
type PP (ToEnum' t p) x = PP t x
eval _ opts x = do
let msg0 = "ToEnum"
pp <- eval (Proxy @p) opts x
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
lr <- catchit @_ @E.SomeException (toEnum $! fromIntegral p)
pure $ case lr of
Left e -> mkNode opts (FailT (msg0 <> " " <> e)) (showL opts p) [hh pp]
Right n -> mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
data ToEnum (t :: Type) p
type ToEnumT (t :: Type) p = ToEnum' (Hole t) p
instance P (ToEnumT t p) x => P (ToEnum t p) x where
type PP (ToEnum t p) x = PP (ToEnumT t p) x
eval _ = eval (Proxy @(ToEnumT t p))
data ToEnumBDef' t def
instance (P def (Proxy (PP t a))
, PP def (Proxy (PP t a)) ~ PP t a
, Show a
, Show (PP t a)
, Bounded (PP t a)
, Enum (PP t a)
, Integral a
) => P (ToEnumBDef' t def) a where
type PP (ToEnumBDef' t def) a = PP t a
eval _ opts a = do
let msg0 = "ToEnumBDef"
case toEnumMay $ fromIntegral a of
Nothing -> do
let msg1 = msg0 <> " out of range"
pp <- eval (Proxy @def) opts (Proxy @(PP t a))
pure $ case getValueLR opts msg1 pp [] of
Left e -> e
Right _ -> mkNode opts (_tBool pp) msg1 [hh pp]
Just n -> pure $ mkNode opts (PresentT n) (show01 opts msg0 n a) []
data ToEnumBDef (t :: Type) def
type ToEnumBDefT (t :: Type) def = ToEnumBDef' (Hole t) def
instance P (ToEnumBDefT t def) x => P (ToEnumBDef t def) x where
type PP (ToEnumBDef t def) x = PP (ToEnumBDefT t def) x
eval _ = eval (Proxy @(ToEnumBDefT t def))
data ToEnumBFail (t :: Type)
type ToEnumBFailT (t :: Type) = ToEnumBDef' (Hole t) (Failp "ToEnum bounded")
instance P (ToEnumBFailT t) x => P (ToEnumBFail t) x where
type PP (ToEnumBFail t) x = PP (ToEnumBFailT t) x
eval _ = eval (Proxy @(ToEnumBFailT t))
data EnumFromTo p q
data p ... q
infix 4 ...
type EnumFromToT p q = EnumFromTo p q
instance P (EnumFromToT p q) x => P (p ... q) x where
type PP (p ... q) x = PP (EnumFromToT p q) x
eval _ = eval (Proxy @(EnumFromToT p q))
instance (P p x
, P q x
, PP p x ~ a
, Show a
, PP q x ~ a
, Enum a
) => P (EnumFromTo p q) x where
type PP (EnumFromTo p q) x = [PP p x]
eval _ opts z = do
let msg0 = "..."
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) -> mkNode opts (PresentT (enumFromTo p q)) (showL opts p <> " " <> msg0 <> " " <> showL opts q) [hh pp, hh qq]
data EnumFromThenTo p q r
instance (P p x
, P q x
, P r x
, PP p x ~ a
, Show a
, PP q x ~ a
, PP r x ~ a
, Enum a
) => P (EnumFromThenTo p q r) x where
type PP (EnumFromThenTo p q r) x = [PP p x]
eval _ opts z = do
let msg0 = "EnumFromThenTo"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts z []
case lr of
Left e -> pure e
Right (p,q,pp,qq) -> do
rr <- eval (Proxy @r) opts z
pure $ case getValueLR opts (msg0 ++ " r failed") rr [hh pp, hh qq] of
Left e -> e
Right r ->
mkNode opts (PresentT (enumFromThenTo p q r)) (msg0 <> " [" <> showL opts p <> ", " <> showL opts q <> " .. " <> showL opts r <> "]") [hh pp, hh qq, hh rr]