report unused definitions

FindUnusedDefinitions.idr

module Main

import Control.App
import Control.App.Console
import Data.SortedSet

data Op = Add | Sub | Mul | Div

data Expr
  = Var String
  | I Int
  | Bin Op Expr Expr

data Stmt
  = Def String Expr
  | E Expr

v : String -> Expr
v = Var

export
Prog : Type
Prog = List Stmt

data UsedVars : Type where

walk : Has [State UsedVars (SortedSet String)] es => Expr -> App es ()
walk (Var n) = put UsedVars $ insert n !(get UsedVars)
walk (Bin _ l r) = walk l *> walk r
walk (I _) = pure ()

check : Has [State UsedVars (SortedSet String)] es => Prog -> App es (SortedSet String)
check Nil = pure empty
check (E e :: ss) = walk e *> check ss
check (Def n e :: ss) = do
  if contains n !(get UsedVars)
    then check ss
    else do
      walk e
      pure $ insert n $ !(check ss)

topCheck : Prog -> IO ()
topCheck prog = do
  m <- run (new empty (check (reverse prog)))
  putStrLn $ show m

prog : Prog
prog = [
  Def "a" (I 1), -- unused
  Def "b" (I 2),
  Def "c" (I 3),
  E $ Bin Add (v "b") (v "c")
  ]
main : IO ()
main = topCheck prog