build CFG for program

BuildCFG.idr

module Main

data Expr = E

data Stmt
  = If Expr Stmt Stmt -- if (condition) then A else B
  -- loop (condition):
  --   do xxx
  | Loop Expr Stmt
  | SE String

Prog : Type
Prog = List Stmt

data CFG
  = From Stmt (List CFG)
  | Node Stmt

Cast Prog CFG where
  cast p = go (\deps => SE "end" `From` deps) $ reverse p
  where
    go : (List CFG -> CFG) -> Prog -> CFG
    go c [] = c []
    go c (If _ a b :: prog) =
      go (\deps => c [a `From` deps, b `From` deps]) prog
    go c (Loop _ b :: prog) =
      go (\deps => c [b `From` (Node b :: deps)]) prog
    go c (s :: prog) =
      go (\deps => c [(s `From` deps)]) prog

cfg : CFG
cfg = cast [SE "start", Loop E (SE "loop"), SE "before if", If E (SE "a") (SE "b"), SE "final"]

main : IO ()
main = pure ()