From 66d954c2919f2c37b053cac3478c7d6de3760637 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 22 Apr 2024 17:41:46 +0200
Subject: [PATCH 01/14] isabelle language

---
 .../Compiler/Backend/Isabelle/Language.hs     | 86 +++++++++++++++++++
 .../Backend/Isabelle/Translation/FromTyped.hs |  1 +
 2 files changed, 87 insertions(+)
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Language.hs
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
new file mode 100644
index 0000000000..0b31f039e3
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -0,0 +1,86 @@
+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
+  | TyBool
+  | TyNat
+  | TyInt
+  | TyFun FunType
+  | TyInd IndApp
+  deriving stock (Eq)
+
+data Var = Var
+  { _varName :: Text
+  }
+  deriving stock (Eq)
+
+data FunType = FunType
+  { _funTypeLeft :: Type,
+    _funTypeRight :: Type
+  }
+  deriving stock (Eq)
+
+data IndApp = IndApp
+  { _indAppInductive :: Name,
+    _indAppParams :: [Type]
+  }
+  deriving stock (Eq)
+
+makeLenses ''Var
+makeLenses ''FunType
+makeLenses ''IndApp
+
+data Statement
+  = StmtDefinition Definition
+  | StmtFunction Function
+  | StmtDatatype Datatype
+  | StmtSynonym Synonym
+
+data Definition = Definition
+  { _definitionName :: Name,
+    _definitionType :: Type
+  }
+
+data Function = Function
+  { _functionName :: Name,
+    _functionType :: Type
+  }
+
+data Datatype = Datatype
+  { _datatypeName :: Name,
+    _datatypeParams :: [Var],
+    _datatypeConstructors :: [Constructor]
+  }
+
+data Constructor = Constructor
+  { _constructorName :: Name,
+    _constructorType :: Type,
+    _constructorFixity :: Maybe Fixity
+  }
+
+data Synonym = Synonym
+  { _synonymName :: Name,
+    _synonymType :: Type
+  }
+
+makeLenses ''Definition
+makeLenses ''Function
+makeLenses ''Datatype
+makeLenses ''Constructor
+makeLenses ''Synonym
+
+data Theory = Theory
+  { _theoryName :: Name,
+    _theoryImports :: [Name],
+    _theoryStatements :: [Statement]
+  }
+
+makeLenses ''Theory
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
new file mode 100644
index 0000000000..71424506ca
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -0,0 +1 @@
+module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where

From ff4917b811cc2995eca1fb00a8a7790a39b0a28d Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 22 Apr 2024 19:12:45 +0200
Subject: [PATCH 02/14] pretty printing

---
 .../Compiler/Backend/Isabelle/Language.hs     |  15 +-
 src/Juvix/Compiler/Backend/Isabelle/Pretty.hs |  22 +++
 .../Compiler/Backend/Isabelle/Pretty/Base.hs  | 140 ++++++++++++++++++
 .../Backend/Isabelle/Pretty/Keywords.hs       |  27 ++++
 .../Backend/Isabelle/Pretty/Options.hs        |  19 +++
 5 files changed, 221 insertions(+), 2 deletions(-)
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Pretty.hs
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
index 0b31f039e3..86bb0590b4 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -18,7 +18,7 @@ data Type
   deriving stock (Eq)
 
 data Var = Var
-  { _varName :: Text
+  { _varName :: Name
   }
   deriving stock (Eq)
 
@@ -62,7 +62,7 @@ data Datatype = Datatype
 
 data Constructor = Constructor
   { _constructorName :: Name,
-    _constructorType :: Type,
+    _constructorArgTypes :: [Type],
     _constructorFixity :: Maybe Fixity
   }
 
@@ -84,3 +84,14 @@ data Theory = Theory
   }
 
 makeLenses ''Theory
+
+instance HasAtomicity Type where
+  atomicity = \case
+    TyVar {} -> Atom
+    TyBool -> Atom
+    TyNat -> Atom
+    TyInt -> Atom
+    TyFun {} -> Aggregate funFixity
+    TyInd IndApp {..}
+      | null _indAppParams -> Atom
+      | otherwise -> Aggregate appFixity
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs
new file mode 100644
index 0000000000..b9989c1845
--- /dev/null
+++ b/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
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
new file mode 100644
index 0000000000..b46fddd77e
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -0,0 +1,140 @@
+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
+
+instance PrettyCode Name where
+  ppCode = return . prettyName False
+
+{-------------------------------------------------------------------}
+
+instance PrettyCode Type where
+  ppCode = \case
+    TyVar v -> ppCode v
+    TyBool -> return $ primitive "bool"
+    TyNat -> return $ primitive "nat"
+    TyInt -> return $ primitive "int"
+    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 IndApp where
+  ppCode IndApp {..} = do
+    params <- mapM ppCode _indAppParams
+    ind <- ppCode _indAppInductive
+    return $ hsep (params ++ [ind])
+
+{-------------------------------------------------------------------}
+
+instance PrettyCode Statement where
+  ppCode = \case
+    StmtDefinition x -> ppCode x
+    StmtFunction x -> ppCode x
+    StmtDatatype x -> ppCode x
+    StmtSynonym 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 Datatype where
+  ppCode Datatype {..} = do
+    n <- ppCode _datatypeName
+    params <- mapM ppCode _datatypeParams
+    ctrs <- mapM ppCode _datatypeConstructors
+    return $ kwDatatype <+> hsep (params ++ [n]) <> line <> "=" <+> vsep (punctuate "|" ctrs)
+
+instance PrettyCode Constructor where
+  ppCode Constructor {..} = do
+    n <- ppCode _constructorName
+    tys <- mapM ppCodeQuoted _constructorArgTypes
+    return $ hsep (n : tys)
+
+instance PrettyCode Synonym where
+  ppCode Synonym {..} = do
+    n <- ppCode _synonymName
+    ty <- ppCodeQuoted _synonymType
+    return $ kwTypeSynonym <+> n <+> "=" <+> ty
+
+{-------------------------------------------------------------------}
+
+instance PrettyCode Theory where
+  ppCode Theory {..} = do
+    n <- ppCode _theoryName
+    imps <- mapM ppCode _theoryImports
+    stmts <- mapM ppCode _theoryStatements
+    return $
+      kwTheory
+        <+> n
+          <> line
+          <> kwImports
+        <+> hsep ("Main" : imps)
+          <> line
+          <> kwBegin
+          <> line
+          <> line
+          <> vsep 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
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
new file mode 100644
index 0000000000..f0c227ce59
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
@@ -0,0 +1,27 @@
+module Juvix.Compiler.Backend.Isabelle.Pretty.Keywords where
+
+import Juvix.Data.CodeAnn
+
+kwDefinition :: Doc Ann
+kwDefinition = keyword "definition"
+
+kwFun :: Doc Ann
+kwFun = keyword "fun"
+
+kwDatatype :: Doc Ann
+kwDatatype = keyword "datatype"
+
+kwTypeSynonym :: Doc Ann
+kwTypeSynonym = keyword "type_synonym"
+
+kwUndefined :: Doc Ann
+kwUndefined = keyword "undefined"
+
+kwTheory :: Doc Ann
+kwTheory = keyword "theory"
+
+kwImports :: Doc Ann
+kwImports = keyword "imports"
+
+kwBegin :: Doc Ann
+kwBegin = keyword "begin"
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Options.hs
new file mode 100644
index 0000000000..0d60385755
--- /dev/null
+++ b/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

From 524dd9e40d9e58690f4e9142eaecf874d3d723bc Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 23 Apr 2024 10:26:49 +0200
Subject: [PATCH 03/14] remove sections

---
 src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index b46fddd77e..03e6b68936 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -8,8 +8,6 @@ import Juvix.Data.CodeAnn
 arrow :: Doc Ann
 arrow = "⇒"
 
-{-------------------------------------------------------------------}
-
 class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
 
@@ -24,8 +22,6 @@ ppCodeQuoted c
 instance PrettyCode Name where
   ppCode = return . prettyName False
 
-{-------------------------------------------------------------------}
-
 instance PrettyCode Type where
   ppCode = \case
     TyVar v -> ppCode v
@@ -51,8 +47,6 @@ instance PrettyCode IndApp where
     ind <- ppCode _indAppInductive
     return $ hsep (params ++ [ind])
 
-{-------------------------------------------------------------------}
-
 instance PrettyCode Statement where
   ppCode = \case
     StmtDefinition x -> ppCode x
@@ -91,8 +85,6 @@ instance PrettyCode Synonym where
     ty <- ppCodeQuoted _synonymType
     return $ kwTypeSynonym <+> n <+> "=" <+> ty
 
-{-------------------------------------------------------------------}
-
 instance PrettyCode Theory where
   ppCode Theory {..} = do
     n <- ppCode _theoryName
@@ -113,8 +105,6 @@ instance PrettyCode Theory where
           <> line
           <> kwEnd
 
-{-------------------------------------------------------------------}
-
 ppRightExpression ::
   (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
   Fixity ->

From a0e1b32a067920b25137346ec140c08d19348eb6 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 23 Apr 2024 16:49:21 +0200
Subject: [PATCH 04/14] translation

---
 .../Compiler/Backend/Isabelle/Language.hs     |  30 +++-
 .../Compiler/Backend/Isabelle/Pretty/Base.hs  |  42 +++--
 .../Backend/Isabelle/Pretty/Keywords.hs       |   7 +-
 .../Backend/Isabelle/Translation/FromTyped.hs | 152 ++++++++++++++++++
 src/Juvix/Compiler/Internal/Extra/Base.hs     |   1 +
 src/Juvix/Compiler/Internal/Language.hs       |   1 +
 .../Internal/Translation/FromConcrete.hs      |   7 +
 .../Analysis/TypeChecking/CheckerNew.hs       |   1 +
 8 files changed, 222 insertions(+), 19 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
index 86bb0590b4..c1ce9885ba 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -41,8 +41,9 @@ makeLenses ''IndApp
 data Statement
   = StmtDefinition Definition
   | StmtFunction Function
-  | StmtDatatype Datatype
   | StmtSynonym Synonym
+  | StmtDatatype Datatype
+  | StmtRecord Record
 
 data Definition = Definition
   { _definitionName :: Name,
@@ -54,6 +55,11 @@ data Function = Function
     _functionType :: Type
   }
 
+data Synonym = Synonym
+  { _synonymName :: Name,
+    _synonymType :: Type
+  }
+
 data Datatype = Datatype
   { _datatypeName :: Name,
     _datatypeParams :: [Var],
@@ -62,20 +68,27 @@ data Datatype = Datatype
 
 data Constructor = Constructor
   { _constructorName :: Name,
-    _constructorArgTypes :: [Type],
-    _constructorFixity :: Maybe Fixity
+    _constructorArgTypes :: [Type]
   }
 
-data Synonym = Synonym
-  { _synonymName :: Name,
-    _synonymType :: 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 ''Synonym
+makeLenses ''Record
+makeLenses ''RecordField
 
 data Theory = Theory
   { _theoryName :: Name,
@@ -85,6 +98,9 @@ data Theory = Theory
 
 makeLenses ''Theory
 
+instance HasAtomicity Var where
+  atomicity _ = Atom
+
 instance HasAtomicity Type where
   atomicity = \case
     TyVar {} -> Atom
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index 03e6b68936..ed6cecfb8a 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -19,6 +19,14 @@ 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
 
@@ -43,16 +51,17 @@ instance PrettyCode FunType where
 
 instance PrettyCode IndApp where
   ppCode IndApp {..} = do
-    params <- mapM ppCode _indAppParams
+    params <- ppParams _indAppParams
     ind <- ppCode _indAppInductive
-    return $ hsep (params ++ [ind])
+    return $ params <?+> ind
 
 instance PrettyCode Statement where
   ppCode = \case
     StmtDefinition x -> ppCode x
     StmtFunction x -> ppCode x
-    StmtDatatype x -> ppCode x
     StmtSynonym x -> ppCode x
+    StmtDatatype x -> ppCode x
+    StmtRecord x -> ppCode x
 
 instance PrettyCode Definition where
   ppCode Definition {..} = do
@@ -66,12 +75,18 @@ instance PrettyCode Function where
     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 <- mapM ppCode _datatypeParams
+    params <- ppParams _datatypeParams
     ctrs <- mapM ppCode _datatypeConstructors
-    return $ kwDatatype <+> hsep (params ++ [n]) <> line <> "=" <+> vsep (punctuate "|" ctrs)
+    return $ kwDatatype <+> params <?+> n <> line <> indent' ("=" <+> vsep (punctuate "|" ctrs))
 
 instance PrettyCode Constructor where
   ppCode Constructor {..} = do
@@ -79,11 +94,18 @@ instance PrettyCode Constructor where
     tys <- mapM ppCodeQuoted _constructorArgTypes
     return $ hsep (n : tys)
 
-instance PrettyCode Synonym where
-  ppCode Synonym {..} = do
-    n <- ppCode _synonymName
-    ty <- ppCodeQuoted _synonymType
-    return $ kwTypeSynonym <+> n <+> "=" <+> ty
+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
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
index f0c227ce59..553c37d59e 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Keywords.hs
@@ -8,11 +8,14 @@ kwDefinition = keyword "definition"
 kwFun :: Doc Ann
 kwFun = keyword "fun"
 
+kwTypeSynonym :: Doc Ann
+kwTypeSynonym = keyword "type_synonym"
+
 kwDatatype :: Doc Ann
 kwDatatype = keyword "datatype"
 
-kwTypeSynonym :: Doc Ann
-kwTypeSynonym = keyword "type_synonym"
+kwRecord :: Doc Ann
+kwRecord = keyword "record"
 
 kwUndefined :: Doc Ann
 kwUndefined = keyword "undefined"
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 71424506ca..26dffa4a98 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -1 +1,153 @@
 module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
+
+import Juvix.Compiler.Backend.Isabelle.Language
+import Juvix.Compiler.Internal.Extra qualified as Internal
+import Juvix.Compiler.Internal.Pretty qualified as Internal
+import Juvix.Extra.Paths qualified as P
+
+fromInternal :: Internal.Module -> Theory
+fromInternal Internal.Module {..} =
+  Theory
+    { _theoryName = _moduleName,
+      _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
+      _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
+    }
+
+goMutualBlock :: Internal.MutualBlock -> [Statement]
+goMutualBlock Internal.MutualBlock {..} = 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)
+
+goFunctionDef :: Internal.FunctionDef -> Statement
+goFunctionDef Internal.FunctionDef {..}
+  | null _funDefArgsInfo =
+      StmtDefinition
+        Definition
+          { _definitionName = _funDefName,
+            _definitionType = goType _funDefType
+          }
+  | otherwise =
+      StmtFunction
+        Function
+          { _functionName = _funDefName,
+            _functionType = goType _funDefType
+          }
+
+goAxiomDef :: Internal.AxiomDef -> Statement
+goAxiomDef Internal.AxiomDef {..}
+  | argsNum == 0 =
+      StmtDefinition
+        Definition
+          { _definitionName = _axiomName,
+            _definitionType = goType _axiomType
+          }
+  | otherwise =
+      StmtFunction
+        Function
+          { _functionName = _axiomName,
+            _functionType = goType _axiomType
+          }
+  where
+    argsNum = length $ fst $ Internal.unfoldFunType _axiomType
+
+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)
+
+goTypeIden :: Internal.Iden -> Type
+goTypeIden = \case
+  Internal.IdenFunction name -> TyInd $ IndApp name []
+  Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
+  Internal.IdenVar name -> TyVar $ Var name
+  Internal.IdenAxiom name -> TyInd $ IndApp name []
+  Internal.IdenInductive name -> TyInd $ IndApp name []
+
+goTypeApp :: Internal.Application -> Type
+goTypeApp app = TyInd $ IndApp 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 {..} = TyFun $ FunType l r
+  where
+    l = goType (_functionLeft ^. Internal.paramType)
+    r = goType _functionRight
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index f39e11c327..b3c113a5ec 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -257,6 +257,7 @@ instance HasExpressions ConstructorDef where
       ConstructorDef
         { _inductiveConstructorType = ty',
           _inductiveConstructorName,
+          _inductiveConstructorIsRecord,
           _inductiveConstructorPragmas
         }
 
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 2c92e21ce4..56adff502d 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/src/Juvix/Compiler/Internal/Language.hs
@@ -330,6 +330,7 @@ data InductiveDef = InductiveDef
 data ConstructorDef = ConstructorDef
   { _inductiveConstructorName :: ConstrName,
     _inductiveConstructorType :: Expression,
+    _inductiveConstructorIsRecord :: Bool,
     _inductiveConstructorPragmas :: Pragmas
   }
   deriving stock (Data)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index ebcfc947f4..46d1e56dd5 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -623,6 +623,7 @@ goConstructorDef retTy ConstructorDef {..} = do
     Internal.ConstructorDef
       { _inductiveConstructorType = ty',
         _inductiveConstructorName = goSymbol _constructorName,
+        _inductiveConstructorIsRecord = isRhsRecord _constructorRhs,
         _inductiveConstructorPragmas = pragmas'
       }
   where
@@ -668,6 +669,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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
index d016e3cb0b..fc9fddd701 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -215,6 +215,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
             ConstructorDef
               { _inductiveConstructorType = cty',
                 _inductiveConstructorName,
+                _inductiveConstructorIsRecord,
                 _inductiveConstructorPragmas
               }
       registerConstructor c'

From 0f930bbfed1fa8bb96e10f09bb3ba3cf0ed45af5 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 23 Apr 2024 17:18:17 +0200
Subject: [PATCH 05/14] update cntlines.sh

---
 cntlines.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/cntlines.sh b/cntlines.sh
index bd1e078c68..559ec20f10 100755
--- a/cntlines.sh
+++ b/cntlines.sh
@@ -17,6 +17,7 @@ RUNTIME_CASM=$(count_ext '*.casm' runtime/casm)
 RUNTIME=$((RUNTIME_C+RUNTIME_RUST+RUNTIME_VAMPIR+RUNTIME_JVT+RUNTIME_CASM))
 
 BACKENDC=$(count src/Juvix/Compiler/Backend/C/)
+ISABELLE=$(count src/Juvix/Compiler/Backend/Isabelle/)
 CAIRO=$(count src/Juvix/Compiler/Backend/Cairo/)
 GEB=$(count src/Juvix/Compiler/Backend/Geb/)
 VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/)
@@ -40,7 +41,7 @@ PRELUDE=$(count src/Juvix/Prelude/)
 STORE=$(count src/Juvix/Compiler/Store/)
 
 FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
-BACK=$((BACKENDC + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
+BACK=$((BACKENDC + GEB + VAMPIR + NOCK + ISABELLE + REG + ASM + TREE + CORE + CASM + CAIRO))
 OTHER=$((APP + STORE + HTML + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
 
@@ -57,6 +58,7 @@ echo "   GEB backend: $GEB LOC"
 echo "   C backend: $BACKENDC LOC"
 echo "   Cairo backend: $((CASM + CAIRO)) LOC"
 echo "   Nockma backend: $NOCK LOC"
+echo "   Isabelle backend: $ISABELLE LOC"
 echo "   JuvixReg: $REG LOC"
 echo "   JuvixAsm: $ASM LOC"
 echo "   JuvixTree: $TREE LOC"

From 7d756416f91f8b3bc01387e88fe3b70c7fb8cbdf Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 23 Apr 2024 18:44:15 +0200
Subject: [PATCH 06/14] CLI

---
 app/Commands/Isabelle.hs                      | 18 ++++++++++++
 app/Commands/Isabelle/Options.hs              | 29 +++++++++++++++++++
 app/TopCommand.hs                             |  2 ++
 app/TopCommand/Options.hs                     | 12 +++++++-
 cntlines.sh                                   | 10 ++++---
 .../Compiler/Backend/Isabelle/Pretty/Base.hs  |  2 +-
 .../Backend/Isabelle/Translation/FromTyped.hs |  4 ++-
 7 files changed, 70 insertions(+), 7 deletions(-)
 create mode 100644 app/Commands/Isabelle.hs
 create mode 100644 app/Commands/Isabelle/Options.hs

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
new file mode 100644
index 0000000000..23c47842ec
--- /dev/null
+++ b/app/Commands/Isabelle.hs
@@ -0,0 +1,18 @@
+module Commands.Isabelle where
+
+import Commands.Base
+import Commands.Isabelle.Options
+import Juvix.Compiler.Backend.Isabelle.Pretty
+import Juvix.Compiler.Backend.Isabelle.Translation.FromTyped
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
+
+runCommand ::
+  (Members '[EmbedIO, TaggedLock, App] r) =>
+  IsabelleOptions ->
+  Sem r ()
+runCommand opts = do
+  let inputFile = opts ^. isabelleInputFile
+  res <- runPipelineNoOptions inputFile upToInternalTyped
+  let md = res ^. resultModule
+  renderStdOut (ppOutDefault (fromInternal md))
+  putStrLn ""
diff --git a/app/Commands/Isabelle/Options.hs b/app/Commands/Isabelle/Options.hs
new file mode 100644
index 0000000000..ca14968d44
--- /dev/null
+++ b/app/Commands/Isabelle/Options.hs
@@ -0,0 +1,29 @@
+module Commands.Isabelle.Options where
+
+import CommonOptions
+
+data IsabelleOptions = IsabelleOptions
+  { _isabelleInputFile :: Maybe (AppPath File),
+    _isabelleOutputDir :: AppPath Dir,
+    _isabelleRecursive :: Bool
+  }
+  deriving stock (Data)
+
+makeLenses ''IsabelleOptions
+
+parseIsabelle :: Parser IsabelleOptions
+parseIsabelle = do
+  _isabelleRecursive <-
+    switch
+      ( long "recursive"
+          <> help "Process imported modules recursively"
+      )
+  _isabelleOutputDir <-
+    parseGenericOutputDir
+      ( value "isabelle"
+          <> showDefault
+          <> help "Isabelle/HOL output directory"
+          <> action "directory"
+      )
+  _isabelleInputFile <- optional (parseInputFile FileExtJuvix)
+  pure IsabelleOptions {..}
diff --git a/app/TopCommand.hs b/app/TopCommand.hs
index 98f21b6ec1..5c7ab1c89d 100644
--- a/app/TopCommand.hs
+++ b/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
diff --git a/app/TopCommand/Options.hs b/app/TopCommand/Options.hs
index 9c56d1ed64..4aef6749ea 100644
--- a/app/TopCommand/Options.hs
+++ b/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
         ]
     )
 
diff --git a/cntlines.sh b/cntlines.sh
index 559ec20f10..646e4977e4 100755
--- a/cntlines.sh
+++ b/cntlines.sh
@@ -17,7 +17,6 @@ RUNTIME_CASM=$(count_ext '*.casm' runtime/casm)
 RUNTIME=$((RUNTIME_C+RUNTIME_RUST+RUNTIME_VAMPIR+RUNTIME_JVT+RUNTIME_CASM))
 
 BACKENDC=$(count src/Juvix/Compiler/Backend/C/)
-ISABELLE=$(count src/Juvix/Compiler/Backend/Isabelle/)
 CAIRO=$(count src/Juvix/Compiler/Backend/Cairo/)
 GEB=$(count src/Juvix/Compiler/Backend/Geb/)
 VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/)
@@ -35,14 +34,16 @@ 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/)
 STORE=$(count src/Juvix/Compiler/Store/)
 
 FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
-BACK=$((BACKENDC + GEB + VAMPIR + NOCK + ISABELLE + REG + ASM + TREE + CORE + CASM + CAIRO))
-OTHER=$((APP + STORE + HTML + EXTRA + DATA + PRELUDE))
+BACK=$((BACKENDC + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
+OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
 TESTS=$(count test/)
 
 TOTAL=$((FRONT+BACK+OTHER+TESTS))
@@ -58,7 +59,6 @@ echo "   GEB backend: $GEB LOC"
 echo "   C backend: $BACKENDC LOC"
 echo "   Cairo backend: $((CASM + CAIRO)) LOC"
 echo "   Nockma backend: $NOCK LOC"
-echo "   Isabelle backend: $ISABELLE LOC"
 echo "   JuvixReg: $REG LOC"
 echo "   JuvixAsm: $ASM LOC"
 echo "   JuvixTree: $TREE LOC"
@@ -73,6 +73,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"
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index ed6cecfb8a..5cd2a24af9 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -122,7 +122,7 @@ instance PrettyCode Theory where
           <> kwBegin
           <> line
           <> line
-          <> vsep stmts
+          <> vsep (punctuate line stmts)
           <> line
           <> line
           <> kwEnd
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 26dffa4a98..c2f7753bd8 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -80,7 +80,7 @@ goConstructorDef Internal.ConstructorDef {..} =
 
 goFunctionDef :: Internal.FunctionDef -> Statement
 goFunctionDef Internal.FunctionDef {..}
-  | null _funDefArgsInfo =
+  | argsNum == 0 =
       StmtDefinition
         Definition
           { _definitionName = _funDefName,
@@ -92,6 +92,8 @@ goFunctionDef Internal.FunctionDef {..}
           { _functionName = _funDefName,
             _functionType = goType _funDefType
           }
+  where
+    argsNum = length $ fst $ Internal.unfoldFunType _funDefType
 
 goAxiomDef :: Internal.AxiomDef -> Statement
 goAxiomDef Internal.AxiomDef {..}

From bb6eb26c11ba6915109891d0a659fdf71c5a6312 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 13:53:48 +0200
Subject: [PATCH 07/14] pipeline & primitive types

---
 app/Commands/Isabelle.hs                      |   9 +-
 .../Compiler/Backend/Isabelle/Data/Result.hs  |   9 +
 .../Backend/Isabelle/Translation/FromTyped.hs | 293 ++++++++++--------
 src/Juvix/Compiler/Pipeline.hs                |   7 +
 4 files changed, 184 insertions(+), 134 deletions(-)
 create mode 100644 src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index 23c47842ec..b076846a4c 100644
--- a/app/Commands/Isabelle.hs
+++ b/app/Commands/Isabelle.hs
@@ -2,9 +2,8 @@ module Commands.Isabelle where
 
 import Commands.Base
 import Commands.Isabelle.Options
+import Juvix.Compiler.Backend.Isabelle.Data.Result
 import Juvix.Compiler.Backend.Isabelle.Pretty
-import Juvix.Compiler.Backend.Isabelle.Translation.FromTyped
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 
 runCommand ::
   (Members '[EmbedIO, TaggedLock, App] r) =>
@@ -12,7 +11,7 @@ runCommand ::
   Sem r ()
 runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
-  res <- runPipelineNoOptions inputFile upToInternalTyped
-  let md = res ^. resultModule
-  renderStdOut (ppOutDefault (fromInternal md))
+  res <- runPipelineNoOptions inputFile upToIsabelle
+  let thy = res ^. resultTheory
+  renderStdOut (ppOutDefault thy)
   putStrLn ""
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs
new file mode 100644
index 0000000000..d11fbb4325
--- /dev/null
+++ b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs
@@ -0,0 +1,9 @@
+module Juvix.Compiler.Backend.Isabelle.Data.Result where
+
+import Juvix.Compiler.Backend.Isabelle.Language
+
+data Result = Result
+  { _resultTheory :: Theory
+  }
+
+makeLenses ''Result
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index c2f7753bd8..d7958f5d5c 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -1,155 +1,190 @@
 module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
 
+import Data.HashMap.Strict qualified as HashMap
+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 :: Internal.Module -> Theory
-fromInternal Internal.Module {..} =
+fromInternal ::
+  forall r.
+  (Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) =>
+  Internal.InternalTypedResult ->
+  Sem r Result
+fromInternal Internal.InternalTypedResult {..} = do
+  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
+  where
+    go :: Internal.InfoTable -> Internal.Module -> Sem r Result
+    go tab md = return $ Result $ goModule tab md
+
+goModule :: Internal.InfoTable -> Internal.Module -> Theory
+goModule infoTable Internal.Module {..} =
   Theory
     { _theoryName = _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
+  where
+    goMutualBlock :: Internal.MutualBlock -> [Statement]
+    goMutualBlock Internal.MutualBlock {..} = map goMutualStatement (toList _mutualStatements)
 
-goMutualBlock :: Internal.MutualBlock -> [Statement]
-goMutualBlock Internal.MutualBlock {..} = 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
+    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
+    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
               }
-  | otherwise =
-      StmtDatatype
-        Datatype
-          { _datatypeName = _inductiveName,
-            _datatypeParams = params,
-            _datatypeConstructors = map goConstructorDef _inductiveConstructors
-          }
-  where
-    params = map goInductiveParameter _inductiveParameters
+      where
+        params = map goInductiveParameter _inductiveParameters
 
-goInductiveParameter :: Internal.InductiveParameter -> Var
-goInductiveParameter Internal.InductiveParameter {..} = Var _inductiveParamName
+    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
+    goRecordField :: Internal.FunctionParameter -> RecordField
+    goRecordField Internal.FunctionParameter {..} =
+      RecordField
+        { _recordFieldName = fromMaybe defaultName _paramName,
+          _recordFieldType = goType _paramType
         }
-    defaultLoc = singletonInterval $ mkInitialLoc P.noFile
-    defaultId =
-      NameId
-        { _nameIdUid = 0,
-          _nameIdModuleId = ModuleId "" "" ""
+      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)
 
-goConstructorDef :: Internal.ConstructorDef -> Constructor
-goConstructorDef Internal.ConstructorDef {..} =
-  Constructor
-    { _constructorName = _inductiveConstructorName,
-      _constructorArgTypes = tyargs
-    }
-  where
-    tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
+    goFunctionDef :: Internal.FunctionDef -> Statement
+    goFunctionDef Internal.FunctionDef {..}
+      | argsNum == 0 =
+          StmtDefinition
+            Definition
+              { _definitionName = _funDefName,
+                _definitionType = goType _funDefType
+              }
+      | otherwise =
+          StmtFunction
+            Function
+              { _functionName = _funDefName,
+                _functionType = goType _funDefType
+              }
+      where
+        argsNum = length $ fst $ Internal.unfoldFunType _funDefType
 
-goFunctionDef :: Internal.FunctionDef -> Statement
-goFunctionDef Internal.FunctionDef {..}
-  | argsNum == 0 =
-      StmtDefinition
-        Definition
-          { _definitionName = _funDefName,
-            _definitionType = goType _funDefType
-          }
-  | otherwise =
-      StmtFunction
-        Function
-          { _functionName = _funDefName,
-            _functionType = goType _funDefType
-          }
-  where
-    argsNum = length $ fst $ Internal.unfoldFunType _funDefType
+    goAxiomDef :: Internal.AxiomDef -> Statement
+    goAxiomDef Internal.AxiomDef {..}
+      | argsNum == 0 =
+          StmtDefinition
+            Definition
+              { _definitionName = _axiomName,
+                _definitionType = goType _axiomType
+              }
+      | otherwise =
+          StmtFunction
+            Function
+              { _functionName = _axiomName,
+                _functionType = goType _axiomType
+              }
+      where
+        argsNum = length $ fst $ Internal.unfoldFunType _axiomType
 
-goAxiomDef :: Internal.AxiomDef -> Statement
-goAxiomDef Internal.AxiomDef {..}
-  | argsNum == 0 =
-      StmtDefinition
-        Definition
-          { _definitionName = _axiomName,
-            _definitionType = goType _axiomType
-          }
-  | otherwise =
-      StmtFunction
-        Function
-          { _functionName = _axiomName,
-            _functionType = goType _axiomType
-          }
-  where
-    argsNum = length $ fst $ Internal.unfoldFunType _axiomType
+    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)
 
-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 = case HashMap.lookup name (infoTable ^. Internal.infoInductives) of
+      Just ii -> case ii ^. Internal.inductiveInfoBuiltin of
+        Just Internal.BuiltinBool -> TyBool
+        Just Internal.BuiltinNat -> TyNat
+        Just Internal.BuiltinInt -> TyInt
+        --        Just Internal.BuiltinList -> TyList
+        _ -> TyInd $ IndApp name params
+      Nothing -> TyInd $ IndApp name params
 
-goTypeIden :: Internal.Iden -> Type
-goTypeIden = \case
-  Internal.IdenFunction name -> TyInd $ IndApp name []
-  Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
-  Internal.IdenVar name -> TyVar $ Var name
-  Internal.IdenAxiom name -> TyInd $ IndApp name []
-  Internal.IdenInductive name -> TyInd $ IndApp name []
+    goTypeIden :: Internal.Iden -> Type
+    goTypeIden = \case
+      Internal.IdenFunction name -> TyInd $ IndApp name []
+      Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
+      Internal.IdenVar name -> TyVar $ Var name
+      Internal.IdenAxiom name -> TyInd $ IndApp name []
+      Internal.IdenInductive name -> mkIndType name []
 
-goTypeApp :: Internal.Application -> Type
-goTypeApp app = TyInd $ IndApp 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)
+    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 {..} = TyFun $ FunType l r
-  where
-    l = goType (_functionLeft ^. Internal.paramType)
-    r = goType _functionRight
+    goTypeFun :: Internal.Function -> Type
+    goTypeFun Internal.Function {..} = TyFun $ FunType l r
+      where
+        l = goType (_functionLeft ^. Internal.paramType)
+        r = goType _functionRight
diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs
index 2bcc1a6aac..582f3d2fbd 100644
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@@ -16,6 +16,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.VampIR.Translation qualified as VampIR
 import Juvix.Compiler.Casm.Data.Builtins qualified as Casm
 import Juvix.Compiler.Casm.Data.Result qualified as Casm
@@ -92,6 +94,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, PathResolver] r) =>
   Sem r Core.CoreResult

From 82bc5a3bf42bb4357f2e642001e905404aba6b8a Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 15:45:58 +0200
Subject: [PATCH 08/14] CLI

---
 app/Commands/Isabelle.hs                      | 19 +++++++++++++++++--
 app/Commands/Isabelle/Options.hs              | 12 ++++++------
 .../Compiler/Backend/Isabelle/Data/Result.hs  |  3 ++-
 .../Compiler/Backend/Isabelle/Pretty/Base.hs  |  3 +--
 .../Backend/Isabelle/Translation/FromTyped.hs |  7 ++++++-
 src/Juvix/Data/FileExt.hs                     |  3 +++
 src/Juvix/Prelude/Prepath.hs                  |  6 +++++-
 7 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index b076846a4c..999dc745f1 100644
--- a/app/Commands/Isabelle.hs
+++ b/app/Commands/Isabelle.hs
@@ -2,6 +2,7 @@ module Commands.Isabelle where
 
 import Commands.Base
 import Commands.Isabelle.Options
+import Data.Text.IO qualified as Text
 import Juvix.Compiler.Backend.Isabelle.Data.Result
 import Juvix.Compiler.Backend.Isabelle.Pretty
 
@@ -13,5 +14,19 @@ runCommand opts = do
   let inputFile = opts ^. isabelleInputFile
   res <- runPipelineNoOptions inputFile upToIsabelle
   let thy = res ^. resultTheory
-  renderStdOut (ppOutDefault thy)
-  putStrLn ""
+  outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
+  if
+      | opts ^. isabelleStdout -> do
+          renderStdOut (ppOutDefault thy)
+          putStrLn ""
+      | otherwise -> do
+          ensureDir outputDir
+          let file :: Path Rel File
+              file =
+                relFile
+                  ( unpack (res ^. resultModuleId . moduleIdPath)
+                      <.> isabelleFileExt
+                  )
+              absPath :: Path Abs File
+              absPath = outputDir <//> file
+          liftIO $ Text.writeFile (toFilePath absPath) (ppPrint thy)
diff --git a/app/Commands/Isabelle/Options.hs b/app/Commands/Isabelle/Options.hs
index ca14968d44..34c057e9a6 100644
--- a/app/Commands/Isabelle/Options.hs
+++ b/app/Commands/Isabelle/Options.hs
@@ -5,7 +5,7 @@ import CommonOptions
 data IsabelleOptions = IsabelleOptions
   { _isabelleInputFile :: Maybe (AppPath File),
     _isabelleOutputDir :: AppPath Dir,
-    _isabelleRecursive :: Bool
+    _isabelleStdout :: Bool
   }
   deriving stock (Data)
 
@@ -13,11 +13,6 @@ makeLenses ''IsabelleOptions
 
 parseIsabelle :: Parser IsabelleOptions
 parseIsabelle = do
-  _isabelleRecursive <-
-    switch
-      ( long "recursive"
-          <> help "Process imported modules recursively"
-      )
   _isabelleOutputDir <-
     parseGenericOutputDir
       ( value "isabelle"
@@ -25,5 +20,10 @@ parseIsabelle = do
           <> help "Isabelle/HOL output directory"
           <> action "directory"
       )
+  _isabelleStdout <-
+    switch
+      ( long "stdout"
+          <> help "Write the output to stdout instead of a file"
+      )
   _isabelleInputFile <- optional (parseInputFile FileExtJuvix)
   pure IsabelleOptions {..}
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs
index d11fbb4325..3c13082b6c 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs
@@ -3,7 +3,8 @@ module Juvix.Compiler.Backend.Isabelle.Data.Result where
 import Juvix.Compiler.Backend.Isabelle.Language
 
 data Result = Result
-  { _resultTheory :: Theory
+  { _resultTheory :: Theory,
+    _resultModuleId :: ModuleId
   }
 
 makeLenses ''Result
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index 5cd2a24af9..d4902d83f6 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -110,14 +110,13 @@ instance PrettyCode RecordField where
 instance PrettyCode Theory where
   ppCode Theory {..} = do
     n <- ppCode _theoryName
-    imps <- mapM ppCode _theoryImports
     stmts <- mapM ppCode _theoryStatements
     return $
       kwTheory
         <+> n
           <> line
           <> kwImports
-        <+> hsep ("Main" : imps)
+        <+> "Main"
           <> line
           <> kwBegin
           <> line
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index d7958f5d5c..5e9384244d 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -28,7 +28,12 @@ fromInternal Internal.InternalTypedResult {..} = do
   go table _resultModule
   where
     go :: Internal.InfoTable -> Internal.Module -> Sem r Result
-    go tab md = return $ Result $ goModule tab md
+    go tab md =
+      return $
+        Result
+          { _resultTheory = goModule tab md,
+            _resultModuleId = md ^. Internal.moduleId
+          }
 
 goModule :: Internal.InfoTable -> Internal.Module -> Theory
 goModule infoTable Internal.Module {..} =
diff --git a/src/Juvix/Data/FileExt.hs b/src/Juvix/Data/FileExt.hs
index dda274981f..2b7f2a4989 100644
--- a/src/Juvix/Data/FileExt.hs
+++ b/src/Juvix/Data/FileExt.hs
@@ -82,6 +82,9 @@ htmlFileExt = ".html"
 markdownFileExt :: (IsString a) => a
 markdownFileExt = ".md"
 
+isabelleFileExt :: (IsString a) => a
+isabelleFileExt = ".thy"
+
 cFileExt :: (IsString a) => a
 cFileExt = ".c"
 
diff --git a/src/Juvix/Prelude/Prepath.hs b/src/Juvix/Prelude/Prepath.hs
index b3e0731e9f..b94765d9d4 100644
--- a/src/Juvix/Prelude/Prepath.hs
+++ b/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

From 75a545afcc7fa4b15e0c8b96dd8cadffc09fdb92 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 15:57:14 +0200
Subject: [PATCH 09/14] CLI

---
 app/Commands/Isabelle.hs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index 999dc745f1..771ac74273 100644
--- a/app/Commands/Isabelle.hs
+++ b/app/Commands/Isabelle.hs
@@ -2,7 +2,6 @@ module Commands.Isabelle where
 
 import Commands.Base
 import Commands.Isabelle.Options
-import Data.Text.IO qualified as Text
 import Juvix.Compiler.Backend.Isabelle.Data.Result
 import Juvix.Compiler.Backend.Isabelle.Pretty
 
@@ -29,4 +28,4 @@ runCommand opts = do
                   )
               absPath :: Path Abs File
               absPath = outputDir <//> file
-          liftIO $ Text.writeFile (toFilePath absPath) (ppPrint thy)
+          writeFileEnsureLn absPath (ppPrint thy <> "\n")

From 535a4fd57867344978b2c455ca6c8adaded62a32 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 16:51:42 +0200
Subject: [PATCH 10/14] refactor

---
 .../Compiler/Backend/Isabelle/Language.hs     | 15 +++++-----
 .../Compiler/Backend/Isabelle/Pretty/Base.hs  | 10 +++++--
 .../Backend/Isabelle/Translation/FromTyped.hs | 30 +++++++++++--------
 3 files changed, 32 insertions(+), 23 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
index c1ce9885ba..9876cdaa6e 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -10,9 +10,6 @@ import Juvix.Prelude
 
 data Type
   = TyVar Var
-  | TyBool
-  | TyNat
-  | TyInt
   | TyFun FunType
   | TyInd IndApp
   deriving stock (Eq)
@@ -28,8 +25,15 @@ data FunType = FunType
   }
   deriving stock (Eq)
 
+data Inductive
+  = IndBool
+  | IndNat
+  | IndInt
+  | IndUser Name
+  deriving stock (Eq)
+
 data IndApp = IndApp
-  { _indAppInductive :: Name,
+  { _indAppInductive :: Inductive,
     _indAppParams :: [Type]
   }
   deriving stock (Eq)
@@ -104,9 +108,6 @@ instance HasAtomicity Var where
 instance HasAtomicity Type where
   atomicity = \case
     TyVar {} -> Atom
-    TyBool -> Atom
-    TyNat -> Atom
-    TyInt -> Atom
     TyFun {} -> Aggregate funFixity
     TyInd IndApp {..}
       | null _indAppParams -> Atom
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index d4902d83f6..cac392a49e 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -33,9 +33,6 @@ instance PrettyCode Name where
 instance PrettyCode Type where
   ppCode = \case
     TyVar v -> ppCode v
-    TyBool -> return $ primitive "bool"
-    TyNat -> return $ primitive "nat"
-    TyInt -> return $ primitive "int"
     TyFun x -> ppCode x
     TyInd x -> ppCode x
 
@@ -49,6 +46,13 @@ instance PrettyCode FunType where
     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"
+    IndUser name -> ppCode name
+
 instance PrettyCode IndApp where
   ppCode IndApp {..} = do
     params <- ppParams _indAppParams
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 5e9384244d..f465060cce 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -160,21 +160,23 @@ goModule infoTable Internal.Module {..} =
         unsupportedType e = error ("unsupported type: " <> Internal.ppTrace e)
 
     mkIndType :: Name -> [Type] -> Type
-    mkIndType name params = case HashMap.lookup name (infoTable ^. Internal.infoInductives) of
-      Just ii -> case ii ^. Internal.inductiveInfoBuiltin of
-        Just Internal.BuiltinBool -> TyBool
-        Just Internal.BuiltinNat -> TyNat
-        Just Internal.BuiltinInt -> TyInt
-        --        Just Internal.BuiltinList -> TyList
-        _ -> TyInd $ IndApp name params
-      Nothing -> TyInd $ IndApp name params
+    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 -> TyList
+            _ -> IndUser name
+          Nothing -> IndUser name
 
     goTypeIden :: Internal.Iden -> Type
     goTypeIden = \case
-      Internal.IdenFunction name -> TyInd $ IndApp name []
+      Internal.IdenFunction name -> mkIndType name []
       Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name)
       Internal.IdenVar name -> TyVar $ Var name
-      Internal.IdenAxiom name -> TyInd $ IndApp name []
+      Internal.IdenAxiom name -> mkIndType name []
       Internal.IdenInductive name -> mkIndType name []
 
     goTypeApp :: Internal.Application -> Type
@@ -189,7 +191,9 @@ goModule infoTable Internal.Module {..} =
           _ -> error ("unsupported type: " <> Internal.ppTrace app)
 
     goTypeFun :: Internal.Function -> Type
-    goTypeFun Internal.Function {..} = TyFun $ FunType l r
+    goTypeFun Internal.Function {..} = case lty of
+      Internal.ExpressionUniverse {} -> goType _functionRight
+      _ ->
+        TyFun $ FunType (goType lty) (goType _functionRight)
       where
-        l = goType (_functionLeft ^. Internal.paramType)
-        r = goType _functionRight
+        lty = _functionLeft ^. Internal.paramType

From 242e0291eb7e056b8c543c3ef36a22458929c82a Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 16:55:44 +0200
Subject: [PATCH 11/14] primitive lists & strings

---
 src/Juvix/Compiler/Backend/Isabelle/Language.hs           | 2 ++
 src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs        | 2 ++
 .../Compiler/Backend/Isabelle/Translation/FromTyped.hs    | 8 ++++++--
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
index 9876cdaa6e..07aab35977 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -29,6 +29,8 @@ data Inductive
   = IndBool
   | IndNat
   | IndInt
+  | IndList
+  | IndString
   | IndUser Name
   deriving stock (Eq)
 
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
index cac392a49e..1924fc9a53 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs
@@ -51,6 +51,8 @@ instance PrettyCode Inductive where
     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
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index f465060cce..4e81d8bf49 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -167,9 +167,13 @@ goModule infoTable Internal.Module {..} =
             Just Internal.BuiltinBool -> IndBool
             Just Internal.BuiltinNat -> IndNat
             Just Internal.BuiltinInt -> IndInt
-            --        Just Internal.BuiltinList -> TyList
+            Just Internal.BuiltinList -> IndList
             _ -> IndUser name
-          Nothing -> 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

From 998bc24b21914b6cae800a598769f06a4882071e Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 17:16:33 +0200
Subject: [PATCH 12/14] type synonyms

---
 .../Backend/Isabelle/Translation/FromTyped.hs | 56 +++++++++----------
 1 file changed, 26 insertions(+), 30 deletions(-)

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 4e81d8bf49..ed14cfcfbe 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -108,39 +108,35 @@ goModule infoTable Internal.Module {..} =
       where
         tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
 
-    goFunctionDef :: Internal.FunctionDef -> Statement
-    goFunctionDef Internal.FunctionDef {..}
-      | argsNum == 0 =
-          StmtDefinition
-            Definition
-              { _definitionName = _funDefName,
-                _definitionType = goType _funDefType
-              }
-      | otherwise =
-          StmtFunction
-            Function
-              { _functionName = _funDefName,
-                _functionType = goType _funDefType
-              }
+    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 _funDefType
+        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 {..}
-      | argsNum == 0 =
-          StmtDefinition
-            Definition
-              { _definitionName = _axiomName,
-                _definitionType = goType _axiomType
-              }
-      | otherwise =
-          StmtFunction
-            Function
-              { _functionName = _axiomName,
-                _functionType = goType _axiomType
-              }
-      where
-        argsNum = length $ fst $ Internal.unfoldFunType _axiomType
+    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType Nothing
 
     goType :: Internal.Expression -> Type
     goType ty = case ty of

From 95f54ab8480d3ef0577a70047de957ef553ca6e2 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 24 Apr 2024 17:30:29 +0200
Subject: [PATCH 13/14] --only-types option

---
 app/Commands/Isabelle.hs                      |  2 +-
 app/Commands/Isabelle/Options.hs              | 16 +++++++++---
 .../Backend/Isabelle/Translation/FromTyped.hs | 25 +++++++++++++------
 src/Juvix/Compiler/Pipeline/EntryPoint.hs     |  6 +++--
 4 files changed, 36 insertions(+), 13 deletions(-)

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index 771ac74273..6dab92bfc9 100644
--- 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
index 34c057e9a6..a06981da63 100644
--- 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
index ed14cfcfbe..734cef5f7f 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -18,6 +18,7 @@ fromInternal ::
   Internal.InternalTypedResult ->
   Sem r Result
 fromInternal Internal.InternalTypedResult {..} = do
+  onlyTypes <- (^. entryPointIsabelleOnlyTypes) <$> ask
   itab <- getInternalModuleTable <$> ask
   let md :: Internal.InternalModule
       md = _resultInternalModule
@@ -25,26 +26,36 @@ fromInternal Internal.InternalTypedResult {..} = do
       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
index df6403e1f8..f437febb5c 100644
--- 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

From da8f71f301a7fe308640796db12e584ea2f34b3e Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Tue, 7 May 2024 18:58:19 +0200
Subject: [PATCH 14/14] use theory names without dots

---
 app/Commands/Isabelle.hs                                  | 3 ++-
 .../Compiler/Backend/Isabelle/Translation/FromTyped.hs    | 8 +++++++-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs
index 6dab92bfc9..98ab281ad0 100644
--- a/app/Commands/Isabelle.hs
+++ b/app/Commands/Isabelle.hs
@@ -3,6 +3,7 @@ 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 ::
@@ -23,7 +24,7 @@ runCommand opts = do
           let file :: Path Rel File
               file =
                 relFile
-                  ( unpack (res ^. resultModuleId . moduleIdPath)
+                  ( unpack (thy ^. theoryName . namePretty)
                       <.> isabelleFileExt
                   )
               absPath :: Path Abs File
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 734cef5f7f..2fc57b1394 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -1,6 +1,7 @@
 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
@@ -39,11 +40,16 @@ fromInternal Internal.InternalTypedResult {..} = do
 goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
 goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = _moduleName,
+    { _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