Check command and raw mode for files

Author: tomaz1502

app/Main.hs

@@ -10,7 +10,7 @@ import Data.List            ( isPrefixOf )
 import System.Environment   ( getArgs )
 
 import Lam.Context ( emptyContext )
-import Lam.Handler ( replWrapper, handleFile )
+import Lam.Handler ( replWrapper, handleFileWrapper )
 import Lam.Result
 
 setup :: IO ()
@@ -27,7 +27,7 @@ main = do
   let flagSet = [Untyped | "--untyped" `elem` flags]
   case nonFlags of
     []      -> run replWrapper flagSet
-    [fName] -> run (handleFile fName) flagSet
+    [fName] -> run (handleFileWrapper fName) flagSet
     _       -> error wrongUsageMsg
   where
     wrongUsageMsg :: String

src/Lam/Agda/Lam/Data.agda

@@ -131,6 +131,7 @@ data Command : Set where
     TypedefC : Id × RawTypeL → Command
     DefineC  : Id × RawExpr → Command
     EvalC    : RawExpr → Command
+    CheckC   : RawExpr → Command
     LoadC    : Id → Command
     ReadC    : Id → Command
     ExitC    : Command

src/Lam/Handler.hs

@@ -4,7 +4,7 @@
 {-# LANGUAGE RankNTypes #-}
 
 module Lam.Handler ( replWrapper
-                   , handleFile
+                   , handleFileWrapper
                    ) where
 
 import Control.Monad.RWS        ( get, put )
@@ -57,9 +57,23 @@ handleEval rExpr = do
   else
     case typeCheck expr of
       Nothing -> throwError "Typing error."
-      Just t  ->
+      Just _  ->
         let normalizedExpr = eval expr in
-        let msg = untypedPrettyPrint normalizedExpr <> " :: " <> prettyPrintType t in
+        let msg = untypedPrettyPrint normalizedExpr in
+        liftIO (putStrLnFlush msg)
+
+handleCheck :: RawExpr -> Result ()
+handleCheck rExpr = do
+  gctx    <- get
+  expr    <- liftEither (eraseNames gctx rExpr)
+  isUntyped <- askUntyped
+  if isUntyped then
+    throwError "Trying to check type of an expr in an untyped context."
+  else
+    case typeCheck expr of
+      Nothing -> throwError "Typing error."
+      Just t  ->
+        let msg = prettyPrintType t in
         liftIO (putStrLnFlush msg)
 
 handleCommand :: Command -> Result ()
@@ -68,12 +82,13 @@ handleCommand c =
     TypedefC (macroName, macroType) -> handleTypedef macroName macroType
     DefineC  (macroName, macroExpr) -> handleDefine macroName macroExpr
     EvalC rExpr                     -> handleEval rExpr
+    CheckC rExpr                    -> handleCheck rExpr
     LoadC path                      -> loadFile path
     ReadC varName                   -> do
-        exprS <- liftIO (readRepl [] "")
-        isUntyped <- askUntyped
-        expr <- liftEither (parseRawExpr isUntyped exprS)
-        handleDefine varName expr
+      exprS <- liftIO (readRepl [] "")
+      isUntyped <- askUntyped
+      expr <- liftEither (parseRawExpr isUntyped exprS)
+      handleDefine varName expr
     ExitC -> return ()
 
 repl :: CmdHistory -> Result ()
@@ -99,3 +114,6 @@ handleFile fName = do
   sc      <- liftIO $ readFile fName
   prog    <- liftEither (parseProg isUntyped sc)
   mapM_ handleCommand prog
+
+handleFileWrapper :: String -> Result ()
+handleFileWrapper fName = runInRawMode (handleFile fName)

src/Lam/Parser/Lexer.x

@@ -24,6 +24,7 @@ tokens :-
 <0> "lam"     { tok Lam             }
 <0> "fix"     { tok Fix             }
 <0> "EVAL"    { tok Eval            }
+<0> "CHECK"   { tok Check           }
 <0> "EXIT"    { tok Exit            }
 <0> "TYPEDEF" { tok Typedef         }
 <0> "DEFINE"  { tok Define          }
@@ -75,6 +76,7 @@ data Token =
   | Lam
   | Fix
   | Eval
+  | Check
   | Exit
   | Typedef
   | Load

src/Lam/Parser/Parser.y

@@ -45,6 +45,7 @@ import Lam.Parser.Lexer qualified as L
   ":="      { L.ColonEq    }
   "DEFINE"  { L.Define     }
   "EVAL"    { L.Eval       }
+  "CHECK"   { L.Check      }
   "EXIT"    { L.Exit       }
   "TYPEDEF" { L.Typedef    }
   "LOAD"    { L.Load       }
@@ -96,6 +97,7 @@ UntypedCommand :: { Command }
   | UntypedEvalCommand   { EvalC $1  }
   | LoadCommand          { LoadC $1 }
   | ReadCommand          { ReadC $1 }
+  | CheckCommand         { CheckC $1 }
   | ExitCommand          { ExitC }
   -- we allow this here but throw an error later
   | TypedefCommand       { TypedefC $1 }
@@ -106,6 +108,9 @@ UntypedDefineCommand :: { (Id, RawExpr) }
 UntypedEvalCommand :: { RawExpr }
   : "EVAL" ":" UntypedRawExpr ";" { $3 }
 
+UntypedCheckCommand :: { RawExpr }
+  : "CHECK" ":" UntypedRawExpr ";" { $3 }
+
 Program :: { [Command] }
   : Command Program { $1 : $2 }
   | { [] }
@@ -114,6 +119,7 @@ Command :: { Command }
   : TypedefCommand { TypedefC $1 }
   | DefineCommand  { DefineC $1 }
   | EvalCommand    { EvalC $1 }
+  | CheckCommand   { CheckC $1 }
   | LoadCommand    { LoadC $1 }
   | ReadCommand    { ReadC $1 }
   | ExitCommand    { ExitC }
@@ -129,6 +135,9 @@ DefineCommand :: { (Id, RawExpr) }
 EvalCommand :: { RawExpr }
   : "EVAL" ":" RawExpr ";" { $3 }
 
+CheckCommand :: { RawExpr }
+  : "CHECK" ":" RawExpr ";" { $3 }
+
 LoadCommand :: { String }
   : "LOAD" ":" path ";" { init (tail $3) {- Removes quotes -} }
   -- yes i will change that later to FilePath thank you