mirror of
https://github.com/anoma/juvix.git
synced 2024-12-04 17:07:28 +03:00
b9d864123a
* Closes #2962 * Depends on #2963 * In Isabelle/HOL comments cannot appear in internal syntax. All comments inside a Juvix definition are moved outside: to before the definition or before the earliest function clause. --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
34 lines
1.0 KiB
Haskell
34 lines
1.0 KiB
Haskell
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 AppEffects r) =>
|
|
IsabelleOptions ->
|
|
Sem r ()
|
|
runCommand opts = do
|
|
let inputFile = opts ^. isabelleInputFile
|
|
res <- runPipeline opts inputFile upToIsabelle
|
|
let thy = res ^. resultTheory
|
|
comments = res ^. resultComments
|
|
outputDir <- fromAppPathDir (opts ^. isabelleOutputDir)
|
|
if
|
|
| opts ^. isabelleStdout -> do
|
|
renderStdOut (ppOutDefault comments thy)
|
|
putStrLn ""
|
|
| otherwise -> do
|
|
ensureDir outputDir
|
|
let file :: Path Rel File
|
|
file =
|
|
relFile
|
|
( unpack (thy ^. theoryName . namePretty)
|
|
<.> isabelleFileExt
|
|
)
|
|
absPath :: Path Abs File
|
|
absPath = outputDir <//> file
|
|
writeFileEnsureLn absPath (ppPrint comments thy <> "\n")
|