Do a lot.

- Add type aliases.
- Make `suc` a symbol.
- Fix incorrect specification for `IsFunction`.
- Write parser for terms.
- Use `collie` to improve command line experience.

1 files changed, 163 insertions, 20 deletions

diff --git a/src/Inky.idr b/src/Inky.idr
index 5c7a821..bd3975f 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -1,13 +1,18 @@
 module Inky
 
+import Collie
 import Control.App
 import Control.App.Console
 import Control.App.FileIO
 import Inky.Context
 import Inky.Parser
+import Inky.Term
 import Inky.Term.Parser
+import Inky.Term.Pretty
+import Inky.Thinning
 import Inky.Type
 import Inky.Type.Pretty
+import System.File.Mode
 import System.File.ReadWrite
 import System.File.Virtual
 import Text.Lexer
@@ -16,6 +21,10 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default partial
 
+%hide Collie.Modifiers.infix.(::=)
+
+-- Actions ---------------------------------------------------------------------
+
 lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
 lexInkyString file = do
   let (tokens, _, _, "") = lex tokenMap file
@@ -31,37 +40,171 @@ parseType toks = do
     | Left msg => throw msg
   pure a
 
+parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (CheckTerm [<] [<])
+parseTerm toks = do
+  let Ok res [] _ = parse @{EqI} OpenCheck toks
+    | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
+    | Err msg => throw msg
+  let Right t = res.try [<] [<]
+    | Left msg => throw msg
+  pure t
+
 checkType : HasErr String es => Ty [<] () -> App es ()
 checkType a = do
   let False = illFormed a
     | True => throw "type ill-formed"
   pure ()
 
+checkTerm : HasErr String es => Ty [<] () -> CheckTerm [<] [<] -> App es ()
+checkTerm a t = do
+  let True = checks [<] [<] a t
+    | False => throw "term ill-typed"
+  pure ()
+
 printType :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
   Ty [<] () -> App es ()
 printType a = do
   primIO $ renderIO $ layoutSmart opts $ prettyType a Open
 
-ppType : FileIO es => PrimIO es => HasErr String es => App es ()
-ppType = do
-  file <- fGetStr stdin
-  toks <- lexInkyString file
-  a <- parseType toks
-  checkType a
-  printType a
+printTerm :
+  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+  CheckTerm [<] [<] -> App es ()
+printTerm a = do
+  primIO $ renderIO $ layoutSmart opts $ prettyCheck a Open
 
-main : IO ()
-main =
-  run $
-  handle {err = IOError}
-    (handle {err = String} ppType
-      (const $ pure ())
-      printErrLn)
-    (const $ pure ())
-    (printErrLn . show)
+readFile : FileIO es => File -> App es String
+readFile f = do
+  content <- read [<] f
+  pure (fastConcat $ content <>> [])
   where
-  printErrLn : PrimIO es => String -> App es ()
-  printErrLn msg = do
-    primIO $ () <$ fPutStrLn stderr msg
-    pure ()
+  read : SnocList String -> File -> App es (SnocList String)
+  read acc f = do
+    False <- fEOF f
+      | True => pure acc
+    str <- fGetStr f
+    read (acc :< str) f
+
+readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
+readFileOrStdin Nothing = readFile stdin
+readFileOrStdin (Just path) = withFile path Read throw readFile
+
+
+-- Arguments -------------------------------------------------------------------
+
+Inky : Command "inky"
+Inky = MkCommand
+  { description = """
+    tool suite for Primrose programs
+    """
+  , subcommands =
+    [ "--help" ::= basic "print this help text" none
+    , "format" ::= MkCommand
+      { description = """
+        pretty print data
+        """
+      , subcommands =
+        [ "type" ::= basic "print a type" filePath
+        , "term" ::= basic "print a term" filePath
+        ]
+      , modifiers = []
+      , arguments = none
+      }
+    , "check" ::= MkCommand
+      { description = """
+        check well-formedness
+        """
+      , subcommands =
+        [ "type" ::= basic "check a type" filePath
+        , "term" ::= MkCommand
+          { description = "check a term"
+          , subcommands = []
+          , modifiers = ["--type" ::= option "type to check against" filePath]
+          , arguments = filePath
+          }
+        ]
+      , modifiers = []
+      , arguments = none
+      }
+    ]
+  , modifiers = []
+  , arguments = none
+  }
+
+-- Driver ----------------------------------------------------------------------
+
+parseArgs :
+  (cmd : Command nm) ->
+  App (String :: Init) (ParseTree cmd)
+parseArgs cmd = do
+  Right args <- primIO cmd.parseArgs
+    | Left msg => throw msg
+  let Pure args = ParsedTree.finalising args
+    | Fail errs => throw (show $ the (Error ()) $ Fail errs)
+  pure args
+
+abortErr : PrimIO es => String -> App es a
+abortErr msg = do
+  primIO $ () <$ fPutStrLn stderr msg
+  primIO exitFailure
+
+showHelp : Console es => App es ()
+showHelp = putStrLn "Usage: \{Inky .usage}"
+
+main : IO ()
+main = run {l = MayThrow} $ do
+  args <- handle {err = String} (parseArgs Inky) pure abortErr
+  Collie.handle {cmd = ("inky" ** Inky)} args
+    [ const showHelp
+    , "--help" ::= [ const showHelp ]
+    , "format" ::=
+      [ const showHelp
+      , "type" ::=
+        [ \cmd => do
+          let path = cmd.arguments
+          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
+          toks <- handle {err = String} (lexInkyString txt) pure abortErr
+          a <- handle {err = String} (parseType toks) pure abortErr
+          printType a
+          pure ()
+        ]
+      , "term" ::=
+        [ \cmd => do
+          let path = cmd.arguments
+          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
+          toks <- handle {err = String} (lexInkyString txt) pure abortErr
+          t <- handle {err = String} (parseTerm toks) pure abortErr
+          printTerm t
+          pure ()
+        ]
+      ]
+    , "check" ::=
+      [ const showHelp
+      , "type" ::=
+        [ \cmd => do
+          let path = cmd.arguments
+          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
+          toks <- handle {err = String} (lexInkyString txt) pure abortErr
+          a <- handle {err = String} (parseType toks) pure abortErr
+          handle {err = String} (checkType a) pure abortErr
+        ]
+      , "term" ::=
+        [ \cmd => do
+          let path = cmd.arguments
+          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
+          toks <- handle {err = String} (lexInkyString txt) pure abortErr
+          t <- handle {err = String} (parseTerm toks) pure abortErr
+          let [type] = cmd.modifiers.content
+          a <-
+            maybe (pure (TArrow TNat TNat))
+              (\path => do
+                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
+                toks <- handle {err = String} (lexInkyString txt) pure abortErr
+                a <- handle {err = String} (parseType toks) pure abortErr
+                handle {err = String} (checkType a) pure abortErr
+                pure a)
+              type
+          handle {err = String} (checkTerm a t) pure abortErr
+        ]
+      ]
+    ]