{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-} {-# OPTIONS_GHC -Wall -fno-warn-tabs #-} module Data.TypeLevel.Maybe (M, pattern N, pattern J, Id(..)) where import Foreign.Storable import Data.TypeLevel.ParMaybe qualified as P newtype Id a = Id a deriving (Int -> Id a -> ShowS [Id a] -> ShowS Id a -> String (Int -> Id a -> ShowS) -> (Id a -> String) -> ([Id a] -> ShowS) -> Show (Id a) forall a. Show a => Int -> Id a -> ShowS forall a. Show a => [Id a] -> ShowS forall a. Show a => Id a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: forall a. Show a => Int -> Id a -> ShowS showsPrec :: Int -> Id a -> ShowS $cshow :: forall a. Show a => Id a -> String show :: Id a -> String $cshowList :: forall a. Show a => [Id a] -> ShowS showList :: [Id a] -> ShowS Show, Id a -> Id a -> Bool (Id a -> Id a -> Bool) -> (Id a -> Id a -> Bool) -> Eq (Id a) forall a. Eq a => Id a -> Id a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: forall a. Eq a => Id a -> Id a -> Bool == :: Id a -> Id a -> Bool $c/= :: forall a. Eq a => Id a -> Id a -> Bool /= :: Id a -> Id a -> Bool Eq, Eq (Id a) Eq (Id a) => (Id a -> Id a -> Ordering) -> (Id a -> Id a -> Bool) -> (Id a -> Id a -> Bool) -> (Id a -> Id a -> Bool) -> (Id a -> Id a -> Bool) -> (Id a -> Id a -> Id a) -> (Id a -> Id a -> Id a) -> Ord (Id a) Id a -> Id a -> Bool Id a -> Id a -> Ordering Id a -> Id a -> Id a forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall a. Ord a => Eq (Id a) forall a. Ord a => Id a -> Id a -> Bool forall a. Ord a => Id a -> Id a -> Ordering forall a. Ord a => Id a -> Id a -> Id a $ccompare :: forall a. Ord a => Id a -> Id a -> Ordering compare :: Id a -> Id a -> Ordering $c< :: forall a. Ord a => Id a -> Id a -> Bool < :: Id a -> Id a -> Bool $c<= :: forall a. Ord a => Id a -> Id a -> Bool <= :: Id a -> Id a -> Bool $c> :: forall a. Ord a => Id a -> Id a -> Bool > :: Id a -> Id a -> Bool $c>= :: forall a. Ord a => Id a -> Id a -> Bool >= :: Id a -> Id a -> Bool $cmax :: forall a. Ord a => Id a -> Id a -> Id a max :: Id a -> Id a -> Id a $cmin :: forall a. Ord a => Id a -> Id a -> Id a min :: Id a -> Id a -> Id a Ord, Ptr (Id a) -> IO (Id a) Ptr (Id a) -> Int -> IO (Id a) Ptr (Id a) -> Int -> Id a -> IO () Ptr (Id a) -> Id a -> IO () Id a -> Int (Id a -> Int) -> (Id a -> Int) -> (Ptr (Id a) -> Int -> IO (Id a)) -> (Ptr (Id a) -> Int -> Id a -> IO ()) -> (forall b. Ptr b -> Int -> IO (Id a)) -> (forall b. Ptr b -> Int -> Id a -> IO ()) -> (Ptr (Id a) -> IO (Id a)) -> (Ptr (Id a) -> Id a -> IO ()) -> Storable (Id a) forall b. Ptr b -> Int -> IO (Id a) forall b. Ptr b -> Int -> Id a -> IO () forall a. Storable a => Ptr (Id a) -> IO (Id a) forall a. Storable a => Ptr (Id a) -> Int -> IO (Id a) forall a. Storable a => Ptr (Id a) -> Int -> Id a -> IO () forall a. Storable a => Ptr (Id a) -> Id a -> IO () forall a. Storable a => Id a -> Int forall a b. Storable a => Ptr b -> Int -> IO (Id a) forall a b. Storable a => Ptr b -> Int -> Id a -> IO () forall a. (a -> Int) -> (a -> Int) -> (Ptr a -> Int -> IO a) -> (Ptr a -> Int -> a -> IO ()) -> (forall b. Ptr b -> Int -> IO a) -> (forall b. Ptr b -> Int -> a -> IO ()) -> (Ptr a -> IO a) -> (Ptr a -> a -> IO ()) -> Storable a $csizeOf :: forall a. Storable a => Id a -> Int sizeOf :: Id a -> Int $calignment :: forall a. Storable a => Id a -> Int alignment :: Id a -> Int $cpeekElemOff :: forall a. Storable a => Ptr (Id a) -> Int -> IO (Id a) peekElemOff :: Ptr (Id a) -> Int -> IO (Id a) $cpokeElemOff :: forall a. Storable a => Ptr (Id a) -> Int -> Id a -> IO () pokeElemOff :: Ptr (Id a) -> Int -> Id a -> IO () $cpeekByteOff :: forall a b. Storable a => Ptr b -> Int -> IO (Id a) peekByteOff :: forall b. Ptr b -> Int -> IO (Id a) $cpokeByteOff :: forall a b. Storable a => Ptr b -> Int -> Id a -> IO () pokeByteOff :: forall b. Ptr b -> Int -> Id a -> IO () $cpeek :: forall a. Storable a => Ptr (Id a) -> IO (Id a) peek :: Ptr (Id a) -> IO (Id a) $cpoke :: forall a. Storable a => Ptr (Id a) -> Id a -> IO () poke :: Ptr (Id a) -> Id a -> IO () Storable) type M = P.M Id pattern N :: M 'Nothing pattern $mN :: forall {r}. M 'Nothing -> ((# #) -> r) -> ((# #) -> r) -> r $bN :: M 'Nothing N <- P.N where N = M 'Nothing forall {k} (t :: k -> *). M t 'Nothing P.N pattern J :: a -> M ('Just a) pattern $mJ :: forall {r} {a}. M ('Just a) -> (a -> r) -> ((# #) -> r) -> r $bJ :: forall a. a -> M ('Just a) J x <- (P.J (Id x)) where J a x = Id a -> M Id ('Just a) forall {k} (t :: k -> *) (a :: k). t a -> M t ('Just a) P.J (Id a -> M Id ('Just a)) -> Id a -> M Id ('Just a) forall a b. (a -> b) -> a -> b $ a -> Id a forall a. a -> Id a Id a x