ddc-core-simpl-0.4.3.1: Disciplined Disciple Compiler code transformations.

DDC.Core.Transform.Rewrite.Disjoint

Description

Check whether two effects are non-interfering

Synopsis

# Documentation

Arguments

 :: Ord n => Type n Type of property we want eg Disjoint e1 e2 -> 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.

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
= True
 :: Ord n => Type n Type of the property we want, eg Distinct r1 r2 -> RewriteEnv a n Environment we're rewriting in. -> Bool