{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -- > import Ouroboros.Consensus.HardFork.Combinator.Util.Tails (Tails(..)) -- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Tails as Tails module Ouroboros.Consensus.HardFork.Combinator.Util.Tails ( Tails (..) -- * Convenience constructors , mk1 , mk2 , mk3 -- * SOP-like operators , hcmap , hcpure , hmap , hpure ) where import Data.Kind (Type) import Data.SOP.Strict hiding (hcmap, hcpure, hmap, hpure) import qualified Data.SOP.Strict as SOP {------------------------------------------------------------------------------- Tails -------------------------------------------------------------------------------} -- | For every tail @(x ': xs)@ of the list, an @f x y@ for every @y@ in @xs@ data Tails (f :: k -> k -> Type) (xs :: [k]) where TNil :: Tails f '[] TCons :: NP (f x) xs -> Tails f xs -> Tails f (x ': xs) {------------------------------------------------------------------------------- Convenience constructors -------------------------------------------------------------------------------} mk1 :: Tails f '[x] mk1 :: Tails f '[x] mk1 = NP (f x) '[] -> Tails f '[] -> Tails f '[x] forall a (f :: a -> a -> *) (x :: a) (xs :: [a]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons NP (f x) '[] forall k (f :: k -> *). NP f '[] Nil Tails f '[] forall k (f :: k -> k -> *). Tails f '[] TNil mk2 :: f x y -> Tails f '[x, y] mk2 :: f x y -> Tails f '[x, y] mk2 f x y xy = NP (f x) '[y] -> Tails f '[y] -> Tails f '[x, y] forall a (f :: a -> a -> *) (x :: a) (xs :: [a]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (f x y xy f x y -> NP (f x) '[] -> NP (f x) '[y] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (f x) '[] forall k (f :: k -> *). NP f '[] Nil) Tails f '[y] forall k (f :: k -> k -> *) (x :: k). Tails f '[x] mk1 mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z] mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z] mk3 f x y xy f x z xz f y z yz = NP (f x) '[y, z] -> Tails f '[y, z] -> Tails f '[x, y, z] forall a (f :: a -> a -> *) (x :: a) (xs :: [a]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (f x y xy f x y -> NP (f x) '[z] -> NP (f x) '[y, z] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* f x z xz f x z -> NP (f x) '[] -> NP (f x) '[z] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (f x) '[] forall k (f :: k -> *). NP f '[] Nil) (f y z -> Tails f '[y, z] forall k (f :: k -> k -> *) (x :: k) (y :: k). f x y -> Tails f '[x, y] mk2 f y z yz) {------------------------------------------------------------------------------- SOP-like operators -------------------------------------------------------------------------------} hmap :: SListI xs => (forall x y. f x y -> g x y) -> Tails f xs -> Tails g xs hmap :: (forall (x :: k) (y :: k). f x y -> g x y) -> Tails f xs -> Tails g xs hmap = Proxy Top -> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y) -> Tails f xs -> Tails g xs forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hcmap :: forall proxy c f g xs. All c xs => proxy c -> (forall x y. (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap :: proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap proxy c p forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y g = Tails f xs -> Tails g xs forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs' go where go :: All c xs' => Tails f xs' -> Tails g xs' go :: Tails f xs' -> Tails g xs' go Tails f xs' TNil = Tails g xs' forall k (f :: k -> k -> *). Tails f '[] TNil go (TCons NP (f x) xs fs Tails f xs fss) = NP (g x) xs -> Tails g xs -> Tails g (x : xs) forall a (f :: a -> a -> *) (x :: a) (xs :: [a]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (proxy c -> (forall (a :: k). c a => f x a -> g x a) -> NP (f x) xs -> NP (g x) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs SOP.hcmap proxy c p forall (a :: k). c a => f x a -> g x a forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y g NP (f x) xs fs) (Tails f xs -> Tails g xs forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs' go Tails f xs fss) hpure :: SListI xs => (forall x y. f x y) -> Tails f xs hpure :: (forall (x :: k) (y :: k). f x y) -> Tails f xs hpure = Proxy Top -> (forall (x :: k) (y :: k). (Top x, Top y) => f x y) -> Tails f xs forall k (proxy :: (k -> Constraint) -> *) (f :: k -> k -> *) (c :: k -> Constraint) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs hcpure (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hcpure :: forall proxy f c xs. All c xs => proxy c -> (forall x y. (c x, c y) => f x y) -> Tails f xs hcpure :: proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs hcpure proxy c p forall (x :: k) (y :: k). (c x, c y) => f x y f = SList xs -> Tails f xs forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: All c xs' => SList xs' -> Tails f xs' go :: SList xs' -> Tails f xs' go SList xs' SNil = Tails f xs' forall k (f :: k -> k -> *). Tails f '[] TNil go SList xs' SCons = NP (f x) xs -> Tails f xs -> Tails f (x : xs) forall a (f :: a -> a -> *) (x :: a) (xs :: [a]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (proxy c -> (forall (a :: k). c a => f x a) -> NP (f x) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs SOP.hcpure proxy c p forall (a :: k). c a => f x a forall (x :: k) (y :: k). (c x, c y) => f x y f) (SList xs -> Tails f xs forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList)