diff --git a/README.md b/README.md index d07ead0..d11b226 100644 --- a/README.md +++ b/README.md @@ -68,12 +68,12 @@ Obviously not fully decidable, but I might be able to implement some basic unifi ### TODO Implicits -Much, much more useful than [inference](#org21ef5f7), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. +Much, much more useful than [inference](#orgb6a8c28), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. ### TODO Universes? -Not really necessary without [inductive definitions](#org4227b35), but could be fun. +Not really necessary without [inductive definitions](#org136d92d), but could be fun. ### TODO Inductive Definitions @@ -89,10 +89,12 @@ This is definitely a stretch goal. It would be cool though, and would turn this Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [prettyprinter](https://hackage.haskell.org/package/prettyprinter) to be able to nicely handle indentation and line breaks. -### TODO Better usage +### DONE Better usage Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [haskeline](https://hackage.haskell.org/package/haskeline) to improve the repl (though `rlwrap` is fine, so not a huge priority). +For even better usage in the future, check out [optparse](https://hackage.haskell.org/package/optparse-applicative) for command line arguments and [this really cool blogpost](https://abhinavsarkar.net/posts/repling-with-haskeline/) for some haskeline magic. + ### TODO Improve error messages @@ -101,7 +103,7 @@ The error messages currently aren’t terrible, but it would be nice to have ### TODO Improve β-equivalence check -The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#org4227b35)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea. +The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#org136d92d)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea. ### DONE Better testing diff --git a/README.org b/README.org index 44cd09a..b8947c8 100644 --- a/README.org +++ b/README.org @@ -71,9 +71,11 @@ This is definitely a stretch goal. It would be cool though, and would turn this *** TODO Prettier pretty printing Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [[https://hackage.haskell.org/package/prettyprinter][prettyprinter]] to be able to nicely handle indentation and line breaks. -*** TODO Better usage +*** DONE Better usage Read input from a file if a filename is given, otherwise drop into a repl. Perhaps use something like [[https://hackage.haskell.org/package/haskeline][haskeline]] to improve the repl (though =rlwrap= is fine, so not a huge priority). +For even better usage in the future, check out [[https://hackage.haskell.org/package/optparse-applicative][optparse]] for command line arguments and [[https://abhinavsarkar.net/posts/repling-with-haskeline/][this really cool blogpost]] for some haskeline magic. + *** TODO Improve error messages The error messages currently aren't terrible, but it would be nice to have, e.g. line numbers. =megaparsec= allows for semantic errors, so somehow hook into that like what I'm doing for unbound variables? diff --git a/app/Main.hs b/app/Main.hs index c1f0c34..92531bf 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,19 +1,30 @@ module Main where import Check +import qualified Data.Text.IO as T import Expr import Parser -import qualified Data.Text.IO as T +import Repl +import System.Environment import System.IO main :: IO () main = do - _ <- T.putStr "> " - _ <- hFlush stdout - input <- T.getLine - case pAll input of - Left err -> T.putStrLn err - Right expr -> case findType [] expr of - Right ty -> T.putStrLn $ pretty expr <> " : " <> pretty ty - Left err -> print err - main + args <- getArgs + case args of + [] -> repl + [file] -> handleFile file + _ -> putStrLn "usage './perga' for repl and './perga ' to get input from a file" + +handleFile :: String -> IO () +handleFile fileName = + do + fileH <- openFile fileName ReadMode + input <- T.hGetContents fileH + case pAll input of + Left err -> putStrLn err + Right expr -> case findType [] expr of + Left err -> print err + Right ty -> do + putStrLn $ "expr:\t" ++ prettyS expr + putStrLn $ "type:\t" ++ prettyS ty diff --git a/app/Repl.hs b/app/Repl.hs new file mode 100644 index 0000000..fee1189 --- /dev/null +++ b/app/Repl.hs @@ -0,0 +1,56 @@ +module Repl (repl) where + +import Check +import qualified Data.Text as T +import Expr +import Parser +import System.Console.Haskeline +import System.Directory (createDirectoryIfMissing, getHomeDirectory) +import System.FilePath (()) + +newtype ReplState = ReplState + { debugMode :: Bool + } + +data ReplCommand = Quit | ToggleDebug | Input String deriving (Show) + +parseCommand :: Maybe String -> Maybe ReplCommand +parseCommand Nothing = Nothing +parseCommand (Just ":q") = Just Quit +parseCommand (Just ":d") = Just ToggleDebug +parseCommand (Just input) = Just (Input input) + +handleInput :: ReplState -> String -> InputT IO () +handleInput state input = case pAll (T.pack input) of + Left err -> outputStrLn err + Right expr -> case findType [] expr of + Left err -> outputStrLn $ show err + Right ty -> + if debugMode state + then printDebugInfo expr ty + else outputStrLn $ prettyS ty + +printDebugInfo :: Expr -> Expr -> InputT IO () +printDebugInfo expr ty = do + outputStrLn $ "expr\t" ++ show expr + outputStrLn $ "type\t" ++ show ty + outputStrLn $ "type\t" ++ prettyS ty + +repl :: IO () +repl = do + home <- getHomeDirectory + let basepath = home ".cache" "perga" + let filepath = basepath "history" + createDirectoryIfMissing True basepath + runInputT (defaultSettings{historyFile = Just filepath}) $ loop (ReplState False) + where + loop :: ReplState -> InputT IO () + loop state = do + minput <- getInputLine "> " + case parseCommand minput of + Nothing -> return () + Just Quit -> return () + Just ToggleDebug -> loop state{debugMode = not (debugMode state)} + Just (Input input) -> do + handleInput state input + loop state diff --git a/dependent-lambda.cabal b/dependent-lambda.cabal index fdf69fc..29901be 100644 --- a/dependent-lambda.cabal +++ b/dependent-lambda.cabal @@ -48,10 +48,14 @@ common warnings executable dependent-lambda import: warnings main-is: Main.hs + other-modules: Repl build-depends: base ^>=4.19.1.0 , dependent-lambda-lib , text + , haskeline + , directory + , filepath hs-source-dirs: app default-language: Haskell2010 default-extensions: OverloadedStrings diff --git a/lib/Parser.hs b/lib/Parser.hs index 5a6859f..c17260c 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -112,5 +112,5 @@ pAppTerm = lexeme $ pLAbs <|> pPAbs <|> pApp pExpr :: Parser Expr pExpr = lexeme $ try pArrow <|> pAppTerm -pAll :: Text -> Either Text Expr -pAll input = first (T.pack . errorBundlePretty) $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) [] +pAll :: Text -> Either String Expr +pAll input = first errorBundlePretty $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []