Safe Haskell | Safe-Inferred |
---|

Check whether two effects are non-interfering

- checkDisjoint :: (Ord n, Show n) => Type n -> RewriteEnv a n -> Bool
- checkDistinct :: Ord n => Type n -> RewriteEnv a n -> Bool

# Documentation

:: (Ord n, Show n) | |

=> Type n | Type of property we want
eg |

-> RewriteEnv a n | Environment we're rewriting in. |

-> Bool |

Check whether a disjointness property is true in the given rewrite environment.

Disjointness means that two effects do not interfere.

Context is important because if two regions are known to be distinct, reading from one and writing to another is valid. If they have different names they may not be distinct.

All read effects are disjoint with other reads.

Disjoint (Read r1) (Read r2) Disjoint (Read r1) (DeepRead a)

Allocation effects are disjoint with everything.

Disjoint (Alloc r) (_)

Atomic reads and write effects are disjoint if they are to distinct regions.

Distinct r1 r2 ----------------------------- Disjoint (Read r1) (Write r2)

`DeepWrite`

effects are only disjoint with allocation effects, because
we don't know what regions it will write to.

An effect sum is disjoint from some other effect if all its components are.

Disjoint f1 g /\ Disjoint f2 g ----------------------------- Disjoint (f1 + f2) g

Disjointness is commutative.

Disjoint f g ------------ Disjoint g f

Example:

checkDisjoint (Disjoint (Read r1 + Read r2) (Write r3)) [Distinct r1 r3, Distinct r2 r3] = True

:: Ord n | |

=> Type n | Type of the property we want,
eg |

-> RewriteEnv a n | Environment we're rewriting in. |

-> Bool |

Check whether a distintness property is true in the given rewrite environment.

Distinctness means that two regions do not alias.