From fa384e2e261032c8c804c3f3d26ccdaf08a8f950 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Mon, 25 Jul 2022 01:21:38 +0200
Subject: [PATCH] add top level parser

---
 src/Main.idr         | 17 ++++++++++++++++-
 src/Parser/Parse.idr | 15 +++++++++++++++
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/Main.idr b/src/Main.idr
index 7b329d5..9bd92c3 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -4,9 +4,24 @@ import Core.Check
 import Core.Term
 import Parser.Parse
 
+import System
+import System.File
+
+ioStr : IO String
+ioStr = getArgs >>= \case
+          []        => getLine
+          (x ::  _) => do
+            r <- readFile x
+            case r of
+               Left  e => do
+                 print e
+                 exitFailure
+               Right s => pure s
+
+
 main : IO ()
 main = do
-  str <- getLine
+  str <- ioStr
   case parse0 str of
        Left e  => putStrLn e
        Right t => print t
diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr
index e492d38..5903d7c 100644
--- a/src/Parser/Parse.idr
+++ b/src/Parser/Parse.idr
@@ -365,6 +365,21 @@ mutual
     match PTRParen
     pure e
 
+definitions : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n)
+definitions n env = do
+    match PTLet
+    commit
+    arg <- match PTIdentifier
+    match PTColon
+    ty <- expr n env
+    match PTDefEq
+    tr <- expr n env
+    next <- definitions (S n) (arg :: env) <|> pure TStar
+    pure (TLet ty tr next)
+
+toplevel : Grammar state PiToken True (Term 0)
+toplevel = definitions 0 []
+
 parsePi : (n : Nat) -> Vect n String -> List (WithBounds PiToken) -> Either String (Term n)
 parsePi n env toks =
   case parse (expr n env) $ filter (not . ignored) toks of