Types

Basic datatypes.

Basic types.

type Binder = String

Program binders (i.e. top-level identifiers) are identified by their name.

data NoCustomEvent

Our Brick TUI does not use any custom events.

data Name

The type of resource names, used throughout the TUI.

Constructors

LeftViewport

RightViewport

viewports

FormField String

form fields

SearchResult Int

search results with numbered occurrences

Other

Instances

Eq Name

Defined in Types

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name

Defined in Types

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Show Name

Defined in Types

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

MonadFail (EventM Name)

Allow pattern matches in EventM monadic do blocks.

Defined in BrickUI

Methods

fail :: String -> EventM Name a

type Cursor = CursorLocation Name

Type of cursors in our TUI.

data Command

Commands that the user can issue through the input form.

Constructors

Step Int

move to given step in the current binder

Trans String

move to the next/previous transformation with the given name

Search String

move to the next/previous occurrence of the searched string

Instances

Eq Command

Defined in Types

Methods

(==) :: Command -> Command -> Bool

(/=) :: Command -> Command -> Bool

Ord Command

Defined in Types

Methods

compare :: Command -> Command -> Ordering

(<) :: Command -> Command -> Bool

(<=) :: Command -> Command -> Bool

(>) :: Command -> Command -> Bool

(>=) :: Command -> Command -> Bool

max :: Command -> Command -> Command

min :: Command -> Command -> Command

Show Command

Defined in Types

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

data OptionsUI term

Options kept and changed throught the TUI's input form.

Constructors

OptionsUI

Fields

• _opts :: Options term

  options for the pretty-printer

• _com :: Command

  command to issue (search string, etc...)

opts :: forall term term. Lens (OptionsUI term) (OptionsUI term) (Options term) (Options term)

com :: forall term. Lens' (OptionsUI term) Command

data VizState term

Bottom-level state of the UI (navigate steps of a top-level binder).

Constructors

VizState

Fields

• _steps :: History term (Ctx term)

  steps of the rewriting process

• _prevState :: Maybe (VizState term)

  previous state (initially Nothing)

• _curExpr :: term

  current (intermediate) expression

• _curStep :: Int

  current step in given top-level entity

• _curOccur :: Int

  current occurrence we are highlighting

• _leftN :: Int

  # of occurrences in the left viewport

• _rightN :: Int

  # of occurrences in the right viewport

steps :: forall term. Lens' (VizState term) (History term (Ctx term))

rightN :: forall term. Lens' (VizState term) Int

prevState :: forall term. Lens' (VizState term) (Maybe (VizState term))

leftN :: forall term. Lens' (VizState term) Int

curStep :: forall term. Lens' (VizState term) Int

curOccur :: forall term. Lens' (VizState term) Int

curExpr :: forall term. Lens' (VizState term) term

data VizStates term

Top-level state of the UI (navigate top-level binders).

Constructors

VizStates

Fields

• _binders :: [Binder]

  all top-level binders

• _curBinder :: Binder

  currently selected binder

• _states :: Map Binder (VizState term)

  state of each binder

• _form :: Form (OptionsUI term) NoCustomEvent Name

  input form for setting parameters

• _showBot :: Bool

  whether to hide bottom pane

• _width :: Int

  current terminal width

• _height :: Int

  current terminal height

• _scroll :: Bool

  whether to scroll to focused region

width :: forall term. Lens' (VizStates term) Int

states :: forall term. Lens' (VizStates term) (Map Binder (VizState term))

showBot :: forall term. Lens' (VizStates term) Bool

scroll :: forall term. Lens' (VizStates term) Bool

height :: forall term. Lens' (VizStates term) Int

form :: forall term. Lens' (VizStates term) (Form (OptionsUI term) NoCustomEvent Name)

curBinder :: forall term. Lens' (VizStates term) Binder

binders :: forall term. Lens' (VizStates term) [Binder]

Getters and setters.

mkForm :: forall term. Diff term => OptionsUI term -> Form (OptionsUI term) NoCustomEvent Name

Create the input form.

createVizStates :: forall term. Diff term => History term (Ctx term) -> VizStates term

Group the rewrite history by the different top-level binders.

initialState :: Diff term => History term (Ctx term) -> VizState term

State initialization for the bottom layer.

currentStepName :: VizState term -> String

Get the name of the current transformation.

getStep :: VizStates term -> Binder -> (Int, Int, String)

Get information about the current step.

getCurrentState :: VizStates term -> VizState term

Get the current state of the bottom layer.

getSearchString :: Diff term => VizStates term -> String

Get the current string we are searching for. NB: Returns the empty string of no search command has been issued.

formData :: forall term. Diff term => Lens' (VizStates term) (OptionsUI term)

Lens from the global state to the input form's data.

updateState :: VizStates term -> VizState term -> VizStates term

Update the local state of the current binder.

getCodeWidth :: VizStates term -> Int

Get the available code width for one of the two code panes.

stepBinder :: VizStates term -> VizStates term

Cycle through top-level binders in the global state.

stepBinder

Proceed forward.

unstepBinder

Proceed backward.

unstepBinder :: VizStates term -> VizStates term

Cycle through top-level binders in the global state.

stepBinder

Proceed forward.

unstepBinder

Proceed backward.

step :: Diff term => VizState term -> VizState term

Cycle through transformations of the current binder in the local state.

step

Proceed forward.

unstep

Proceed backward.

reset

Reset to the initial state.

unstep :: Diff term => VizState term -> VizState term

Cycle through transformations of the current binder in the local state.

step

Proceed forward.

unstep

Proceed backward.

reset

Reset to the initial state.

reset :: Diff term => VizState term -> VizState term

Cycle through transformations of the current binder in the local state.

step

Proceed forward.

unstep

Proceed backward.

reset

Reset to the initial state.

User-issued commands.

data Direction

Some user commands have a notion of direction; either going forth or back.

Constructors

Forward

Backward

moveTo :: Diff term => Int -> VizState term -> VizState term

Move to a specified step of the transformations of the current binder.

nextTrans :: Diff term => Direction -> String -> VizState term -> VizState term

Move to the next/previous step with the given transformation name.

nextOccur :: Diff term => Direction -> VizState term -> VizState term

Cycle through search occurrences.