module Synthesizer.Dimensional.RateAmplitude.Cut (
splitAt,
take,
drop,
takeUntilPause,
unzip,
unzip3,
leftFromStereo, rightFromStereo,
concat, concatVolume,
append, appendVolume,
zip, zipVolume,
zip3, zip3Volume,
mergeStereo, mergeStereoVolume,
arrange, arrangeVolume,
arrangeStorableVolume,
) where
import qualified Synthesizer.Dimensional.Amplitude.Cut as CutV
import qualified Synthesizer.Dimensional.Rate.Cut as CutR
import qualified Synthesizer.Storable.Cut as CutSt
import qualified Synthesizer.Storable.Signal as SigSt
import qualified Synthesizer.State.Cut as CutS
import qualified Synthesizer.State.Signal as Sig
import qualified Synthesizer.Generic.Signal as SigG
import qualified Synthesizer.Frame.Stereo as Stereo
import Foreign.Storable (Storable, )
import qualified Synthesizer.Dimensional.Amplitude as Amp
import qualified Synthesizer.Dimensional.Rate as Rate
import qualified Synthesizer.Dimensional.Signal.Private as SigA
import qualified Synthesizer.Dimensional.Process as Proc
import Synthesizer.Dimensional.Process (($#), toTimeScalar, intFromTime98, )
import Synthesizer.Dimensional.Signal.Private (toAmplitudeScalar, )
import qualified Number.DimensionTerm as DN
import qualified Algebra.DimensionTerm as Dim
import qualified Data.EventList.Relative.TimeBody as EventList
import qualified Numeric.NonNegative.Wrapper as NonNeg
import qualified Algebra.NormedSpace.Maximum as NormedMax
import qualified Algebra.Module as Module
import qualified Algebra.RealRing as RealRing
import qualified Algebra.Field as Field
import qualified Algebra.Ring as Ring
import qualified Data.List as List
import NumericPrelude.Base ((.), ($), Ord, (<=), map, return, )
import Prelude (RealFrac, )
{-# INLINE splitAt #-}
splitAt :: (RealRing.C t, Dim.C u, Dim.C v, Storable yv) =>
DN.T u t -> Proc.T s u t (SigA.R s v y yv -> (SigA.R s v y yv, SigA.R s v y yv))
splitAt :: forall t u v yv s y.
(C t, C u, C v, Storable yv) =>
T u t -> T s u t (R s v y yv -> (R s v y yv, R s v y yv))
splitAt T u t
t' =
do t
t <- forall t u s. (C t, C u) => T u t -> T s u t t
toTimeScalar T u t
t'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \R s v y yv
x ->
let (T yv
ss0,T yv
ss1) = forall a. Storable a => Int -> T a -> (T a, T a)
Sig.splitAt (forall a b. (C a, C b) => a -> b
RealRing.round t
t) (forall rate amplitude body. T rate amplitude body -> body
SigA.body R s v y yv
x)
in (forall sig1 rate amp sig0.
sig1 -> T rate amp sig0 -> T rate amp sig1
SigA.replaceBody T yv
ss0 R s v y yv
x,
forall sig1 rate amp sig0.
sig1 -> T rate amp sig0 -> T rate amp sig1
SigA.replaceBody T yv
ss1 R s v y yv
x)
{-# INLINE take #-}
take :: (RealRing.C t, Dim.C u, Dim.C v) =>
DN.T u t -> Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv)
take :: forall t u v s y yv.
(C t, C u, C v) =>
T u t -> T s u t (R s v y yv -> R s v y yv)
take T u t
t' =
forall sig t u s amp.
(Transform sig, C t, C u) =>
T u t -> T s u t (Signal s amp sig -> Signal s amp sig)
CutR.take T u t
t'
{-# INLINE drop #-}
drop :: (RealRing.C t, Dim.C u, Dim.C v) =>
DN.T u t -> Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv)
drop :: forall t u v s y yv.
(C t, C u, C v) =>
T u t -> T s u t (R s v y yv -> R s v y yv)
drop T u t
t' =
forall sig t u s amp.
(Transform sig, C t, C u) =>
T u t -> T s u t (Signal s amp sig -> Signal s amp sig)
CutR.drop T u t
t'
{-# INLINE takeUntilPause #-}
takeUntilPause ::
(RealRing.C t, Dim.C u,
Field.C y, NormedMax.C y yv, Dim.C v) =>
DN.T v y -> DN.T u t -> Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv)
takeUntilPause :: forall t u y yv v s.
(C t, C u, C y, C y yv, C v) =>
T v y -> T u t -> T s u t (R s v y yv -> R s v y yv)
takeUntilPause T v y
y' T u t
t' =
do t
t <- forall t u s. (C t, C u) => T u t -> T s u t t
toTimeScalar T u t
t'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \R s v y yv
x ->
let y :: y
y = forall y v rate sig.
(C y, C v) =>
T rate (Dimensional v y) sig -> T v y -> y
toAmplitudeScalar R s v y yv
x T v y
y'
in forall sig0 sig1 rate amp.
(sig0 -> sig1) -> T rate amp sig0 -> T rate amp sig1
SigA.processBody
(forall a. (a -> Bool) -> Int -> T a -> T a
CutS.takeUntilInterval ((forall a. Ord a => a -> a -> Bool
<=y
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a v. C a v => v -> a
NormedMax.norm)
(forall a b. (C a, C b) => a -> b
RealRing.ceiling t
t)) R s v y yv
x
{-# INLINE unzip #-}
unzip :: (Dim.C u, Dim.C v) =>
Proc.T s u t
(SigA.R s v y (yv0, yv1) ->
(SigA.R s v y yv0, SigA.R s v y yv1))
unzip :: forall u v s t y yv0 yv1.
(C u, C v) =>
T s u t (R s v y (yv0, yv1) -> (R s v y yv0, R s v y yv1))
unzip = forall a s u t. a -> T s u t a
Proc.pure forall (sig :: * -> *) yv0 yv1 rate amp.
(Transform sig (yv0, yv1), Transform sig yv0, Transform sig yv1) =>
T rate amp (sig (yv0, yv1))
-> (T rate amp (sig yv0), T rate amp (sig yv1))
CutV.unzip
{-# INLINE unzip3 #-}
unzip3 :: (Dim.C u, Dim.C v) =>
Proc.T s u t
(SigA.R s v y (yv0, yv1, yv2) ->
(SigA.R s v y yv0, SigA.R s v y yv1, SigA.R s v y yv2))
unzip3 :: forall u v s t y yv0 yv1 yv2.
(C u, C v) =>
T s
u
t
(R s v y (yv0, yv1, yv2)
-> (R s v y yv0, R s v y yv1, R s v y yv2))
unzip3 = forall a s u t. a -> T s u t a
Proc.pure forall (sig :: * -> *) yv0 yv1 yv2 rate amp.
(Transform sig (yv0, yv1, yv2), Transform sig yv0,
Transform sig yv1, Transform sig yv2) =>
T rate amp (sig (yv0, yv1, yv2))
-> (T rate amp (sig yv0), T rate amp (sig yv1),
T rate amp (sig yv2))
CutV.unzip3
{-# INLINE leftFromStereo #-}
leftFromStereo :: (Dim.C u) =>
Proc.T s u t
(SigA.R s u y (Stereo.T yv) -> SigA.R s u y yv)
leftFromStereo :: forall u s t y yv. C u => T s u t (R s u y (T yv) -> R s u y yv)
leftFromStereo = forall a s u t. a -> T s u t a
Proc.pure forall u s y yv. C u => R s u y (T yv) -> R s u y yv
CutV.leftFromStereo
{-# INLINE rightFromStereo #-}
rightFromStereo :: (Dim.C u) =>
Proc.T s u t
(SigA.R s u y (Stereo.T yv) -> SigA.R s u y yv)
rightFromStereo :: forall u s t y yv. C u => T s u t (R s u y (T yv) -> R s u y yv)
rightFromStereo = forall a s u t. a -> T s u t a
Proc.pure forall u s y yv. C u => R s u y (T yv) -> R s u y yv
CutV.rightFromStereo
{-# INLINE concat #-}
concat ::
(Ord y, Field.C y, Dim.C v, Dim.C u,
Module.C y yv) =>
Proc.T s u t ([SigA.R s v y yv] -> SigA.R s v y yv)
concat :: forall y v u yv s t.
(Ord y, C y, C v, C u, C y yv) =>
T s u t ([R s v y yv] -> R s v y yv)
concat = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(Ord y, C y, C u, C y yv, Transform sig yv) =>
[Signal s u y sig yv] -> Signal s u y sig yv
CutV.concat
{-# INLINE concatVolume #-}
concatVolume ::
(Field.C y, Dim.C v, Dim.C u,
Module.C y yv) =>
DN.T v y -> Proc.T s u t ([SigA.R s v y yv] -> SigA.R s v y yv)
concatVolume :: forall y v u yv s t.
(C y, C v, C u, C y yv) =>
T v y -> T s u t ([R s v y yv] -> R s v y yv)
concatVolume T v y
amp = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(C y, C u, C y yv, Transform sig yv) =>
T u y -> [Signal s u y sig yv] -> Signal s u y sig yv
CutV.concatVolume T v y
amp
{-# INLINE append #-}
append ::
(Ord y, Field.C y, Dim.C v, Dim.C u,
Module.C y yv) =>
Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv -> SigA.R s v y yv)
append :: forall y v u yv s t.
(Ord y, C y, C v, C u, C y yv) =>
T s u t (R s v y yv -> R s v y yv -> R s v y yv)
append = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(Ord y, C y, C u, C y yv, Transform sig yv) =>
Signal s u y sig yv -> Signal s u y sig yv -> Signal s u y sig yv
CutV.append
{-# INLINE appendVolume #-}
appendVolume ::
(Field.C y, Dim.C v, Dim.C u,
Module.C y yv) =>
DN.T v y ->
Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv -> SigA.R s v y yv)
appendVolume :: forall y v u yv s t.
(C y, C v, C u, C y yv) =>
T v y -> T s u t (R s v y yv -> R s v y yv -> R s v y yv)
appendVolume T v y
amp = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(C y, C u, C y yv, Transform sig yv) =>
T u y
-> Signal s u y sig yv
-> Signal s u y sig yv
-> Signal s u y sig yv
CutV.appendVolume T v y
amp
{-# INLINE zip #-}
zip ::
(Ord y, Field.C y, Dim.C v,
Module.C y yv0, Module.C y yv1) =>
Proc.T s u t (SigA.R s v y yv0 -> SigA.R s v y yv1 -> SigA.R s v y (yv0,yv1))
zip :: forall y v yv0 yv1 s u t.
(Ord y, C y, C v, C y yv0, C y yv1) =>
T s u t (R s v y yv0 -> R s v y yv1 -> R s v y (yv0, yv1))
zip = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv0 yv1 (sig :: * -> *) s.
(Ord y, C y, C u, C y yv0, C y yv1, Read sig yv0,
Transform sig yv1, Transform sig (yv0, yv1)) =>
Signal s u y sig yv0
-> Signal s u y sig yv1 -> Signal s u y sig (yv0, yv1)
CutV.zip
{-# INLINE zipVolume #-}
zipVolume ::
(Field.C y, Dim.C v,
Module.C y yv0, Module.C y yv1) =>
DN.T v y ->
Proc.T s u t (SigA.R s v y yv0 -> SigA.R s v y yv1 -> SigA.R s v y (yv0,yv1))
zipVolume :: forall y v yv0 yv1 s u t.
(C y, C v, C y yv0, C y yv1) =>
T v y -> T s u t (R s v y yv0 -> R s v y yv1 -> R s v y (yv0, yv1))
zipVolume T v y
amp = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv0 yv1 (sig :: * -> *) s.
(C y, C u, C y yv0, C y yv1, Read sig yv0, Transform sig yv1,
Transform sig (yv0, yv1)) =>
T u y
-> Signal s u y sig yv0
-> Signal s u y sig yv1
-> Signal s u y sig (yv0, yv1)
CutV.zipVolume T v y
amp
{-# INLINE mergeStereo #-}
mergeStereo ::
(Ord y, Field.C y, Dim.C v,
Module.C y yv) =>
Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv -> SigA.R s v y (Stereo.T yv))
mergeStereo :: forall y v yv s u t.
(Ord y, C y, C v, C y yv) =>
T s u t (R s v y yv -> R s v y yv -> R s v y (T yv))
mergeStereo = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(Ord y, C y, C u, C y yv, Transform sig yv,
Transform sig (T yv)) =>
Signal s u y sig yv
-> Signal s u y sig yv -> Signal s u y sig (T yv)
CutV.mergeStereo
{-# INLINE mergeStereoVolume #-}
mergeStereoVolume ::
(Field.C y, Dim.C v,
Module.C y yv) =>
DN.T v y ->
Proc.T s u t (SigA.R s v y yv -> SigA.R s v y yv -> SigA.R s v y (Stereo.T yv))
mergeStereoVolume :: forall y v yv s u t.
(C y, C v, C y yv) =>
T v y -> T s u t (R s v y yv -> R s v y yv -> R s v y (T yv))
mergeStereoVolume T v y
amp = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv (sig :: * -> *) s.
(C y, C u, C y yv, Transform sig yv, Transform sig (T yv)) =>
T u y
-> Signal s u y sig yv
-> Signal s u y sig yv
-> Signal s u y sig (T yv)
CutV.mergeStereoVolume T v y
amp
{-# INLINE zip3 #-}
zip3 ::
(Ord y, Field.C y, Dim.C v,
Module.C y yv0, Module.C y yv1, Module.C y yv2) =>
Proc.T s u t (
SigA.R s v y yv0 -> SigA.R s v y yv1 -> SigA.R s v y yv2 ->
SigA.R s v y (yv0,yv1,yv2))
zip3 :: forall y v yv0 yv1 yv2 s u t.
(Ord y, C y, C v, C y yv0, C y yv1, C y yv2) =>
T s
u
t
(R s v y yv0
-> R s v y yv1 -> R s v y yv2 -> R s v y (yv0, yv1, yv2))
zip3 = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv0 yv1 yv2 (sig :: * -> *) s.
(Ord y, C y, C u, C y yv0, C y yv1, C y yv2, Read sig yv0,
Read sig yv1, Transform sig yv2, Transform sig (yv0, yv1, yv2)) =>
Signal s u y sig yv0
-> Signal s u y sig yv1
-> Signal s u y sig yv2
-> Signal s u y sig (yv0, yv1, yv2)
CutV.zip3
{-# INLINE zip3Volume #-}
zip3Volume ::
(Field.C y, Dim.C v,
Module.C y yv0, Module.C y yv1, Module.C y yv2) =>
DN.T v y ->
Proc.T s u t (
SigA.R s v y yv0 -> SigA.R s v y yv1 -> SigA.R s v y yv2 ->
SigA.R s v y (yv0,yv1,yv2))
zip3Volume :: forall y v yv0 yv1 yv2 s u t.
(C y, C v, C y yv0, C y yv1, C y yv2) =>
T v y
-> T s
u
t
(R s v y yv0
-> R s v y yv1 -> R s v y yv2 -> R s v y (yv0, yv1, yv2))
zip3Volume T v y
amp = forall a s u t. a -> T s u t a
Proc.pure forall a b. (a -> b) -> a -> b
$ forall y u yv0 yv1 yv2 (sig :: * -> *) s.
(C y, C u, C y yv0, C y yv1, C y yv2, Read sig yv0, Read sig yv1,
Transform sig yv2, Transform sig (yv0, yv1, yv2)) =>
T u y
-> Signal s u y sig yv0
-> Signal s u y sig yv1
-> Signal s u y sig yv2
-> Signal s u y sig (yv0, yv1, yv2)
CutV.zip3Volume T v y
amp
{-# INLINE arrange #-}
arrange ::
(Ring.C t, Dim.C u,
RealFrac t,
Ord y, Field.C y, Dim.C v,
Module.C y yv, Storable yv) =>
DN.T u t
-> DN.T u t
-> Proc.T s u t (
EventList.T (NonNeg.T t) (SigA.R s v y yv)
-> SigA.R s v y yv)
arrange :: forall t u y v yv s.
(C t, C u, RealFrac t, Ord y, C y, C v, C y yv, Storable yv) =>
T u t -> T u t -> T s u t (T (T t) (R s v y yv) -> R s v y yv)
arrange T u t
chunkSize T u t
unit' =
forall a s u t b. (a -> T s u t b) -> T s u t (a -> b)
Proc.withParam forall a b. (a -> b) -> a -> b
$ \T (T t) (R s v y yv)
sched ->
let amp :: T v y
amp = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
List.maximum (forall a b. (a -> b) -> [a] -> [b]
map forall rate amp sig. T rate (Numeric amp) sig -> amp
SigA.actualAmplitude (forall time body. T time body -> [body]
EventList.getBodies T (T t) (R s v y yv)
sched))
in forall t u y v yv s.
(C t, C u, RealFrac t, C y, C v, C y yv, Storable yv) =>
T u t
-> T v y -> T u t -> T s u t (T (T t) (R s v y yv) -> R s v y yv)
arrangeVolume T u t
chunkSize T v y
amp T u t
unit' forall (f :: * -> *) a b. Functor f => f (a -> b) -> a -> f b
$# T (T t) (R s v y yv)
sched
{-# INLINE arrangeVolume #-}
arrangeVolume ::
(Ring.C t, Dim.C u,
RealFrac t,
Field.C y, Dim.C v,
Module.C y yv, Storable yv) =>
DN.T u t
-> DN.T v y
-> DN.T u t
-> Proc.T s u t (
EventList.T (NonNeg.T t) (SigA.R s v y yv)
-> SigA.R s v y yv)
arrangeVolume :: forall t u y v yv s.
(C t, C u, RealFrac t, C y, C v, C y yv, Storable yv) =>
T u t
-> T v y -> T u t -> T s u t (T (T t) (R s v y yv) -> R s v y yv)
arrangeVolume T u t
chunkSize' T v y
amp T u t
unit' =
do t
unit <- forall t u s. (C t, C u) => T u t -> T s u t t
toTimeScalar T u t
unit'
Int
chunkSize <-
forall t u s.
(C t, RealFrac t, C u) =>
String -> T u t -> T s u t Int
intFromTime98 String
"Dimensional.Cut.arrangeStorableVolume" T u t
chunkSize'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \T (T t) (R s v y yv)
sched ->
let z :: T (Phantom s) (Numeric (T v y)) (T yv)
z =
forall amp sig s. amp -> sig -> T (Phantom s) (Numeric amp) sig
SigA.fromBody T v y
amp forall a b. (a -> b) -> a -> b
$
forall (sig :: * -> *) y.
(Read0 sig, Storage (sig y)) =>
sig y -> T y
SigG.toState forall a b. (a -> b) -> a -> b
$
forall v. (Storable v, C v) => ChunkSize -> T Int (T v) -> T v
CutSt.arrange (Int -> ChunkSize
SigSt.chunkSize Int
chunkSize) forall a b. (a -> b) -> a -> b
$
forall time i body.
(C time, RealFrac time, C i, Integral i) =>
time -> T time body -> T i body
EventList.resample
(forall a. (Ord a, Num a) => String -> a -> T a
NonNeg.fromNumberMsg String
"Dimensional.Cut.arrangeVolume" t
unit) forall a b. (a -> b) -> a -> b
$
forall body0 body1 time.
(body0 -> body1) -> T time body0 -> T time body1
EventList.mapBody
(forall (sig :: * -> *) y. Write sig y => LazySize -> T y -> sig y
SigG.fromState (Int -> LazySize
SigG.LazySize Int
chunkSize) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall y yv (sig :: * -> *) amp rate.
(C y yv, Transform sig yv) =>
(amp -> y) -> T rate (Numeric amp) (sig yv) -> sig yv
SigA.vectorSamples (forall y v rate sig.
(C y, C v) =>
T rate (Dimensional v y) sig -> T v y -> y
toAmplitudeScalar T (Phantom s) (Numeric (T v y)) (T yv)
z))
T (T t) (R s v y yv)
sched
in forall {s}. T (Phantom s) (Numeric (T v y)) (T yv)
z
{-# INLINE arrangeStorableVolume #-}
arrangeStorableVolume ::
(Ring.C t, Dim.C u,
RealFrac t,
Field.C y, Dim.C v,
Module.C y yv, Storable yv) =>
DN.T u t
-> DN.T v y
-> DN.T u t
-> Proc.T s u t (
EventList.T (NonNeg.T t)
(SigA.T (Rate.Phantom s) (Amp.Dimensional v y) (SigSt.T yv))
-> (SigA.T (Rate.Phantom s) (Amp.Dimensional v y) (SigSt.T yv)))
arrangeStorableVolume :: forall t u y v yv s.
(C t, C u, RealFrac t, C y, C v, C y yv, Storable yv) =>
T u t
-> T v y
-> T u t
-> T s
u
t
(T (T t) (T (Phantom s) (Dimensional v y) (T yv))
-> T (Phantom s) (Dimensional v y) (T yv))
arrangeStorableVolume T u t
chunkSize' T v y
amp T u t
unit' =
do t
unit <- forall t u s. (C t, C u) => T u t -> T s u t t
toTimeScalar T u t
unit'
Int
chunkSize <-
forall t u s.
(C t, RealFrac t, C u) =>
String -> T u t -> T s u t Int
intFromTime98 String
"Dimensional.Cut.arrangeStorableVolume" T u t
chunkSize'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \T (T t) (T (Phantom s) (Dimensional v y) (T yv))
sched ->
let z :: T (Phantom s) (Dimensional v y) (T yv)
z =
forall amp sig s. amp -> sig -> T (Phantom s) (Numeric amp) sig
SigA.fromBody T v y
amp forall a b. (a -> b) -> a -> b
$
forall v. (Storable v, C v) => ChunkSize -> T Int (T v) -> T v
CutSt.arrange (Int -> ChunkSize
SigSt.chunkSize Int
chunkSize) forall a b. (a -> b) -> a -> b
$
forall time i body.
(C time, RealFrac time, C i, Integral i) =>
time -> T time body -> T i body
EventList.resample
(forall a. (Ord a, Num a) => String -> a -> T a
NonNeg.fromNumberMsg String
"Dimensional.Cut.arrangeStorableVolume" t
unit) forall a b. (a -> b) -> a -> b
$
forall body0 body1 time.
(body0 -> body1) -> T time body0 -> T time body1
EventList.mapBody
(forall y yv (sig :: * -> *) amp rate.
(C y yv, Transform sig yv) =>
(amp -> y) -> T rate (Numeric amp) (sig yv) -> sig yv
SigA.vectorSamples (forall y v rate sig.
(C y, C v) =>
T rate (Dimensional v y) sig -> T v y -> y
toAmplitudeScalar T (Phantom s) (Dimensional v y) (T yv)
z))
T (T t) (T (Phantom s) (Dimensional v y) (T yv))
sched
in forall {s}. T (Phantom s) (Dimensional v y) (T yv)
z