improved usage

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

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?
 

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 "> "
+    args <- getArgs
-    _ <- hFlush stdout
+    case args of
-    input <- T.getLine
+        [] -> repl
+        [file] -> handleFile file
+        _ -> putStrLn "usage './perga' for repl and './perga <filename>' 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 -> T.putStrLn err
+            Left err -> putStrLn err
             Right expr -> case findType [] expr of
-            Right ty -> T.putStrLn $ pretty expr <> " : " <> pretty ty
                 Left err -> print err
-    main
+                Right ty -> do
+                    putStrLn $ "expr:\t" ++ prettyS expr
+                    putStrLn $ "type:\t" ++ prettyS ty

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

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

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 :: Text -> Either String Expr
-pAll input = first (T.pack . errorBundlePretty) $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []
+pAll input = first errorBundlePretty $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) []