module Main where
{- TODO:
profiling
write tests
-}
import Paths_Delta_Lambda (version)
import Control.Monad
import Control.Applicative
import Control.Monad.Except
import Control.Monad.Reader
import Data.Version
import Data.Word (Word64)
import Data.Char (isSpace, isNumber)
import Data.ByteString (writeFile, readFile)
import Data.Text (Text, pack)
import Data.Text.IO
import Prelude hiding (getContents, putStrLn)
import System.IO (Handle, IOMode (ReadMode, ReadWriteMode), withFile)
import Data.Serialize
import Options
import System.FilePath hiding ((</>))
import System.Console.Haskeline
import Text.Megaparsec (SourcePos(..))
import AST
import Reduction
import Check
import Parser
import Printer ()
data ReplOptions = ReplOptions
{ interactive :: Bool
, writeHistory :: Bool
, historyFileN :: String
, noHelpPrompt :: Bool
}
data FileOptions = FileOptions
{ usePreprocessor :: Bool
, compileToByteCode :: Bool
, saveMetadata :: Bool
, preprocessorOptions :: [String]
}
data MainOptions = MainOptions
{ inFile :: String
, echoType :: Bool
, useExtension :: [String]
, replOptions :: ReplOptions
, fileOptions :: FileOptions
}
fileGroup :: Maybe Group
fileGroup = Just $ group "file" "file commands" "commands that only affect files"
replGroup :: Maybe Group
replGroup = Just $ group "repl" "repl commands" "commands that only affect the repl"
fileAndReplGroup :: Maybe Group
fileAndReplGroup = Just $ group "file-and-repl" "file and repl commands" "commands that both the file compiler and the repl interpreter share"
instance Options ReplOptions where
defineOptions = pure ReplOptions
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["interactive"]
, optionDefault = False
, optionShortFlags = ['n']
, optionDescription = "start repl"
, optionGroup = replGroup
})
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["write-history"]
, optionDefault = True
, optionShortFlags = ['w']
, optionDescription = "enable writing to the history file"
, optionGroup = replGroup
})
<*> defineOption optionType_string (\o -> o
{ optionLongFlags = ["history-file"]
, optionDefault = "~/.delta-lambda"
, optionShortFlags = ['f']
, optionDescription = "set the history file name and location"
, optionGroup = replGroup
})
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["no-help-prompt"]
, optionDefault = False
, optionShortFlags = ['k']
, optionDescription = "dont issue help prompt on initial repl load"
, optionGroup = replGroup
})
instance Options FileOptions where
defineOptions = pure FileOptions
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["use-preprocessor"]
, optionDefault = True
, optionShortFlags = ['p']
, optionDescription = "enable the preprocessor"
, optionGroup = fileGroup
})
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["compile"]
, optionDefault = False
, optionShortFlags = ['o']
, optionDescription = "enable compilation to bytecode"
, optionGroup = fileGroup
})
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["without-metadata"]
, optionDefault = False
, optionShortFlags = ['s']
, optionDescription = "save metadata during compilation to bytecode"
, optionGroup = fileGroup
})
<*> defineOption (optionType_list ',' optionType_string) (\o -> o
{ optionLongFlags = ["preprocessor-flags"]
, optionDefault = []
, optionShortFlags = ['c']
, optionDescription = "passes the proceeding flags to the preprocessor"
, optionGroup = fileGroup
})
instance Options MainOptions where
defineOptions = pure MainOptions
<*> defineOption optionType_string (\o -> o
{ optionLongFlags = ["in-file"]
, optionDefault = "stdin"
, optionShortFlags = ['i']
, optionDescription =
"input file usable extension must be one of "
++ "(*.dl, *.cdl). note that if the \"-n\""
++ " or \"--interactive\" flags are not used"
++ " in combination with this option, the compiler"
++ " will not load the file."
, optionGroup = fileAndReplGroup
})
<*> defineOption optionType_bool (\o -> o
{ optionLongFlags = ["echo-type"]
, optionDefault = True
, optionShortFlags = ['e']
, optionDescription = "enable echoing the type of a term after checking"
, optionGroup = fileAndReplGroup
})
<*> defineOption (optionType_list ',' optionType_string) (\o -> o
{ optionLongFlags = ["use-extensions"]
, optionDefault = []
, optionShortFlags = ['x']
, optionDescription =
"enables a set of extensions"
, optionGroup = fileAndReplGroup
})
<*> defineOptions
<*> defineOptions
--version :: Version
--version = Version
-- { versionBranch = [0,3,0,0]
-- , versionTags = [] -- depreciated, but showVersion throws an exception without it
-- }
replPrompt :: Version -> String
replPrompt vers = Prelude.unlines
[ " /\\ /\\"
, " / \\ / \\"
, " / /\\ \\ / /\\ \\"
, " / /__\\ \\ / / \\ \\"
, "/________\\ /_/ \\_\\"
, "Welcome to Delta-Lambda, the 1000 line[s of haskell] theorem prover!"
, "This is apha level software! no documentation currently, and dragons galore!"
, "version: " ++ showVersion vers
]
helpPrompt :: String
helpPrompt = Prelude.unlines
[ "/-----------------------------------------------------------------------------\\"
, "| command | parameters | description |"
, "| :c | input term | check that the input term is correct |"
, "| :e | posn, term | add a term to the context at the position |"
, "| :f | input term | provide the final type of the input term |"
, "| :g | position | get the type of a term name (or position) in context |"
, "| :h | | display this table |"
, "| :o | file name | open a file and load it |"
, "| :q | | quit this repl |"
, "| :r | input term | provide the normal form of the input term |"
, "| :t | input term | provide the type of the input term |"
, "| :s | input flag | set a flag, restart the repl |"
, "| :? | | syntax and semantics tutorial (not implemented) |"
, "\\-----------------------------------------------------------------------------/"
]
data ReplState = ReplState
{ replContext :: Context SourcePos Text Word64
, replTerm :: Maybe (Term SourcePos Text Word64)
, replOpts :: MainOptions
}
-- I _*really*_ dislike the code following this comment
-- it basically is a bunch of shenanigans dealing with somewhat non-composible
-- MONADS. maybe I should just bite the bullet, and use exceptions in IO...
main :: IO ()
main = runCommand $ \opts _ ->
if interactive $ replOptions opts then
repl opts
else
if takeExtension (inFile opts) == ".dl" then
withFile (inFile opts) ReadMode $ parseCheckAndType opts
else
if takeExtension (inFile opts) == ".cdl" then
putStrLn . pack $ "cannot open binary file in non interactive mode!"
else
putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile opts)
preprocess :: MainOptions -> Text -> IO (Either String Text)
preprocess options fileContents =
if usePreprocessor $ fileOptions options then
preprocessor (preprocessorOptions $ fileOptions options) (inFile options) fileContents
else return $ Right fileContents
compile :: (Serialize m , Serialize v, Serialize i) => Term m v i -> MainOptions -> IO ()
compile val options
| not (saveMetadata $ fileOptions options) = Data.ByteString.writeFile compiledFilename (encode file)
| otherwise = Data.ByteString.writeFile compiledFilename (encode cleaned)
where header = DecompiledFileHeader
{ compiledFileName = pack $ inFile options
, interpreterVersion = version
, extensionsUsed = map pack $ useExtension options
}
file = DecompiledFile
{ decompiledFileHeader = header
, decompiledTerm = val
}
cleaned = transpile (const ()) id id file
compiledFilename = dropExtension (inFile options) -<.> ".cdl"
checkAndType :: (Enum i, Show v, BetaEq (PseudoTerm SourcePos) v i) => Term SourcePos v i -> MainOptions -> Context SourcePos v i -> IO (Maybe ())
checkAndType term options context =
case runReaderT (termCorrect term) context of
Left err -> do
putStrLn $ pack err
return Nothing
Right _
| echoType options ->
case runReaderT (typeSynth term) context of
Left err -> do
putStrLn $ pack err
return Nothing
Right val -> do
putStrLn . pack $ show val
return $ Just ()
| otherwise -> return $ Just ()
-- touch, peel, and stand anyone?
parseCheckAndType :: MainOptions -> Handle -> IO ()
parseCheckAndType options file = do
input <- Data.Text.IO.hGetContents file
input' <- preprocess options input
case input' of
Left pperr -> putStrLn $ pack pperr
Right ppval ->
case parseInput ppval of
Left perr -> putStrLn $ pack perr
Right pval -> do
checked <- checkAndType pval options []
case checked of
Nothing -> return ()
Just _ ->
when (compileToByteCode $ fileOptions options) $
compile pval options
-- halp. much blegh. very not DRY. super wet.
repl :: MainOptions -> IO ()
repl options = do
Data.Text.IO.putStr $ pack (replPrompt version)
unless (noHelpPrompt (replOptions options)) $ Data.Text.IO.putStr (pack helpPrompt)
if inFile options == "stdin" then
runInputT replSettings $ loop (initReplState Nothing options)
else
if takeExtension (inFile options) == ".dl" then
withFile (inFile options) ReadWriteMode $ \h -> do
input <- Data.Text.IO.hGetContents h
input' <- preprocess options input
case input' of
Left pperr -> putStrLn $ pack pperr
Right ppval ->
case parseInput ppval of
Left perr -> putStrLn $ pack perr
Right pval -> do
checked <- checkAndType pval options []
case checked of
Nothing -> return ()
Just _ -> runInputT replSettings $ loop (initReplState (Just pval) options)
else
if takeExtension (inFile options) == ".cdl" then do
fileCont <- Data.ByteString.readFile (inFile options)
case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
Left perr -> putStrLn $ pack perr
Right pval -> do
let fvers = interpreterVersion (decompiledFileHeader pval)
if fvers < version then
putStrLn . pack $ "cannot load file \"" ++ inFile options ++ "\n" ++
"compiler version of file: " ++ showVersion fvers ++ "\n" ++
"compiler version of system: " ++ showVersion version
else do
let val = decompiledTerm pval
runInputT replSettings $ loop (initReplState (Just val) options)
else
putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile options)
where replSettings = defaultSettings
{ historyFile = Just $ historyFileN (replOptions options)
, autoAddHistory = writeHistory (replOptions options)
}
initReplState term options = ReplState
{ replContext = []
, replTerm = term
, replOpts = options
}
-- dragons. you where warned!
loop :: ReplState -> InputT IO ()
loop state = do
let count = Prelude.length (replContext state)
input <- getInputLine $ if count == 0 then "|- " else show count ++ " |- "
case input of
Nothing -> loop state
Just (':':'c':' ':rest) ->
case parseInput (pack rest) of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
lift $ checkAndType pval (replOpts state) (replContext state)
loop state
Just (':':'e':' ':rest) -> do
let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
let termStr = dropWhile (\x -> not (isSpace x) && isNumber x) rest
if null positionStr then do
outputStrLn "please enter a non-negative number"
loop state
else do
let position :: Int = read positionStr
case parseInput $ pack termStr of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
checked <- lift $ checkAndType pval (replOpts state) (replContext state)
case checked of
Nothing -> loop state
Just _ -> do
let (before, after) = splitAt position (replContext state)
let pval' = bindContext (replContext state) 1 pval
loop (state { replContext = before ++ [pval'] ++ after })
Just (':':'f':' ':rest) ->
case parseInput (pack rest) of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
checked <- lift $ checkAndType pval (replOpts state) (replContext state)
case checked of
Nothing -> loop state
Just _ ->
case runReaderT (fTypeSynth pval) (replContext state) of
Left err -> do
outputStrLn err
loop state
Right val -> do
outputStrLn $ show val
loop state
Just (':':'g':' ':rest) -> do
let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
if null positionStr then do
outputStrLn "please enter a non-negative number"
loop state
else do
let position :: Int = read positionStr
if position > Prelude.length (replContext state) then do
outputStrLn "position of term in context cannot be outside of context"
loop state
else do
let term = replContext state !! (position - 1)
outputStrLn $ show term
loop state
Just (':':'h': _) -> do
outputStrLn helpPrompt
loop state
Just (':':'o':' ':rest)
| takeExtension rest == ".dl" -> do
loaded <- lift $ withFile rest ReadWriteMode $ \h -> do
input <- Data.Text.IO.hGetContents h
input' <- preprocess (replOpts state) input
case input' of
Left pperr -> do
putStrLn $ pack pperr
return Nothing
Right ppval ->
case parseInput ppval of
Left perr -> do
putStrLn $ pack perr
return Nothing
Right pval -> do
checked <- checkAndType pval (replOpts state) []
case checked of
Nothing -> return Nothing
Just _ -> return $ Just pval
case loaded of
Nothing -> loop state
Just val -> loop (state{ replTerm = Just val, replContext = [] })
| takeExtension rest == ".cdl" -> do
fileCont <- lift $ Data.ByteString.readFile rest
case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
let fvers = interpreterVersion (decompiledFileHeader pval)
if fvers < version then do
outputStrLn $ "cannot load file \"" ++ rest ++ "\n" ++
"compiler version of file: " ++ showVersion fvers ++ "\n" ++
"compiler version of system: " ++ showVersion version
loop state
else do
let val = decompiledTerm pval
loop (state { replTerm = Just val, replContext = [] })
| otherwise -> do
outputStrLn $ "extension not recognized: " ++ rest
loop state
Just (':':'q': _) -> return ()
Just (':':'r':' ':rest) ->
case parseInput (pack rest) of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
checked <- lift $ checkAndType pval (replOpts state) (replContext state)
case checked of
Nothing -> loop state
Just _ -> do
outputStrLn $ show . nfTerm $ pval
loop state
Just (':':'t':' ':rest) ->
case parseInput (pack rest) of
Left perr -> do
outputStrLn perr
loop state
Right pval -> do
checked <- lift $ checkAndType pval (replOpts state) (replContext state)
case checked of
Nothing -> loop state
Just _ ->
case runReaderT (typeSynth pval) (replContext state) of
Left err -> do
outputStrLn err
loop state
Right val -> do
outputStrLn $ show val
loop state
Just (':':'s':' ':rest) -> do
let pOpts = Options.parseOptions (split rest " ")
case parsedOptions pOpts of
Nothing ->
case parsedError pOpts of
Nothing -> do
outputStrLn $ "an unknow error occured during proccessing of the options: "
++ "\n" ++ rest
loop state
Just err -> do
outputStrLn err
loop state
Just opts -> loop (state {replOpts = opts})
Just (':':'?':_) -> do
outputStrLn "the turorial is under construction!"
loop state
Just input -> do
outputStrLn $ "input : " ++ input ++ "\n not recognised"
loop state
split :: String -> String -> [String]
split str pat = helper str pat [] [] where
helper :: String -> String -> String -> String -> [String]
helper [] _ n _ = [n]
helper xs [] n _ = n : split xs pat
helper (x:xs) (y:ys) n m
| x /= y = helper xs pat ((n++m)++[x]) m
| otherwise = helper xs ys n (m++[y])