{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Versioning.Base (
V (..)
, VPred
, VSucc
, VNat
, VCmp
, Since
, SinceS
, Until
, UntilS
, NA
, na
, V0
, V1
, V2
, V3
, V4
, V5
, V6
, V7
, V8
, V9
, V10
, V11
, V12
, V13
, V14
, V15
, V16
, V17
, V18
, V19
, V20
, versionNumber
) where
import Data.Proxy (Proxy (..))
import GHC.TypeNats (type (+), KnownNat, Nat, natVal)
import Numeric.Natural (Natural)
import Versioning.Internal.Base (Bare)
data V = VZero | VSucc V deriving (V -> V -> Bool
(V -> V -> Bool) -> (V -> V -> Bool) -> Eq V
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: V -> V -> Bool
$c/= :: V -> V -> Bool
== :: V -> V -> Bool
$c== :: V -> V -> Bool
Eq, Int -> V -> ShowS
[V] -> ShowS
V -> String
(Int -> V -> ShowS) -> (V -> String) -> ([V] -> ShowS) -> Show V
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [V] -> ShowS
$cshowList :: [V] -> ShowS
show :: V -> String
$cshow :: V -> String
showsPrec :: Int -> V -> ShowS
$cshowsPrec :: Int -> V -> ShowS
Show)
type family VPred (v :: V) :: V where
VPred ('VSucc v) = v
VPred 'VZero = 'VZero
type VSucc = 'VSucc
type family VNat (v :: V) :: Nat where
VNat v = VNat' v 0
type family VNat' (v :: V) (n :: Nat) :: Nat where
VNat' 'VZero n = n
VNat' ('VSucc v) n = VNat' v (n + 1)
type family VCmp (v :: V) (w :: V) :: Ordering where
VCmp 'VZero 'VZero = 'EQ
VCmp 'VZero v = 'LT
VCmp v 'VZero = 'GT
VCmp ('VSucc v) ('VSucc w) = VCmp v w
versionNumber :: forall a v. KnownNat (VNat v) => a v -> Natural
versionNumber :: a v -> Natural
versionNumber a v
_ = Proxy (VNat' v 0) -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy (VNat v)
forall k (t :: k). Proxy t
Proxy :: Proxy (VNat v))
type family Since (s :: V) (v :: V) a where
Since s v a = Since' (VCmp s v) a NA
type family SinceS (s :: V) (v :: V) a where
SinceS s v a = Since' (VCmp s v) a Bare
type family Since' (o :: Ordering) a absent :: * where
Since' 'LT a _ = a
Since' 'EQ a _ = a
Since' 'GT a absent = absent
type family Until (u :: V) (v :: V) a where
Until u v a = Until' (VCmp u v) a NA
type family UntilS (u :: V) (v :: V) a where
UntilS u v a = Until' (VCmp u v) a Bare
type family Until' (o :: Ordering) a absent :: * where
Until' 'GT a _ = a
Until' 'EQ a _ = a
Until' 'LT a absent = absent
type NA = Maybe Bare
na :: NA
na :: NA
na = NA
forall a. Maybe a
Nothing
type V0 = 'VZero
type V1 = 'VSucc V0
type V2 = 'VSucc V1
type V3 = 'VSucc V2
type V4 = 'VSucc V3
type V5 = 'VSucc V4
type V6 = 'VSucc V5
type V7 = 'VSucc V6
type V8 = 'VSucc V7
type V9 = 'VSucc V8
type V10 = 'VSucc V9
type V11 = 'VSucc V10
type V12 = 'VSucc V11
type V13 = 'VSucc V12
type V14 = 'VSucc V13
type V15 = 'VSucc V14
type V16 = 'VSucc V15
type V17 = 'VSucc V16
type V18 = 'VSucc V17
type V19 = 'VSucc V18
type V20 = 'VSucc V19