Modulevortex-journal-0.1.0GHC2024

Vortex.Journal.Migrate

Migration along a morphism of nets. A morphism sends each answered operation of the source to one of the target and each token to a marking of the target; it is a morphism when the target's initial marking, pre and post are the images of the source's. A log migrates by sending each entry along it, and then folding the migrated log in the target is sending the source fold along it: the fold is a functor.

2 types
3 values

Packagevortex-journal-0.1.0
Exports5
LanguageGHC2024
LicenceMIT
SourceMigrate.hs

datadata NetMorphism op ans tok op' ans' tok'

A candidate morphism from nets over one operation and token type to nets over another.

Constructors

MkNetMorphism
- morphAnswered :: Answered op ans -> Answered op' ans'
- morphToken :: tok -> Marking tok'

valuetranslate

:: Ord tok'
=> NetMorphism op ans tok op' ans' tok'
-> Marking tok
-> Marking tok'

A marking sent along the morphism.

valuemigrate

:: Ord tok'
=> NetMorphism op ans tok op' ans' tok'
-> Log op ans tok
-> Log op' ans' tok'

A log sent along the morphism, entry by entry (a resumed log's base marking too).

datadata MorphismError op ans

Why a candidate is not a morphism.

Constructors

InitialNotPreserved
PreNotPreserved (Answered op ans)
PostNotPreserved (Answered op ans)

Instances2Eq, Show

(Eq op, Eq ans) => Eq (MorphismError op ans)Defined in vortex-journal-0.1.0 · Vortex.Journal.Migrate
(Show op, Show ans) => Show (MorphismError op ans)Defined in vortex-journal-0.1.0 · Vortex.Journal.Migrate

valuecheckMorphism

:: Ord tok'
=> Net op ans tok
-> Net op' ans' tok'
-> [Answered op ans]
-> NetMorphism op ans tok op' ans' tok'
-> [MorphismError op ans]

Check a candidate against the source's operations, as listed: the target's initial marking must be the source's sent along it, and so must every operation's pre and post.