{-|
Module:      SMT2Lib.SExprProcess
Description: Create a process that communicates via S-expressions
Copyright:   (c) 2016 The MITRE Corporation
License:     BSD

The 'SExprProcess' type and its associated operations.
-}

{-# LANGUAGE CPP #-}

-- Uncomment the following if you want to see what is being sent to Z3.
-- When defined, a log of the S-expressions will be written to z3.smt2.

-- #define LOGGING

-- Copyright (c) 2016 The MITRE Corporation
--
-- This program is free software: you can redistribute it and/or
-- modify it under the terms of the BSD License as published by the
-- University of California.

module SMT2Lib.SExprProcess (SExprProcess, createSExprProcess,
                             call, wait) where

import System.IO
import System.Exit (ExitCode)
import System.Process
import CPSA.Lib.SExpr

-- | A process that communicates via S-expressions.
data SExprProcess
  = SExprProcess { to :: Handle,
                   from :: PosHandle,
#if defined LOGGING
                   logger :: Handle,
#endif
                   xproc :: ProcessHandle }

-- | Create a process by invoking a program with a list of arguments.
-- The process is connected to the current process using pipes for
-- input and output.  S-expressions are used to send data along the
-- pipes.
createSExprProcess :: FilePath -> [String] -> IO SExprProcess
createSExprProcess prog args =
  do
    (Just to, Just from, _, xproc) <-
      createProcess (proc prog args){ std_in = CreatePipe,
                                      std_out = CreatePipe }
    from <- posHandle "" from
#if defined LOGGING
    log <- openFile "z3.smt2" WriteMode
#endif
    return $ SExprProcess { to = to,
                            from = from,
#if defined LOGGING
                            logger = log,
#endif
                            xproc = xproc }

-- | Send an S-expression and wait for one in reply.
call :: SExprProcess -> SExpr a -> IO (SExpr Pos)
call sp x =
  do
#if defined LOGGING
    writeSExpr (logger sp) x
#endif
    writeSExpr (to sp) x
    mx <- load (from sp)
    case mx of
      Just x -> return x
      Nothing -> fail "SExprProcess.callSExpr: EOF when reading"

-- Send an S-expression
writeSExpr :: Handle -> SExpr a -> IO ()
writeSExpr h x =
  do
    putSExpr h x
    hPutChar h '\n'
    hFlush h

-- Write an S-expression
putSExpr :: Handle -> SExpr a -> IO ()
putSExpr h (S _ s) = hPutStr h s
putSExpr h (Q _ s) = hPutStr h (showQuoted s "")
putSExpr h (N _ n) = hPutStr h (show n)
putSExpr h (L _ []) = hPutStr h "()"
putSExpr h (L _ (x:xs)) =
  do
    hPutChar h '('
    putSExpr h x
    mapM_ putSpSExpr xs
    hPutChar h ')'
  where
    putSpSExpr x =
      do
        hPutChar h ' '
        putSExpr h x

-- | Wait for the child process to exit.  Use this to collect timing
-- data about the child.
wait :: SExprProcess -> IO ExitCode
wait sp = waitForProcess $ xproc sp