ControlFlow.CBlock

Definitions

MbPhis : (List lbl -> Type) -> Neighbors lbl -> Type

  Constructs the type of the phi assignment list of a `CBlock` based on its
  predecessors (`ins`).
  
  * For an undefined list of predecessors (`Nothing`), the "list" is of the
  unit type, as the phi assignments are impossible to construct in such case.
  
  * For a defined list of predecessors (`Just ins`), the list is an actual
  list of phi assignemtns, whose "inputs" coincide with the inputs
  (predecessors) of the block.
  
  @ lbl the type of vertex identifiers / block labels
  @ phi the type that represents a phi assignment,
        parametrized by its input labels
  @ ins the predecessors of the block

Visibility: public export

MbTerm : (List lbl -> Type) -> Neighbors lbl -> Type

  Constructs the type of the terminating instruction of a `CBlock` based on
  its successors (`outs`)
  
  * For an undefined list of successors (`Nothing`), the terminator is of the
  unit type, as it is impossible to determine its type in such case.
  
  * For a defined list of successors (`Just outs`), the terminator an a ctual
  terminating instruction, whose "outputs" concide with the
  outputs (successors) of the block.
  
  @ lbl the type of vertex identifiers / block labels
  @ term the type that represents the terminating instruction,
         parametrized by its output labels
  @ outs the succcessors of the block

Visibility: public export

record CBlock : (List l -> Type) -> Type -> (List l -> Type) -> l -> Neighbors l -> Neighbors l -> Type

  A potentially incomplete basic block.
  
  @ l     the type of vertex identifiers / block labels
  @ phi   the type that represents a phi assignment,
          parametrized by its input labels
  @ instr the type that represents the simple (non-terminating,
          non-phi-assignments)) instructions that the block consists of
  @ term  the type that represents the terminating instruction,
          parametrized by its output labels
  @ lbl   the label of the block (its identifier)
  @ ins   the potentially undefined list of the predecessors of the block
  @ outs  the potentially undefined list of the successors of the block

Totality: total
Visibility: public export
Constructor: 

MkBB : Singleton lbl -> MbPhis phi ins -> List instr -> MbTerm terminator outs -> CBlock phi instr terminator lbl ins outs

  Make a potentially incomplete basic block

Projections:

.body : CBlock phi instr terminator lbl ins outs -> List instr

  The body of the block, i.e. the instructions it consists of.

.phis : CBlock phi instr terminator lbl ins outs -> MbPhis phi ins

  The potentially undefined list of phi assignments of the block

.term : CBlock phi instr terminator lbl ins outs -> MbTerm terminator outs

  The potentially undefined instruction that terminates the block

.theLabel : CBlock phi instr terminator lbl ins outs -> Singleton lbl

  the runtime manifestation of the label (the identifier) of the block.
  
  Wrapped in the `Singleton` type constructor to avoid shadowing the type
  parameter by the field or vice versa.

Hint: 

Connectable (CBlock phi instr terminator)

.theLabel : CBlock phi instr terminator lbl ins outs -> Singleton lbl

  the runtime manifestation of the label (the identifier) of the block.
  
  Wrapped in the `Singleton` type constructor to avoid shadowing the type
  parameter by the field or vice versa.

Visibility: public export

theLabel : CBlock phi instr terminator lbl ins outs -> Singleton lbl

  the runtime manifestation of the label (the identifier) of the block.
  
  Wrapped in the `Singleton` type constructor to avoid shadowing the type
  parameter by the field or vice versa.

Visibility: public export

.phis : CBlock phi instr terminator lbl ins outs -> MbPhis phi ins

  The potentially undefined list of phi assignments of the block

Visibility: public export

phis : CBlock phi instr terminator lbl ins outs -> MbPhis phi ins

  The potentially undefined list of phi assignments of the block

Visibility: public export

.body : CBlock phi instr terminator lbl ins outs -> List instr

  The body of the block, i.e. the instructions it consists of.

Visibility: public export

body : CBlock phi instr terminator lbl ins outs -> List instr

  The body of the block, i.e. the instructions it consists of.

Visibility: public export

.term : CBlock phi instr terminator lbl ins outs -> MbTerm terminator outs

  The potentially undefined instruction that terminates the block

Visibility: public export

term : CBlock phi instr terminator lbl ins outs -> MbTerm terminator outs

  The potentially undefined instruction that terminates the block

Visibility: public export

emptyCBlock : CBlock phi instr trm lbl Nothing Nothing

  Create `CBlock` that has no instructions
  @ lbl the block label

Visibility: export

(++) : CBlock phi instr terminator lbl ins Nothing -> CBlock phi instr terminator lbl Nothing outs -> CBlock phi instr terminator lbl ins outs

  Concatenates two blocks
  Appends a postfix with undefine inputs to a prefix with undefined outputs.
  @ pre  the prefix
  @ post the postfix

Visibility: export
Fixity Declaration: infixr operator, level 7

(<++) : CBlock phi instr trm lbl ins Nothing -> List instr -> CBlock phi instr trm lbl ins Nothing

  Append a list of simple instructions to the block
  Leaves the type signature of the block unchanged
  @ pre  the block        (the prefix)
  @ post the instructions (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 7

(<+) : CBlock phi instr trm lbl ins Nothing -> instr -> CBlock phi instr trm lbl ins Nothing

  Append a single simple instruction to the block
  Leaves the type signature of the block unchanged
  @ pre  the block       (the prefix)
  @ post the instruction (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 7

(<+|) : CBlock phi instr trm lbl ins Nothing -> trm outs -> CBlock phi instr trm lbl ins (Just outs)

  Defines the outputs of a block by appending to it a terminating
  insrtruction
  @ pre  the block      (the prefix)
  @ post the terminator (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 6

(|++>) : List (phi inputs) -> CBlock phi instr trm lbl Nothing outs -> CBlock phi instr trm lbl (Just inputs) outs

  Defines the inputs of a block by prepending to it a list of phi assignemts
  @ pre  the phi assignments (the prefix)
  @ post the block           (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 6

(|+>) : phi inputs -> CBlock phi instr trm lbl Nothing outs -> CBlock phi instr trm lbl (Just inputs) outs

  Defines the inputs of a block by prepending to it a single phi assignemt
  @ pre  the phi assignment (the prefix)
  @ post the block          (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 6

(+|) : phi inputs -> CBlock phi instr trm lbl (Just inputs) outs -> CBlock phi instr trm lbl (Just inputs) outs

  Prepends a phi assignment to a block with already defined inputs
  @ pre  the phi assignment (the prefix)
  @ post the block          (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 5

(++|) : List (phi inputs) -> CBlock phi instr trm lbl (Just inputs) outs -> CBlock phi instr trm lbl (Just inputs) outs

  Prepends a list of phi assignments to a block with already defined inputs
  @ pre  the phi assignments (the prefix)
  @ post the block           (the postfix)

Visibility: export
Fixity Declaration: infixr operator, level 5

emptyCFG : CFG (CBlock phi instr terminatorrt) (Undefined lbl) (Undefined lbl)

  Make a graph that consists of a single empty block
  @ lbl the label of the block

Visibility: export