
   0 | module ControlFlow.CBlock
   1 | 
   2 | import Data.Singleton
   3 | 
   4 | import ControlFlow.CFG
   5 | 
   6 | ||| Constructs the type of the phi assignment list of a `CBlock` based on its
   7 | ||| predecessors (`ins`).
   8 | |||
   9 | ||| * For an undefined list of predecessors (`Nothing`), the "list" is of the
  10 | ||| unit type, as the phi assignments are impossible to construct in such case.
  11 | |||
  12 | ||| * For a defined list of predecessors (`Just ins`), the list is an actual
  13 | ||| list of phi assignemtns, whose "inputs" coincide with the inputs
  14 | ||| (predecessors) of the block.
  15 | |||
  16 | ||| @ lbl the type of vertex identifiers / block labels
  17 | ||| @ phi the type that represents a phi assignment,
  18 | |||       parametrized by its input labels
  19 | ||| @ ins the predecessors of the block
  20 | public export
  21 | MbPhis : (phi : List lbl -> Type) -> (ins : Neighbors lbl) -> Type
  22 | MbPhis phi Nothing = ()
  23 | MbPhis phi (Just ins) = List (phi ins)
  24 | 
  25 | ||| Constructs the type of the terminating instruction of a `CBlock` based on
  26 | ||| its successors (`outs`)
  27 | |||
  28 | ||| * For an undefined list of successors (`Nothing`), the terminator is of the
  29 | ||| unit type, as it is impossible to determine its type in such case.
  30 | |||
  31 | ||| * For a defined list of successors (`Just outs`), the terminator an a ctual
  32 | ||| terminating instruction, whose "outputs" concide with the
  33 | ||| outputs (successors) of the block.
  34 | |||
  35 | ||| @ lbl the type of vertex identifiers / block labels
  36 | ||| @ term the type that represents the terminating instruction,
  37 | |||        parametrized by its output labels
  38 | ||| @ outs the succcessors of the block
  39 | public export
  40 | MbTerm : (term : List lbl -> Type) -> (outs : Neighbors lbl) -> Type
  41 | MbTerm term Nothing = ()
  42 | MbTerm term (Just outs) = term outs
  43 | 
  44 | ||| A potentially incomplete basic block.
  45 | |||
  46 | ||| @ l     the type of vertex identifiers / block labels
  47 | ||| @ phi   the type that represents a phi assignment,
  48 | |||         parametrized by its input labels
  49 | ||| @ instr the type that represents the simple (non-terminating,
  50 | |||         non-phi-assignments)) instructions that the block consists of
  51 | ||| @ term  the type that represents the terminating instruction,
  52 | |||         parametrized by its output labels
  53 | ||| @ lbl   the label of the block (its identifier)
  54 | ||| @ ins   the potentially undefined list of the predecessors of the block
  55 | ||| @ outs  the potentially undefined list of the successors of the block
  56 | public export
  57 | record CBlock
  58 |   (phi        : List l -> Type)
  59 |   (instr      : Type)
  60 |   (terminator : List l -> Type)
  61 |   (lbl        : l)
  62 |   (ins        : Neighbors l)
  63 |   (outs       : Neighbors l)
  64 |   where
  65 | 
  66 |   ||| Make a potentially incomplete basic block
  67 |   constructor MkBB
  68 | 
  69 |   ||| the runtime manifestation of the label (the identifier) of the block.
  70 |   |||
  71 |   ||| Wrapped in the `Singleton` type constructor to avoid shadowing the type
  72 |   ||| parameter by the field or vice versa.
  73 |   theLabel : Singleton lbl
  74 | 
  75 |   ||| The potentially undefined list of phi assignments of the block
  76 |   phis : MbPhis phi ins
  77 | 
  78 |   ||| The body of the block, i.e. the instructions it consists of.
  79 |   body : List instr
  80 | 
  81 |   ||| The potentially undefined instruction that terminates the block
  82 |   term : MbTerm terminator outs
  83 | 
  84 | -- TODO why implicit?
  85 | ||| Create `CBlock` that has no instructions
  86 | ||| @ lbl the block label
  87 | export
  88 | emptyCBlock : {lbl : l} -> CBlock phi instr trm lbl Nothing Nothing
  89 | emptyCBlock {lbl} = MkBB { theLabel = Val lbl, phis = (), body = [], term = () }
  90 | 
  91 | 
  92 | 
  93 | 
  94 | export infixr 7 <++, <+
  95 | export infixr 6 <+|, |+>, |++>
  96 | export infixr 5 +|, ++|
  97 | 
  98 | ||| Concatenates two blocks
  99 | ||| Appends a postfix with undefine inputs to a prefix with undefined outputs.
 100 | ||| @ pre  the prefix
 101 | ||| @ post the postfix
 102 | export
 103 | (++)
 104 |    : (pre  : CBlock phi instr terminator lbl ins     Nothing)
 105 |   -> (post : CBlock phi instr terminator lbl Nothing outs)
 106 |   ->         CBlock phi instr terminator lbl ins     outs
 107 | (++)
 108 |   ( MkBB
 109 |     { theLabel
 110 |     , phis
 111 |     , body
 112 |     , term = ()
 113 |     }
 114 |   )
 115 |   ( MkBB
 116 |     { theLabel = theLabel'
 117 |     , phis = ()
 118 |     , body = body'
 119 |     , term = term'
 120 |     }
 121 |   )
 122 |   = MkBB
 123 |     { theLabel
 124 |     , phis
 125 |     , body = (body ++ body')
 126 |     , term = term'
 127 |     }
 128 | 
 129 | ||| Append a list of simple instructions to the block
 130 | ||| Leaves the type signature of the block unchanged
 131 | ||| @ pre  the block        (the prefix)
 132 | ||| @ post the instructions (the postfix)
 133 | export
 134 | (<++)
 135 |    : (pre  : CBlock phi instr trm lbl ins Nothing)
 136 |   -> (post : List instr)
 137 |   ->         CBlock phi instr trm lbl ins Nothing
 138 | (MkBB { theLabel, phis , body , term = () }) <++ instrs
 139 |   = MkBB { theLabel, phis, body = (body ++ instrs), term = () }
 140 | 
 141 | ||| Append a single simple instruction to the block
 142 | ||| Leaves the type signature of the block unchanged
 143 | ||| @ pre  the block       (the prefix)
 144 | ||| @ post the instruction (the postfix)
 145 | export
 146 | (<+)
 147 |    : (pre  : CBlock phi instr trm lbl ins Nothing)
 148 |   -> (post : instr)
 149 |   ->         CBlock phi instr trm lbl ins Nothing
 150 | blk <+ instr = blk <++ [instr]
 151 | 
 152 | ||| Defines the outputs of a block by appending to it a terminating
 153 | ||| insrtruction
 154 | ||| @ pre  the block      (the prefix)
 155 | ||| @ post the terminator (the postfix)
 156 | export
 157 | (<+|)
 158 |    : (pre  : CBlock phi instr trm lbl ins Nothing)
 159 |   -> (post : trm                                outs)
 160 |   ->         CBlock phi instr trm lbl ins (Just outs)
 161 | MkBB { theLabel, phis, body, term = () } <+| term = MkBB { theLabel, phis, body, term }
 162 | 
 163 | ||| Defines the inputs of a block by prepending to it a list of phi assignemts
 164 | ||| @ pre  the phi assignments (the prefix)
 165 | ||| @ post the block           (the postfix)
 166 | export
 167 | (|++>)
 168 |    : (pre  : List (phi                      inputs))
 169 |   -> (post : CBlock phi instr trm lbl Nothing       outs)
 170 |   ->         CBlock phi instr trm lbl (Just inputs) outs
 171 | phis |++> MkBB { theLabel, phis = (), body, term }
 172 |         = MkBB { theLabel, phis,      body, term }
 173 | 
 174 | ||| Defines the inputs of a block by prepending to it a single phi assignemt
 175 | ||| @ pre  the phi assignment (the prefix)
 176 | ||| @ post the block          (the postfix)
 177 | export
 178 | (|+>)
 179 |    : (pre  : phi                            inputs)
 180 |   -> (post : CBlock phi instr trm lbl Nothing       outs)
 181 |   ->         CBlock phi instr trm lbl (Just inputs) outs
 182 | instr |+> blk = [instr] |++> blk
 183 | 
 184 | ||| Prepends a phi assignment to a block with already defined inputs
 185 | ||| @ pre  the phi assignment (the prefix)
 186 | ||| @ post the block          (the postfix)
 187 | export
 188 | (+|)
 189 |    : (pre  : phi                            inputs)
 190 |   -> (post : CBlock phi instr trm lbl (Just inputs) outs)
 191 |   ->         CBlock phi instr trm lbl (Just inputs) outs
 192 | instr +| MkBB { theLabel, phis, body, term }
 193 |   = MkBB { theLabel, phis = instr :: phis, body, term }
 194 | 
 195 | ||| Prepends a list of phi assignments to a block with already defined inputs
 196 | ||| @ pre  the phi assignments (the prefix)
 197 | ||| @ post the block           (the postfix)
 198 | export
 199 | (++|)
 200 |    : (pre  : List (phi                      inputs))
 201 |   -> (post : CBlock phi instr trm lbl (Just inputs) outs)
 202 |   ->         CBlock phi instr trm lbl (Just inputs) outs
 203 | phis ++| blk = foldl (flip (+|)) blk phis
 204 | 
 205 | export
 206 | implementation Connectable (CBlock phi instr terminator) where
 207 |   cnct = (++)
 208 | 
 209 | -- TODO why implicit?
 210 | ||| Make a graph that consists of a single empty block
 211 | ||| @ lbl the label of the block
 212 | export
 213 | emptyCFG : {lbl : l} -> CFG (CBlock phi instr terminatorrt) (Undefined lbl) (Undefined lbl)
 214 | emptyCFG = initGraph emptyCBlock
 215 |