mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
0ef464668d
This PR adds support for all recent changes in GEB introduced by: - https://github.com/anoma/geb/pull/70 - Closes #1814 Summary: - [x] Add LeftInj, RightIng, and Absurd types in GEB language - [x] Fix FromCore translation for the new data types and minor code styling issues. - [x] Fix GEB-STLC type inference and checking - [X] Add support for evaluating typed morphism "(typed ...)" in the Geb repl and .geb files. - [x] Simplify a bit the Geb parser - [x] Fix `dev geb check` command - [x] Type check files in `tests/Geb/positive` After this PR, we should include interval location for Geb terms to facility debugging type-checking errors.
33 lines
1.1 KiB
Haskell
33 lines
1.1 KiB
Haskell
module Commands.Dev.Geb.Infer where
|
|
|
|
import Commands.Base
|
|
import Commands.Dev.Geb.Infer.Options
|
|
import Juvix.Compiler.Backend.Geb qualified as Geb
|
|
|
|
runCommand ::
|
|
forall r.
|
|
(Member App r, Member (Embed IO) r) =>
|
|
GebInferOptions ->
|
|
Sem r ()
|
|
runCommand opts = do
|
|
let b :: SomeBase File
|
|
b = opts ^. gebInferOptionsInputFile . pathPath
|
|
f :: Path Abs File <- someBaseToAbs' b
|
|
content :: Text <- embed (readFile (toFilePath f))
|
|
case Geb.runParser f content of
|
|
Right (Geb.ExpressionMorphism gebTerm) ->
|
|
case Geb.inferObject' gebTerm of
|
|
Left err -> exitJuvixError (JuvixError err)
|
|
Right obj -> renderStdOut (Geb.ppOut opts obj)
|
|
Right (Geb.ExpressionTypedMorphism tyMorph) -> do
|
|
case run . runError @Geb.CheckingError $ Geb.check' tyMorph of
|
|
Left err -> exitJuvixError (JuvixError err)
|
|
Right _ ->
|
|
renderStdOut $
|
|
Geb.ppOut
|
|
opts
|
|
(tyMorph ^. Geb.typedMorphismObject)
|
|
Right (Geb.ExpressionObject _) ->
|
|
exitJuvixError (error @JuvixError "No inference for objects")
|
|
Left err -> exitJuvixError (JuvixError err)
|