Safe Haskell | None |
---|---|

Language | Haskell2010 |

- removeFL :: (MyEq p, Commute p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
- removeRL :: (MyEq p, Commute p) => p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
- removeCommon :: (MyEq p, Commute p) => (FL p :\/: FL p) wX wY -> (FL p :\/: FL p) wX wY
- commuteWhatWeCanFL :: Commute p => (p :> FL p) wX wY -> (FL p :> (p :> FL p)) wX wY
- commuteWhatWeCanRL :: Commute p => (RL p :> p) wX wY -> (RL p :> (p :> RL p)) wX wY
- genCommuteWhatWeCanRL :: Commute p => (forall wA wB. (p :> q) wA wB -> Maybe ((q :> p) wA wB)) -> (RL p :> q) wX wY -> (RL p :> (q :> RL p)) wX wY
- genCommuteWhatWeCanFL :: Commute q => (forall wA wB. (p :> q) wA wB -> Maybe ((q :> p) wA wB)) -> (p :> FL q) wX wY -> (FL q :> (p :> FL q)) wX wY
- partitionFL :: Commute p => (forall wU wV. p wU wV -> Bool) -> FL p wX wY -> (FL p :> (FL p :> FL p)) wX wY
- partitionRL :: Commute p => (forall wU wV. p wU wV -> Bool) -> RL p wX wY -> (RL p :> RL p) wX wY
- simpleHeadPermutationsFL :: Commute p => FL p wX wY -> [FL p wX wY]
- headPermutationsRL :: Commute p => RL p wX wY -> [RL p wX wY]
- headPermutationsFL :: Commute p => FL p wX wY -> [(p :> FL p) wX wY]
- removeSubsequenceFL :: (MyEq p, Commute p) => FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
- removeSubsequenceRL :: (MyEq p, Commute p) => RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
- partitionConflictingFL :: (Commute p1, Invert p1) => CommuteFn p1 p2 -> FL p1 wX wY -> p2 wX wZ -> (FL p1 :> FL p1) wX wY
- inverseCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p

# Documentation

genCommuteWhatWeCanRL :: Commute p => (forall wA wB. (p :> q) wA wB -> Maybe ((q :> p) wA wB)) -> (RL p :> q) wX wY -> (RL p :> (q :> RL p)) wX wY Source

genCommuteWhatWeCanFL :: Commute q => (forall wA wB. (p :> q) wA wB -> Maybe ((q :> p) wA wB)) -> (p :> FL q) wX wY -> (FL q :> (p :> FL q)) wX wY Source

:: Commute p | |

=> (forall wU wV. p wU wV -> Bool) | predicate; if true we would like the patch in the "left" list |

-> FL p wX wY | input |

-> (FL p :> (FL p :> FL p)) wX wY | "left", "middle" and "right" |

split an `FL`

into "left" and "right" lists according to a predicate `p`

, using commutation as necessary.
If a patch does satisfy the predicate but cannot be commuted past one that does not satisfy
the predicate, it goes in the "middle" list; to sum up, we have: `all p left`

and `all (not.p) right`

, while
midddle is mixed.
Note that `p`

should be invariant under commutation (i.e. if `x1`

can commute to `x2`

then 'p x1 = p x2').

:: Commute p | |

=> (forall wU wV. p wU wV -> Bool) | predicate; if true we would like the patch in the "right" list |

-> RL p wX wY | input |

-> (RL p :> RL p) wX wY | "left" and "right" results |

split an `RL`

into "left" and "right" lists according to a predicate, using commutation as necessary.
If a patch does satisfy the predicate but cannot be commuted past one that does not satisfy
the predicate, it goes in the "left" list.

simpleHeadPermutationsFL :: Commute p => FL p wX wY -> [FL p wX wY] Source

This is a minor variant of `headPermutationsFL`

with each permutation
is simply returned as a `FL`

headPermutationsRL :: Commute p => RL p wX wY -> [RL p wX wY] Source

`headPermutationsRL`

is like `headPermutationsFL`

, except that we
operate on an `RL`

(in other words, we are pushing things to the end of a
patch sequence instead of to the beginning).

headPermutationsFL :: Commute p => FL p wX wY -> [(p :> FL p) wX wY] Source

`headPermutationsFL`

`p:>:ps`

returns all the permutations of the list
in which one element of `ps`

is commuted past `p`

Suppose we have a sequence of patches

X h a y s-t-c k

Suppose furthermore that the patch `c`

depends on `t`

, which in turn
depends on `s`

. This function will return

X :> h a y s t c k h :> X a y s t c k a :> X h y s t c k y :> X h a s t c k s :> X h a y t c k k :> X h a y s t c

removeSubsequenceFL :: (MyEq p, Commute p) => FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC) Source

`removeSubsequenceFL`

`ab abc`

returns `Just c'`

where all the patches in
`ab`

have been commuted out of it, if possible. If this is not possible
for any reason (the set of patches `ab`

is not actually a subset of `abc`

,
or they can't be commuted out) we return `Nothing`

.

removeSubsequenceRL :: (MyEq p, Commute p) => RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb) Source

`removeSubsequenceRL`

is like `removeSubsequenceFL`

except that it works
on `RL`