Dovin.V1

Documentation

module Dovin.Dump

addMana :: ManaString -> GameMonad ()

Add mana to actor's mana pool.

addMana "2RG"

Validates

• Mana specification is valid.

Effects

• Mana pool is increased.

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.

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.

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.

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.

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.

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.

damage

Arguments

:: (Card -> Int)

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

-> Target

-> CardName

-> 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.

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 cardStrength (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.

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

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.

Effects

• Card gains tapped attribute.

untap :: CardName -> GameMonad ()

Untaps a card.

Validates

• Card is in play.
• Card is tapped.

Effects

• Card loses tapped attribute.

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.

validatePhase :: Phase -> GameMonad ()

Validates that the game is in a particular phase.

validatePhase BeginCombat

Validates

• Game is in the given phase.

validateCanCastSorcery :: GameMonad ()

Validates that a sorcery is able to be cast.

Validates

• Stack is empty.
• In a main phase.

withStateBasedActions :: GameMonad () -> GameMonad ()

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

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.

step :: String -> GameMonad () -> GameMonad ()

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.

module Dovin.Attributes

addCard :: CardName -> GameMonad ()

addAura :: CardName -> GameMonad ()

addArtifact :: CardName -> GameMonad ()

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

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

addEnchantment :: CardName -> GameMonad ()

addInstant :: CardName -> GameMonad ()

addLand :: CardName -> GameMonad ()

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

addSorcery :: CardName -> GameMonad ()

as :: Player -> GameMonad () -> GameMonad ()

Perform action as the specified player.

withAttribute :: String -> GameMonad () -> GameMonad ()

Add an attribute to the created card, as identified by a string. Attributes with that special meaning to Dovin built-ins (such as flying) are defined in Dovin.Attributes.

withAttributes :: [String] -> GameMonad () -> GameMonad ()

Helper version of withAttribute for adding multiple attributes at a time.

withEffect

Arguments

:: CardMatcher

A matcher that must apply to this card for this affect to apply. matchInPlay is a typical value.

-> (Card -> CardMatcher)

Given the current card, return a matcher that matches cards that this affect applies to.

-> (Card -> GameMonad Card)

Apply an effect to the given card.

-> GameMonad ()

-> GameMonad ()

Add an effect to the created card.

withPlusOneCounters :: Int -> GameMonad () -> GameMonad ()

Set the number of +1/+1 counters of the created card.

module Dovin.Formatting

module Dovin.Helpers

module Dovin.Types

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

Validate that a card matches a matcher.

validate "Angrath's Marauders" $ matchAttribute "pirate"

Validates

• Card matches matcher.

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

Validates a player has a specific life total.

validateLife Opponent 0

Validates

• Player life equals amount.

withLocation :: CardLocation -> GameMonad () -> GameMonad ()

Set the location of the created card.

activate :: ManaString -> CardName -> ExceptT String (ReaderT Env (StateT Board (WriterT [(String, Board)] Identity))) ()

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