mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 10:03:22 +03:00
bf6603eb33
GEB 0.3.2 introduces the following changes. * The STLC frontend no longer requires full type information in terms. The syntax of the terms changed. * An error node has been introduced which allows to compile Juvix `fail` nodes. The following features required for compilation from Juvix are still missing in GEB. * Modular arithmetic types ([GEB issue #61](https://github.com/anoma/geb/issues/61)). * Functor/algebra iteration to implement bounded inductive types ([GEB issue #62](https://github.com/anoma/geb/issues/62)).
27 lines
850 B
Haskell
27 lines
850 B
Haskell
module Commands.Dev.Geb.Check where
|
|
|
|
import Commands.Base
|
|
import Commands.Dev.Geb.Infer.Options
|
|
import Juvix.Compiler.Backend.Geb qualified as Geb
|
|
import Juvix.Compiler.Backend.Geb.Pretty
|
|
|
|
runCommand ::
|
|
forall r.
|
|
(Member App r, Member (Embed IO) r) =>
|
|
GebInferOptions ->
|
|
Sem r ()
|
|
runCommand opts = do
|
|
let b :: AppPath File
|
|
b = opts ^. gebInferOptionsInputFile
|
|
f :: Path Abs File <- fromAppPathFile b
|
|
content :: Text <- embed (readFile (toFilePath f))
|
|
case Geb.runParser f content of
|
|
Right (Geb.ExpressionMorphism morph) -> do
|
|
case Geb.inferObject' morph of
|
|
Left err -> exitJuvixError (JuvixError err)
|
|
Right ty -> do
|
|
renderStdOut (ppOutDefault ty)
|
|
embed (putStrLn "")
|
|
Right _ -> exitJuvixError (error @JuvixError "Not a morphism")
|
|
Left err -> exitJuvixError (JuvixError err)
|