Istari

Reordering

A reordering allows one to to reorder the subgoals generated by a tactic, or reorder the prover’s active goals. Reorderings have the type 'a reordering, where 'a is the tactic monad’s type argument. Most reorderings are polymorphic.

signature REORDER =
   sig

      type 'a reordering

      val reorder : 'a Tactic.tacticm -> 'a reordering -> 'a Tactic.tacticm

      val id : 'a reordering
      val swap : int -> int -> 'a reordering
      val pull : int -> 'a reordering
      val push : int -> 'a reordering
      val rotateForward : int -> 'a reordering
      val rotateBackward : int -> 'a reordering
      val compose : 'a reordering list -> 'a reordering
      val withCount : (int -> 'a reordering) -> 'a reordering
      val contract : int -> 'a reordering
      val sort : ('a -> 'a -> bool) -> 'a reordering

   end

structure Reorder : REORDER

• reorder tac reord

  Uses reord to reorder the subgoals generated by tac.

  (Goals can also be reordered at the top level using Prover.reorder : Message.label Reorder.reordering -> unit.)

• swap i j

  Swaps the first i goals with the next j goals.

• pull i

  Pulls the ith goal to the front. Equivalent to swap i 1.

• push i

  Pushes the first goal to the ith position. Equivalent to swap 1 i.

• rotateForward i

  Rotates goals i positions toward the front. Equivalent to withCount (fn n => swap i (n-i)).

• rotateBackward i

  Rotates goals i positions toward the back. Equivalent to withCount (fn n => swap (n-i) i).

• compose [r1, ..., rn]

  Reorder with r1, then r2, etc.

• withCount reord

  If there are n subgoals, equivalent to reord n.

• contract n

  Contract the first n+1 goals (all of which must be identical) into a single goal.

• sort f

  Place the goals in order from least to greatest, according to the ordering given by f.

This site is open source. Improve this page.