Isabelle/HOL translation: recursive translation of the whole project

.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

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -69,17 +69,19 @@ fromInternal [email protected] {..} = do
 goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
 goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = overNameText toIsabelleName _moduleName,
-      _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
+    { _theoryName = overNameText toIsabelleTheoryName _moduleName,
+      _theoryImports =
+        map
+          (overNameText toIsabelleTheoryName . (^. Internal.importModuleName))
+          (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
         Just (PragmaIsabelleIgnore True) -> []
         _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
-    toIsabelleName :: Text -> Text
-    toIsabelleName name = case reverse $ filter (/= "") $ T.splitOn "." name of
-      h : _ -> h
-      [] -> impossible
+    toIsabelleTheoryName :: Text -> Text
+    toIsabelleTheoryName name =
+      quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name
 
     isTypeDef :: Statement -> Bool
     isTypeDef = \case
@@ -195,8 +197,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 }
       where
         argnames =
-          map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
-        name' = overNameText quote name
+          map quoteName $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo
+        name' = quoteName name
         loc = getLoc name
 
     isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool
@@ -376,18 +378,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
     goTypeIden :: Internal.Iden -> Type
     goTypeIden = \case
-      Internal.IdenFunction name -> mkIndType (overNameText quote name) []
+      Internal.IdenFunction name -> mkIndType (quoteName name) []
       Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
-      Internal.IdenVar name -> TyVar $ TypeVar (overNameText quote name)
-      Internal.IdenAxiom name -> mkIndType (overNameText quote name) []
-      Internal.IdenInductive name -> mkIndType (overNameText quote name) []
+      Internal.IdenVar name -> TyVar $ TypeVar (quoteName name)
+      Internal.IdenAxiom name -> mkIndType (quoteName name) []
+      Internal.IdenInductive name -> mkIndType (quoteName name) []
 
     goTypeApp :: Internal.Application -> Type
     goTypeApp app = mkIndType name params
       where
         (ind, args) = Internal.unfoldApplication app
         params = map goType (toList args)
-        name = overNameText quote $ case ind of
+        name = quoteName $ case ind of
           Internal.ExpressionIden (Internal.IdenFunction n) -> n
           Internal.ExpressionIden (Internal.IdenAxiom n) -> n
           Internal.ExpressionIden (Internal.IdenInductive n) -> n
@@ -416,8 +418,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               setNameText "None" name
             Just Internal.BuiltinMaybeJust ->
               setNameText "Some" name
-            _ -> overNameText quote name
-        Nothing -> overNameText quote name
+            _ -> quoteName name
+        Nothing -> quoteName name
 
     getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter]
     getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType
@@ -430,8 +432,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
             Just funInfo ->
               case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
                 Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
-                Nothing -> overNameText quote name
-            Nothing -> overNameText quote name
+                Nothing -> quoteName name
+            Nothing -> quoteName name
       x -> x
 
     lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression
@@ -490,8 +492,8 @@ goModule onlyTypes infoTable Internal.Module {..} =
               Nothing -> return $ ExprIden (goConstrName name)
           Internal.IdenVar name -> do
             lookupName name
-          Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name)
-          Internal.IdenInductive name -> return $ ExprIden (overNameText quote name)
+          Internal.IdenAxiom name -> return $ ExprIden (quoteName name)
+          Internal.IdenInductive name -> return $ ExprIden (quoteName name)
 
         goApplication :: Internal.Application -> Sem r Expression
         goApplication [email protected] {..}
@@ -1217,9 +1219,40 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
                 ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
+    quoteName :: Name -> Name
+    quoteName name = overNameText goNameText name
+      where
+        goNameText :: Text -> Text
+        goNameText txt
+          | Text.elem '.' txt =
+              let idenName = snd $ Text.breakOnEnd "." txt
+                  modulePath = name ^. nameId . nameIdModuleId . moduleIdPath
+                  modulePathText = Text.intercalate "." (modulePath ^. modulePathKeyDir ++ [modulePath ^. modulePathKeyName])
+                  moduleName' = toIsabelleTheoryName modulePathText
+                  idenName' = quote idenName
+               in moduleName' <> "." <> idenName'
+          | otherwise = quote txt
+
     quote :: Text -> Text
-    quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+    quote txt0
+      | Text.elem '.' txt0 = moduleName' <> "." <> idenName'
+      | otherwise = quote'' txt0
       where
+        (moduleName, idenName) = Text.breakOnEnd "." txt0
+        moduleName' = toIsabelleTheoryName (removeLastDot moduleName)
+        idenName' = quote'' idenName
+
+        removeLastDot :: Text -> Text
+        removeLastDot txt
+          | Text.last txt == '.' = Text.init txt
+          | otherwise = txt
+
+        quote'' :: Text -> Text
+        quote'' =
+          quote'
+            . Text.filter isLatin1
+            . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
+
         quote' :: Text -> Text
         quote' txt
           | HashSet.member txt reservedNames = quote' (prime txt)