WAGS.Move

class Move (at :: Ptr) (from :: Type) (to :: Nat) (i :: Graph) (o :: Graph) | at from to i -> o where

Move an edge in an edge list for a given node. As an example, if we have a gain node with incoming edges 7,8,9, this can be used to move 7 to the end of the list so that we have 8,9,7. This is useful in conjunction with rebasing if two graphs are almost similar save their edge lists, which have a different order.

at - a ptr to the node whose edges we will move from - the edge we are moving - either an index (Nat) or audio unit ref to - the new position in the list i - the input universe o - the output universe

Members

• move :: forall env audio engine proof m res currentIdx changeBit skolems. Monad m => AudioUnitRef at -> from -> Proxy to -> FrameT env audio engine proof m res (UniverseC currentIdx i changeBit skolems) (UniverseC currentIdx o changeBit skolems) Unit

Instances

• (GraphToNodeList graphi nodeListI, MovePointers at from to nodeListI nodeListO, GraphToNodeList grapho nodeListO) => Move at from to graphi grapho

class PtrListLen (i :: PtrList) (n :: Nat) | i -> n

Get the length of pointer list i as natural number n/

Instances

• PtrListLen PtrListNil Z
• (PtrListLen b x) => PtrListLen (PtrListCons a b) (Succ x)

class MovePointer''' (from :: Nat) (to :: Nat) (i :: PtrList) (o :: PtrList) | from to i -> o

Move a poitner from position from to position to in list i and return it as o.

Instances

• (PtrListLen i li, LtEq to li, RemoveAt from i fptr i', InsertIn fptr to i' o) => MovePointer''' from to i o

class InsertIn (fptr :: Ptr) (newTo :: Nat) (i' :: PtrList) (o :: PtrList) | fptr newTo i' -> o

Insert a poitner fptr at newTo in list i' and return it as o.

Instances

• InsertIn fptr Z PtrListNil (PtrListCons fptr PtrListNil)
• InsertIn fptr Z (PtrListCons a b) (PtrListCons fptr (PtrListCons a b))
• (InsertIn fptr x b o) => InsertIn fptr (Succ x) (PtrListCons a b) (PtrListCons a o)

class RemoveAt (from :: Nat) (i :: PtrList) (fptr :: Ptr) (i' :: PtrList) | from i -> fptr i'

Remove whatever is at position from in list i, returning the removed fptr as well as the new pointer list i'.

Instances

• RemoveAt Z (PtrListCons a b) a b
• (RemoveAt x b fptr b') => RemoveAt (Succ x) (PtrListCons a b) fptr (PtrListCons a b')

class GetPtrIndex (found :: Type) (here :: Nat) (ptr :: Ptr) (i :: PtrList) (idx :: Nat) | found here ptr i -> idx

Tail recursive function to get assert that a pointer is at an index

• found - the accumulator of whether we've found the pointer or not
• here - the current index in the recursive function, starts at Z
• ptr - the pointer we are looking for
• i - the pointer list
• idx - the index at which the pointer is found if it is found

Instances

• GetPtrIndex True here ptr i here
• (BinEq ptr a tf, Gate tf here (Succ here) idx, GetPtrIndex tf idx ptr b o) => GetPtrIndex False here ptr (PtrListCons a b) o

class MovePointer'' (from :: Type) (to :: Nat) (i :: PtrList) (o :: PtrList) | from to i -> o

Move a poitner from from, which is either a position or a reference to a value at an index, to position to in list i and return it as o.

Instances

• (GetPtrIndex False Z ptr i idx, MovePointer''' idx to i o) => MovePointer'' (AudioUnitRef ptr) to i o
• (MovePointer''' Z to i o) => MovePointer'' (Proxy Z) to i o
• (MovePointer''' (Succ x) to i o) => MovePointer'' (Proxy (Succ x)) to i o

class MovePointer' (from :: Type) (to :: Nat) (i :: EdgeProfile) (o :: EdgeProfile) | from to i -> o

Move from, which is either a position or a reference to a value at an index, to position to in edge profile i and return the edge profile as o.

Instances

• (MovePointer'' from to (PtrListCons a b) (PtrListCons x y)) => MovePointer' from to (ManyEdges a b) (ManyEdges x y)

class MovePointer (at :: Ptr) (from :: Type) (to :: Nat) (i :: Node) (o :: Node) | at from to i -> o

Instances

• (MovePointer' from to (ManyEdges e l) oe) => MovePointer at from to (NodeC (TGain at) (ManyEdges e l)) (NodeC (TGain at) oe)
• (MovePointer' from to (ManyEdges e l) oe) => MovePointer at from to (NodeC (TSpeaker at) (ManyEdges e l)) (NodeC (TSpeaker at) oe)
• MovePointer at from to i i

class MovePointers (at :: Ptr) (from :: Type) (to :: Nat) (i :: NodeList) (o :: NodeList) | at from to i -> o

At pointer at, move from, which is either a position or a reference to a value at an index, to position to in edge profile i and return the edge profile as o.

Instances

• MovePointers at a b NodeListNil NodeListNil
• (MovePointer at a b head headRes, MovePointers at a b tail tailRes) => MovePointers at a b (NodeListCons head tail) (NodeListCons headRes tailRes)