Script which loads a given file into Agda and prints the normalised form of a given expression.

agda2_compute_toplevel.hs

module agda2_compute_toplevel where

import Control.Concurrent (forkIO)
import Data.List (isPrefixOf)
import System.Environment (getEnv)
import System.FilePath (splitSearchPath)
import System.IO
import System.Process
import Text.Printf (printf)


nf_prefix = "(agda2-info-action \"*Normal Form*\" "
nf_suffix = " nil)"

nf :: String -> String
nf = read . reverse . drop (length nf_suffix) . reverse . drop (length nf_prefix)


agda_path :: IO [FilePath]
agda_path = splitSearchPath <$> getEnv "AGDA_PATH"


cmd_load :: FilePath -> [String] -> String
cmd_load file path = printf "IOTCM %s NonInteractive Indirect ( Cmd_load %s %s )"
                (show file) (show file) (show path)


cmd_compute_toplevel :: FilePath -> String -> String
cmd_compute_toplevel file expr
  =  printf "IOTCM %s None Indirect ( Cmd_compute_toplevel False %s )"
     (show file) (show expr)


compute_toplevel :: FilePath -> [String] -> IO ()
compute_toplevel file exprs = do
  (hin,hout,herr,_) <- runInteractiveCommand "agda --interaction"

  hSetBinaryMode hin  False
  hSetBinaryMode hout False
  hSetBinaryMode herr False
  hSetBuffering  hin  LineBuffering
  hSetBuffering  hout NoBuffering
  hSetBuffering  herr NoBuffering

  agda_path' <- agda_path

  hPutStrLn hin (cmd_load file agda_path')
  sequence_ (hPutStrLn hin . cmd_compute_toplevel file <$> exprs)
  resp <- hGetContents hout

  let nfs = map nf (filter (nf_prefix `isPrefixOf`) (lines resp))
  mapM_ putStrLn nfs