From c35b8e39f7dda2d9a330a60e60c7489bfecbd842 Mon Sep 17 00:00:00 2001
From: Dmitry <0nkery@users.noreply.github.com>
Date: Fri, 10 Jul 2020 20:08:21 +0700
Subject: [PATCH] Add command line option to typecheck package without codegen
 (#412)

---
 src/Idris/CommandLine.idr |  4 +++
 src/Idris/Package.idr     | 53 +++++++++++++++++++++++++++++++--------
 2 files changed, 47 insertions(+), 10 deletions(-)

diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr
index 2d3a00b9f..2b5cfad93 100644
--- a/src/Idris/CommandLine.idr
+++ b/src/Idris/CommandLine.idr
@@ -19,6 +19,7 @@ public export
 data PkgCommand
       = Build
       | Install
+      | Typecheck
       | Clean
       | REPL
 
@@ -26,6 +27,7 @@ export
 Show PkgCommand where
   show Build = "--build"
   show Install = "--install"
+  show Typecheck = "--typecheck"
   show Clean = "--clean"
   show REPL = "--repl"
 
@@ -180,6 +182,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Build modules/executable for the given package"),
            MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])
               (Just "Install the given package"),
+           MkOpt ["--typecheck"] [Required "package file"] (\f => [Package Typecheck f])
+              (Just "Typechecks the given package without code generation"),
            MkOpt ["--clean"] [Required "package file"] (\f => [Package Clean f])
               (Just "Clean intermediate files/executables for the given package"),
            MkOpt ["--repl"] [Required "package file"] (\f => [Package REPL f])
diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
index 49772a7dd..97755a76b 100644
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@@ -276,6 +276,27 @@ compileMain mainn mmod exec
          compileExp (PRef replFC mainn) exec
          pure ()
 
+prepareCompilation : {auto c : Ref Ctxt Defs} ->
+                     {auto s : Ref Syn SyntaxInfo} ->
+                     {auto o : Ref ROpts REPLOpts} ->
+                     PkgDesc ->
+                     List CLOpt ->
+                     Core (List Error)
+prepareCompilation pkg opts =
+  do
+    defs <- get Ctxt
+    addDeps pkg
+
+    processOptions (options pkg)
+    preOptions opts
+
+    runScript (prebuild pkg)
+
+    let toBuild = maybe (map snd (modules pkg))
+                        (\m => snd m :: map snd (modules pkg))
+                        (mainmod pkg)
+    buildAll toBuild
+
 build : {auto c : Ref Ctxt Defs} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto o : Ref ROpts REPLOpts} ->
@@ -283,16 +304,8 @@ build : {auto c : Ref Ctxt Defs} ->
         List CLOpt ->
         Core (List Error)
 build pkg opts
-    = do defs <- get Ctxt
-         addDeps pkg
-         processOptions (options pkg)
-         preOptions opts
-         runScript (prebuild pkg)
-         let toBuild = maybe (map snd (modules pkg))
-                             (\m => snd m :: map snd (modules pkg))
-                             (mainmod pkg)
-         [] <- buildAll toBuild
-              | errs => pure errs
+    = do [] <- prepareCompilation pkg opts
+            | errs => pure errs
 
          case executable pkg of
               Nothing => pure ()
@@ -301,6 +314,7 @@ build pkg opts
                                | Nothing => throw (GenericMsg emptyFC "No main module given")
                       let mainName = NS mainNS (UN "main")
                       compileMain mainName mainFile exec
+
          runScript (postbuild pkg)
          pure []
 
@@ -360,6 +374,21 @@ install pkg opts -- not used but might be in the future
          coreLift $ changeDir srcdir
          runScript (postinstall pkg)
 
+-- Check package without compiling anything.
+check : {auto c : Ref Ctxt Defs} ->
+        {auto s : Ref Syn SyntaxInfo} ->
+        {auto o : Ref ROpts REPLOpts} ->
+        PkgDesc ->
+        List CLOpt ->
+        Core (List Error)
+check pkg opts =
+  do
+    [] <- prepareCompilation pkg opts
+      | errs => pure errs
+
+    runScript (postbuild pkg)
+    pure []
+
 -- Data.These.bitraverse hand specialised for Core
 bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d)
 bitraverseC f g (This a)   = [| This (f a) |]
@@ -496,6 +525,10 @@ processPackage cmd file opts
                       Install => do [] <- build pkg opts
                                        | errs => coreLift (exitWith (ExitFailure 1))
                                     install pkg opts
+                      Typecheck => do
+                        [] <- check pkg opts
+                          | errs => coreLift (exitWith (ExitFailure 1))
+                        pure ()
                       Clean => clean pkg opts
                       REPL => do
                         [] <- build pkg opts