module Main( main ) where
{- TODO:
profiling
write tests
-}
--import Paths_Delta-Lambda (version)
import Data.Char (isSpace, isNumber)
import System.FilePath hiding ((</>))
import Control.Applicative
import Control.Monad.Except
import Control.Monad.Reader
import Control.Parallel
import Data.ByteString (writeFile, readFile)
import Data.Text (Text, pack, unpack, length)
import Data.Text.Encoding
import Data.Text.IO
import Data.Version
import Data.Word (Word64)
import GHC.Generics
import Prelude hiding (getContents, putStrLn)
import System.IO (Handle, IOMode (ReadMode, ReadWriteMode), withFile)
import Text.Megaparsec hiding (space)
import qualified Text.Megaparsec.Lexer as Lexer
import Text.Megaparsec.Text
import Options
import Text.PrettyPrint.Leijen hiding ((<$>))
import Language.Preprocessor.Cpphs
import System.Console.Haskeline
import Data.Serialize
-- represent a term with variable name type v, and variable binding index type i
-- that has metadata m associated to each node and leaf
data Term m v i = Variable v i m
| Abstraction v m (Term m v i) (Term m v i)
| Application m (Term m v i) (Term m v i)
| Type m
deriving (Generic)
data Kind m v i = Function v m (Term m v i) (Kind m v i)
| Kind m
deriving (Generic)
data DecompiledFileHeader = DecompiledFileHeader
{ compiledFileName :: Text
, interpreterVersion :: Version
, extensionsUsed :: [Text]
}
data DecompiledFile m v i = DecompiledFile
{ decompiledFileHeader :: DecompiledFileHeader
, decompiledTerm :: Term m v i
}
instance (Serialize m, Serialize v, Serialize i) => Serialize (Term m v i) where
instance (Serialize m, Serialize v, Serialize i) => Serialize (Kind m v i) where
-- some orphan instances
instance Serialize Version where
put = \vers -> putListOf (put :: Putter Int) (versionBranch vers)
get = do
branchList :: [Int] <- getListOf get
return Version { versionBranch = branchList
, versionTags = []
}
instance Serialize Text where
put = \text' -> do
putWord64le (fromIntegral (Data.Text.length text') :: Word64)
put (encodeUtf8 text')
get = do
leng <- getWord64le
bs <- getByteString (fromIntegral leng :: Int)
return (decodeUtf8 bs)
instance Serialize SourcePos where
put = \srcPos -> do
put (sourceName srcPos)
put (sourceLine srcPos)
put (sourceColumn srcPos)
get = do str :: String <- get
pos1 :: Pos <- get
pos2 :: Pos <- get
return $ SourcePos str pos1 pos2
instance Serialize Pos where
put = \pos -> putWord64le (fromIntegral (unPos pos) :: Word64)
get = getWord64le >>= return . unsafePos . fromIntegral
instance Serialize DecompiledFileHeader where
put = \decompHeader -> do
put (compiledFileName decompHeader)
put (interpreterVersion decompHeader)
put (extensionsUsed decompHeader)
get = do
fname :: Text <- get
iversion :: Version <- get
xtensions :: [Text] <- get
return DecompiledFileHeader
{ compiledFileName = fname
, interpreterVersion = iversion
, extensionsUsed = xtensions
}
instance (Serialize m, Serialize v, Serialize i) => Serialize (DecompiledFile m v i) where
put = \decomp -> do
put (decompiledFileHeader decomp)
put (decompiledTerm decomp)
get = do
fileHeader :: DecompiledFileHeader <- get
fileBody :: Term m v i <- get
return DecompiledFile
{ decompiledFileHeader = fileHeader
, decompiledTerm = fileBody
}
transpile :: (m -> m') -> (v -> v') -> (i -> i') -> DecompiledFile m v i -> DecompiledFile m' v' i'
transpile fm fv fi decompFile@DecompiledFile{ decompiledTerm = fileBody } =
let transpile' t = case t of
Type m -> Type (fm m)
Variable v i m -> Variable (fv v) (fi i) (fm m)
Application m a f ->
Application (fm m) (transpile' a) (transpile' f)
Abstraction v m t b ->
Abstraction (fv v) (fm m) (transpile' t) (transpile' b)
in decompFile { decompiledTerm = transpile' fileBody }
bindTerm :: (Eq v, Eq i, Enum i) => v -> i -> Term m v i -> Term m v i
bindTerm variable index subject = case subject of
Type metadata -> Type metadata
Application metadata argument function ->
Application metadata (bindTerm variable index argument) (bindTerm variable index function)
Abstraction variable' metadata parameter body ->
Abstraction variable' metadata (bindTerm variable index parameter)
(bindTerm variable (succ index) body)
Variable variable' index' metadata
| variable == variable' && index' == toEnum 0 -> Variable variable' index metadata
| otherwise -> subject
bindContext :: (Eq i, Enum i, Show i) => [Term m Text i] -> i -> Term m Text i -> Term m Text i
bindContext context index term = case context of
[] -> term
_:rest -> bindContext rest (succ index) (bindTerm (pack ("$" ++ show index)) index term)
updateTerm :: (Ord i, Enum i) => i -> i -> Term m v i -> Term m v i
updateTerm i k subject = case subject of
Type metadata -> Type metadata
Application metadata argument function ->
Application metadata (updateTerm i k argument) (updateTerm i k function)
Abstraction variable metadata parameter body ->
Abstraction variable metadata (updateTerm i k parameter) (updateTerm i (succ k) body)
Variable variable index metadata
| index > k -> Variable variable (toEnum $ fromEnum index + fromEnum i - 1) metadata
| otherwise -> subject
substituteTerm :: (Ord i, Enum i) => i -> Term m v i -> Term m v i -> Term m v i
substituteTerm index replacement' subject =
case subject of
Type metadata -> Type metadata
Application metadata argument function ->
Application metadata (substituteTerm index replacement' argument)
(substituteTerm index replacement' function)
Abstraction variable metadata parameter body ->
Abstraction variable metadata (substituteTerm index replacement' parameter)
(substituteTerm (succ index) replacement' body)
Variable variable index' metadata
| index' > index -> Variable variable (pred index') metadata
| index' == index -> updateTerm index (toEnum 0) replacement'
| index' < index -> subject
substituteKind :: (Ord i, Enum i) => i -> Term m v i -> Kind m v i -> Kind m v i
substituteKind index replacement' subject = case subject of
Kind metadata -> Kind metadata
Function variable metadata parameter body ->
Function variable metadata (substituteTerm index replacement' parameter)
(substituteKind (succ index) replacement' body)
whnf :: (Ord i, Enum i) => Term m v i -> Term m v i
whnf reduct =
case reduct of
Application metadata argument function ->
case whnf function of
Abstraction _ _ _ body ->
whnf $ substituteTerm (toEnum 1) argument body
f@_ -> Application metadata argument f
reduct'@_ -> reduct'
nfTerm :: (Enum i, Ord i) => Term m v i -> Term m v i
nfTerm reduct =
case reduct of
Abstraction variable metadata parameter body ->
let parameter' = nfTerm parameter
body' = parameter' `par` nfTerm body
in Abstraction variable metadata parameter' body'
Application metadata argument function ->
case whnf function of
Abstraction _ _ _ body ->
let arg = nfTerm argument
bod = arg `seq` substituteTerm (toEnum 1) arg (nfTerm body)
in nfTerm bod
f@_ -> Application metadata (nfTerm argument) (nfTerm f)
_ -> reduct
nfKind :: (Enum i, Ord i) => Kind m v i -> Kind m v i
nfKind reduct =
case reduct of
Kind metadata -> Kind metadata
Function variable metadata parameter body ->
let param = nfTerm parameter
body' = param `par` nfKind body
in Function variable metadata param body'
instance (Enum i, Ord i, Eq v) => Eq (Term m v i) where
Type _ == Type _ = True
Variable variable index _ == Variable variable' index' _ = variable == variable' && index == index'
Application _ argument function == Application _ argument' function' =
let ftest = function == function'
atest = ftest `par` argument == argument'
in ftest && atest
Abstraction variable metadata parameter body == Abstraction _ _ parameter' body' =
let ptest = parameter == parameter'
var = Variable variable (toEnum 1) metadata
btest = ptest `par` body == substituteTerm (toEnum 1) var body'
in ptest && btest
_ == _ = False
instance (Enum i, Ord i, Eq v, Eq i) => Eq (Kind m v i) where
Kind _ == Kind _ = True
Function variable metadata parameter body == Function _ _ parameter' body' =
let ptest = parameter == parameter'
var = Variable variable (toEnum 1) metadata
btest = ptest `par` body == substituteKind (toEnum 1) var body'
in ptest && btest
_ == _ = False
infix 4 ===
class (Enum i, Ord i, Eq i, Eq v) => BetaEq t v i where
(===) :: (Enum i, Ord i, Eq i, Eq v) => t v i -> t v i -> Bool
instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (Term m) v i where
a === b = nfTerm a == nfTerm b
instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (Kind m) v i where
a === b = nfKind a == nfKind b
instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (PseudoTerm m) v i where
Term a === Term b = nfTerm a == nfTerm b
Kind' a === Kind' b = nfKind a == nfKind b
_ === _ = False
data PseudoTerm m v i = Term (Term m v i)
| Kind' (Kind m v i)
type Context m v i = [Term m v i]
type Judgement m v i a = ReaderT (Context m v i) (Either String) a
typeSynth :: (Show v, Enum i) => Term SourcePos v i -> Judgement SourcePos v i (PseudoTerm SourcePos v i)
typeSynth term' =
case term' of
Type metadata -> return $ Kind' (Kind metadata)
Variable variable index position -> do
context <- ask
if Prelude.length context <= fromEnum index - 1 then
throwError $ "invalid variable encountered during type synthesis: "
++ show variable ++ "\nat " ++ show position
else return $ Term $ context !! (fromEnum index - 1)
Application position argument function -> do
function' <- typeSynth function
case function' of
Term f -> return $ Term $ Application position argument f
Kind' _ -> throwError $ "invalid kind constructed during type synthesis"
++ "\nat " ++ show position
Abstraction variable position parameter body -> do
body' <- local (parameter:) (typeSynth body)
case body' of
Term b -> return $ Term $ Abstraction variable position parameter b
Kind' b -> return $ Kind' $ Function variable position parameter b
fTypeSynth :: (Show v, Enum i) => Term SourcePos v i -> Judgement SourcePos v i (PseudoTerm SourcePos v i)
fTypeSynth t = do
typ <- typeSynth t
case typ of
Term t' -> fTypeSynth t'
Kind' _ -> return typ
termCorrect :: (Enum i, Show v, BetaEq (PseudoTerm SourcePos) v i) => Term SourcePos v i -> Judgement SourcePos v i ()
termCorrect t = case t of
Type _ -> return ()
Variable{} ->
void (typeSynth t)
Abstraction _ _ parameter body -> do
termCorrect parameter
local (parameter:) (termCorrect body)
Application pos argument function -> do
argType <- typeSynth argument
termCorrect argument
Term funType <- fTypeSynth function
case nfTerm funType of
Abstraction _ _ parameter body ->
if Term parameter === argType then
termCorrect (nfTerm $ substituteTerm (toEnum 1) argument body)
else
let argPosition = show $ getNodeMetadata (Term argument)
parPosition = show $ getNodeMetadata (Term parameter)
in throwError $ "argument type and function parameter do not match: \n"
++ "at " ++ argPosition ++ " with argument type of: " ++ show argType ++ "\n"
++ "at " ++ parPosition ++ " with parameter value of: " ++ show parameter ++ "\n"
e@_ -> throwError $ "attempted application onto non function type at "
++ show pos ++ "\nwith type: " ++ show e
lineComment, blockComment, spaceToken :: Parser ()
lineComment = Lexer.skipLineComment "--" <|> Lexer.skipLineComment "#"
blockComment = Lexer.skipBlockComment "{-" "-}"
spaceToken = Lexer.space (void spaceChar) lineComment blockComment
lexeme :: Parser a -> Parser a
lexeme = Lexer.lexeme spaceToken
symbol :: String -> Parser String
symbol = Lexer.symbol spaceToken
variableToken :: Parser Text
variableToken = lexeme =<<
return . pack <$> ((:) <$> (letterChar <|> Text.Megaparsec.char '$') <*> many alphaNumChar)
commaToken, colonToken, typeToken :: Parser ()
commaToken = void (symbol ",")
colonToken = void (symbol ":")
typeToken = void (symbol "type")
parensToken, bracketsToken :: Parser a -> Parser a
parensToken = between (symbol "(") (symbol ")")
bracketsToken = between (symbol "[") (symbol "]")
vector :: Parser [Term SourcePos Text Word64]
vector = sepBy1 term commaToken
telescope :: Parser [([(Text, SourcePos)], Term SourcePos Text Word64)]
telescope = sepBy1 ((,) <$> sepBy ((,) <$> variableToken <*> getPosition) spaceToken <*> (colonToken >> term)) commaToken
term :: Parser (Term SourcePos Text Word64)
term = (Type <$> (typeToken >> getPosition) <?> "type")
<|> try (Variable <$> variableToken <*> return 0 <*> getPosition <?> "variable")
<|> (apply <$> parensToken vector <*> term <?> "application")
<|> (funct <$> bracketsToken telescope <*> term <?> "abstraction")
apply :: [Term SourcePos v i] -> Term SourcePos v i -> Term SourcePos v i
apply = flip $ foldl (\f a -> Application (getNodeMetadata (Term a)) a f)
funct :: [([(Text, SourcePos)], Term SourcePos Text Word64)] -> Term SourcePos Text Word64 -> Term SourcePos Text Word64
funct = flip $ foldr $ \(ns, typ) bod -> foldr (\(n, p) -> Abstraction n p typ . bindTerm n 1) bod ns
parseString :: String -> Text -> Either String (Term SourcePos Text Word64)
parseString filename' input = case parse term filename' input of
Left err -> Left $ show err
Right val -> Right val
parseInput :: Text -> Either String (Term SourcePos Text Word64)
parseInput = parseString "stdin"
getNodeMetadata :: PseudoTerm m v i -> m
getNodeMetadata node = case node of
Term term' -> case term' of
Type metadata -> metadata
Variable _ _ metadata -> metadata
Abstraction _ metadata _ _ -> metadata
Application metadata _ _ -> metadata
Kind' kind -> case kind of
Kind metadata -> metadata
Function _ metadata _ _ -> metadata
prettyKind :: Show v => Kind m v i -> Doc
prettyKind kind = case kind of
Kind _ -> text "kind"
Function variable _ parameter body ->
let (args, bod) = collectAbstr [(variable, parameter)] body
argsDoc = list $ fmap (\(n, t) -> text (show n) <> colon <+> prettyTerm t) args
funDoc = argsDoc `par` prettyKind bod
collectAbstr args' (Function v _ t b) = collectAbstr (args' ++ [(v, t)]) b
collectAbstr args' fun = (args', fun)
in argsDoc </> funDoc
prettyTerm :: Show v => Term m v i -> Doc
prettyTerm term' = case term' of
Type _ -> text "type"
Variable variable _ _ -> text $ show variable
Application _ arg fun ->
let (args, fun') = collectApply [arg] fun
argsDoc = tupled $ map prettyTerm args
funDoc = argsDoc `par` prettyTerm fun'
collectApply args' (Application _ arg' fun'') = collectApply (args' ++ [arg']) fun''
collectApply args' fun'' = (args', fun'')
in argsDoc </> funDoc
Abstraction var _ typ bod ->
let (args, bod') = collectAbstr [(var, typ)] bod
argsDoc = list $ fmap (\(n, t) -> text (show n) <> colon <+> prettyTerm t) args
funDoc = argsDoc `par` prettyTerm bod'
collectAbstr args' (Abstraction v _ t b) = collectAbstr (args' ++ [(v, t)]) b
collectAbstr args' fun = (args', fun)
in argsDoc </> funDoc
instance Show v => Show (Term m v i) where
showsPrec _ term' = displayS $ renderPretty 0.4 100 $ prettyTerm term'
instance Show v => Show (Kind m v i) where
showsPrec _ kind = displayS $ renderPretty 0.4 100 $ prettyKind kind
instance (Show v) => Show (PseudoTerm m v i) where
show p = case p of
Term t -> show t
Kind' k -> show k
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 $ Options.group "file" "file commands" "commands that only affect files"
replGroup :: Maybe Group
replGroup = Just $ Options.group "repl" "repl commands" "commands that only affect the repl"
fileAndReplGroup :: Maybe Group
fileAndReplGroup = Just $ Options.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,1,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
}
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
case Language.Preprocessor.Cpphs.parseOptions (preprocessorOptions $ fileOptions options) of
Left err -> return $ Left err
Right cpphsOpts -> do
fileContents' <- runCpphs cpphsOpts (inFile options) (unpack fileContents)
return $ Right $ pack 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 -> do
return $ Just ()
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 _ ->
if compileToByteCode $ fileOptions options then
compile pval options
else
return ()
repl :: MainOptions -> IO ()
repl options = do
Data.Text.IO.putStr $ pack (replPrompt version)
when (not (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 do
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
}
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) -> do
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) -> do
if takeExtension rest == ".dl" then 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 = [] })
else
if takeExtension rest == ".cdl" then 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 = [] })
else 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 -> do
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])