Skip to content

Latest commit

 

History

History
649 lines (388 loc) · 8.14 KB

COMMANDS.md

File metadata and controls

649 lines (388 loc) · 8.14 KB
Raw

Wingman Metaprogram Command Reference

application

arguments: none.
non-deterministic.

Apply any function in the hypothesis that returns the correct type.

Example

Given:

f :: a -> b

_ :: b

running application will produce:

f (_ :: a)

apply

arguments: single reference.
deterministic.

Apply the given function from local scope.

Example

Given:

f :: a -> b

_ :: b

running apply f will produce:

f (_ :: a)

assume

arguments: single reference.
deterministic.

Use the given term from the hypothesis, unifying it with the current goal

Example

Given:

some_a_val :: a

_ :: a

running assume some_a_val will produce:

some_a_val

assumption

arguments: none.
non-deterministic.

Use any term in the hypothesis that can unify with the current goal.

Example

Given:

some_a_val :: a

_ :: a

running assumption will produce:

some_a_val

auto

arguments: none.
non-deterministic.

Repeatedly attempt to split, destruct, apply functions, and recurse in an attempt to fill the hole.

Example

Given:

f :: a -> b
g :: b -> c

_ :: a -> c

running auto will produce:

g . f

binary

arguments: none.
deterministic.

Produce a hole for a two-parameter function, as well as holes for its arguments. The argument holes have the same type but are otherwise unconstrained, and will be solved before the function.

Example

In the example below, the variable a is free, and will unify to the resulting extract from any subsequent tactic.

Given:

_ :: Int

running binary will produce:

(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)

cata

arguments: single reference.
deterministic.

Destruct the given term, recursing on every resulting binding.

Example

Assume we're called in the context of a function f.

Given:

x :: (a, a)

_

running cata x will produce:

case x of
  (a1, a2) ->
    let a1_c = f a1
        a2_c = f a2
     in _

collapse

arguments: none.
deterministic.

Collapse every term in scope with the same type as the goal.

Example

Given:

a1 :: a
a2 :: a
a3 :: a

_ :: a

running collapse will produce:

(_ :: a -> a -> a -> a) a1 a2 a3

ctor

arguments: single reference.
deterministic.

Use the given data cosntructor.

Example

Given:

_ :: Maybe a

running ctor Just will produce:

Just (_ :: a)

destruct

arguments: single reference.
deterministic.

Pattern match on the argument.

Example

Given:

a :: Bool

_

running destruct a will produce:

case a of
  False -> _
  True -> _

destruct_all

arguments: none.
deterministic.

Pattern match on every function paramater, in original binding order.

Example

Assume a and b were bound via f a b = _.

Given:

a :: Bool
b :: Maybe Int

_

running destruct_all will produce:

case a of
  False -> case b of
    Nothing -> _
    Just i -> _
  True -> case b of
    Nothing -> _
    Just i -> _

homo

arguments: single reference.
deterministic.

Pattern match on the argument, and fill the resulting hole in with the same data constructor.

Example

Only applicable when the type constructor of the argument is the same as that of the hole.

Given:

e :: Either a b

_ :: Either x y

running homo e will produce:

case e of
  Left a -> Left (_ :: x)
  Right b -> Right (_ :: y)

intro

arguments: single binding.
deterministic.

Construct a lambda expression, binding an argument with the given name.

Example

Given:

_ :: a -> b -> c -> d

running intro aye will produce:

\aye -> (_ :: b -> c -> d)

intros

arguments: varadic binding.
deterministic.

Construct a lambda expression, using the specific names if given, generating unique names otherwise. When no arguments are given, all of the function arguments will be bound; otherwise, this tactic will bind only enough to saturate the given names. Extra names are ignored.

Example

Given:

_ :: a -> b -> c -> d

running intros will produce:

\a b c -> (_ :: d)

Example

Given:

_ :: a -> b -> c -> d

running intros aye will produce:

\aye -> (_ :: b -> c -> d)

Example

Given:

_ :: a -> b -> c -> d

running intros x y z w will produce:

\x y z -> (_ :: d)

let

arguments: varadic binding.
deterministic.

Create let-bindings for each binder given to this tactic.

Example

Given:

_ :: x

running let a b c will produce:

let a = _1 :: a
    b = _2 :: b
    c = _3 :: c
 in (_4 :: x)

nested

arguments: single reference.
non-deterministic.

Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need with_arg to use this tactic in a saturated context.

Example

Given:

_ :: [(Int, Either Bool a)] -> [(Int, Either Bool b)]

running nested fmap will produce:

fmap (fmap (fmap _))

obvious

arguments: none.
non-deterministic.

Produce a nullary data constructor for the current goal.

Example

Given:

_ :: [a]

running obvious will produce:

[]

pointwise

arguments: tactic.
deterministic.

Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings.

Example

In the context of f (a1, b1) (a2, b2) = _. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.

Given:

_

running pointwise (use mappend) will produce:

mappend _ _

recursion

arguments: none.
deterministic.

Fill the current hole with a call to the defining function.

Example

In the context of foo (a :: Int) (b :: b) = _:

Given:

_

running recursion will produce:

foo (_ :: Int) (_ :: b)

sorry

arguments: none.
deterministic.

"Solve" the goal by leaving a hole.

Example

Given:

_ :: b

running sorry will produce:

_ :: b

split

arguments: none.
non-deterministic.

Produce a data constructor for the current goal.

Example

Given:

_ :: Either a b

running split will produce:

Right (_ :: b)

try

arguments: tactic.
non-deterministic.

Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states.

Example

Given:

f :: a -> b

_ :: b

running try (apply f) will produce:

-- BOTH of:

f (_ :: a)

-- and

_ :: b

unary

arguments: none.
deterministic.

Produce a hole for a single-parameter function, as well as a hole for its argument. The argument holes are completely unconstrained, and will be solved before the function.

Example

In the example below, the variable a is free, and will unify to the resulting extract from any subsequent tactic.

Given:

_ :: Int

running unary will produce:

(_2 :: a -> Int) (_1 :: a)

use

arguments: single reference.
deterministic.

Apply the given function from module scope.

Example

import Data.Char (isSpace)

Given:

_ :: Bool

running use isSpace will produce:

isSpace (_ :: Char)

with_arg

arguments: none.
deterministic.

Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context.

Example

Where a is a new unifiable type variable.

Given:

_ :: r

running with_arg will produce:

(_2 :: a -> r) (_1 :: a)