pisigma-0.1.0.1: src/PiSigma.hs

{-# LANGUAGE ScopedTypeVariables #-}

module Main where

import Prelude hiding (catch)
import System.IO
import System.Environment
import System.Console.Haskeline hiding (catch)
import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Exception
import Data.List
import Data.Char
   
import PiSigma.Syntax
import PiSigma.Evaluation
import PiSigma.Check
import PiSigma.Print
import PiSigma.Nf
import PiSigma.Equality
import PiSigma.Parser

main :: IO ()
main = 
  do
    args <- getArgs
    let ini = mapM_ (handleCommand . Load) args
    liftM fst $ runStateT (runInputT 
                            (setComplete pisigmaCompletion defaultSettings)
                            (ini >> repl))
                          initialReplState

-- | Completion in PiSigma. For the moment, we use file name completion
-- while in a load command, and identifier completion everywhere else.
pisigmaCompletion :: CompletionFunc (StateT ReplState IO)
pisigmaCompletion (x1,x2)
  | ":l" `isPrefixOf` reverse x1 = completeFilename (x1,x2)
  | otherwise                    = completeWord Nothing " " identifier (x1,x2)
  where
    identifier x = do
                     (Scope sc,env) <- gets replState
                     let names = map fst sc
                         xr    = reverse x
                         cands = filter (x `isPrefixOf`) names
                     return $ map simpleCompletion (sort cands)

type Repl = InputT (StateT ReplState IO)
type Continue = Bool

data ReplState =
  ReplState
    { replState :: (Scope, EnvEntries)
    , replFiles :: [FilePath]
    }

data ReplCommand =
    Load String
  | Reload
  | Quit
  | EvalPhrase Phrase
  | Noop
  | Clear
  | Equal (Term,Term)
  | TypeOf Term
  | Help

-- TODO:
-- browse current identifiers

-- | Preliminary interpreter help message.
help :: String
help =
    unlines $
    [ "PiSigma currently supports the following commands:",
      "",
      "  :l         load a source file",
      "  :r         reload current source file",
      "  :c         clear the environment",
      "  :t         ask for the type of a term",
      "  :e         test two terms for beta equality",
      "  :q         quit",
      "",
      "Type a declaration or an expression to evaluate it." ]

initialReplState :: ReplState
initialReplState = 
  ReplState (emptyScope, emptyE) []

replStep :: Repl Continue
replStep =
  do
    f <- lift $ gets replFiles
    x <- getInputLine (unwords (reverse f) ++ "> ")
    c <- interpretInput x
    handleCommand c

-- | Preliminary input interpretation, based on the
-- current parser and no particular intelligence in
-- parsing commands correctly.
interpretInput :: Maybe String -> Repl ReplCommand
interpretInput Nothing  = return Quit
interpretInput (Just x)
  | ":l" `isPrefixOf` x = case break (== ' ') x of
                            (x1,x2) -> return (Load (norm (trim x2)))
  | ":r" `isPrefixOf` x = return Reload
  | ":q" `isPrefixOf` x = return Quit
  | ":c" `isPrefixOf` x = return Clear
  | ":e" `isPrefixOf` x = case break (== ' ') x of
                            (x1,x2) -> parseInputInteractive s2Terms Equal x2
  | ":t" `isPrefixOf` x = case break (== ' ') x of
                            (x1,x2) -> parseInputInteractive sTerm TypeOf x2
  | ":h" `isPrefixOf` x || ":?" `isPrefixOf` x
                        = return Help
  | ":"  `isPrefixOf` x = replMessage "unknown command" >> return Noop
  | otherwise           = parseInputInteractive sPhrase EvalPhrase x

-- | Turn a string into a Repl command.
parseInput :: String -> SParser t -> (t -> ReplCommand) ->
              String -> Repl ReplCommand
parseInput f p cmd s =
    case parse p f s of
      Left s     -> do
                      liftIO $ putStrLn ("Parse error: " ++ show s ++ "\n")
                      return Noop
      Right p    -> return (cmd p)

parseInputInteractive = parseInput "<interactive>"

-- | Placeholder for a message function that can depend
-- on verbosity settings.
replMessage :: String -> Repl ()
replMessage = liftIO . putStrLn

-- | Command handler. Returns a flag indicating whether
-- the interpreter should continue.
handleCommand :: ReplCommand -> Repl Continue
handleCommand c =
  case c of
    Help ->
      do
        replMessage $ help
        return True
    Load f ->
      do
        fs <- lift $ gets replFiles
        if f `elem` fs then do
            replMessage $ "Skipping " ++ f ++ "."
            return True
          else do
            mx <- liftIO $ catch (liftM Just (readFile f))
                                 (\ (_ :: IOException) -> return Nothing)
            case mx of
              Nothing -> do
                replMessage $ "Could not find " ++ f ++ "."
                return True
              Just x -> do
                -- Allow source files to have interpreter commands at the top;
                -- we currently use this as a replacement for a module system
                let (cmds,rest) = span (":" `isPrefixOf`) (lines x)
                mapM_ (\ c -> interpretInput (Just c) >>= handleCommand) cmds
                -- We print the "Loaded" message after executing initial
                -- interpreter commands in order to reflect the dependency
                -- order of different source files.
                replMessage $ "Loaded " ++ f ++ "."
                p <- parseInput f sProg (EvalPhrase . Prog)
                                (unlines (replicate (length cmds) "" ++ rest))
                lift $ modify (\ s -> s { replFiles =
                                            case replFiles s of
                                             (g : fs) | g == f -> g : fs
                                             xs                -> f : xs })
                handleCommand p
    Reload ->
      do
        f <- lift $ gets replFiles
        handleCommand Clear
        mapM_ (handleCommand . Load) (reverse f)
        return True
    Quit ->
      return False
    EvalPhrase (Prog p) ->
      do
        execProg p
        return True
    EvalPhrase (Term t) ->
      do
        execTerm t
        return True
    Equal (t1,t2) ->
      do
        eqTerms t1 t2
        return True
    TypeOf t ->
      do
        inferTerm t
        return True
    Clear ->
      do
        lift $ put initialReplState
        return True
    Noop ->
      return True

execProg :: Prog -> Repl ()
execProg p =
  do
    s <- lift get
    let (con,env) = replState s
    case run env (checkProg (p,con)) of
      Right s' -> lift $ put (s { replState = s' })
      Left e   -> liftIO $ putStrLn e

execTerm :: Term -> Repl ()
execTerm t =
  do
    s <- lift get
    let (con,env) = replState s
        p = do
          a <- infer (t,con)
          pa <- prt a
          t' <- nf [] (t,con)
          pt <- prt t'
          return (pt++"\n: "++pa)
    case run env p of
        Right (m,_) -> liftIO $ putStrLn m
        Left  e     -> liftIO $ putStrLn e

eqTerms :: Term -> Term -> Repl ()
eqTerms t1 t2 =
  do
    s <- lift get
    let (con,env) = replState s
        p = eq (t1,con) (t2,con)
    case run env p of
        Right _ -> liftIO $ putStrLn "yes"
        Left  e -> liftIO $ putStrLn e
    

inferTerm :: Term -> Repl ()
inferTerm t =
  do
    s <- lift get
    let (con,env) = replState s
        p = infer (t,con) >>= prt
    case run env p of
        Right (m,_) -> liftIO $ putStrLn m
        Left  e     -> liftIO $ putStrLn e

-- | Run the interpreter as long as desired.
repl :: Repl ()
repl =
  do
    continue <- replStep
    when continue repl

-- * Helper functions

trim :: String -> String
trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

norm :: String -> String
norm []          = []
norm ('\\':c:xs) = c : norm xs
norm (x:xs)      = x : norm xs