Dovin.Actions

Actions correspond to things you can do in Magic. They progress the state machine while verifying applicable properties. The all run inside a GameMonad.

Actions will modify the state as specified by the effects listed in their documentation. If any of the validation steps fail away, the proof will fail. Actions are not atomic: if one fails, some effects may have already been applied.

Documentation

step :: String -> GameMonad a -> GameMonad a

Define a high-level step in the proof. A proof typically consists on multiple steps. Each step is a human-readable description, then a definition of that step using actions. If a step fails, no subsequent steps will be run. runStateBasedActions is implicitly called at the end of each step. Nested step invocations execute the nested action but have no other effects - generally they should be avoided.

fork :: String -> GameMonad () -> GameMonad ()

Branch off a labeled alternate line. Steps inside the fork will be reported at the end of the main line output.

Casting

cast :: ManaPool -> CardName -> GameMonad ()

Casts a card from actor's hand. See castFromLocation for specification.

cast "R" "Shock"

Validates

• Card exists in hand.

castFromLocation :: CardLocation -> ManaPool -> CardName -> GameMonad ()

Move a card to the stack, spending the specified mana. If not tracking mana, use the empty string to cast for no mana. Typically you will want to resolve after casting. For the common case of casting from hand, see cast. See spendMana for additional mana validations and effects.

castFromLocation "1B" "Oathsworn Vampire" >> resolveTop

Validates

• Card exists in location.
• If not an instant or has flash, see validateCanCastSorcery for extra validations.

Effects

• Card moved to top of stack.
• Counter storm incremented if card has instant or sorcery attribute.

counter :: CardName -> GameMonad ()

Remove a spell from the stack.

counter "Shock"

Validates

• Card is on stack.
• Card is not a triggered or activated ability.

Effects

• Card is moved to graveyard. (See move for alternate effects.)

flashback :: ManaPool -> CardName -> GameMonad ()

Cast a card from actor's graveyard, exiling it when it leaves the stack. See castFromLocation for further specification.

flashback "R" "Shock"

Does not validate whether the card actually has a flashback cost. If important, use a wrapper function in your solution:

flashbackSnapped mana castName = do
  validate (matchAttribute "snapcastered") castName
  flashback mana castName

Validates

• Card is in actor's graveyard.

Effects

• Card gains exileWhenLeaveStack.

jumpstart :: ManaPool -> CardName -> CardName -> GameMonad ()

Cast a card from active player's graveyard, discarding a card in addition to its mana cost, exiling it when it leaves the stack. See castFromLocation for further specification.

jumpstart "R" "Mountain" "Shock"

Validates

• Card is in actor's graveyard.
• Discard card is in actor's hand.

Effects

• Card gains exileWhenLeaveStack.
• Discard card moved to graveyard.

resolve :: CardName -> GameMonad ()

Resolves a card on the stack.

cast "R" "Shock" >> resolve "Shock"

Validates

• Stack is not empty.
• Card is on top of stack.

Effects

• See resolveTop.

resolveTop :: GameMonad ()

Resolves the top card of the stack. Use this for simple cast-and-resolve scenarios. For more complicated stack states, prefer resolve with a named spell to ensure the expected one is resolving.

Validates

• Stack is not empty.

Effects

• If spell, move card to graveyard of owner.
• If permanent, move card to play area of owner.
• If trigger, remove card.
• See move for possible alternate effects, depending on card attributes.

resolveMentor :: CardName -> CardName -> ExceptT String (ReaderT Env (StateT Board (WriterT [Step] Identity))) ()

Resolves a trigger created by triggerMentor. Adds +1/+1 to target card if still a valid mentor target.

resolveMentor "Goblin 1" "Legion Warboss"

Validates

• Mentor trigger is top of stack.
• Target card is attacking.
• Target card has less power than source card.

Effects

• Target card gets +1/+1.
• Trigger is removed from top of stack.

splice :: CardName -> ManaString -> CardName -> GameMonad ()

Splices a spell on to a previously cast arcane spell.

splice "Goryo's Vengeance" "2RR" "Through the Breach"

Validates

• Target spell is arcane.
• Target spell is on stack.
• Spliced spell is in hand.
• See spendMana for additional validations.

Effects

• See spendMana for additional effects.

tapForMana :: ManaString -> CardName -> GameMonad ()

Combination of tap and addMana, see them for specification.

target :: CardName -> GameMonad ()

Target a permanent.

Validates

• Card is in play.
• If card belongs to opponent, does not have hexproof.

targetInLocation :: CardLocation -> CardName -> GameMonad ()

Target a card in a non-play location.

Validates

• Card is in zone.

Uncategorized

activate :: CardName -> ManaPool -> CardName -> GameMonad ()

Activate an ability of a permanent. See spendMana for additional mana validations and effects. Typically you will want to resolve after activating.

activate "Create Soldier" "3W" "Dawn of Hope" >> resolveTop

Validates

• Card is in play or graveyard.
• Card is controlled by actor.

Effects

• A card with activated is added to stack.

activatePlaneswalker :: CardName -> Int -> CardName -> GameMonad ()

Activate a loyalty ability of a planeswalker. Typically you will want to resolve after activating.

activatePlaneswalker2 "Get a card" (-1) "Karn, Scion of Urza" >> resolveTop

Validates

• Card is in play.
• Card has enough loyalty.

Effects

• Card loyalty is adjusted.

See activate for additional validations and effects.

addEffect :: LayeredEffectPart -> CardName -> GameMonad ()

Adds an "until end of turn" effect to a card. Note in practice, since turns aren't modeled, the effect will stay around until the end of the solution.

addEffect (effectPTSet 1 1) "Soldier"

Effects

• Adds a new "until end of turn" effect to the card with the current timestamp.

attackWith :: [CardName] -> GameMonad ()

Start an attack with the given creatures.

attackWith ["Fanatical Firebrand"]

Validates

• Cards are in play.
• Cards have creature attribute.
• Cards either have haste or are missing summoned.
• Cards do not have defender.

Effects

• Cards become tapped, unless they have vigilance.
• Cards gain attacking attribute.
• Transitions to DeclareAttackers step.

combatDamage :: [CardName] -> CardName -> GameMonad ()

Apply combat damage between an attacker and blockers, using a simple damage assignment algorithm. For more complex assignments, use damage directly.

combatDamage ["Spirit 1", "Spirit 2"] "Angel"

See damage for other validations and effects.

Validates

• Attacker has attribute attacking.
• Attacker and blockers are in play.
• Attacker controlled by current actor.
• Blockers have attribute creature.

Effects

• Damage is dealt to blockers in order given, with the final blocker receiving any left over damage.
• If no blockers, damage is dealt to opposing player.
• If attacker has trample, any remaining damage is dealt to opposing player.

copySpell :: CardName -> CardName -> ExceptT String (ReaderT Env (StateT Board (WriterT [Step] Identity))) ()

Copy a spell on the stack, adding it to top of stack.

copySpell "Snap Copy" "Snap"

Validates

• Card is on stack.

Effects

• New card is on top of stack.

damage

Arguments

:: (Card -> Int)

A function that returns the amount of damage to apply, given the source card.

-> Target

Target to apply damage to

-> CardName

Source card

-> GameMonad ()

Applies damage from a source to a target.

damage (const 2) (targetPlayer Opponent) "Shock"

Validates

• Source exists.
• Damage is not less than zero.
• If targeting a card, target is in play and is either a creature or a planeswalker.

Effects

• Adds damage to the target.
• If target is a planeswalker, remove loyalty counters instead.
• If source has deathtouch and target is a creature and damage is non-zero, add deathtouched attribute to target.
• If source has lifelink, controller of source gains life equal to damage dealt.
• Note runStateBasedActions handles actual destruction (if applicable) of creatures and planeswalkers.

destroy :: CardName -> GameMonad ()

Destroy a permanent.

Validates

• Card is in play.
• Card is not indestructible

Effects

• Card is moved to graveyard. See move for possible alternate effects.

discard :: CardName -> GameMonad ()

Discard a card from the active player's hand.

discard "Mountain"

Validates

• Card exists in active player's hand.

Effects

• Card moved to graveyard.

exert :: CardName -> GameMonad ()

Exert a card. Works best when card has an associated effect that applies when exerted attribute is present.

withAttributes [flying]
  $ withEffect
      (matchInPlay <> matchAttribute exerted)
      (    matchLocation . view cardLocation
        <> const (matchAttribute creature)
      )
      (pure . over cardStrengthModifier (mkStrength (1, 1) <>))
  $ addCreature (2, 2) "Tah-Crop Elite"
attackWith ["Tah-Crop Elite"]
exert "Tah-Crop Elite"

Validates

• Card has tapped attribute.

Effects

• Card gains exerted attribute.

exile :: CardName -> GameMonad ()

Move a card to the Exile zone.

exile "Bridge from Below"

See moveTo for validations and effects.

fight :: CardName -> CardName -> GameMonad ()

Have one card fight another (each deals damage to the other).

Validates

• Card is in play.
• Card is a creature.

Effects

• Each card has damage dealt to it equal to the other's power. A creature fighting itself will take twice its power in damage.
• Note runStateBasedActions handles actual destruction (if applicable) of creatures.

gainLife :: Int -> GameMonad ()

Increments life total for current actor.

as Opponent $ gainLife 1

Effects

• Increases life total by amount

loseLife :: Int -> GameMonad ()

Decrements life total for current actor.

as Opponent $ loseLife 1

Effects

• Decreases life total by amount

modifyStrength :: (Int, Int) -> CardName -> GameMonad ()

Modify the strength of a card in play. It will be reset to base when the card leaves play.

modifyStrength (-2, -2) "Soldier"

Validates

• Card is in play.
• Card is a creature.

Effects

• Changes the strength modifier for the card.

moveTo :: Location -> CardName -> GameMonad ()

Move card to location with same controller.

moveTo Graveyard "Forest"

Validates

• Card exists.

Effects

• Card is moved to location.
• See move for possible alternate effects, depending on card

sacrifice :: CardName -> GameMonad ()

Sacrifice a permanent.

sacrifice "Soldier"

Validates

• Permanent controlled by current actor.
• Permanent is in play.

Effects

• Card is moved to graveyard. See move for possible alternate effects.

setLife :: Int -> GameMonad ()

Sets life total for current actor.

as Opponent $ setLife 1

Effects

• Sets life total to amount

transitionTo :: Phase -> GameMonad ()

Transition to a new game phase or step.

transitionTo DeclareAttackers

Validates

• The new phase would occur after the current phase in a normal turn.

Effects

• Empty the mana pool.
• Transition to new phase.

transitionToForced :: Phase -> GameMonad ()

Equivalent to transitionTo except it skips all validation. Useful when an effect has modified the normal order of phases, such as adding an extra combat step.

trigger :: CardName -> CardName -> GameMonad ()

Triggers an effect of a permanent. Typically you will want to resolve after triggering.

trigger "Draw Card" "Dawn of Hope" >> resolveTop

Validates

• Card is in play or graveyard.
• Card is cotrolled by actor.

Effects

• A card with triggered is added to stack.

triggerMentor :: CardName -> CardName -> GameMonad ()

Triggers a mentor effect from an attacking creature, targeting another attacking creature with lesser power. Typically you will want to resolveMentor after triggering.

triggerMentor "Goblin 1" "Legion Warboss"

Validates

• Source card has attacking and mentor attributes.
• Target card is attacking.
• Target card has less power than source card.

Effects

• A triggered card is placed on the stack.

with :: CardName -> (CardName -> GameMonad ()) -> GameMonad ()

Helper function to provide a scoped let.

with "Angel" $ \cn -> target cn >> destroy cn

Validations

validate :: CardMatcher -> CardName -> GameMonad ()

Validate that a card matches a matcher.

validate (matchAttribute "pirate") "Angrath's Marauders"

Validates

• Card matches matcher.

validateCanCastSorcery :: GameMonad ()

Validates that a sorcery is able to be cast.

Validates

• Stack is empty.
• In a main phase.

validateLife :: Int -> Player -> GameMonad ()

Validates a player has a specific life total.

validateLife 0 Opponent

Validates

• Player life equals amount.

validatePhase :: Phase -> GameMonad ()

Validates that the game is in a particular phase.

validatePhase BeginCombat

Validates

• Game is in the given phase.

validateRemoved :: CardName -> GameMonad ()

Validates that a card is no longer present in the game. Particularly helpful for checking destruction of tokens.

validateRemoved "Angel"

Validates

• Name does not refer to a card.

State-based Actions

Fine-grained control over when state-based actions are run. By default, all actions will runStateBasedEffects on completion, so most of the time you don't need to use these functions explicitly.

runStateBasedActions :: GameMonad ()

Run state-based actions. These include:

• If a creature does not have indestructible, and has damage exceeding toughess or deathtouched attribute, destroy it.
• If a card is a token and is not in play, remove it.
• If a card is a copy and is not on the stack, remove it.

These are run implicitly at the end of each step, so it's not usually needed to call this explicitly. Even then, using withStateBasedActions is usually preferred.

Running state-based actions can in turn trigger more state-based actions. This method loops until no more are generated, which has the potential for non-termination for pathological game states.

withStateBasedActions :: GameMonad a -> GameMonad a

Pause running of state-based actions for the duration of the action, running them at the end.

Low-level

These actions provide low-level control over the game. Where possible, try to use the more descriptive higher-level actions.

addMana :: ManaString -> GameMonad ()

Add mana to actor's mana pool.

addMana "2RG"

Validates

• Mana specification is valid.

Effects

• Mana pool is increased.

move :: CardLocation -> CardLocation -> CardName -> GameMonad ()

Move a card from one location to another.

move (Opponent, Play) (Active, Play) "Angel"

Validates

• Card exists in source location.
• Destination is not stack (use a cast variant instead).
• Destination does not match source.
• If card has token attribute, source is in play. (Removing token once they have left play is handled by runStateBasedActions.)
• If card has copy attribute, source is the stack. (Removing token once they have left play is handled by runStateBasedActions.)

Effects

• Card moved to destination location.
• If card is leaving play, remove all damage, counters, and gained attributes.
• If card has exileWhenLeaveStack attribute, move to exile and remove exileWhenLeaveStack instead.
• If card has undying, is moving from play to graveyard, and has no +1/+1 counters, add a +1/+1 counter instead. (Note: undying should move card to graveyard then back to play for owner, but since neither triggers nor owner tracking are implemented, this simplification is valid.)
• If card is entering play or changing controller, add summoned attribute.

remove :: CardName -> GameMonad ()

spendMana :: ManaString -> GameMonad ()

Remove mana from the pool. Colored mana will be removed first, then extra mana of any type will be removed to match the colorless required.

spendMana "2RG"

Validates

• Mana specification is valid.
• Sufficient mana exists in pool.

Effects

• Mana pool is reduced.

tap :: CardName -> GameMonad ()

Taps a card.

Validates

• Card is in play.
• Card is not tapped.
• If creature, is not summoned or has haste.

Effects

• Card gains tapped attribute.

untap :: CardName -> GameMonad ()

Untaps a card.

Validates

• Card is in play.
• Card is tapped.

Effects

• Card loses tapped attribute.