Safe Haskell	None
Language	GHC2024

Proarrow.Tools.DPO

Description

Double-pushout (DPO) rewriting.

A rewrite Rule is a span l <~ a ~> r: a is the interface that's preserved by the rewrite, l is matched against the host object, and r replaces it. Applying a rule at a match m :: l ~> g proceeds in two pushout steps, both performed by dpoStep:

Compute the pushout complement of the rule's left leg and the match, giving the "rest of the world" object d together with legs a ~> d and d ~> g. This step can fail if the match doesn't satisfy the gluing condition.
Push a ~> d out along the rule's right leg a ~> r to get the result h, together with legs d ~> h and r ~> h.

The two legs out of d (d ~> g and d ~> h) exhibit the rewrite step as a cospan g <- d -> h relating the object before and after the rewrite.

Synopsis

class HasPushouts k => HasPushoutComplements k where
- pushoutComplement :: forall (a :: k) (l :: k) (g :: k) ans. (a ~> l) -> (l ~> g) -> (forall (d :: k). (a ~> d) -> (d ~> g) -> ans) -> ans -> ans
data Rule (a :: k) (l :: k) (r :: k) where
- Rule :: forall {k} (a :: k) (l :: k) (r :: k). (a ~> l) -> (a ~> r) -> Rule a l r
dpoStep :: forall {k} (a :: k) (l :: k) (r :: k) (g :: k) ans. HasPushoutComplements k => Rule a l r -> (l ~> g) -> (forall (d :: k) (h :: k). (d ~> g) -> (d ~> h) -> (r ~> h) -> ans) -> ans -> ans

Documentation

class HasPushouts k => HasPushoutComplements k where Source Github #

Categories where pushout complements can be computed, or shown not to exist.

Given the left leg ll :: a ~> l of a rule (assumed mono, i.e. a embeds into l) and a match m :: l ~> g, pushoutComplement either succeeds with an object d and legs a ~> d, d ~> g forming a pushout square with ll and m, or calls the second continuation when no such object exists (the gluing condition fails).

Methods

pushoutComplement :: forall (a :: k) (l :: k) (g :: k) ans. (a ~> l) -> (l ~> g) -> (forall (d :: k). (a ~> d) -> (d ~> g) -> ans) -> ans -> ans Source Github #

Instances

Instances details

HasPushoutComplements FINHASK Source Github #
Instance details Defined in Proarrow.Tools.DPO Methods pushoutComplement :: forall (a :: FINHASK) (l :: FINHASK) (g :: FINHASK) ans. (a ~> l) -> (l ~> g) -> (forall (d :: FINHASK). (a ~> d) -> (d ~> g) -> ans) -> ans -> ans Source Github #

data Rule (a :: k) (l :: k) (r :: k) where Source Github #

A rewrite rule: a span l <~ a ~> r. Both legs are conventionally mono: a is the shared interface, l \ a is what the rule deletes, r \ a is what it creates.

Constructors

Rule :: forall {k} (a :: k) (l :: k) (r :: k). (a ~> l) -> (a ~> r) -> Rule a l r

dpoStep :: forall {k} (a :: k) (l :: k) (r :: k) (g :: k) ans. HasPushoutComplements k => Rule a l r -> (l ~> g) -> (forall (d :: k) (h :: k). (d ~> g) -> (d ~> h) -> (r ~> h) -> ans) -> ans -> ans Source Github #

Apply a Rule at a match l ~> g. On success, the continuation receives the rewrite step's cospan legs d ~> g, d ~> h and the embedding r ~> h of the newly created pattern in the result h. Calls the failure continuation if the gluing condition fails.