Juvix to Isabelle/HOL translation (#2752)

* Closes #2689 
* Adds the command `juvix isabelle program.juvix` which translates a
given file to an Isabelle/HOL theory.
* Currently, only a single module is translated.
* By default translates types and function signatures. Translating
function signatures can be disabled with the `--only-types` option.

Blocked by:
- https://github.com/anoma/juvix/issues/2763

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>

app/Commands/Isabelle.hs

@@ -0,0 +1,32 @@
+module Commands.Isabelle where
+
+import Commands.Base
+import Commands.Isabelle.Options
+import Juvix.Compiler.Backend.Isabelle.Data.Result
+import Juvix.Compiler.Backend.Isabelle.Language
+import Juvix.Compiler.Backend.Isabelle.Pretty
+
+runCommand ::
+  (Members '[EmbedIO, TaggedLock, App] r) =>
+  IsabelleOptions ->
+  Sem r ()
+runCommand opts = do
+  let inputFile = opts ^. isabelleInputFile
+  res <- runPipeline opts inputFile upToIsabelle
+  let thy = res ^. resultTheory
+  outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
+  if
+      | opts ^. isabelleStdout -> do
+          renderStdOut (ppOutDefault 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 thy <> "\n")

app/Commands/Isabelle/Options.hs

@@ -0,0 +1,39 @@
+module Commands.Isabelle.Options where
+
+import CommonOptions
+import Juvix.Compiler.Pipeline.EntryPoint
+
+data IsabelleOptions = IsabelleOptions
+  { _isabelleInputFile :: Maybe (AppPath File),
+    _isabelleOutputDir :: AppPath Dir,
+    _isabelleStdout :: Bool,
+    _isabelleOnlyTypes :: Bool
+  }
+  deriving stock (Data)
+
+makeLenses ''IsabelleOptions
+
+parseIsabelle :: Parser IsabelleOptions
+parseIsabelle = do
+  _isabelleOutputDir <-
+    parseGenericOutputDir
+      ( value "isabelle"
+          <> showDefault
+          <> help "Isabelle/HOL output directory."
+          <> action "directory"
+      )
+  _isabelleStdout <-
+    switch
+      ( long "stdout"
+          <> 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}

app/TopCommand.hs

@@ -10,6 +10,7 @@ import Commands.Eval qualified as Eval
 import Commands.Format qualified as Format
 import Commands.Html qualified as Html
 import Commands.Init qualified as Init
+import Commands.Isabelle qualified as Isabelle
 import Commands.Markdown qualified as Markdown
 import Commands.Repl qualified as Repl
 import Commands.Typecheck qualified as Typecheck
@@ -35,6 +36,7 @@ runTopCommand = \case
   DisplayNumericVersion -> runDisplayNumericVersion
   DisplayHelp -> showHelpText
   Doctor opts -> runLogIO (Doctor.runCommand opts)
+  Isabelle opts -> Isabelle.runCommand opts
   Init opts -> runLogIO (Init.init opts)
   Dev opts -> Dev.runCommand opts
   Typecheck opts -> Typecheck.runCommand opts

app/TopCommand/Options.hs

@@ -9,6 +9,7 @@ import Commands.Eval.Options
 import Commands.Format.Options
 import Commands.Html.Options
 import Commands.Init.Options
+import Commands.Isabelle.Options
 import Commands.Markdown.Options
 import Commands.Repl.Options
 import Commands.Typecheck.Options
@@ -27,6 +28,7 @@ data TopCommand
   | Eval EvalOptions
   | Html HtmlOptions
   | Markdown MarkdownOptions
+  | Isabelle IsabelleOptions
   | Dev Dev.DevCommand
   | Doctor DoctorOptions
   | Init InitOptions
@@ -198,6 +200,13 @@ commandMarkdown =
       (Markdown <$> parseJuvixMarkdown)
       (progDesc "Translate Juvix code blocks in a Markdown file to Markdown")
 
+commandIsabelle :: Mod CommandFields TopCommand
+commandIsabelle =
+  command "isabelle" $
+    info
+      (Isabelle <$> parseIsabelle)
+      (progDesc "Generate Isabelle/HOL types for a Juvix file")
+
 commandDev :: Mod CommandFields TopCommand
 commandDev =
   command "dev" $
@@ -215,7 +224,8 @@ parseCompilerCommand =
           commandCompile,
           commandEval,
           commandHtml,
-          commandMarkdown
+          commandMarkdown,
+          commandIsabelle
         ]
     )
 

cntlines.sh

@@ -35,6 +35,8 @@ PIPELINE=$(count src/Juvix/Compiler/Pipeline/)
 
 APP=$(count app/)
 HTML=$(count src/Juvix/Compiler/Backend/Html/)
+MARKDOWN=$(count src/Juvix/Compiler/Backend/Markdown/)
+ISABELLE=$(count src/Juvix/Compiler/Backend/Isabelle/)
 EXTRA=$(count src/Juvix/Extra/)
 DATA=$(count src/Juvix/Data/)
 PRELUDE=$(count src/Juvix/Prelude/)
@@ -42,7 +44,7 @@ STORE=$(count src/Juvix/Compiler/Store/)
 
 FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
 BACK=$((BACKENDC + BACKENDRUST + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
-OTHER=$((APP + STORE + HTML + EXTRA + DATA + PRELUDE))
+OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
 
 TOTAL=$((FRONT+BACK+OTHER+TESTS))
@@ -73,6 +75,8 @@ echo "Other: $OTHER LOC"
 echo "   Application: $APP LOC"
 echo "   Store: $STORE LOC"
 echo "   Html: $HTML LOC"
+echo "   Markdown: $MARKDOWN LOC"
+echo "   Isabelle: $ISABELLE LOC"
 echo "   Extra: $EXTRA LOC"
 echo "   Data: $DATA LOC"
 echo "   Prelude: $PRELUDE LOC"

src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs

@@ -0,0 +1,10 @@
+module Juvix.Compiler.Backend.Isabelle.Data.Result where
+
+import Juvix.Compiler.Backend.Isabelle.Language
+
+data Result = Result
+  { _resultTheory :: Theory,
+    _resultModuleId :: ModuleId
+  }
+
+makeLenses ''Result

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -0,0 +1,116 @@
+module Juvix.Compiler.Backend.Isabelle.Language
+  ( module Juvix.Compiler.Backend.Isabelle.Language,
+    module Juvix.Compiler.Internal.Data.Name,
+    module Juvix.Prelude,
+  )
+where
+
+import Juvix.Compiler.Internal.Data.Name
+import Juvix.Prelude
+
+data Type
+  = TyVar Var
+  | TyFun FunType
+  | TyInd IndApp
+  deriving stock (Eq)
+
+data Var = Var
+  { _varName :: Name
+  }
+  deriving stock (Eq)
+
+data FunType = FunType
+  { _funTypeLeft :: Type,
+    _funTypeRight :: Type
+  }
+  deriving stock (Eq)
+
+data Inductive
+  = IndBool
+  | IndNat
+  | IndInt
+  | IndList
+  | IndString
+  | IndUser Name
+  deriving stock (Eq)
+
+data IndApp = IndApp
+  { _indAppInductive :: Inductive,
+    _indAppParams :: [Type]
+  }
+  deriving stock (Eq)
+
+makeLenses ''Var
+makeLenses ''FunType
+makeLenses ''IndApp
+
+data Statement
+  = StmtDefinition Definition
+  | StmtFunction Function
+  | StmtSynonym Synonym
+  | StmtDatatype Datatype
+  | StmtRecord Record
+
+data Definition = Definition
+  { _definitionName :: Name,
+    _definitionType :: Type
+  }
+
+data Function = Function
+  { _functionName :: Name,
+    _functionType :: Type
+  }
+
+data Synonym = Synonym
+  { _synonymName :: Name,
+    _synonymType :: Type
+  }
+
+data Datatype = Datatype
+  { _datatypeName :: Name,
+    _datatypeParams :: [Var],
+    _datatypeConstructors :: [Constructor]
+  }
+
+data Constructor = Constructor
+  { _constructorName :: Name,
+    _constructorArgTypes :: [Type]
+  }
+
+data Record = Record
+  { _recordName :: Name,
+    _recordParams :: [Var],
+    _recordFields :: [RecordField]
+  }
+
+data RecordField = RecordField
+  { _recordFieldName :: Name,
+    _recordFieldType :: Type
+  }
+
+makeLenses ''Definition
+makeLenses ''Function
+makeLenses ''Synonym
+makeLenses ''Datatype
+makeLenses ''Constructor
+makeLenses ''Record
+makeLenses ''RecordField
+
+data Theory = Theory
+  { _theoryName :: Name,
+    _theoryImports :: [Name],
+    _theoryStatements :: [Statement]
+  }
+
+makeLenses ''Theory
+
+instance HasAtomicity Var where
+  atomicity _ = Atom
+
+instance HasAtomicity Type where
+  atomicity = \case
+    TyVar {} -> Atom
+    TyFun {} -> Aggregate funFixity
+    TyInd IndApp {..}
+      | null _indAppParams -> Atom
+      | otherwise -> Aggregate appFixity

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

@@ -0,0 +1,22 @@
+module Juvix.Compiler.Backend.Isabelle.Pretty where
+
+import Juvix.Compiler.Backend.Isabelle.Pretty.Base
+import Juvix.Compiler.Backend.Isabelle.Pretty.Options
+import Juvix.Data.PPOutput
+import Juvix.Prelude
+import Prettyprinter.Render.Terminal qualified as Ansi
+
+ppOutDefault :: (PrettyCode c) => c -> AnsiText
+ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
+
+ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
+ppOut o = mkAnsiText . PPOutput . doc (project o)
+
+ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text
+ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts)
+
+ppTrace :: (PrettyCode c) => c -> Text
+ppTrace = ppTrace' traceOptions
+
+ppPrint :: (PrettyCode c) => c -> Text
+ppPrint = show . ppOutDefault

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

@@ -0,0 +1,157 @@
+module Juvix.Compiler.Backend.Isabelle.Pretty.Base where
+
+import Juvix.Compiler.Backend.Isabelle.Language
+import Juvix.Compiler.Backend.Isabelle.Pretty.Keywords
+import Juvix.Compiler.Backend.Isabelle.Pretty.Options
+import Juvix.Data.CodeAnn
+
+arrow :: Doc Ann
+arrow = "⇒"
+
+class PrettyCode c where
+  ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
+
+doc :: (PrettyCode c) => Options -> c -> Doc Ann
+doc opts = run . runReader opts . ppCode
+
+ppCodeQuoted :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => c -> Sem r (Doc Ann)
+ppCodeQuoted c
+  | atomicity c == Atom = ppCode c
+  | otherwise = dquotes <$> ppCode c
+
+ppParams :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => [c] -> Sem r (Maybe (Doc Ann))
+ppParams = \case
+  [] -> return Nothing
+  [x] -> Just <$> ppRightExpression appFixity x
+  params -> do
+    ps <- mapM ppCode params
+    return $ Just $ parens (hsep (punctuate comma ps))
+
+instance PrettyCode Name where
+  ppCode = return . prettyName False
+
+instance PrettyCode Type where
+  ppCode = \case
+    TyVar v -> ppCode v
+    TyFun x -> ppCode x
+    TyInd x -> ppCode x
+
+instance PrettyCode Var where
+  ppCode Var {..} =
+    (squote <>) <$> ppCode _varName
+
+instance PrettyCode FunType where
+  ppCode FunType {..} = do
+    l <- ppLeftExpression funFixity _funTypeLeft
+    r <- ppRightExpression funFixity _funTypeRight
+    return $ l <+> arrow <+> r
+
+instance PrettyCode Inductive where
+  ppCode = \case
+    IndBool -> return $ primitive "bool"
+    IndNat -> return $ primitive "nat"
+    IndInt -> return $ primitive "int"
+    IndList -> return $ primitive "list"
+    IndString -> return $ primitive "string"
+    IndUser name -> ppCode name
+
+instance PrettyCode IndApp where
+  ppCode IndApp {..} = do
+    params <- ppParams _indAppParams
+    ind <- ppCode _indAppInductive
+    return $ params <?+> ind
+
+instance PrettyCode Statement where
+  ppCode = \case
+    StmtDefinition x -> ppCode x
+    StmtFunction x -> ppCode x
+    StmtSynonym x -> ppCode x
+    StmtDatatype x -> ppCode x
+    StmtRecord x -> ppCode x
+
+instance PrettyCode Definition where
+  ppCode Definition {..} = do
+    n <- ppCode _definitionName
+    ty <- ppCodeQuoted _definitionType
+    return $ kwDefinition <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "=" <+> kwUndefined)
+
+instance PrettyCode Function where
+  ppCode Function {..} = do
+    n <- ppCode _functionName
+    ty <- ppCodeQuoted _functionType
+    return $ kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> dquotes (n <+> "_" <+> "=" <+> kwUndefined)
+
+instance PrettyCode Synonym where
+  ppCode Synonym {..} = do
+    n <- ppCode _synonymName
+    ty <- ppCodeQuoted _synonymType
+    return $ kwTypeSynonym <+> n <+> "=" <+> ty
+
+instance PrettyCode Datatype where
+  ppCode Datatype {..} = do
+    n <- ppCode _datatypeName
+    params <- ppParams _datatypeParams
+    ctrs <- mapM ppCode _datatypeConstructors
+    return $ kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> vsep (punctuate "|" ctrs))
+
+instance PrettyCode Constructor where
+  ppCode Constructor {..} = do
+    n <- ppCode _constructorName
+    tys <- mapM ppCodeQuoted _constructorArgTypes
+    return $ hsep (n : tys)
+
+instance PrettyCode Record where
+  ppCode Record {..} = do
+    n <- ppCode _recordName
+    params <- ppParams _recordParams
+    fields <- mapM ppCode _recordFields
+    return $ kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
+
+instance PrettyCode RecordField where
+  ppCode RecordField {..} = do
+    n <- ppCode _recordFieldName
+    ty <- ppCodeQuoted _recordFieldType
+    return $ n <+> "::" <+> ty
+
+instance PrettyCode Theory where
+  ppCode Theory {..} = do
+    n <- ppCode _theoryName
+    stmts <- mapM ppCode _theoryStatements
+    return $
+      kwTheory
+        <+> n
+          <> line
+          <> kwImports
+        <+> "Main"
+          <> line
+          <> kwBegin
+          <> line
+          <> line
+          <> vsep (punctuate line stmts)
+          <> line
+          <> line
+          <> kwEnd
+
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppRightExpression = ppLRExpression isRightAssoc
+
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLeftExpression = ppLRExpression isLeftAssoc
+
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLRExpression associates fixlr e =
+  parensCond (atomParens associates (atomicity e) fixlr)
+    <$> ppCode e

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

@@ -0,0 +1,30 @@
+module Juvix.Compiler.Backend.Isabelle.Pretty.Keywords where
+
+import Juvix.Data.CodeAnn
+
+kwDefinition :: Doc Ann
+kwDefinition = keyword "definition"
+
+kwFun :: Doc Ann
+kwFun = keyword "fun"
+
+kwTypeSynonym :: Doc Ann
+kwTypeSynonym = keyword "type_synonym"
+
+kwDatatype :: Doc Ann
+kwDatatype = keyword "datatype"
+
+kwRecord :: Doc Ann
+kwRecord = keyword "record"
+
+kwUndefined :: Doc Ann
+kwUndefined = keyword "undefined"
+
+kwTheory :: Doc Ann
+kwTheory = keyword "theory"
+
+kwImports :: Doc Ann
+kwImports = keyword "imports"
+
+kwBegin :: Doc Ann
+kwBegin = keyword "begin"

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

@@ -0,0 +1,19 @@
+module Juvix.Compiler.Backend.Isabelle.Pretty.Options where
+
+import Juvix.Prelude
+
+data Options = Options
+
+makeLenses ''Options
+
+defaultOptions :: Options
+defaultOptions = Options
+
+traceOptions :: Options
+traceOptions = defaultOptions
+
+fromGenericOptions :: GenericOptions -> Options
+fromGenericOptions _ = defaultOptions
+
+instance CanonicalProjection GenericOptions Options where
+  project = fromGenericOptions

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

@@ -0,0 +1,216 @@
+module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text qualified as T
+import Juvix.Compiler.Backend.Isabelle.Data.Result
+import Juvix.Compiler.Backend.Isabelle.Language
+import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
+import Juvix.Compiler.Internal.Extra qualified as Internal
+import Juvix.Compiler.Internal.Pretty qualified as Internal
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
+import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Compiler.Store.Extra
+import Juvix.Compiler.Store.Language
+import Juvix.Extra.Paths qualified as P
+
+fromInternal ::
+  forall r.
+  (Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) =>
+  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 onlyTypes table _resultModule
+  where
+    go :: Bool -> Internal.InfoTable -> Internal.Module -> Sem r Result
+    go onlyTypes tab md =
+      return $
+        Result
+          { _resultTheory = goModule onlyTypes tab md,
+            _resultModuleId = md ^. Internal.moduleId
+          }
+
+goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
+goModule onlyTypes infoTable Internal.Module {..} =
+  Theory
+    { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
+      _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
+      _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
+    }
+  where
+    toIsabelleName :: Text -> Text
+    toIsabelleName name = case reverse $ filter (/= "") $ T.splitOn "." name of
+      h : _ -> h
+      [] -> impossible
+
+    isTypeDef :: Statement -> Bool
+    isTypeDef = \case
+      StmtDefinition {} -> False
+      StmtFunction {} -> False
+      StmtSynonym {} -> True
+      StmtDatatype {} -> True
+      StmtRecord {} -> True
+
+    goMutualBlock :: Internal.MutualBlock -> [Statement]
+    goMutualBlock Internal.MutualBlock {..} =
+      filter (\stmt -> not onlyTypes || isTypeDef stmt) $
+        map goMutualStatement (toList _mutualStatements)
+
+    goMutualStatement :: Internal.MutualStatement -> Statement
+    goMutualStatement = \case
+      Internal.StatementInductive x -> goInductiveDef x
+      Internal.StatementFunction x -> goFunctionDef x
+      Internal.StatementAxiom x -> goAxiomDef x
+
+    goInductiveDef :: Internal.InductiveDef -> Statement
+    goInductiveDef Internal.InductiveDef {..}
+      | length _inductiveConstructors == 1
+          && head' _inductiveConstructors ^. Internal.inductiveConstructorIsRecord =
+          let tyargs = fst $ Internal.unfoldFunType $ head' _inductiveConstructors ^. Internal.inductiveConstructorType
+           in StmtRecord
+                Record
+                  { _recordName = _inductiveName,
+                    _recordParams = params,
+                    _recordFields = map goRecordField tyargs
+                  }
+      | otherwise =
+          StmtDatatype
+            Datatype
+              { _datatypeName = _inductiveName,
+                _datatypeParams = params,
+                _datatypeConstructors = map goConstructorDef _inductiveConstructors
+              }
+      where
+        params = map goInductiveParameter _inductiveParameters
+
+    goInductiveParameter :: Internal.InductiveParameter -> Var
+    goInductiveParameter Internal.InductiveParameter {..} = Var _inductiveParamName
+
+    goRecordField :: Internal.FunctionParameter -> RecordField
+    goRecordField Internal.FunctionParameter {..} =
+      RecordField
+        { _recordFieldName = fromMaybe defaultName _paramName,
+          _recordFieldType = goType _paramType
+        }
+      where
+        defaultName =
+          Name
+            { _nameText = "_",
+              _nameId = defaultId,
+              _nameKind = KNameLocal,
+              _namePretty = "",
+              _nameLoc = defaultLoc,
+              _nameFixity = Nothing
+            }
+        defaultLoc = singletonInterval $ mkInitialLoc P.noFile
+        defaultId =
+          NameId
+            { _nameIdUid = 0,
+              _nameIdModuleId = ModuleId "" "" ""
+            }
+
+    goConstructorDef :: Internal.ConstructorDef -> Constructor
+    goConstructorDef Internal.ConstructorDef {..} =
+      Constructor
+        { _constructorName = _inductiveConstructorName,
+          _constructorArgTypes = tyargs
+        }
+      where
+        tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
+
+    goDef :: Name -> Internal.Expression -> Maybe Internal.Expression -> Statement
+    goDef name ty body = case ty of
+      Internal.ExpressionUniverse {} ->
+        StmtSynonym
+          Synonym
+            { _synonymName = name,
+              _synonymType = goType $ fromMaybe (error "unsupported axiomatic type") body
+            }
+      _
+        | argsNum == 0 ->
+            StmtDefinition
+              Definition
+                { _definitionName = name,
+                  _definitionType = goType ty
+                }
+        | otherwise ->
+            StmtFunction
+              Function
+                { _functionName = name,
+                  _functionType = goType ty
+                }
+      where
+        argsNum = length $ fst $ Internal.unfoldFunType ty
+
+    goFunctionDef :: Internal.FunctionDef -> Statement
+    goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType (Just _funDefBody)
+
+    goAxiomDef :: Internal.AxiomDef -> Statement
+    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType Nothing
+
+    goType :: Internal.Expression -> Type
+    goType ty = case ty of
+      Internal.ExpressionIden x -> goTypeIden x
+      Internal.ExpressionApplication x -> goTypeApp x
+      Internal.ExpressionFunction x -> goTypeFun x
+      Internal.ExpressionLiteral {} -> unsupportedType ty
+      Internal.ExpressionHole {} -> unsupportedType ty
+      Internal.ExpressionInstanceHole {} -> unsupportedType ty
+      Internal.ExpressionLet {} -> unsupportedType ty
+      Internal.ExpressionUniverse {} -> unsupportedType ty
+      Internal.ExpressionSimpleLambda {} -> unsupportedType ty
+      Internal.ExpressionLambda {} -> unsupportedType ty
+      Internal.ExpressionCase {} -> unsupportedType ty
+      where
+        unsupportedType :: Internal.Expression -> a
+        unsupportedType e = error ("unsupported type: " <> Internal.ppTrace e)
+
+    mkIndType :: Name -> [Type] -> Type
+    mkIndType name params = TyInd $ IndApp ind params
+      where
+        ind = case HashMap.lookup name (infoTable ^. Internal.infoInductives) of
+          Just ii -> case ii ^. Internal.inductiveInfoBuiltin of
+            Just Internal.BuiltinBool -> IndBool
+            Just Internal.BuiltinNat -> IndNat
+            Just Internal.BuiltinInt -> IndInt
+            Just Internal.BuiltinList -> IndList
+            _ -> IndUser name
+          Nothing -> case HashMap.lookup name (infoTable ^. Internal.infoAxioms) of
+            Just ai -> case ai ^. Internal.axiomInfoDef . Internal.axiomBuiltin of
+              Just Internal.BuiltinString -> IndString
+              _ -> IndUser name
+            Nothing -> IndUser name
+
+    goTypeIden :: Internal.Iden -> Type
+    goTypeIden = \case
+      Internal.IdenFunction name -> mkIndType name []
+      Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
+      Internal.IdenVar name -> TyVar $ Var name
+      Internal.IdenAxiom name -> mkIndType name []
+      Internal.IdenInductive name -> mkIndType name []
+
+    goTypeApp :: Internal.Application -> Type
+    goTypeApp app = mkIndType name params
+      where
+        (ind, args) = Internal.unfoldApplication app
+        params = map goType (toList args)
+        name = case ind of
+          Internal.ExpressionIden (Internal.IdenFunction n) -> n
+          Internal.ExpressionIden (Internal.IdenAxiom n) -> n
+          Internal.ExpressionIden (Internal.IdenInductive n) -> n
+          _ -> error ("unsupported type: " <> Internal.ppTrace app)
+
+    goTypeFun :: Internal.Function -> Type
+    goTypeFun Internal.Function {..} = case lty of
+      Internal.ExpressionUniverse {} -> goType _functionRight
+      _ ->
+        TyFun $ FunType (goType lty) (goType _functionRight)
+      where
+        lty = _functionLeft ^. Internal.paramType

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -257,6 +257,7 @@ instance HasExpressions ConstructorDef where
       ConstructorDef
         { _inductiveConstructorType = ty',
           _inductiveConstructorName,
+          _inductiveConstructorIsRecord,
           _inductiveConstructorPragmas
         }
 

src/Juvix/Compiler/Internal/Language.hs

@@ -372,6 +372,7 @@ data InductiveDef = InductiveDef
 data ConstructorDef = ConstructorDef
   { _inductiveConstructorName :: ConstrName,
     _inductiveConstructorType :: Expression,
+    _inductiveConstructorIsRecord :: Bool,
     _inductiveConstructorPragmas :: Pragmas
   }
   deriving stock (Data)

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -627,6 +627,7 @@ goConstructorDef retTy ConstructorDef {..} = do
     Internal.ConstructorDef
       { _inductiveConstructorType = ty',
         _inductiveConstructorName = goSymbol _constructorName,
+        _inductiveConstructorIsRecord = isRhsRecord _constructorRhs,
         _inductiveConstructorPragmas = pragmas'
       }
   where
@@ -672,6 +673,12 @@ goConstructorDef retTy ConstructorDef {..} = do
       ConstructorRhsRecord r -> goRecordType r
       ConstructorRhsAdt r -> goAdtType r
 
+    isRhsRecord :: Concrete.ConstructorRhs 'Scoped -> Bool
+    isRhsRecord = \case
+      ConstructorRhsGadt {} -> False
+      ConstructorRhsRecord {} -> True
+      ConstructorRhsAdt {} -> False
+
 goLiteral :: LiteralLoc -> Internal.LiteralLoc
 goLiteral = fmap go
   where

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -214,6 +214,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
             ConstructorDef
               { _inductiveConstructorType = cty',
                 _inductiveConstructorName,
+                _inductiveConstructorIsRecord,
                 _inductiveConstructorPragmas
               }
       registerConstructor c'

src/Juvix/Compiler/Pipeline.hs

@@ -17,6 +17,8 @@ import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Backend.Cairo qualified as Cairo
 import Juvix.Compiler.Backend.Geb qualified as Geb
+import Juvix.Compiler.Backend.Isabelle.Data.Result qualified as Isabelle
+import Juvix.Compiler.Backend.Isabelle.Translation.FromTyped qualified as Isabelle
 import Juvix.Compiler.Backend.Rust.Translation.FromReg qualified as Rust
 import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
 import Juvix.Compiler.Casm.Data.Builtins qualified as Casm
@@ -126,6 +128,11 @@ upToInternalTyped ::
   Sem r Internal.InternalTypedResult
 upToInternalTyped = Internal.typeCheckingNew upToInternal
 
+upToIsabelle ::
+  (Members '[HighlightBuilder, Reader Parser.ParserResult, Error JuvixError, Reader EntryPoint, Reader Store.ModuleTable, NameIdGen] r) =>
+  Sem r Isabelle.Result
+upToIsabelle = upToInternalTyped >>= Isabelle.fromInternal
+
 upToCore ::
   (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError] r) =>
   Sem r Core.CoreResult

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

src/Juvix/Data/FileExt.hs

@@ -83,6 +83,9 @@ htmlFileExt = ".html"
 markdownFileExt :: (IsString a) => a
 markdownFileExt = ".md"
 
+isabelleFileExt :: (IsString a) => a
+isabelleFileExt = ".thy"
+
 cFileExt :: (IsString a) => a
 cFileExt = ".c"
 

src/Juvix/Prelude/Prepath.hs

@@ -19,15 +19,19 @@ import Juvix.Prelude.Pretty
 import System.Directory (getHomeDirectory)
 import System.Directory qualified as System
 import System.Environment
+import Prelude (show)
 
 -- | A file/directory path that may contain environmental variables
 newtype Prepath d = Prepath
   { _prepath :: String
   }
-  deriving stock (Show, Eq, Data, Generic)
+  deriving stock (Eq, Data, Generic)
 
 makeLenses ''Prepath
 
+instance Show (Prepath d) where
+  show Prepath {..} = _prepath
+
 type PrepathParts = NonEmpty PrepathPart
 
 data PrepathPart