add top level parser

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

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