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:
- #2763

---------

Co-authored-by: Jonathan Cubides <[email protected]>

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,14 +35,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 + 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