{- |
Module      :  ./Maude/Shellout.hs
Description :  Maude Development Graphs
Copyright   :  (c) Adrian Riesco, Facultad de Informatica UCM 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ariesco@fdi.ucm.es
Stability   :  experimental
Portability :  portable

-}

module Maude.Shellout (
    runMaude,
    basicAnalysis,
    findSpec,
    getAllSpec,
    getErrors,
    maudePutStrLn
) where

import System.FilePath
import System.IO
import System.Process
import System.Timeout

import Maude.AS_Maude

import Maude.Sign (Sign, inlineSign)
import Maude.Sentence (Sentence)
import qualified Maude.Sign as Sign
import qualified Maude.Sentence as Sen

import Data.List (isPrefixOf)

import Common.Doc
import Common.DocUtils ()
import Common.Utils

import qualified Control.Monad.Fail as Fail

maudePath :: String
maudePath :: String
maudePath = "maude"
maudeArgs :: [String]
maudeArgs :: [String]
maudeArgs = ["-interactive", "-no-banner", "-no-advise"]
maudeHetsPath :: String
maudeHetsPath :: String
maudeHetsPath = "hets.prj"

-- | runs @maude@ in an interactive subprocess
runMaude :: IO (String, Handle, Handle, Handle, ProcessHandle)
runMaude :: IO (String, Handle, Handle, Handle, ProcessHandle)
runMaude = do
  String
ml <- String -> String -> IO String
getEnvDef "MAUDE_LIB" ""
  String
hml <- String -> String -> IO String
getEnvDef "HETS_MAUDE_LIB" "Maude"
  if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
ml then String -> IO (String, Handle, Handle, Handle, ProcessHandle)
forall a. HasCallStack => String -> a
error "environment variable MAUDE_LIB is not set" else do
    (hIn :: Handle
hIn, hOut :: Handle
hOut, hErr :: Handle
hErr, procH :: ProcessHandle
procH) <-
        String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess String
maudePath [String]
maudeArgs Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing
    (String, Handle, Handle, Handle, ProcessHandle)
-> IO (String, Handle, Handle, Handle, ProcessHandle)
forall (m :: * -> *) a. Monad m => a -> m a
return ("in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hml String -> String -> String
</> String
maudeHetsPath, Handle
hIn, Handle
hOut, Handle
hErr, ProcessHandle
procH)

maudePutStrLn :: Handle -> String -> IO ()
maudePutStrLn :: Handle -> String -> IO ()
maudePutStrLn hIn :: Handle
hIn str :: String
str = do
  Handle -> String -> IO ()
hPutStrLn Handle
hIn String
str
  Handle -> IO ()
hFlush Handle
hIn

{- | performs the basic analysis, extracting the signature and the sentences
of the given Maude text, that can use the signature accumulated thus far. -}
basicAnalysis :: Sign -> MaudeText -> IO (Sign, [Sentence])
basicAnalysis :: Sign -> MaudeText -> IO (Sign, [Sentence])
basicAnalysis sign :: Sign
sign (MaudeText mt :: String
mt) = do
    (inString :: String
inString, hIn :: Handle
hIn, hOut :: Handle
hOut, _, _) <- IO (String, Handle, Handle, Handle, ProcessHandle)
runMaude
    Handle -> String -> IO ()
maudePutStrLn Handle
hIn String
inString
    let sigStr :: String
sigStr = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens
          (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [String -> Doc
text "mod FROM-HETS is", Sign -> Doc
inlineSign Sign
sign, String -> Doc
text String
mt
                 , String -> Doc
text "endm"]
    Handle -> String -> IO ()
maudePutStrLn Handle
hIn String
sigStr
    String
specOut <- Handle -> IO String
hGetContents Handle
hOut
    Handle -> IO ()
hClose Handle
hIn
    let spStr :: String
spStr = String -> String
findSpec String
specOut
    case String -> Maybe Spec
forall a. Read a => String -> Maybe a
readMaybe String
spStr of
      Just sp :: Spec
sp -> (Sign, [Sentence]) -> IO (Sign, [Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign, [Sentence]) -> IO (Sign, [Sentence]))
-> (Sign, [Sentence]) -> IO (Sign, [Sentence])
forall a b. (a -> b) -> a -> b
$ Spec -> (Sign, [Sentence])
convertSpec Spec
sp
      Nothing ->
          String -> IO (Sign, [Sentence])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO (Sign, [Sentence]))
-> String -> IO (Sign, [Sentence])
forall a b. (a -> b) -> a -> b
$ "cannot interpret the following maude output:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
spStr
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\ncreated for:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sigStr
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nmaude return:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
specOut

-- | extracts the signature and the sentences from a specification
convertSpec :: Spec -> (Sign, [Sentence])
convertSpec :: Spec -> (Sign, [Sentence])
convertSpec (SpecMod spec :: Module
spec) = (Module -> Sign
Sign.fromSpec Module
spec, Module -> [Sentence]
Sen.fromSpec Module
spec)
convertSpec _ = (Sign
Sign.empty, [])

-- | extracts the string corresponding to a specification
findSpec :: String -> String
findSpec :: String -> String
findSpec = let
        findSpecBeg :: [String] -> [String]
findSpecBeg = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((String -> Bool) -> [String] -> [String])
-> (String -> Bool) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Spec"
        findSpecEnd :: [String] -> [String]
findSpecEnd = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((String -> Bool) -> [String] -> [String])
-> (String -> Bool) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "@#$endHetsSpec$#@"
        filterNil :: String -> String
filterNil = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter ((Char -> Bool) -> String -> String)
-> (Char -> Bool) -> String -> String
forall a b. (a -> b) -> a -> b
$ Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
(/=) '\NUL'
    in String -> String
filterNil (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
findSpecEnd ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
findSpecBeg ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines

-- | extracts the Haskell representation of a Maude module or view
getAllSpec :: Handle -> String -> Bool -> IO String
getAllSpec :: Handle -> String -> Bool -> IO String
getAllSpec hOut :: Handle
hOut s :: String
s False = do
    Bool
ready <- Handle -> Int -> IO Bool
hWaitForInput Handle
hOut 2000
    if Bool
ready
        then do  -- 5 secs per line
            Maybe String
ms <- Int -> IO String -> IO (Maybe String)
forall a. Int -> IO a -> IO (Maybe a)
timeout 5000000 (IO String -> IO (Maybe String)) -> IO String -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
hOut
            case Maybe String
ms of
              Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s
              Just ss :: String
ss -> Handle -> String -> Bool -> IO String
getAllSpec Handle
hOut (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ss) (String -> Bool
finalSpec String
ss)
        else do
            String
handle <- Handle -> IO String
hShow Handle
hOut
            String -> IO String
forall a. HasCallStack => String -> a
error (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "No spec available on handle: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
handle
getAllSpec _ s :: String
s True = String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
s

getErrors :: Handle -> IO (Bool, String)
getErrors :: Handle -> IO (Bool, String)
getErrors hErr :: Handle
hErr = do
  String
ss <- Handle -> IO String
hGetContents Handle
hErr
  (Bool, String) -> IO (Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
ss, String
ss)

-- | end of the Haskell representation of a Maude module or view
finalSpec :: String -> Bool
finalSpec :: String -> Bool
finalSpec "@#$endHetsSpec$#@" = Bool
True
finalSpec _ = Bool
False