Isabelle/HOL translation: fix creation of polymorphic records

.github/workflows/ci.yml

@@ -28,7 +28,7 @@ env:
   RISC0_VM_VERSION: v1.0.1
   ANOMA_VERSION: f52cd44235f35a907c22c428ce1fdf3237c97927
   JUST_ARGS: runtimeCcArg=$CC runtimeLibtoolArg=$LIBTOOL
-  STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j
+  STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j --stack-yaml=stack.yaml
 
 jobs:
   pre-commit:

app/App.hs

@@ -261,19 +261,37 @@ runPipeline opts input_ =
   runPipelineLogger opts input_
     . inject
 
+runPipelineUpTo ::
+  (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) =>
+  Bool ->
+  opts ->
+  Maybe (AppPath File) ->
+  Sem (PipelineEff r) a ->
+  Sem r (a, [a])
+runPipelineUpTo bNonRecursive opts input_ a
+  | bNonRecursive = do
+      r <- runPipeline opts input_ a
+      return (r, [])
+  | otherwise = runPipelineUpToRecursive opts input_ a
+
 runPipelineHtml ::
   (Members '[App, EmbedIO, Logger, TaggedLock] r) =>
   Bool ->
   Maybe (AppPath File) ->
   Sem r (InternalTypedResult, [InternalTypedResult])
-runPipelineHtml bNonRecursive input_
-  | bNonRecursive = do
-      r <- runPipelineNoOptions input_ upToInternalTyped
-      return (r, [])
-  | otherwise = do
-      args <- askArgs
-      entry <- getEntryPoint' args input_
-      runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError
+runPipelineHtml bNonRecursive input_ = runPipelineUpTo bNonRecursive () input_ upToInternalTyped
+
+runPipelineUpToRecursive ::
+  (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) =>
+  opts ->
+  Maybe (AppPath File) ->
+  Sem (PipelineEff r) a ->
+  Sem r (a, [a])
+runPipelineUpToRecursive opts input_ a = do
+  args <- askArgs
+  entry <- getEntryPoint' args input_
+  let entry' = applyOptions opts entry
+  runReader defaultPipelineOptions (runPipelineRecursiveEither entry' (inject a)) >>= fromRightJuvixError
 
 runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a
 runPipelineOptions m = do

app/Commands/Isabelle.hs

@@ -12,22 +12,28 @@ runCommand ::
   Sem r ()
 runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
-  res <- runPipeline opts inputFile upToIsabelle
-  let thy = res ^. resultTheory
-      comments = res ^. resultComments
-  outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
-  if
-      | opts ^. isabelleStdout -> do
-          renderStdOut (ppOutDefault comments thy)
-          putStrLn ""
-      | otherwise -> do
-          ensureDir outputDir
-          let file :: Path Rel File
-              file =
-                relFile
-                  ( unpack (thy ^. theoryName . namePretty)
-                      <.> isabelleFileExt
-                  )
-              absPath :: Path Abs File
-              absPath = outputDir <//> file
-          writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
+  (r, rs) <- runPipelineUpTo (opts ^. isabelleNonRecursive) opts inputFile upToIsabelle
+  let pkg = r ^. resultModuleId . moduleIdPackage
+  mapM_ (translateTyped opts pkg) (r : rs)
+
+translateTyped :: (Members AppEffects r) => IsabelleOptions -> Text -> Result -> Sem r ()
+translateTyped opts pkg res
+  | res ^. resultModuleId . moduleIdPackage == pkg = do
+      let thy = res ^. resultTheory
+          comments = res ^. resultComments
+      outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
+      if
+          | opts ^. isabelleStdout ->
+              renderStdOutLn (ppOutDefault comments thy)
+          | otherwise -> do
+              ensureDir outputDir
+              let file :: Path Rel File
+                  file =
+                    relFile
+                      ( unpack (thy ^. theoryName . namePretty)
+                          <.> isabelleFileExt
+                      )
+                  absPath :: Path Abs File
+                  absPath = outputDir <//> file
+              writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
+  | otherwise = return ()

app/Commands/Isabelle/Options.hs

@@ -4,7 +4,8 @@ import CommonOptions
 import Juvix.Compiler.Pipeline.EntryPoint
 
 data IsabelleOptions = IsabelleOptions
-  { _isabelleInputFile :: Maybe (AppPath File),
+  { _isabelleNonRecursive :: Bool,
+    _isabelleInputFile :: Maybe (AppPath File),
     _isabelleOutputDir :: AppPath Dir,
     _isabelleStdout :: Bool,
     _isabelleOnlyTypes :: Bool
@@ -15,6 +16,11 @@ makeLenses ''IsabelleOptions
 
 parseIsabelle :: Parser IsabelleOptions
 parseIsabelle = do
+  _isabelleNonRecursive <-
+    switch
+      ( long "non-recursive"
+          <> help "Do not process imported modules recursively"
+      )
   _isabelleOutputDir <-
     parseGenericOutputDir
       ( value "isabelle"

package.yaml

@@ -12,7 +12,7 @@ author:
     Lukasz Czajka,
     Github's contributors,
   ]
-tested-with: ghc == 9.8.2
+tested-with: ghc == 9.10.1
 homepage: https://juvix.org
 bug-reports: https://github.com/anoma/juvix/issues
 description: The Juvix compiler
@@ -52,7 +52,7 @@ dependencies:
   - aeson-pretty == 0.8.*
   - ansi-terminal == 1.1.*
   - array == 0.5.*
-  - base == 4.19.*
+  - base == 4.20.*
   - base16-bytestring == 1.0.*
   - base64-bytestring == 1.2.*
   - bitvec == 1.1.*
@@ -68,14 +68,14 @@ dependencies:
   - edit-distance == 0.2.*
   - effectful == 2.3.*
   - effectful-core == 2.3.*
-  - effectful-th == 1.0.*
+  - effectful-th == 1.0.0.2
   - exceptions == 0.10.*
   - extra == 1.7.*
   - file-embed == 0.0.*
   - filelock == 0.1.*
   - filepath == 1.4.*
   - flatparse == 0.5.*
-  - ghc == 9.8.2
+  - ghc == 9.10.1
   - githash == 0.1.*
   - hashable == 1.4.*
   - language-c == 0.9.*
@@ -102,7 +102,7 @@ dependencies:
   - stm == 2.5.*
   - Stream == 0.4.*
   - string-interpolate == 0.3.*
-  - template-haskell == 2.21.*
+  - template-haskell == 2.22.*
   - temporary == 1.3.*
   - text == 2.1.*
   - th-utilities == 0.2.*

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -315,7 +315,7 @@ instance PrettyCode RecordField where
 
 ppImports :: [Name] -> Sem r [Doc Ann]
 ppImports ns =
-  return $ map (dquotes . pretty) $ filter (not . Text.isPrefixOf "Stdlib/") $ map (Text.replace "." "/" . (^. namePretty)) ns
+  return $ map pretty $ filter (not . Text.isPrefixOf "Stdlib_" . (^. namePretty)) ns
 
 instance PrettyCode Theory where
   ppCode Theory {..} = do