Add typecheck and internal command (#270)

* Closes #269 * Add internal command * w.i.p * Fix shell tests. * Rename check command and add shell-tests
anoma · Jul 12, 2022 · eb6819f · eb6819f
1 parent 329bec5
commit eb6819f
Show file tree

Hide file tree

Showing 27 changed files with 428 additions and 343 deletions.
diff --git a/app/Command.hs b/app/Command.hs
@@ -2,38 +2,24 @@ module Command
   ( module Command,
     module Commands.Extra,
     module Commands.Html,
-    module Commands.MicroJuvix,
-    module Commands.Parse,
-    module Commands.Scope,
-    module Commands.Termination,
     module Commands.Compile,
+    module Commands.Internal,
   )
 where
 
 import Commands.Compile
 import Commands.Extra
 import Commands.Html
-import Commands.MicroJuvix
-import Commands.Parse
-import Commands.Scope
-import Commands.Termination
+import Commands.Internal
 import GlobalOptions
 import Juvix.Prelude hiding (Doc)
-import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import Options.Applicative
 
 data Command
-  = Compile CompileOptions
-  | DisplayRoot
-  | Highlight
+  = Check
+  | Compile CompileOptions
   | Html HtmlOptions
-  | MicroJuvix MicroJuvixCommand
-  | MiniC
-  | MiniHaskell
-  | MonoJuvix
-  | Parse ParseOptions
-  | Scope ScopeOptions
-  | Termination TerminationCommand
+  | Internal InternalCommand
 
 data CommandGlobalOptions = CommandGlobalOptions
   { _cliCommand :: Command,
@@ -48,97 +34,41 @@ parseCommandGlobalOptions = do
   cmd <-
     hsubparser
       ( mconcat
-          [ commandCompile,
-            commandHighlight,
+          [ commandCheck,
+            commandCompile,
             commandHtml,
-            commandMicroJuvix,
-            commandMiniC,
-            commandMonoJuvix,
-            commandParse,
-            commandScope,
-            commandShowRoot,
-            commandTermination
+            commandInternal
           ]
       )
-      <|> hsubparser (commandMiniHaskell <> internal)
   return (cmd {_cliGlobalOptions = opts <> cmd ^. cliGlobalOptions})
 
+commandCheck :: Mod CommandFields CommandGlobalOptions
+commandCheck =
+  command "typecheck" $
+    info
+      (addGlobalOptions (pure Check))
+      (progDesc "Type check a Juvix file")
+
 commandCompile :: Mod CommandFields CommandGlobalOptions
 commandCompile =
   command "compile" $
     info
       (addGlobalOptions (Compile <$> parseCompile))
       (progDesc "Compile a Juvix file")
 
-commandHighlight :: Mod CommandFields CommandGlobalOptions
-commandHighlight =
-  command "highlight" $
-    info
-      (addGlobalOptions (pure Highlight))
-      (progDesc "Highlight a Juvix file")
-
 commandHtml :: Mod CommandFields CommandGlobalOptions
 commandHtml =
   command "html" $
     info
       (addGlobalOptions (Html <$> parseHtml))
       (progDesc "Generate HTML for a Juvix file")
 
-commandMiniC :: Mod CommandFields CommandGlobalOptions
-commandMiniC =
-  command "minic" $
-    info
-      (addGlobalOptions (pure MiniC))
-      (progDesc "Translate a Juvix file to MiniC")
-
-commandMicroJuvix :: Mod CommandFields CommandGlobalOptions
-commandMicroJuvix =
-  command "microjuvix" $
-    info
-      (addGlobalOptions (MicroJuvix <$> parseMicroJuvixCommand))
-      (progDesc "Subcommands related to MicroJuvix")
-
-commandMiniHaskell :: Mod CommandFields CommandGlobalOptions
-commandMiniHaskell =
-  command "minihaskell" $
-    info
-      (addGlobalOptions (pure MiniHaskell))
-      (progDesc "Translate a Juvix file to MiniHaskell")
-
-commandMonoJuvix :: Mod CommandFields CommandGlobalOptions
-commandMonoJuvix =
-  command "monojuvix" $
+commandInternal :: Mod CommandFields CommandGlobalOptions
+commandInternal =
+  command "internal" $
     info
-      (addGlobalOptions (pure MonoJuvix))
-      (progDesc "Translate a Juvix file to MonoJuvix")
-
-commandParse :: Mod CommandFields CommandGlobalOptions
-commandParse =
-  command "parse" $
-    info
-      (addGlobalOptions (Parse <$> parseParse))
-      (progDesc "Parse a Juvix file")
-
-commandScope :: Mod CommandFields CommandGlobalOptions
-commandScope =
-  command "scope" $
-    info
-      (addGlobalOptions (Scope <$> parseScope))
-      (progDesc "Parse and scope a Juvix file")
-
-commandShowRoot :: Mod CommandFields CommandGlobalOptions
-commandShowRoot =
-  command "root" $
-    info
-      (liftParserCmd (pure DisplayRoot))
-      (progDesc "Show the root path for a Juvix project")
-
-commandTermination :: Mod CommandFields CommandGlobalOptions
-commandTermination =
-  command "termination" $
-    info
-      (addGlobalOptions $ Termination <$> parseTerminationCommand)
-      (progDesc "Subcommands related to termination checking")
+      (addGlobalOptions (Internal <$> parseInternalCommand))
+      (progDesc "Internal subcommands")
 
 --------------------------------------------------------------------------------
 -- Misc
@@ -154,17 +84,10 @@ liftParserCmd cmd = cmdDefaultOptions <$> cmd
 addGlobalOptions :: Parser Command -> Parser CommandGlobalOptions
 addGlobalOptions parser = do
   flags1 <- parseGlobalFlags True
-  ~(opts2, _cliCommand) <- addParser (parseGlobalOptions True) parser
+  ~(opts2, _cliCommand) <- addParser (parseGlobalFlags True) parser
   fs <- parserInputFiles
   return
     CommandGlobalOptions
       { _cliGlobalOptions = flags1 <> opts2 <> mempty {_globalInputFiles = fs},
         ..
       }
-
-mkScopePrettyOptions :: GlobalOptions -> ScopeOptions -> Scoper.Options
-mkScopePrettyOptions g ScopeOptions {..} =
-  Scoper.defaultOptions
-    { Scoper._optShowNameIds = g ^. globalShowNameIds,
-      Scoper._optInlineImports = _scopeInlineImports
-    }
diff --git a/app/Commands/Extra.hs b/app/Commands/Extra.hs
@@ -1,10 +1,16 @@
 module Commands.Extra where
 
 import Juvix.Prelude hiding (Doc)
-import Options.Applicative
+import Options.Applicative hiding (hidden)
 import Options.Applicative.Builder.Internal
 import Options.Applicative.Types
 
+hidden :: Bool -> Mod f a
+hidden sure = optionMod $ \p ->
+  if
+      | not sure -> p
+      | otherwise -> p {propVisibility = min Hidden (propVisibility p)}
+
 parserInputFile :: Parser FilePath
 parserInputFile =
   argument
@@ -39,9 +45,3 @@ addParser parser = \case
   (BindP p k) -> BindP (addParser parser p) $ \(g1, x) ->
     BindP (addParser parser $ k x) $ \(g2, x') ->
       pure (g1 <> g2, x')
-
-hidden :: Bool -> Mod f a
-hidden sure = optionMod $ \p ->
-  if
-      | not sure -> p
-      | otherwise -> p {propVisibility = min Hidden (propVisibility p)}
diff --git a/app/Commands/Internal.hs b/app/Commands/Internal.hs
@@ -0,0 +1,105 @@
+module Commands.Internal
+  ( module Commands.Internal,
+    module Commands.Internal.MicroJuvix,
+    module Commands.Internal.Parse,
+    module Commands.Internal.Scope,
+    module Commands.Internal.Termination,
+  )
+where
+
+import Commands.Internal.MicroJuvix
+import Commands.Internal.Parse
+import Commands.Internal.Scope
+import Commands.Internal.Termination
+import Juvix.Prelude
+import Options.Applicative
+
+data InternalCommand
+  = DisplayRoot
+  | Highlight
+  | MicroJuvix MicroJuvixCommand
+  | MiniC
+  | MiniHaskell
+  | MonoJuvix
+  | Parse ParseOptions
+  | Scope ScopeOptions
+  | Termination TerminationCommand
+
+parseInternalCommand :: Parser InternalCommand
+parseInternalCommand =
+  hsubparser
+    ( mconcat
+        [ commandHighlight,
+          commandMicroJuvix,
+          commandMiniC,
+          commandMiniHaskell,
+          commandMonoJuvix,
+          commandParse,
+          commandScope,
+          commandShowRoot,
+          commandTermination
+        ]
+    )
+
+commandHighlight :: Mod CommandFields InternalCommand
+commandHighlight =
+  command "highlight" $
+    info
+      (pure Highlight)
+      (progDesc "Highlight a Juvix file")
+
+commandMiniC :: Mod CommandFields InternalCommand
+commandMiniC =
+  command "minic" $
+    info
+      (pure MiniC)
+      (progDesc "Translate a Juvix file to MiniC")
+
+commandMicroJuvix :: Mod CommandFields InternalCommand
+commandMicroJuvix =
+  command "microjuvix" $
+    info
+      (MicroJuvix <$> parseMicroJuvixCommand)
+      (progDesc "Subcommands related to MicroJuvix")
+
+commandMiniHaskell :: Mod CommandFields InternalCommand
+commandMiniHaskell =
+  command "minihaskell" $
+    info
+      (pure MiniHaskell)
+      (progDesc "Translate a Juvix file to MiniHaskell")
+
+commandMonoJuvix :: Mod CommandFields InternalCommand
+commandMonoJuvix =
+  command "monojuvix" $
+    info
+      (pure MonoJuvix)
+      (progDesc "Translate a Juvix file to MonoJuvix")
+
+commandParse :: Mod CommandFields InternalCommand
+commandParse =
+  command "parse" $
+    info
+      (Parse <$> parseParse)
+      (progDesc "Parse a Juvix file")
+
+commandScope :: Mod CommandFields InternalCommand
+commandScope =
+  command "scope" $
+    info
+      (Scope <$> parseScope)
+      (progDesc "Parse and scope a Juvix file")
+
+commandShowRoot :: Mod CommandFields InternalCommand
+commandShowRoot =
+  command "root" $
+    info
+      (pure DisplayRoot)
+      (progDesc "Show the root path for a Juvix project")
+
+commandTermination :: Mod CommandFields InternalCommand
+commandTermination =
+  command "termination" $
+    info
+      (Termination <$> parseTerminationCommand)
+      (progDesc "Subcommands related to termination checking")
diff --git a/app/Commands/MicroJuvix.hs → app/Commands/Internal/MicroJuvix.hs b/app/Commands/MicroJuvix.hs → app/Commands/Internal/MicroJuvix.hs
@@ -1,4 +1,4 @@
-module Commands.MicroJuvix where
+module Commands.Internal.MicroJuvix where
 
 import Juvix.Prelude hiding (Doc)
 import Options.Applicative
@@ -14,6 +14,22 @@ newtype MicroJuvixTypeOptions = MicroJuvixTypeOptions
 
 makeLenses ''MicroJuvixTypeOptions
 
+defaultMicroJuvixTypeOptions :: MicroJuvixTypeOptions
+defaultMicroJuvixTypeOptions =
+  MicroJuvixTypeOptions
+    { _microJuvixTypePrint = False
+    }
+
+instance Semigroup MicroJuvixTypeOptions where
+  o1 <> o2 =
+    MicroJuvixTypeOptions
+      { _microJuvixTypePrint = (o1 ^. microJuvixTypePrint) || (o2 ^. microJuvixTypePrint)
+      }
+
+instance Monoid MicroJuvixTypeOptions where
+  mempty = defaultMicroJuvixTypeOptions
+  mappend = (<>)
+
 parseMicroJuvixCommand :: Parser MicroJuvixCommand
 parseMicroJuvixCommand =
   hsubparser $

diff --git a/app/Commands/Parse.hs → app/Commands/Internal/Parse.hs b/app/Commands/Parse.hs → app/Commands/Internal/Parse.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE ApplicativeDo #-}
-
-module Commands.Parse where
+module Commands.Internal.Parse where
 
 import Juvix.Prelude hiding (Doc)
 import Options.Applicative

diff --git a/app/Commands/Scope.hs → app/Commands/Internal/Scope.hs b/app/Commands/Scope.hs → app/Commands/Internal/Scope.hs
@@ -1,6 +1,8 @@
-module Commands.Scope where
+module Commands.Internal.Scope where
 
+import GlobalOptions
 import Juvix.Prelude hiding (Doc)
+import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import Options.Applicative
 
 newtype ScopeOptions = ScopeOptions
@@ -17,3 +19,10 @@ parseScope = do
           <> help "Show the code of imported modules next to the import statement"
       )
   pure ScopeOptions {..}
+
+mkScopePrettyOptions :: GlobalOptions -> ScopeOptions -> Scoper.Options
+mkScopePrettyOptions g ScopeOptions {..} =
+  Scoper.defaultOptions
+    { Scoper._optShowNameIds = g ^. globalShowNameIds,
+      Scoper._optInlineImports = _scopeInlineImports
+    }
diff --git a/app/Commands/Termination.hs → app/Commands/Internal/Termination.hs b/app/Commands/Termination.hs → app/Commands/Internal/Termination.hs
@@ -1,4 +1,4 @@
-module Commands.Termination where
+module Commands.Internal.Termination where
 
 import Control.Monad.Extra
 import Data.Text qualified as Text