--only-types option

anoma · May 6, 2024 · 638d946 · 638d946
1 parent 02c3035
commit 638d946
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 13 deletions.
diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
@@ -11,7 +11,7 @@ runCommand ::
   Sem r ()
 runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
-  res <- runPipelineNoOptions inputFile upToIsabelle
+  res <- runPipeline opts inputFile upToIsabelle
   let thy = res ^. resultTheory
   outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
   if

diff --git a/app/Commands/Isabelle/Options.hs b/app/Commands/Isabelle/Options.hs
@@ -1,11 +1,13 @@
 module Commands.Isabelle.Options where
 
 import CommonOptions
+import Juvix.Compiler.Pipeline.EntryPoint
 
 data IsabelleOptions = IsabelleOptions
   { _isabelleInputFile :: Maybe (AppPath File),
     _isabelleOutputDir :: AppPath Dir,
-    _isabelleStdout :: Bool
+    _isabelleStdout :: Bool,
+    _isabelleOnlyTypes :: Bool
   }
   deriving stock (Data)
 
@@ -17,13 +19,21 @@ parseIsabelle = do
     parseGenericOutputDir
       ( value "isabelle"
           <> showDefault
-          <> help "Isabelle/HOL output directory"
+          <> help "Isabelle/HOL output directory."
           <> action "directory"
       )
   _isabelleStdout <-
     switch
       ( long "stdout"
-          <> help "Write the output to stdout instead of a file"
+          <> help "Write the output to stdout instead of a file."
+      )
+  _isabelleOnlyTypes <-
+    switch
+      ( long "only-types"
+          <> help "Translate types only. Omit function signatures."
       )
   _isabelleInputFile <- optional (parseInputFile FileExtJuvix)
   pure IsabelleOptions {..}
+
+instance EntryPointOptions IsabelleOptions where
+  applyOptions IsabelleOptions {..} e = e {_entryPointIsabelleOnlyTypes = _isabelleOnlyTypes}
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -18,33 +18,44 @@ fromInternal ::
   Internal.InternalTypedResult ->
   Sem r Result
 fromInternal Internal.InternalTypedResult {..} = do
+  onlyTypes <- (^. entryPointIsabelleOnlyTypes) <$> ask
   itab <- getInternalModuleTable <$> ask
   let md :: Internal.InternalModule
       md = _resultInternalModule
       itab' :: Internal.InternalModuleTable
       itab' = Internal.insertInternalModule itab md
       table :: Internal.InfoTable
       table = Internal.computeCombinedInfoTable itab'
-  go table _resultModule
+  go onlyTypes table _resultModule
   where
-    go :: Internal.InfoTable -> Internal.Module -> Sem r Result
-    go tab md =
+    go :: Bool -> Internal.InfoTable -> Internal.Module -> Sem r Result
+    go onlyTypes tab md =
       return $
         Result
-          { _resultTheory = goModule tab md,
+          { _resultTheory = goModule onlyTypes tab md,
             _resultModuleId = md ^. Internal.moduleId
           }
 
-goModule :: Internal.InfoTable -> Internal.Module -> Theory
-goModule infoTable Internal.Module {..} =
+goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
+goModule onlyTypes infoTable Internal.Module {..} =
   Theory
     { _theoryName = _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
+    isTypeDef :: Statement -> Bool
+    isTypeDef = \case
+      StmtDefinition {} -> False
+      StmtFunction {} -> False
+      StmtSynonym {} -> True
+      StmtDatatype {} -> True
+      StmtRecord {} -> True
+
     goMutualBlock :: Internal.MutualBlock -> [Statement]
-    goMutualBlock Internal.MutualBlock {..} = map goMutualStatement (toList _mutualStatements)
+    goMutualBlock Internal.MutualBlock {..} =
+      filter (\stmt -> not onlyTypes || isTypeDef stmt) $
+        map goMutualStatement (toList _mutualStatements)
 
     goMutualStatement :: Internal.MutualStatement -> Statement
     goMutualStatement = \case

diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
@@ -40,7 +40,8 @@ data EntryPoint = EntryPoint
     _entryPointModulePath :: Maybe (Path Abs File),
     _entryPointSymbolPruningMode :: SymbolPruningMode,
     _entryPointOffline :: Bool,
-    _entryPointFieldSize :: Natural
+    _entryPointFieldSize :: Natural,
+    _entryPointIsabelleOnlyTypes :: Bool
   }
   deriving stock (Eq, Show)
 
@@ -81,7 +82,8 @@ defaultEntryPointNoFile pkg root =
       _entryPointModulePath = Nothing,
       _entryPointSymbolPruningMode = FilterUnreachable,
       _entryPointOffline = False,
-      _entryPointFieldSize = defaultFieldSize
+      _entryPointFieldSize = defaultFieldSize,
+      _entryPointIsabelleOnlyTypes = False
     }
 
 defaultUnrollLimit :: Int